These reference-counted arguments were taken by reference, which made it
necessary to clone them. If a reference-counted object is created for the
sole purpose of being passed to one of these methods, it would be cloned
unnecessarily. This changes the signatures to take these arguments by
value, shifting the responsibility of cloning the reference-counted
objects to the users of these methods.
Existential and universal quantification used redundant data
representations, while they actually share the same structure. This
unifies both into a single QuantifiedFormula type.
For convenience, support biconditionals with more than one argument.
An n-ary “if and only if” statement
F_1 <-> F_2 <-> ... <-> F_n
is to be interpreted as
F_1 <-> F_2 and F2 <-> F3 and ... and F_(n - 1) <-> F_n
This provides an abstract syntax tree for first-order logic with integer
arithmetics. Initially, the following types of formulas are supported:
- Booleans values (true and false)
- predicates
- negated formulas
- comparisons of terms (<, ≤, >, ≥, =, ≠)
- implications and biconditionals
- conjunctions and disjunctions of formulas
- existentially and universally quantified formulas
In addition, these types of terms are provided:
- Boolean values (true and false)
- integers
- strings
- special integers (infimum and supremum)
- symbolic functions
- variables
- binary operations (addition, subtraction, multiplication, division,
modulo, exponentiation)
- unary operations (absolute value, numeric negation)