reimplemented pre-saturation by given clause without generating inferences
bitvector module
reimplementation of the subsumption test (not tested enough yet)
fixed bug in CNF reduction
removed lazy fields from clauses to limit non-determinism;
cleaned a bit Clauses.CSet
reverted back to old term hash function; looks better
how to build and print an ordering history (building the ordering seems ok now)
forgot some cases in condensation
changed the way profiling is done;
small updates for terms, clauses, utils, precedence...
only demodulation is done backward now, but it is cleaner (and hopefully more efficient);
calculus split between different kinds of simplifications, using distinct sets;
calculus#list_simplify returns a list of clauses, without option
removed hExtlib module
update of run.py, with a CLI option to choose the DB
changed printing of stats in run.py
way to build a clause while providing selected/max literals already;
possibility to update a precedence by giving it a patch history (not tested)
featureVector is a bit smarter when building its list of features
big change in the way symbol_ordering (now 'precedence') works:
no more current_signature(), an explicit signature, computable from sets of clauses, has to be provided.
Also #refresh() does not exit anymore, but the precedence has add_symbols() to complete w.r.t.
a list of symbols given explicitely.
PartialOrder is more limited but much more efficient, and is still used to extend the precedence
in a compatible way (keeping old symbols in the same order)
update of run.py stats output
do not try to orient trivially oriented rewrite rules
possibility of changing the precedence of an ordering
when updating an ordering's precedence, check its compatibility