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

author	Amalee Wilson <amalee@cs.stanford.edu>
	Thu, 14 Apr 2022 15:26:49 +0000 (08:26 -0700)
committer	GitHub <noreply@github.com>
	Thu, 14 Apr 2022 15:26:49 +0000 (15:26 +0000)
commit	74a46ddc8efe114b4823865d08c370ca518f1cbd
tree	1747943f36675d4806f45003c0edae3e41767b99	tree
parent	4b57f0aaa295d0203157ac81ad38360f5210f915	commit \| diff

Revised partitioning (#8143)

This adds the "revised" partitioning algorithm to the splitter and adds support for collecting literals from the sat solver. There is only one partitioning strategy in this PR, but the others will be added in subsequent PRs.

13 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/options/parallel_options.toml	[new file with mode: 0644]	blob
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/minisat.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/theory/partition_generator.cpp	[new file with mode: 0644]	blob
src/theory/partition_generator.h	[new file with mode: 0644]	blob
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history

RSS Atom