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-04-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
Fixes 2887. | |||
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. |