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

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

2021-10-04	Andrew Reynolds	Move isFiniteType from theory engine to Env (#7287)	blob \| commitdiff \| raw
2021-10-01	Aina Niemetz	Rename SmtEngine to SolverEngine. (#7282)	blob \| commitdiff \| raw \| diff to current
2021-09-30	Andrew Reynolds	Make theory engine modules use Env (#7277)	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-03	Aina Niemetz	theory: Have more classes in theory with reference...	blob \| commitdiff \| raw \| diff to current
2021-09-01	Aina Niemetz	Clean up TheoryEngine header according to code style...	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-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-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-04	Andrew Reynolds	Move env into smt solver, theory engine, prop engine...	blob \| commitdiff \| raw \| diff to current
2021-04-15	Aina Niemetz	Rename occurrences of CVC4 to CVC5. (#6351)	blob \| commitdiff \| raw \| diff to current
2021-04-14	Gereon Kremer	Refactor / reimplement statistics (#6162)	blob \| commitdiff \| raw \| diff to current
2021-04-14	Aina Niemetz	Rename public and private headers in src/include. ...	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-09	Aina Niemetz	Rename CVC4__ header guards to CVC5__. (#6326)	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-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	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-05	Andrew Reynolds	Miscellaneous cleaning in theory engine (#5854)	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-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-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-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	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-18	Andrew Reynolds	Add the shared solver (#4982)	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-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-01	Haniel Barbosa	Removes old proof code (#4964)	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-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
next

RSS Atom