summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
AgeCommit message (Expand)Author
2020-06-03Update CEGQI to use lemma status instead of forcing preprocess (#4551)Andrew Reynolds
2020-04-01Initialize theory rewriters in theories (#4197)Andres Noetzli
2020-03-31Remove replay and use-theory options and idl (#4186)Andrew Reynolds
2020-03-18Move node visitor class from smt_util/ to expr/ (#4110)Alex Ozdemir
2020-03-05Move ownership of DecisionEngine into PropEngine. (#3850)Aina Niemetz
2020-03-05Revert "Move ownership of DecisionEngine into PropEngine. (#3850)"Aina Niemetz
2020-03-05Move ownership of DecisionEngine into PropEngine. (#3850)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-29 Throw warning instead of error for non-constant values in check-model stages...Andrew Reynolds
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-26Remove portfolio leftovers (#3821)Andres Noetzli
2020-02-21Dump boolean propagations and conflicts for decision tree org-mode viewer (#3...makaimann
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2020-02-17 Fix soundness bug in reduction of integer div/mod (#3766)Andrew Reynolds
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-16Trace tags for dumping the decision tree in org-mode format (#2871)makaimann
2019-11-04Make check synth solution robust to auxiliary assertions (#3432)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-15Fix OOB access (#3383)Andres Noetzli
2019-10-10Make order of theories explicit in the source code. (#3379)Aina Niemetz
2019-09-19Support context-(in)dependent decision strategies. (#3281)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-09-16Return RecoverableModalException when model is not available. (#3283)Andrew Reynolds
2019-04-17More use of isClosure (#2959)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-11-27Lazy model construction in TheoryEngine (#2633)Andrew Reynolds
2018-10-04Clean remaining references to getNextDecisionRequest and simplify (#2500)Andrew Reynolds
2018-09-14Refactor how assertions are added to decision engine (#2396)Andres Noetzli
2018-09-12 Initial infrastructure for theory decision manager (#2447)Andrew Reynolds
2018-09-04Minor improvements to theory model builder interface. (#2408)Andrew Reynolds
2018-08-25Refactor unconstrained simplification pass (#2374)Andres Noetzli
2018-08-23Refactor ITE simplification preprocessing pass. (#2360)Aina Niemetz
2018-08-17Remove support for flipDecision (#2319)Andrew Reynolds
2018-08-16 Initialize inputAssertions only when proofRecipe is non-null (#2325)Tim King
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-06-28Remove comment about model value hack (#2118)Andrew Reynolds
2018-05-27Fix cegqi assertions for quantified non-linear cases. (#1999)Andrew Reynolds
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-10Refactored BVAckermann preprocessing pass. (#1889)Aina Niemetz
2018-05-08Refactor bv-abstraction preprocessing pass. (#1860)Mathias Preiner
2018-05-08Infrastructure for approximations in model output (#1884)Andrew Reynolds
2018-05-03Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)Andrew Reynolds
2018-04-25Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)yoni206
2018-04-16RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)Andres Noetzli
2018-04-12Fixes for free variables in assertions (#1762)Andrew Reynolds
2018-04-08Check free variables in assertions (#1737)Andrew Reynolds
2018-04-04Do not debug check models when unknown (#1748)Andrew Reynolds
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
2018-03-06Simplify initialization of quantifiers engine (#1641)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback