Package | Description |
---|---|
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
Modifier and Type | Method and Description |
---|---|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerDiv(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer division.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerGeq(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the greater or equal.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerGt(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the greater than.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerLeq(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the less or equal.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerLt(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the less than.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerMinus(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer minus.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerMod(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer modulo.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerMult(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer multiplication.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerPlus(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer plus.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerUnaryMinus(java.lang.StringBuffer arg)
Translate a unary minus.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateIntegerValue(long val)
Translate a sort.
|
java.lang.StringBuffer |
SMTObjTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings) |
java.lang.StringBuffer |
AbstractSMTTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings) |
java.lang.CharSequence |
SMTTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings)
Translates a problem into the given syntax.
|
SMTFile |
SMTObjTranslator.translateProblem(Term problem)
Translates a KeY problem into a SMTFile.
|
java.util.ArrayList<java.lang.StringBuffer> |
AbstractSMTTranslator.translateTaclets(Services services,
SMTSettings settings)
Translates the list
tacletFormulae to the given syntax. |
SMTTerm |
SMTObjTranslator.translateTerm(Term term)
Translates a KeY term to an SMT term.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateTerm(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Translates the given term into input syntax and adds the resulting
string to the StringBuffer sb.
|
protected java.lang.StringBuffer |
SmtLibTranslator.translateTermIfThenElse(java.lang.StringBuffer cond,
java.lang.StringBuffer ifterm,
java.lang.StringBuffer elseterm) |
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateTermIfThenElse(java.lang.StringBuffer cond,
java.lang.StringBuffer ifterm,
java.lang.StringBuffer elseterm)
Translate the if_then_else construct for terms (i.e.
|
protected java.lang.StringBuffer |
SmtLib2Translator.translateTermIfThenElse(java.lang.StringBuffer cond,
java.lang.StringBuffer ifterm,
java.lang.StringBuffer elseterm) |
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateUniqueness(AbstractSMTTranslator.FunctionWrapper function,
java.util.Collection<AbstractSMTTranslator.FunctionWrapper> distinct)
Translates the unique-property of a function.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateUnknown(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Takes care of sequent tree parts that were not matched in
translate(term, skolemization).
|
Copyright © 2003-2019 The KeY-Project.