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

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

2021-10-04	Andrew Reynolds	Move isFiniteType from theory engine to Env (#7287)	blob \| commitdiff \| raw
2021-09-30	Andrew Reynolds	Make theory engine modules use Env (#7277)	blob \| commitdiff \| raw \| diff to current
2021-09-29	Abdalrhman Mohamed	Remove support for extended `(check-sat <term>)` comman...	blob \| commitdiff \| raw \| diff to current
2021-09-23	Abdalrhman Mohamed	Use `\|` to print quoted strings in `set-info` command...	blob \| commitdiff \| raw \| diff to current
2021-09-13	Andrew Reynolds	Connect difficulty manager to TheoryEngine (#7161)	blob \| commitdiff \| raw \| diff to current
2021-09-11	Gereon Kremer	Use StatisticsRegistry from Env (#7166)	blob \| commitdiff \| raw \| diff to current
2021-09-10	Andres Noetzli	Use C++17 attributes (#7154)	blob \| commitdiff \| raw \| diff to current
2021-09-03	Aina Niemetz	EnvObj: Add options(), context(), userContext(). (...	blob \| commitdiff \| raw \| diff to current
2021-09-03	Aina Niemetz	theory: Have more classes in theory with reference...	blob \| commitdiff \| raw \| diff to current
2021-09-02	Andrew Reynolds	Remove more instances of ufHo (#7087)	blob \| commitdiff \| raw \| diff to current
2021-09-01	Aina Niemetz	rewriter: Make registerTheoryRewriter non-static. ...	blob \| commitdiff \| raw \| diff to current
2021-08-20	Andrew Reynolds	Simplify how user-provided quantifier attributes are...	blob \| commitdiff \| raw \| diff to current
2021-08-20	Andrew Reynolds	Eliminate eager model building (#7038)	blob \| commitdiff \| raw \| diff to current
2021-08-19	Andrew Reynolds	Catch cases where recursive functions reference functio...	blob \| commitdiff \| raw \| diff to current
2021-08-16	Gereon Kremer	Make Theory class use Env (#7011)	blob \| commitdiff \| raw \| diff to current
2021-08-04	Andrew Reynolds	Remove dependencies on smt engine in smt solver (#6965)	blob \| commitdiff \| raw \| diff to current
2021-08-03	Andrew Reynolds	Refactor shared solver to use theory builtin inference...	blob \| commitdiff \| raw \| diff to current
2021-07-29	Andrew Reynolds	Integrate central equality engine approach into theory...	blob \| commitdiff \| raw \| diff to current
2021-07-29	Andrew Reynolds	Minor updates to shared terms database for central...	blob \| commitdiff \| raw \| diff to current
2021-07-22	Andrew Reynolds	Miscellaneous changes in preparation for central equali...	blob \| commitdiff \| raw \| diff to current
2021-07-05	Andrew Reynolds	Make buffered inference manager more robust to backtrac...	blob \| commitdiff \| raw \| diff to current
2021-05-27	Andrew Reynolds	Update proof namespaces (#6614)	blob \| commitdiff \| raw \| diff to current
2021-05-24	Andrew Reynolds	Move proof utilities to src/proof/ (#6611)	blob \| commitdiff \| raw \| diff to current
2021-05-13	Mathias Preiner	Add std::hash overloads for Node, TNode and TypeNode...	blob \| commitdiff \| raw \| diff to current
2021-05-10	Andrew Reynolds	Unify top-level substitutions and model substitutions...	blob \| commitdiff \| raw \| diff to current
2021-05-04	Andrew Reynolds	Move env into smt solver, theory engine, prop engine...	blob \| commitdiff \| raw \| diff to current
2021-04-14	Gereon Kremer	Refactor / reimplement statistics (#6162)	blob \| commitdiff \| raw \| diff to current
2021-04-14	Haniel Barbosa	[unsat-cores] Improving new unsat cores (#6356)	blob \| commitdiff \| raw \| diff to current
2021-04-14	Andrew Reynolds	Add interface for getting relevant assertions (#5131)	blob \| commitdiff \| raw \| diff to current
2021-04-12	Andrew Reynolds	Fix computation of whether a type is finite (#6312)	blob \| commitdiff \| raw \| diff to current
2021-04-12	Gereon Kremer	Refactor resource manager (#6322)	blob \| commitdiff \| raw \| diff to current
2021-04-12	Aina Niemetz	Refactor and update copyright headers. (#6316)	blob \| commitdiff \| raw \| diff to current
2021-04-10	Aina Niemetz	Rename CVC4_ macros to CVC5_. (#6327)	blob \| commitdiff \| raw \| diff to current
2021-04-08	Andrew Reynolds	Add identifiers for sources of incompleteness (#6311)	blob \| commitdiff \| raw \| diff to current
2021-04-06	Andres Noetzli	Remove template argument from `NodeBuilder` (#6290)	blob \| commitdiff \| raw \| diff to current
2021-04-05	Haniel Barbosa	[proof-new] Registering proof checkers uniformly from...	blob \| commitdiff \| raw \| diff to current
2021-04-01	Aina Niemetz	Rename namespace CVC5 to cvc5. (#6258)	blob \| commitdiff \| raw \| diff to current
2021-03-31	Aina Niemetz	Rename namespace CVC4 to CVC5. (#6249)	blob \| commitdiff \| raw \| diff to current
2021-03-29	Andrew Reynolds	Move decision manager into theory inference manager...	blob \| commitdiff \| raw \| diff to current
2021-03-19	Andrew Reynolds	Refactor initialization of quantifiers model and builde...	blob \| commitdiff \| raw \| diff to current
2021-03-10	Andrew Reynolds	(proof-new) Update ppRewrite to use skolem lemmas ...	blob \| commitdiff \| raw \| diff to current
2021-03-09	Gereon Kremer	Some more cleanup of includes (#6083)	blob \| commitdiff \| raw \| diff to current
2021-03-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	blob \| commitdiff \| raw \| diff to current
2021-03-03	Gereon Kremer	More cleanup of includes to reduce compilation times...	blob \| commitdiff \| raw \| diff to current
2021-02-24	Andrew Reynolds	Add interface to TheoryState for sort inference and...	blob \| commitdiff \| raw \| diff to current
2021-02-10	Andrew Reynolds	Refactor term registration visitors (#5875)	blob \| commitdiff \| raw \| diff to current
2021-02-06	Andrew Reynolds	Do not combine theories if theory engine needs check...	blob \| commitdiff \| raw \| diff to current
2021-02-05	Andrew Reynolds	Miscellaneous cleaning in theory engine (#5854)	blob \| commitdiff \| raw \| diff to current
2021-02-02	Andrew Reynolds	(proof-new) Miscellaneous fixes and regressions (#5841)	blob \| commitdiff \| raw \| diff to current
2021-02-02	Andrew Reynolds	Cleanup some includes (#5847)	blob \| commitdiff \| raw \| diff to current
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
next

RSS Atom