Releases
2.1
c-cube
released this
09 Sep 11:36
add logtk.arith
sub-library, using either zarith or num
implemented two new calculi (with corresponding term orders):
Superposition with first-class Booleans [https://link.springer.com/chapter/10.1007/978-3-030-79876-5_22]
Superposition for full HOL [https://link.springer.com/chapter/10.1007/978-3-030-79876-5_23]
old 'Case' rules are removed and replaced with corresponding 'BoolHoist' rules
a new system for selection of Boolean subterms (--bool-select)
many modes for Boolean reasoning (--boolean-reasoning)
a whole set of SAT-inspired pre- and inprocessing techniques:
Blocked clause elimination
Nonsingular predicate elimination with definition set recognition
Hidden literal elimination
Quasipure literal elimination
fixed various issues in handling clause weight, priority and literal selection heuristics
improved communication with backend
better (complete) support for renaming common subformulas
profiling that emits catapult traces (if env contains TEF=1
)
You can’t perform that action at this time.