Package org.sosy_lab.java_smt.api

Interface BooleanFormulaManager

All Known Implementing Classes:

AbstractBooleanFormulaManager, DebuggingBooleanFormulaManager

public interface BooleanFormulaManager

Manager for dealing with boolean formulas.

Method Summary

Modifier and Type	Method	Description
BooleanFormula	and(Collection<BooleanFormula> bits)
BooleanFormula	and(BooleanFormula... bits)
BooleanFormula	and(BooleanFormula bits1, BooleanFormula bits2)	Creates a formula representing an AND of the two arguments.
BooleanFormula	equivalence(BooleanFormula formula1, BooleanFormula formula2)	Creates a formula representing an equivalence of the two arguments.
<T extends Formula> T	ifThenElse(BooleanFormula cond, T f1, T f2)	Creates a formula representing IF cond THEN f1 ELSE f2.
BooleanFormula	implication(BooleanFormula formula1, BooleanFormula formula2)
boolean	isFalse(BooleanFormula formula)	Check, if the formula is the formula "FALSE".
boolean	isTrue(BooleanFormula formula)	Check, if the formula is the formula "TRUE".
default BooleanFormula	makeBoolean(boolean value)	Returns a BooleanFormula representing the given value.
BooleanFormula	makeFalse()	Shortcut for makeBoolean(false).
BooleanFormula	makeTrue()	Shortcut for makeBoolean(true).
BooleanFormula	makeVariable(String pVar)	Creates a variable with exactly the given name.
BooleanFormula	not(BooleanFormula bits)	Creates a formula representing a negation of the argument.
BooleanFormula	or(Collection<BooleanFormula> bits)
BooleanFormula	or(BooleanFormula... bits)
BooleanFormula	or(BooleanFormula bits1, BooleanFormula bits2)	Creates a formula representing an OR of the two arguments.
Collector<BooleanFormula,?,BooleanFormula>	toConjunction()	Return a stream Collector that creates a conjunction of all elements in the stream.
Set<BooleanFormula>	toConjunctionArgs(BooleanFormula f, boolean flatten)	Return a set of formulas such that a conjunction over them is equivalent to the input formula.
Collector<BooleanFormula,?,BooleanFormula>	toDisjunction()	Return a stream Collector that creates a disjunction of all elements in the stream.
Set<BooleanFormula>	toDisjunctionArgs(BooleanFormula f, boolean flatten)	Return a set of formulas such that a disjunction over them is equivalent to the input formula.
BooleanFormula	transformRecursively(BooleanFormula f, BooleanFormulaTransformationVisitor pVisitor)	Visit the formula recursively with a given BooleanFormulaVisitor.
<R> R	visit(BooleanFormula pFormula, BooleanFormulaVisitor<R> visitor)	Visit the formula with the given visitor.
void	visitRecursively(BooleanFormula f, BooleanFormulaVisitor<TraversalProcess> rFormulaVisitor)	Visit the formula recursively with a given BooleanFormulaVisitor.
BooleanFormula	xor(BooleanFormula bits1, BooleanFormula bits2)	Creates a formula representing XOR of the two arguments.

Method Detail

makeBoolean

default BooleanFormula makeBoolean(boolean value)

Returns a BooleanFormula representing the given value.

Parameters:

value - the boolean value the returned Formula should represent

Returns:

a Formula representing the given value

makeTrue

BooleanFormula makeTrue()

Shortcut for makeBoolean(true).

makeFalse

BooleanFormula makeFalse()

Shortcut for makeBoolean(false).

makeVariable

BooleanFormula 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.

equivalence

BooleanFormula equivalence(BooleanFormula formula1,
                           BooleanFormula formula2)

Creates a formula representing an equivalence of the two arguments.

Parameters:

formula1 - a Formula

formula2 - a Formula

Returns:

formula1 <-> formula2

implication

BooleanFormula implication(BooleanFormula formula1,
                           BooleanFormula formula2)

Returns:

formula1 => formula2.

isTrue

boolean isTrue(BooleanFormula formula)

Check, if the formula is the formula "TRUE". This does not include a satisfiability check, but only a syntactical matching. However, depending on the SMT solver, there might be some pre-processing of formulas such that trivial cases like "1==1" are recognized and rewritten as "TRUE", and thus such formulas might also be matched.

isFalse

boolean isFalse(BooleanFormula formula)

Check, if the formula is the formula "FALSE". This does not include a satisfiability check, but only a syntactical matching. However, depending on the SMT solver, there might be some pre-processing of formulas such that trivial cases like "1==2" are recognized and rewritten as "FALSE", and thus such formulas might also be matched.

ifThenElse

<T extends Formula> T ifThenElse(BooleanFormula cond,
                                 T f1,
                                 T f2)

Creates a formula representing IF cond THEN f1 ELSE f2.

Parameters:

cond - a Formula

f1 - a Formula

f2 - a Formula

Returns:

(IF cond THEN f1 ELSE f2)

not

BooleanFormula not(BooleanFormula bits)

Creates a formula representing a negation of the argument.

Parameters:

bits - a Formula

Returns:

!bits

and

BooleanFormula and(BooleanFormula bits1,
                   BooleanFormula bits2)

Creates a formula representing an AND of the two arguments.

Parameters:

bits1 - a Formula

bits2 - a Formula

Returns:

bits1 & bits2

and

BooleanFormula and(Collection<BooleanFormula> bits)

See Also:

and(BooleanFormula, BooleanFormula)

and

BooleanFormula and(BooleanFormula... bits)

See Also:

and(BooleanFormula, BooleanFormula)

toConjunction

Collector<BooleanFormula,?,BooleanFormula> toConjunction()

Return a stream Collector that creates a conjunction of all elements in the stream.

or

BooleanFormula or(BooleanFormula bits1,
                  BooleanFormula bits2)

Creates a formula representing an OR of the two arguments.

Parameters:

bits1 - a Formula

bits2 - a Formula

Returns:

bits1 | bits2

or

BooleanFormula or(Collection<BooleanFormula> bits)

See Also:

or(BooleanFormula, BooleanFormula)

or

BooleanFormula or(BooleanFormula... bits)

See Also:

or(BooleanFormula, BooleanFormula)

toDisjunction

Collector<BooleanFormula,?,BooleanFormula> toDisjunction()

Return a stream Collector that creates a disjunction of all elements in the stream.

xor

BooleanFormula xor(BooleanFormula bits1,
                   BooleanFormula bits2)

Creates a formula representing XOR of the two arguments.

visit

@CanIgnoreReturnValue
<R> R visit(BooleanFormula pFormula,
            BooleanFormulaVisitor<R> visitor)

Visit the formula with the given visitor.

visitRecursively

void visitRecursively(BooleanFormula f,
                      BooleanFormulaVisitor<TraversalProcess> rFormulaVisitor)

Visit the formula recursively with a given BooleanFormulaVisitor.

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.

transformRecursively

BooleanFormula transformRecursively(BooleanFormula f,
                                    BooleanFormulaTransformationVisitor pVisitor)

Visit the formula recursively with a given BooleanFormulaVisitor. The arguments each visitor method receives are already transformed.

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.

toConjunctionArgs

Set<BooleanFormula> toConjunctionArgs(BooleanFormula f,
                                      boolean flatten)

Return a set of formulas such that a conjunction over them is equivalent to the input formula.

Example output:

• For conjunction A /\ B /\ C: A, B, C
• For "true": empty set.
• For anything else: singleton set consisting of the input formula.

Parameters:

flatten - If true, flatten recursively.

toDisjunctionArgs

Set<BooleanFormula> toDisjunctionArgs(BooleanFormula f,
                                      boolean flatten)

Return a set of formulas such that a disjunction over them is equivalent to the input formula.

Example output:

• For conjunction A \/ B \/ C: A, B, C
• For "false": empty set.
• For anything else: singleton set consisting of the input formula.

Parameters:

flatten - If true, flatten recursively.