java.lang.Object
- org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

All Implemented Interfaces:: BooleanFormulaManager

public abstract class AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
implements BooleanFormulaManager

Field Summary

Fields
Modifier and Type Field Description

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

Constructor Summary

Constructors
Modifier Constructor Description

protected AbstractBooleanFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)

Method Summary

All Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`BooleanFormula`	`and(Collection<BooleanFormula> pBits)`
`BooleanFormula`	`and(BooleanFormula... pBits)`
`BooleanFormula`	`and(BooleanFormula pBits1, BooleanFormula pBits2)`	Creates a formula representing an AND of the two arguments.
`protected abstract TFormulaInfo`	`and(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`protected TFormulaInfo`	`andImpl(Collection<TFormulaInfo> pParams)`	Create an n-ary conjunction.
`BooleanFormula`	`equivalence(BooleanFormula pBits1, BooleanFormula pBits2)`	Creates a formula representing an equivalence of the two arguments.
`protected abstract TFormulaInfo`	`equivalence(TFormulaInfo bits1, TFormulaInfo bits2)`
`protected TFormulaInfo`	`extractInfo(Formula pBits)`
`protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>`	`getFormulaCreator()`
`<T extends Formula> T`	`ifThenElse(BooleanFormula pBits, T f1, T f2)`	Creates a formula representing "IF cond THEN f1 ELSE f2".
`protected abstract TFormulaInfo`	`ifThenElse(TFormulaInfo cond, TFormulaInfo f1, TFormulaInfo f2)`
`BooleanFormula`	`implication(BooleanFormula pBits1, BooleanFormula pBits2)`
`protected TFormulaInfo`	`implication(TFormulaInfo bits1, TFormulaInfo bits2)`
`boolean`	`isFalse(BooleanFormula pBits)`	Check, if the formula is the formula "FALSE".
`protected abstract boolean`	`isFalse(TFormulaInfo bits)`
`boolean`	`isTrue(BooleanFormula pBits)`	Check, if the formula is the formula "TRUE".
`protected abstract boolean`	`isTrue(TFormulaInfo bits)`
`protected abstract TFormulaInfo`	`makeBooleanImpl(boolean 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.
`protected abstract TFormulaInfo`	`makeVariableImpl(String pVar)`
`BooleanFormula`	`not(BooleanFormula pBits)`	Creates a formula representing a negation of the argument.
`protected abstract TFormulaInfo`	`not(TFormulaInfo pParam1)`
`BooleanFormula`	`or(Collection<BooleanFormula> pBits)`
`BooleanFormula`	`or(BooleanFormula... pBits)`
`BooleanFormula`	`or(BooleanFormula pBits1, BooleanFormula pBits2)`	Creates a formula representing an OR of the two arguments.
`protected abstract TFormulaInfo`	`or(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`protected TFormulaInfo`	`orImpl(Collection<TFormulaInfo> pParams)`	Create an n-ary disjunction.
`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.
`protected TType`	`toSolverType(FormulaType<?> formulaType)`
`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 pF, BooleanFormulaVisitor<TraversalProcess> pFormulaVisitor)`	Visit the formula recursively with a given `BooleanFormulaVisitor`.
`BooleanFormula`	`xor(BooleanFormula pBits1, BooleanFormula pBits2)`	Creates a formula representing XOR of the two arguments.
`protected abstract TFormulaInfo`	`xor(TFormulaInfo pParam1, TFormulaInfo pParam2)`

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

- Field Detail
  - formulaCreator
```
protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator
```
- Constructor Detail
  - AbstractBooleanFormulaManager
```
protected AbstractBooleanFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)
```
- Method Detail
  - 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
  - makeVariableImpl
```
protected abstract TFormulaInfo makeVariableImpl(String pVar)
```
  - 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
  - makeBooleanImpl
```
protected abstract TFormulaInfo makeBooleanImpl(boolean value)
```
  - not
```
public BooleanFormula not(BooleanFormula pBits)
```
    Description copied from interface: BooleanFormulaManager
    
    Creates a formula representing a negation of the argument.
    
    Specified by:
    
    not in interface BooleanFormulaManager
    
    Parameters:
    
    pBits - a Formula
    
    Returns:
    
    !bits
  - not
```
protected abstract TFormulaInfo not(TFormulaInfo pParam1)
```
  - and
```
public BooleanFormula and(BooleanFormula pBits1,
                          BooleanFormula pBits2)
```
    Description copied from interface: BooleanFormulaManager
    
    Creates a formula representing an AND of the two arguments.
    
    Specified by:
    
    and in interface BooleanFormulaManager
    
    Parameters:
    
    pBits1 - a Formula
    
    pBits2 - a Formula
    
    Returns:
    
    bits1 & bits2
  - and
```
protected abstract TFormulaInfo and(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2)
```
  - and
```
public BooleanFormula and(Collection<BooleanFormula> pBits)
```
    Specified by:
    
    and in interface BooleanFormulaManager
    
    See Also:
    
    BooleanFormulaManager.and(BooleanFormula, BooleanFormula)
  - and
```
public BooleanFormula and(BooleanFormula... pBits)
```
    Specified by:
    
    and in interface BooleanFormulaManager
    
    See Also:
    
    BooleanFormulaManager.and(BooleanFormula, BooleanFormula)
  - andImpl
```
protected TFormulaInfo andImpl(Collection<TFormulaInfo> pParams)
```
    Create an n-ary conjunction. The default implementation delegates to and(Object, Object) and assumes that all simplifications are done by that method. This method can be overridden, in which case it should filter out irrelevant operands.
    
    Parameters:
    
    pParams - A collection of at least 3 operands.
    
    Returns:
    
    A term that is equivalent to a conjunction of pParams.
  - toConjunction
```
public final 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 pBits1,
                         BooleanFormula pBits2)
```
    Description copied from interface: BooleanFormulaManager
    
    Creates a formula representing an OR of the two arguments.
    
    Specified by:
    
    or in interface BooleanFormulaManager
    
    Parameters:
    
    pBits1 - a Formula
    
    pBits2 - a Formula
    
    Returns:
    
    bits1 | bits2
  - or
```
public BooleanFormula or(BooleanFormula... pBits)
```
    Specified by:
    
    or in interface BooleanFormulaManager
    
    See Also:
    
    BooleanFormulaManager.or(BooleanFormula, BooleanFormula)
  - or
```
protected abstract TFormulaInfo or(TFormulaInfo pParam1,
                                   TFormulaInfo pParam2)
```
  - xor
```
public BooleanFormula xor(BooleanFormula pBits1,
                          BooleanFormula pBits2)
```
    Description copied from interface: BooleanFormulaManager
    
    Creates a formula representing XOR of the two arguments.
    
    Specified by:
    
    xor in interface BooleanFormulaManager
  - or
```
public BooleanFormula or(Collection<BooleanFormula> pBits)
```
    Specified by:
    
    or in interface BooleanFormulaManager
    
    See Also:
    
    BooleanFormulaManager.or(BooleanFormula, BooleanFormula)
  - orImpl
```
protected TFormulaInfo orImpl(Collection<TFormulaInfo> pParams)
```
    Create an n-ary disjunction. The default implementation delegates to or(Object, Object) and assumes that all simplifications are done by that method. This method can be overridden, in which case it should filter out irrelevant operands.
    
    Parameters:
    
    pParams - A collection of at least 3 operands.
    
    Returns:
    
    A term that is equivalent to a disjunction of pParams.
  - toDisjunction
```
public final 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
```
protected abstract TFormulaInfo xor(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2)
```
  - equivalence
```
public final BooleanFormula equivalence(BooleanFormula pBits1,
                                        BooleanFormula pBits2)
```
    Creates a formula representing an equivalence of the two arguments.
    
    Specified by:
    
    equivalence in interface BooleanFormulaManager
    
    Parameters:
    
    pBits1 - a Formula
    
    pBits2 - a Formula
    
    Returns:
    
    f1 <-> f2
  - equivalence
```
protected abstract TFormulaInfo equivalence(TFormulaInfo bits1,
                                            TFormulaInfo bits2)
```
  - implication
```
public final BooleanFormula implication(BooleanFormula pBits1,
                                        BooleanFormula pBits2)
```
    Specified by:
    
    implication in interface BooleanFormulaManager
    
    Returns:
    
    formula1 => formula2.
  - implication
```
protected TFormulaInfo implication(TFormulaInfo bits1,
                                   TFormulaInfo bits2)
```
  - isTrue
```
public final boolean isTrue(BooleanFormula pBits)
```
    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
  - isTrue
```
protected abstract boolean isTrue(TFormulaInfo bits)
```
  - isFalse
```
public final boolean isFalse(BooleanFormula pBits)
```
    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
  - isFalse
```
protected abstract boolean isFalse(TFormulaInfo bits)
```
  - ifThenElse
```
public final <T extends Formula> T ifThenElse(BooleanFormula pBits,
                                              T f1,
                                              T f2)
```
    Creates a formula representing "IF cond THEN f1 ELSE f2".
    
    Specified by:
    
    ifThenElse in interface BooleanFormulaManager
    
    Parameters:
    
    pBits - a Formula
    
    f1 - a Formula
    
    f2 - a Formula
    
    Returns:
    
    (IF cond THEN f1 ELSE f2)
  - ifThenElse
```
protected abstract TFormulaInfo ifThenElse(TFormulaInfo cond,
                                           TFormulaInfo f1,
                                           TFormulaInfo f2)
```
  - 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 pF,
                             BooleanFormulaVisitor<TraversalProcess> pFormulaVisitor)
```
    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.
  - getFormulaCreator
```
protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> getFormulaCreator()
```
  - extractInfo
```
protected final TFormulaInfo extractInfo(Formula pBits)
```
  - toSolverType
```
protected final TType toSolverType(FormulaType<?> formulaType)
```

Class AbstractBooleanFormulaManager<TFormulaInfo,​TType,​TEnv,​TFuncDecl>

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

formulaCreator

Constructor Detail

AbstractBooleanFormulaManager

Method Detail

makeVariable

makeVariableImpl

makeTrue

makeFalse

makeBooleanImpl

not

not

and

and

and

and

andImpl

toConjunction

or

or

or

xor

or

orImpl

toDisjunction

xor

equivalence

equivalence

implication

implication

isTrue

isTrue

isFalse

isFalse

ifThenElse

ifThenElse

visit

visitRecursively

transformRecursively

toConjunctionArgs

toDisjunctionArgs

getFormulaCreator

extractInfo

toSolverType

Class AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>