summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-07-28Merge branch 'master' into docsLinkdocsLinkAndres Noetzli
2021-07-28Make extended rewriter methods const (#6948)Andrew Reynolds
2021-07-27bv: Refactor getEqualityStatus and use for both bitblasting solvers. (#6933)Mathias Preiner
2021-07-27proof: Add eqrange expansion rule. (#6936)Mathias Preiner
2021-07-27Track instantiation reasons in proofs (#6935)Andrew Reynolds
2021-07-27Add basic LFSC utilities (#6879)Andrew Reynolds
2021-07-27Move enum value generator to own file (#6941)Andrew Reynolds
2021-07-27Minor fix for term database + central equality engine (#6928)Andrew Reynolds
2021-07-27Revert change to regression (#6940)Andrew Reynolds
2021-07-27Make all dependencies in the fast enumerator optional (#6918)Andrew Reynolds
2021-07-27Add print expression utility (#6880)Andrew Reynolds
2021-07-27Add regression for fixed `str.indexof_re` issue (#6938)Andres Noetzli
2021-07-27Minor changes from proof-new (#6937)Andrew Reynolds
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-21Print link to docs previewAndres Noetzli
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback