Interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
-
- Type Parameters:
ParamFormulaType
- formulaType of the parametersResultFormulaType
- formulaType of arithmetic results
- All Known Subinterfaces:
IntegerFormulaManager
,RationalFormulaManager
- All Known Implementing Classes:
AbstractNumeralFormulaManager
,DebuggingIntegerFormulaManager
,DebuggingNumeralFormulaManager
,DebuggingRationalFormulaManager
public interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
This interface represents the Numeral Theory.
-
-
Method Summary
-
-
-
Method Detail
-
makeNumber
ResultFormulaType makeNumber(long number)
-
makeNumber
ResultFormulaType makeNumber(BigInteger number)
-
makeNumber
ResultFormulaType makeNumber(double number)
Create a numeric literal with a given value. Note: if the theory represented by this instance cannot handle rational numbers, the value may get rounded or otherwise represented imprecisely.
-
makeNumber
ResultFormulaType makeNumber(BigDecimal number)
Create a numeric literal with a given value. Note: if the theory represented by this instance cannot handle rational numbers, the value may get rounded or otherwise represented imprecisely.
-
makeNumber
ResultFormulaType makeNumber(String pI)
-
makeNumber
ResultFormulaType makeNumber(Rational pRational)
-
makeVariable
ResultFormulaType makeVariable(String pVar)
Creates a variable with exactly the given name.Please make sure that the given name is valid in SMT-LIB2. Take a look at
FormulaManager.isValidName(java.lang.String)
for further information.This method does not quote or unquote the given name, but uses the plain name "AS IS".
Formula.toString()
can return a different String than the given one.
-
getFormulaType
FormulaType<ResultFormulaType> getFormulaType()
-
negate
ResultFormulaType negate(ParamFormulaType number)
-
add
ResultFormulaType add(ParamFormulaType number1, ParamFormulaType number2)
-
sum
ResultFormulaType sum(List<ParamFormulaType> operands)
-
subtract
ResultFormulaType subtract(ParamFormulaType number1, ParamFormulaType number2)
-
divide
ResultFormulaType divide(ParamFormulaType numerator, ParamFormulaType denumerator)
Create a formula representing the division of two operands.If the denumerator evaluates to zero (division-by-zero), either directly as value or indirectly via an additional constraint, then the solver is allowed to choose an arbitrary value for the result of the division (cf. SMTLIB standard for the division operator in Ints or Reals theory).
Note: Some solvers, e.g., Yices2, abort with an exception when exploring a division-by-zero during the SAT-check. This is not compliant to the SMTLIB standard, but sadly happens.
-
multiply
ResultFormulaType multiply(ParamFormulaType number1, ParamFormulaType number2)
-
equal
BooleanFormula equal(ParamFormulaType number1, ParamFormulaType number2)
-
distinct
BooleanFormula distinct(List<ParamFormulaType> pNumbers)
All given numbers are pairwise unequal.
-
greaterThan
BooleanFormula greaterThan(ParamFormulaType number1, ParamFormulaType number2)
-
greaterOrEquals
BooleanFormula greaterOrEquals(ParamFormulaType number1, ParamFormulaType number2)
-
lessThan
BooleanFormula lessThan(ParamFormulaType number1, ParamFormulaType number2)
-
lessOrEquals
BooleanFormula lessOrEquals(ParamFormulaType number1, ParamFormulaType number2)
-
floor
NumeralFormula.IntegerFormula floor(ParamFormulaType formula)
Thefloor
operation returns the nearest integer formula that is less or equal to the given argument formula.For rational formulas, SMTlib2 denotes this operation as
to_int
.
-
-