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

Age	Commit message (Collapse)	Author
2019-09-27	Make substitution index context-independent (#2474)	Andres Noetzli
	When we do solving in incremental mode, we store substitutions at a special index in our list of assertions. Previously, we used a context-dependent variable for that. However, this is not needed since the list of assertions just consists of the assertions currently being processed, which are independent of the assertions seen so far. This commit changes the index to be an ordinary integer and moves it to the AssertionPipeline. Additionally, it abstracts access to the index in preparation for splitting AssertionPipeline into three vectors (see issue #2473).
2019-03-26	Update copyright headers.	Aina Niemetz

2018-10-31	Record assumption info in AssertionPipeline (#2678)	Andres Noetzli

2018-09-14	Refactor how assertions are added to decision engine (#2396)	Andres Noetzli
	Before refactoring the preprocessing passes, we were using three arguments to add assertions to the decision engine. Now all that information lives in the AssertionPipeline. This commit moves the AssertionPipeline to its own file and changes the `addAssertions()` methods related to the decision engine to take an AssertionPipeline as an arguement instead of three separate ones. Additionally, the TheoryEngine now uses an AssertionPipeline for lemmas.