projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3e98be4) | patch
Refactor skolem definitions notifications for the decision engine (#7310)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 6 Oct 2021 16:45:13 +0000 (11:45 -0500)
committerGitHub <noreply@github.com>
Wed, 6 Oct 2021 16:45:13 +0000 (16:45 +0000)
commit36bfe4c1802ddeb88517a399ddab9f79976ae10d
tree9d5d46600417901f7625ddf5d1faa31fb236458atree
parent3e98be42bca89a10119352d190af7584bab2f39fcommit | diff
Refactor skolem definitions notifications for the decision engine (#7310)

These changes are taken from the SAT relevancy branch. This does not change the behavior of the current code, it breaks the dependency of decision engine on the skolem definition manager and makes the latter solely managed by TheoryProxy.

This is in preparation for virtual clause deletion.
src/decision/decision_engine.h diff | blob | history
src/decision/justification_strategy.cpp diff | blob | history
src/decision/justification_strategy.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/theory_proxy.cpp diff | blob | history
src/prop/theory_proxy.h diff | blob | history