Skip to content

Commit

Permalink
Refactor pbRewrites preprocessing pass (cvc5#1767)
Browse files Browse the repository at this point in the history
This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.
  • Loading branch information
4tXJ7f authored Apr 19, 2018
1 parent 4af9af2 commit 70046d3
Show file tree
Hide file tree
Showing 8 changed files with 3,190 additions and 162 deletions.
8 changes: 4 additions & 4 deletions src/Makefile.am
Original file line number Diff line number Diff line change
Expand Up @@ -62,10 +62,12 @@ libcvc4_la_SOURCES = \
decision/decision_strategy.h \
decision/justification_heuristic.cpp \
decision/justification_heuristic.h \
preprocessing/passes/int_to_bv.cpp \
preprocessing/passes/int_to_bv.h \
preprocessing/passes/bv_gauss.cpp \
preprocessing/passes/bv_gauss.h \
preprocessing/passes/int_to_bv.cpp \
preprocessing/passes/int_to_bv.h \
preprocessing/passes/pseudo_boolean_processor.cpp \
preprocessing/passes/pseudo_boolean_processor.h \
preprocessing/preprocessing_pass.cpp \
preprocessing/preprocessing_pass.h \
preprocessing/preprocessing_pass_context.cpp \
Expand Down Expand Up @@ -246,8 +248,6 @@ libcvc4_la_SOURCES = \
theory/arith/normal_form.h\
theory/arith/partial_model.cpp \
theory/arith/partial_model.h \
theory/arith/pseudoboolean_proc.cpp \
theory/arith/pseudoboolean_proc.h \
theory/arith/simplex.cpp \
theory/arith/simplex.h \
theory/arith/simplex_update.cpp \
Expand Down
Loading

0 comments on commit 70046d3

Please sign in to comment.