Visitor schema that traverses an expression in depth-first left-first order.
Class to generate a relational encoding of functions.
Class to generate a relational encoding of functions. This means that an (n+1)-ary predicate is introduced for each n-ary function, together with axioms for totality and functionality, and that all applications of the function are replaced referring to the predicate. The state of the class consists of the mapping from functions to relations (so far), as well as the axioms that have been introduced for the relational encoding.
Application of an uninterpreted predicate to a list of terms.
Boolean combination of two formulae.
Boolean literal.
Symbolic constants.
Epsilon term, which is defined to evaluate to an arbitrary value
satisfying the formula cond
.
Epsilon term, which is defined to evaluate to an arbitrary value
satisfying the formula cond
. cond
is expected
to contain a bound variable with de Bruijn index 0.
Abstract syntax for prover input.
Abstract syntax for prover input. The language represented by the following constructors is more general than the logic that the prover actually can handle (e.g., there are also functions, equivalence, etc.). The idea is that inputs first have to be normalised in some way so that the prover can handle them.
Abstract class representing formulae in input-syntax.
If-then-else formula.
Application of an uninterpreted function to a list of terms.
An uninterpreted function with fixed arity.
An uninterpreted function with fixed arity. The function can optionally
be partial
(no totality axiom) or relational
(no functionality axiom).
Equation or inequality.
Integer literals.
Specification of an interpolation problem, consisting of two lists of formula names.
A labelled formula with name name
.
A labelled formula with name name
.
Negation of a formula.
Sum of two terms.
Application of a quantifier to a formula containing a free variable with de Bruijn index 0.
Abstract class representing terms in input-syntax.
If-then-else term.
Product between a term and an integer coefficient.
Trigger/patterns that are used to define in which way a quantified formula is supposed to be instantiated.
Trigger/patterns that are used to define in which way a quantified
formula is supposed to be instantiated. Triggers are only allowed to occur
immediately after (inside) a quantifier. This class can both represent
uni-triggers (for patterns.size == 1
and multi-triggers.
Special case for a prefix only containing zeroes
Bound variables, represented using their de Bruijn index.
Implementation of the Knuth-Bendix term order
Implementation of the Knuth-Bendix term order
The used weights are: IFunction, IConstant => as given by the weight functions IIntLit => 1 IVariable => 1 ITimes, IPlus => 0
The used basic ordering is: functions > + > * > constants > Variables > literals
Class to turn an IFormula
into a list of
IFormula
, the disjuncts of the given formula.
Class to turn an IFormula
into a list of
IFormula
, the disjuncts of the given formula. The boolean result
returned by the visitor tells whether the current (sub)formula has been added
to the parts
map.
Formula label, used to give names to different partitions used for interpolation.
Class for printing IExpression
s in pretty Scala syntax
Class for printing IExpression
s in pretty Scala syntax
Visitor for collecting all quantifiers in a formula.
Visitor for collecting all quantifiers in a formula. The visitor will not consider quantifiers expressing divisibility constraints.
Count the number of quantifiers in a formula
Class for printing IFormula
s in the SMT-Lib format
Class for printing IFormula
s in the SMT-Lib format
Count the number of quantifiers in a formula
Class to simplify input formulas using various rewritings.
Class to simplify input formulas using various rewritings.
Argument splittingLimit
controls whether
the formula is also (naively) turned into DNF.
Class for printing IFormula
s in the TPTP format
Class for printing IFormula
s in the TPTP format
A parser for TPTP, both FOF and TFF
Turn a formula into prenex form.
Class to automatically generate triggers for quantified formulae, using heuristics similar to Simplify.
Class to automatically generate triggers for quantified formulae, using
heuristics similar to Simplify. The parameter
consideredFunctions
determines which functions are allowed in
triggers. The argument of the visitor determines how many existential
quantifiers are immediately above the current position
Uniform substitution of predicates: replace all occurrences of predicates
with a formula; the replacement of an n-ary predicate can contain free variables
_0, _1, ..., _(n-1)
which are replaced with the predicate arguments.
Uniform substitution of predicates: replace all occurrences of predicates
with a formula; the replacement of an n-ary predicate can contain free variables
_0, _1, ..., _(n-1)
which are replaced with the predicate arguments.
Transformation for pulling out common disjuncts/conjuncts from conjunctions/disjunctions.
Class for printing IFormula
s in the CSIsat format
Class for printing IFormula
s in the CSIsat format
Currently, functions are not handled in this class
Substitute some of the constants in an expression with arbitrary terms
Check whether an expression contains some IVariable
,
IConstant
, IAtom
, or IFunApp
.
Check whether an expression contains some IVariable
,
IConstant
, IAtom
, or IFunApp
.
Functions for converting formulas to DNF.
Class to turn <-> into conjunction and disjunctions, eliminate if-then-else expressions and epsilon terms, and move universal quantifiers outwards (to make later Skolemisation more efficient; currently disabled)
Simple class for pulling out EX quantifiers from a formula.
Binary Boolean connectives.
Integer relation operators.
Class to compress chains of implications, for faster constraint propagation
Converter from the internal formula datastructures to the input level AST datastructures
Visitor for checking whether a formula contains any existential quantifiers without explicitly specified triggers.
Turn a formula f1 ∗ f2 ∗ ... ∗ fn
(where ∗
is some binary operator) into
List(f1, f2, ..., fn)
Turn a formula f1 ∗ f2 ∗ ... ∗ fn
(where ∗
is some binary operator) into
List(f1, f2, ..., fn)
Visitor that eliminates all occurrences of the INamedPart
operator from a formula.
Visitor that eliminates all occurrences of the INamedPart
operator from a formula.
Evaluate all (literally) constant expressions.
Substitute some predicates in an expression with arbitrary formulae
Preprocess an InputAbsy formula in order to make it suitable for proving.
Preprocess an InputAbsy formula in order to make it suitable for
proving. The result is a list of formulae, because the original formula
may contain named parts (INamedPart
).
Class for printing IFormula
s in the Princess format
Class for printing IFormula
s in the Princess format
Simple rewriting engine on the input AST datastructures
Class for printing IFormula
s in the SMT-LIB 2 format
Class for printing IFormula
s in the SMT-LIB 2 format
Simple class for pushing down blocks of EX quantifiers; turn EX x.
Simple class for pushing down blocks of EX quantifiers; turn EX x. (phi | psi) into (EX x. phi) | (EX x. psi)
Substitute some of the constants in an expression with arbitrary terms, and immediately simplify the resulting expression if possible.
Substitute variables in an expression with arbitrary terms, and immediately simplify the resulting expression if possible.
Compute the number of operators in an expression.
Visitor that is able to detect shared sub-expression (i.e., sub-expressions with object identity) and replace them with abbreviations.
Class for printing IFormula
s in the TPTP format
Class for printing IFormula
s in the TPTP format
Push negations down to the atoms in a formula
More general visitor for renaming variables.
More general visitor for renaming variables. The argument of the visitor
methods is a pair (List[Int], Int)
that describes how each
variable should be shifted: (List(0, 2, -1), 1)
specifies that
variable 0 stays the same, variable 1 is increased by 2 (renamed to 3),
variable 2 is renamed to 1, and all other variables n are renamed to n+1.
Substitute variables in an expression with arbitrary terms
Visitor schema that traverses an expression in depth-first left-first order. For each node, the method
preVisit
is called when descending and the methodpostVisit
when returning. The visitor works with iteration (not recursion) and is able to deal also with large expressions