summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2021-08-04Proper printing of proofs in the internal calculus (#6975)Andrew Reynolds
2021-08-04Fix policy for merging subproofs (#6981)Andrew Reynolds
2021-08-04[proof] [dot] Fix comments on dot printer (#6983)Diego Della Rocca de Camargos
2021-08-04Add inference ids for remainder of sygus solver (#6977)Andrew Reynolds
2021-08-04Improve error messages for UF catching higher-order (#6982)Haniel Barbosa
2021-08-04syqi: Add debug information for dumping instantiations. (#6978)Mathias Preiner
2021-08-04Add optional debug information for dumping instantiations (#6950)Andrew Reynolds
2021-08-04Add containsAssumption proof utility (#6953)Andrew Reynolds
2021-08-04Refactor managed streams (#6934)Gereon Kremer
2021-08-04Add API function to get list of option names (#6971)Gereon Kremer
2021-08-04Replace numeric predicates by explicit minimum and maximum (#6976)Gereon Kremer
2021-08-04Add missing inference identifiers (#6962)Andrew Reynolds
2021-08-04[proof] Add getProof to API and use it in GetProofCommand (#6974)Haniel Barbosa
2021-08-04Add IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951)Alex Ozdemir
2021-08-03Remove dependencies on smt engine in smt solver (#6965)Andrew Reynolds
2021-08-03Use int64_t, uint64_t or double for all numeric options. (#6970)Gereon Kremer
2021-08-03Refactor shared solver to use theory builtin inference manager (#6960)Andrew Reynolds
2021-08-03Remove "inUnsatCore" flag throughout (#6964)Andrew Reynolds
2021-08-03Properly honor --stats-all and --stats-expert when printing statistics (#6967)Gereon Kremer
2021-08-02bv: Enable equality engine for bitblast-internal. (#6961)Mathias Preiner
2021-07-31Perform statistics printing via the API (#6952)Gereon Kremer
2021-07-30Allow changing certain options while solving (#6945)Gereon Kremer
2021-07-30Simplify smt2 printer (#6954)Andrew Reynolds
2021-07-29[proofs] Set BV solver to better proof-producing one when proofs on (#6903)Haniel Barbosa
2021-07-29Integrate central equality engine approach into theory engine, add option and...Andrew Reynolds
2021-07-29Minor updates to shared terms database for central equality engine (#6929)Andrew Reynolds
2021-07-28Fixes for building python wheels on manylinux2014 (#6947)makaimann
2021-07-28Minor changes to arrays in preparation for central equality engine (#6917)Andrew Reynolds
2021-07-28Only use libedit on tty inputs (#6946)Gereon Kremer
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-27Make all dependencies in the fast enumerator optional (#6918)Andrew Reynolds
2021-07-27Add print expression utility (#6880)Andrew Reynolds
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-23FP: Add option to word-blast more lazily. (#6904)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback