public abstract class AbstractSMTTranslator extends Object implements SMTTranslator
Modifier and Type | Class and Description |
---|---|
static class |
AbstractSMTTranslator.Configuration |
protected static class |
AbstractSMTTranslator.FunctionWrapper
remember all function declarations
|
Modifier and Type | Field and Description |
---|---|
private ArrayList<StringBuffer> |
assumptions |
private static String |
BPROD_STRING |
private static String |
BSUM_STRING |
private StringBuffer |
castPredicate
This stringbuffer is used as predicate name for casts from int-valued
to u-valued obects
|
private AbstractSMTTranslator.Configuration |
config |
private HashMap<Long,StringBuffer> |
constantsForBigIntegers
If a integer is not supported by a solver because it is too big, the
integer is translated into a constant.
|
private HashMap<Long,StringBuffer> |
constantsForSmallIntegers
If a integer is not supported by a solver because it is too small,
the integer is translated into a constant.
|
private HashMap<Term,StringBuffer> |
constantTypePreds |
private Collection<Throwable> |
exceptionsForTacletTranslation |
private HashMap<Operator,ArrayList<Sort>> |
functionDecls |
private Sort |
integerSort |
private HashMap<Term,StringBuffer> |
modalityPredicates
map used for storing predicates representing modalities or updates
|
private Function |
multiplicationFunction
If the solver supports only simple multiplications, complex
multiplications are translated into a uninterpreted function.
|
private int |
nameCounter |
private HashMap<Operator,ArrayList<Sort>> |
predicateDecls |
private SMTSettings |
smtSettings |
private HashSet<Function> |
specialFunctions |
private StringBuffer |
standardSort
The string used as standard sort for translations
|
private ArrayList<StringBuffer> |
tacletAssumptions
Assumptions made of taclets - the translation of
tacletFormulae |
private TacletSetTranslation |
tacletSetTranslation
Formulae made of taclets, used for assumptions.
|
private TermBuilder |
tb |
protected String |
text
The translation result is stored in this variable.
|
private HashMap<Sort,StringBuffer> |
typePredicates |
private HashMap<Term,StringBuffer> |
uninterpretedBindingFunctionNames |
private HashMap<Term,StringBuffer> |
uninterpretedBindingPredicateNames |
private HashMap<Term,StringBuffer> |
usedBprodTerms |
private HashMap<Term,StringBuffer> |
usedBsumTerms |
protected HashMap<Sort,StringBuffer> |
usedDisplaySort |
private HashMap<Operator,StringBuffer> |
usedFunctionNames |
private Collection<AbstractSMTTranslator.FunctionWrapper> |
usedFunctions |
private HashMap<Operator,StringBuffer> |
usedPredicateNames |
protected HashMap<Sort,StringBuffer> |
usedRealSort |
private HashMap<Operator,StringBuffer> |
usedVariableNames |
protected static int |
YESNOT |
Constructor and Description |
---|
AbstractSMTTranslator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
AbstractSMTTranslator(Services s,
AbstractSMTTranslator.Configuration config)
For translating only terms and not complete sequents.
|
Modifier and Type | Method and Description |
---|---|
private void |
addConstantTypePredicate(Term term,
StringBuffer name) |
private void |
addFunction(Operator op,
ArrayList<Sort> sorts,
Sort result) |
private void |
addPredicate(Operator op,
ArrayList<Sort> sorts) |
private void |
addSpecialFunction(Function fun)
Add an interpreted function to the set of special functions.
|
private void |
addTypePredicate(StringBuffer sortname,
Sort s)
Create a type predicate for a given sort.
|
private ArrayList<StringBuffer> |
buildAssumptionsForIntegers() |
private ArrayList<StringBuffer> |
buildAssumptionsForIntegers(Collection<StringBuffer> constants,
boolean upperBound) |
private ArrayList<StringBuffer> |
buildAssumptionsForSorts(TermServices services) |
private ArrayList<StringBuffer> |
buildAssumptionsForUninterpretedMultiplication(Services services) |
protected abstract StringBuffer |
buildCompleteText(StringBuffer formula,
ArrayList<StringBuffer> assum,
ArrayList<ContextualBlock> assumptionBlocks,
ArrayList<ArrayList<StringBuffer>> functions,
ArrayList<ArrayList<StringBuffer>> predicates,
ArrayList<ContextualBlock> predicateBlocks,
ArrayList<StringBuffer> types,
SortHierarchy sortHierarchy,
SMTSettings settings)
Build the text, that can be read by the final decider.
|
private StringBuffer |
buildComplText(Services serv,
StringBuffer formula,
SMTSettings settings) |
private StringBuffer |
buildGeneralHierarchyPredicate(SortWrapper child,
SortWrapper parent) |
protected StringBuffer |
buildInjectiveFunctionAssumption(AbstractSMTTranslator.FunctionWrapper fw) |
private StringBuffer |
buildInstantiatedHierarchyPredicate(SortWrapper child,
SortWrapper parent,
StringBuffer constant) |
private SortHierarchy |
buildSortHierarchy(Services services,
SMTSettings settings)
Build the sorthierarchy for the sorts If null was used, add
typepredicates for all types.
|
private ArrayList<ArrayList<StringBuffer>> |
buildTranslatedFuncDecls(TermServices services)
Build the translated function declarations.
|
private ArrayList<ArrayList<StringBuffer>> |
buildTranslatedPredDecls(ArrayList<ContextualBlock> predicateTypes)
Build the translated predicate declarations.
|
private ArrayList<StringBuffer> |
buildTranslatedSorts()
ArrayList of all sorts, that were used as sorts.
|
private ArrayList<StringBuffer> |
buildUniqueAssumptions() |
private StringBuffer |
buildUniqueConstant(long integer,
TermServices services) |
private StringBuffer |
cast(StringBuffer formula)
Cast a formula of type int to type u.
|
private StringBuffer |
castIfNeccessary(StringBuffer formula,
Sort formulaSort,
Sort targetSort)
This method adds a type cast to a translated formula, if neccessary.
|
private StringBuffer |
createGenericVariable(int pos) |
protected ArrayList<StringBuffer> |
createGenericVariables(int count,
int start) |
private Term |
createLogicalVar(TermServices services,
String baseName,
Sort sort) |
private ArrayList<Sort> |
getArgSorts(Function function) |
private ArrayList<StringBuffer> |
getAssumptions(Services services,
ArrayList<ContextualBlock> assumptionTypes,
SMTSettings settings)
get the assumptions made by the logic.
|
protected abstract StringBuffer |
getBoolSort()
The String used for boolean values.
|
AbstractSMTTranslator.Configuration |
getConfig() |
Collection<Throwable> |
getExceptionsOfTacletTranslation()
Returns all exceptions that have occurred while translating the taclets.
|
protected abstract StringBuffer |
getIntegerSort()
The String used for integer values.
|
private long |
getMaxNumber()
Returns the maximum number that is supported by the solver.
|
private long |
getMinNumber()
Returns the minimum number that is supported by the solver.
|
private StringBuffer |
getModalityPredicate(Term t,
Vector<QuantifiableVariable> quantifiedVars,
Services services)
Get a predicate representing a modality.
|
private Function |
getMultiplicationFunction(Services services) |
private StringBuffer |
getNameForIntegerConstant(TermServices services,
long integer) |
protected abstract StringBuffer |
getNullName() |
private Long |
getRightBorderAsInteger(long integer,
TermServices services) |
private Term |
getRightBorderAsTerm(long integer,
TermServices services) |
private HashMap<Long,StringBuffer> |
getRightConstantContainer(long integer) |
protected SMTSettings |
getSettings() |
private StringBuffer |
getSingleFunctionDef(StringBuffer funName,
ArrayList<Sort> sorts)
Get the type predicate definition for a given function.
|
private ArrayList<StringBuffer> |
getSortHierarchyPredicates(Services services,
SMTSettings settings)
Get the expression for that defines the typepredicates for sort
hierarchy.
|
private ArrayList<StringBuffer> |
getSpecialSortPredicates(Services services)
build the formulas, that make sure, special functions keep typing
|
TacletSetTranslation |
getTacletSetTranslation() |
private ArrayList<StringBuffer> |
getTypeDefinitions()
Returns a set of formula s, that defines the resulttypes of
functions, all constants and other elements (i.e.
|
protected StringBuffer |
getTypePredicate(Sort s,
StringBuffer arg)
Get the type predicate for the given sort and the given expression.
|
private boolean |
hasNumberLimit()
returns
true if the format supports only integers within
a certain interval. |
private boolean |
isComplexMultiplication(Services services,
Term t1,
Term t2) |
protected abstract boolean |
isMultiSorted()
Returns, whether the Structure, this translator creates should be a
Structure, that is multi sorted.
|
private boolean |
isNumberSymbol(Services services,
Operator op) |
protected boolean |
isSomeIntegerSort(Sort s) |
private boolean |
isUsingUninterpretedMultiplication() |
protected StringBuffer |
makeUnique(StringBuffer name) |
private StringBuffer |
removeIllegalChars(StringBuffer template,
ArrayList<String> toReplace,
ArrayList<String> replacement) |
private StringBuffer |
translateAsBindingUninterpretedFunction(Term term,
Function fun,
Vector<QuantifiableVariable> quantifiedVars,
ImmutableArray<Term> subs,
Services services)
Translate an uninterpreted function, which binds variables
|
private StringBuffer |
translateAsBindingUninterpretedPredicate(Term term,
Function fun,
Vector<QuantifiableVariable> quantifiedVars,
ImmutableArray<Term> subs,
Services services) |
private StringBuffer |
translateAsUninterpretedFunction(Function fun,
Vector<QuantifiableVariable> quantifiedVars,
ImmutableArray<Term> subs,
Services services) |
protected StringBuffer |
translateBprodFunction(Term bprodterm,
ArrayList<StringBuffer> sub)
translate a bprod function.
|
protected StringBuffer |
translateBsumFunction(Term bsumterm,
ArrayList<StringBuffer> sub)
translate a bsum function.
|
protected StringBuffer |
translateComment(int newLines,
String comment) |
protected StringBuffer |
translateDistinct(AbstractSMTTranslator.FunctionWrapper[] functions) |
protected StringBuffer |
translateFunc(Operator o,
ArrayList<StringBuffer> sub)
translate a function.
|
protected abstract StringBuffer |
translateFunction(StringBuffer name,
ArrayList<StringBuffer> args)
Translate a function.
|
protected abstract StringBuffer |
translateFunctionName(StringBuffer name)
Get the name for a function symbol.
|
protected StringBuffer |
translateIntegerDiv(StringBuffer arg1,
StringBuffer arg2)
Translate the integer division.
|
protected StringBuffer |
translateIntegerGeq(StringBuffer arg1,
StringBuffer arg2)
Translate the greater or equal.
|
protected StringBuffer |
translateIntegerGt(StringBuffer arg1,
StringBuffer arg2)
Translate the greater than.
|
protected StringBuffer |
translateIntegerLeq(StringBuffer arg1,
StringBuffer arg2)
Translate the less or equal.
|
protected StringBuffer |
translateIntegerLt(StringBuffer arg1,
StringBuffer arg2)
Translate the less than.
|
protected StringBuffer |
translateIntegerMinus(StringBuffer arg1,
StringBuffer arg2)
Translate the integer minus.
|
protected StringBuffer |
translateIntegerMod(StringBuffer arg1,
StringBuffer arg2)
Translate the integer modulo.
|
protected StringBuffer |
translateIntegerMult(StringBuffer arg1,
StringBuffer arg2)
Translate the integer multiplication.
|
protected StringBuffer |
translateIntegerPlus(StringBuffer arg1,
StringBuffer arg2)
Translate the integer plus.
|
protected StringBuffer |
translateIntegerUnaryMinus(StringBuffer arg)
Translate a unary minus.
|
protected StringBuffer |
translateIntegerValue(long val)
Translate a sort.
|
protected StringBuffer |
translateLogicalAll(ArrayList<StringBuffer> variables,
ArrayList<Sort> sorts,
StringBuffer result) |
protected StringBuffer |
translateLogicalAll(StringBuffer var,
Sort sort,
StringBuffer result) |
protected abstract StringBuffer |
translateLogicalAll(StringBuffer var,
StringBuffer type,
StringBuffer form)
Build the logical forall formula.
|
protected abstract StringBuffer |
translateLogicalAnd(StringBuffer arg1,
StringBuffer arg2)
Build the logical konjunction.
|
protected abstract StringBuffer |
translateLogicalConstant(StringBuffer name)
Build the Stringbuffer for an constant.
|
protected abstract StringBuffer |
translateLogicalEquivalence(StringBuffer arg1,
StringBuffer arg2)
Build the logical equivalence.
|
protected abstract StringBuffer |
translateLogicalExist(StringBuffer var,
StringBuffer type,
StringBuffer form)
Build the logical exists formula.
|
protected abstract StringBuffer |
translateLogicalFalse()
Translate the logical false.
|
protected abstract StringBuffer |
translateLogicalIfThenElse(StringBuffer cond,
StringBuffer ifterm,
StringBuffer elseterm)
Translate the logical if_then_else construct.
|
protected abstract StringBuffer |
translateLogicalImply(StringBuffer arg1,
StringBuffer arg2)
Build the logical implication.
|
protected abstract StringBuffer |
translateLogicalNot(StringBuffer arg)
Build the Stringbuffer for a logical NOT.
|
protected abstract StringBuffer |
translateLogicalOr(StringBuffer arg1,
StringBuffer arg2)
Build the logical disjunction.
|
protected abstract StringBuffer |
translateLogicalTrue()
Translate the logical true.
|
protected abstract StringBuffer |
translateLogicalVar(StringBuffer name)
Build the Stringbuffer for an variable.
|
protected abstract StringBuffer |
translateNull()
Translate the NULL element
|
protected abstract StringBuffer |
translateNullSort()
Translate the NULL element's Sort.
|
protected abstract StringBuffer |
translateObjectEqual(StringBuffer arg1,
StringBuffer arg2)
Build the Stringbuffer for an object equivalence.
|
private StringBuffer |
translatePred(Operator o,
ArrayList<StringBuffer> sub)
Translate a predicate.
|
protected abstract StringBuffer |
translatePredicate(StringBuffer name,
ArrayList<StringBuffer> args)
Translate a predicate.
|
protected abstract StringBuffer |
translatePredicateName(StringBuffer name)
Get the name for a predicate symbol.
|
StringBuffer |
translateProblem(Term problem,
Services services,
SMTSettings settings)
Translates a problem into the given syntax.
|
private StringBuffer |
translateSort(Sort s) |
protected abstract StringBuffer |
translateSort(String name,
boolean isIntVal)
Translate a sort.
|
private ArrayList<StringBuffer> |
translateTaclets(Services services,
SMTSettings settings)
Translates the list
tacletFormulae to the given syntax. |
protected StringBuffer |
translateTerm(Term term,
Vector<QuantifiableVariable> quantifiedVars,
Services services)
Translates the given term into input syntax and adds the resulting
string to the StringBuffer sb.
|
protected StringBuffer |
translateTermIfThenElse(StringBuffer cond,
StringBuffer ifterm,
StringBuffer elseterm)
Translate the if_then_else construct for terms (i.e.
|
private StringBuffer |
translateTermIte(Term iteTerm,
Vector<QuantifiableVariable> quantifiedVars,
Services services) |
protected StringBuffer |
translateUniqueness(AbstractSMTTranslator.FunctionWrapper function,
Collection<AbstractSMTTranslator.FunctionWrapper> distinct)
Translates the unique-property of a function.
|
protected StringBuffer |
translateUnknown(Term term,
Vector<QuantifiableVariable> quantifiedVars,
Services services)
Takes care of sequent tree parts that were not matched in
translate(term, skolemization).
|
protected StringBuffer |
translateVariable(Operator op) |
private final TermBuilder tb
private int nameCounter
private Sort integerSort
private final StringBuffer standardSort
protected static final int YESNOT
protected String text
private final HashMap<Term,StringBuffer> usedBsumTerms
private final HashMap<Term,StringBuffer> usedBprodTerms
private HashMap<Term,StringBuffer> uninterpretedBindingFunctionNames
private HashMap<Term,StringBuffer> uninterpretedBindingPredicateNames
private HashMap<Operator,StringBuffer> usedVariableNames
private HashMap<Operator,StringBuffer> usedFunctionNames
private Collection<AbstractSMTTranslator.FunctionWrapper> usedFunctions
private HashMap<Operator,StringBuffer> usedPredicateNames
protected HashMap<Sort,StringBuffer> usedDisplaySort
protected HashMap<Sort,StringBuffer> usedRealSort
private HashMap<Sort,StringBuffer> typePredicates
private HashMap<Term,StringBuffer> constantTypePreds
private HashMap<Term,StringBuffer> modalityPredicates
private final HashMap<Long,StringBuffer> constantsForBigIntegers
private final HashMap<Long,StringBuffer> constantsForSmallIntegers
private ArrayList<StringBuffer> assumptions
private TacletSetTranslation tacletSetTranslation
private Collection<Throwable> exceptionsForTacletTranslation
private ArrayList<StringBuffer> tacletAssumptions
tacletFormulae
private SMTSettings smtSettings
private AbstractSMTTranslator.Configuration config
private Function multiplicationFunction
private static final String BSUM_STRING
private static final String BPROD_STRING
private StringBuffer castPredicate
public AbstractSMTTranslator(Sequent sequent, Services services, AbstractSMTTranslator.Configuration config)
sequent
- The sequent which shall be translated.services
- The services object belonging to sequent.public AbstractSMTTranslator(Services s, AbstractSMTTranslator.Configuration config)
s
- public TacletSetTranslation getTacletSetTranslation()
public final StringBuffer translateProblem(Term problem, Services services, SMTSettings settings) throws IllegalFormulaException
SMTTranslator
translate(Term t, Services services)
is that assumptions
will be added.translateProblem
in interface SMTTranslator
problem
- the problem to be translated.IllegalFormulaException
public Collection<Throwable> getExceptionsOfTacletTranslation()
SMTTranslator
getExceptionsOfTacletTranslation
in interface SMTTranslator
protected final SMTSettings getSettings()
public AbstractSMTTranslator.Configuration getConfig()
private boolean isUsingUninterpretedMultiplication()
private ArrayList<StringBuffer> getAssumptions(Services services, ArrayList<ContextualBlock> assumptionTypes, SMTSettings settings) throws IllegalFormulaException
services
- the services object to be used.assumptionTypes
- IllegalFormulaException
private ArrayList<StringBuffer> getSpecialSortPredicates(Services services) throws IllegalFormulaException
IllegalFormulaException
private StringBuffer buildComplText(Services serv, StringBuffer formula, SMTSettings settings) throws IllegalFormulaException
IllegalFormulaException
private SortHierarchy buildSortHierarchy(Services services, SMTSettings settings)
private ArrayList<StringBuffer> getSortHierarchyPredicates(Services services, SMTSettings settings)
private StringBuffer buildGeneralHierarchyPredicate(SortWrapper child, SortWrapper parent)
private StringBuffer buildInstantiatedHierarchyPredicate(SortWrapper child, SortWrapper parent, StringBuffer constant)
private ArrayList<StringBuffer> getTypeDefinitions()
private StringBuffer getSingleFunctionDef(StringBuffer funName, ArrayList<Sort> sorts)
funName
- the name of the function.sorts
- the sorts, the function is defined for. Last element
is the return type.private ArrayList<ArrayList<StringBuffer>> buildTranslatedFuncDecls(TermServices services)
private ArrayList<ArrayList<StringBuffer>> buildTranslatedPredDecls(ArrayList<ContextualBlock> predicateTypes)
private ArrayList<StringBuffer> buildTranslatedSorts()
private ArrayList<StringBuffer> buildUniqueAssumptions() throws IllegalFormulaException
IllegalFormulaException
private Term createLogicalVar(TermServices services, String baseName, Sort sort)
private ArrayList<StringBuffer> buildAssumptionsForUninterpretedMultiplication(Services services) throws IllegalFormulaException
IllegalFormulaException
private ArrayList<StringBuffer> buildAssumptionsForIntegers() throws IllegalFormulaException
IllegalFormulaException
private ArrayList<StringBuffer> buildAssumptionsForIntegers(Collection<StringBuffer> constants, boolean upperBound) throws IllegalFormulaException
IllegalFormulaException
private ArrayList<StringBuffer> buildAssumptionsForSorts(TermServices services)
private HashMap<Long,StringBuffer> getRightConstantContainer(long integer)
private Term getRightBorderAsTerm(long integer, TermServices services)
private Long getRightBorderAsInteger(long integer, TermServices services)
private StringBuffer getNameForIntegerConstant(TermServices services, long integer)
private StringBuffer buildUniqueConstant(long integer, TermServices services) throws IllegalFormulaException
IllegalFormulaException
protected abstract StringBuffer buildCompleteText(StringBuffer formula, ArrayList<StringBuffer> assum, ArrayList<ContextualBlock> assumptionBlocks, ArrayList<ArrayList<StringBuffer>> functions, ArrayList<ArrayList<StringBuffer>> predicates, ArrayList<ContextualBlock> predicateBlocks, ArrayList<StringBuffer> types, SortHierarchy sortHierarchy, SMTSettings settings)
formula
- The formula, that was built out of the internal
representation. It is built by ante implies succ.assum
- Assumptions made in this logic. Set of formulas, that
are assumed to be true.assumptionBlocks
- List of ContextualBlocks, which refer to the position
of different types of assumptions in the container
assumptions
. Use these objects to make
detailed comments in the translations. For more
information see the class ContextualBlock
.functions
- List of functions. Each Listelement is built up like
(name | sort1 | ... | sortn | resultsort)predicates
- List of predicates. Each Listelement is built up like
(name | sort1 | ... | sortn)predicateBlocks
- List of ContextualBlocks, which refer to the position
of different types of predicate in the container
predicates
. Use these objects to make
detailed comments in the translations. For more
information see the class ContextualBlock
.types
- List of the used types.protected abstract boolean isMultiSorted()
protected abstract StringBuffer getIntegerSort()
protected abstract StringBuffer getBoolSort()
protected abstract StringBuffer translateLogicalNot(StringBuffer arg)
arg
- The Formula to be negated.protected abstract StringBuffer translateLogicalAnd(StringBuffer arg1, StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract StringBuffer translateLogicalOr(StringBuffer arg1, StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract StringBuffer translateLogicalImply(StringBuffer arg1, StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract StringBuffer translateLogicalEquivalence(StringBuffer arg1, StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract StringBuffer translateLogicalAll(StringBuffer var, StringBuffer type, StringBuffer form)
var
- the bounded variable.type
- the type of the bounded variable.form
- The formula containing the bounded variable.protected abstract StringBuffer translateLogicalExist(StringBuffer var, StringBuffer type, StringBuffer form)
var
- the bounded variable.type
- the type of the bounded variable.form
- The formula containing the bounded variable.protected abstract StringBuffer translateLogicalTrue()
protected abstract StringBuffer translateLogicalFalse()
protected abstract StringBuffer translateObjectEqual(StringBuffer arg1, StringBuffer arg2)
arg1
- The first formula of the equivalence.arg2
- The second formula of the equivalence.protected abstract StringBuffer translateLogicalVar(StringBuffer name)
protected abstract StringBuffer translateLogicalConstant(StringBuffer name)
protected abstract StringBuffer translatePredicate(StringBuffer name, ArrayList<StringBuffer> args)
name
- The Symbol of the predicate.args
- The arguments of the predicate.protected abstract StringBuffer translatePredicateName(StringBuffer name)
name
- The name that can be used to create the symbol.protected abstract StringBuffer translateFunction(StringBuffer name, ArrayList<StringBuffer> args)
name
- The Symbol of the function.args
- The arguments of the function.protected abstract StringBuffer translateFunctionName(StringBuffer name)
name
- The name that can be used to create the symbol.protected StringBuffer translateIntegerPlus(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- first val of the sum.arg2
- second val of the sum.IllegalFormulaException
protected StringBuffer translateIntegerMinus(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the substraction.arg2
- second val of the substraction.IllegalFormulaException
protected StringBuffer translateIntegerUnaryMinus(StringBuffer arg) throws IllegalFormulaException
arg
- the argument of the unary minus.IllegalFormulaException
protected StringBuffer translateIntegerMult(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the multiplication.arg2
- second val of the multiplication.IllegalFormulaException
protected StringBuffer translateIntegerDiv(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the division.arg2
- second val of the division.IllegalFormulaException
protected StringBuffer translateIntegerMod(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the modulo.arg2
- second val of the modulo.IllegalFormulaException
protected StringBuffer translateIntegerGt(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the greater than.arg2
- second val of the greater than.IllegalFormulaException
protected StringBuffer translateIntegerLt(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the less than.arg2
- second val of the less than.IllegalFormulaException
protected StringBuffer translateIntegerGeq(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the greater or equal.arg2
- second val of the greater or equal.IllegalFormulaException
protected StringBuffer translateIntegerLeq(StringBuffer arg1, StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the less or equal.arg2
- second val of the less or equal.IllegalFormulaException
protected abstract StringBuffer translateNull()
protected abstract StringBuffer getNullName()
protected abstract StringBuffer translateNullSort()
protected abstract StringBuffer translateSort(String name, boolean isIntVal)
name
- the sorts nameisIntVal
- true, if the sort should represent some kind of
integerprotected StringBuffer translateIntegerValue(long val) throws IllegalFormulaException
IllegalFormulaException
protected abstract StringBuffer translateLogicalIfThenElse(StringBuffer cond, StringBuffer ifterm, StringBuffer elseterm)
cond
- the condition term.ifterm
- the formula used, if cond=trueelseterm
- the term used, if cond=falseprotected StringBuffer translateTermIfThenElse(StringBuffer cond, StringBuffer ifterm, StringBuffer elseterm) throws IllegalFormulaException
cond
- the condition formulaifterm
- the term used if cond = true.elseterm
- the term used if cond = false.IllegalFormulaException
- if this construct is not supported.protected StringBuffer translateUniqueness(AbstractSMTTranslator.FunctionWrapper function, Collection<AbstractSMTTranslator.FunctionWrapper> distinct) throws IllegalFormulaException
function
- the function itselfdistinct
- the set of functions, that should be distinct.IllegalFormulaException
protected StringBuffer buildInjectiveFunctionAssumption(AbstractSMTTranslator.FunctionWrapper fw)
private StringBuffer createGenericVariable(int pos)
protected ArrayList<StringBuffer> createGenericVariables(int count, int start)
protected StringBuffer translateDistinct(AbstractSMTTranslator.FunctionWrapper[] functions)
protected StringBuffer translateLogicalAll(ArrayList<StringBuffer> variables, ArrayList<Sort> sorts, StringBuffer result)
protected StringBuffer translateLogicalAll(StringBuffer var, Sort sort, StringBuffer result)
private final StringBuffer translateTermIte(Term iteTerm, Vector<QuantifiableVariable> quantifiedVars, Services services) throws IllegalFormulaException
IllegalFormulaException
private void addConstantTypePredicate(Term term, StringBuffer name)
protected StringBuffer translateTerm(Term term, Vector<QuantifiableVariable> quantifiedVars, Services services) throws IllegalFormulaException
term
- the Term which should be written in Simplify syntaxquantifiedVars
- a Vector containing all variables that have been bound
in super-terms. It is only used for the translation of
modulo terms, but must be looped through until we get
there.IllegalFormulaException
private StringBuffer translateAsBindingUninterpretedPredicate(Term term, Function fun, Vector<QuantifiableVariable> quantifiedVars, ImmutableArray<Term> subs, Services services) throws IllegalFormulaException
IllegalFormulaException
private StringBuffer translateAsBindingUninterpretedFunction(Term term, Function fun, Vector<QuantifiableVariable> quantifiedVars, ImmutableArray<Term> subs, Services services) throws IllegalFormulaException
term
- The term with the binding function on top levelfun
- the function operatorquantifiedVars
- subs
- the subterms of the functionservices
- IllegalFormulaException
private StringBuffer translateAsUninterpretedFunction(Function fun, Vector<QuantifiableVariable> quantifiedVars, ImmutableArray<Term> subs, Services services) throws IllegalFormulaException
IllegalFormulaException
private boolean isComplexMultiplication(Services services, Term t1, Term t2)
private StringBuffer castIfNeccessary(StringBuffer formula, Sort formulaSort, Sort targetSort)
formula
- The formula, that was translated.formulaSort
- The sort, the translatet formula has.targetSort
- The sort, the translated formula is expected to have.private StringBuffer cast(StringBuffer formula)
formula
- the formula to cast.private StringBuffer getModalityPredicate(Term t, Vector<QuantifiableVariable> quantifiedVars, Services services) throws IllegalFormulaException
t
- The term representing the modality.quantifiedVars
- quantified variables.services
- the services object to use.IllegalFormulaException
private void addSpecialFunction(Function fun)
fun
- the interpreted function to be added.protected StringBuffer getTypePredicate(Sort s, StringBuffer arg)
s
- The sort, the type predicate is wanted for.arg
- The expression, whose type should be defined.protected final StringBuffer translateUnknown(Term term, Vector<QuantifiableVariable> quantifiedVars, Services services) throws IllegalFormulaException
term
- The Term given to translateIllegalFormulaException
protected final StringBuffer translateVariable(Operator op)
protected final StringBuffer translateFunc(Operator o, ArrayList<StringBuffer> sub)
o
- the Operator used for this function.sub
- The StringBuffers representing the arguments of this
Function.protected final StringBuffer translateBsumFunction(Term bsumterm, ArrayList<StringBuffer> sub)
iterterm
- The term used as third argument of the bsum function.protected final StringBuffer translateBprodFunction(Term bprodterm, ArrayList<StringBuffer> sub)
iterterm
- The term used as third argument of the bsum function.private void addFunction(Operator op, ArrayList<Sort> sorts, Sort result)
op
- the operator used for this function.sorts
- the list of sort parameter of this functionprivate final StringBuffer translatePred(Operator o, ArrayList<StringBuffer> sub)
o
- the operator used for this predicate.sub
- The terms representing the arguments.private final StringBuffer translateSort(Sort s)
private void addTypePredicate(StringBuffer sortname, Sort s)
sortname
- the name, that should be used for the sort.s
- the sort, this predicate belongs to.protected boolean isSomeIntegerSort(Sort s)
private StringBuffer removeIllegalChars(StringBuffer template, ArrayList<String> toReplace, ArrayList<String> replacement)
protected StringBuffer makeUnique(StringBuffer name)
private ArrayList<StringBuffer> translateTaclets(Services services, SMTSettings settings) throws IllegalFormulaException
tacletFormulae
to the given syntax.services
- used for translateTerm
IllegalFormulaException
protected StringBuffer translateComment(int newLines, String comment)
private long getMaxNumber()
hasNumberLimit
returns
true
.private long getMinNumber()
hasNumberLimit
returns
true
.private boolean hasNumberLimit()
true
if the format supports only integers within
a certain interval.