Package org.sosy_lab.java_smt.basicimpl

Class AbstractNumeralFormulaManager<TFormulaInfo,TType,TEnv,ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula,TFuncDecl>

java.lang.Object

org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager<TFormulaInfo,TType,TEnv,ParamFormulaType,ResultFormulaType,TFuncDecl>

All Implemented Interfaces:

NumeralFormulaManager<ParamFormulaType,ResultFormulaType>

public abstract class AbstractNumeralFormulaManager<TFormulaInfo,TType,TEnv,ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula,TFuncDecl>
extends Object
implements NumeralFormulaManager<ParamFormulaType,ResultFormulaType>

Similar to the other Abstract*FormulaManager classes in this package, this class serves as a helper for implementing NumeralFormulaManager. It handles all the unwrapping and wrapping from Formula instances to solver-specific formula representations, such that the concrete class needs to handle only its own internal types.

Implementation Requirements:

The method NumeralFormulaManager.getFormulaType() must be safe to be called from the constructor (the default implementations of IntegerFormulaManager and RationalFormulaManager satisfy this).

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	AbstractNumeralFormulaManager.NonLinearArithmetic

Field Summary

Fields

Modifier and Type	Field	Description
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	formulaCreator

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractNumeralFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator, AbstractNumeralFormulaManager.NonLinearArithmetic pNonLinearArithmetic)

Method Summary

Modifier and Type	Method	Description
ResultFormulaType	add(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected abstract TFormulaInfo	add(TFormulaInfo pParam1, TFormulaInfo pParam2)
protected TFormulaInfo	decimalAsInteger(BigDecimal val)	This method tries to represent a BigDecimal using only BigInteger.
BooleanFormula	distinct(List<ParamFormulaType> pNumbers)	All given numbers are pairwise unequal.
protected abstract TFormulaInfo	distinctImpl(List<TFormulaInfo> pNumbers)
ResultFormulaType	divide(ParamFormulaType pNumber1, ParamFormulaType pNumber2)	Create a formula representing the division of two operands according to Boute's Euclidean definition (DOI: 10.1145/128861.128862).
protected TFormulaInfo	divide(TFormulaInfo pParam1, TFormulaInfo pParam2)	If a solver does not support this operation, e.g.
BooleanFormula	equal(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected abstract TFormulaInfo	equal(TFormulaInfo pParam1, TFormulaInfo pParam2)
protected TFormulaInfo	extractInfo(Formula pBits)
NumeralFormula.IntegerFormula	floor(ParamFormulaType number)	The floor operation returns the nearest integer formula that is less or equal to the given argument formula.
protected TFormulaInfo	floor(TFormulaInfo number)
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	getFormulaCreator()
BooleanFormula	greaterOrEquals(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected abstract TFormulaInfo	greaterOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2)
BooleanFormula	greaterThan(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected abstract TFormulaInfo	greaterThan(TFormulaInfo pParam1, TFormulaInfo pParam2)
protected abstract boolean	isNumeral(TFormulaInfo val)	Check whether the argument is a numeric constant (including negated constants).
BooleanFormula	lessOrEquals(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected abstract TFormulaInfo	lessOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2)
BooleanFormula	lessThan(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected abstract TFormulaInfo	lessThan(TFormulaInfo pParam1, TFormulaInfo pParam2)
ResultFormulaType	makeNumber(double pNumber)	Create a numeric literal with a given value.
ResultFormulaType	makeNumber(long i)
ResultFormulaType	makeNumber(String i)
ResultFormulaType	makeNumber(BigDecimal pNumber)	Create a numeric literal with a given value.
ResultFormulaType	makeNumber(BigInteger i)
ResultFormulaType	makeNumber(Rational pRational)
protected abstract TFormulaInfo	makeNumberImpl(double pNumber)
protected abstract TFormulaInfo	makeNumberImpl(long i)
protected abstract TFormulaInfo	makeNumberImpl(String i)
protected abstract TFormulaInfo	makeNumberImpl(BigDecimal pNumber)
protected abstract TFormulaInfo	makeNumberImpl(BigInteger i)
protected TFormulaInfo	makeNumberImpl(Rational pRational)
ResultFormulaType	makeVariable(String pVar)	Creates a variable with exactly the given name.
protected abstract TFormulaInfo	makeVariableImpl(String i)
BooleanFormula	modularCongruence(ParamFormulaType pNumber1, ParamFormulaType pNumber2, long pModulo)
BooleanFormula	modularCongruence(ParamFormulaType pNumber1, ParamFormulaType pNumber2, BigInteger pModulo)
protected TFormulaInfo	modularCongruence(TFormulaInfo a, TFormulaInfo b, long m)
protected TFormulaInfo	modularCongruence(TFormulaInfo a, TFormulaInfo b, BigInteger m)
ResultFormulaType	modulo(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected TFormulaInfo	modulo(TFormulaInfo pParam1, TFormulaInfo pParam2)	If a solver does not support this operation, e.g.
ResultFormulaType	multiply(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected TFormulaInfo	multiply(TFormulaInfo pParam1, TFormulaInfo pParam2)	If a solver does not support this operation, e.g.
ResultFormulaType	negate(ParamFormulaType pNumber)
protected abstract TFormulaInfo	negate(TFormulaInfo pParam1)
ResultFormulaType	subtract(ParamFormulaType pNumber1, ParamFormulaType pNumber2)
protected abstract TFormulaInfo	subtract(TFormulaInfo pParam1, TFormulaInfo pParam2)
ResultFormulaType	sum(List<ParamFormulaType> operands)
protected TFormulaInfo	sumImpl(List<TFormulaInfo> operands)
protected TType	toSolverType(FormulaType<?> formulaType)
protected TFormulaInfo	toType(TFormulaInfo param)	Make sure the value is of correct type (Int vs.
protected ResultFormulaType	wrap(TFormulaInfo pTerm)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.sosy_lab.java_smt.api.NumeralFormulaManager

getFormulaType

Field Detail

formulaCreator

protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator

Constructor Detail

AbstractNumeralFormulaManager

protected AbstractNumeralFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator,
                                        AbstractNumeralFormulaManager.NonLinearArithmetic pNonLinearArithmetic)

Method Detail

wrap

protected ResultFormulaType wrap(TFormulaInfo pTerm)

isNumeral

protected abstract boolean isNumeral(TFormulaInfo val)

Check whether the argument is a numeric constant (including negated constants).

makeNumber

public ResultFormulaType makeNumber(long i)

Specified by:

makeNumber in interface NumeralFormulaManager<TFormulaInfo,TType>

makeNumberImpl

protected abstract TFormulaInfo makeNumberImpl(long i)

makeNumber

public ResultFormulaType makeNumber(BigInteger i)

Specified by:

makeNumber in interface NumeralFormulaManager<TFormulaInfo,TType>

makeNumberImpl

protected abstract TFormulaInfo makeNumberImpl(BigInteger i)

makeNumber

public ResultFormulaType makeNumber(String i)

Specified by:

makeNumber in interface NumeralFormulaManager<TFormulaInfo,TType>

makeNumberImpl

protected abstract TFormulaInfo makeNumberImpl(String i)

makeNumber

public ResultFormulaType makeNumber(Rational pRational)

Specified by:

makeNumber in interface NumeralFormulaManager<TFormulaInfo,TType>

makeNumberImpl

protected TFormulaInfo makeNumberImpl(Rational pRational)

makeNumber

public ResultFormulaType makeNumber(double pNumber)

Description copied from interface: NumeralFormulaManager

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.

Specified by:

makeNumber in interface NumeralFormulaManager<TFormulaInfo,TType>

makeNumberImpl

protected abstract TFormulaInfo makeNumberImpl(double pNumber)

makeNumber

public ResultFormulaType makeNumber(BigDecimal pNumber)

Description copied from interface: NumeralFormulaManager

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.

Specified by:

makeNumber in interface NumeralFormulaManager<TFormulaInfo,TType>

makeNumberImpl

protected abstract TFormulaInfo makeNumberImpl(BigDecimal pNumber)

decimalAsInteger

protected final TFormulaInfo decimalAsInteger(BigDecimal val)

This method tries to represent a BigDecimal using only BigInteger. It can be used for implementing makeNumber(BigDecimal) when the current theory supports only integers and division by constants.

makeVariable

public ResultFormulaType makeVariable(String pVar)

Description copied from interface: NumeralFormulaManager

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.

Specified by:

makeVariable in interface NumeralFormulaManager<TFormulaInfo,TType>

makeVariableImpl

protected abstract TFormulaInfo makeVariableImpl(String i)

negate

public ResultFormulaType negate(ParamFormulaType pNumber)

Specified by:

negate in interface NumeralFormulaManager<TFormulaInfo,TType>

negate

protected abstract TFormulaInfo negate(TFormulaInfo pParam1)

add

public ResultFormulaType add(ParamFormulaType pNumber1,
                             ParamFormulaType pNumber2)

Specified by:

add in interface NumeralFormulaManager<TFormulaInfo,TType>

add

protected abstract TFormulaInfo add(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2)

sum

public ResultFormulaType sum(List<ParamFormulaType> operands)

Specified by:

sum in interface NumeralFormulaManager<TFormulaInfo,TType>

sumImpl

protected TFormulaInfo sumImpl(List<TFormulaInfo> operands)

subtract

public ResultFormulaType subtract(ParamFormulaType pNumber1,
                                  ParamFormulaType pNumber2)

Specified by:

subtract in interface NumeralFormulaManager<TFormulaInfo,TType>

subtract

protected abstract TFormulaInfo subtract(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2)

divide

public ResultFormulaType divide(ParamFormulaType pNumber1,
                                ParamFormulaType pNumber2)

Description copied from interface: NumeralFormulaManager

Create a formula representing the division of two operands according to Boute's Euclidean definition (DOI: 10.1145/128861.128862).

If the denominator 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 version 2.6 for the division operator in Int or Real theory). The details of this are implementation specific and may change solver by solver.

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.

Specified by:

divide in interface NumeralFormulaManager<TFormulaInfo,TType>

divide

protected TFormulaInfo divide(TFormulaInfo pParam1,
                              TFormulaInfo pParam2)

If a solver does not support this operation, e.g. because of missing support for non-linear arithmetics, we throw UnsupportedOperationException.

Parameters:

pParam1 - the dividend

pParam2 - the divisor

modulo

public ResultFormulaType modulo(ParamFormulaType pNumber1,
                                ParamFormulaType pNumber2)

modulo

protected TFormulaInfo modulo(TFormulaInfo pParam1,
                              TFormulaInfo pParam2)

If a solver does not support this operation, e.g. because of missing support for non-linear arithmetics, we throw UnsupportedOperationException.

Parameters:

pParam1 - the dividend

pParam2 - the divisor

modularCongruence

public BooleanFormula modularCongruence(ParamFormulaType pNumber1,
                                        ParamFormulaType pNumber2,
                                        long pModulo)

modularCongruence

public BooleanFormula modularCongruence(ParamFormulaType pNumber1,
                                        ParamFormulaType pNumber2,
                                        BigInteger pModulo)

modularCongruence

protected TFormulaInfo modularCongruence(TFormulaInfo a,
                                         TFormulaInfo b,
                                         BigInteger m)

Parameters:

a - first operand

b - second operand

m - the modulus

Returns:

the formula representing a = b (mod m)

modularCongruence

protected TFormulaInfo modularCongruence(TFormulaInfo a,
                                         TFormulaInfo b,
                                         long m)

Parameters:

a - first operand

b - second operand

m - the modulus

Returns:

the formula representing a = b (mod m)

multiply

public ResultFormulaType multiply(ParamFormulaType pNumber1,
                                  ParamFormulaType pNumber2)

Specified by:

multiply in interface NumeralFormulaManager<TFormulaInfo,TType>

multiply

protected TFormulaInfo multiply(TFormulaInfo pParam1,
                                TFormulaInfo pParam2)

If a solver does not support this operation, e.g. because of missing support for non-linear arithmetics, we throw UnsupportedOperationException.

Parameters:

pParam1 - first factor

pParam2 - second factor

equal

public BooleanFormula equal(ParamFormulaType pNumber1,
                            ParamFormulaType pNumber2)

Specified by:

equal in interface NumeralFormulaManager<TFormulaInfo,TType>

equal

protected abstract TFormulaInfo equal(TFormulaInfo pParam1,
                                      TFormulaInfo pParam2)

distinct

public BooleanFormula distinct(List<ParamFormulaType> pNumbers)

Description copied from interface: NumeralFormulaManager

All given numbers are pairwise unequal.

Specified by:

distinct in interface NumeralFormulaManager<TFormulaInfo,TType>

distinctImpl

protected abstract TFormulaInfo distinctImpl(List<TFormulaInfo> pNumbers)

greaterThan

public BooleanFormula greaterThan(ParamFormulaType pNumber1,
                                  ParamFormulaType pNumber2)

Specified by:

greaterThan in interface NumeralFormulaManager<TFormulaInfo,TType>

greaterThan

protected abstract TFormulaInfo greaterThan(TFormulaInfo pParam1,
                                            TFormulaInfo pParam2)

greaterOrEquals

public BooleanFormula greaterOrEquals(ParamFormulaType pNumber1,
                                      ParamFormulaType pNumber2)

Specified by:

greaterOrEquals in interface NumeralFormulaManager<TFormulaInfo,TType>

greaterOrEquals

protected abstract TFormulaInfo greaterOrEquals(TFormulaInfo pParam1,
                                                TFormulaInfo pParam2)

lessThan

public BooleanFormula lessThan(ParamFormulaType pNumber1,
                               ParamFormulaType pNumber2)

Specified by:

lessThan in interface NumeralFormulaManager<TFormulaInfo,TType>

lessThan

protected abstract TFormulaInfo lessThan(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2)

lessOrEquals

public BooleanFormula lessOrEquals(ParamFormulaType pNumber1,
                                   ParamFormulaType pNumber2)

Specified by:

lessOrEquals in interface NumeralFormulaManager<TFormulaInfo,TType>

lessOrEquals

protected abstract TFormulaInfo lessOrEquals(TFormulaInfo pParam1,
                                             TFormulaInfo pParam2)

floor

public NumeralFormula.IntegerFormula floor(ParamFormulaType number)

Description copied from interface: NumeralFormulaManager

The floor 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.

Specified by:

floor in interface NumeralFormulaManager<TFormulaInfo,TType>

floor

protected TFormulaInfo floor(TFormulaInfo number)

toType

protected TFormulaInfo toType(TFormulaInfo param)

Make sure the value is of correct type (Int vs. Real) and add a cast if necessary.

getFormulaCreator

protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> getFormulaCreator()

extractInfo

protected final TFormulaInfo extractInfo(Formula pBits)

toSolverType

protected final TType toSolverType(FormulaType<?> formulaType)