diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-23 16:17:48 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-23 16:17:48 -0600 |
| commit | a04226ef3519c4fdce7bd6c3ff92f18bf6bee83c (patch) | |
| tree | 40ba3c986de4107e322adb19a5e3a247dcec0972 /src/prop/minisat | |
| parent | 42f51547174e2644a244464c170115ff3b2bc22f (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.
Diffstat (limited to 'src/prop/minisat')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 4 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.h | 7 |
2 files changed, 8 insertions, 3 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index ca29e604f..12246be41 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -274,7 +274,8 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo polarity .push(sign); decision .push(); trail .capacity(v+1); - theory .push(isTheoryAtom); + // push whether it corresponds to a theory atom + theory.push(isTheoryAtom); setDecisionVar(v, dvar); @@ -306,7 +307,6 @@ void Solver::resizeVars(int newSize) { polarity.shrink(shrinkSize); decision.shrink(shrinkSize); theory.shrink(shrinkSize); - } if (Debug.isOn("minisat::pop")) { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 00d68cf80..8fa489f65 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -390,7 +390,12 @@ protected: ClauseAllocator ca; // CVC4 Stuff - vec<bool> theory; // Is the variable representing a theory atom + /** + * A vector determining whether each variable represents a theory atom. + * More generally, this value is true for any literal that the theory proxy + * should be notified about when asserted. + */ + vec<bool> theory; enum TheoryCheckType { // Quick check, but don't perform theory reasoning |