diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 37 |
1 files changed, 20 insertions, 17 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 508a4b323..cbcccd734 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -26,9 +26,10 @@ #include "smt_util/command.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" #include "theory/valuation.h" - using namespace std; namespace CVC4 { @@ -54,27 +55,28 @@ const bool d_solveWrite2 = false; TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals), - d_numRow("theory::arrays::number of Row lemmas", 0), - d_numExt("theory::arrays::number of Ext lemmas", 0), - d_numProp("theory::arrays::number of propagations", 0), - d_numExplain("theory::arrays::number of explanations", 0), - d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), - d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), - d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0), - d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0), - d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0), - d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0), - d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true), + const LogicInfo& logicInfo, SmtGlobals* globals, + std::string name) + : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals, name), + d_numRow(name + "theory::arrays::number of Row lemmas", 0), + d_numExt(name + "theory::arrays::number of Ext lemmas", 0), + d_numProp(name + "theory::arrays::number of propagations", 0), + d_numExplain(name + "theory::arrays::number of explanations", 0), + d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear", 0), + d_numSharedArrayVarSplits(name + "theory::arrays::number of shared array var splits", 0), + d_numGetModelValSplits(name + "theory::arrays::number of getModelVal splits", 0), + d_numGetModelValConflicts(name + "theory::arrays::number of getModelVal conflicts", 0), + d_numSetModelValSplits(name + "theory::arrays::number of setModelVal splits", 0), + d_numSetModelValConflicts(name + "theory::arrays::number of setModelVal conflicts", 0), + d_ppEqualityEngine(u, name + "theory::arrays::TheoryArraysPP" , true), d_ppFacts(u), // d_ppCache(u), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true), + d_mayEqualEqualityEngine(c, name + "theory::arrays::TheoryArraysMayEqual", true), d_notify(*this), - d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true), + d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true), d_conflict(c, false), d_backtracker(c), d_infoMap(c, &d_backtracker), @@ -1385,7 +1387,8 @@ void TheoryArrays::check(Effort e) { weakEquivBuildCond(r[0], r[1], conjunctions); weakEquivBuildCond(r2[0], r[1], conjunctions); lemma = mkAnd(conjunctions, true); - d_out->lemma(lemma, false, false, true); + // LSH FIXME: which kind of arrays lemma is this + d_out->lemma(lemma, RULE_INVALID, false, false, true); d_readTableContext->pop(); return; } |