cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2021-04-01	Rename namespace CVC5 to cvc5. (#6258)	Aina Niemetz

2021-03-31	Rename namespace CVC4 to CVC5. (#6249)	Aina Niemetz

2021-03-09	Some more cleanup of includes (#6083)	Gereon Kremer
	This PR does some more cleanup of the includes.
2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2021-01-28	Simplify lemma interface (#5819)	Andrew Reynolds
	This makes it so that TheoryEngine::lemma returns void not LemmaStatus. Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions. It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.
2021-01-28	Use standard equality engine information in quantifiers state (#5824)	Andrew Reynolds
	This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState. This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
2020-10-02	(proof-new) Make shared solver proof producing (#5169)	Andrew Reynolds
	This makes the shared terms database use a proof equality engine as a layer on top of its equality engine, analogous to how this done in theories.
2020-09-26	Connect the shared solver to theory engine (#5103)	Andrew Reynolds
	This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database. It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus. This PR has no intended behavior changes. FYI @barrettcw
2020-09-22	Update copyright header script to support CMake and Python files (#5067)	Mathias Preiner
	This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-08-28	(proof-new) Make CombinationEngine proof producing (#4955)	Andrew Reynolds
	Makes combination engine proof producing (for Boolean splits). Followup PRs will start to add proof production in TheoryEngine.
2020-08-25	Add the combination engine (#4939)	Andrew Reynolds
	This adds the combination engine, which is the module of TheoryEngine which implements the combineTheories method and owns the various components of theory combination, which includes equality engine manager, model manager, and the "shared solver" (to come later). It will have two variants, CombinationCareGraph and CombinationModelBased, the former is added with this PR. FYI @barrettcw The next PR will connect this module to TheoryEngine and remove a few existing methods from TheoryEngine, as they are implemented in the modules of this class.