summaryrefslogtreecommitdiff
path: root/src/smt/set_defaults.cpp
AgeCommit message (Expand)Author
2021-09-02Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-09-02Implement lazy proof checking modes (#7106)Andrew Reynolds
2021-09-02Enable sygus-inst for FP, NIA and NRA. (#7098)Aina Niemetz
2021-08-30Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-08-30Further refactoring of set defaults for incompatibility methods (#7072)Andrew Reynolds
2021-08-26Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-08-26Consolidate language types (#7065)Gereon Kremer
2021-08-24Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-08-24Top-level structure for set defaults (#7047)Andrew Reynolds
2021-08-20Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
2021-08-20More refactoring of set defaults (#7043)Andrew Reynolds
2021-08-18Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-08-17Fix policy for eliminating quantified formulas (#7017)Andrew Reynolds
2021-08-17Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-08-17Initial refactoring of set defaults (#7021)Andrew Reynolds
2021-08-16Fix from mergeajreynol
2021-08-16Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-08-13Refactor setDefaults to use an options object (#6994)Gereon Kremer
2021-08-04Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
2021-08-04Refactor managed streams (#6934)Gereon Kremer
2021-07-29Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
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-26Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-07-26More updates to arithmetic in preparation for central equality engine (#6927)Andrew Reynolds
2021-07-22Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-07-22Add support for minimal unsat cores (#4605)Andres Noetzli
2021-07-14Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-07-15bv: Disable bv-assert-input if proofs are enabled. (#6886)Mathias Preiner
2021-07-12Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
2021-07-09Implement stop-only for new justification heuristic (#6847)Andrew Reynolds
2021-07-08Formatajreynol
2021-07-06Integrate learned rewrite preprocessing pass (#6840)Andrew Reynolds
2021-07-01Merge branch 'master' into proof-newHaniel Barbosa
2021-06-30Do not apply fmfBound to standard quantifiers when only stringsExp is enabled...Andrew Reynolds
2021-06-24Merge branch 'master' into proof-newHaniel Barbosa
2021-06-23[hol] Disable bound fmf when HOL (#6792)Haniel Barbosa
2021-06-21fixHaniel Barbosa
2021-06-21Merge branch 'master' into proof-newHaniel 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-11Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
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-08Fix optionajreynol
2021-06-07Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-06-07Remove `Options::wasSetByUser()` (#6682)Gereon Kremer
2021-06-03Formatajreynol
2021-06-02Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-06-02Fix issues when poly is disabled (#6668)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback