Module src.olaaaf.formula

Representation of logical formulas and multiple tools to use them, abstracted depending on the operator's formula.

Declaration of a new olaaaf.formula.formula.Formula

To declare a new olaaaf.formula.formula.Formula, you have multiple options:

  • Use the usual class constructors. Depending on the operator's arity, the arguments that are expected might change (namely, those represents the arguments of the operators and, as such, a different number of them could be expected). Please note that they have an optional argument name that we'll talk about in the point after next.

  • Use Python's built-in (but restrictive) operators between two existing formulas, namely:

    • & for the and operator, represented by olaaaf.formula.naryFormula.andOperator.And

    • | for the or operator, represented by olaaaf.formula.naryFormula.orOperator.Or

    • ~ for the not operator, represented by olaaaf.formula.unaryFormula.notOperator.Not

    • >> for the implication operator, represented by olaaaf.formula.binaryFormula.implicationOperator.Implication

    • // for the equivalence operator, represented by olaaaf.formula.binaryFormula.equivalenceOperator.Equivalence

    • != for the xor operator, represented by olaaaf.formula.binaryFormula.xorOperator.Xor

  • Use olaaaf.formula.formulaManager.FormulaManager.parser to declare a formula using a parser with customizable operators. While more intuitive due to the less restrictive scope of usable operators, this method of declaring formulas assume you previously named them, either via the fmName attribute in their constructor or thanks to olaaaf.formula.formulaManager.FormulaManager.declare. The operators could be customized in olaaaf.constants.Constants but are by default:

    • & for the and operator, represented by olaaaf.formula.naryFormula.andOperator.And

    • | for the or operator, represented by olaaaf.formula.naryFormula.orOperator.Or

    • ~ for the not operator, represented by olaaaf.formula.unaryFormula.notOperator.Not

    • -> for the implication operator, represented by olaaaf.formula.binaryFormula.implicationOperator.Implication

    • <-> for the equivalence operator, represented by olaaaf.formula.binaryFormula.equivalenceOperator.Equivalence

    • <+> for the xor operator, represented by olaaaf.formula.binaryFormula.xorOperator.Xor

Exemple of declaration

IntegerVariable.declare("x")

a = Not(LinearConstraint("x <= 7/9"))
b = LinearConstraint("2.4*x >= 4")

And(formulaName = "phi", a, b)
Implication(formulaName = "psi", ~(a | b), ~b)

Sub-modules

src.olaaaf.formula.binaryFormula

Representation of binary formulas, meaning formulas with 2 arguments.

src.olaaaf.formula.formula

Abstract Formula class, representing a Formula in PCMLC as a syntax tree.

src.olaaaf.formula.formulaDisplay

Utility class, allowing the user to get a visualisation of a olaaaf.formula.formula.Formula.

src.olaaaf.formula.formulaManager

This class allows the user to easily declare a new olaaaf.formula.formula.Formula thanks to olaaaf.formula.formulaManager.FormulaManager.parser …

src.olaaaf.formula.naryFormula

Representation of n-ary formulas, meaning formulas with n arguments.

src.olaaaf.formula.nullaryFormula

Representation of nullary formulas, meaning formulas with no arguments.

src.olaaaf.formula.unaryFormula

Representation of unary formulas, meaning formulas with only one argument.