projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Utilities in preparation for print benchmark utility (#7190)
[cvc5.git] / src / smt / command.cpp
2021-09-14 Andrew ReynoldsUtilities in preparation for print benchmark utility... blob | commitdiff | raw
2021-09-08 Gereon KremerA couple of minor cleanups (#7141) blob | commitdiff | raw | diff to current
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084) blob | commitdiff | raw | diff to current
2021-08-26 Gereon KremerConsolidate language types (#7065) blob | commitdiff | raw | diff to current
2021-08-20 Gereon KremerMake driver use options from the solver (#6930) blob | commitdiff | raw | diff to current
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... blob | commitdiff | raw | diff to current
2021-08-19 Andrew ReynoldsRefactor proof output for TPTP (#7029) blob | commitdiff | raw | diff to current
2021-08-04 Gereon KremerConsolidate solver resets (#6986) blob | commitdiff | raw | diff to current
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma... blob | commitdiff | raw | diff to current
2021-08-03 Andrew ReynoldsRemove "inUnsatCore" flag throughout (#6964) blob | commitdiff | raw | diff to current
2021-06-15 Gereon KremerRemove public option wrappers (#6716) blob | commitdiff | raw | diff to current
2021-06-09 Andrew ReynoldsFixes related to printing tuples, define-fun commands... blob | commitdiff | raw | diff to current
2021-06-09 Gereon KremerPush complex check inside GetInstantiationsCommand... blob | commitdiff | raw | diff to current
2021-05-21 Andrew ReynoldsUpdate to sygus standard output for check-synth respons... blob | commitdiff | raw | diff to current
2021-05-20 Aina NiemetzFix echo printing. (#6573) blob | commitdiff | raw | diff to current
2021-05-20 Gereon KremerAdd more getters for api::Term (#6496) blob | commitdiff | raw | diff to current
2021-04-28 Gereon KremerRemove exception headers from options.h (#6456) blob | commitdiff | raw | diff to current
2021-04-20 Andrew ReynoldsAdd instantiation pool feature to the API (#6358) blob | commitdiff | raw | diff to current
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-06 Aina NiemetzNew C++ Api: Rename and move headers. (#6292) blob | commitdiff | raw | diff to current
2021-04-02 Andrew ReynoldsCleaning up friend relationships for commands (#6254) blob | commitdiff | raw | diff to current
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) blob | commitdiff | raw | diff to current
2021-04-01 Gereon KremerMake ResetCommand go through APISolver (#6172) blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) blob | commitdiff | raw | diff to current
2021-03-18 Abdalrhman MohamedEliminate more uses of SExpr. (#6149) blob | commitdiff | raw | diff to current
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw | diff to current
2021-03-04 Aina NiemetzNew C++ Api: Clean up usage of internal types in Term... blob | commitdiff | raw | diff to current
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of internal Type/TypeNodes... blob | commitdiff | raw | diff to current
2021-03-03 Abdalrhman MohamedRemove uses of SExpr class. (#6035) blob | commitdiff | raw | diff to current
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) blob | commitdiff | raw | diff to current
2021-02-01 Abdalrhman MohamedAvoid calling the printers while converting sexpr to... blob | commitdiff | raw | diff to current
2021-01-08 Haniel Barbosa[proof-new] Implementing getProof in the API and SMT... blob | commitdiff | raw | diff to current
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682) blob | commitdiff | raw | diff to current
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) blob | commitdiff | raw | diff to current
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) blob | commitdiff | raw | diff to current
2020-12-03 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2020-11-30 Abdalrhman MohamedEliminate uses of SExpr from the parser. (#5496) blob | commitdiff | raw | diff to current
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) blob | commitdiff | raw | diff to current
2020-11-26 Andrew ReynoldsRemoving infrastructure related to SMT model (#5527) blob | commitdiff | raw | diff to current
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) blob | commitdiff | raw | diff to current
2020-11-25 Andrew ReynoldsUse symbol manager for printing responses get-model... blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) blob | commitdiff | raw | diff to current
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
next