projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5c09e3f) | patch
Reorganizing use of skolem definition manager in prop engine (#6415)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 22 Apr 2021 19:12:23 +0000 (14:12 -0500)
committerGitHub <noreply@github.com>
Thu, 22 Apr 2021 19:12:23 +0000 (19:12 +0000)
commit7295b8da3f77d0121ab0215a7f309dab90b02854
tree3ea57fb04d3a279460b5df4634c0bd13c40e2652tree
parent5c09e3f6e14f92b3c66b260837bd460973b4cc57commit | diff
 Reorganizing use of skolem definition manager in prop engine (#6415)

Towards setting up the proper callbacks into the new justification heuristic.

Moves ownership of skolem definition manager from TheoryProxy to PropEngine.
src/decision/decision_engine.cpp diff | blob | history
src/decision/decision_engine.h diff | blob | history
src/decision/decision_strategy.h diff | blob | history
src/decision/justification_heuristic.cpp diff | blob | history
src/decision/justification_heuristic.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/prop/skolem_def_manager.cpp diff | blob | history
src/prop/skolem_def_manager.h diff | blob | history
src/prop/theory_proxy.cpp diff | blob | history
src/prop/theory_proxy.h diff | blob | history