Skip to content
Compare
Choose a tag to compare
@c-cube c-cube released this 09 Sep 11:36
· 226 commits to master since this release
1051eaa
  • add logtk.arith sub-library, using either zarith or num
  • implemented two new calculi (with corresponding term orders):
    1. Superposition with first-class Booleans [https://link.springer.com/chapter/10.1007/978-3-030-79876-5_22]
    2. 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:
    1. Blocked clause elimination
    2. Nonsingular predicate elimination with definition set recognition
    3. Hidden literal elimination
    4. 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)