summaryrefslogtreecommitdiff
path: root/src/theory/arrays/theory_arrays.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r--src/theory/arrays/theory_arrays.cpp137
1 files changed, 111 insertions, 26 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 631785437..fcde18b66 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,13 +21,14 @@
#include "expr/kind.h"
#include "options/arrays_options.h"
#include "options/smt_options.h"
+#include "proof/array_proof.h"
+#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
#include "smt/command.h"
#include "smt/logic_exception.h"
#include "smt/smt_statistics_registry.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;
@@ -78,7 +79,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true),
d_conflict(c, false),
d_backtracker(c),
- d_infoMap(c, &d_backtracker),
+ d_infoMap(c, &d_backtracker, name),
d_mergeQueue(c),
d_mergeInProgress(false),
d_RowQueue(c),
@@ -383,21 +384,27 @@ bool TheoryArrays::propagate(TNode literal)
}/* TheoryArrays::propagate(TNode) */
-void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) {
// Do the work
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
//eq::EqProof * eqp = new eq::EqProof;
- eq::EqProof * eqp = NULL;
+ // eq::EqProof * eqp = NULL;
if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
- d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp);
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof);
} else {
- d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+ d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof);
}
- if( eqp ){
- Debug("array-pf") << " Proof is : " << std::endl;
- eqp->debug_print("array-pf");
+ if(proof){
+ Debug("pf::array") << " Proof is : " << std::endl;
+ proof->debug_print("pf::array");
}
+
+ Debug("pf::array") << "Array: explain( " << literal << " ):" << std::endl << "\t";
+ for (unsigned i = 0; i < assumptions.size(); ++i) {
+ Debug("pf::array") << assumptions[i] << " ";
+ }
+ Debug("pf::array") << std::endl;
}
TNode TheoryArrays::weakEquivGetRep(TNode node) {
@@ -597,7 +604,7 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
}
}
}
- }
+ }
}
/**
@@ -787,6 +794,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
else {
d_equalityEngine.addTerm(node);
}
+
break;
}
// Invariant: preregistered terms are exactly the terms in the equality engine
@@ -807,12 +815,16 @@ void TheoryArrays::propagate(Effort e)
}
-Node TheoryArrays::explain(TNode literal)
+Node TheoryArrays::explain(TNode literal) {
+ return explain(literal, NULL);
+}
+
+Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
{
++d_numExplain;
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
std::vector<TNode> assumptions;
- explain(literal, assumptions);
+ explain(literal, assumptions, proof);
return mkAnd(assumptions);
}
@@ -1230,7 +1242,11 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
makeEqual = false;
}
}
+
+ Debug("pf::array") << "Pregistering a Skolem" << std::endl;
preRegisterTermInternal(skolem);
+ Debug("pf::array") << "Pregistering a Skolem DONE" << std::endl;
+
if (makeEqual) {
Node d = skolem.eqNode(ref);
Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
@@ -1239,6 +1255,8 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
d_skolemAssertions.push_back(d);
d_skolemIndex = d_skolemIndex + 1;
}
+
+ Debug("pf::array") << "getSkolem DONE" << std::endl;
return skolem;
}
@@ -1293,28 +1311,76 @@ void TheoryArrays::check(Effort e) {
// Apply ArrDiseq Rule if diseq is between arrays
if(fact[0][0].getType().isArray() && !d_conflict) {
+ if (d_conflict) { Debug("pf::array") << "Entering the skolemization branch" << std::endl; }
+
NodeManager* nm = NodeManager::currentNM();
TypeNode indexType = fact[0][0].getType()[0];
- TNode k = getSkolem(fact,"array_ext_index", indexType, "an extensional lemma index variable from the theory of arrays", false);
+
+ TNode k;
+ // k is the skolem for this disequality.
+ if (!d_proofsEnabled) {
+ Debug("pf::array") << "Check: kind::NOT: array theory making a skolem" << std::endl;
+
+ // If not in replay mode, generate a fresh skolem variable
+ k = getSkolem(fact,
+ "array_ext_index",
+ indexType,
+ "an extensional lemma index variable from the theory of arrays",
+ false);
+
+ // Register this skolem for the proof replay phase
+ PROOF(ProofManager::getSkolemizationManager()->registerSkolem(fact, k));
+ } else {
+ if (!ProofManager::getSkolemizationManager()->hasSkolem(fact)) {
+ // In the solution pass we didn't need this skolem. Therefore, we don't need it
+ // in this reply pass, either.
+ break;
+ }
+
+ // Reuse the same skolem as in the solution pass
+ k = ProofManager::getSkolemizationManager()->getSkolem(fact);
+ Debug("pf::array") << "Skolem = " << k << std::endl;
+ }
Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
Node eq = ak.eqNode(bk);
Node lemma = fact[0].orNode(eq.notNode());
+
+ // In solve mode we don't care if ak and bk are registered. If they aren't, they'll be registered
+ // when we output the lemma. However, in replay need the lemma to be propagated, and so we
+ // preregister manually.
+ if (d_proofsEnabled) {
+ if (!d_equalityEngine.hasTerm(ak)) { preRegisterTermInternal(ak); }
+ if (!d_equalityEngine.hasTerm(bk)) { preRegisterTermInternal(bk); }
+ }
+
if (options::arraysPropagate() > 0 && d_equalityEngine.hasTerm(ak) && d_equalityEngine.hasTerm(bk)) {
// Propagate witness disequality - might produce a conflict
d_permRef.push_back(lemma);
- d_equalityEngine.assertEquality(eq, false, lemma, eq::MERGED_ARRAYS_EXT);
+ Debug("pf::array") << "Asserting to the equality engine:" << std::endl
+ << "\teq = " << eq << std::endl
+ << "\treason = " << fact << std::endl;
+
+ d_equalityEngine.assertEquality(eq, false, fact, eq::MERGED_ARRAYS_EXT);
++d_numProp;
}
- Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
- d_out->lemma(lemma);
- ++d_numExt;
+
+ if (!d_proofsEnabled) {
+ // If this is the solution pass, generate the lemma. Otherwise, don't generate it -
+ // as this is the lemma that we're reproving...
+ Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
+ d_out->lemma(lemma);
+ ++d_numExt;
+ }
+ } else {
+ Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl;
+ d_modelConstraints.push_back(fact);
}
}
break;
- default:
- Unreachable();
+ default:
+ Unreachable();
}
}
@@ -1389,8 +1455,10 @@ void TheoryArrays::check(Effort e) {
weakEquivBuildCond(r2[0], r[1], conjunctions);
lemma = mkAnd(conjunctions, true);
// LSH FIXME: which kind of arrays lemma is this
+ Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n";
d_out->lemma(lemma, RULE_INVALID, false, false, true);
d_readTableContext->pop();
+ Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
return;
}
}
@@ -1401,7 +1469,7 @@ void TheoryArrays::check(Effort e) {
if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) {
// generate the lemmas on the worklist
- Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+ Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
while (d_RowQueue.size() > 0 && !d_conflict) {
if (dischargeLemmas()) {
break;
@@ -1865,6 +1933,9 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
void TheoryArrays::propagate(RowLemmaType lem)
{
+ Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
+ << options::arraysPropagate() << std::endl;
+
TNode a = lem.first;
TNode b = lem.second;
TNode i = lem.third;
@@ -1919,6 +1990,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
void TheoryArrays::queueRowLemma(RowLemmaType lem)
{
+ Debug("pf::array") << "Array solver: queue row lemma called" << std::endl;
+
if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
return;
}
@@ -1958,14 +2031,20 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
// Prefer equality between indexes so as not to introduce new read terms
if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
- Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));
+ Node i_eq_j;
+ if (!d_proofsEnabled) {
+ i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
+ } else {
+ i_eq_j = i.eqNode(j);
+ }
+
getOutputChannel().requirePhase(i_eq_j, true);
d_decisionRequests.push(i_eq_j);
}
// TODO: maybe add triggers here
- if (options::arraysEagerLemmas() || bothExist) {
+ if ((options::arraysEagerLemmas() || bothExist) && !d_proofsEnabled) {
// Make sure that any terms introduced by rewriting are appropriately stored in the equality database
Node aj2 = Rewriter::rewrite(aj);
@@ -2137,14 +2216,20 @@ bool TheoryArrays::dischargeLemmas()
}
void TheoryArrays::conflict(TNode a, TNode b) {
+ Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
+ eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
if (a.getKind() == kind::CONST_BOOLEAN) {
- d_conflictNode = explain(a.iffNode(b));
+ d_conflictNode = explain(a.iffNode(b), proof);
} else {
- d_conflictNode = explain(a.eqNode(b));
+ d_conflictNode = explain(a.eqNode(b), proof);
}
+
if (!d_inCheckModel) {
- d_out->conflict(d_conflictNode);
+ if (proof) { proof->debug_print("pf::array"); }
+ ProofArray* proof_array = d_proofsEnabled ? new ProofArray( proof ) : NULL;
+ d_out->conflict(d_conflictNode, proof_array);
}
+
d_conflict = true;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback