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

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

2020-08-25	Andrew Reynolds	Add the combination engine (#4939)	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	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-14	Andrew Reynolds	Simplify equality engine notifications (#4896)	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-15	Andrew Reynolds	Simplify entailment check interface (#4744)	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-08	Andres Noetzli	Perform theory widening eagerly (#4044)	blob \| commitdiff \| raw \| diff to current
2020-04-03	Andres Noetzli	Update theory rewriter ownership, add stats to strings...	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-11	Andres Noetzli	reset-assertions: Update TheoryEngine's PropEngine...	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-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-20	Mathias Preiner	resource manager: Add statistic for every resource...	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-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-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-24	Mathias Preiner	Do not use __ prefix for header guards. (#2974)	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-12	Andrew Reynolds	Initial infrastructure for theory decision manager...	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-02	Andrew Reynolds	Remove references to deprecated propagate as decision...	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	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-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-04-25	yoni206	Refactor bv-to-bool and bool-to-bv preprocessing passes...	blob \| commitdiff \| raw \| diff to current
2018-03-05	Mathias Preiner	Enable -Wsuggest-override by default. (#1643)	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-14	Tim King	Initializes NodeTheoryPair::timestamp in the default...	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-10-03	Andres Noetzli	Unify hash functions for pairs (#1161)	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-04-04	ajreynol	Simplify Theory::collectModelInfo interface to not...	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 ppNotifyAssertions take a const vector.	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	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2016-11-18	Tim King	Removing some throw specifiers from OutputChannel....	blob \| commitdiff \| raw \| diff to current
2016-10-28	ajreynol	Add get instantiations utilities to API.	blob \| commitdiff \| raw \| diff to current
2016-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-09-02	Tim King	Merge pull request #91 from timothy-king/no-throw	blob \| commitdiff \| raw \| diff to current
2016-09-01	ajreynol	Updates to cbqi. New strategy --cbqi-nested-qe to...	blob \| commitdiff \| raw \| diff to current
2016-09-01	Tim King	Removing the forward declaration of QuantInfo from...	blob \| commitdiff \| raw \| diff to current
2016-08-25	ajreynol	Minor cleanup preprocessing, add ppNotifyAssertions.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-08-03	barrettcw	Merge pull request #87 from 4tXJ7f/fix_oob_access	blob \| commitdiff \| raw \| diff to current
2016-07-28	Guy	Proper instrumentation of the preprocessing phase	blob \| commitdiff \| raw \| diff to current
2016-07-25	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-07-25	Guy	Proper handling for lemmas that are conjuncts:	blob \| commitdiff \| raw \| diff to current
2016-07-20	ajreynol	Infrastructure for storing and printing heap models...	blob \| commitdiff \| raw \| diff to current
2016-07-06	ajreynol	Add comment field for model, resolves hack for printing...	blob \| commitdiff \| raw \| diff to current
2016-07-05	ajreynol	Refactor last call for theories, only create one model...	blob \| commitdiff \| raw \| diff to current
2016-07-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-06-06	guykatzz	Merge pull request #85 from CVC4/master_for_proof_merge	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Revert "Merging proof branch"	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merging proof branch	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-09	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-04-09	Kshitij Bansal	cardinality operation for finite sets (based on my...	blob \| commitdiff \| raw \| diff to current
2016-04-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2016-03-23	guykatzz	Merge pull request #82 from CVC4/master_for_merge	blob \| commitdiff \| raw \| diff to current
2016-03-23	Guy	squash-merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-02-17	ajreynol	Refactor quantifiers attributes. Make quantifier elimin...	blob \| commitdiff \| raw \| diff to current
2016-02-16	ajreynol	Public interface for quantifier elimination. Minor...	blob \| commitdiff \| raw \| diff to current
2016-02-02	Tim King	Moving dump., command., model.*, and ite_removal...	blob \| commitdiff \| raw \| diff to current
2016-01-28	Tim King	Adding listeners to Options.	blob \| commitdiff \| raw \| diff to current
2016-01-27	Liana Hadarean	Merged bit-vector and uf proof branch.	blob \| commitdiff \| raw \| diff to current
2016-01-09	Tim King	Removing StatisticsRegistry's static functions current...	blob \| commitdiff \| raw \| diff to current
2016-01-06	Tim King	Add SmtGlobals Class	blob \| commitdiff \| raw \| diff to current
2015-12-27	Clark Barrett	Merged my changes from experimental branch (new array...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom