Builds a conjunction of formulas.
Builds a conjunction of formulas.
sequence of formulas to be combined
a new Formula instance that represents the conjunction of the input formulas
Returns the formula representation of a Boolean
.
Returns the formula representation of a Boolean
.
a Boolean literal to wrap into a formula
Formulas.True if input is true
and Formulas.False if input is false
Builds a disjunction of formulas.
Builds a disjunction of formulas.
sequence of formulas to be combined
a new Formula instance that represents the disjunction of the input formulas
Returns the formula representation of a propositional variable.
Returns the formula representation of a propositional variable.
The propositional variable is always fresh and unique, there is no need to use a different name for different invocations. You need to maintain a pointer to the returned instance if you want to refer to it later in your code.
a String prefix to the name of that variable
A fresh and unique propositional variable with a name starting with prefix
Contains helper functions for building Formula.
The basic building blocks of formulas are true/false literals and propositional variables. You get a PropVar with propVar and bool2formula provides an implicit conversion from
Boolean
to True/False.Once you have a Formula instance, you can combine it using its methods matching regular boolean operators. You can also use n-ary combinators or and and.