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

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

2020-08-21	Andrew Reynolds	Dynamic allocation of model equality engine (#4911)	blob \| commitdiff \| raw
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
2018-04-08	Andrew Reynolds	Check free variables in assertions (#1737)	blob \| commitdiff \| raw \| diff to current
2018-04-04	Andrew Reynolds	Do not debug check models when unknown (#1748)	blob \| commitdiff \| raw \| diff to current
2018-03-07	Mathias Preiner	Make statistics output consistent. (#1647)	blob \| commitdiff \| raw \| diff to current
2018-03-06	Andrew Reynolds	Simplify initialization of quantifiers engine (#1641)	blob \| commitdiff \| raw \| diff to current
2018-02-22	Aina Niemetz	Fixed disabling the BV equality slicer for quantifiers...	blob \| commitdiff \| raw \| diff to current
2018-02-22	Aina Niemetz	Disable BV equality slicer if not pure QF_BV. (#1619)	blob \| commitdiff \| raw \| diff to current
2018-02-14	Andrew Reynolds	Quantifiers subdirectories (#1608)	blob \| commitdiff \| raw \| diff to current
2018-02-02	Haniel Barbosa	Option to check solutions produced by SyGuS solver...	blob \| commitdiff \| raw \| diff to current
2018-01-16	Tim King	Removing more miscellaneous throw specifiers. (#1509)	blob \| commitdiff \| raw \| diff to current
2017-12-08	Andrew Reynolds	Make collect model info return a Bool (#1421)	blob \| commitdiff \| raw \| diff to current
2017-12-07	Andrew Reynolds	Add command for define-fun-rec and add to API (#1412)	blob \| commitdiff \| raw \| diff to current
2017-11-15	Tim King	Adding garbage collection for Proof objects. (#1294)	blob \| commitdiff \| raw \| diff to current
2017-11-01	Andrew Reynolds	(Move-only) Refactor and document theory model part...	blob \| commitdiff \| raw \| diff to current
2017-10-26	Tim King	Removing throw specifiers from OutputChannel and subcla...	blob \| commitdiff \| raw \| diff to current
2017-09-14	Martin	Floating point symfpu support (#1093)	blob \| commitdiff \| raw \| diff to current
2017-08-24	Andrew Reynolds	Merge pull request #191 from timothy-king/cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-08-24	Andres Noetzli	Fix typos	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Merge branch 'master' into cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Moving from the gnu extensions for hash maps to the...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-06-21	Andrew Reynolds	Merge pull request #175 from CVC4/fix_uninit	blob \| commitdiff \| raw \| diff to current
2017-06-18	ajreynol	Fix assertion	blob \| commitdiff \| raw \| diff to current
2017-06-18	ajreynol	Minor change to ensureTheoryAtoms for bug 828.	blob \| commitdiff \| raw \| diff to current
2017-04-04	ajreynol	Simplify Theory::collectModelInfo interface to not...	blob \| commitdiff \| raw \| diff to current
2017-04-04	Clark Barrett	Merge pull request #141 from 4tXJ7f/remove_def	blob \| commitdiff \| raw \| diff to current
2017-04-03	Andrew Reynolds	Merge pull request #142 from timothy-king/nlAlgMerge	blob \| commitdiff \| raw \| diff to current
2017-04-03	Tim King	Adding a model based axiom instantiation scheme for...	blob \| commitdiff \| raw \| diff to current
2017-03-27	Clark Barrett	Merge pull request #137 from 4tXJ7f/throw_quals	blob \| commitdiff \| raw \| diff to current
2017-03-27	Tim King	Making the ExtTheory object a private member of Theory.	blob \| commitdiff \| raw \| diff to current
2017-03-27	Tim King	Making ppNotifyAssertions take a const vector.	blob \| commitdiff \| raw \| diff to current
2017-03-27	Tim King	Moving the CareGraph into its own file.	blob \| commitdiff \| raw \| diff to current
2017-03-24	ajreynol	Refactor model building for quantifiers to be a single...	blob \| commitdiff \| raw \| diff to current
2017-03-06	Clark Barrett	Adding support for bool-to-bv	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Minor cleanup and reorganization related to last commit.	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2017-01-04	Andrew Reynolds	Merge pull request #122 from 4tXJ7f/fix_lfsc_str	blob \| commitdiff \| raw \| diff to current
2017-01-04	guykatzz	Merge pull request #120 from 4tXJ7f/fix_f_pp_holes	blob \| commitdiff \| raw \| diff to current
2016-12-17	Andres Notzli	Fix dependency tracing for fewerPreprocessingHoles	blob \| commitdiff \| raw \| diff to current
next

RSS Atom