projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Use symbol manager for unsat cores (#5468)
[cvc5.git] / src / smt / command.cpp
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) blob | commitdiff | raw
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) blob | commitdiff | raw | diff to current
2020-11-12 Andrew ReynoldsFix printing of define named function (#5425) blob | commitdiff | raw | diff to current
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) blob | commitdiff | raw | diff to current
2020-11-11 Andrew ReynoldsPass symbol manager to commands (#5410) blob | commitdiff | raw | diff to current
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... blob | commitdiff | raw | diff to current
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) blob | commitdiff | raw | diff to current
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... blob | commitdiff | raw | diff to current
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... blob | commitdiff | raw | diff to current
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) blob | commitdiff | raw | diff to current
2020-10-27 Abdalrhman MohamedRefactor DeclareSygusVarCommand and SynthFunCommand... blob | commitdiff | raw | diff to current
2020-10-20 Abdalrhman MohamedRemove some Commands from the API. (#5268) blob | commitdiff | raw | diff to current
2020-10-10 Abdalrhman MohamedProvide API version of some SMT Commands. (#5222) blob | commitdiff | raw | diff to current
2020-10-06 Abdalrhman MohamedRecover from some exceptions. (#5203) blob | commitdiff | raw | diff to current
2020-09-23 Abdalrhman MohamedRefactor Commands to use the Public API. (#5105) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... blob | commitdiff | raw | diff to current
2020-09-04 Abdalrhman MohamedUse Result::Sat instead of BenchmarkStatus in printers... blob | commitdiff | raw | diff to current
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) blob | commitdiff | raw | diff to current
2020-08-20 Andrew ReynoldsSplit QuantElimSolver from SmtEngine (#4919) blob | commitdiff | raw | diff to current
2020-08-18 Abdalrhman MohamedRefactor functions that print commands (Part 2) (#4905) blob | commitdiff | raw | diff to current
2020-08-18 Andrew ReynoldsSplit SygusSolver from SmtEngine (#4891) blob | commitdiff | raw | diff to current
2020-08-12 Abdalrhman MohamedRefactor functions that print commands (Part 1) (#4869) blob | commitdiff | raw | diff to current
2020-08-06 Andrew ReynoldsSplit preprocessor from SmtEngine (#4854) blob | commitdiff | raw | diff to current
2020-08-05 Andrew ReynoldsSplit Assertions from SmtEngine (#4788) blob | commitdiff | raw | diff to current
2020-08-04 Abdalrhman MohamedModify the smt2 parser to use the Sygus grammar. (... blob | commitdiff | raw | diff to current
2020-07-15 Andrew ReynoldsSplit abduction solver from SmtEngine (#4733) blob | commitdiff | raw | diff to current
2020-07-11 Andrew V. JonesAdd support for printing 'get-abduct' in verbose mode... blob | commitdiff | raw | diff to current
2020-06-30 Ying ShengInterpolation step 1 (#4638) blob | commitdiff | raw | diff to current
2020-06-25 Andrew ReynoldsRemove sygus1 parser (#4651) blob | commitdiff | raw | diff to current
2020-06-19 Andres NoetzliAdd logic check for define-fun(s)-rec (#4577) blob | commitdiff | raw | diff to current
2020-06-16 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2020-06-06 Andres NoetzliKeep definitions when global-declarations enabled ... blob | commitdiff | raw | diff to current
2020-04-01 Aina NiemetzRename checkValid/query to checkEntailed. (#4191) blob | commitdiff | raw | diff to current
2020-03-06 Andrew ReynoldsSimplify DatatypeDeclarationCommand command (#3928) blob | commitdiff | raw | diff to current
2020-02-20 Andres NoetzliRemove unused code (#3782) blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) blob | commitdiff | raw | diff to current
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) blob | commitdiff | raw | diff to current
2019-12-16 makaimannTrace tags for dumping the decision tree in org-mode... blob | commitdiff | raw | diff to current
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... blob | commitdiff | raw | diff to current
2019-07-29 Andrew ReynoldsModel blocker feature (#3112) blob | commitdiff | raw | diff to current
2019-07-29 Andrew ReynoldsSupport get-abduct smt2 command (#3122) blob | commitdiff | raw | diff to current
2019-04-30 Andrew ReynoldsEliminate APPLY kind (#2976) blob | commitdiff | raw | diff to current
2019-03-26 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2018-10-22 Andres NoetzliRecover from wrong use of get-info :reason-unknown... blob | commitdiff | raw | diff to current
2018-10-18 Haniel BarbosaIntroducing internal commands for SyGuS commands (... blob | commitdiff | raw | diff to current
2018-08-21 Tim KingRemoving unused bool members in command.cpp. Also initi... blob | commitdiff | raw | diff to current
2018-08-14 Andres NoetzliFix get-unsat-assumptions output (#2301) blob | commitdiff | raw | diff to current
2018-06-25 Aina NiemetzUpdated copyright headers. blob | commitdiff | raw | diff to current
2018-05-21 Andrew ReynoldsImprovements in parsing and printing related to mixed... blob | commitdiff | raw | diff to current
2018-04-10 Aina NiemetzFix dumping of benchmark in SmtEngine::checkSatisfiabil... blob | commitdiff | raw | diff to current
2018-03-09 Aina NiemetzAdd support for SMT-LIB v2.5 command get-unsat-assumpti... blob | commitdiff | raw | diff to current
2018-03-05 Aina NiemetzAdd support for check-sat-assuming. (#1637) blob | commitdiff | raw | diff to current
2018-02-28 Aina NiemetzSmtEngine::getAssignment now returns a vector of assign... blob | commitdiff | raw | diff to current
2018-01-08 Tim KingRemoves throw specifiers from command.{h,cpp}. (#1485) blob | commitdiff | raw | diff to current
2017-12-07 Andrew ReynoldsAdd command for define-fun-rec and add to API (#1412) blob | commitdiff | raw | diff to current
2017-11-15 Tim KingAdding garbage collection for Proof objects. (#1294) blob | commitdiff | raw | diff to current
2017-11-14 Tim KingCleaning up exporting vectors within commands. Resolves... blob | commitdiff | raw | diff to current
2017-11-03 Andrew ReynoldsSygus clean main (#1297) blob | commitdiff | raw | diff to current
2017-10-17 Tim KingMaking the values argument const in the SetUserAttribut... blob | commitdiff | raw | diff to current
2017-10-11 Andrew ReynoldsMove unsat core names to smt engine (#1192) blob | commitdiff | raw | diff to current
2017-09-26 Tim KingFixing CIDs 1172014 and 1172013: Initializing members... blob | commitdiff | raw | diff to current
2017-09-26 Tim KingCID 1362904: Initializing GetInstantiationsCommand... blob | commitdiff | raw | diff to current
2017-09-25 Tim KingCID 1362907: Initializing d_smtEngine to nullptr. ... blob | commitdiff | raw | diff to current
2017-09-19 Andres NoetzliFix issue #1074, improve non-fatal error handling ... blob | commitdiff | raw | diff to current
2017-07-07 Mathias PreinerUpdate copyright headers. blob | commitdiff | raw | diff to current
2017-03-30 Clark BarrettMerge pull request #139 from 4tXJ7f/remove_throw blob | commitdiff | raw | diff to current
2017-03-30 Andres Notzli[Coverity] Remove throw qualifiers in src/smt blob | commitdiff | raw | diff to current
2016-04-20 PaulMengupdate from the master blob | commitdiff | raw | diff to current
2016-04-09 GuyMerge branch 'master' of https://github.com/CVC4/CVC4 blob | commitdiff | raw | diff to current
2016-04-04 Tim KingUpdating the copyright headers and scripts. blob | commitdiff | raw | diff to current
2016-03-08 ajreynolExtend synthesis solver to handle single invocation... blob | commitdiff | raw | diff to current
2016-02-16 ajreynolPublic interface for quantifier elimination. Minor... blob | commitdiff | raw | diff to current
2016-02-02 Tim KingMoving dump.*, command.*, model.*, and ite_removal... blob | commitdiff | raw | diff to current