projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1e6a665) | patch
Add argument to distinguish lemmas and input assertions (#7326)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 8 Oct 2021 20:23:15 +0000 (15:23 -0500)
committerGitHub <noreply@github.com>
Fri, 8 Oct 2021 20:23:15 +0000 (20:23 +0000)
commit7fe20b85b18ae99461c4de339c9109fe68ca48f2
tree7780e71fad2603ab4da69bcaed090a437f9ae2b9tree
parent1e6a6658573e0d11e7bac8fd51066f401c3aa25ccommit | diff
Add argument to distinguish lemmas and input assertions (#7326)

Work towards virtual clause deletion, where lemmas will be SAT-context dependent.

This adds an argument to the decision engine so it can distinguish lemmas from input assertions.
src/decision/decision_engine.cpp diff | blob | history
src/decision/decision_engine.h diff | blob | history
src/decision/decision_engine_old.cpp diff | blob | history
src/decision/decision_engine_old.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