Package org.sosy_lab.java_smt.delegate.debugging

Class DebuggingBooleanFormulaManager

java.lang.Object

org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

All Implemented Interfaces:

BooleanFormulaManager

public class DebuggingBooleanFormulaManager
extends Object
implements BooleanFormulaManager

Constructor Summary

Constructors

Constructor	Description
DebuggingBooleanFormulaManager(BooleanFormulaManager pDelegate, org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)

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

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

makeBoolean

Constructor Detail

DebuggingBooleanFormulaManager

public DebuggingBooleanFormulaManager(BooleanFormulaManager pDelegate,
                                      org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)

Method Detail

makeTrue

public BooleanFormula makeTrue()

Description copied from interface: BooleanFormulaManager

Shortcut for makeBoolean(true).

Specified by:

makeTrue in interface BooleanFormulaManager

makeFalse

public BooleanFormula makeFalse()

Description copied from interface: BooleanFormulaManager

Shortcut for makeBoolean(false).

Specified by:

makeFalse in interface BooleanFormulaManager

makeVariable

public BooleanFormula makeVariable(String pVar)

Description copied from interface: BooleanFormulaManager

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 BooleanFormulaManager

equivalence

public BooleanFormula equivalence(BooleanFormula formula1,
                                  BooleanFormula formula2)

Description copied from interface: BooleanFormulaManager

Creates a formula representing an equivalence of the two arguments.

Specified by:

equivalence in interface BooleanFormulaManager

Parameters:

formula1 - a Formula

formula2 - a Formula

Returns:

formula1 <-> formula2

implication

public BooleanFormula implication(BooleanFormula formula1,
                                  BooleanFormula formula2)

Specified by:

implication in interface BooleanFormulaManager

Returns:

formula1 => formula2.

isTrue

public boolean isTrue(BooleanFormula formula)

Description copied from interface: BooleanFormulaManager

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.

Specified by:

isTrue in interface BooleanFormulaManager

isFalse

public boolean isFalse(BooleanFormula formula)

Description copied from interface: BooleanFormulaManager

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.

Specified by:

isFalse in interface BooleanFormulaManager

ifThenElse

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

Description copied from interface: BooleanFormulaManager

Creates a formula representing IF cond THEN f1 ELSE f2.

Specified by:

ifThenElse in interface BooleanFormulaManager

Parameters:

cond - a Formula

f1 - a Formula

f2 - a Formula

Returns:

(IF cond THEN f1 ELSE f2)

not

public BooleanFormula not(BooleanFormula bits)

Description copied from interface: BooleanFormulaManager

Creates a formula representing a negation of the argument.

Specified by:

not in interface BooleanFormulaManager

Parameters:

bits - a Formula

Returns:

!bits

and

public BooleanFormula and(BooleanFormula bits1,
                          BooleanFormula bits2)

Description copied from interface: BooleanFormulaManager

Creates a formula representing an AND of the two arguments.

Specified by:

and in interface BooleanFormulaManager

Parameters:

bits1 - a Formula

bits2 - a Formula

Returns:

bits1 & bits2

and

public BooleanFormula and(Collection<BooleanFormula> bits)

Specified by:

and in interface BooleanFormulaManager

See Also:

BooleanFormulaManager.and(BooleanFormula, BooleanFormula)

and

public BooleanFormula and(BooleanFormula... bits)

Specified by:

and in interface BooleanFormulaManager

See Also:

BooleanFormulaManager.and(BooleanFormula, BooleanFormula)

toConjunction

public Collector<BooleanFormula,?,BooleanFormula> toConjunction()

Description copied from interface: BooleanFormulaManager

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

Specified by:

toConjunction in interface BooleanFormulaManager

or

public BooleanFormula or(BooleanFormula bits1,
                         BooleanFormula bits2)

Description copied from interface: BooleanFormulaManager

Creates a formula representing an OR of the two arguments.

Specified by:

or in interface BooleanFormulaManager

Parameters:

bits1 - a Formula

bits2 - a Formula

Returns:

bits1 | bits2

or

public BooleanFormula or(Collection<BooleanFormula> bits)

Specified by:

or in interface BooleanFormulaManager

See Also:

BooleanFormulaManager.or(BooleanFormula, BooleanFormula)

or

public BooleanFormula or(BooleanFormula... bits)

Specified by:

or in interface BooleanFormulaManager

See Also:

BooleanFormulaManager.or(BooleanFormula, BooleanFormula)

toDisjunction

public Collector<BooleanFormula,?,BooleanFormula> toDisjunction()

Description copied from interface: BooleanFormulaManager

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

Specified by:

toDisjunction in interface BooleanFormulaManager

xor

public BooleanFormula xor(BooleanFormula bits1,
                          BooleanFormula bits2)

Description copied from interface: BooleanFormulaManager

Creates a formula representing XOR of the two arguments.

Specified by:

xor in interface BooleanFormulaManager

visit

public <R> R visit(BooleanFormula pFormula,
                   BooleanFormulaVisitor<R> visitor)

Description copied from interface: BooleanFormulaManager

Visit the formula with the given visitor.

Specified by:

visit in interface BooleanFormulaManager

visitRecursively

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

Description copied from interface: BooleanFormulaManager

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.

Specified by:

visitRecursively in interface BooleanFormulaManager

transformRecursively

public BooleanFormula transformRecursively(BooleanFormula f,
                                           BooleanFormulaTransformationVisitor pVisitor)

Description copied from interface: BooleanFormulaManager

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.

Specified by:

transformRecursively in interface BooleanFormulaManager

toConjunctionArgs

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

Description copied from interface: BooleanFormulaManager

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.

Specified by:

toConjunctionArgs in interface BooleanFormulaManager

flatten - If true, flatten recursively.

toDisjunctionArgs

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

Description copied from interface: BooleanFormulaManager

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.

Specified by:

toDisjunctionArgs in interface BooleanFormulaManager

flatten - If true, flatten recursively.