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.cpp265
1 files changed, 108 insertions, 157 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 603dc9639..408f4c682 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -43,7 +43,6 @@ namespace arrays {
// Use static configuration of options for now
const bool d_ccStore = false;
-const bool d_useArrTable = false;
//const bool d_eagerLemmas = false;
const bool d_preprocess = true;
const bool d_solveWrite = true;
@@ -85,7 +84,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
d_isPreRegistered(c),
d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
d_notify(*this),
- d_conflict(c, false),
d_backtracker(c),
d_infoMap(c, &d_backtracker, name),
d_mergeQueue(c),
@@ -175,10 +173,6 @@ void TheoryArrays::finishInit()
{
d_equalityEngine->addFunctionKind(kind::STORE);
}
- if (d_useArrTable)
- {
- d_equalityEngine->addFunctionKind(kind::ARR_TABLE_FUN);
- }
}
/////////////////////////////////////////////////////////////////////////////
@@ -401,7 +395,8 @@ bool TheoryArrays::propagateLit(TNode literal)
<< std::endl;
// If already in conflict, no more propagation
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
Debug("arrays") << spaces(getSatContext()->getLevel())
<< "TheoryArrays::propagateLit(" << literal
<< "): already in conflict" << std::endl;
@@ -414,7 +409,7 @@ bool TheoryArrays::propagateLit(TNode literal)
}
bool ok = d_out->propagate(literal);
if (!ok) {
- d_conflict = true;
+ d_state.notifyInConflict();
}
return ok;
}/* TheoryArrays::propagate(TNode) */
@@ -644,7 +639,8 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
*/
void TheoryArrays::preRegisterTermInternal(TNode node)
{
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
return;
}
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
@@ -788,7 +784,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
// The may equal needs the node
d_mayEqualEqualityEngine.addTerm(node);
d_equalityEngine->addTerm(node);
- Assert(d_equalityEngine->getSize(node) == 1);
}
else {
d_equalityEngine->addTerm(node);
@@ -802,7 +797,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
// !d_equalityEngine->consistent());
}
-
void TheoryArrays::preRegisterTerm(TNode node)
{
preRegisterTermInternal(node);
@@ -863,23 +857,6 @@ void TheoryArrays::notifySharedTerm(TNode t)
}
}
-
-EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
- Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
- if (d_equalityEngine->areEqual(a, b))
- {
- // The terms are implied to be equal
- return EQUALITY_TRUE;
- }
- else if (d_equalityEngine->areDisequal(a, b, false))
- {
- // The terms are implied to be dis-equal
- return EQUALITY_FALSE;
- }
- return EQUALITY_UNKNOWN;//FALSE_IN_MODEL;
-}
-
-
void TheoryArrays::checkPair(TNode r1, TNode r2)
{
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl;
@@ -1061,6 +1038,7 @@ bool TheoryArrays::collectModelValues(TheoryModel* m,
NodeManager* nm = NodeManager::currentNM();
// Compute arrays that we need to produce representatives for
std::vector<Node> arrays;
+
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
for (; !eqcs_i.isFinished(); ++eqcs_i) {
Node eqc = (*eqcs_i);
@@ -1113,12 +1091,14 @@ bool TheoryArrays::collectModelValues(TheoryModel* m,
//}
// Loop through all array equivalence classes that need a representative computed
- for (size_t i=0; i<arrays.size(); ++i) {
- TNode n = arrays[i];
- TNode nrep = d_equalityEngine->getRepresentative(n);
+ for (size_t i = 0; i < arrays.size(); ++i)
+ {
+ TNode n = arrays[i];
+ TNode nrep = d_equalityEngine->getRepresentative(n);
- //if (fullModel) {
- // Compute default value for this array - there is one default value for every mayEqual equivalence class
+ // if (fullModel) {
+ // Compute default value for this array - there is one default value for
+ // every mayEqual equivalence class
TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
it = d_defValues.find(mayRep);
// If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
@@ -1220,7 +1200,7 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
Node d = skolem.eqNode(ref);
Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
d_equalityEngine->assertEquality(d, true, d_true);
- Assert(!d_conflict);
+ Assert(!d_state.isInConflict());
d_skolemAssertions.push_back(d);
d_skolemIndex = d_skolemIndex + 1;
}
@@ -1229,115 +1209,11 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
return skolem;
}
-
-void TheoryArrays::check(Effort e) {
- if (done() && !fullEffort(e)) {
- return;
- }
-
- getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
-
- TimerStat::CodeTimer checkTimer(d_checkTime);
-
- while (!done() && !d_conflict)
+void TheoryArrays::postCheck(Effort level)
+{
+ if ((options::arraysEagerLemmas() || fullEffort(level))
+ && !d_state.isInConflict() && options::arraysWeakEquivalence())
{
- // Get all the assertions
- Assertion assertion = get();
- TNode fact = assertion.d_assertion;
-
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
-
- bool polarity = fact.getKind() != kind::NOT;
- TNode atom = polarity ? fact : fact[0];
-
- if (!assertion.d_isPreregistered)
- {
- if (atom.getKind() == kind::EQUAL) {
- if (!d_equalityEngine->hasTerm(atom[0]))
- {
- Assert(atom[0].isConst());
- d_equalityEngine->addTerm(atom[0]);
- }
- if (!d_equalityEngine->hasTerm(atom[1]))
- {
- Assert(atom[1].isConst());
- d_equalityEngine->addTerm(atom[1]);
- }
- }
- }
-
- // Do the work
- switch (fact.getKind()) {
- case kind::EQUAL:
- d_equalityEngine->assertEquality(fact, true, fact);
- break;
- case kind::SELECT:
- d_equalityEngine->assertPredicate(fact, true, fact);
- break;
- case kind::NOT:
- if (fact[0].getKind() == kind::SELECT) {
- d_equalityEngine->assertPredicate(fact[0], false, fact);
- }
- else if (!d_equalityEngine->areDisequal(fact[0][0], fact[0][1], false))
- {
- // Assert the dis-equality
- d_equalityEngine->assertEquality(fact[0], false, fact);
-
- // 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;
- // k is the skolem for this disequality.
- Debug("pf::array")
- << "Check: kind::NOT: array theory making a skolem"
- << std::endl;
- k = getSkolem(
- fact,
- "array_ext_index",
- indexType,
- "an extensional lemma index variable from the theory of arrays",
- false);
- 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());
-
- if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
- && d_equalityEngine->hasTerm(bk))
- {
- // Propagate witness disequality - might produce a conflict
- d_permRef.push_back(lemma);
- Debug("pf::array") << "Asserting to the equality engine:" << std::endl
- << "\teq = " << eq << std::endl
- << "\treason = " << fact << std::endl;
-
- d_equalityEngine->assertEquality(
- eq, false, fact, theory::eq::MERGED_THROUGH_EXT);
- ++d_numProp;
- }
-
- // 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();
- break;
- }
- }
-
- if ((options::arraysEagerLemmas() || fullEffort(e)) && !d_conflict && options::arraysWeakEquivalence()) {
// Replay all array merges to update weak equivalence data structures
context::CDList<Node>::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end();
TNode a, b, eq;
@@ -1424,10 +1300,13 @@ void TheoryArrays::check(Effort e) {
d_readTableContext->pop();
}
- if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) {
+ if (!options::arraysEagerLemmas() && fullEffort(level)
+ && !d_state.isInConflict() && !options::arraysWeakEquivalence())
+ {
// generate the lemmas on the worklist
Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
- while (d_RowQueue.size() > 0 && !d_conflict) {
+ while (d_RowQueue.size() > 0 && !d_state.isInConflict())
+ {
if (dischargeLemmas()) {
break;
}
@@ -1437,6 +1316,84 @@ void TheoryArrays::check(Effort e) {
Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
}
+bool TheoryArrays::preNotifyFact(
+ TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+ if (!isPrereg)
+ {
+ if (atom.getKind() == kind::EQUAL)
+ {
+ if (!d_equalityEngine->hasTerm(atom[0]))
+ {
+ Assert(atom[0].isConst());
+ d_equalityEngine->addTerm(atom[0]);
+ }
+ if (!d_equalityEngine->hasTerm(atom[1]))
+ {
+ Assert(atom[1].isConst());
+ d_equalityEngine->addTerm(atom[1]);
+ }
+ }
+ }
+ return false;
+}
+
+void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
+{
+ // if a disequality
+ if (atom.getKind() == kind::EQUAL && !pol)
+ {
+ // Apply ArrDiseq Rule if diseq is between arrays
+ if (fact[0][0].getType().isArray() && !d_state.isInConflict())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ TypeNode indexType = fact[0][0].getType()[0];
+
+ TNode k;
+ // k is the skolem for this disequality.
+ 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);
+
+ 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());
+
+ if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
+ && d_equalityEngine->hasTerm(bk))
+ {
+ // Propagate witness disequality - might produce a conflict
+ d_permRef.push_back(lemma);
+ Debug("pf::array") << "Asserting to the equality engine:" << std::endl
+ << "\teq = " << eq << std::endl
+ << "\treason = " << fact << std::endl;
+
+ d_equalityEngine->assertEquality(eq, false, fact);
+ ++d_numProp;
+ }
+
+ // 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);
+ }
+ }
+}
Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned startIndex)
{
@@ -1641,7 +1598,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
}
// If no more to do, break
- if (d_conflict || d_mergeQueue.empty()) {
+ if (d_state.isInConflict() || d_mergeQueue.empty())
+ {
break;
}
@@ -1865,7 +1823,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
{
Debug("pf::array") << "Array solver: queue row lemma called" << std::endl;
- if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
+ if (d_state.isInConflict() || d_RowAlreadyAdded.contains(lem))
+ {
return;
}
TNode a, b, i, j;
@@ -1892,15 +1851,6 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
propagate(lem);
}
- // If equivalent lemma already exists, don't enqueue this one
- if (d_useArrTable) {
- Node tableEntry = NodeManager::currentNM()->mkNode(kind::ARR_TABLE_FUN, a, b, i, j);
- if (d_equalityEngine->getSize(tableEntry) != 1)
- {
- return;
- }
- }
-
// Prefer equality between indexes so as not to introduce new read terms
if (options::arraysEagerIndexSplitting() && !bothExist
&& !d_equalityEngine->areDisequal(i, j, false))
@@ -2025,7 +1975,8 @@ bool TheoryArrays::dischargeLemmas()
int prop = options::arraysPropagate();
if (prop > 0) {
propagate(l);
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
return true;
}
}
@@ -2103,7 +2054,7 @@ void TheoryArrays::conflict(TNode a, TNode b) {
d_out->conflict(d_conflictNode);
}
- d_conflict = true;
+ d_state.notifyInConflict();
}
TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy(
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback