Package org.sosy_lab.java_smt.basicimpl

Class AbstractFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

java.lang.Object

org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

Type Parameters:

TFormulaInfo - The solver specific type.

All Implemented Interfaces:

FormulaManager

public abstract class AbstractFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
implements FormulaManager

Simplifies building a solver from the specific theories.

Field Summary

Fields

Modifier and Type	Field	Description
static ImmutableSet<String>	BASIC_OPERATORS	Avoid using basic mathematical or logical operators of SMT-LIB2 as names for symbols.
static ImmutableBiMap<Character,String>	DISALLOWED_CHARACTER_REPLACEMENT	Mapping of disallowed char to their escaped counterparts.
static ImmutableSet<String>	SMTLIB2_KEYWORDS	Avoid using basic keywords of SMT-LIB2 as names for symbols.

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pFormulaCreator, AbstractUFManager<TFormulaInfo,?,TType,TEnv> functionManager, AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> booleanManager, @Nullable IntegerFormulaManager pIntegerManager, @Nullable RationalFormulaManager pRationalManager, @Nullable AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> bitvectorManager, @Nullable AbstractFloatingPointFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> floatingPointManager, @Nullable AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> quantifiedManager, @Nullable AbstractArrayFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> arrayManager, @Nullable AbstractSLFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> slManager, @Nullable AbstractStringFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> strManager, @Nullable AbstractEnumerationFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> enumManager)	Builds a solver from the given theory implementations.

Method Summary

Modifier and Type	Method	Description
protected BooleanFormula	applyCNFImpl(BooleanFormula pF)	Apply conjunctive normal form (CNF) transformation to the given input formula.
protected BooleanFormula	applyNNFImpl(BooleanFormula input)	Apply negation normal form (NNF) transformation to the given input formula.
protected BooleanFormula	applyQELightImpl(BooleanFormula pF)	Eliminate quantifiers from the given input formula.
BooleanFormula	applyTactic(BooleanFormula f, Tactic tactic)	Apply a tactic which performs formula transformation.
protected BooleanFormula	applyUFEImpl(BooleanFormula pF)	Eliminate UFs from the given input formula.
static void	checkVariableName(String variableName)	This method is similar to isValidName(java.lang.String) and throws an exception for invalid symbol names.
Appender	dumpFormula(BooleanFormula t)	Serialize an input formula to an SMT-LIB format.
protected abstract String	dumpFormulaImpl(TFormulaInfo t)
String	escape(String pVar)	Get an escaped symbol/name for variables or undefined functions, if necessary.
TFormulaInfo	extractInfo(Formula f)
ImmutableMap<String,Formula>	extractVariables(Formula f)	Extract names of all free variables in a formula.
ImmutableMap<String,Formula>	extractVariablesAndUFs(Formula f)	Extract the names of all free variables and UFs in a formula.
ArrayFormulaManager	getArrayFormulaManager()	Returns the Array-Theory.
AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>	getBitvectorFormulaManager()	Returns the Bitvector-Theory.
AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>	getBooleanFormulaManager()	Returns the Boolean-Theory.
EnumerationFormulaManager	getEnumerationFormulaManager()	Returns the Enumeration Theory, e.g., also known as 'limited domain'.
TEnv	getEnvironment()
FloatingPointFormulaManager	getFloatingPointFormulaManager()	Returns the Floating-Point-Theory.
FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	getFormulaCreator()
<T extends Formula> FormulaType<T>	getFormulaType(T formula)	Returns the type of the given Formula.
IntegerFormulaManager	getIntegerFormulaManager()	Returns the Integer-Theory.
AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>	getQuantifiedFormulaManager()	Returns the interface for handling quantifiers.
RationalFormulaManager	getRationalFormulaManager()	Returns the Rational-Theory.
SLFormulaManager	getSLFormulaManager()	Returns the Seperation-Logic-Theory.
StringFormulaManager	getStringFormulaManager()	Returns the String Theory.
AbstractUFManager<TFormulaInfo,?,TType,TEnv>	getUFManager()	Returns the function for dealing with uninterpreted functions (UFs).
boolean	isValidName(String pVar)	Check whether the given String can be used as symbol/name for variables or undefined functions.
<T extends Formula> T	makeApplication(FunctionDeclaration<T> declaration, List<? extends Formula> args)	Create a function application to the given list of arguments.
<T extends Formula> T	makeApplication(FunctionDeclaration<T> declaration, Formula... args)	Create a function application to the given list of arguments.
<T extends Formula> T	makeVariable(FormulaType<T> formulaType, String name)	Create variable of the type equal to formulaType.
BooleanFormula	parse(String formulaStr)	Parse a boolean formula given as a String in an SMTLIB file format.
protected abstract TFormulaInfo	parseImpl(String formulaStr)
<T extends Formula> T	simplify(T f)	Simplify an input formula, while ensuring equivalence.
protected TFormulaInfo	simplify(TFormulaInfo f)	Apply a simplification procedure for the given formula.
<T extends Formula> T	substitute(T pF, Map<? extends Formula,? extends Formula> pFromToMapping)	Substitute every occurrence of any item from changeFrom in formula f to the corresponding occurrence from changeTo.
<T extends Formula> T	transformRecursively(T f, FormulaTransformationVisitor pFormulaVisitor)	Visit the formula recursively with a given FormulaVisitor.
BooleanFormula	translateFrom(BooleanFormula formula, FormulaManager otherManager)	Translates the formula from another context into the context represented by this.
String	unescape(String pVar)	Unescape the symbol/name for variables or undefined functions, if necessary.
<R> R	visit(Formula input, FormulaVisitor<R> visitor)	Visit the formula with a given visitor.
void	visitRecursively(Formula pF, FormulaVisitor<TraversalProcess> pFormulaVisitor)	Visit the formula recursively with a given FormulaVisitor.

Methods inherited from class java.lang.Object

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

Field Detail

BASIC_OPERATORS

public static final ImmutableSet<String> BASIC_OPERATORS

Avoid using basic mathematical or logical operators of SMT-LIB2 as names for symbols.

We do not accept some names as identifiers for variables or UFs, because they easily misguide the user. Most solvers even would allow such identifiers directly, currently only SMTInterpol has problems with some of them. For consistency, we disallow those names for all solvers.

SMTLIB2_KEYWORDS

public static final ImmutableSet<String> SMTLIB2_KEYWORDS

Avoid using basic keywords of SMT-LIB2 as names for symbols.

We do not accept some names as identifiers for variables or UFs, because they easily misguide the user. Most solvers even would allow such identifiers directly, currently only SMTInterpol has problems with some of them. For consistency, we disallow those names for all solvers.

DISALLOWED_CHARACTER_REPLACEMENT

public static final ImmutableBiMap<Character,String> DISALLOWED_CHARACTER_REPLACEMENT

Mapping of disallowed char to their escaped counterparts.

Constructor Detail

AbstractFormulaManager

protected AbstractFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pFormulaCreator,
                                 AbstractUFManager<TFormulaInfo,?,TType,TEnv> functionManager,
                                 AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> booleanManager,
                                 @Nullable IntegerFormulaManager pIntegerManager,
                                 @Nullable RationalFormulaManager pRationalManager,
                                 @Nullable AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> bitvectorManager,
                                 @Nullable AbstractFloatingPointFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> floatingPointManager,
                                 @Nullable AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> quantifiedManager,
                                 @Nullable AbstractArrayFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> arrayManager,
                                 @Nullable AbstractSLFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> slManager,
                                 @Nullable AbstractStringFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> strManager,
                                 @Nullable AbstractEnumerationFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> enumManager)

Builds a solver from the given theory implementations.

Method Detail

getFormulaCreator

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

getIntegerFormulaManager

public IntegerFormulaManager getIntegerFormulaManager()

Description copied from interface: FormulaManager

Returns the Integer-Theory. Because most SAT-solvers support automatic casting between Integer- and Rational-Theory, the Integer- and the RationalFormulaManager both return the same Formulas for numeric operations like ADD, SUBTRACT, TIMES, LESSTHAN, EQUAL and others.

Specified by:

getIntegerFormulaManager in interface FormulaManager

getRationalFormulaManager

public RationalFormulaManager getRationalFormulaManager()

Description copied from interface: FormulaManager

Returns the Rational-Theory. Because most SAT-solvers support automatic casting between Integer- and Rational-Theory, the Integer- and the RationalFormulaManager both return the same Formulas for numeric operations like ADD, SUBTRACT, TIMES, LESSTHAN, EQUAL, etc.

Specified by:

getRationalFormulaManager in interface FormulaManager

getBooleanFormulaManager

public AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> getBooleanFormulaManager()

Description copied from interface: FormulaManager

Returns the Boolean-Theory.

Specified by:

getBooleanFormulaManager in interface FormulaManager

getBitvectorFormulaManager

public AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> getBitvectorFormulaManager()

Description copied from interface: FormulaManager

Returns the Bitvector-Theory.

Specified by:

getBitvectorFormulaManager in interface FormulaManager

getFloatingPointFormulaManager

public FloatingPointFormulaManager getFloatingPointFormulaManager()

Description copied from interface: FormulaManager

Returns the Floating-Point-Theory.

Specified by:

getFloatingPointFormulaManager in interface FormulaManager

getUFManager

public AbstractUFManager<TFormulaInfo,?,TType,TEnv> getUFManager()

Description copied from interface: FormulaManager

Returns the function for dealing with uninterpreted functions (UFs).

Specified by:

getUFManager in interface FormulaManager

getSLFormulaManager

public SLFormulaManager getSLFormulaManager()

Description copied from interface: FormulaManager

Returns the Seperation-Logic-Theory.

Specified by:

getSLFormulaManager in interface FormulaManager

getQuantifiedFormulaManager

public AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> getQuantifiedFormulaManager()

Description copied from interface: FormulaManager

Returns the interface for handling quantifiers.

Specified by:

getQuantifiedFormulaManager in interface FormulaManager

getArrayFormulaManager

public ArrayFormulaManager getArrayFormulaManager()

Description copied from interface: FormulaManager

Returns the Array-Theory.

Specified by:

getArrayFormulaManager in interface FormulaManager

getStringFormulaManager

public StringFormulaManager getStringFormulaManager()

Description copied from interface: FormulaManager

Returns the String Theory.

Specified by:

getStringFormulaManager in interface FormulaManager

getEnumerationFormulaManager

public EnumerationFormulaManager getEnumerationFormulaManager()

Description copied from interface: FormulaManager

Returns the Enumeration Theory, e.g., also known as 'limited domain'.

Specified by:

getEnumerationFormulaManager in interface FormulaManager

parseImpl

protected abstract TFormulaInfo parseImpl(String formulaStr)
                                   throws IllegalArgumentException

Throws:

IllegalArgumentException

parse

public BooleanFormula parse(String formulaStr)
                     throws IllegalArgumentException

Description copied from interface: FormulaManager

Parse a boolean formula given as a String in an SMTLIB file format. We expect exactly one assertion to be contained in the query.

Example: (declare-fun x () Int)(assert (= 0 x))

It depends on the used SMT solver whether the given query must be self-contained and include declarations for all used symbols or not, and also whether the query is allowed to contain symbols with equal name, but different type/sort than existing symbols. The safest way is to always declare all used symbols and to avoid conflicting types for them.

The behavior of the SMT solver is undefined if commands are provided in the SMTLIB-based String that are different from declarations or an assertion, such as push/pop or set-info. Most solvers just ignore those commands.

Variables that are defined, but not used in the assertion, might be ignored by the SMT solver and they might not be available for later usage.

Specified by:

parse in interface FormulaManager

Returns:

A single formula from the assertion in the internal representation.

Throws:

IllegalArgumentException - If the string cannot be parsed.

dumpFormulaImpl

protected abstract String dumpFormulaImpl(TFormulaInfo t)
                                   throws IOException

Throws:

IOException

dumpFormula

public Appender dumpFormula(BooleanFormula t)

Description copied from interface: FormulaManager

Serialize an input formula to an SMT-LIB format. Very useful when passing formulas between different solvers.

To get a String, simply call Object.toString() on the returned object. This method is lazy and does not create an output string until the returned object is actually used.

Specified by:

dumpFormula in interface FormulaManager

Returns:

SMT-LIB formula serialization.

getFormulaType

public final <T extends Formula> FormulaType<T> getFormulaType(T formula)

Description copied from interface: FormulaManager

Returns the type of the given Formula.

Specified by:

getFormulaType in interface FormulaManager

getEnvironment

public final TEnv getEnvironment()

extractInfo

public final TFormulaInfo extractInfo(Formula f)

applyTactic

public BooleanFormula applyTactic(BooleanFormula f,
                                  Tactic tactic)
                           throws InterruptedException

Description copied from interface: FormulaManager

Apply a tactic which performs formula transformation. The available tactics depend on the used solver.

Specified by:

applyTactic in interface FormulaManager

Throws:

InterruptedException

applyUFEImpl

protected BooleanFormula applyUFEImpl(BooleanFormula pF)
                               throws InterruptedException

Eliminate UFs from the given input formula.

Throws:

InterruptedException - Can be thrown by the native code.

applyQELightImpl

protected BooleanFormula applyQELightImpl(BooleanFormula pF)
                                   throws InterruptedException

Eliminate quantifiers from the given input formula.

This is the light version that does not need to eliminate all quantifiers.

Throws:

InterruptedException - Can be thrown by the native code.

applyCNFImpl

protected BooleanFormula applyCNFImpl(BooleanFormula pF)
                               throws InterruptedException

Apply conjunctive normal form (CNF) transformation to the given input formula.

Parameters:

pF - Input to apply the CNF transformation to.

Throws:

InterruptedException - Can be thrown by the native code.

applyNNFImpl

protected BooleanFormula applyNNFImpl(BooleanFormula input)
                               throws InterruptedException

Apply negation normal form (NNF) transformation to the given input formula.

Throws:

InterruptedException - Can be thrown by the native code.

simplify

public <T extends Formula> T simplify(T f)
                               throws InterruptedException

Description copied from interface: FormulaManager

Simplify an input formula, while ensuring equivalence.

For solvers that do not provide a simplification API, an original formula is returned.

Specified by:

simplify in interface FormulaManager

Parameters:

f - The input formula

Returns:

Simplified version of the formula

Throws:

InterruptedException

simplify

protected TFormulaInfo simplify(TFormulaInfo f)
                         throws InterruptedException

Apply a simplification procedure for the given formula.

This does not need to change something, but it might simplify the formula.

Throws:

InterruptedException - Can be thrown by the native code.

visit

public <R> R visit(Formula input,
                   FormulaVisitor<R> visitor)

Description copied from interface: FormulaManager

Visit the formula with a given visitor.

This method does not recursively visit sub-components of a formula its own, so the given FormulaVisitor needs to call such visitation on its own.

Please be aware that calling this method might cause extensive stack usage depending on the nesting of the given formula and the given FormulaVisitor. Additionally, sub-formulas that are used several times in the formula might be visited several times. For an efficient formula traversing, we also provide FormulaManager.visitRecursively(Formula, FormulaVisitor).

Specified by:

visit in interface FormulaManager

Parameters:

input - formula to be visited

visitor - an implementation that provides steps for each kind of formula.

visitRecursively

public void visitRecursively(Formula pF,
                             FormulaVisitor<TraversalProcess> pFormulaVisitor)

Description copied from interface: FormulaManager

Visit the formula recursively with a given FormulaVisitor. This method traverses sub-components of a formula automatically, depending on the return value of the TraversalProcess in the given FormulaVisitor.

This method guarantees that the traversal is done iteratively, without using Java recursion, and thus is not prone to StackOverflowErrors.

Furthermore, this method also guarantees that every equal part of the formula is visited only once. Thus, it can be used to traverse DAG-like formulas efficiently.

The traversal is done in PRE-ORDER manner with regard to caching identical subtrees, i.e., a parent will be visited BEFORE its children. The unmodified child-formulas are passed as argument to the parent's visitation.

Specified by:

visitRecursively in interface FormulaManager

transformRecursively

public <T extends Formula> T transformRecursively(T f,
                                                  FormulaTransformationVisitor pFormulaVisitor)

Description copied from interface: FormulaManager

Visit the formula recursively with a given FormulaVisitor.

This method guarantees that the traversal is done iteratively, without using Java recursion, and thus is not prone to StackOverflowErrors.

Furthermore, this method also guarantees that every equal part of the formula is visited only once. Thus, it can be used to traverse DAG-like formulas efficiently.

The traversal is done in POST-ORDER manner with regard to caching identical subtrees, i.e., a parent will be visited AFTER its children. The result of the child-visitation is passed as argument to the parent's visitation.

Specified by:

transformRecursively in interface FormulaManager

pFormulaVisitor - Transformation described by the user.

extractVariables

public ImmutableMap<String,Formula> extractVariables(Formula f)

Extract names of all free variables in a formula.

Specified by:

extractVariables in interface FormulaManager

Parameters:

f - The input formula

Returns:

Map from variable names to the corresponding formulas.

extractVariablesAndUFs

public ImmutableMap<String,Formula> extractVariablesAndUFs(Formula f)

Extract the names of all free variables and UFs in a formula.

Specified by:

extractVariablesAndUFs in interface FormulaManager

Parameters:

f - The input formula

Returns:

Map from variable names to the corresponding formulas. If an UF occurs multiple times in the input formula, an arbitrary instance of an application of this UF is in the map.

translateFrom

public BooleanFormula translateFrom(BooleanFormula formula,
                                    FormulaManager otherManager)

Description copied from interface: FormulaManager

Translates the formula from another context into the context represented by this. Default implementation relies on string serialization (FormulaManager.dumpFormula(BooleanFormula) and FormulaManager.parse(String)), but each solver may implement more efficient translation between its own contexts.

Specified by:

translateFrom in interface FormulaManager

Parameters:

formula - Formula belonging to otherContext.

otherManager - Formula manager belonging to the other context.

Returns:

Formula belonging to this context.

makeVariable

public <T extends Formula> T makeVariable(FormulaType<T> formulaType,
                                          String name)

Description copied from interface: FormulaManager

Create variable of the type equal to formulaType.

Specified by:

makeVariable in interface FormulaManager

Parameters:

formulaType - the type of the variable.

name - the name of the variable.

Returns:

the created variable.

makeApplication

public <T extends Formula> T makeApplication(FunctionDeclaration<T> declaration,
                                             List<? extends Formula> args)

Description copied from interface: FormulaManager

Create a function application to the given list of arguments.

Specified by:

makeApplication in interface FormulaManager

Parameters:

declaration - Function declaration

args - List of arguments

Returns:

Constructed formula

makeApplication

public <T extends Formula> T makeApplication(FunctionDeclaration<T> declaration,
                                             Formula... args)

Description copied from interface: FormulaManager

Create a function application to the given list of arguments.

Specified by:

makeApplication in interface FormulaManager

Parameters:

declaration - Function declaration

args - List of arguments

Returns:

Constructed formula

substitute

public <T extends Formula> T substitute(T pF,
                                        Map<? extends Formula,? extends Formula> pFromToMapping)

Description copied from interface: FormulaManager

Substitute every occurrence of any item from changeFrom in formula f to the corresponding occurrence from changeTo.

E.g. if changeFrom contains a variable a and changeTo contains a variable b all occurrences of a will be changed to b in the returned formula.

Specified by:

substitute in interface FormulaManager

Parameters:

pF - Formula to change.

pFromToMapping - Mapping of old and new formula parts.

Returns:

Formula with parts replaced.

isValidName

public final boolean isValidName(String pVar)

Check whether the given String can be used as symbol/name for variables or undefined functions. We disallow some keywords from SMTLib2 and other basic operators to be used as symbols.

This method must be kept in sync with checkVariableName(java.lang.String).

Specified by:

isValidName in interface FormulaManager

checkVariableName

public static void checkVariableName(String variableName)

This method is similar to isValidName(java.lang.String) and throws an exception for invalid symbol names. While isValidName(java.lang.String) can be used from users, this method should be used internally to validate user-given symbol names.

This method must be kept in sync with isValidName(java.lang.String).

escape

public final String escape(String pVar)

Description copied from interface: FormulaManager

Get an escaped symbol/name for variables or undefined functions, if necessary.

See FormulaManager.isValidName(String) for further details.

Specified by:

escape in interface FormulaManager

unescape

public final String unescape(String pVar)

Description copied from interface: FormulaManager

Unescape the symbol/name for variables or undefined functions, if necessary.

The result is undefined for Strings that are not properly escaped.

See FormulaManager.isValidName(String) for further details.

Specified by:

unescape in interface FormulaManager