parser
Introduction of triggers using the complete strategy that avoids the need for totality axioms (as in Kanger's calculus).
Visitor schema that traverses an expression in depth-first left-first order.
Introduction of triggers using the complete strategy that avoids the need for totality axioms (as in Kanger's calculus).
Introduction of triggers using the complete strategy that avoids the need for totality axioms (as in Kanger's calculus).
An extended version of the CollectingVisitor that also keeps
track of the sign of a sub-expression (positive or negative), and of the
bound variables.
An extended version of the CollectingVisitor that also keeps
track of the sign of a sub-expression (positive or negative), and of the
bound variables.
Class for collecting the functions occurring in an expression.
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.
Class managing the generation of triggers for e-matching, and the encoding of functions using relations.
Class managing the generation of triggers for e-matching, and the
encoding of functions using relations. This class is called from
Preprocessing.
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 and the given sort.
Equation between two terms.
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).
Integer 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 and the given sort.
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 and the given sort.
Application of a quantifier to a formula containing a free variable with de Bruijn index 0 and the given sort.
Bound variables, represented using their de Bruijn index and the sort.
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 and the sort.
Common trait for IExpression classes that bind variables.
Common trait for IExpression classes that bind variables.
Bound variables are represented using de Bruijn indexes.
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.
Postprocess a formula output by the prover, for instance a model or the result of interpolation or quantifier elimination.
Visitor that eliminates occurrences of the INamedPart
operator from a formula.
Visitor that eliminates occurrences of the INamedPart
operator from a formula. All parts with a name accepted by
toElim will be stripped of their name.
Class for printing IExpressions in pretty Scala syntax
Class for printing IExpressions 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 IFormulas in the SMT-Lib format
Class for printing IFormulas 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.
Introduction of triggers according to the chosen
-triggerStrategy.
Introduction of triggers according to the chosen
-triggerStrategy.
Class for collecting the variables, constants, or nullary predicates occurring in an expression.
Class for printing IFormulas in the TPTP format
Class for printing IFormulas 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.
Visitor to shift all variables with index >= offset by
shift.
Visitor to shift all variables with index >= offset by
shift.
Transformation for pulling out common disjuncts/conjuncts from conjunctions/disjunctions.
Class for printing IFormulas in the CSIsat format
Class for printing IFormulas 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 the given expression contains some predicate.
Check whether an expression contains some IVariable,
IConstant, IAtom, or IFunApp.
Check whether an expression contains some IVariable,
IConstant, IAtom, or IFunApp.
Check whether an expression contains the variable with index
index.
Check whether an expression contains the variable with index
index.
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)
Class to inline equivalences of the form p <-> f, for
some Boolean variable p.
Class to inline equivalences of the form p <-> f, for
some Boolean variable p.
Simple class for pulling out EX quantifiers from a formula.
Visitor to replace occurrences of one expression with another expression.
Class for collecting the functions occurring in an expression.
Binary Boolean connectives.
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 and any sort.
Companion object of IExpression, with various helper methods.
Companion object of IExpression, with various helper methods.
Integer relation operators.
Application of a quantifier to a formula containing a free variable with de Bruijn index 0 and any sort.
Bound variables of any sort.
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.
Visitor for checking whether a formula contains any existential quantifiers without explicitly specified triggers.
TODO: this does not capture all cases, and has quadratic complexity, should be revised.
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 IFormulas in the Princess format
Class for printing IFormulas in the Princess format
Simple rewriting engine on the input AST datastructures
Class for printing IFormulas in the SMT-LIB 2 format
Class for printing IFormulas 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 collecting the variables, constants, or nullary predicates occurring in an expression.
Class for printing IFormulas in the TPTP format
Class for printing IFormulas in the TPTP format
Push negations down to the atoms in a formula
Class for collecting the indexes of free variables occurring in an expression.
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.
Visitor to shift all variables with index >= offset by
shift.
Visitor to shift all variables with index >= offset by
shift.
Visitor that checks whether the sorts of variables are consistent with the sort of their binders.
Visitor to replace quantifiers of sort Any with sorted
quantifiers, by inferring the sort of the quantified variables.
Visitor to replace quantifiers of sort Any with sorted
quantifiers, by inferring the sort of the quantified variables.
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
preVisitis called when descending and the methodpostVisitwhen returning. The visitor works with iteration (not recursion) and is able to deal also with large expressions