use new renaming for Clause checks (safer)
remove literal simplification at construction time, because
it breaks invariants on positions of subterms, etc.
only index clauses in Chaining if the calculus is enabled
changed the signature of Literal.fold_terms, so it also works
with maximal terms of ineq/arith literals;
Monome.Focus and .fold_max;
many views for arithmetic literals
more functions for Monome, Literal and Clause.Eligible
unification, substitution, etc. for Monome.Focused
added ArithLit and ArithLit.Focus to deal with arithmetic literals;
moved corresponding code from Literal/Literals to it;
unification, etc. for Monome and Monome.Focus
started implementation of arithmetic inferences
bugfixes, unification of ArithLit.Focus.t and additional index in ArithInt
detect more absurd literals (including 0!=0)
cancellation implemented
global default signature (extended by arith plugin)
arith eq. factoring
cancellative chaining; simpl rule for <= --> <; fix in eq factoring
remove cancellative eq. reflexivity
bugfix in Monome.add
use a "subsumes" function on literals, slightly more general than matching,
in Superposition.subsumes
more efficient hashing of lits
added simplification rules that return multiple clauses
to Env (and Saturate); useful for distributivity or other advanced rules
declaration of AC-property for sum in ArithInt