projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Split listener classes from SmtEngine (#4816)
[cvc5.git] / src / smt / smt_engine.h
2020-07-31 Andrew ReynoldsSplit listener classes from SmtEngine (#4816) blob | commitdiff | raw
2020-07-28 Andres NoetzliReplace Expr with Node in Term/Op (#4781) blob | commitdiff | raw | diff to current
2020-07-17 Andrew ReynoldsReplace options listener infrastructure (#4764) blob | commitdiff | raw | diff to current
2020-07-16 Andrew ReynoldsSplit abstract values utility from SmtEngine (#4754) blob | commitdiff | raw | diff to current
2020-07-16 Gereon KremerRemove cumulative time limits and cpu time limits ... blob | commitdiff | raw | diff to current
2020-07-15 Andres NoetzliUse Nodes for SmtEngine assertions (#4752) blob | commitdiff | raw | diff to current
2020-07-15 Andrew ReynoldsSplit abduction solver from SmtEngine (#4733) blob | commitdiff | raw | diff to current
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... 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-06-04 Aina NiemetzNew C++ Api: Second and last batch of API guards. ... blob | commitdiff | raw | diff to current
2020-04-09 Andrew ReynoldsSplit ProcessAssertions module from SmtEngine (#4210) blob | commitdiff | raw | diff to current
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... blob | commitdiff | raw | diff to current
2020-04-01 Aina NiemetzRename checkValid/query to checkEntailed. (#4191) blob | commitdiff | raw | diff to current
2020-03-31 Andrew ReynoldsRemove replay and use-theory options and idl (#4186) blob | commitdiff | raw | diff to current
2020-03-27 Andrew ReynoldsMove set defaults function to its own file (#4154) blob | commitdiff | raw | diff to current
2020-03-17 Aina NiemetzSmtEngine: Convert members owned by SmtEngine to unique... blob | commitdiff | raw | diff to current
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) blob | commitdiff | raw | diff to current
2020-03-05 Aina NiemetzMove ownership of DecisionEngine into PropEngine. ... blob | commitdiff | raw | diff to current
2020-03-05 Aina NiemetzRevert "Move ownership of DecisionEngine into PropEngin... blob | commitdiff | raw | diff to current
2020-03-05 Andrew ReynoldsMove ownership of DecisionEngine into PropEngine. ... blob | commitdiff | raw | diff to current
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821) blob | commitdiff | raw | diff to current
2019-11-13 Andrew ReynoldsDistinguish unknown status for model printing (#3454) blob | commitdiff | raw | diff to current
2019-11-04 Andrew ReynoldsMake getSynthSolution return a Bool (#3306) blob | commitdiff | raw | diff to current
2019-09-04 Andrew ReynoldsTowards incremental SyGuS in SMT engine (#3195) blob | commitdiff | raw | diff to current
2019-08-19 Aina NiemetzNew C++ API: Add checks for Solver::checkValid and... blob | commitdiff | raw | diff to current
2019-08-14 Andrew ReynoldsCall separate SMT engine for single invocation sygus... blob | commitdiff | raw | diff to current
2019-08-14 Aina NiemetzSmtEngine: Reorganize class according to guidelines... blob | commitdiff | raw | diff to current
2019-08-13 Andrew Reynolds Track sygus variable to term relationship via attribut... blob | commitdiff | raw | diff to current
2019-08-13 Andrew ReynoldsImplement check abduct feature (#3152) blob | commitdiff | raw | diff to current
2019-08-07 Aina NiemetzNew C++ API: Add checks and tests for push/pop. (#3121) blob | commitdiff | raw | diff to current
2019-08-02 Andrew ReynoldsFlip the polarity of the argument of get-abduct (#3153) blob | commitdiff | raw | diff to current
2019-07-30 Andrew Reynolds Track solver execution mode (#3132) 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-06-04 Andres NoetzliAdd check that result matches benchmark status (#3028) blob | commitdiff | raw | diff to current
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) blob | commitdiff | raw | diff to current
2019-03-26 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744) blob | commitdiff | raw | diff to current
2019-01-11 Aina NiemetzNew C++ API: Add unit tests for setInfo, setLogic,... blob | commitdiff | raw | diff to current
2018-10-18 Haniel BarbosaIntroducing internal commands for SyGuS commands (... blob | commitdiff | raw | diff to current
2018-08-23 Haniel BarbosaMakes the filename be set in the SMT engine by default... blob | commitdiff | raw | diff to current
2018-08-15 Andres NoetzliFix dumping of get-unsat-assumptions (#2302) blob | commitdiff | raw | diff to current
2018-08-08 Andres NoetzliDelete functions instead of using CVC4_UNDEFINED (... blob | commitdiff | raw | diff to current
2018-08-01 ayveejayImprovements and tests for the API around separation... blob | commitdiff | raw | diff to current
2018-07-24 ayveejayAdding API access methods to get heap/nil expressions... blob | commitdiff | raw | diff to current
2018-05-22 Andrew ReynoldsMake sygus infer find function definitions (#1951) blob | commitdiff | raw | diff to current
2018-03-13 Aina NiemetzSmtEngine::getModel() is now public. (#1665) 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-03-02 Aina NiemetzFixed comments in smt_engine.h. 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-02-02 Haniel BarbosaOption to check solutions produced by SyGuS solver... blob | commitdiff | raw | diff to current
2018-01-25 Tim KingCommenting out throw specifiers on SmtEngine. These... blob | commitdiff | raw | diff to current
2018-01-03 Andrew ReynoldsGlobal negate (#1466) blob | commitdiff | raw | diff to current
2017-12-11 justinxu421Add new infrastructure for preprocessing passes (#1053) 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-07 Andrew ReynoldsAllow FORALL in quantifier elimination command (#1322) 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-14 Tim KingSimplifying the throw specifier of SmtEngine::checkSat... blob | commitdiff | raw | diff to current
2017-07-21 Tim KingMerge branch 'master' into cleanup-regexp blob | commitdiff | raw | diff to current
2017-07-20 Tim KingRemoving the unused CDAttribute. This makes CDHashMap... blob | commitdiff | raw | diff to current
2017-07-07 Mathias PreinerUpdate copyright headers. blob | commitdiff | raw | diff to current
2017-05-12 Andres NotzliMake signal handlers safer blob | commitdiff | raw | diff to current
2017-04-04 Clark BarrettMerge pull request #141 from 4tXJ7f/remove_def blob | commitdiff | raw | diff to current
2017-03-31 Andres NotzliRemove decl. of getStatisticsRegistry(SmtEngine*) 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-11-04 ajreynolFix a few more minor memory leaks. blob | commitdiff | raw | diff to current
2016-10-28 ajreynolAdd get instantiations utilities to API. 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-22 Tim KingDeleting the contents of d_modelGlobalsCommands before... blob | commitdiff | raw | diff to current
2016-03-08 ajreynolExtend synthesis solver to handle single invocation... blob | commitdiff | raw | diff to current
2016-02-17 ajreynolRefactor quantifiers attributes. Make quantifier elimin... blob | commitdiff | raw | diff to current
2016-02-16 ajreynolPublic interface for quantifier elimination. Minor... blob | commitdiff | raw | diff to current
2016-01-28 Tim KingAdding listeners to Options. blob | commitdiff | raw | diff to current
2016-01-09 Tim KingRemoving StatisticsRegistry's static functions current... blob | commitdiff | raw | diff to current
2016-01-06 Tim KingMoving sexpr.{cpp,h,i} from expr/ back into util/. blob | commitdiff | raw | diff to current
2016-01-06 Tim KingAdd SmtGlobals Class blob | commitdiff | raw | diff to current
2015-12-15 Tim KingRefactoring Options Handler & Library Cycle Breaking blob | commitdiff | raw | diff to current
2015-10-26 Tim KingThis commit fixes a bug related to a public header... blob | commitdiff | raw | diff to current
2015-07-31 ajreynolMake --fmf-fun and --macros-quant work in incremental... blob | commitdiff | raw | diff to current
2015-07-31 ajreynolSygus support for inductive datatypes. blob | commitdiff | raw | diff to current
2015-05-12 barrettcwMerge pull request #74 from finnhaedicke/namespace_minisat blob | commitdiff | raw | diff to current
2015-04-23 Clark BarrettMerge branch 'master' into google blob | commitdiff | raw | diff to current
2015-04-23 Liana HadareanAdded option for --check-unsat-cores and various core... blob | commitdiff | raw | diff to current
2015-02-06 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4 blob | commitdiff | raw | diff to current
2015-01-26 ajreynolOutput solutions for synthesis conjectures with --dump... blob | commitdiff | raw | diff to current
2014-11-27 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4 blob | commitdiff | raw | diff to current
2014-11-17 Liana HadareanResource-limiting work. blob | commitdiff | raw | diff to current
2014-11-10 Morgan DetersMerge branch '1.4.x' blob | commitdiff | raw | diff to current
2014-11-07 Morgan DetersMerge branch '1.4.x' blob | commitdiff | raw | diff to current
2014-11-07 Morgan DetersMerge branch '1.4.x' blob | commitdiff | raw | diff to current
2014-11-07 Morgan DetersMerge branch '1.4.x' blob | commitdiff | raw | diff to current
next