projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Move non-stream options out of `printer_options.toml` (#8909)
[cvc5.git] / src / smt / solver_engine.cpp
2022-06-23 Andres NoetzliMove non-stream options out of `printer_options.toml... blob | commitdiff | raw
2022-06-03 Andrew ReynoldsDisable arithmetic static learning when unsat cores... blob | commitdiff | raw | diff to current
2022-06-01 Gereon KremerRefactor how options are passed to the printer (#8827) blob | commitdiff | raw | diff to current
2022-05-25 Andrew ReynoldsEliminate some static options access (#8795) blob | commitdiff | raw | diff to current
2022-05-25 Andrew ReynoldsAdd model-based quantifier instantiation (#8729) blob | commitdiff | raw | diff to current
2022-05-19 Andrew ReynoldsAdd options and regressions to increase coverage (... blob | commitdiff | raw | diff to current
2022-05-18 Andrew ReynoldsEliminate subtypes (#8783) blob | commitdiff | raw | diff to current
2022-05-12 Gereon KremerMake regular options access const (#8754) blob | commitdiff | raw | diff to current
2022-05-04 Andrew ReynoldsAdd declareOracleFun interface to SolverEngine (#8622) blob | commitdiff | raw | diff to current
2022-04-22 Andrew ReynoldsAdd `deep-restart` option (#8644) blob | commitdiff | raw | diff to current
2022-04-20 Andrew ReynoldsUpdates to zero level learner (#8597) blob | commitdiff | raw | diff to current
2022-04-18 Andrew ReynoldsSimplify management of separation logic heap (#8580) blob | commitdiff | raw | diff to current
2022-04-07 Andrew ReynoldsEliminate SmtSolver dependency on SolverEngineState... blob | commitdiff | raw | diff to current
2022-04-05 Mathias PreinerUpdate copyright headers for release 1.0 (#8539) blob | commitdiff | raw | diff to current
2022-04-01 Andres Noetzli[API] Add mode argument for `Solver::blockModel()`... blob | commitdiff | raw | diff to current
2022-03-30 Mathias PreinerMove cvc5::internal::context to cvc5::context. (#8451) blob | commitdiff | raw | diff to current
2022-03-30 Aina NiemetzTypeNode: Rename isSort() and getSortConstructorArity... blob | commitdiff | raw | diff to current
2022-03-29 Mathias PreinerIntroduce internal namespace and remove api namespace... blob | commitdiff | raw | diff to current
2022-03-28 Mathias PreinerRename get-interpol to get-interpolant. (#8424) blob | commitdiff | raw | diff to current
2022-03-26 yoni206Separating produce-interpols from the mode of interpola... blob | commitdiff | raw | diff to current
2022-03-25 Andrew ReynoldsUpdate checkSynth and checkSynthNext to return SynthRes... blob | commitdiff | raw | diff to current
2022-03-22 Andrew ReynoldsRefactor result class (#8313) blob | commitdiff | raw | diff to current
2022-03-14 Andrew ReynoldsRemove unecessary methods from the API (#8260) blob | commitdiff | raw | diff to current
2022-03-11 Andrew ReynoldsUpdate abduction and interpolation API to not use pass... blob | commitdiff | raw | diff to current
2022-03-04 Andrew ReynoldsAdd support for get learned literals in the API (#8099) blob | commitdiff | raw | diff to current
2022-02-24 Andrew ReynoldsCheck for free variables in several SolverEngine calls... blob | commitdiff | raw | diff to current
2022-02-23 Andrew ReynoldsFurther relax what is considered a value in the model... blob | commitdiff | raw | diff to current
2022-02-23 Gereon KremerRemove long obsolete unsafe interrupt exception (#8139) blob | commitdiff | raw | diff to current
2022-02-18 Andrew ReynoldsAdd well formed term check to solver engine (#8056) blob | commitdiff | raw | diff to current
2022-02-18 Andrew ReynoldsMake spurious assertion into warning (#8051) blob | commitdiff | raw | diff to current
2022-02-09 Andres NoetzliFix handling of `LogicException` during solving (#8000) blob | commitdiff | raw | diff to current
2022-02-08 Andrew ReynoldsDistinguish proof mode from unsat core mode (#8062) blob | commitdiff | raw | diff to current
2022-02-08 Andrew ReynoldsAlways produce assertions (#8041) blob | commitdiff | raw | diff to current
2022-01-14 Gereon KremerPreprare central model building for RANs (#7951) blob | commitdiff | raw | diff to current
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889) blob | commitdiff | raw | diff to current
2022-01-06 Andrew ReynoldsDisallow separation logic in incremental mode (#7888) blob | commitdiff | raw | diff to current
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872) blob | commitdiff | raw | diff to current
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) blob | commitdiff | raw | diff to current
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) blob | commitdiff | raw | diff to current
2021-12-20 Andrew ReynoldsAllow SyGuS subsolver to be reused in incremental mode... blob | commitdiff | raw | diff to current
2021-12-17 Andrew ReynoldsRefactoring initialization of proofs (#7834) blob | commitdiff | raw | diff to current
2021-12-08 Gereon KremerStatic options acceses again (#7771) blob | commitdiff | raw | diff to current
2021-12-07 Andrew ReynoldsTowards support for incremental sygus (#7736) blob | commitdiff | raw | diff to current
2021-12-07 Andrew ReynoldsEliminate more static calls to Rewriter::rewrite (... blob | commitdiff | raw | diff to current
2021-11-16 Haniel Barbosa[proofs] Make sure --proof-check=... is no-op when... blob | commitdiff | raw | diff to current
2021-11-09 Gereon KremerRemove command-verbosity option (#7581) blob | commitdiff | raw | diff to current
2021-11-06 Gereon KremerRemove `Notice()` in favor of new `verbose()` (#7588) blob | commitdiff | raw | diff to current
2021-11-05 Gereon KremerEliminate `Warning` macro in favor of `EnvObj::warning... blob | commitdiff | raw | diff to current
2021-11-04 Andrew ReynoldsReplace the old dump infrastructure (#7572) blob | commitdiff | raw | diff to current
2021-11-04 Gereon KremerStart refactoring of `-o` and `-v` (#7449) blob | commitdiff | raw | diff to current
2021-11-04 Gereon KremerMinor cleanup in SolverEngine::setInfo() (#7566) blob | commitdiff | raw | diff to current
2021-10-20 Andrew ReynoldsEliminate last static calls to rewriter from smt layer... blob | commitdiff | raw | diff to current
2021-10-14 Gereon KremerFix (get-info :authors) (#7373) blob | commitdiff | raw | diff to current
2021-10-12 Aina NiemetzRename SmtEngineState to SolverEngineState. (#7344) blob | commitdiff | raw | diff to current
2021-10-11 Aina NiemetzRename SmtEngineStatistics to SolverEngineStatistics... blob | commitdiff | raw | diff to current
2021-10-11 Aina NiemetzRename SmtScope to SolverEngineScope. (#7284) blob | commitdiff | raw | diff to current
2021-10-07 Andrew ReynoldsMove preprocessor to smt solver (#7321) blob | commitdiff | raw | diff to current
2021-10-07 Andrew ReynoldsEliminate more circular dependencies on solver engine... blob | commitdiff | raw | diff to current
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) blob | commitdiff | raw | diff to current
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... blob | commitdiff | raw | diff to current