public abstract class AbstractSMTTranslator extends java.lang.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 java.util.ArrayList<java.lang.StringBuffer> |
assumptions |
private static java.lang.String |
BPROD_STRING |
private static java.lang.String |
BSUM_STRING |
private java.lang.StringBuffer |
castPredicate
This stringbuffer is used as predicate name for casts from int-valued
to u-valued obects
|
private AbstractSMTTranslator.Configuration |
config |
private java.util.HashMap<java.lang.Long,java.lang.StringBuffer> |
constantsForBigIntegers
If a integer is not supported by a solver because it is too big, the
integer is translated into a constant.
|
private java.util.HashMap<java.lang.Long,java.lang.StringBuffer> |
constantsForSmallIntegers
If a integer is not supported by a solver because it is too small,
the integer is translated into a constant.
|
private java.util.HashMap<Term,java.lang.StringBuffer> |
constantTypePreds |
private java.util.Collection<java.lang.Throwable> |
exceptionsForTacletTranslation |
private java.util.HashMap<Operator,java.util.ArrayList<Sort>> |
functionDecls |
private Sort |
integerSort |
private java.util.HashMap<Term,java.lang.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 java.util.HashMap<Operator,java.util.ArrayList<Sort>> |
predicateDecls |
private SMTSettings |
smtSettings |
private java.util.HashSet<Function> |
specialFunctions |
private java.lang.StringBuffer |
standardSort
The string used as standard sort for translations
|
private java.util.ArrayList<java.lang.StringBuffer> |
tacletAssumptions
Assumptions made of taclets - the translation of
tacletFormulae |
private TacletSetTranslation |
tacletSetTranslation
Formulae made of taclets, used for assumptions.
|
private TermBuilder |
tb |
protected java.lang.String |
text
The translation result is stored in this variable.
|
private java.util.HashMap<Sort,java.lang.StringBuffer> |
typePredicates |
private java.util.HashMap<Term,java.lang.StringBuffer> |
uninterpretedBindingFunctionNames |
private java.util.HashMap<Term,java.lang.StringBuffer> |
uninterpretedBindingPredicateNames |
private java.util.HashMap<Term,java.lang.StringBuffer> |
usedBprodTerms |
private java.util.HashMap<Term,java.lang.StringBuffer> |
usedBsumTerms |
protected java.util.HashMap<Sort,java.lang.StringBuffer> |
usedDisplaySort |
private java.util.HashMap<Operator,java.lang.StringBuffer> |
usedFunctionNames |
private java.util.Collection<AbstractSMTTranslator.FunctionWrapper> |
usedFunctions |
private java.util.HashMap<Operator,java.lang.StringBuffer> |
usedPredicateNames |
protected java.util.HashMap<Sort,java.lang.StringBuffer> |
usedRealSort |
private java.util.HashMap<Operator,java.lang.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,
java.lang.StringBuffer name) |
private void |
addFunction(Operator op,
java.util.ArrayList<Sort> sorts,
Sort result) |
private void |
addPredicate(Operator op,
java.util.ArrayList<Sort> sorts) |
private void |
addSpecialFunction(Function fun)
Add an interpreted function to the set of special functions.
|
private void |
addTypePredicate(java.lang.StringBuffer sortname,
Sort s)
Create a type predicate for a given sort.
|
private java.util.ArrayList<java.lang.StringBuffer> |
buildAssumptionsForIntegers() |
private java.util.ArrayList<java.lang.StringBuffer> |
buildAssumptionsForIntegers(java.util.Collection<java.lang.StringBuffer> constants,
boolean upperBound) |
private java.util.ArrayList<java.lang.StringBuffer> |
buildAssumptionsForSorts(TermServices services) |
private java.util.ArrayList<java.lang.StringBuffer> |
buildAssumptionsForUninterpretedMultiplication(Services services) |
protected abstract java.lang.StringBuffer |
buildCompleteText(java.lang.StringBuffer formula,
java.util.ArrayList<java.lang.StringBuffer> assum,
java.util.ArrayList<ContextualBlock> assumptionBlocks,
java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> functions,
java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> predicates,
java.util.ArrayList<ContextualBlock> predicateBlocks,
java.util.ArrayList<java.lang.StringBuffer> types,
SortHierarchy sortHierarchy,
SMTSettings settings)
Build the text, that can be read by the final decider.
|
private java.lang.StringBuffer |
buildComplText(Services serv,
java.lang.StringBuffer formula,
SMTSettings settings) |
private java.lang.StringBuffer |
buildGeneralHierarchyPredicate(SortWrapper child,
SortWrapper parent) |
protected java.lang.StringBuffer |
buildInjectiveFunctionAssumption(AbstractSMTTranslator.FunctionWrapper fw) |
private java.lang.StringBuffer |
buildInstantiatedHierarchyPredicate(SortWrapper child,
SortWrapper parent,
java.lang.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 java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> |
buildTranslatedFuncDecls(TermServices services)
Build the translated function declarations.
|
private java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> |
buildTranslatedPredDecls(java.util.ArrayList<ContextualBlock> predicateTypes)
Build the translated predicate declarations.
|
private java.util.ArrayList<java.lang.StringBuffer> |
buildTranslatedSorts()
ArrayList of all sorts, that were used as sorts.
|
private java.util.ArrayList<java.lang.StringBuffer> |
buildUniqueAssumptions() |
private java.lang.StringBuffer |
buildUniqueConstant(long integer,
TermServices services) |
private java.lang.StringBuffer |
cast(java.lang.StringBuffer formula)
Cast a formula of type int to type u.
|
private java.lang.StringBuffer |
castIfNeccessary(java.lang.StringBuffer formula,
Sort formulaSort,
Sort targetSort)
This method adds a type cast to a translated formula, if neccessary.
|
private java.lang.StringBuffer |
createGenericVariable(int pos) |
protected java.util.ArrayList<java.lang.StringBuffer> |
createGenericVariables(int count,
int start) |
private Term |
createLogicalVar(TermServices services,
java.lang.String baseName,
Sort sort) |
private java.util.ArrayList<Sort> |
getArgSorts(Function function) |
private java.util.ArrayList<java.lang.StringBuffer> |
getAssumptions(Services services,
java.util.ArrayList<ContextualBlock> assumptionTypes,
SMTSettings settings)
get the assumptions made by the logic.
|
protected abstract java.lang.StringBuffer |
getBoolSort()
The String used for boolean values.
|
AbstractSMTTranslator.Configuration |
getConfig() |
java.util.Collection<java.lang.Throwable> |
getExceptionsOfTacletTranslation()
Returns all exceptions that have occurred while translating the taclets.
|
protected abstract java.lang.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 java.lang.StringBuffer |
getModalityPredicate(Term t,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Get a predicate representing a modality.
|
private Function |
getMultiplicationFunction(Services services) |
private java.lang.StringBuffer |
getNameForIntegerConstant(TermServices services,
long integer) |
protected abstract java.lang.StringBuffer |
getNullName() |
private java.lang.Long |
getRightBorderAsInteger(long integer,
TermServices services) |
private Term |
getRightBorderAsTerm(long integer,
TermServices services) |
private java.util.HashMap<java.lang.Long,java.lang.StringBuffer> |
getRightConstantContainer(long integer) |
protected SMTSettings |
getSettings() |
private java.lang.StringBuffer |
getSingleFunctionDef(java.lang.StringBuffer funName,
java.util.ArrayList<Sort> sorts)
Get the type predicate definition for a given function.
|
private java.util.ArrayList<java.lang.StringBuffer> |
getSortHierarchyPredicates(Services services,
SMTSettings settings)
Get the expression for that defines the typepredicates for sort
hierarchy.
|
private java.util.ArrayList<java.lang.StringBuffer> |
getSpecialSortPredicates(Services services)
build the formulas, that make sure, special functions keep typing
|
TacletSetTranslation |
getTacletSetTranslation() |
private java.util.ArrayList<java.lang.StringBuffer> |
getTypeDefinitions()
Returns a set of formula s, that defines the resulttypes of
functions, all constants and other elements (i.e. constant number
symbols).
|
protected java.lang.StringBuffer |
getTypePredicate(Sort s,
java.lang.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 java.lang.StringBuffer |
makeUnique(java.lang.StringBuffer name) |
private java.lang.StringBuffer |
removeIllegalChars(java.lang.StringBuffer template,
java.util.ArrayList<java.lang.String> toReplace,
java.util.ArrayList<java.lang.String> replacement) |
private java.lang.StringBuffer |
translateAsBindingUninterpretedFunction(Term term,
Function fun,
java.util.Vector<QuantifiableVariable> quantifiedVars,
ImmutableArray<Term> subs,
Services services)
Translate an uninterpreted function, which binds variables
|
private java.lang.StringBuffer |
translateAsBindingUninterpretedPredicate(Term term,
Function fun,
java.util.Vector<QuantifiableVariable> quantifiedVars,
ImmutableArray<Term> subs,
Services services) |
private java.lang.StringBuffer |
translateAsUninterpretedFunction(Function fun,
java.util.Vector<QuantifiableVariable> quantifiedVars,
ImmutableArray<Term> subs,
Services services) |
protected java.lang.StringBuffer |
translateBprodFunction(Term bprodterm,
java.util.ArrayList<java.lang.StringBuffer> sub)
translate a bprod function.
|
protected java.lang.StringBuffer |
translateBsumFunction(Term bsumterm,
java.util.ArrayList<java.lang.StringBuffer> sub)
translate a bsum function.
|
protected java.lang.StringBuffer |
translateComment(int newLines,
java.lang.String comment) |
protected java.lang.StringBuffer |
translateDistinct(AbstractSMTTranslator.FunctionWrapper[] functions) |
protected java.lang.StringBuffer |
translateFunc(Operator o,
java.util.ArrayList<java.lang.StringBuffer> sub)
translate a function.
|
protected abstract java.lang.StringBuffer |
translateFunction(java.lang.StringBuffer name,
java.util.ArrayList<java.lang.StringBuffer> args)
Translate a function.
|
protected abstract java.lang.StringBuffer |
translateFunctionName(java.lang.StringBuffer name)
Get the name for a function symbol.
|
protected java.lang.StringBuffer |
translateIntegerDiv(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer division.
|
protected java.lang.StringBuffer |
translateIntegerGeq(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the greater or equal.
|
protected java.lang.StringBuffer |
translateIntegerGt(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the greater than.
|
protected java.lang.StringBuffer |
translateIntegerLeq(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the less or equal.
|
protected java.lang.StringBuffer |
translateIntegerLt(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the less than.
|
protected java.lang.StringBuffer |
translateIntegerMinus(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer minus.
|
protected java.lang.StringBuffer |
translateIntegerMod(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer modulo.
|
protected java.lang.StringBuffer |
translateIntegerMult(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer multiplication.
|
protected java.lang.StringBuffer |
translateIntegerPlus(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Translate the integer plus.
|
protected java.lang.StringBuffer |
translateIntegerUnaryMinus(java.lang.StringBuffer arg)
Translate a unary minus.
|
protected java.lang.StringBuffer |
translateIntegerValue(long val)
Translate a sort.
|
protected java.lang.StringBuffer |
translateLogicalAll(java.util.ArrayList<java.lang.StringBuffer> variables,
java.util.ArrayList<Sort> sorts,
java.lang.StringBuffer result) |
protected java.lang.StringBuffer |
translateLogicalAll(java.lang.StringBuffer var,
Sort sort,
java.lang.StringBuffer result) |
protected abstract java.lang.StringBuffer |
translateLogicalAll(java.lang.StringBuffer var,
java.lang.StringBuffer type,
java.lang.StringBuffer form)
Build the logical forall formula.
|
protected abstract java.lang.StringBuffer |
translateLogicalAnd(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the logical konjunction.
|
protected abstract java.lang.StringBuffer |
translateLogicalConstant(java.lang.StringBuffer name)
Build the Stringbuffer for an constant.
|
protected abstract java.lang.StringBuffer |
translateLogicalEquivalence(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the logical equivalence.
|
protected abstract java.lang.StringBuffer |
translateLogicalExist(java.lang.StringBuffer var,
java.lang.StringBuffer type,
java.lang.StringBuffer form)
Build the logical exists formula.
|
protected abstract java.lang.StringBuffer |
translateLogicalFalse()
Translate the logical false.
|
protected abstract java.lang.StringBuffer |
translateLogicalIfThenElse(java.lang.StringBuffer cond,
java.lang.StringBuffer ifterm,
java.lang.StringBuffer elseterm)
Translate the logical if_then_else construct.
|
protected abstract java.lang.StringBuffer |
translateLogicalImply(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the logical implication.
|
protected abstract java.lang.StringBuffer |
translateLogicalNot(java.lang.StringBuffer arg)
Build the Stringbuffer for a logical NOT.
|
protected abstract java.lang.StringBuffer |
translateLogicalOr(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the logical disjunction.
|
protected abstract java.lang.StringBuffer |
translateLogicalTrue()
Translate the logical true.
|
protected abstract java.lang.StringBuffer |
translateLogicalVar(java.lang.StringBuffer name)
Build the Stringbuffer for an variable.
|
protected abstract java.lang.StringBuffer |
translateNull()
Translate the NULL element
|
protected abstract java.lang.StringBuffer |
translateNullSort()
Translate the NULL element's Sort.
|
protected abstract java.lang.StringBuffer |
translateObjectEqual(java.lang.StringBuffer arg1,
java.lang.StringBuffer arg2)
Build the Stringbuffer for an object equivalence.
|
private java.lang.StringBuffer |
translatePred(Operator o,
java.util.ArrayList<java.lang.StringBuffer> sub)
Translate a predicate.
|
protected abstract java.lang.StringBuffer |
translatePredicate(java.lang.StringBuffer name,
java.util.ArrayList<java.lang.StringBuffer> args)
Translate a predicate.
|
protected abstract java.lang.StringBuffer |
translatePredicateName(java.lang.StringBuffer name)
Get the name for a predicate symbol.
|
java.lang.StringBuffer |
translateProblem(Term problem,
Services services,
SMTSettings settings)
Translates a problem into the given syntax.
|
private java.lang.StringBuffer |
translateSort(Sort s) |
protected abstract java.lang.StringBuffer |
translateSort(java.lang.String name,
boolean isIntVal)
Translate a sort.
|
private java.util.ArrayList<java.lang.StringBuffer> |
translateTaclets(Services services,
SMTSettings settings)
Translates the list
tacletFormulae to the given syntax. |
protected java.lang.StringBuffer |
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 |
translateTermIfThenElse(java.lang.StringBuffer cond,
java.lang.StringBuffer ifterm,
java.lang.StringBuffer elseterm)
Translate the if_then_else construct for terms (i.e. ifterm and
condterm are not of Sort FORMULA) If this method is nor overriden, a
default implementation is used.
|
private java.lang.StringBuffer |
translateTermIte(Term iteTerm,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services) |
protected java.lang.StringBuffer |
translateUniqueness(AbstractSMTTranslator.FunctionWrapper function,
java.util.Collection<AbstractSMTTranslator.FunctionWrapper> distinct)
Translates the unique-property of a function.
|
protected java.lang.StringBuffer |
translateUnknown(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Takes care of sequent tree parts that were not matched in
translate(term, skolemization).
|
protected java.lang.StringBuffer |
translateVariable(Operator op) |
private final TermBuilder tb
private int nameCounter
private Sort integerSort
private final java.lang.StringBuffer standardSort
protected static final int YESNOT
protected java.lang.String text
private final java.util.HashMap<Term,java.lang.StringBuffer> usedBsumTerms
private final java.util.HashMap<Term,java.lang.StringBuffer> usedBprodTerms
private java.util.HashMap<Term,java.lang.StringBuffer> uninterpretedBindingFunctionNames
private java.util.HashMap<Term,java.lang.StringBuffer> uninterpretedBindingPredicateNames
private java.util.HashSet<Function> specialFunctions
private java.util.HashMap<Operator,java.lang.StringBuffer> usedVariableNames
private java.util.HashMap<Operator,java.lang.StringBuffer> usedFunctionNames
private java.util.Collection<AbstractSMTTranslator.FunctionWrapper> usedFunctions
private java.util.HashMap<Operator,java.lang.StringBuffer> usedPredicateNames
protected java.util.HashMap<Sort,java.lang.StringBuffer> usedDisplaySort
protected java.util.HashMap<Sort,java.lang.StringBuffer> usedRealSort
private java.util.HashMap<Sort,java.lang.StringBuffer> typePredicates
private java.util.HashMap<Term,java.lang.StringBuffer> constantTypePreds
private java.util.HashMap<Term,java.lang.StringBuffer> modalityPredicates
private final java.util.HashMap<java.lang.Long,java.lang.StringBuffer> constantsForBigIntegers
private final java.util.HashMap<java.lang.Long,java.lang.StringBuffer> constantsForSmallIntegers
private java.util.ArrayList<java.lang.StringBuffer> assumptions
private TacletSetTranslation tacletSetTranslation
private java.util.Collection<java.lang.Throwable> exceptionsForTacletTranslation
private java.util.ArrayList<java.lang.StringBuffer> tacletAssumptions
tacletFormulae
private SMTSettings smtSettings
private AbstractSMTTranslator.Configuration config
private Function multiplicationFunction
private static final java.lang.String BSUM_STRING
private static final java.lang.String BPROD_STRING
private java.lang.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 java.lang.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 java.util.Collection<java.lang.Throwable> getExceptionsOfTacletTranslation()
SMTTranslator
getExceptionsOfTacletTranslation
in interface SMTTranslator
protected final SMTSettings getSettings()
public AbstractSMTTranslator.Configuration getConfig()
private boolean isUsingUninterpretedMultiplication()
private java.util.ArrayList<java.lang.StringBuffer> getAssumptions(Services services, java.util.ArrayList<ContextualBlock> assumptionTypes, SMTSettings settings) throws IllegalFormulaException
services
- the services object to be used.assumptionTypes
- IllegalFormulaException
private java.util.ArrayList<java.lang.StringBuffer> getSpecialSortPredicates(Services services) throws IllegalFormulaException
IllegalFormulaException
private java.lang.StringBuffer buildComplText(Services serv, java.lang.StringBuffer formula, SMTSettings settings) throws IllegalFormulaException
IllegalFormulaException
private SortHierarchy buildSortHierarchy(Services services, SMTSettings settings)
private java.util.ArrayList<java.lang.StringBuffer> getSortHierarchyPredicates(Services services, SMTSettings settings)
private java.lang.StringBuffer buildGeneralHierarchyPredicate(SortWrapper child, SortWrapper parent)
private java.lang.StringBuffer buildInstantiatedHierarchyPredicate(SortWrapper child, SortWrapper parent, java.lang.StringBuffer constant)
private java.util.ArrayList<java.lang.StringBuffer> getTypeDefinitions()
private java.lang.StringBuffer getSingleFunctionDef(java.lang.StringBuffer funName, java.util.ArrayList<Sort> sorts)
funName
- the name of the function.sorts
- the sorts, the function is defined for. Last element
is the return type.private java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> buildTranslatedFuncDecls(TermServices services)
private java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> buildTranslatedPredDecls(java.util.ArrayList<ContextualBlock> predicateTypes)
private java.util.ArrayList<java.lang.StringBuffer> buildTranslatedSorts()
private java.util.ArrayList<java.lang.StringBuffer> buildUniqueAssumptions() throws IllegalFormulaException
IllegalFormulaException
private Term createLogicalVar(TermServices services, java.lang.String baseName, Sort sort)
private java.util.ArrayList<java.lang.StringBuffer> buildAssumptionsForUninterpretedMultiplication(Services services) throws IllegalFormulaException
IllegalFormulaException
private java.util.ArrayList<java.lang.StringBuffer> buildAssumptionsForIntegers() throws IllegalFormulaException
IllegalFormulaException
private java.util.ArrayList<java.lang.StringBuffer> buildAssumptionsForIntegers(java.util.Collection<java.lang.StringBuffer> constants, boolean upperBound) throws IllegalFormulaException
IllegalFormulaException
private java.util.ArrayList<java.lang.StringBuffer> buildAssumptionsForSorts(TermServices services)
private java.util.HashMap<java.lang.Long,java.lang.StringBuffer> getRightConstantContainer(long integer)
private Term getRightBorderAsTerm(long integer, TermServices services)
private java.lang.Long getRightBorderAsInteger(long integer, TermServices services)
private java.lang.StringBuffer getNameForIntegerConstant(TermServices services, long integer)
private java.lang.StringBuffer buildUniqueConstant(long integer, TermServices services) throws IllegalFormulaException
IllegalFormulaException
protected abstract java.lang.StringBuffer buildCompleteText(java.lang.StringBuffer formula, java.util.ArrayList<java.lang.StringBuffer> assum, java.util.ArrayList<ContextualBlock> assumptionBlocks, java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> functions, java.util.ArrayList<java.util.ArrayList<java.lang.StringBuffer>> predicates, java.util.ArrayList<ContextualBlock> predicateBlocks, java.util.ArrayList<java.lang.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 java.lang.StringBuffer getIntegerSort()
protected abstract java.lang.StringBuffer getBoolSort()
protected abstract java.lang.StringBuffer translateLogicalNot(java.lang.StringBuffer arg)
arg
- The Formula to be negated.protected abstract java.lang.StringBuffer translateLogicalAnd(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract java.lang.StringBuffer translateLogicalOr(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract java.lang.StringBuffer translateLogicalImply(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract java.lang.StringBuffer translateLogicalEquivalence(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula.arg2
- The second formula.protected abstract java.lang.StringBuffer translateLogicalAll(java.lang.StringBuffer var, java.lang.StringBuffer type, java.lang.StringBuffer form)
var
- the bounded variable.type
- the type of the bounded variable.form
- The formula containing the bounded variable.protected abstract java.lang.StringBuffer translateLogicalExist(java.lang.StringBuffer var, java.lang.StringBuffer type, java.lang.StringBuffer form)
var
- the bounded variable.type
- the type of the bounded variable.form
- The formula containing the bounded variable.protected abstract java.lang.StringBuffer translateLogicalTrue()
protected abstract java.lang.StringBuffer translateLogicalFalse()
protected abstract java.lang.StringBuffer translateObjectEqual(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2)
arg1
- The first formula of the equivalence.arg2
- The second formula of the equivalence.protected abstract java.lang.StringBuffer translateLogicalVar(java.lang.StringBuffer name)
protected abstract java.lang.StringBuffer translateLogicalConstant(java.lang.StringBuffer name)
protected abstract java.lang.StringBuffer translatePredicate(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args)
name
- The Symbol of the predicate.args
- The arguments of the predicate.protected abstract java.lang.StringBuffer translatePredicateName(java.lang.StringBuffer name)
name
- The name that can be used to create the symbol.protected abstract java.lang.StringBuffer translateFunction(java.lang.StringBuffer name, java.util.ArrayList<java.lang.StringBuffer> args)
name
- The Symbol of the function.args
- The arguments of the function.protected abstract java.lang.StringBuffer translateFunctionName(java.lang.StringBuffer name)
name
- The name that can be used to create the symbol.protected java.lang.StringBuffer translateIntegerPlus(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- first val of the sum.arg2
- second val of the sum.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerMinus(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the substraction.arg2
- second val of the substraction.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerUnaryMinus(java.lang.StringBuffer arg) throws IllegalFormulaException
arg
- the argument of the unary minus.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerMult(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the multiplication.arg2
- second val of the multiplication.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerDiv(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the division.arg2
- second val of the division.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerMod(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the modulo.arg2
- second val of the modulo.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerGt(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the greater than.arg2
- second val of the greater than.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerLt(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the less than.arg2
- second val of the less than.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerGeq(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the greater or equal.arg2
- second val of the greater or equal.IllegalFormulaException
protected java.lang.StringBuffer translateIntegerLeq(java.lang.StringBuffer arg1, java.lang.StringBuffer arg2) throws IllegalFormulaException
arg1
- The first val of the less or equal.arg2
- second val of the less or equal.IllegalFormulaException
protected abstract java.lang.StringBuffer translateNull()
protected abstract java.lang.StringBuffer getNullName()
protected abstract java.lang.StringBuffer translateNullSort()
protected abstract java.lang.StringBuffer translateSort(java.lang.String name, boolean isIntVal)
name
- the sorts nameisIntVal
- true, if the sort should represent some kind of
integerprotected java.lang.StringBuffer translateIntegerValue(long val) throws IllegalFormulaException
IllegalFormulaException
protected abstract java.lang.StringBuffer translateLogicalIfThenElse(java.lang.StringBuffer cond, java.lang.StringBuffer ifterm, java.lang.StringBuffer elseterm)
cond
- the condition term.ifterm
- the formula used, if cond=trueelseterm
- the term used, if cond=falseprotected java.lang.StringBuffer translateTermIfThenElse(java.lang.StringBuffer cond, java.lang.StringBuffer ifterm, java.lang.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 java.lang.StringBuffer translateUniqueness(AbstractSMTTranslator.FunctionWrapper function, java.util.Collection<AbstractSMTTranslator.FunctionWrapper> distinct) throws IllegalFormulaException
function
- the function itselfdistinct
- the set of functions, that should be distinct.IllegalFormulaException
protected java.lang.StringBuffer buildInjectiveFunctionAssumption(AbstractSMTTranslator.FunctionWrapper fw)
private java.lang.StringBuffer createGenericVariable(int pos)
protected java.util.ArrayList<java.lang.StringBuffer> createGenericVariables(int count, int start)
protected java.lang.StringBuffer translateDistinct(AbstractSMTTranslator.FunctionWrapper[] functions)
protected java.lang.StringBuffer translateLogicalAll(java.util.ArrayList<java.lang.StringBuffer> variables, java.util.ArrayList<Sort> sorts, java.lang.StringBuffer result)
protected java.lang.StringBuffer translateLogicalAll(java.lang.StringBuffer var, Sort sort, java.lang.StringBuffer result)
private final java.lang.StringBuffer translateTermIte(Term iteTerm, java.util.Vector<QuantifiableVariable> quantifiedVars, Services services) throws IllegalFormulaException
IllegalFormulaException
private void addConstantTypePredicate(Term term, java.lang.StringBuffer name)
protected java.lang.StringBuffer translateTerm(Term term, java.util.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 java.lang.StringBuffer translateAsBindingUninterpretedPredicate(Term term, Function fun, java.util.Vector<QuantifiableVariable> quantifiedVars, ImmutableArray<Term> subs, Services services) throws IllegalFormulaException
IllegalFormulaException
private java.lang.StringBuffer translateAsBindingUninterpretedFunction(Term term, Function fun, java.util.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 java.lang.StringBuffer translateAsUninterpretedFunction(Function fun, java.util.Vector<QuantifiableVariable> quantifiedVars, ImmutableArray<Term> subs, Services services) throws IllegalFormulaException
IllegalFormulaException
private boolean isComplexMultiplication(Services services, Term t1, Term t2)
private java.lang.StringBuffer castIfNeccessary(java.lang.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 java.lang.StringBuffer cast(java.lang.StringBuffer formula)
formula
- the formula to cast.private java.lang.StringBuffer getModalityPredicate(Term t, java.util.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 java.lang.StringBuffer getTypePredicate(Sort s, java.lang.StringBuffer arg)
s
- The sort, the type predicate is wanted for.arg
- The expression, whose type should be defined.protected final java.lang.StringBuffer translateUnknown(Term term, java.util.Vector<QuantifiableVariable> quantifiedVars, Services services) throws IllegalFormulaException
term
- The Term given to translateIllegalFormulaException
protected final java.lang.StringBuffer translateVariable(Operator op)
protected final java.lang.StringBuffer translateFunc(Operator o, java.util.ArrayList<java.lang.StringBuffer> sub)
o
- the Operator used for this function.sub
- The StringBuffers representing the arguments of this
Function.protected final java.lang.StringBuffer translateBsumFunction(Term bsumterm, java.util.ArrayList<java.lang.StringBuffer> sub)
iterterm
- The term used as third argument of the bsum function.protected final java.lang.StringBuffer translateBprodFunction(Term bprodterm, java.util.ArrayList<java.lang.StringBuffer> sub)
iterterm
- The term used as third argument of the bsum function.private void addFunction(Operator op, java.util.ArrayList<Sort> sorts, Sort result)
op
- the operator used for this function.sorts
- the list of sort parameter of this functionprivate final java.lang.StringBuffer translatePred(Operator o, java.util.ArrayList<java.lang.StringBuffer> sub)
o
- the operator used for this predicate.sub
- The terms representing the arguments.private final java.lang.StringBuffer translateSort(Sort s)
private void addTypePredicate(java.lang.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 java.lang.StringBuffer removeIllegalChars(java.lang.StringBuffer template, java.util.ArrayList<java.lang.String> toReplace, java.util.ArrayList<java.lang.String> replacement)
protected java.lang.StringBuffer makeUnique(java.lang.StringBuffer name)
private java.util.ArrayList<java.lang.StringBuffer> translateTaclets(Services services, SMTSettings settings) throws IllegalFormulaException
tacletFormulae
to the given syntax.services
- used for translateTerm
IllegalFormulaException
protected java.lang.StringBuffer translateComment(int newLines, java.lang.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.