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

Age	Commit message (Collapse)	Author
2020-04-28	Register lower bound for str.to_int (#4408)	Andres Noetzli
	This commit changes the term registration for str.to_int terms. Before, we were not sending out any lemmas when registering str.to_int terms. Now, we send a simple lemma that asserts that the value is greater or equal to negative one.
2020-04-15	Split TermRegistry object from TheoryStrings (#4312)	Andrew Reynolds
	This consolidates functionalities from TheoryStrings and InferenceManager related to registering terms, including sending "preregistration lemmas" for them. The main purpose of this PR is to detangle this module from InferenceManager so that these two modules have exactly one call to OutputChannel::lemma each. For the purposes of the theory solvers, TermRegistry contains the official SkolemCache of TheoryStrings, and can be seen as subsuming the previous interface for this class. This PR is needed for further progress on strings proofs, marking as major since this will be a blocker shortly for this project. A few things were cleaned in this PR. One function changed name InferenceManager::registerTerm --> TermRegistry::getRegisterTermLemma. No major behavior changes.