Refactor how assertions are added to decision engine (#2396)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 15 Sep 2018 05:15:37 +0000 (22:15 -0700)
committerGitHub <noreply@github.com>
Sat, 15 Sep 2018 05:15:37 +0000 (22:15 -0700)
commit2060f439c873c8b1928cbd5f54967571176f2aba
tree45fab904b632b6174ee66807081465693a5da83f
parentc2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010
Refactor how assertions are added to decision engine (#2396)

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.
23 files changed:
src/Makefile.am
src/api/cvc4cpp.cpp
src/decision/decision_engine.cpp
src/decision/decision_engine.h
src/decision/decision_strategy.h
src/decision/justification_heuristic.cpp
src/decision/justification_heuristic.h
src/include/cvc4_private_library.h
src/preprocessing/assertion_pipeline.cpp [new file with mode: 0644]
src/preprocessing/assertion_pipeline.h [new file with mode: 0644]
src/preprocessing/passes/apply_substs.cpp
src/preprocessing/passes/miplib_trick.cpp
src/preprocessing/passes/non_clausal_simp.cpp
src/preprocessing/preprocessing_pass.cpp
src/preprocessing/preprocessing_pass.h
src/preprocessing/preprocessing_pass_context.cpp
src/preprocessing/preprocessing_pass_context.h
src/smt/smt_engine.cpp
src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/sygus/sygus_repair_const.cpp
src/theory/theory_engine.cpp
test/unit/preprocessing/pass_bv_gauss_white.h