arithconj
The class for a conjunction of equations, negated equations and inequalities
Class for storing information about eliminated predicates, without giving a precise description how their value can be reconstructed.
Class for creating models (assignments of
integer literals to constants) of Formula, for certain
special cases.
Class for creating models (assignments of
integer literals to constants) of Formula, for certain
special cases. This class is used in EliminateFactsTask
Class for creating models that assign truth values to Boolean variables.
Class for creating models (assignments of
integer literals to constants) of Formula, for certain
special cases.
Class for creating models (assignments of
integer literals to constants) of Formula, for certain
special cases. This class is used in EliminateFactsTask
Class for creating models (assignments of
integer literals to constants, and boolean variables to truth values)
of Formula, for certain
special cases.
Class for creating models (assignments of
integer literals to constants, and boolean variables to truth values)
of Formula, for certain
special cases. This class is used in EliminateFactsTask
Class for creating models based on formulas from which a reducer is able to extract an assignment.
Class for storing information about eliminated predicates, without giving a precise description how their value can be reconstructed. This is currently used for "abbreviations", which are eliminated from proof branches when it becomes clear that they will never be expanded.