Class to represent the context of constants bound above a certain node in the proof tree.
Class to represent the set of constants that are considered as "free" (i.e., that are only unifiable with themselves).
Class to represent the set of constants that are considered as "free" (i.e., that are only unifiable with themselves). Objects of this class are stored in the nodes of proof tree and are updated when the proof is expanded in order to eventually reach a fixed point.
TODO: avoid the creation of new objects whenever possible
A prover that tries to construct an exhaustive proof for a given goal.
A prover that tries to construct an exhaustive proof for a given goal. The
prover tries to optimise by early stopping the expansion of the proof tree
if it is detected that a certain subtree can never yield a satisfiable
closing constraint. There are two main modes of operation: with
depthFirst
, it is tried to derive a satisfiable constraint from
the given problem, without aiming for exhaustiveness. Without this option,
the tree is expanded depth-first until it is exhaustive (which terminates
in the case of PA formulae, but not in general).
A prover that tries to construct a countermodel of a ground formula.
A prover that tries to construct a countermodel of a ground formula. This
prover works in depth-first mode, in contrast to the
ExhaustiveProver
.
A prover that tries to construct a countermodel of a ground formula.
A prover that tries to construct a countermodel of a ground formula. This
prover works in depth-first mode, in contrast to the
ExhaustiveProver
.
Prover to eliminate quantifiers in a PA formula.
Prover to eliminate quantifiers in a PA formula. The prover is losely based on the idea in the paper "A Quantifier Elimination Algorithm for Linear Real Arithmetic" by David Monniaux, although it does not explicitly compute solutions of the matrix of a quantified formula like in the paper. Instead, the constraint extracted from an exhaustive subtree is injected as a lemma into other subtrees and used to close such subtrees earlier.
It is assumed that it is never necessary to adjust the constant freedom of a
proof tree in this setting, because all constants that shield formulas also
have to be eliminated constants and, thus, never occur in constraints
anyway. This makes it possible to construct proof trees in a purely
depth-first way (just like in the ModelSearchProver
)
TODO: at the moment, this prover does not support theories like bit-vectors or multiplication
Class to represent the context of constants bound above a certain node in the proof tree. This constant can be seen as a partial ordering on constants: inner bound constants are bigger than outer bound constants