summaryrefslogtreecommitdiff
path: root/src/smt/set_defaults.cpp
AgeCommit message (Expand)Author
2021-10-27Deterministic variables for RE elim (#7489)Andrew Reynolds
2021-10-26Disable sygus-inst when incremental (#7485)Andrew Reynolds
2021-10-25Add new method for enumerating unsat queries with SyGuS (#7459)Andrew Reynolds
2021-10-25Remove HOL/fmf bound messages in set defaults (#7487)Andrew Reynolds
2021-10-25Add inference for count map (#7264)mudathirmahgoub
2021-10-22Remove options::X__name (#7414)Gereon Kremer
2021-10-22Remove `--uf-ho` option (#7463)Andrew Reynolds
2021-10-07Eliminate more circular dependencies on solver engine (#7311)Andrew Reynolds
2021-10-06Change semantics of dumpUnsatCoresFull (#7314)Gereon Kremer
2021-09-30Rename SmtEngine to SolverEngine. (#7282)Aina Niemetz
2021-09-14Add get-difficulty to the API (#7194)Andrew Reynolds
2021-09-13Connect difficulty manager to TheoryEngine (#7161)Andrew Reynolds
2021-09-10More refactoring of set defaults (#7160)Andrew Reynolds
2021-09-09Disable shared selectors for quantified logics without SyGuS (#7156)Andrew Reynolds
2021-09-08Add option for using bound inference for relevant assertions (#7152)Andrew Reynolds
2021-09-07Refactoring and fixes of set defaults for quantifiers (#7120)Andrew Reynolds
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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback