Make substitution index context-independent (#2474)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 27 Sep 2019 17:57:58 +0000 (10:57 -0700)
committerGitHub <noreply@github.com>
Fri, 27 Sep 2019 17:57:58 +0000 (10:57 -0700)
commit6c878c1cf54620b10bac95e5765d0d03bf718f5c
treee173b16c2d36abd2953a29e8659cb9bafec1c068
parent64e8ad696a1accdf489a3073cc480f591be04c39
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).
src/preprocessing/assertion_pipeline.cpp
src/preprocessing/assertion_pipeline.h
src/preprocessing/passes/apply_substs.cpp
src/preprocessing/passes/non_clausal_simp.cpp
src/preprocessing/preprocessing_pass_context.cpp
src/preprocessing/preprocessing_pass_context.h
src/smt/smt_engine.cpp