diff options
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 |