git.libre-soc.org Git - cvc5.git/commit

author	Andres Noetzli <andres.noetzli@gmail.com>
	Thu, 19 Apr 2018 18:47:38 +0000 (11:47 -0700)
committer	GitHub <noreply@github.com>
	Thu, 19 Apr 2018 18:47:38 +0000 (11:47 -0700)
commit	70046d35f2aff41867cbb6490e5bf6d026dc55a1
tree	a6903beb73a028ea159b07bb5c773386c1e5c5f5	tree
parent	4af9af22f728ebb12afe48c587cfe665fc8cb123	commit \| diff

Refactor pbRewrites preprocessing pass (#1767)

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.

src/Makefile.am		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.cpp	[new file with mode: 0644]	blob
src/preprocessing/passes/pseudo_boolean_processor.h	[new file with mode: 0644]	blob
src/preprocessing/preprocessing_pass_context.h		diff \| blob \| history
src/preprocessing/preprocessing_pass_registry.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/pseudoboolean_proc.cpp	[deleted file]	blob \| history
src/theory/arith/pseudoboolean_proc.h	[deleted file]	blob \| history
test/regress/Makefile.tests		diff \| blob \| history
test/regress/regress1/arith/pbrewrites-test.smt2	[new file with mode: 0644]	blob

RSS Atom