projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 42f5154) | patch
Add option to track and notify from CNF stream (#5708)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 23 Dec 2020 22:17:48 +0000 (16:17 -0600)
committerGitHub <noreply@github.com>
Wed, 23 Dec 2020 22:17:48 +0000 (16:17 -0600)
commita04226ef3519c4fdce7bd6c3ff92f18bf6bee83c
tree40ba3c986de4107e322adb19a5e3a247dcec0972tree
parent42f51547174e2644a244464c170115ff3b2bc22fcommit | diff
Add option to track and notify from CNF stream (#5708)

This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals).

This will be required for SAT relevancy.

No behavior changes in this PR.
src/prop/cnf_stream.cpp diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/prop/minisat/core/Solver.cc diff | blob | history
src/prop/minisat/core/Solver.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/theory/bv/bitblast/eager_bitblaster.cpp diff | blob | history
src/theory/bv/bitblast/lazy_bitblaster.cpp diff | blob | history
src/theory/bv/bv_eager_solver.cpp diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history