summaryrefslogtreecommitdiff
path: root/src/smt/set_defaults.cpp
AgeCommit message (Expand)Author
2021-08-30Further refactoring of set defaults for incompatibility methods (#7072)Andrew Reynolds
2021-08-26Consolidate language types (#7065)Gereon Kremer
2021-08-24Top-level structure for set defaults (#7047)Andrew Reynolds
2021-08-20More refactoring of set defaults (#7043)Andrew Reynolds
2021-08-17Fix policy for eliminating quantified formulas (#7017)Andrew Reynolds
2021-08-17Initial refactoring of set defaults (#7021)Andrew Reynolds
2021-08-13Refactor setDefaults to use an options object (#6994)Gereon Kremer
2021-08-04Refactor managed streams (#6934)Gereon Kremer
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-26More updates to arithmetic in preparation for central equality engine (#6927)Andrew Reynolds
2021-07-22Add support for minimal unsat cores (#4605)Andres Noetzli
2021-07-15bv: Disable bv-assert-input if proofs are enabled. (#6886)Mathias Preiner
2021-07-09Implement stop-only for new justification heuristic (#6847)Andrew Reynolds
2021-07-06Integrate learned rewrite preprocessing pass (#6840)Andrew Reynolds
2021-06-30Do not apply fmfBound to standard quantifiers when only stringsExp is enabled...Andrew Reynolds
2021-06-23[hol] Disable bound fmf when HOL (#6792)Haniel Barbosa
2021-06-15Remove public option wrappers (#6716)Gereon Kremer
2021-06-11Better support for HOL parsing and set up (#6697)Haniel Barbosa
2021-06-11Remove support for lazy BV extended function reductions and inferences (#6728)Andrew Reynolds
2021-06-10Ensure bv2nat and int2bv are not rewritten when using solve-bv-as-int (#6725)Andrew Reynolds
2021-06-07Remove `Options::wasSetByUser()` (#6682)Gereon Kremer
2021-06-02Fix issues when poly is disabled (#6668)Gereon Kremer
2021-05-29Remove `Options::set()` method (#6556)Gereon Kremer
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
2021-05-20Remove old unsat cores (#6581)Haniel Barbosa
2021-05-19Change the default unsat cores (#6571)Haniel Barbosa
2021-05-19bv: Add support for --bitblast=eager. (#6516)Mathias Preiner
2021-05-17Improve integration of CAD with nl-Ext (#6542)Gereon Kremer
2021-04-26First part of options refactoring (#6428)Gereon Kremer
2021-04-23Enable strings exp by default for strings specific logics (#6424)Andrew Reynolds
2021-04-22Minor changes to unsat core default setting (#6425)Andrew Reynolds
2021-04-22Reconciling proofs and unsat cores (#6405)Haniel Barbosa
2021-04-14[unsat-cores] Improving new unsat cores (#6356)Haniel Barbosa
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-05Enable UF when pre-skolem nested option is enabled (#6282)Andrew Reynolds
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-25Add missing includes. (#6207)Gereon Kremer
2021-03-17(proof-new) Fixes to set defaults (#6163)Andrew Reynolds
2021-03-16[proof-new] Activating proofs when dumping proofs (#6155)Haniel Barbosa
2021-03-16[proof-new] Renaming proof option to be in sync with SMT-LIB (#6154)Haniel Barbosa
2021-03-09Remove logic request (#6089)Andrew Reynolds
2021-03-09(proof-new) Minor fix and allow proof option (#6085)Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-02-22(proof-new) Change proof-new option to proof (#5955)Andrew Reynolds
2021-02-16Add bit-level propagation support to BV bitblast solver. (#5906)Mathias Preiner
2021-02-09Remove track instantiations infrastructure (#5883)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback