summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
AgeCommit message (Expand)Author
2021-08-17Make SmtEngineState use Env (#7028)Andrew Reynolds
2021-08-17Initial refactoring of set defaults (#7021)Andrew Reynolds
2021-08-04Add optional debug information for dumping instantiations (#6950)Andrew Reynolds
2021-08-03Remove dependencies on smt engine in smt solver (#6965)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-07-31Perform statistics printing via the API (#6952)Gereon Kremer
2021-07-26Move public options functions to separate file (#6671)Gereon Kremer
2021-07-22Add support for minimal unsat cores (#4605)Andres Noetzli
2021-06-15Remove public option wrappers (#6716)Gereon Kremer
2021-06-07Remove `Options::wasSetByUser()` (#6682)Gereon Kremer
2021-06-02Remove `Options::operator[]` (#6649)Gereon Kremer
2021-05-29Remove `Options::set()` method (#6556)Gereon Kremer
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
2021-05-20Remove old unsat cores (#6581)Haniel Barbosa
2021-05-19Change the default unsat cores (#6571)Haniel Barbosa
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-07Simplifications to expand definitions (#6487)Andrew Reynolds
2021-05-04Move env into smt solver, theory engine, prop engine (#6486)Andrew Reynolds
2021-04-30Use substitutions for implementing defined functions (#6437)Andrew Reynolds
2021-04-28Refactor resource manager options (#6446)Gereon Kremer
2021-04-28Remove exception headers from options.h (#6456)Gereon Kremer
2021-04-26First part of options refactoring (#6428)Gereon Kremer
2021-04-23Add assumption-based unsat cores. (#6427)Mathias Preiner
2021-04-22Reconciling proofs and unsat cores (#6405)Haniel Barbosa
2021-04-20Add InferenceId as resources (#6339)Gereon Kremer
2021-04-16Replace SExpr class by simpler conversion routines (#6363)Gereon Kremer
2021-04-15Avoid options listener for resource manager. (#6366)Gereon Kremer
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-14[unsat-cores] Improving new unsat cores (#6356)Haniel Barbosa
2021-04-14Add internal API methods for pool-based instantiation (#6350)Andrew Reynolds
2021-04-13Fix sexpr bug with AST output language. (#6329)Abdalrhman Mohamed
2021-04-12Refactor resource manager (#6322)Gereon Kremer
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-07Fixes for abducts (#6279)Andrew Reynolds
2021-04-06Remove template argument from `NodeBuilder` (#6290)Andres Noetzli
2021-04-02Minor refactoring (#6273)Gereon Kremer
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-04-01Make ResetCommand go through APISolver (#6172)Gereon Kremer
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-23Removing unused build options and deprecated proof compile flag (#6195)Haniel Barbosa
2021-03-23Remove internal includes of Api header. (#6193)Aina Niemetz
2021-03-22Move statistics from the driver into the SmtEngine (#6170)Gereon Kremer
2021-03-18When giving an SMT-LIB version, defaulting to SMT-LIB 2.6 (#6171)Haniel Barbosa
2021-03-18Move stats registry to env. (#6173)Gereon Kremer
2021-03-18Eliminate more uses of SExpr. (#6149)Abdalrhman Mohamed
2021-03-16[proof-new] Renaming proof option to be in sync with SMT-LIB (#6154)Haniel Barbosa
2021-03-12(proof-new) Miscellaneous sync to master (#6129)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback