summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-09-27 10:57:58 -0700
committerGitHub <noreply@github.com>2019-09-27 10:57:58 -0700
commit6c878c1cf54620b10bac95e5765d0d03bf718f5c (patch)
treee173b16c2d36abd2953a29e8659cb9bafec1c068 /src/theory/strings
parent64e8ad696a1accdf489a3073cc480f591be04c39 (diff)
Make substitution index context-independent (#2474)
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).
Diffstat (limited to 'src/theory/strings')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback