+++ /dev/null
-/********************* */
-/*! \file static_fact_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Clark Barrett, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Path-compressing, backtrackable union-find using an undo
- ** stack. Refactored from the UF union-find.
- **
- ** Path-compressing, backtrackable union-find using an undo stack
- ** rather than storing items in a CDMap<>.
- **/
-
-#include <iostream>
-
-#include "base/check.h"
-#include "expr/node.h"
-#include "theory/arrays/static_fact_manager.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-bool StaticFactManager::areEq(TNode a, TNode b) {
- return (find(a) == find(b));
-}
-
-bool StaticFactManager::areDiseq(TNode a, TNode b) {
- Node af = find(a);
- Node bf = find(b);
- Node left, right;
- unsigned i;
- for (i = 0; i < d_diseq.size(); ++i) {
- left = find(d_diseq[i][0]);
- right = find(d_diseq[i][1]);
- if ((left == af && right == bf) ||
- (left == bf && right == af)) {
- return true;
- }
- }
- return false;
-}
-
-void StaticFactManager::addDiseq(TNode eq) {
- Assert(eq.getKind() == kind::EQUAL);
- d_diseq.push_back(eq);
-}
-
-void StaticFactManager::addEq(TNode eq) {
- Assert(eq.getKind() == kind::EQUAL);
- Node a = find(eq[0]);
- Node b = find(eq[1]);
-
- if( a == b) {
- return;
- }
-
- /*
- * take care of the congruence closure part
- */
-
- // make "a" the one with shorter diseqList
- // CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
- // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
-
- // if(deq_ia != d_disequalities.end()) {
- // if(deq_ib == d_disequalities.end() ||
- // (*deq_ia).second->size() > (*deq_ib).second->size()) {
- // TNode tmp = a;
- // a = b;
- // b = tmp;
- // }
- // }
- // a = find(a);
- // b = find(b);
-
-
- // b becomes the canon of a
- setCanon(a, b);
-
- // deq_ia = d_disequalities.find(a);
- // map<TNode, TNode> alreadyDiseqs;
- // if(deq_ia != d_disequalities.end()) {
- // /*
- // * Collecting the disequalities of b, no need to check for conflicts
- // * since the representative of b does not change and we check all the things
- // * in a's class when we look at the diseq list of find(a)
- // */
-
- // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
- // if(deq_ib != d_disequalities.end()) {
- // CTNodeListAlloc* deq = (*deq_ib).second;
- // for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end();
- // j++) {
- // TNode deqn = *j;
- // TNode s = deqn[0];
- // TNode t = deqn[1];
- // TNode sp = find(s);
- // TNode tp = find(t);
- // Assert(sp == b || tp == b);
- // if(sp == b) {
- // alreadyDiseqs[tp] = deqn;
- // } else {
- // alreadyDiseqs[sp] = deqn;
- // }
- // }
- // }
-
- // /*
- // * Looking for conflicts in the a disequality list. Note
- // * that at this point a and b are already merged. Also has
- // * the side effect that it adds them to the list of b (which
- // * became the canonical representative)
- // */
-
- // CTNodeListAlloc* deqa = (*deq_ia).second;
- // for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end();
- // i++) {
- // TNode deqn = (*i);
- // Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() ==
- // kind::IFF); TNode s = deqn[0]; TNode t = deqn[1]; TNode sp = find(s);
- // TNode tp = find(t);
-
- // if(find(s) == find(t)) {
- // d_conflict = deqn;
- // return;
- // }
- // Assert( sp == b || tp == b);
-
- // // make sure not to add duplicates
-
- // if(sp == b) {
- // if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
- // appendToDiseqList(b, deqn);
- // alreadyDiseqs[tp] = deqn;
- // }
- // } else {
- // if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
- // appendToDiseqList(b, deqn);
- // alreadyDiseqs[sp] = deqn;
- // }
- // }
-
- // }
- // }
-
- // // TODO: check for equality propagations
- // // a and b are find(a) and find(b) here
- // checkPropagations(a,b);
-
- // if(a.getType().isArray()) {
- // checkRowLemmas(a,b);
- // checkRowLemmas(b,a);
- // // note the change in order, merge info adds the list of
- // // the 2nd argument to the first
- // d_infoMap.mergeInfo(b, a);
- // }
-}
-
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file static_fact_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Clark Barrett, Mathias Preiner, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Path-compressing, backtrackable union-find using an undo
- ** stack. Refactored from the UF union-find.
- **
- ** Path-compressing, backtrackable union-find using an undo stack
- ** rather than storing items in a CDMap<>.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
-#define CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
-
-#include <utility>
-#include <vector>
-#include <unordered_map>
-
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
- class StaticFactManager {
- /** Our underlying map type. */
- typedef std::unordered_map<Node, Node, NodeHashFunction> MapType;
-
- /**
- * Our map of Nodes to their canonical representatives.
- * If a Node is not present in the map, it is its own
- * representative.
- */
- MapType d_map;
- std::vector<Node> d_diseq;
-
-public:
- StaticFactManager() {}
-
- /**
- * Return a Node's union-find representative, doing path compression.
- */
- inline TNode find(TNode n);
-
- /**
- * Return a Node's union-find representative, NOT doing path compression.
- * This is useful for Assert() statements, debug checking, and similar
- * things that you do NOT want to mutate the structure.
- */
- inline TNode debugFind(TNode n) const;
-
- /**
- * Set the canonical representative of n to newParent. They should BOTH
- * be their own canonical representatives on entry to this funciton.
- */
- inline void setCanon(TNode n, TNode newParent);
-
- bool areEq(TNode a, TNode b);
- bool areDiseq(TNode a, TNode b);
- void addDiseq(TNode eq);
- void addEq(TNode eq);
-
-};/* class StaticFactManager<> */
-
-inline TNode StaticFactManager::debugFind(TNode n) const {
- MapType::const_iterator i = d_map.find(n);
- if(i == d_map.end()) {
- return n;
- } else {
- return debugFind((*i).second);
- }
-}
-
-inline TNode StaticFactManager::find(TNode n) {
- Trace("arraysuf") << "arraysUF find of " << n << std::endl;
- MapType::iterator i = d_map.find(n);
- if(i == d_map.end()) {
- Trace("arraysuf") << "arraysUF it is rep" << std::endl;
- return n;
- } else {
- Trace("arraysuf") << "arraysUF not rep: par is " << (*i).second << std::endl;
- std::pair<TNode, TNode> pr = *i;
- // our iterator is invalidated by the recursive call to find(),
- // since it mutates the map
- TNode p = find(pr.second);
- if(p == pr.second) {
- return p;
- }
- pr.second = p;
- d_map.insert(pr);
- return p;
- }
-}
-
-inline void StaticFactManager::setCanon(TNode n, TNode newParent) {
- Assert(d_map.find(n) == d_map.end());
- Assert(d_map.find(newParent) == d_map.end());
- if(n != newParent) {
- d_map[n] = newParent;
- }
-}
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /*CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */
// 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;
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),
{
d_equalityEngine->addFunctionKind(kind::STORE);
}
- if (d_useArrTable)
- {
- d_equalityEngine->addFunctionKind(kind::ARR_TABLE_FUN);
- }
}
/////////////////////////////////////////////////////////////////////////////
<< 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;
}
bool ok = d_out->propagate(literal);
if (!ok) {
- d_conflict = true;
+ d_state.notifyInConflict();
}
return ok;
}/* TheoryArrays::propagate(TNode) */
*/
void TheoryArrays::preRegisterTermInternal(TNode node)
{
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
return;
}
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
// 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);
// !d_equalityEngine->consistent());
}
-
void TheoryArrays::preRegisterTerm(TNode node)
{
preRegisterTermInternal(node);
}
}
-
-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;
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);
//}
// 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
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;
}
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;
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;
}
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)
{
}
// If no more to do, break
- if (d_conflict || d_mergeQueue.empty()) {
+ if (d_state.isInConflict() || d_mergeQueue.empty())
+ {
break;
}
{
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;
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))
int prop = options::arraysPropagate();
if (prop > 0) {
propagate(l);
- if (d_conflict) {
+ if (d_state.isInConflict())
+ {
return true;
}
}
d_out->conflict(d_conflictNode);
}
- d_conflict = true;
+ d_state.notifyInConflict();
}
TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy(
projects / cvc5.git / commitdiff