summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2021-09-07Refactoring of proof manager initialization (#7073)Andrew Reynolds
2021-09-07Refactoring and fixes of set defaults for quantifiers (#7120)Andrew Reynolds
2021-09-03EnvObj: Add options(), context(), userContext(). (#7137)Aina Niemetz
2021-09-03Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133)Andrew Reynolds
2021-09-03theory: Have Theory and TheoryArith* derive from EnvObj. (#7128)Aina Niemetz
2021-09-02EnvObj: Restrict access. (#7121)Aina Niemetz
2021-09-02Remove options::getAll() (#7111)Gereon Kremer
2021-09-02Implement lazy proof checking modes (#7106)Andrew Reynolds
2021-09-02Enable sygus-inst for FP, NIA and NRA. (#7098)Aina Niemetz
2021-09-02Add class EnvObj. (#7113)Aina Niemetz
2021-09-01Print response to get-model using the API (#7084)Andrew Reynolds
2021-09-01Make driver::totalTime a TimerStat (#7089)Gereon Kremer
2021-09-01Lazy proof reconstruction for strings theory solver (#7096)Andrew Reynolds
2021-08-31bv: Remove dump=bv-rewrites. (#7099)Aina Niemetz
2021-08-30Further refactoring of set defaults for incompatibility methods (#7072)Andrew Reynolds
2021-08-30Refactor filename handling (#7088)Gereon Kremer
2021-08-27Expand definitions in sygus operators at the SMT level (#7077)Andrew Reynolds
2021-08-27Add missing methods to Solver API for models (#7052)Andrew Reynolds
2021-08-26Eliminate currentSmtEngine for subsolver calls (#7068)Andrew Reynolds
2021-08-26Dump models for isNotEntailed results (#7071)Andrew Reynolds
2021-08-26Consolidate language types (#7065)Gereon Kremer
2021-08-24Top-level structure for set defaults (#7047)Andrew Reynolds
2021-08-24Miscellaneous changes from proof-new (#7042)Andrew Reynolds
2021-08-20Make driver use options from the solver (#6930)Gereon Kremer
2021-08-20Simplify how user-provided quantifier attributes are handled (#6963)Andrew Reynolds
2021-08-20More refactoring of set defaults (#7043)Andrew Reynolds
2021-08-20Eliminate eager model building (#7038)Andrew Reynolds
2021-08-19Catch cases where recursive functions reference functions-to-synthesize (#6993)Andrew Reynolds
2021-08-19Split proof final callback to its own file (#6984)Andrew Reynolds
2021-08-19Refactor proof output for TPTP (#7029)Andrew Reynolds
2021-08-18Make TheoryProxy use Env, simplify initialization of PropEngine (#7031)Andrew Reynolds
2021-08-17Make SmtEngineState use Env (#7028)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-16Make Theory class use Env (#7011)Gereon Kremer
2021-08-13Refactor setDefaults to use an options object (#6994)Gereon Kremer
2021-08-06Clear options manager (#6991)Gereon Kremer
2021-08-04Consolidate solver resets (#6986)Gereon Kremer
2021-08-04Add optional debug information for dumping instantiations (#6950)Andrew Reynolds
2021-08-04Refactor managed streams (#6934)Gereon Kremer
2021-08-04[proof] Add getProof to API and use it in GetProofCommand (#6974)Haniel Barbosa
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-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-27Track instantiation reasons in proofs (#6935)Andrew Reynolds
2021-07-26Move public options functions to separate file (#6671)Gereon Kremer
2021-07-26More updates to arithmetic in preparation for central equality engine (#6927)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback