git.libre-soc.org Git - cvc5.git/history - src/theory/theory

[cvc5.git] / src / theory / theory_engine.cpp

2021-02-02	Andrew Reynolds	Cleanup some includes (#5847)	blob \| commitdiff \| raw
2021-01-28	Andrew Reynolds	Reorganize calls to quantifiers engine from SmtEngine...	blob \| commitdiff \| raw \| diff to current
2021-01-28	Andrew Reynolds	Simplify lemma interface (#5819)	blob \| commitdiff \| raw \| diff to current
2021-01-28	Andrew Reynolds	Use standard equality engine information in quantifiers...	blob \| commitdiff \| raw \| diff to current
2021-01-27	Andrew Reynolds	(proof-new) Improvements to quantifiers engine and...	blob \| commitdiff \| raw \| diff to current
2021-01-26	Andrew Reynolds	Refactor quantifiers engine initialization (#5813)	blob \| commitdiff \| raw \| diff to current
2021-01-24	Andrew Reynolds	Add interface for getting preprocessed term (#5798)	blob \| commitdiff \| raw \| diff to current
2020-12-22	Andrew Reynolds	Make theory preprocess rewrite equalities a preprocessi...	blob \| commitdiff \| raw \| diff to current
2020-12-21	Andrew Reynolds	Move ownership of theory preprocessor to TheoryProxy...	blob \| commitdiff \| raw \| diff to current
2020-12-16	Andrew Reynolds	Move ownership of term formula removal to theory prepro...	blob \| commitdiff \| raw \| diff to current
2020-12-10	Gereon Kremer	Fixed a bunch of clang warnings. (#5637)	blob \| commitdiff \| raw \| diff to current
2020-12-09	Andrew Reynolds	(proof-new) Make theory preprocessor proofs self contai...	blob \| commitdiff \| raw \| diff to current
2020-12-09	Andrew Reynolds	Make decision engine independent of AssertionsPipeline...	blob \| commitdiff \| raw \| diff to current
2020-12-07	Andrew Reynolds	Do not expand theory definitions at the beginning of...	blob \| commitdiff \| raw \| diff to current
2020-12-07	Andrew Reynolds	(proof-new) Split proof ensure closed checks to own...	blob \| commitdiff \| raw \| diff to current
2020-11-20	Andrew Reynolds	Fix remove term formula policy for terms beneath quanti...	blob \| commitdiff \| raw \| diff to current
2020-11-19	Andrew Reynolds	Enable new implementation of CEGQI based on nested...	blob \| commitdiff \| raw \| diff to current
2020-11-19	Andrew Reynolds	Fix issues related to eliminating extended arithmetic...	blob \| commitdiff \| raw \| diff to current
2020-11-10	Andrew Reynolds	Add proper support for the declare-heap command for...	blob \| commitdiff \| raw \| diff to current
2020-10-22	Andrew Reynolds	(proof-new) Make theory preprocessor user-context depen...	blob \| commitdiff \| raw \| diff to current
2020-10-20	Andrew Reynolds	(proof-new) Update add lazy step interface in LazyCDPro...	blob \| commitdiff \| raw \| diff to current
2020-10-18	Andrew Reynolds	(proof-new) Improvements for theory engine (#5292)	blob \| commitdiff \| raw \| diff to current
2020-10-09	Andrew Reynolds	(proof-new) Theory engine proof producing (#5195)	blob \| commitdiff \| raw \| diff to current
2020-10-06	Andrew Reynolds	(proof-new) Add interface for trusted substitution...	blob \| commitdiff \| raw \| diff to current
2020-09-26	Andrew Reynolds	Connect the shared solver to theory engine (#5103)	blob \| commitdiff \| raw \| diff to current
2020-09-22	mudathirmahgoub	Add skeleton for theory of bags (multisets) (#5100)	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-16	Abdalrhman Mohamed	Dump commands in internal code using command printing...	blob \| commitdiff \| raw \| diff to current
2020-09-15	Andrew Reynolds	Move quantifiers engine private to own file (#5053)	blob \| commitdiff \| raw \| diff to current
2020-09-12	Andrew Reynolds	(proof-new) Update TheoryEngine lemma and conflict...	blob \| commitdiff \| raw \| diff to current
2020-09-03	Andrew Reynolds	Minor cleanup of quantifiers engine (#4994)	blob \| commitdiff \| raw \| diff to current
2020-09-03	Andrew Reynolds	(proof-new) Support proofs of quantifier instantiation...	blob \| commitdiff \| raw \| diff to current
2020-09-01	Haniel Barbosa	Removes old proof code (#4964)	blob \| commitdiff \| raw \| diff to current
2020-08-28	Andrew Reynolds	Replace Theory::Set with TheoryIdSet (#4959)	blob \| commitdiff \| raw \| diff to current
2020-08-28	Andrew Reynolds	(proof-new) Make CombinationEngine proof producing...	blob \| commitdiff \| raw \| diff to current
2020-08-26	Andrew Reynolds	Connect combination engine to theory engine (#4940)	blob \| commitdiff \| raw \| diff to current
2020-08-25	Andrew Reynolds	Add the combination engine (#4939)	blob \| commitdiff \| raw \| diff to current
2020-08-24	Andrew Reynolds	Extend the standard Theory template based on equality...	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Dynamic allocation of model equality engine (#4911)	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Connect the relevance manager to TheoryEngine and use...	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Remove BV equality slicer (#4928)	blob \| commitdiff \| raw \| diff to current
2020-08-18	Andrew Reynolds	(proof-new) Theory preprocessor proof producing (#4807)	blob \| commitdiff \| raw \| diff to current
2020-08-18	Andrew Reynolds	Quantifiers engine stores a pointer to the master equal...	blob \| commitdiff \| raw \| diff to current
2020-08-17	Andrew Reynolds	Dynamic allocation of equality engine in Theory (#4890)	blob \| commitdiff \| raw \| diff to current
2020-08-05	Andrew V. Jones	When checking models, ensure that error message is...	blob \| commitdiff \| raw \| diff to current
2020-07-28	Andrew Reynolds	Use lemma property enum for OutputChannel::lemma (...	blob \| commitdiff \| raw \| diff to current
2020-07-27	Andrew Reynolds	(proof-new) Proof production for term formula removal...	blob \| commitdiff \| raw \| diff to current
2020-07-15	Andrew Reynolds	Simplify entailment check interface (#4744)	blob \| commitdiff \| raw \| diff to current
2020-07-14	Andres Noetzli	Fix caching in TheoryEngine::getExplanation() (#4736)	blob \| commitdiff \| raw \| diff to current
2020-07-11	Andrew Reynolds	Cache explanations in TheoryEngine::getExplanation...	blob \| commitdiff \| raw \| diff to current
2020-07-11	Andrew Reynolds	(proof-new) Update Theory interface for proof-new ...	blob \| commitdiff \| raw \| diff to current
2020-07-07	Andrew Reynolds	Transfer ownership of internal Options from NodeManager...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-06-12	Andrew Reynolds	(proof-new) Split TheoryEngine (#4558)	blob \| commitdiff \| raw \| diff to current
2020-06-03	Andrew Reynolds	Update CEGQI to use lemma status instead of forcing...	blob \| commitdiff \| raw \| diff to current
2020-04-02	Andres Noetzli	Initialize theory rewriters in theories (#4197)	blob \| commitdiff \| raw \| diff to current
2020-03-31	Andrew Reynolds	Remove replay and use-theory options and idl (#4186)	blob \| commitdiff \| raw \| diff to current
2020-03-18	Alex Ozdemir	Move node visitor class from smt_util/ to expr/ (#4110)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Aina Niemetz	Move ownership of DecisionEngine into PropEngine. ...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Aina Niemetz	Revert "Move ownership of DecisionEngine into PropEngin...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Andrew Reynolds	Move ownership of DecisionEngine into PropEngine. ...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	blob \| commitdiff \| raw \| diff to current
2020-02-29	Andrew Reynolds	Throw warning instead of error for non-constant values...	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andres Noetzli	Remove portfolio leftovers (#3821)	blob \| commitdiff \| raw \| diff to current
2020-02-22	makaimann	Dump boolean propagations and conflicts for decision...	blob \| commitdiff \| raw \| diff to current
2020-02-20	Mathias Preiner	resource manager: Add statistic for every resource...	blob \| commitdiff \| raw \| diff to current
2020-02-17	Andrew Reynolds	Fix soundness bug in reduction of integer div/mod...	blob \| commitdiff \| raw \| diff to current
2019-12-17	Mathias Preiner	Generate code for options with modes. (#3561)	blob \| commitdiff \| raw \| diff to current
2019-12-16	makaimann	Trace tags for dumping the decision tree in org-mode...	blob \| commitdiff \| raw \| diff to current
2019-11-04	Andrew Reynolds	Make check synth solution robust to auxiliary assertion...	blob \| commitdiff \| raw \| diff to current
2019-11-04	Andrew Reynolds	Make getSynthSolution return a Bool (#3306)	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-10-15	Andres Noetzli	Fix OOB access (#3383)	blob \| commitdiff \| raw \| diff to current
2019-10-11	Aina Niemetz	Make order of theories explicit in the source code...	blob \| commitdiff \| raw \| diff to current
2019-09-19	Andrew Reynolds	Support context-(in)dependent decision strategies....	blob \| commitdiff \| raw \| diff to current
2019-09-16	Andrew Reynolds	Remove equality inference option for quantifiers (...	blob \| commitdiff \| raw \| diff to current
2019-09-16	Andrew Reynolds	Return RecoverableModalException when model is not...	blob \| commitdiff \| raw \| diff to current
2019-04-17	Andrew Reynolds	More use of isClosure (#2959)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-11-27	Andrew Reynolds	Lazy model construction in TheoryEngine (#2633)	blob \| commitdiff \| raw \| diff to current
2018-10-04	Andrew Reynolds	Clean remaining references to getNextDecisionRequest...	blob \| commitdiff \| raw \| diff to current
2018-09-15	Andres Noetzli	Refactor how assertions are added to decision engine...	blob \| commitdiff \| raw \| diff to current
2018-09-12	Andrew Reynolds	Initial infrastructure for theory decision manager...	blob \| commitdiff \| raw \| diff to current
2018-09-04	Andrew Reynolds	Minor improvements to theory model builder interface...	blob \| commitdiff \| raw \| diff to current
2018-08-26	Andres Noetzli	Refactor unconstrained simplification pass (#2374)	blob \| commitdiff \| raw \| diff to current
2018-08-23	Aina Niemetz	Refactor ITE simplification preprocessing pass. (#2360)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Andrew Reynolds	Remove support for flipDecision (#2319)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Tim King	Initialize inputAssertions only when proofRecipe is...	blob \| commitdiff \| raw \| diff to current
2018-08-16	Andres Noetzli	Move node algorithms to separate file (#2311)	blob \| commitdiff \| raw \| diff to current
2018-06-28	Andrew Reynolds	Remove comment about model value hack (#2118)	blob \| commitdiff \| raw \| diff to current
2018-05-27	Andrew Reynolds	Fix cegqi assertions for quantified non-linear cases...	blob \| commitdiff \| raw \| diff to current
2018-05-23	Andrew Reynolds	Add notions of evaluated kinds in TheoryModel (#1947)	blob \| commitdiff \| raw \| diff to current
2018-05-10	Aina Niemetz	Refactored BVAckermann preprocessing pass. (#1889)	blob \| commitdiff \| raw \| diff to current
2018-05-08	Mathias Preiner	Refactor bv-abstraction preprocessing pass. (#1860)	blob \| commitdiff \| raw \| diff to current
2018-05-08	Andrew Reynolds	Infrastructure for approximations in model output ...	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andrew Reynolds	Interleave quantifiers checks with ground theory checks...	blob \| commitdiff \| raw \| diff to current
2018-04-25	yoni206	Refactor bv-to-bool and bool-to-bv preprocessing passes...	blob \| commitdiff \| raw \| diff to current
2018-04-16	Andres Noetzli	RemoveTermFormulas: Remove ContainsTermITEVisitor ...	blob \| commitdiff \| raw \| diff to current
2018-04-12	Andrew Reynolds	Fixes for free variables in assertions (#1762)	blob \| commitdiff \| raw \| diff to current
next

RSS Atom