summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-07-27Merge branch 'master' into fix6639fix6639Andrew Reynolds
2021-07-27Minor changes from proof-new (#6937)Andrew Reynolds
2021-07-26Add regression for fixed `str.indexof_re` issueAndres Noetzli
2021-07-26Miscellaneous fixes from proof-new (#6914)Andrew Reynolds
2021-07-27Add proof letify utility (#6881)Andrew Reynolds
2021-07-27Fix eq proof conversion for constant merged parameterized ops (#6926)Andrew Reynolds
2021-07-27Default equality proofs for bags and separation logic (#6932)Andrew Reynolds
2021-07-27Add sygus enumerator callback (#6923)Andrew Reynolds
2021-07-26Move public options functions to separate file (#6671)Gereon Kremer
2021-07-26Enable default equality proofs for sets (#6931)Andrew Reynolds
2021-07-26More updates to arithmetic in preparation for central equality engine (#6927)Andrew Reynolds
2021-07-25Changes to datatypes in preparation for central equality engine (#6901)Andrew Reynolds
2021-07-25Refactor equality engine setup for arithmetic congruence manager (#6902)Andrew Reynolds
2021-07-24Fix CLN build (#6920)Andres Noetzli
2021-07-23Configuration: Indicate dependencies being built (#6921)Andres Noetzli
2021-07-23Fix CoCoA build for newer compilers (#6919)Andres Noetzli
2021-07-23FP: Add option to word-blast more lazily. (#6904)Aina Niemetz
2021-07-22Simplify computation of relevant terms in datatypes (#6885)Andrew Reynolds
2021-07-22Add the central equality engine manager (#6893)Andrew Reynolds
2021-07-22Miscellaneous changes in preparation for central equality engine (#6900)Andrew Reynolds
2021-07-22Add support for minimal unsat cores (#4605)Andres Noetzli
2021-07-22Preparation for carry the rewrite rule database in the proof checker (#6915)Andrew Reynolds
2021-07-22Add std::vector<Term> Op:: getIndices() and operator[] for Op (#6397)mudathirmahgoub
2021-07-20[AUTHORS] Add CVC4 as part of CVC series (#6907)Haniel Barbosa
2021-07-20ANTLR3: Install into `CMAKE_INSTALL_LIBDIR` (#6912)Andres Noetzli
2021-07-19'CryptoMiniSat_LIBRARIES' should respect lib/lib64 (#6905)Andrew V. Jones
2021-07-18'ANTLR3_RUNTIME' should respect lib/lib64 (#6906)Andrew V. Jones
2021-07-18Add n-ary term utilities (#6896)Andrew Reynolds
2021-07-16Do not exhaustive instantiation when FMF is disabled (#6899)Andrew Reynolds
2021-07-16[Unit Tests] Avoid linking against external libs (#6898)Andres Noetzli
2021-07-16[Unit Tests] Reenable `top_scope_context_obj` (#6892)Andres Noetzli
2021-07-15Fix context for proofs of instantiations (#6890)Andrew Reynolds
2021-07-15Distinguish quantifiers preprocess as its own proof rule (#6897)Andrew Reynolds
2021-07-15Connect the equality solver to theory arith (#6894)Andrew Reynolds
2021-07-15Arithmetic equality solver (#6876)Andrew Reynolds
2021-07-15Move master equality engine notification to own file (#6877)Andrew Reynolds
2021-07-15Add node converter utility (#6878)Andrew Reynolds
2021-07-15bv: Disable bv-assert-input if proofs are enabled. (#6886)Mathias Preiner
2021-07-15bv: Rename BBSimple to NodeBitblaster. (#6891)Mathias Preiner
2021-07-15bv: Rename lazy solver to layered solver. (#6889)Mathias Preiner
2021-07-14bv: Rename simple solver to bitblast-internal. (#6888)Mathias Preiner
2021-07-14[proof] Fix open proof issues in SAT proof (#6887)Haniel Barbosa
2021-07-14Add option that exercises the previously buggy behavior (#6884)Haniel Barbosa
2021-07-14Generalize congruence handling for HO in eq proofs (#6883)Haniel Barbosa
2021-07-14Fix for context on input proof generator (#6873)Andrew Reynolds
2021-07-14Move synthesis verification check to own file (#6882)Andrew Reynolds
2021-07-14Refactor setup of proof equality engine for central EE (#6831)Andrew Reynolds
2021-07-14Fix models for sequences of infinite element type (#6870)Andrew Reynolds
2021-07-14Clean up option usage in command executor (#6844)Gereon Kremer
2021-07-14Add missing space for check macro error messages. (#6875)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback