diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/theory/arrays | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 37 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 |
2 files changed, 21 insertions, 18 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; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index f1b02d99e..88d83bfb9 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -128,7 +128,7 @@ class TheoryArrays : public Theory { TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals); + SmtGlobals* globals, std::string name = ""); ~TheoryArrays(); void setMasterEqualityEngine(eq::EqualityEngine* eq); |