LDFLAGS="$cvc4_save_LDFLAGS"
fi
if test $cvc4_has_threads = no; then
- if test $with_portfolio = yes; then
+ if test x$with_portfolio = xyes; then
AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
fi
with_portfolio=no
{ $t = PARSER_STATE->getSort(name); }
| BITVECTOR_TOK '[' NUMERAL_TOK ']' {
$t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK));
- }
+ }
+ /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in
+ * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */
+ | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' {
+ $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)),
+ EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2)));
+ }
;
/**
logicMap["QF_UFLIRA"] = QF_UFLIRA;
logicMap["QF_UFNIA"] = QF_UFNIA;
logicMap["QF_UFNIRA"] = QF_UFNIRA;
+ logicMap["QF_ABV"] = QF_ABV;
+ logicMap["QF_AUFBV"] = QF_AUFBV;
+ logicMap["QF_UFNIRA"] = QF_UFNIRA;
logicMap["QF_AUFLIA"] = QF_AUFLIA;
logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
return logicMap;
addTheory(THEORY_BITVECTORS);
break;
+ case QF_ABV:
+ addTheory(THEORY_ARRAYS_EX);
+ addTheory(THEORY_BITVECTORS);
+ break;
+
+ case QF_AUFBV:
+ addUf();
+ addTheory(THEORY_ARRAYS_EX);
+ addTheory(THEORY_BITVECTORS);
+ break;
+
case QF_AUFLIA:
addTheory(THEORY_ARRAYS_EX);
addUf();
case AUFNIRA:
case LRA:
case UFNIA:
- case QF_AUFBV:
Unhandled(name);
}
}
AUFLIRA,
AUFNIRA,
LRA,
+ QF_ABV,
QF_AUFBV,
QF_AUFLIA,
QF_AUFLIRA,
addTheory(THEORY_BITVECTORS);
break;
+ case Smt::QF_ABV:
+ addTheory(THEORY_ARRAYS);
+ addTheory(THEORY_BITVECTORS);
+ break;
+
+ case Smt::QF_AUFBV:
+ addOperator(kind::APPLY_UF);
+ addTheory(THEORY_ARRAYS);
+ addTheory(THEORY_BITVECTORS);
+ break;
+
case Smt::QF_AUFLIA:
addTheory(THEORY_ARRAYS);
addOperator(kind::APPLY_UF);
case Smt::AUFNIRA:
case Smt::LRA:
case Smt::UFNIA:
- case Smt::QF_AUFBV:
Unhandled(name);
}
}
bool Solver::addClause_(vec<Lit>& ps)
{
- assert(decisionLevel() == 0);
+ if (decisionLevel() > 0) {
+ cancelUntil(0);
+ }
+
if (!ok) return false;
// Check if clause is satisfied and remove false/duplicate literals:
only_bcp = true;
ccmin_mode = 0;
lbool result = search(-1, UIP_FIRST);
+ return result;
} else {
return l_True;
}
model.clear();
conflict.clear();
- ccmin_mode = 2;
-
- // reduce the database
- reduceDB();
-
- // this is a new search, reset the parameters
- restart_first = opt_restart_first;
- restart_inc = opt_restart_inc;
+ ccmin_mode = 0;
if (!ok) return l_False;
//
void addMarkerLiteral(Var var) {
+ // make sure it wasn't already marked
+ Assert(marker[var] == 0);
marker[var] = 1;
}
delete d_satSolver;
}
+void PropEngine::processAssertionsStart() {
+ d_theoryEngine->preprocessStart();
+}
+
void PropEngine::assertFormula(TNode node) {
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "assertFormula(" << node << ")" << endl;
*/
void shutdown() { }
+ /**
+ * Signal that a new round of assertions is ready so we can notify the theory engine
+ */
+ void processAssertionsStart();
+
/**
* Converts the given formula to CNF and assert the CNF to the SAT solver.
* The formula is asserted permanently for the current context.
}
}
+ d_smt.d_propEngine->processAssertionsStart();
+
// Push the formula to SAT
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
}
Node TheoryArith::ppRewrite(TNode atom) {
+
+ if (!atom.getType().isBoolean()) {
+ return atom;
+ }
+
Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
Node a = d_pbSubstitutions.apply(atom);
};
+void ArrayInfo::setNonLinear(const TNode a) {
+ Assert(a.getType().isArray());
+ Info* temp_info;
+ CNodeInfoMap::iterator it = info_map.find(a);
+ if(it == info_map.end()) {
+ temp_info = new Info(ct, bck);
+ temp_info->isNonLinear = true;
+ info_map[a] = temp_info;
+ } else {
+ (*it).second->isNonLinear = true;
+ }
+
+}
+
/**
* Returns the information associated with TNode a
return emptyInfo;
}
+const bool ArrayInfo::isNonLinear(const TNode a) const
+{
+ CNodeInfoMap::const_iterator it = info_map.find(a);
+
+ if(it!= info_map.end())
+ return (*it).second->isNonLinear;
+ return false;
+}
+
List<TNode>* ArrayInfo::getIndices(const TNode a) const{
CNodeInfoMap::const_iterator it = info_map.find(a);
if(it!= info_map.end()) {
namespace arrays {
typedef context::CDList<TNode> CTNodeList;
+typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
-struct TNodeQuadHashFunction {
- size_t operator()(const quad<CVC4::TNode, CVC4::TNode, CVC4::TNode, CVC4::TNode>& q ) const {
+struct RowLemmaTypeHashFunction {
+ size_t operator()(const RowLemmaType& q ) const {
TNode n1 = q.first;
TNode n2 = q.second;
TNode n3 = q.third;
n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF);
}
-};/* struct TNodeQuadHashFunction */
+};/* struct RowLemmaTypeHashFunction */
void printList (CTNodeList* list);
void printList( List<TNode>* list);
class Info {
public:
+ context::CDO<bool> isNonLinear;
List<TNode>* indices;
CTNodeList* stores;
CTNodeList* in_stores;
- Info(context::Context* c, Backtracker<TNode>* bck) {
+ Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false) {
indices = new List<TNode>(bck);
stores = new(true)CTNodeList(c);
in_stores = new(true)CTNodeList(c);
void addStore(const Node a, const TNode st);
void addInStore(const TNode a, const TNode st);
+ void setNonLinear(const TNode a);
/**
* Returns the information associated with TNode a
const Info* getInfo(const TNode a) const;
+ const bool isNonLinear(const TNode a) const;
+
List<TNode>* getIndices(const TNode a) const;
const CTNodeList* getStores(const TNode a) const;
theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
typechecker "theory/arrays/theory_arrays_type_rules.h"
-properties polite stable-infinite
+properties polite stable-infinite parametric
properties check propagate presolve
rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
# store a i e is a[i] <= e
operator STORE 3 "array store"
+# used internally by array theory
+operator ARR_TABLE_FUN 4 "array table function"
+
typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
+typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
endtheory
#include <map>
#include "theory/rewriter.h"
#include "expr/command.h"
+#include "theory/uf/equality_engine_impl.h"
+
using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-TheoryArrays::TheoryArrays(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+
+// These are the options that produce the best empirical results on QF_AX benchmarks.
+// Use static configuration of options for now
+const bool d_ccStore = false;
+const bool d_useArrTable = false;
+const bool d_eagerLemmas = true;
+const bool d_propagateLemmas = false;
+const bool d_preprocess = true;
+const bool d_solveWrite = true;
+const bool d_useNonLinearOpt = true;
+
+
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
Theory(THEORY_ARRAY, c, u, out, valuation),
- d_ccChannel(this),
- d_cc(c, &d_ccChannel),
- d_unionFind(c),
- d_backtracker(c),
- d_infoMap(c,&d_backtracker),
- d_disequalities(c),
- d_equalities(c),
- d_prop_queue(c),
- d_atoms(),
- d_explanations(c),
- d_conflict(),
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_checkTimer("theory::arrays::checkTime"),
- d_donePreregister(false)
+ d_ppNotify(),
+ d_ppEqualityEngine(d_ppNotify, u, "theory::arrays::TheoryArraysPP"),
+ d_ppFacts(u),
+ // d_ppCache(u),
+ d_literalsToPropagate(c),
+ d_literalsToPropagateIndex(c, 0),
+ d_mayEqualNotify(),
+ d_mayEqualEqualityEngine(d_mayEqualNotify, c, "theory::arrays::TheoryArraysMayEqual"),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"),
+ d_conflict(c, false),
+ d_backtracker(c),
+ d_infoMap(c, &d_backtracker),
+ d_mergeQueue(c),
+ d_mergeInProgress(false),
+ d_RowQueue(u),
+ d_RowAlreadyAdded(u),
+ d_sharedArrays(c),
+ d_sharedTerms(c, false),
+ d_reads(c),
+ d_permRef(c)
{
- //d_backtracker = new Backtracker<TNode>(c);
- //d_infoMap = ArrayInfo(c, d_backtracker);
-
StatisticsRegistry::registerStat(&d_numRow);
StatisticsRegistry::registerStat(&d_numExt);
StatisticsRegistry::registerStat(&d_numProp);
StatisticsRegistry::registerStat(&d_numExplain);
+ StatisticsRegistry::registerStat(&d_numNonLinear);
+ StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits);
StatisticsRegistry::registerStat(&d_checkTimer);
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+
+ d_ppEqualityEngine.addTerm(d_true);
+ d_ppEqualityEngine.addTerm(d_false);
+ d_ppEqualityEngine.addTriggerEquality(d_true, d_false, d_false);
+
+ d_equalityEngine.addTerm(d_true);
+ d_equalityEngine.addTerm(d_false);
+ d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine.addFunctionKind(kind::SELECT);
+ if (d_ccStore) {
+ d_equalityEngine.addFunctionKind(kind::STORE);
+ }
+ d_equalityEngine.addFunctionKind(kind::EQUAL);
+ if (d_useArrTable) {
+ d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
+ }
}
StatisticsRegistry::unregisterStat(&d_numExt);
StatisticsRegistry::unregisterStat(&d_numProp);
StatisticsRegistry::unregisterStat(&d_numExplain);
+ StatisticsRegistry::unregisterStat(&d_numNonLinear);
+ StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits);
StatisticsRegistry::unregisterStat(&d_checkTimer);
}
-void TheoryArrays::addSharedTerm(TNode t) {
- Trace("arrays") << "Arrays::addSharedTerm(): "
- << t << endl;
-}
-
-
-void TheoryArrays::notifyEq(TNode lhs, TNode rhs) {
-}
-
-void TheoryArrays::notifyCongruent(TNode a, TNode b) {
- Trace("arrays") << "Arrays::notifyCongruent(): "
- << a << " = " << b << endl;
- if(!d_conflict.isNull()) {
- return;
- }
- merge(a,b);
-}
-
-
-void TheoryArrays::check(Effort e) {
- TimerStat::CodeTimer codeTimer(d_checkTimer);
-
- if(!d_donePreregister ) {
- // only start looking for lemmas after preregister on all input terms
- // has been called
- return;
- }
-
- Trace("arrays") <<"Arrays::start check ";
- while(!done()) {
- Node assertion = get();
- Trace("arrays") << "Arrays::check(): " << assertion << endl;
-
- switch(assertion.getKind()) {
- case kind::EQUAL:
- case kind::IFF:
- d_cc.addEquality(assertion);
- if(!d_conflict.isNull()) {
- // addEquality can cause a notify congruent which calls merge
- // which can lead to a conflict
- Node conflict = constructConflict(d_conflict);
- d_conflict = Node::null();
- d_out->conflict(conflict);
- return;
- }
- merge(assertion[0], assertion[1]);
- break;
- case kind::NOT:
- {
- Assert(assertion[0].getKind() == kind::EQUAL ||
- assertion[0].getKind() == kind::IFF );
- Node a = assertion[0][0];
- Node b = assertion[0][1];
- addDiseq(assertion[0]);
-
- d_cc.addTerm(a);
- d_cc.addTerm(b);
-
- if(!d_conflict.isNull()) {
- // we got notified through notifyCongruent which called merge
- // after addTerm since we weren't watching a or b before
- Node conflict = constructConflict(d_conflict);
- d_conflict = Node::null();
- d_out->conflict(conflict);
- return;
- }
- else if(find(a) == find(b)) {
- Node conflict = constructConflict(assertion[0]);
- d_conflict = Node::null();
- d_out->conflict(conflict);
- return;
- }
- Assert(!d_cc.areCongruent(a,b));
- if(a.getType().isArray()) {
- queueExtLemma(a, b);
- }
- break;
- }
- default:
- Unhandled(assertion.getKind());
- }
-
- }
-
- if(fullEffort(e)) {
- // generate the lemmas on the worklist
- //while(!d_RowQueue.empty() || ! d_extQueue.empty()) {
- dischargeLemmas();
- Trace("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n";
- //}
- }
- Trace("arrays") << "Arrays::check(): done" << endl;
-}
-
-Node TheoryArrays::getValue(TNode n) {
- NodeManager* nodeManager = NodeManager::currentNM();
-
- switch(n.getKind()) {
+/////////////////////////////////////////////////////////////////////////////
+// PREPROCESSING
+/////////////////////////////////////////////////////////////////////////////
- case kind::VARIABLE:
- Unhandled(kind::VARIABLE);
-
- case kind::EQUAL: // 2 args
- return nodeManager->
- mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
-
- default:
- Unhandled(n.getKind());
- }
-}
-
-Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
- switch(in.getKind()) {
- case kind::EQUAL:
- {
- d_staticFactManager.addEq(in);
- if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
- outSubstitutions.addSubstitution(in[0], in[1]);
- return PP_ASSERT_STATUS_SOLVED;
- }
- if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
- outSubstitutions.addSubstitution(in[1], in[0]);
- return PP_ASSERT_STATUS_SOLVED;
- }
- break;
- }
- case kind::NOT:
- {
- Assert(in[0].getKind() == kind::EQUAL ||
- in[0].getKind() == kind::IFF );
- Node a = in[0][0];
- Node b = in[0][1];
- d_staticFactManager.addDiseq(in[0]);
- break;
- }
- default:
- break;
- }
- return PP_ASSERT_STATUS_UNSOLVED;
-}
-Node TheoryArrays::preprocessTerm(TNode term) {
+Node TheoryArrays::ppRewrite(TNode term) {
+ if (!d_preprocess) return term;
switch (term.getKind()) {
case kind::SELECT: {
// select(store(a,i,v),j) = select(a,j)
// IF i != j
if (term[0].getKind() == kind::STORE &&
- d_staticFactManager.areDiseq(term[0][1], term[1])) {
+ (d_ppEqualityEngine.areDisequal(term[0][1], term[1]) ||
+ (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
}
break;
// IF i != j and j comes before i in the ordering
if (term[0].getKind() == kind::STORE &&
(term[1] < term[0][1]) &&
- d_staticFactManager.areDiseq(term[1], term[0][1])) {
+ (d_ppEqualityEngine.areDisequal(term[1], term[0][1]) ||
+ (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
return outer;
break;
}
case kind::EQUAL: {
+ if (!d_solveWrite) break;
if (term[0].getKind() == kind::STORE ||
term[1].getKind() == kind::STORE) {
TNode left = term[0];
NodeBuilder<> hyp(kind::AND);
for (j = leftWrites - 1; j > i; --j) {
index_j = write_j[1];
- if (d_staticFactManager.areDiseq(index_i, index_j)) {
+ if (d_ppEqualityEngine.areDisequal(index_i, index_j) ||
+ (index_i.isConst() && index_j.isConst() && index_i != index_j)) {
continue;
}
Node hyp2(index_i.getType() == nm->booleanType()?
Node l = left;
Node tmp;
NodeBuilder<> nb(kind::AND);
- while (right.getKind() == STORE) {
+ while (right.getKind() == kind::STORE) {
tmp = nm->mkNode(kind::SELECT, l, right[1]);
nb << tmp.eqNode(right[2]);
tmp = nm->mkNode(kind::SELECT, right[0], right[1]);
return term;
}
-Node TheoryArrays::recursivePreprocessTerm(TNode term) {
- unsigned nc = term.getNumChildren();
- if (nc == 0 ||
- (theoryOf(term) != theory::THEORY_ARRAY &&
- term.getType() != NodeManager::currentNM()->booleanType())) {
- return term;
- }
- NodeMap::iterator find = d_ppCache.find(term);
- if (find != d_ppCache.end()) {
- return (*find).second;
- }
- NodeBuilder<> newNode(term.getKind());
- unsigned i;
- for (i = 0; i < nc; ++i) {
- newNode << recursivePreprocessTerm(term[i]);
- }
- Node newTerm = Rewriter::rewrite(newNode);
- Node newTerm2 = preprocessTerm(newTerm);
- if (newTerm != newTerm2) {
- newTerm = recursivePreprocessTerm(Rewriter::rewrite(newTerm2));
- }
- d_ppCache[term] = newTerm;
- return newTerm;
-}
-Node TheoryArrays::ppRewrite(TNode atom) {
- if (d_donePreregister) return atom;
- Assert(atom.getKind() == kind::EQUAL, "expected EQUAL, got %s", atom.toString().c_str());
- return recursivePreprocessTerm(atom);
+Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+ switch(in.getKind()) {
+ case kind::EQUAL:
+ {
+ d_ppFacts.push_back(in);
+ d_ppEqualityEngine.addEquality(in[0], in[1], in);
+ if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+ outSubstitutions.addSubstitution(in[0], in[1]);
+ return PP_ASSERT_STATUS_SOLVED;
+ }
+ if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+ outSubstitutions.addSubstitution(in[1], in[0]);
+ return PP_ASSERT_STATUS_SOLVED;
+ }
+ break;
+ }
+ case kind::NOT:
+ {
+ d_ppFacts.push_back(in);
+ Assert(in[0].getKind() == kind::EQUAL ||
+ in[0].getKind() == kind::IFF );
+ Node a = in[0][0];
+ Node b = in[0][1];
+ d_ppEqualityEngine.addDisequality(a, b, in);
+ break;
+ }
+ default:
+ break;
+ }
+ return PP_ASSERT_STATUS_UNSOLVED;
}
-void TheoryArrays::merge(TNode a, TNode b) {
- Assert(d_conflict.isNull());
+/////////////////////////////////////////////////////////////////////////////
+// T-PROPAGATION / REGISTRATION
+/////////////////////////////////////////////////////////////////////////////
- Trace("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl;
- /*
- * take care of the congruence closure part
- */
+bool TheoryArrays::propagate(TNode literal)
+{
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl;
- // make "a" the one with shorter diseqList
- CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
- CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
+ // If already in conflict, no more propagation
+ if (d_conflict) {
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl;
+ return false;
+ }
- 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;
+ // See if the literal has been asserted already
+ Node normalized = Rewriter::rewrite(literal);
+ bool satValue = false;
+ bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
+
+ // If asserted, we're done or in conflict
+ if (isAsserted) {
+ if (!satValue) {
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+ std::vector<TNode> assumptions;
+ Node negatedLiteral;
+ if (normalized != d_false) {
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+ assumptions.push_back(negatedLiteral);
+ }
+ explain(literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ return false;
}
+ // Propagate even if already known in SAT - could be a new equation between shared terms
+ // (terms that weren't shared when the literal was asserted!)
}
- a = find(a);
- b = find(b);
- if( a == b) {
- return;
- }
+ // Nothing, just enqueue it for propagation and mark it as asserted already
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+ d_literalsToPropagate.push_back(literal);
+ return true;
+}/* TheoryArrays::propagate(TNode) */
- // 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;
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
+ TNode lhs, rhs;
+ switch (literal.getKind()) {
+ case kind::EQUAL:
+ lhs = literal[0];
+ rhs = literal[1];
+ break;
+ case kind::SELECT:
+ lhs = literal;
+ rhs = d_true;
+ break;
+ case kind::NOT:
+ if (literal[0].getKind() == kind::EQUAL) {
+ // Disequalities
+ d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
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;
- }
+ // Predicates
+ lhs = literal[0];
+ rhs = d_false;
+ break;
}
+ case kind::CONST_BOOLEAN:
+ // we get to explain true = false, since we set false to be the trigger of this
+ lhs = d_true;
+ rhs = d_false;
+ break;
+ default:
+ Unreachable();
+ }
+ d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
+
+ /**
+ * Stores in d_infoMap the following information for each term a of type array:
+ *
+ * - all i, such that there exists a term a[i] or a = store(b i v)
+ * (i.e. all indices it is being read atl; store(b i v) is implicitly read at
+ * position i due to the implicit axiom store(b i v)[i] = v )
+ *
+ * - all the stores a is congruent to (this information is context dependent)
+ *
+ * - all store terms of the form store (a i v) (i.e. in which a appears
+ * directly; this is invariant because no new store terms are created)
+ *
+ * Note: completeness depends on having pre-register called on all the input
+ * terms before starting to instantiate lemmas.
+ */
+void TheoryArrays::preRegisterTerm(TNode node)
+{
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
+
+ switch (node.getKind()) {
+ case kind::EQUAL:
+ // Add the terms
+ // d_equalityEngine.addTerm(node[0]);
+ // d_equalityEngine.addTerm(node[1]);
+ d_equalityEngine.addTerm(node);
+ // Add the trigger for equality
+ d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+ d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
+ break;
+ case kind::SELECT:
+ // Reads
+ d_equalityEngine.addTerm(node);
+ // Maybe it's a predicate
+ // TODO: remove this or keep it if we allow Boolean elements in arrays.
+ if (node.getType().isBoolean()) {
+ // Get triggered for both equal and dis-equal
+ d_equalityEngine.addTriggerEquality(node, d_true, node);
+ d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
}
- }
- // TODO: check for equality propagations
- // a and b are find(a) and find(b) here
- checkPropagations(a,b);
+ d_infoMap.addIndex(node[0], node[1]);
+ checkRowForIndex(node[1], d_equalityEngine.getRepresentative(node[0]));
+ d_reads.push_back(node);
+ break;
- 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);
- }
+ case kind::STORE: {
+ d_equalityEngine.addTriggerTerm(node);
+ TNode a = node[0];
+ TNode i = node[1];
+ TNode v = node[2];
-}
+ d_mayEqualEqualityEngine.addEquality(node, node[0], d_true);
+ NodeManager* nm = NodeManager::currentNM();
+ Node ni = nm->mkNode(kind::SELECT, node, i);
+ if (!d_equalityEngine.hasTerm(ni)) {
+ preRegisterTerm(ni);
+ }
-void TheoryArrays::checkPropagations(TNode a, TNode b) {
- EqLists::const_iterator ita = d_equalities.find(a);
- EqLists::const_iterator itb = d_equalities.find(b);
+ // Apply RIntro1 Rule
+ d_equalityEngine.addEquality(ni, v, d_true);
- if(ita != d_equalities.end()) {
- if(itb!= d_equalities.end()) {
- // because b is the canonical representative
- List<TNode>* eqsa = (*ita).second;
- List<TNode>* eqsb = (*itb).second;
+ d_infoMap.addStore(node, node);
+ d_infoMap.addInStore(a, node);
- for(List<TNode>::const_iterator it = eqsa->begin(); it!= eqsa->end(); ++it) {
- Node eq = *it;
- Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF);
- if(find(eq[0])== find(eq[1])) {
- d_prop_queue.push_back(eq);
- }
- }
- eqsb->concat(eqsa);
+ checkStore(node);
+ break;
+ }
+ default:
+ // Variables etc
+ if (node.getType().isArray()) {
+ d_equalityEngine.addTriggerTerm(node);
}
else {
- List<TNode>* eqsb = new List<TNode>(&d_backtracker);
- List<TNode>* eqsa = (*ita).second;
- d_equalities.insert(b, eqsb);
- eqsb->concat(eqsa);
+ d_equalityEngine.addTerm(node);
}
- } else {
- List<TNode>* eqsb = new List<TNode>(&d_backtracker);
- d_equalities.insert(b, eqsb);
- List<TNode>* eqsa = new List<TNode>(&d_backtracker);
- d_equalities.insert(a, eqsa);
- eqsb->concat(eqsa);
+ break;
}
}
-bool TheoryArrays::isNonLinear(TNode a) {
- Assert(a.getType().isArray());
- const CTNodeList* inst = d_infoMap.getInStores(find(a));
- if(inst->size()<=1) {
- return false;
- }
- return true;
-}
-
-bool TheoryArrays::isAxiom(TNode t1, TNode t2) {
- Trace("arrays-axiom")<<"Arrays::isAxiom start "<<t1<<" = "<<t2<<"\n";
- if(t1.getKind() == kind::SELECT) {
- TNode a = t1[0];
- TNode i = t1[1];
-
- if(a.getKind() == kind::STORE) {
- TNode b = a[0];
- TNode j = a[1];
- TNode v = a[2];
- if(i == j && v == t2) {
- Trace("arrays-axiom")<<"Arrays::isAxiom true\n";
- return true;
+void TheoryArrays::propagate(Effort e)
+{
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl;
+ if (!d_conflict) {
+ for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+ TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl;
+ bool satValue;
+ Node normalized = Rewriter::rewrite(literal);
+ if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
+ d_out->propagate(literal);
+ } else {
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
+ Node negatedLiteral;
+ std::vector<TNode> assumptions;
+ if (normalized != d_false) {
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+ assumptions.push_back(negatedLiteral);
+ }
+ explain(literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ break;
}
}
}
- return false;
+
}
-Node TheoryArrays::constructConflict(TNode diseq) {
- Trace("arrays") << "arrays: begin constructConflict()" << endl;
- Trace("arrays") << "arrays: using diseq == " << diseq << endl;
+Node TheoryArrays::explain(TNode literal)
+{
+ ++d_numExplain;
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
+ std::vector<TNode> assumptions;
+ explain(literal, assumptions);
+ return mkAnd(assumptions);
+}
+
- // returns the reason the two terms are equal
- Node explanation = d_cc.explain(diseq[0], diseq[1]);
+/////////////////////////////////////////////////////////////////////////////
+// SHARING
+/////////////////////////////////////////////////////////////////////////////
- NodeBuilder<> nb(kind::AND);
- if(explanation.getKind() == kind::EQUAL ||
- explanation.getKind() == kind::IFF) {
- // if the explanation is only one literal
- if(!isAxiom(explanation[0], explanation[1]) &&
- !isAxiom(explanation[1], explanation[0])) {
- nb<<explanation;
- }
+void TheoryArrays::addSharedTerm(TNode t) {
+ Debug("arrays::sharing") << spaces(getContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
+ d_equalityEngine.addTriggerTerm(t);
+ if (t.getType().isArray()) {
+ d_sharedArrays.insert(t,true);
}
else {
- Assert(explanation.getKind() == kind::AND);
- for(TNode::iterator i = TNode(explanation).begin();
- i != TNode(explanation).end(); i++) {
- if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) {
- nb<<*i;
- }
- }
+ d_sharedTerms = true;
}
-
- nb<<diseq.notNode();
- Node conflict = nb;
- Trace("arrays") << "conflict constructed : " << conflict << endl;
- return conflict;
}
-/*
-void TheoryArrays::addAtom(TNode eq) {
- Assert(eq.getKind() == kind::EQUAL);
-
- TNode lhs = eq[0];
- TNode rhs = eq[1];
-
- appendToAtomList(find(lhs), rhs);
- appendToAtomList(find(rhs), lhs);
-}
-void TheoryArrays::appendToAtomList(TNode a, TNode b) {
- Assert(find(a) == a);
-
- NodeTNodesMap::const_iterator it = d_atoms.find(a);
- if(it != d_atoms.end()) {
- (*it).second->push_back(b);
+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 {
- CTNodeList* list = new (true)CTNodeList(getContext());
- list->push_back(b);
- d_atoms[a] = list;
+ if (d_equalityEngine.areDisequal(a, b)) {
+ // The terms are implied to be dis-equal
+ return EQUALITY_FALSE;
}
-
+ //TODO: can we be more precise sometimes?
+ return EQUALITY_UNKNOWN;
}
-*/
-void TheoryArrays::addEq(TNode eq) {
- Assert(eq.getKind() == kind::EQUAL ||
- eq.getKind() == kind::IFF);
- TNode a = eq[0];
- TNode b = eq[1];
-
- // don't need to say find(a) because due to the structure of the lists it gets
- // automatically added
- appendToEqList(a, eq);
- appendToEqList(b, eq);
-
-}
-void TheoryArrays::appendToEqList(TNode n, TNode eq) {
- Assert(eq.getKind() == kind::EQUAL ||
- eq.getKind() == kind::IFF);
-
- EqLists::const_iterator it = d_equalities.find(n);
- if(it == d_equalities.end()) {
- List<TNode>* eqs = new List<TNode>(&d_backtracker);
- eqs->append(eq);
- d_equalities.insert(n, eqs);
- } else {
- List<TNode>* eqs = (*it).second;
- eqs->append(eq);
+void TheoryArrays::computeCareGraph()
+{
+ if (d_sharedArrays.size() > 0) {
+ context::CDHashMap<TNode, bool, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
+ for (; it1 != iend; ++it1) {
+ for (it2 = it1, ++it2; it2 != iend; ++it2) {
+ EqualityStatus eqStatusArr = getEqualityStatus((*it1).first, (*it2).first);
+ if (eqStatusArr != EQUALITY_UNKNOWN) {
+ continue;
+ }
+ Assert(d_valuation.getEqualityStatus((*it1).first, (*it2).first) == EQUALITY_UNKNOWN);
+ addCarePair((*it1).first, (*it2).first);
+ ++d_numSharedArrayVarSplits;
+ return;
+ }
+ }
}
-}
+ if (d_sharedTerms) {
-void TheoryArrays::addDiseq(TNode diseq) {
- Assert(diseq.getKind() == kind::EQUAL ||
- diseq.getKind() == kind::IFF);
- TNode a = diseq[0];
- TNode b = diseq[1];
+ vector< pair<TNode, TNode> > currentPairs;
- appendToDiseqList(find(a), diseq);
- appendToDiseqList(find(b), diseq);
+ // Go through the read terms and see if there are any to split on
+ unsigned size = d_reads.size();
+ for (unsigned i = 0; i < size; ++ i) {
+ TNode r1 = d_reads[i];
-}
+ for (unsigned j = i + 1; j < size; ++ j) {
+ TNode r2 = d_reads[j];
-void TheoryArrays::appendToDiseqList(TNode of, TNode eq) {
- Trace("arrays") << "appending " << eq << endl
- << " to diseq list of " << of << endl;
- Assert(eq.getKind() == kind::EQUAL ||
- eq.getKind() == kind::IFF);
-
- CNodeTNodesMap::iterator deq_i = d_disequalities.find(of);
- CTNodeListAlloc* deq;
- if(deq_i == d_disequalities.end()) {
- deq = new(getContext()->getCMM()) CTNodeListAlloc(true, getContext(), false,
- ContextMemoryAllocator<TNode>(getContext()->getCMM()));
- d_disequalities.insertDataFromContextMemory(of, deq);
- } else {
- deq = (*deq_i).second;
- }
+ Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl;
- deq->push_back(eq);
-}
+ // If the terms are already known to be equal, we are also in good shape
+ if (d_equalityEngine.areEqual(r1, r2)) {
+ Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl;
+ continue;
+ }
+ if (r1[0] != r2[0]) {
+ // If arrays are known to be disequal, or cannot become equal, we can continue
+ if (d_equalityEngine.areDisequal(r1[0], r2[0]) ||
+ (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0]))) {
+ Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
+ continue;
+ }
+ }
-/**
- * Iterates through the indices of a and stores of b and checks if any new
- * Row lemmas need to be instantiated.
- */
-bool TheoryArrays::isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j) {
- Assert(a.getType().isArray());
- Assert(b.getType().isArray());
+ TNode x = r1[1];
+ TNode y = r2[1];
- if(d_RowAlreadyAdded.count(make_quad(a, b, i, j)) != 0 ||
- d_RowAlreadyAdded.count(make_quad(b, a, i, j)) != 0 ) {
- return true;
- }
+ EqualityStatus eqStatus = getEqualityStatus(x, y);
- return false;
-}
+ if (eqStatus != EQUALITY_UNKNOWN) {
+ Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality status known, skipping" << std::endl;
+ continue;
+ }
-bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) {
- NodeManager* nm = NodeManager::currentNM();
- Node aj = nm->mkNode(kind::SELECT, a, j);
- Node bj = nm->mkNode(kind::SELECT, b, j);
+ if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+ Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
+ continue;
+ }
- if(find(i) == find(j) || find(aj) == find(bj)) {
- Trace("arrays") << "isRedundantInContext valid "
- << a << " " << b << " " << i << " " << j << endl;
- checkRowForIndex(j, b); // why am i doing this?
- checkRowForIndex(i, a);
- return true;
- }
- Trace("arrays") << "isRedundantInContext " << a << endl
- << "isRedundantInContext " << b << endl
- << "isRedundantInContext " << i << endl
- << "isRedundantInContext " << j << endl;
- Node ieqj = i.eqNode(j);
- Node literal1 = Rewriter::rewrite(ieqj);
- bool hasValue1, satValue1;
- Node ff = nm->mkConst<bool>(false);
- Node tt = nm->mkConst<bool>(true);
- if (literal1 == ff) {
- hasValue1 = true;
- satValue1 = false;
- } else if (literal1 == tt) {
- hasValue1 = true;
- satValue1 = true;
- } else {
- hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1));
- }
- if (hasValue1) {
- if (satValue1) {
- Trace("arrays") << "isRedundantInContext returning, hasValue1 && satValue1" << endl;
- return true;
- }
- Node ajeqbj = aj.eqNode(bj);
- Node literal2 = Rewriter::rewrite(ajeqbj);
- bool hasValue2, satValue2;
- if (literal2 == ff) {
- hasValue2 = true;
- satValue2 = false;
- } else if (literal2 == tt) {
- hasValue2 = true;
- satValue2 = true;
- } else {
- hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2));
- }
- if (hasValue2) {
- if (satValue2) {
- Trace("arrays") << "isRedundantInContext returning, hasValue2 && satValue2" << endl;
- return true;
+ // Get representative trigger terms
+ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x);
+ TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y);
+
+ EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
+ switch (eqStatusDomain) {
+ case EQUALITY_FALSE_AND_PROPAGATED:
+ case EQUALITY_FALSE:
+ continue;
+ break;
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ case EQUALITY_TRUE:
+ // Should have been propagated to us
+ Assert(false);
+ continue;
+ break;
+ case EQUALITY_FALSE_IN_MODEL:
+ Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model, skipping" << std::endl;
+ continue;
+ break;
+ default:
+ break;
+ }
+
+ // Otherwise, add this pair
+ Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl;
+ addCarePair(x_shared, y_shared);
}
- // conflict
- Assert(!satValue1 && !satValue2);
- Assert(literal1.getKind() == kind::EQUAL && literal2.getKind() == kind::EQUAL);
- NodeBuilder<2> nb(kind::AND);
- //literal1 = areDisequal(literal1[0], literal1[1]);
- //literal2 = areDisequal(literal2[0], literal2[1]);
- Assert(!literal1.isNull() && !literal2.isNull());
- nb << literal1.notNode() << literal2.notNode();
- literal1 = nb;
- d_conflict = Node::null();
- d_out->conflict(literal1);
- Trace("arrays") << "TheoryArrays::isRedundantInContext() "
- << "conflict via lemma: " << literal1 << endl;
- return true;
}
}
- if(alreadyAddedRow(a, b, i, j)) {
- Trace("arrays") << "isRedundantInContext already added "
- << a << " " << b << " " << i << " " << j << endl;
- return true;
- }
- return false;
}
-TNode TheoryArrays::areDisequal(TNode a, TNode b) {
- Trace("arrays-prop") << "Arrays::areDisequal " << a << " " << b << "\n";
-
- a = find(a);
- b = find(b);
-
- CNodeTNodesMap::const_iterator it = d_disequalities.find(a);
- if(it!= d_disequalities.end()) {
- CTNodeListAlloc::const_iterator i = (*it).second->begin();
- for( ; i!= (*it).second->end(); i++) {
- Trace("arrays-prop") << " " << *i << "\n";
- TNode s = (*i)[0];
- TNode t = (*i)[1];
-
- Assert(find(s) == a || find(t) == a);
- TNode sp, tp;
- if(find(t) == a) {
- sp = find(t);
- tp = find(s);
- }
- else {
- sp = find(s);
- tp = find(t);
- }
- if(tp == b) {
- return *i;
- }
+/////////////////////////////////////////////////////////////////////////////
+// MODEL GENERATION
+/////////////////////////////////////////////////////////////////////////////
- }
- }
- Trace("arrays-prop") << " not disequal \n";
- return TNode::null();
-}
-bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) {
- Trace("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+Node TheoryArrays::getValue(TNode n)
+{
+ // TODO: Implement this
+ NodeManager* nodeManager = NodeManager::currentNM();
- NodeManager* nm = NodeManager::currentNM();
- Node aj = nm->mkNode(kind::SELECT, a, j);
- Node bj = nm->mkNode(kind::SELECT, b, j);
+ switch(n.getKind()) {
- Node eq_aj_bj = nm->mkNode(kind::EQUAL,aj, bj);
- Node eq_ij = nm->mkNode(kind::EQUAL, i, j);
-
- // first check if the current context implies NOT (i = j)
- // in which case we can propagate a[j] = b[j]
- // FIXME: does i = j need to be a SAT literal or can we propagate anyway?
-
- // if it does not have an atom we must add the lemma (do we?!)
- if(d_atoms.count(eq_aj_bj) != 0 ||
- d_atoms.count(nm->mkNode(kind::EQUAL, bj, aj))!=0) {
- Node diseq = areDisequal(i, j);
- // check if the current context implies that (NOT i = j)
- if(diseq != TNode::null()) {
- // if it's unassigned
- Trace("arrays-prop")<<"satValue "<<d_valuation.getSatValue(eq_aj_bj).isNull();
- if(d_valuation.getSatValue(eq_aj_bj).isNull()) {
- d_out->propagate(eq_aj_bj);
- ++d_numProp;
- // save explanation
- d_explanations.insert(eq_aj_bj,std::make_pair(eq_ij, diseq));
- return true;
- }
+ case kind::VARIABLE:
+ Unhandled(kind::VARIABLE);
- }
- }
+ case kind::EQUAL: // 2 args
+ return nodeManager->
+ mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
- // now check if the current context implies NOT a[j] = b[j]
- // in which case we propagate i = j
+ default:
+ Unhandled(n.getKind());
+ }
+}
- // we can't propagate if it does not have an atom
- if(d_atoms.count(eq_ij) != 0 || d_atoms.count(nm->mkNode(kind::EQUAL, j, i))!= 0) {
- Node diseq = areDisequal(aj, bj);
- Assert(TNode::null() == Node::null());
+/////////////////////////////////////////////////////////////////////////////
+// NOTIFICATIONS
+/////////////////////////////////////////////////////////////////////////////
- if(diseq != TNode::null()) {
- if(d_valuation.getSatValue(eq_ij) == Node::null()) {
- d_out->propagate(eq_ij);
- ++d_numProp;
- // save explanation
- d_explanations.insert(eq_ij, std::make_pair(eq_aj_bj,diseq));
- return true;
- }
- }
- }
- Trace("arrays-prop")<<"Arrays::propagateFromRow no prop \n";
- return false;
+void TheoryArrays::presolve()
+{
+ Trace("arrays")<<"Presolving \n";
}
-Node TheoryArrays::explain(TNode n) {
+/////////////////////////////////////////////////////////////////////////////
+// MAIN SOLVER
+/////////////////////////////////////////////////////////////////////////////
- Trace("arrays")<<"Arrays::explain start for "<<n<<"\n";
- ++d_numExplain;
-
- Assert(n.getKind()==kind::EQUAL);
- Node explanation = d_cc.explain(n[0], n[1]);
+void TheoryArrays::check(Effort e) {
+ TimerStat::CodeTimer codeTimer(d_checkTimer);
- NodeBuilder<> nb(kind::AND);
+ while (!done() && !d_conflict)
+ {
+ // Get all the assertions
+ Assertion assertion = get();
+ TNode fact = assertion.assertion;
+
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
+
+ // If the assertion doesn't have a literal, it's a shared equality
+ Assert(assertion.isPreregistered ||
+ ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
+ (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
+ d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+
+ // Do the work
+ switch (fact.getKind()) {
+ case kind::EQUAL:
+ d_equalityEngine.addEquality(fact[0], fact[1], fact);
+ break;
+ case kind::SELECT:
+ d_equalityEngine.addPredicate(fact, true, fact);
+ break;
+ case kind::NOT:
+ if (fact[0].getKind() == kind::SELECT) {
+ d_equalityEngine.addPredicate(fact[0], false, fact);
+ } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) {
+ // Assert the dis-equality
+ d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
+
+ // Apply ArrDiseq Rule if diseq is between arrays
+ if(fact[0][0].getType().isArray()) {
+ NodeManager* nm = NodeManager::currentNM();
+ TypeNode indexType = fact[0][0].getType()[0];
+ TNode k;
+ std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact);
+ if (it == d_diseqCache.end()) {
+ Node newk = nm->mkVar(indexType);
+ Dump.declareVar(newk.toExpr(),
+ "an extensional lemma index variable from the theory of arrays");
+ d_diseqCache[fact] = newk;
+ k = newk;
+ }
+ else {
+ k = (*it).second;
+ }
- if(explanation.getKind() == kind::EQUAL ||
- explanation.getKind() == kind::IFF) {
- // if the explanation is only one literal
- if(!isAxiom(explanation[0], explanation[1]) &&
- !isAxiom(explanation[1], explanation[0])) {
- nb<<explanation;
+ Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
+ Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
+ if (!d_equalityEngine.hasTerm(ak)) {
+ preRegisterTerm(ak);
+ }
+ if (!d_equalityEngine.hasTerm(bk)) {
+ preRegisterTerm(bk);
+ }
+ d_equalityEngine.addDisequality(ak, bk, fact);
+ Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n";
+ ++d_numExt;
+ }
+ }
+ break;
+ default:
+ Unreachable();
}
}
+
+ // If in conflict, output the conflict
+ if (d_conflict) {
+ Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl;
+ d_out->conflict(d_conflictNode);
+ }
else {
- Assert(explanation.getKind() == kind::AND);
- for(TNode::iterator i = TNode(explanation).begin();
- i != TNode(explanation).end(); i++) {
- if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) {
- nb<<*i;
- }
+ // Otherwise we propagate
+ propagate(e);
+
+ if(!d_eagerLemmas && fullEffort(e)) {
+ // generate the lemmas on the worklist
+ Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+ dischargeLemmas();
}
}
- Node reason = nb;
-
- return reason;
-
- /*
- context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction>::const_iterator
- it = d_explanations.find(n);
- Assert(it!= d_explanations.end());
- TNode diseq = (*it).second.second;
- TNode s = diseq[0];
- TNode t = diseq[1];
- TNode eq = (*it).second.first;
- TNode a = eq[0];
- TNode b = eq[1];
+ Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::check(): done" << endl;
+}
- Assert ((find(a) == find(s) && find(b) == find(t)) ||
- (find(a) == find(t) && find(b) == find(s)));
+Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
+{
+ Assert(conjunctions.size() > 0);
- if(find(a) == find(t)) {
- TNode temp = t;
- t = s;
- s = temp;
- }
+ std::set<TNode> all;
+ std::set<TNode> explained;
- // construct the explanation
+ unsigned i = 0;
+ TNode t;
+ for (; i < conjunctions.size(); ++i) {
+ t = conjunctions[i];
- NodeBuilder<> nb(kind::AND);
- Node explanation1 = d_cc.explain(a, s);
- Node explanation2 = d_cc.explain(b, t);
+ // Remove true node - represents axiomatically true assertion
+ if (t == d_true) continue;
- if(explanation1.getKind() == kind::AND) {
- for(TNode::iterator i= TNode(explanation1).begin();
- i!=TNode(explanation1).end(); ++i) {
- nb << *i;
+ // Expand explanation resulting from propagating a ROW lemma
+ if (t.getKind() == kind::OR) {
+ if ((explained.find(t) == explained.end())) {
+ Assert(t[1].getKind() == kind::EQUAL);
+ d_equalityEngine.explainDisequality(t[1][0], t[1][1], conjunctions);
+ explained.insert(t);
+ }
+ continue;
}
- } else {
- Assert(explanation1.getKind() == kind::EQUAL ||
- explanation1.getKind() == kind::IFF);
- nb << explanation1;
+ all.insert(t);
}
- if(explanation2.getKind() == kind::AND) {
- for(TNode::iterator i= TNode(explanation2).begin();
- i!=TNode(explanation2).end(); ++i) {
- nb << *i;
- }
- } else {
- Assert(explanation2.getKind() == kind::EQUAL ||
- explanation2.getKind() == kind::IFF);
- nb << explanation2;
+ Assert(all.size() > 0);
+ if (all.size() == 1) {
+ // All the same, or just one
+ return *(all.begin());
+ }
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
}
- nb << diseq;
- Node reason = nb;
- d_out->explanation(reason);
- Trace("arrays")<<"explanation "<< reason<<" done \n";
- */
+ return conjunction;
}
-void TheoryArrays::checkRowLemmas(TNode a, TNode b) {
- Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
- if(Trace.isOn("arrays-crl"))
- d_infoMap.getInfo(a)->print();
- Trace("arrays-crl")<<" ------------ and "<<b<<"\n";
- if(Trace.isOn("arrays-crl"))
- d_infoMap.getInfo(b)->print();
+void TheoryArrays::setNonLinear(TNode a)
+{
+ if (d_infoMap.isNonLinear(a)) return;
+
+ Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n";
+ d_infoMap.setNonLinear(a);
+ ++d_numNonLinear;
List<TNode>* i_a = d_infoMap.getIndices(a);
- const CTNodeList* st_b = d_infoMap.getStores(b);
- const CTNodeList* inst_b = d_infoMap.getInStores(b);
+ const CTNodeList* st_a = d_infoMap.getStores(a);
+ const CTNodeList* inst_a = d_infoMap.getInStores(a);
- List<TNode>::const_iterator it = i_a->begin();
- CTNodeList::const_iterator its;
+ CTNodeList::const_iterator it = st_a->begin();
- for( ; it != i_a->end(); it++ ) {
- TNode i = *it;
- its = st_b->begin();
- for ( ; its != st_b->end(); its++) {
- TNode store = *its;
+ // Propagate non-linearity down chain of stores
+ for(; it!= st_a->end(); ++it) {
+ TNode store = *it;
+ Assert(store.getKind()==kind::STORE);
+ setNonLinear(store[0]);
+ }
+
+ // Instantiate ROW lemmas that were ignored before
+ List<TNode>::const_iterator itl = i_a->begin();
+ RowLemmaType lem;
+ for(; itl != i_a->end(); ++itl ) {
+ TNode i = *itl;
+ it = inst_a->begin();
+ for ( ; it !=inst_a->end(); ++it) {
+ TNode store = *it;
Assert(store.getKind() == kind::STORE);
TNode j = store[1];
TNode c = store[0];
-
- if( !isRedundantRowLemma(store, c, j, i)){
- //&&!propagateFromRow(store, c, j, i)) {
- queueRowLemma(store, c, j, i);
- }
+ lem = make_quad(store, c, j, i);
+ Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+ queueRowLemma(lem);
}
-
}
- it = i_a->begin();
+}
- for( ; it != i_a->end(); it++ ) {
- TNode i = *it;
- its = inst_b->begin();
- for ( ; its !=inst_b->end(); its++) {
- TNode store = *its;
- Assert(store.getKind() == kind::STORE);
- TNode j = store[1];
- TNode c = store[0];
- if ( isNonLinear(c)
- &&!isRedundantRowLemma(store, c, j, i)){
- //&&!propagateFromRow(store, c, j, i)) {
- queueRowLemma(store, c, j, i);
+void TheoryArrays::mergeArrays(TNode a, TNode b)
+{
+ // Note: a is the new representative
+ Assert(a.getType().isArray() && b.getType().isArray());
+
+ if (d_mergeInProgress) {
+ // Nested call to mergeArrays, just push on the queue and return
+ d_mergeQueue.push(a.eqNode(b));
+ return;
+ }
+
+ d_mergeInProgress = true;
+
+ Node n;
+ while (true) {
+ if (d_useNonLinearOpt) {
+ bool aNL = d_infoMap.isNonLinear(a);
+ bool bNL = d_infoMap.isNonLinear(b);
+ if (aNL) {
+ if (bNL) {
+ // already both marked as non-linear - no need to do anything
+ }
+ else {
+ // Set b to be non-linear
+ setNonLinear(b);
+ }
}
+ else {
+ if (bNL) {
+ // Set a to be non-linear
+ setNonLinear(a);
+ }
+ else {
+ // Check for new non-linear arrays
+ const CTNodeList* astores = d_infoMap.getStores(a);
+ const CTNodeList* bstores = d_infoMap.getStores(a);
+ Assert(astores->size() <= 1 && bstores->size() <= 1);
+ if (astores->size() > 0 && bstores->size() > 0) {
+ setNonLinear(a);
+ setNonLinear(b);
+ }
+ }
+ }
+ }
+
+ d_mayEqualEqualityEngine.addEquality(a, b, d_true);
+ checkRowLemmas(a,b);
+ checkRowLemmas(b,a);
+
+ // merge info adds the list of the 2nd argument to the first
+ d_infoMap.mergeInfo(a, b);
+
+ // If no more to do, break
+ if (d_conflict || d_mergeQueue.empty()) {
+ break;
}
- }
- Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
+ // Otherwise, prepare for next iteration
+ n = d_mergeQueue.front();
+ a = n[0];
+ b = n[1];
+ d_mergeQueue.pop();
+ }
+ d_mergeInProgress = false;
}
-/**
- * Adds a new Row lemma of the form i = j OR a[j] = b[j] if i and j are not the
- * same and a and b are also not identical.
- *
- */
-
-inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) {
- Assert(a.getType().isArray());
- Assert(b.getType().isArray());
- // construct lemma
- NodeManager* nm = NodeManager::currentNM();
- Node aj = nm->mkNode(kind::SELECT, a, j);
- Node bj = nm->mkNode(kind::SELECT, b, j);
- Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
- Node eq2 = nm->mkNode(kind::EQUAL, i, j);
- Node lem = nm->mkNode(kind::OR, eq2, eq1);
+void TheoryArrays::checkStore(TNode a) {
+ Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
+ if(Trace.isOn("arrays-cri")) {
+ d_infoMap.getInfo(a)->print();
+ }
+ Assert(a.getType().isArray());
+ Assert(a.getKind()==kind::STORE);
+ TNode b = a[0];
+ TNode i = a[1];
+ TNode brep = d_equalityEngine.getRepresentative(b);
- Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
- d_RowAlreadyAdded.insert(make_quad(a,b,i,j));
- d_out->lemma(lem);
- ++d_numRow;
+ if (!d_useNonLinearOpt || d_infoMap.isNonLinear(brep)) {
+ List<TNode>* js = d_infoMap.getIndices(brep);
+ List<TNode>::const_iterator it = js->begin();
+ RowLemmaType lem;
+ for(; it!= js->end(); ++it) {
+ TNode j = *it;
+ if (i == j) continue;
+ lem = make_quad(a,b,i,j);
+ Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
+ queueRowLemma(lem);
+ }
+ }
}
-/**
- * Because a is now being read at position i check if new lemmas can be
- * instantiated for all store terms equal to a and all store terms of the form
- * store(a _ _ )
- */
-void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
+void TheoryArrays::checkRowForIndex(TNode i, TNode a)
+{
Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
Trace("arrays-cri")<<" index "<<i<<"\n";
d_infoMap.getInfo(a)->print();
}
Assert(a.getType().isArray());
+ Assert(d_equalityEngine.getRepresentative(a) == a);
const CTNodeList* stores = d_infoMap.getStores(a);
const CTNodeList* instores = d_infoMap.getInStores(a);
CTNodeList::const_iterator it = stores->begin();
+ RowLemmaType lem;
- for(; it!= stores->end(); it++) {
+ for(; it!= stores->end(); ++it) {
TNode store = *it;
Assert(store.getKind()==kind::STORE);
TNode j = store[1];
- //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
- if(!isRedundantRowLemma(store, store[0], j, i)) {
- //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
- queueRowLemma(store, store[0], j, i);
- }
+ if (i == j) continue;
+ lem = make_quad(store, store[0], j, i);
+ Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+ queueRowLemma(lem);
}
- it = instores->begin();
- for(; it!= instores->end(); it++) {
- TNode instore = *it;
- Assert(instore.getKind()==kind::STORE);
- TNode j = instore[1];
- //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
- if(!isRedundantRowLemma(instore, instore[0], j, i)) {
- //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
- queueRowLemma(instore, instore[0], j, i);
+ if (!d_useNonLinearOpt || d_infoMap.isNonLinear(a)) {
+ it = instores->begin();
+ for(; it!= instores->end(); ++it) {
+ TNode instore = *it;
+ Assert(instore.getKind()==kind::STORE);
+ TNode j = instore[1];
+ if (i == j) continue;
+ lem = make_quad(instore, instore[0], j, i);
+ Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+ queueRowLemma(lem);
}
}
-
}
-void TheoryArrays::checkStore(TNode a) {
- Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
-
- if(Trace.isOn("arrays-cri")) {
+// a just became equal to b
+// look for new ROW lemmas
+void TheoryArrays::checkRowLemmas(TNode a, TNode b)
+{
+ Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
+ if(Trace.isOn("arrays-crl"))
d_infoMap.getInfo(a)->print();
- }
- Assert(a.getType().isArray());
- Assert(a.getKind()==kind::STORE);
- TNode b = a[0];
- TNode i = a[1];
+ Trace("arrays-crl")<<" ------------ and "<<b<<"\n";
+ if(Trace.isOn("arrays-crl"))
+ d_infoMap.getInfo(b)->print();
- List<TNode>* js = d_infoMap.getIndices(b);
- List<TNode>::const_iterator it = js->begin();
+ List<TNode>* i_a = d_infoMap.getIndices(a);
+ const CTNodeList* st_b = d_infoMap.getStores(b);
+ const CTNodeList* inst_b = d_infoMap.getInStores(b);
+
+ List<TNode>::const_iterator it = i_a->begin();
+ CTNodeList::const_iterator its;
- for(; it!= js->end(); it++) {
- TNode j = *it;
+ RowLemmaType lem;
- if(!isRedundantRowLemma(a, b, i, j)) {
- //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
- queueRowLemma(a,b,i,j);
+ for( ; it != i_a->end(); ++it ) {
+ TNode i = *it;
+ its = st_b->begin();
+ for ( ; its != st_b->end(); ++its) {
+ TNode store = *its;
+ Assert(store.getKind() == kind::STORE);
+ TNode j = store[1];
+ TNode c = store[0];
+ lem = make_quad(store, c, j, i);
+ Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+ queueRowLemma(lem);
}
}
+ if (!d_useNonLinearOpt || d_infoMap.isNonLinear(b)) {
+ for(it = i_a->begin() ; it != i_a->end(); ++it ) {
+ TNode i = *it;
+ its = inst_b->begin();
+ for ( ; its !=inst_b->end(); ++its) {
+ TNode store = *its;
+ Assert(store.getKind() == kind::STORE);
+ TNode j = store[1];
+ TNode c = store[0];
+ lem = make_quad(store, c, j, i);
+ Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+ queueRowLemma(lem);
+ }
+ }
+ }
+ Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
}
-inline void TheoryArrays::queueExtLemma(TNode a, TNode b) {
+
+void TheoryArrays::queueRowLemma(RowLemmaType lem)
+{
+ if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
+ return;
+ }
+ TNode a = lem.first;
+ TNode b = lem.second;
+ TNode i = lem.third;
+ TNode j = lem.fourth;
Assert(a.getType().isArray() && b.getType().isArray());
+ if (d_equalityEngine.areEqual(a,b) ||
+ d_equalityEngine.areEqual(i,j)) {
+ return;
+ }
- d_extQueue.insert(make_pair(a,b));
-}
+ NodeManager* nm = NodeManager::currentNM();
-void TheoryArrays::queueRowLemma(TNode a, TNode b, TNode i, TNode j) {
- Assert(a.getType().isArray() && b.getType().isArray());
-//if(!isRedundantInContext(a,b,i,j)) {
- d_RowQueue.insert(make_quad(a, b, i, j));
-}
+ Node aj = nm->mkNode(kind::SELECT, a, j);
+ Node bj = nm->mkNode(kind::SELECT, b, j);
+ if (!d_equalityEngine.hasTerm(aj)) {
+ preRegisterTerm(aj);
+ }
+ if (!d_equalityEngine.hasTerm(bj)) {
+ preRegisterTerm(bj);
+ }
+
+ if (d_equalityEngine.areEqual(aj,bj)) {
+ return;
+ }
+
+ if (d_useArrTable) {
+ Node tableEntry = nm->mkNode(kind::ARR_TABLE_FUN, a, b, i, j);
+ if (d_equalityEngine.getSize(tableEntry) != 1) {
+ return;
+ }
+ }
-/**
-* Adds a new Ext lemma of the form
-* a = b OR a[k]!=b[k], for a new variable k
-*/
+ //Propagation
+ if (d_propagateLemmas) {
+ if (d_equalityEngine.areDisequal(i,j)) {
+ Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
+ Node reason = nm->mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j));
+ d_permRef.push_back(reason);
+ d_equalityEngine.addEquality(aj, bj, reason);
+ ++d_numProp;
+ return;
+ }
+ if (d_equalityEngine.areDisequal(aj,bj)) {
+ Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
+ Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj));
+ d_permRef.push_back(reason);
+ d_equalityEngine.addEquality(i, j, reason);
+ ++d_numProp;
+ return;
+ }
+ }
-inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
- Assert(a.getType().isArray());
- Assert(b.getType().isArray());
+ // TODO: maybe add triggers here
- Trace("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n";
- Trace("arrays-cle")<<" and "<<b<<" \n";
+ if (d_eagerLemmas) {
+ Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
+ Node eq2 = nm->mkNode(kind::EQUAL, i, j);
+ Node lemma = nm->mkNode(kind::OR, eq2, eq1);
+ Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lemma<<"\n";
+ d_RowAlreadyAdded.insert(lem);
+ d_out->lemma(lemma);
+ ++d_numRow;
+ }
+ else {
+ d_RowQueue.push(lem);
+ }
+}
- if( d_extAlreadyAdded.count(make_pair(a, b)) == 0
- && d_extAlreadyAdded.count(make_pair(b, a)) == 0) {
+void TheoryArrays::dischargeLemmas()
+{
+ size_t sz = d_RowQueue.size();
+ for (unsigned count = 0; count < sz; ++count) {
+ RowLemmaType l = d_RowQueue.front();
+ d_RowQueue.pop();
+ if (d_RowAlreadyAdded.count(l) != 0) {
+ continue;
+ }
- NodeManager* nm = NodeManager::currentNM();
- TypeNode ixType = a.getType()[0];
- Node k = nm->mkVar(ixType);
- Dump.declareVar(k.toExpr(), "an extensional lemma index variable from the theory of arrays");
- Node eq = nm->mkNode(kind::EQUAL, a, b);
- Node ak = nm->mkNode(kind::SELECT, a, k);
- Node bk = nm->mkNode(kind::SELECT, b, k);
- Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk));
- Node lem = nm->mkNode(kind::OR, eq, neq);
+ TNode a = l.first;
+ TNode b = l.second;
+ TNode i = l.third;
+ TNode j = l.fourth;
+ Assert(a.getType().isArray() && b.getType().isArray());
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node aj = nm->mkNode(kind::SELECT, a, j);
+ Node bj = nm->mkNode(kind::SELECT, b, j);
+
+ // Check for redundant lemma
+ // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
+ if (d_equalityEngine.areEqual(i,j) ||
+ d_equalityEngine.areEqual(a,b) ||
+ d_equalityEngine.areEqual(aj,bj)) {
+ d_RowQueue.push(l);
+ continue;
+ }
- Trace("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n";
- d_extAlreadyAdded.insert(make_pair(a,b));
- d_out->lemma(lem);
- ++d_numExt;
- return;
- }
+ // construct lemma
+ Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
+ Node eq2 = nm->mkNode(kind::EQUAL, i, j);
+ Node lem = nm->mkNode(kind::OR, eq2, eq1);
- Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
+ Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
+ d_RowAlreadyAdded.insert(l);
+ d_out->lemma(lem);
+ ++d_numRow;
+ }
}
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
/*! \file theory_arrays.h
** \verbatim
** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: lianah
** Minor contributors (to current version): barrett
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
#include "theory/theory.h"
-#include "theory/arrays/union_find.h"
-#include "util/congruence_closure.h"
#include "theory/arrays/array_info.h"
-#include "util/hash.h"
-#include "util/ntuple.h"
#include "util/stats.h"
-#include "util/backtrackable.h"
-#include "theory/arrays/static_fact_manager.h"
-
-#include <iostream>
-#include <map>
+#include "theory/uf/equality_engine.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
namespace CVC4 {
namespace theory {
* check. Ext lemmas are stored in a cache to prevent instantiating essentially
* the same lemma multiple times.
*/
-class TheoryArrays : public Theory {
-private:
+static inline std::string spaces(int level)
+{
+ std::string indentStr(level, ' ');
+ return indentStr;
+}
+class TheoryArrays : public Theory {
- class CongruenceChannel {
- TheoryArrays* d_arrays;
+ /////////////////////////////////////////////////////////////////////////////
+ // MISC
+ /////////////////////////////////////////////////////////////////////////////
- public:
- CongruenceChannel(TheoryArrays* arrays) : d_arrays(arrays) {}
- void notifyCongruent(TNode a, TNode b) {
- d_arrays->notifyCongruent(a, b);
- }
- }; /* class CongruenceChannel*/
- friend class CongruenceChannel;
+ private:
- /**
- * Output channel connected to the congruence closure module.
- */
- CongruenceChannel d_ccChannel;
+ /** True node for predicates = true */
+ Node d_true;
- /**
- * Instance of the congruence closure module.
- */
- CongruenceClosure<CongruenceChannel, CONGRUENCE_OPERATORS_1
- (kind::SELECT)> d_cc;
+ /** True node for predicates = false */
+ Node d_false;
- /**
- * (Temporary) fact manager for preprocessing - eventually handle this with
- * something more standard (like congruence closure module)
- */
- StaticFactManager d_staticFactManager;
+ // Statistics
- /**
- * Cache for proprocessing of atoms.
- */
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
- NodeMap d_ppCache;
+ /** number of Row lemmas */
+ IntStat d_numRow;
+ /** number of Ext lemmas */
+ IntStat d_numExt;
+ /** number of propagations */
+ IntStat d_numProp;
+ /** number of explanations */
+ IntStat d_numExplain;
+ /** calls to non-linear */
+ IntStat d_numNonLinear;
+ /** splits on array variables */
+ IntStat d_numSharedArrayVarSplits;
+ /** time spent in check() */
+ TimerStat d_checkTimer;
- /**
- * Union find for storing the equalities.
- */
+ public:
- UnionFind<Node, NodeHashFunction> d_unionFind;
+ TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+ ~TheoryArrays();
- Backtracker<TNode> d_backtracker;
+ std::string identify() const { return std::string("TheoryArrays"); }
+ /////////////////////////////////////////////////////////////////////////////
+ // PREPROCESSING
+ /////////////////////////////////////////////////////////////////////////////
- /**
- * Context dependent map from a congruence class canonical representative of
- * type array to an Info pointer that keeps track of information useful to axiom
- * instantiation
- */
+ private:
- ArrayInfo d_infoMap;
+ // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used
+ class PPNotifyClass {
+ public:
+ bool notify(TNode propagation) { return true; }
+ void notify(TNode t1, TNode t2) { }
+ };
- /**
- * Received a notification from the congruence closure algorithm that the two
- * nodes a and b have become congruent.
- */
+ /** The notify class for d_ppEqualityEngine */
+ PPNotifyClass d_ppNotify;
- void notifyCongruent(TNode a, TNode b);
+ /** Equaltity engine */
+ uf::EqualityEngine<PPNotifyClass> d_ppEqualityEngine;
+ // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine
+ context::CDList<Node> d_ppFacts;
- typedef context::CDChunkList<TNode> CTNodeListAlloc;
- typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
- typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
+ Node preprocessTerm(TNode term);
+ Node recursivePreprocessTerm(TNode term);
+ public:
- typedef __gnu_cxx::hash_map<TNode, CTNodeList*, TNodeHashFunction> NodeTNodesMap;
- /**
- * List of all disequalities this theory has seen. Maintains the invariant that
- * if a is in the disequality list of b, then b is in that of a. FIXME? make non context dep map
- * */
- CNodeTNodesMap d_disequalities;
- EqLists d_equalities;
- context::CDList<TNode> d_prop_queue;
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ Node ppRewrite(TNode atom);
- void checkPropagations(TNode a, TNode b);
+ /////////////////////////////////////////////////////////////////////////////
+ // T-PROPAGATION / REGISTRATION
+ /////////////////////////////////////////////////////////////////////////////
- /** List of all atoms the SAT solver knows about and are candidates for
- * propagation. */
- __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_atoms;
+ private:
- /** List of disequalities needed to construct explanations for propagated
- * row lemmas */
+ /** Literals to propagate */
+ context::CDList<Node> d_literalsToPropagate;
- context::CDHashMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations;
+ /** Index of the next literal to propagate */
+ context::CDO<unsigned> d_literalsToPropagateIndex;
- /**
- * stores the conflicting disequality (still need to call construct
- * conflict to get the actual explanation)
- */
- Node d_conflict;
+ /** Should be called to propagate the literal. */
+ bool propagate(TNode literal);
- typedef context::CDList< quad<TNode, TNode, TNode, TNode > > QuadCDList;
+ /** Explain why this literal is true by adding assumptions */
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+ public:
- /**
- * Ext lemma workslist that stores extensionality lemmas that still need to be added
- */
- std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extQueue;
+ void preRegisterTerm(TNode n);
+ void propagate(Effort e);
+ Node explain(TNode n);
- /**
- * Row Lemma worklist, stores lemmas that can still be added to the SAT solver
- * to be emptied during full effort check
- */
- std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowQueue;
+ /////////////////////////////////////////////////////////////////////////////
+ // SHARING
+ /////////////////////////////////////////////////////////////////////////////
- /**
- * Extensionality lemma cache which stores the array pair (a,b) for which
- * a lemma of the form (a = b OR a[k]!= b[k]) has been added to the SAT solver.
- */
- std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extAlreadyAdded;
+ private:
- /**
- * Read-over-write lemma cache storing a quadruple (a,b,i,j) for which a
- * the lemma (i = j OR a[j] = b[j]) has been added to the SAT solver. Needed
- * to prevent infinite recursion in addRowLemma.
- */
- std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowAlreadyAdded;
+ class MayEqualNotifyClass {
+ public:
+ bool notify(TNode propagation) { return true; }
+ void notify(TNode t1, TNode t2) { }
+ };
- /*
- * Congruence helper methods
- */
+ /** The notify class for d_mayEqualEqualityEngine */
+ MayEqualNotifyClass d_mayEqualNotify;
- void addDiseq(TNode diseq);
- void addEq(TNode eq);
+ /** Equaltity engine for determining if two arrays might be equal */
+ uf::EqualityEngine<MayEqualNotifyClass> d_mayEqualEqualityEngine;
- void appendToDiseqList(TNode of, TNode eq);
- void appendToEqList(TNode a, TNode b);
- Node constructConflict(TNode diseq);
+ public:
- /**
- * Merges two congruence classes in the internal union-find and checks for a
- * conflict.
- */
+ void addSharedTerm(TNode t);
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+ void computeCareGraph();
+ bool isShared(TNode t)
+ { return (d_sharedArrays.find(t) != d_sharedArrays.end()); }
- void merge(TNode a, TNode b);
- inline TNode find(TNode a);
- inline TNode debugFind(TNode a) const;
- inline void setCanon(TNode a, TNode b);
+ /////////////////////////////////////////////////////////////////////////////
+ // MODEL GENERATION
+ /////////////////////////////////////////////////////////////////////////////
- void queueRowLemma(TNode a, TNode b, TNode i, TNode j);
- inline void queueExtLemma(TNode a, TNode b);
+ private:
+ public:
- /**
- * Adds a Row lemma of the form:
- * i = j OR a[j] = b[j]
- */
- void addRowLemma(TNode a, TNode b, TNode i, TNode j);
+ Node getValue(TNode n);
- /**
- * Adds a new Ext lemma of the form
- * a = b OR a[k]!=b[k], for a new variable k
- */
- void addExtLemma(TNode a, TNode b);
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
- /**
- * Because Row1 axioms of the form (store a i v) [i] = v are not added as
- * explicitly but are kept track of internally, is axiom recognizez an axiom
- * of the above form given the two terms in the equality.
- */
- bool isAxiom(TNode lhs, TNode rhs);
+ private:
+ public:
+ void presolve();
+ void shutdown() { }
- bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j);
- bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j);
+ /////////////////////////////////////////////////////////////////////////////
+ // MAIN SOLVER
+ /////////////////////////////////////////////////////////////////////////////
+ public:
+ void check(Effort e);
- bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) {
- //Trace("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
- std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin();
- a = find(a);
- b = find(b);
- i = find(i);
- j = find(j);
+ private:
- for( ; it!= d_RowAlreadyAdded.end(); it++) {
+ // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
+ class NotifyClass {
+ TheoryArrays& d_arrays;
+ public:
+ NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
- TNode a_ = find((*it).first);
- TNode b_ = find((*it).second);
- TNode i_ = find((*it).third);
- TNode j_ = find((*it).fourth);
- if( a == a_ && b == b_ && i==i_ && j==j_) {
- //Trace("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n";
- return true;
- }
+ bool notify(TNode propagation) {
+ Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+ // Just forward to arrays
+ return d_arrays.propagate(propagation);
}
- return false;
- }
-
-
- bool isNonLinear(TNode n);
-
- /**
- * Checks if any new Row lemmas need to be generated after merging arrays a
- * and b; called after setCanon.
- */
- void checkRowLemmas(TNode a, TNode b);
-
- /**
- * Called after a new select term a[i] is created to check whether new Row
- * lemmas need to be instantiated.
- */
- void checkRowForIndex(TNode i, TNode a);
-
- void checkStore(TNode a);
- /**
- * Lemma helper functions to prevent changing the list we are iterating through.
- */
- void insertInQuadQueue(std::set<quad<TNode, TNode, TNode, TNode> >& queue, TNode a, TNode b, TNode i, TNode j){
- if(i != j) {
- queue.insert(make_quad(a,b,i,j));
- }
- }
-
- void dischargeLemmas() {
- // we need to swap the temporary lists because adding a lemma calls preregister
- // which might modify the d_RowQueue we would be iterating through
- std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > temp_Row;
- temp_Row.swap(d_RowQueue);
-
- std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it1 = temp_Row.begin();
- for( ; it1!= temp_Row.end(); it1++) {
- if(!isRedundantInContext((*it1).first, (*it1).second, (*it1).third, (*it1).fourth)) {
- addRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth);
- }
- else {
- // add it to queue may be needed later
- queueRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth);
+ void notify(TNode t1, TNode t2) {
+ Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+ if (t1.getType().isArray()) {
+ d_arrays.mergeArrays(t1, t2);
+ if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
+ return;
+ }
}
+ // Propagate equality between shared terms
+ Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+ d_arrays.propagate(equality);
}
+ };
- std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> temp_ext;
- temp_ext.swap(d_extQueue);
- std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> ::const_iterator it2 = temp_ext.begin();
- for(; it2 != temp_ext.end(); it2++) {
- addExtLemma((*it2).first, (*it2).second);
- }
- }
+ /** The notify class for d_equalityEngine */
+ NotifyClass d_notify;
- /** Checks if instead of adding a lemma of the form i = j OR a[j] = b[j]
- * we can propagate either i = j or NOT a[j] = b[j] and does the propagation.
- * Returns whether it did propagate.
- */
- bool propagateFromRow(TNode a, TNode b, TNode i, TNode j);
+ /** Equaltity engine */
+ uf::EqualityEngine<NotifyClass> d_equalityEngine;
- TNode areDisequal(TNode a, TNode b);
-
-
-
- /*
- * === STATISTICS ===
- */
+ // Are we in conflict?
+ context::CDO<bool> d_conflict;
- /** number of Row lemmas */
- IntStat d_numRow;
- /** number of Ext lemmas */
- IntStat d_numExt;
-
- /** number of propagations */
- IntStat d_numProp;
- IntStat d_numExplain;
- /** time spent in check() */
- TimerStat d_checkTimer;
-
- bool d_donePreregister;
-
- Node preprocessTerm(TNode term);
- Node recursivePreprocessTerm(TNode term);
-
-public:
- TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
- ~TheoryArrays();
+ /** The conflict node */
+ Node d_conflictNode;
/**
- * Stores in d_infoMap the following information for each term a of type array:
- *
- * - all i, such that there exists a term a[i] or a = store(b i v)
- * (i.e. all indices it is being read atl; store(b i v) is implicitly read at
- * position i due to the implicit axiom store(b i v)[i] = v )
- *
- * - all the stores a is congruent to (this information is context dependent)
- *
- * - all store terms of the form store (a i v) (i.e. in which a appears
- * directly; this is invariant because no new store terms are created)
- *
- * Note: completeness depends on having pre-register called on all the input
- * terms before starting to instantiate lemmas.
+ * Context dependent map from a congruence class canonical representative of
+ * type array to an Info pointer that keeps track of information useful to axiom
+ * instantiation
*/
- void preRegisterTerm(TNode n) {
- //TimerStat::CodeTimer codeTimer(d_preregisterTimer);
- Trace("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n";
- //TODO: check non-linear arrays with an AlwaysAssert!!!
- //if(n.getType().isArray())
-
- switch(n.getKind()) {
- case kind::EQUAL:
- // stores the seen atoms for propagation
- Trace("arrays-preregister")<<"atom "<<n<<"\n";
- d_atoms.insert(n);
- // add to proper equality lists
- addEq(n);
- break;
- case kind::SELECT:
- //Trace("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n";
- d_infoMap.addIndex(n[0], n[1]);
- checkRowForIndex(n[1], find(n[0]));
- //Trace("arrays-preregister")<<"n[0] \n";
- //d_infoMap.getInfo(n[0])->print();
- //Trace("arrays-preregister")<<"find(n[0]) \n";
- //d_infoMap.getInfo(find(n[0]))->print();
- break;
-
- case kind::STORE:
- {
- // this should always be called at level0 since we do not create new store terms
- TNode a = n[0];
- TNode i = n[1];
- TNode v = n[2];
-
- NodeManager* nm = NodeManager::currentNM();
- Node ni = nm->mkNode(kind::SELECT, n, i);
- Node eq = nm->mkNode(kind::EQUAL, ni, v);
-
- d_cc.addEquality(eq);
-
- d_infoMap.addIndex(n, i);
- d_infoMap.addStore(n, n);
- d_infoMap.addInStore(a, n);
-
- checkStore(n);
-
- break;
- }
- default:
- Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n";
- }
- }
- //void registerTerm(TNode n) {
- // Trace("arrays-register")<<"Arrays::registerTerm "<<n<<"\n";
- //}
+ Backtracker<TNode> d_backtracker;
+ ArrayInfo d_infoMap;
- void presolve() {
- Trace("arrays")<<"Presolving \n";
- d_donePreregister = true;
- }
+ context::CDQueue<Node> d_mergeQueue;
- void addSharedTerm(TNode t);
- void notifyEq(TNode lhs, TNode rhs);
- void check(Effort e);
+ bool d_mergeInProgress;
- void propagate(Effort e) {
+ typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
- // Trace("arrays-prop")<<"Propagating \n";
+ context::CDQueue<RowLemmaType> d_RowQueue;
+ context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
- // context::CDList<TNode>::const_iterator it = d_prop_queue.begin();
- /*
- for(; it!= d_prop_queue.end(); it++) {
- TNode eq = *it;
- if(d_valuation.getSatValue(eq).isNull()) {
- //FIXME remove already propagated literals?
- d_out->propagate(eq);
- ++d_numProp;
- }
- }*/
- //d_prop_queue.deleteSelf();
- /*
- __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator it = d_atoms.begin();
-
- for(; it!= d_atoms.end(); it++) {
- TNode eq = *it;
- Assert(eq.getKind()==kind::EQUAL);
- Trace("arrays-prop")<<"value of "<<eq<<" ";
- Trace("arrays-prop")<<d_valuation.getSatValue(eq);
- if(find(eq[0]) == find(eq[1])) {
- Trace("arrays-prop")<<" eq \n";
- ++d_numProp;
- }
- }
- */
+ context::CDHashMap<TNode, bool, TNodeHashFunction> d_sharedArrays;
+ context::CDO<bool> d_sharedTerms;
+ context::CDList<TNode> d_reads;
+ std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
- }
- Node explain(TNode n);
+ // List of nodes that need permanent references in this context
+ context::CDList<Node> d_permRef;
- Node getValue(TNode n);
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
- Node ppRewrite(TNode atom);
- void shutdown() { }
- std::string identify() const { return std::string("TheoryArrays"); }
+ Node mkAnd(std::vector<TNode>& conjunctions);
+ void setNonLinear(TNode a);
+ void mergeArrays(TNode a, TNode b);
+ void checkStore(TNode a);
+ void checkRowForIndex(TNode i, TNode a);
+ void checkRowLemmas(TNode a, TNode b);
+ void queueRowLemma(RowLemmaType lem);
+ void dischargeLemmas();
};/* class TheoryArrays */
-inline void TheoryArrays::setCanon(TNode a, TNode b) {
- d_unionFind.setCanon(a, b);
-}
-
-inline TNode TheoryArrays::find(TNode a) {
- return d_unionFind.find(a);
-}
-
-inline TNode TheoryArrays::debugFind(TNode a) const {
- return d_unionFind.debugFind(a);
-}
-
}/* CVC4::theory::arrays namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
switch (node.getKind()) {
case kind::SELECT: {
- // select(store(a,i,v),i) = v
TNode store = node[0];
- if (store.getKind() == kind::STORE &&
- store[1] == node[1]) {
- return RewriteResponse(REWRITE_DONE, store[2]);
+ if (store.getKind() == kind::STORE) {
+ // select(store(a,i,v),j)
+ Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1]));
+ if (eqRewritten.getKind() == kind::CONST_BOOLEAN) {
+ bool value = eqRewritten.getConst<bool>();
+ if (value) {
+ // select(store(a,i,v),i) = v
+ return RewriteResponse(REWRITE_DONE, store[2]);
+ }
+ else {
+ // select(store(a,i,v),j) = select(a,j) if i /= j
+ Node newNode = NodeManager::currentNM()->mkNode(kind::SELECT, store[0], node[1]);
+ return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+ }
+ }
}
break;
}
value[1] == node[1]) {
return RewriteResponse(REWRITE_DONE, store);
}
- // store(store(a,i,v),i,w) = store(a,i,w)
- if (store.getKind() == kind::STORE &&
- store[1] == node[1]) {
- Node newNode = NodeManager::currentNM()->mkNode(kind::STORE, store[0], store[1], value);
- return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+ if (store.getKind() == kind::STORE) {
+ // store(store(a,i,v),j,w)
+ Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1]));
+ if (eqRewritten.getKind() == kind::CONST_BOOLEAN) {
+ bool val = eqRewritten.getConst<bool>();
+ NodeManager* nm = NodeManager::currentNM();
+ if (val) {
+ // store(store(a,i,v),i,w) = store(a,i,w)
+ Node newNode = nm->mkNode(kind::STORE, store[0], store[1], value);
+ return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+ }
+ else if (node[1] < store[1]) {
+ // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
+ // IF i != j and j comes before i in the ordering
+ Node newNode = nm->mkNode(kind::STORE, store[0], node[1], value);
+ newNode = nm->mkNode(kind::STORE, newNode, store[1], store[2]);
+ return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+ }
+ }
}
break;
}
}
};/* struct ArrayStoreTypeRule */
+struct ArrayTableFunTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::ARR_TABLE_FUN);
+ TypeNode arrayType = n[0].getType(check);
+ if( check ) {
+ if(!arrayType.isArray()) {
+ throw TypeCheckingExceptionPrivate(n, "array table fun arg 0 is non-array");
+ }
+ TypeNode arrType2 = n[1].getType(check);
+ if(!arrayType.isArray()) {
+ throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array");
+ }
+ TypeNode indexType = n[2].getType(check);
+ if(arrayType.getArrayIndexType() != indexType) {
+ throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array");
+ }
+ indexType = n[3].getType(check);
+ if(arrayType.getArrayIndexType() != indexType) {
+ throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array");
+ }
+ }
+ return arrayType.getArrayIndexType();
+ }
+};/* struct ArrayStoreTypeRule */
+
struct CardinalityComputer {
inline static Cardinality computeCardinality(TypeNode type) {
Assert(type.getKind() == kind::ARRAY_TYPE);
}
void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
- Assert (node.getKind() == kind::VARIABLE);
+ // Assert (node.getKind() == kind::VARIABLE);
Assert(bits.size() == 0);
for (unsigned i = 0; i < utils::getSize(node); ++i) {
return;
}
+ // make sure it is marked as an atom
+ addAtom(node);
+
BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
++d_statistics.d_numAtoms;
// the bitblasted definition of the atom
}
void Bitblaster::initTermBBStrategies() {
+ // Changed this to DefaultVarBB because any foreign kind should be treated as a variable
+ // TODO: check this is OK
for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
- d_termBBStrategies[i] = UndefinedTermBBStrategy;
+ d_termBBStrategies[i] = DefaultVarBB;
}
/// setting default bb strategies for terms:
- d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB;
+ // d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB;
d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB;
d_termBBStrategies [ kind::BITVECTOR_NOT ] = DefaultNotBB;
d_termBBStrategies [ kind::BITVECTOR_CONCAT ] = DefaultConcatBB;
currently asserted by the DPLL SAT solver. */
/// helper methods
+ public:
bool hasBBAtom(TNode node);
+ private:
bool hasBBTerm(TNode node);
void getBBTerm(TNode node, Bits& bits);
Node bbOptimize(TNode node);
void bbAtom(TNode node);
+ void addAtom(TNode atom);
// division is bitblasted in terms of constraints
// so it needs to use private bitblaster interface
void bbUdiv(TNode node, Bits& bits);
bool solve(bool quick_solve = false);
void bitblast(TNode node);
void getConflict(std::vector<TNode>& conflict);
- void addAtom(TNode atom);
+
bool getPropagations(std::vector<TNode>& propagations);
void explainPropagation(TNode atom, std::vector<Node>& explanation);
private:
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/valuation.h"
-
#include "theory/bv/bv_sat.h"
+#include "theory/uf/equality_engine_impl.h"
using namespace CVC4;
using namespace CVC4::theory;
using namespace std;
using namespace CVC4::theory::bv::utils;
+
+const bool d_useEqualityEngine = true;
+const bool d_useSatPropagation = true;
+
+
TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
: Theory(THEORY_BV, c, u, out, valuation),
d_context(c),
d_assertions(c),
d_bitblaster(new Bitblaster(c) ),
d_statistics(),
- d_alreadyPropagatedSet(c)
- {
+ d_alreadyPropagatedSet(c),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
+ d_conflict(c, false),
+ d_literalsToPropagate(c),
+ d_literalsToPropagateIndex(c, 0),
+ d_toBitBlast(c)
+ {
d_true = utils::mkTrue();
+ d_false = utils::mkFalse();
+
+ if (d_useEqualityEngine) {
+ d_equalityEngine.addTerm(d_true);
+ d_equalityEngine.addTerm(d_false);
+ d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
+ d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
+ d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
+ // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
+
+ }
}
+
TheoryBV::~TheoryBV() {
delete d_bitblaster;
}
node.getKind() == kind::BITVECTOR_SLT ||
node.getKind() == kind::BITVECTOR_SLE) {
d_bitblaster->bitblast(node);
- d_bitblaster->addAtom(node);
}
+
+ if (d_useEqualityEngine) {
+ switch (node.getKind()) {
+ case kind::EQUAL:
+ // Add the terms
+ d_equalityEngine.addTerm(node);
+ // Add the trigger for equality
+ d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+ d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
+ break;
+ default:
+ d_equalityEngine.addTerm(node);
+ break;
+ }
+ }
+
}
-void TheoryBV::check(Effort e) {
- BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
+void TheoryBV::check(Effort e)
+{
+ BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
- while (!done()) {
- TNode assertion = get();
- // make sure we do not assert things we propagated
- if (!hasBeenPropagated(assertion)) {
- BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n";
- bool ok = d_bitblaster->assertToSat(assertion, true);
+ while (!done() && !d_conflict) {
+ Assertion assertion = get();
+ TNode fact = assertion.assertion;
+
+ BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
+
+ // If the assertion doesn't have a literal, it's a shared equality
+ bool shared = !assertion.isPreregistered;
+ Assert(!d_useEqualityEngine || !shared ||
+ ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
+ (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
+ d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+
+ // Notify the Equality Engine
+ switch (fact.getKind()) {
+ case kind::EQUAL:
+ if (d_useEqualityEngine) {
+ d_equalityEngine.addEquality(fact[0], fact[1], fact);
+ }
+ if (shared && !d_bitblaster->hasBBAtom(fact)) {
+ d_bitblaster->bitblast(fact);
+ }
+ break;
+ case kind::NOT:
+ if (fact[0].getKind() == kind::EQUAL) {
+ // Assert the dis-equality
+ if (d_useEqualityEngine) {
+ d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
+ }
+ if (shared && !d_bitblaster->hasBBAtom(fact[0])) {
+ d_bitblaster->bitblast(fact[0]);
+ }
+ } else {
+ if (d_useEqualityEngine) {
+ d_equalityEngine.addPredicate(fact[0], false, fact);
+ }
+ break;
+ }
+ break;
+ default:
+ if (d_useEqualityEngine) {
+ d_equalityEngine.addPredicate(fact, true, fact);
+ }
+ break;
+ }
+
+ // make sure we do not assert things we propagated
+ if (!d_conflict && d_alreadyPropagatedSet.count(fact) == 0) {
+ bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
if (!ok) {
std::vector<TNode> conflictAtoms;
d_bitblaster->getConflict(conflictAtoms);
d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
- Node conflict = mkConjunction(conflictAtoms);
- d_out->conflict(conflict);
- BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n ";
- return;
+ d_conflict = true;
+ d_conflictNode = mkConjunction(conflictAtoms);
+ break;
}
}
}
+ // If in conflict, output the conflict
+ if (d_conflict) {
+ Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
+ d_out->conflict(d_conflictNode);
+ return;
+ }
+
if (e == EFFORT_FULL) {
+
+ Assert(done() && !d_conflict);
BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
// in standard effort we only do boolean constraint propagation
bool ok = d_bitblaster->solve(false);
}
}
-bool TheoryBV::hasBeenPropagated(TNode node) {
- return d_alreadyPropagatedSet.count(node);
-}
void TheoryBV::propagate(Effort e) {
- BVDebug("bitvector") << "TheoryBV::propagate() \n";
+ BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate()" << std::endl;
+
+ if (d_conflict) {
+ return;
+ }
+
+ // get new propagations from the equality engine
+ for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+ TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
+ BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl;
+ bool satValue;
+ Node normalized = Rewriter::rewrite(literal);
+ if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
+ d_out->propagate(literal);
+ } else {
+ Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
+ Node negatedLiteral;
+ std::vector<TNode> assumptions;
+ if (normalized != d_false) {
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+ assumptions.push_back(negatedLiteral);
+ }
+ explain(literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ return;
+ }
+ }
// get new propagations from the sat solver
std::vector<TNode> propagations;
for (unsigned i = 0; i < propagations.size(); ++ i) {
TNode node = propagations[i];
BVDebug("bitvector") << "TheoryBV::propagate " << node <<" \n";
+ if (!d_valuation.isSatLiteral(node)) {
+ // TODO: maybe propagate shared terms too?
+ continue;
+ }
if (d_valuation.getSatValue(node) == Node::null()) {
vector<Node> explanation;
d_bitblaster->explainPropagation(node, explanation);
}
-Node TheoryBV::explain(TNode n) {
- BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n";
- std::vector<Node> explanation;
- d_bitblaster->explainPropagation(n, explanation);
- Node exp;
+// Node TheoryBV::explain(TNode n) {
+// BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n";
+// std::vector<Node> explanation;
+// d_bitblaster->explainPropagation(n, explanation);
+// Node exp;
- if (explanation.size() == 0) {
- return utils::mkTrue();
- }
+// if (explanation.size() == 0) {
+// return utils::mkTrue();
+// }
- exp = utils::mkAnd(explanation);
+// exp = utils::mkAnd(explanation);
- BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n";
- return exp;
-}
+// BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n";
+// return exp;
+// }
Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
switch(in.getKind()) {
}
return PP_ASSERT_STATUS_UNSOLVED;
}
+
+
+bool TheoryBV::propagate(TNode literal)
+{
+ Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl;
+
+ // If already in conflict, no more propagation
+ if (d_conflict) {
+ Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl;
+ return false;
+ }
+
+ // See if the literal has been asserted already
+ Node normalized = Rewriter::rewrite(literal);
+ bool satValue = false;
+ bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
+
+ // If asserted, we might be in conflict
+ if (isAsserted) {
+ if (!satValue) {
+ Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+ std::vector<TNode> assumptions;
+ Node negatedLiteral;
+ if (normalized != d_false) {
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+ assumptions.push_back(negatedLiteral);
+ }
+ explain(literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ return false;
+ }
+ // Propagate even if already known in SAT - could be a new equation between shared terms
+ // (terms that weren't shared when the literal was asserted!)
+ }
+
+ // Nothing, just enqueue it for propagation and mark it as asserted already
+ Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+ d_literalsToPropagate.push_back(literal);
+
+ return true;
+}/* TheoryBV::propagate(TNode) */
+
+
+void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
+ TNode lhs, rhs;
+ switch (literal.getKind()) {
+ case kind::EQUAL:
+ lhs = literal[0];
+ rhs = literal[1];
+ break;
+ case kind::NOT:
+ if (literal[0].getKind() == kind::EQUAL) {
+ // Disequalities
+ d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
+ return;
+ } else {
+ // Predicates
+ lhs = literal[0];
+ rhs = d_false;
+ break;
+ }
+ case kind::CONST_BOOLEAN:
+ // we get to explain true = false, since we set false to be the trigger of this
+ lhs = d_true;
+ rhs = d_false;
+ break;
+ default:
+ Unreachable();
+ }
+ d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
+
+
+Node TheoryBV::explain(TNode node) {
+ BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+ std::vector<TNode> assumptions;
+ explain(node, assumptions);
+ return mkAnd(assumptions);
+}
+
+
+void TheoryBV::addSharedTerm(TNode t) {
+ Debug("bitvector::sharing") << spaces(getContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
+ if (d_useEqualityEngine) {
+ d_equalityEngine.addTriggerTerm(t);
+ }
+}
+
+
+EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
+{
+ if (d_useEqualityEngine) {
+ if (d_equalityEngine.areEqual(a, b)) {
+ // The terms are implied to be equal
+ return EQUALITY_TRUE;
+ }
+ if (d_equalityEngine.areDisequal(a, b)) {
+ // The terms are implied to be dis-equal
+ return EQUALITY_FALSE;
+ }
+ }
+ return EQUALITY_UNKNOWN;
+}
+
#include "context/cdhashset.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/stats.h"
+#include "theory/uf/equality_engine.h"
+#include "context/cdqueue.h"
namespace BVMinisat {
class SimpSolver;
/// forward declarations
class Bitblaster;
+static inline std::string spaces(int level)
+{
+ std::string indentStr(level, ' ');
+ return indentStr;
+}
+
class TheoryBV : public Theory {
/** Bitblaster */
Bitblaster* d_bitblaster;
Node d_true;
-
+ Node d_false;
+
/** Context dependent set of atoms we already propagated */
context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
- bool hasBeenPropagated(TNode node);
public:
TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
void check(Effort e);
- void propagate(Effort e);
-
Node explain(TNode n);
Node getValue(TNode n);
Statistics d_statistics;
+ // Added by Clark
+ // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
+ class NotifyClass {
+ TheoryBV& d_bv;
+ public:
+ NotifyClass(TheoryBV& uf): d_bv(uf) {}
+
+ bool notify(TNode propagation) {
+ Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+ // Just forward to bv
+ return d_bv.propagate(propagation);
+ }
+
+ void notify(TNode t1, TNode t2) {
+ Debug("arrays") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+ // Propagate equality between shared terms
+ Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+ d_bv.propagate(t1.eqNode(t2));
+ }
+ };
+
+ /** The notify class for d_equalityEngine */
+ NotifyClass d_notify;
+
+ /** Equaltity engine */
+ uf::EqualityEngine<NotifyClass> d_equalityEngine;
+
+ // Are we in conflict?
+ context::CDO<bool> d_conflict;
+
+ /** The conflict node */
+ Node d_conflictNode;
+
+ /** Literals to propagate */
+ context::CDList<Node> d_literalsToPropagate;
+
+ /** Index of the next literal to propagate */
+ context::CDO<unsigned> d_literalsToPropagateIndex;
+
+ context::CDQueue<Node> d_toBitBlast;
+
+ /** Should be called to propagate the literal. */
+ bool propagate(TNode literal);
+
+ /** Explain why this literal is true by adding assumptions */
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+
+ void addSharedTerm(TNode t);
+
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+
+public:
+
+ void propagate(Effort e);
+
};/* class TheoryBV */
}/* CVC4::theory::bv namespace */
BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
TNode a = node[0];
unsigned power = utils::isPow2Const(node[1]) - 1;
+ if (power == 0) {
+ return utils::mkConst(utils::getSize(node), 0);
+ }
Node extract = utils::mkExtract(a, power - 1, 0);
Node zeros = utils::mkConst(utils::getSize(node) - power, 0);
return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract);
}
+inline Node mkAnd(const std::vector<TNode>& conjunctions) {
+ Assert(conjunctions.size() > 0);
+
+ std::set<TNode> all;
+ all.insert(conjunctions.begin(), conjunctions.end());
+
+ if (all.size() == 1) {
+ // All the same, or just one
+ return conjunctions[0];
+ }
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
+}/* mkAnd() */
+
+
// Turn a set into a string
inline std::string setToString(const std::set<TNode>& nodeSet) {
std::stringstream out;
**/
#include "theory/shared_terms_database.h"
+#include "theory/uf/equality_engine_impl.h"
using namespace CVC4;
-using namespace CVC4::theory;
+using namespace theory;
+
+SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context)
+ : ContextNotifyObj(context),
+ d_context(context),
+ d_statSharedTerms("theory::shared_terms", 0),
+ d_addedSharedTermsSize(context, 0),
+ d_termsToTheories(context),
+ d_alreadyNotifiedMap(context),
+ d_sharedNotify(notify),
+ d_termToNotifyList(context),
+ d_allocatedNLSize(0),
+ d_allocatedNLNext(context, 0),
+ d_EENotify(*this),
+ d_equalityEngine(d_EENotify, context, "SharedTermsDatabase")
+{
+ StatisticsRegistry::registerStat(&d_statSharedTerms);
+ NodeManager* nm = NodeManager::currentNM();
+ d_true = nm->mkConst<bool>(true);
+ d_false = nm->mkConst<bool>(false);
+ d_equalityEngine.addTerm(d_true);
+ d_equalityEngine.addTerm(d_false);
+ d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+}
+
+
+SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException)
+{
+ StatisticsRegistry::unregisterStat(&d_statSharedTerms);
+ for (unsigned i = 0; i < d_allocatedNLSize; ++i) {
+ d_allocatedNL[i]->deleteSelf();
+ }
+}
+
void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) {
Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl;
d_addedSharedTerms.push_back(atom);
d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
d_termsToTheories[search_pair] = theories;
+ if (!d_equalityEngine.hasTerm(term)) {
+ d_equalityEngine.addTriggerTerm(term);
+ }
} else {
Assert(theories != (*find).second);
d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second);
return Theory::setDifference((*find).second, alreadyNotified);
}
+
Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const {
// Get the theories that were already notified
AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
}
}
+
+SharedTermsDatabase::NotifyList* SharedTermsDatabase::getNewNotifyList()
+{
+ NotifyList* retval;
+ if (d_allocatedNLSize == d_allocatedNLNext) {
+ retval = new (true) NotifyList(d_context);
+ d_allocatedNL.push_back(retval);
+ d_allocatedNLNext = ++d_allocatedNLSize;
+ }
+ else {
+ retval = d_allocatedNL[d_allocatedNLNext];
+ d_allocatedNLNext = d_allocatedNLNext + 1;
+ }
+ Assert(retval->empty());
+ return retval;
+}
+
+
+void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b)
+{
+ // Note: a is the new representative
+
+ NotifyList* pnlLeft = NULL;
+ NotifyList* pnlRight = NULL;
+
+ TermToNotifyList::iterator it = d_termToNotifyList.find(a);
+ if (it == d_termToNotifyList.end()) {
+ pnlLeft = getNewNotifyList();
+ d_termToNotifyList[a] = pnlLeft;
+ }
+ else {
+ pnlLeft = (*it).second;
+ }
+ it = d_termToNotifyList.find(b);
+ if (it != d_termToNotifyList.end()) {
+ pnlRight = (*it).second;
+ }
+
+ // Get theories interested in EC for lhs
+ Theory::Set lhsSet = getNotifiedTheories(a);
+ Theory::Set rhsSet = getNotifiedTheories(b);
+ NotifyList::iterator nit;
+ TNode left, right;
+
+ for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
+
+ if (Theory::setContains(currentTheory, rhsSet)) {
+ right = b;
+ }
+ else if (pnlRight != NULL &&
+ ((nit = pnlRight->end()) != pnlRight->end())) {
+ right = (*nit).second;
+ }
+ else {
+ // no match for right: continue
+ continue;
+ }
+
+ if (Theory::setContains(currentTheory, lhsSet)) {
+ left = a;
+ }
+ else if ((nit = pnlLeft->find(currentTheory)) != pnlLeft->end()) {
+ left = (*nit).second;
+ }
+ else {
+ // no match for left: insert right into left
+ (*pnlLeft)[currentTheory] = right;
+ continue;
+ }
+
+ // New shared equality: notify the client
+
+ // TODO: add propagation of disequalities?
+
+ // Normalize the equality
+ Node equality = left.eqNode(right);
+ Node normalized = Rewriter::rewriteEquality(currentTheory, equality);
+ if (normalized.getKind() != kind::CONST_BOOLEAN) {
+ // Notify client
+ d_sharedNotify.notify(normalized, equality, currentTheory);
+ } else {
+ Assert(equality.getConst<bool>());
+ }
+ }
+
+}
+
+
void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) {
- d_alreadyNotifiedMap[term] = Theory::setUnion(theories, d_alreadyNotifiedMap[term]);
+ Theory::Set alreadyNotified = d_alreadyNotifiedMap[term];
+ Theory::Set newlyNotified = Theory::setDifference(theories, alreadyNotified);
+ if (newlyNotified != 0) {
+ TNode rep = d_equalityEngine.getRepresentative(term);
+ if (rep != term) {
+ TermToNotifyList::iterator it = d_termToNotifyList.find(rep);
+ Assert(it != d_termToNotifyList.end());
+ NotifyList* pnl = (*it).second;
+ for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) {
+ if (Theory::setContains(theory, newlyNotified) &&
+ pnl->find(theory) == pnl->end()) {
+ (*pnl)[theory] = term;
+ }
+ }
+ }
+ }
+ d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified);
+}
+
+
+bool SharedTermsDatabase::areEqual(TNode a, TNode b) {
+ return d_equalityEngine.areEqual(a,b);
+}
+
+
+bool SharedTermsDatabase::areDisequal(TNode a, TNode b) {
+ return d_equalityEngine.areDisequal(a,b);
+}
+
+
+void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason)
+{
+ bool negated = literal.getKind() == kind::NOT;
+ TNode atom = negated ? literal[0] : literal;
+ if (negated) {
+ Assert(!d_equalityEngine.areDisequal(atom[0], atom[1]));
+ d_equalityEngine.addDisequality(atom[0], atom[1], reason);
+ }
+ else {
+ Assert(!d_equalityEngine.areEqual(atom[0], atom[1]));
+ d_equalityEngine.addEquality(atom[0], atom[1], reason);
+ }
}
+
+static Node mkAnd(const std::vector<TNode>& conjunctions) {
+ Assert(conjunctions.size() > 0);
+
+ std::set<TNode> all;
+ all.insert(conjunctions.begin(), conjunctions.end());
+
+ if (all.size() == 1) {
+ // All the same, or just one
+ return conjunctions[0];
+ }
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
+}/* mkAnd() */
+
+
+Node SharedTermsDatabase::explain(TNode literal)
+{
+ std::vector<TNode> assumptions;
+ explain(literal, assumptions);
+ return mkAnd(assumptions);
+}
+
+
+void SharedTermsDatabase::explain(TNode literal, std::vector<TNode>& assumptions) {
+ TNode lhs, rhs;
+ switch (literal.getKind()) {
+ case kind::EQUAL:
+ lhs = literal[0];
+ rhs = literal[1];
+ break;
+ case kind::NOT:
+ if (literal[0].getKind() == kind::EQUAL) {
+ // Disequalities
+ d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
+ return;
+ }
+ case kind::CONST_BOOLEAN:
+ // we get to explain true = false, since we set false to be the trigger of this
+ lhs = d_true;
+ rhs = d_false;
+ break;
+ default:
+ Unreachable();
+ }
+ d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
#include "theory/theory.h"
#include "context/context.h"
#include "util/stats.h"
+#include "theory/uf/equality_engine.h"
namespace CVC4 {
private:
+ Node d_true;
+
+ Node d_false;
+
/** The context */
context::Context* d_context;
/** Map from term to theories that have already been notified about the shared term */
AlreadyNotifiedMap d_alreadyNotifiedMap;
+public:
+ /** Class for notifications about new shared term equalities */
+ class SharedTermsNotifyClass {
+ public:
+ SharedTermsNotifyClass() {}
+ virtual ~SharedTermsNotifyClass() {}
+ virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0;
+ };
+
+private:
+ // Instance of class to send shared term notifications to
+ SharedTermsNotifyClass& d_sharedNotify;
+
+ // Type for list of theory, node pairs: theory is theory to be notified,
+ // node is the representative for this equivalence class known to the
+ // theory that will be notified
+ typedef context::CDHashMap<theory::TheoryId, TNode, __gnu_cxx::hash<unsigned> > NotifyList;
+ typedef context::CDHashMap<TNode, NotifyList*, TNodeHashFunction> TermToNotifyList;
+
+ // Map from terms (only valid for reps) to their notify lists
+ // Note that theory, term pairs only need to be in the notify list if the
+ // representative term is not a valid shared term for the theory.
+ TermToNotifyList d_termToNotifyList;
+
+ // List of allocated NotifyList* objects
+ std::vector<NotifyList*> d_allocatedNL;
+
+ // Total number of allocated NotifyList* objects
+ unsigned d_allocatedNLSize;
+
+ // Size of portion of d_allocatedNL that is currently in use
+ context::CDO<unsigned> d_allocatedNLNext;
+
/** This method removes all the un-necessary stuff from the maps */
void backtrack();
-public:
+ // EENotifyClass: template helper class for d_equalityEngine - handles call-backs
+ class EENotifyClass {
+ SharedTermsDatabase& d_sharedTerms;
+ public:
+ EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
+ bool notify(TNode propagation) { return true; } // Not used
+ void notify(TNode t1, TNode t2) {
+ d_sharedTerms.mergeSharedTerms(t1, t2);
+ }
+ };
- SharedTermsDatabase(context::Context* context)
- : ContextNotifyObj(context),
- d_context(context),
- d_statSharedTerms("theory::shared_terms", 0),
- d_addedSharedTermsSize(context, 0),
- d_termsToTheories(context),
- d_alreadyNotifiedMap(context)
- {
- StatisticsRegistry::registerStat(&d_statSharedTerms);
- }
+ /** The notify class for d_equalityEngine */
+ EENotifyClass d_EENotify;
- ~SharedTermsDatabase() throw(AssertionException)
- {
- StatisticsRegistry::unregisterStat(&d_statSharedTerms);
- }
+ /** Equaltity engine */
+ theory::uf::EqualityEngine<EENotifyClass> d_equalityEngine;
+
+ /** Attach a new notify list to an equivalence class representative */
+ NotifyList* getNewNotifyList();
+
+ /** Method called by equalityEngine when a becomes equal to b */
+ void mergeSharedTerms(TNode a, TNode b);
+
+ /** Internal explanation method */
+ void explain(TNode literal, std::vector<TNode>& assumptions);
+
+public:
+
+ SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context);
+ ~SharedTermsDatabase() throw(AssertionException);
/**
* Add a shared term to the database. The shared term is a subterm of the atom and
*/
void markNotified(TNode term, theory::Theory::Set theories);
+ bool isShared(TNode term) const {
+ return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
+ }
+
+ bool areEqual(TNode a, TNode b);
+
+ bool areDisequal(TNode a, TNode b);
+
+ void processSharedLiteral(TNode literal, TNode reason);
+
+ Node explain(TNode literal);
+
/**
* This method gets called on backtracks from the context manager.
*/
// We don't care about the terms of different types
continue;
}
- switch (getEqualityStatus(a, b)) {
+ switch (d_valuation.getEqualityStatus(a, b)) {
case EQUALITY_TRUE_AND_PROPAGATED:
case EQUALITY_FALSE_AND_PROPAGATED:
// If we know about it, we should have propagated it, so we can skip
id = kindToTheoryId(typeNode.getKind());
}
if (id == THEORY_BUILTIN) {
- Trace("theory") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
+ Trace("theory::internal") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
return s_uninterpretedSortOwner;
}
return id;
/** a - b */
static inline Set setDifference(Set a, Set b) {
- return ((~b) & AllTheories) & a;
+ return (~b) & a;
}
static inline std::string setToString(theory::Theory::Set theorySet) {
d_context(context),
d_userContext(userContext),
d_activeTheories(context, 0),
- d_sharedTerms(context),
- d_atomPreprocessingCache(),
+ d_notify(*this),
+ d_sharedTerms(d_notify, context),
+ d_ppCache(),
d_possiblePropagations(),
d_hasPropagated(context),
d_inConflict(context, false),
d_sharedTermsExist(context, false),
d_hasShutDown(false),
d_incomplete(context, false),
- d_sharedAssertions(context),
+ d_sharedLiteralsIn(context),
+ d_assertedLiteralsOut(context),
d_propagatedLiterals(context),
d_propagatedLiteralsIndex(context, 0),
d_decisionRequests(context),
// Do the checking
try {
- // Clear any leftover propagated equalities
- d_propagatedEqualities.clear();
+ // Clear any leftover propagated shared literals
+ d_propagatedSharedLiterals.clear();
// Mark the output channel unused (if this is FULL_EFFORT, and nothing
// is done by the theories, no additional check will be needed)
// We are still satisfiable, propagate as much as possible
propagate(effort);
- // If we have any propagated equalities, we enqueue them to the theories and re-check
- if (d_propagatedEqualities.size() > 0) {
- Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl;
- assertSharedEqualities();
+ // If we have any propagated shared literals, we enqueue them to the theories and re-check
+ if (d_propagatedSharedLiterals.size() > 0) {
+ Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl;
+ outputSharedLiterals();
continue;
}
// Do the combination
Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl;
combineTheories();
- // If we have any propagated equalities, we enqueue them to the theories and re-check
- if (d_propagatedEqualities.size() > 0) {
- Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl;
- assertSharedEqualities();
+ // If we have any propagated shared literals, we enqueue them to the theories and re-check
+ if (d_propagatedSharedLiterals.size() > 0) {
+ Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl;
+ outputSharedLiterals();
} else {
- // No propagated equalities, we're either sat, or there are lemmas added
+ // No propagated shared literals, we're either sat, or there are lemmas added
break;
}
} else {
}
}
- // Clear any leftover propagated equalities
- d_propagatedEqualities.clear();
+ // Clear any leftover propagated shared literals
+ d_propagatedSharedLiterals.clear();
Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl;
}
}
-void TheoryEngine::assertSharedEqualities() {
- // Assert all the shared equalities
- for (unsigned i = 0; i < d_propagatedEqualities.size(); ++ i) {
- const SharedEquality& eq = d_propagatedEqualities[i];
+void TheoryEngine::outputSharedLiterals() {
+ // Assert all the shared literals
+ for (unsigned i = 0; i < d_propagatedSharedLiterals.size(); ++ i) {
+ const SharedLiteral& eq = d_propagatedSharedLiterals[i];
// Check if the theory already got this one
- if (d_sharedAssertions.find(eq.toAssert) == d_sharedAssertions.end()) {
- Debug("sharing") << "TheoryEngine::assertSharedEqualities(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl;
- Debug("sharing") << "TheoryEngine::assertSharedEqualities(): orignal " << eq.toExplain.node << " from " << eq.toExplain.theory << std::endl;
- d_sharedAssertions[eq.toAssert] = eq.toExplain;
+ if (d_assertedLiteralsOut.find(eq.toAssert) == d_assertedLiteralsOut.end()) {
+ Debug("sharing") << "TheoryEngine::outputSharedLiterals(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl;
+ Debug("sharing") << "TheoryEngine::outputSharedLiterals(): orignal " << eq.toExplain << std::endl;
+ d_assertedLiteralsOut[eq.toAssert] = eq.toExplain;
if (eq.toAssert.theory == theory::THEORY_LAST) {
d_propagatedLiterals.push_back(eq.toAssert.node);
} else {
}
}
// Clear the equalities
- d_propagatedEqualities.clear();
+ d_propagatedSharedLiterals.clear();
}
Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl;
+ if (d_sharedTerms.areEqual(carePair.a, carePair.b) ||
+ d_sharedTerms.areDisequal(carePair.a, carePair.b)) {
+ continue;
+ }
+
+ if (carePair.a.isConst() && carePair.b.isConst()) {
+ // TODO: equality engine should auto-detect these as disequal
+ d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), NodeManager::currentNM()->mkConst<bool>(true));
+ continue;
+ }
+
Node equality = carePair.a.eqNode(carePair.b);
Node normalizedEquality = Rewriter::rewrite(equality);
bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN;
-
- // If the node has a literal, it has been asserted so we should just check it
bool value;
if (isTrivial || (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value))) {
+ // Missed propagation!
Debug("sharing") << "TheoryEngine::combineTheories(): has a literal or is trivial" << std::endl;
-
+
if (isTrivial) {
- // if the equality is trivial, we assert it back to the theory saying the sat solver should explain
value = normalizedEquality.getConst<bool>();
+ normalizedEquality = NodeManager::currentNM()->mkConst<bool>(true);
}
-
- // Normalize the equality to the theory that requested it
- Node toAssert = Rewriter::rewriteEquality(carePair.theory, equality);
-
- if (value) {
- SharedEquality sharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory);
- if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) {
- d_propagatedEqualities.push_back(sharedEquality);
- }
- } else {
- SharedEquality sharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory);
- if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) {
- d_propagatedEqualities.push_back(sharedEquality);
- }
+ else {
+ d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST;
+ if (!value) normalizedEquality = normalizedEquality.notNode();
}
- } else {
- Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
-
- // There is no value, so we need to split on it
- lemma(equality.orNode(equality.notNode()), false, false);
+ if (!value) {
+ equality = equality.notNode();
+ }
+ d_sharedTerms.processSharedLiteral(equality, normalizedEquality);
+ continue;
}
+
+ // There is no value, so we need to split on it
+ Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
+ lemma(equality.orNode(equality.notNode()), false, false);
+
}
}
return solveStatus;
}
+// Recursively traverse a term and call the theory rewriter on its sub-terms
+Node TheoryEngine::ppTheoryRewrite(TNode term)
+{
+ NodeMap::iterator find = d_ppCache.find(term);
+ if (find != d_ppCache.end()) {
+ return (*find).second;
+ }
+ unsigned nc = term.getNumChildren();
+ if (nc == 0) {
+ return theoryOf(term)->ppRewrite(term);
+ }
+ Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
+ NodeBuilder<> newNode(term.getKind());
+ if (term.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newNode << term.getOperator();
+ }
+ unsigned i;
+ for (i = 0; i < nc; ++i) {
+ newNode << ppTheoryRewrite(term[i]);
+ }
+ Node newTerm = Rewriter::rewrite(newNode);
+ Node newTerm2 = theoryOf(newTerm)->ppRewrite(newTerm);
+ if (newTerm != newTerm2) {
+ newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
+ }
+ d_ppCache[term] = newTerm;
+ Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm << "}" << endl;
+ return newTerm;
+}
+
+
+void TheoryEngine::preprocessStart()
+{
+ d_ppCache.clear();
+}
+
+
struct preprocess_stack_element {
TNode node;
bool children_added;
Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << endl;
// If node already in the cache we're done, pop from the stack
- NodeMap::iterator find = d_atomPreprocessingCache.find(current);
- if (find != d_atomPreprocessingCache.end()) {
+ NodeMap::iterator find = d_ppCache.find(current);
+ if (find != d_ppCache.end()) {
toVisit.pop_back();
continue;
}
- // If this is an atom, we preprocess it with the theory
+ // If this is an atom, we preprocess its terms with the theory ppRewriter
if (Theory::theoryOf(current) != THEORY_BOOL) {
- d_atomPreprocessingCache[current] = theoryOf(current)->ppRewrite(current);
+ d_ppCache[current] = ppTheoryRewrite(current);
continue;
}
builder << current.getOperator();
}
for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
- Assert(d_atomPreprocessingCache.find(current[i]) != d_atomPreprocessingCache.end());
- builder << d_atomPreprocessingCache[current[i]];
+ Assert(d_ppCache.find(current[i]) != d_ppCache.end());
+ builder << d_ppCache[current[i]];
}
// Mark the substitution and continue
Node result = builder;
Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl;
- d_atomPreprocessingCache[current] = result;
+ d_ppCache[current] = result;
toVisit.pop_back();
} else {
// Mark that we have added the children if any
// We need to add the children
for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
TNode childNode = *child_it;
- NodeMap::iterator childFind = d_atomPreprocessingCache.find(childNode);
- if (childFind == d_atomPreprocessingCache.end()) {
+ NodeMap::iterator childFind = d_ppCache.find(childNode);
+ if (childFind == d_ppCache.end()) {
toVisit.push_back(childNode);
}
}
} else {
// No children, so we're done
Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << endl;
- d_atomPreprocessingCache[current] = current;
+ d_ppCache[current] = current;
toVisit.pop_back();
}
}
}
// Return the substituted version
- return d_atomPreprocessingCache[assertion];
+ return d_ppCache[assertion];
}
void TheoryEngine::assertFact(TNode node)
{
Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
+ Trace("theory::assertFact") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
d_propEngine->checkTime();
// Get the atom
- TNode atom = node.getKind() == kind::NOT ? node[0] : node;
-
- // Assert the fact to the appropriate theory and mark it active
+ bool negated = node.getKind() == kind::NOT;
+ TNode atom = negated ? node[0] : node;
Theory* theory = theoryOf(atom);
- theory->assertFact(node, true);
- markActive(Theory::setInsert(theory->getId()));
- // If any shared terms, notify the theories
- if (d_sharedTerms.hasSharedTerms(atom)) {
- SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
- SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
- for (; it != it_end; ++ it) {
- TNode term = *it;
- Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
- for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) {
- if (Theory::setContains(theory, theories)) {
- theoryOf(theory)->addSharedTermInternal(term);
+ //TODO: there is probably a bug here if shared terms start to exist after some asseritons have been processed
+ if (d_sharedTermsExist) {
+
+ // If any shared terms, notify the theories
+ if (d_sharedTerms.hasSharedTerms(atom)) {
+ SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
+ SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
+ for (; it != it_end; ++ it) {
+ TNode term = *it;
+ Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
+ for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
+ if (Theory::setContains(id, theories)) {
+ theoryOf(id)->addSharedTermInternal(term);
+ }
}
+ d_sharedTerms.markNotified(term, theories);
+ markActive(theories);
+ }
+ }
+
+ if (atom.getKind() == kind::EQUAL &&
+ d_sharedTerms.isShared(atom[0]) &&
+ d_sharedTerms.isShared(atom[1])) {
+ Debug("sharing") << "TheoryEngine::assertFact: asserting shared node: " << node << std::endl;
+ // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain
+ if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) ||
+ ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) {
+ Debug("sharing") << "TheoryEngine::assertFact: sharedLiteral already known(" << node << ")" << std::endl;
+ return;
+ }
+ d_sharedLiteralsIn[node] = THEORY_LAST;
+ d_sharedTerms.processSharedLiteral(node, node);
+ if (d_propagatedSharedLiterals.size() > 0) {
+ Debug("theory") << "TheoryEngine::assertFact: distributing shared literals" << std::endl;
+ outputSharedLiterals();
+ }
+ // TODO: have processSharedLiteral propagate disequalities?
+ if (node.getKind() == kind::EQUAL) {
+ // Don't have to assert it - this will be taken care of by processSharedLiteral
+ Assert(isActive(theory->getId()));
+ return;
}
- d_sharedTerms.markNotified(term, theories);
- markActive(theories);
+ }
+ // If theory didn't already get this literal, add to the map
+ NodeTheoryPair ntp(node, theory->getId());
+ if (d_assertedLiteralsOut.find(ntp) == d_assertedLiteralsOut.end()) {
+ d_assertedLiteralsOut[ntp] = Node();
}
}
+
+ // Assert the fact to the appropriate theory and mark it active
+ theory->assertFact(node, true);
+ markActive(Theory::setInsert(theory->getId()));
}
void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
- Debug("theory") << "EngineOutputChannel::propagate(" << literal << ", " << theory << ")" << std::endl;
+ Debug("theory") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << std::endl;
d_propEngine->checkTime();
d_hasPropagated.insert(literal);
}
- TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+ bool negated = (literal.getKind() == kind::NOT);
+ TNode atom = negated ? literal[0] : literal;
+ bool value;
- if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL) {
- // If not an equality it must be a SAT literal so we enlist it, and it can only
- // be propagated by the theory that owns it, as it is the only one that got
- // a preregister call with it.
+ if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL ||
+ !d_sharedTerms.isShared(atom[0]) || !d_sharedTerms.isShared(atom[1])) {
+ // If not an equality or if an equality between terms that are not both shared,
+ // it must be a SAT literal so we enqueue it
Assert(d_propEngine->isSatLiteral(literal));
- d_propagatedLiterals.push_back(literal);
+ if (d_propEngine->hasValue(literal, value)) {
+ // if we are propagting something that already has a sat value we better be the same
+ Debug("theory") << "literal " << literal << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
+ Assert(value);
+ } else {
+ d_propagatedLiterals.push_back(literal);
+ }
} else {
- // Otherwise it might be a shared-term (dis-)equality
+ // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain
+ if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) ||
+ ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) {
+ Debug("sharing") << "TheoryEngine::propagate: sharedLiteral already known(" << literal << ")" << std::endl;
+ return;
+ }
+
+ // Otherwise it is a shared-term (dis-)equality
Node normalizedLiteral = Rewriter::rewrite(literal);
if (d_propEngine->isSatLiteral(normalizedLiteral)) {
- // If there is a literal, just enqueue it, same as above
- bool value;
+ // If there is a literal, propagate it to SAT
if (d_propEngine->hasValue(normalizedLiteral, value)) {
// if we are propagting something that already has a sat value we better be the same
- Debug("theory") << "literal " << literal << " (" << normalizedLiteral << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
+ Debug("theory") << "literal " << literal << ", normalized = " << normalizedLiteral << ", propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
Assert(value);
} else {
- SharedEquality sharedEquality(normalizedLiteral, literal, theory, theory::THEORY_LAST);
- d_propagatedEqualities.push_back(sharedEquality);
- }
- }
- // Otherwise, we assert it to all interested theories
- Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(atom[0]);
- Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(atom[1]);
- // Now notify the theories
- if (Theory::setIntersection(lhsNotified, rhsNotified) != 0) {
- bool negated = literal.getKind() == kind::NOT;
- for (TheoryId currentTheory = theory::THEORY_FIRST; currentTheory != theory::THEORY_LAST; ++ currentTheory) {
- if (currentTheory == theory) {
- // Don't reassert to the same theory
- continue;
- }
- // Assert if theory is interested in both terms
- if (Theory::setContains(currentTheory, lhsNotified) && Theory::setContains(currentTheory, rhsNotified)) {
- // Normalize the equality
- Node equality = Rewriter::rewriteEquality(currentTheory, atom);
- if (equality.getKind() != kind::CONST_BOOLEAN) {
- // The assertion
- Node assertion = negated ? equality.notNode() : equality;
- // Remember it to assert later
- d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory));
- } else {
- Assert(negated || equality.getConst<bool>());
- }
- }
+ SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST);
+ d_propagatedSharedLiterals.push_back(sharedLiteral);
}
}
+ // Assert to interested theories
+ Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl;
+ d_sharedLiteralsIn[literal] = theory;
+ d_sharedTerms.processSharedLiteral(literal, literal);
}
}
+
void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) {
Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl;
theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
Assert(a.getType() == b.getType());
+ if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {
+ if (d_sharedTerms.areEqual(a,b)) {
+ return EQUALITY_TRUE_AND_PROPAGATED;
+ }
+ else if (d_sharedTerms.areDisequal(a,b)) {
+ return EQUALITY_FALSE_AND_PROPAGATED;
+ }
+ }
return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
}
Theory* theory;
//This is true if atom is a shared assertion
- bool sharedAssertion = false;
+ bool sharedLiteral = false;
- SharedAssertionsMap::iterator find;
+ AssertedLiteralsOutMap::iterator find;
// "find" will have a value when sharedAssertion is true
if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) {
- find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST));
- sharedAssertion = (find != d_sharedAssertions.end());
+ find = d_assertedLiteralsOut.find(NodeTheoryPair(node, theory::THEORY_LAST));
+ sharedLiteral = (find != d_assertedLiteralsOut.end());
}
// Get the explanation
- if(sharedAssertion){
- theory = theoryOf((*find).second.theory);
- explanation = theory->explain((*find).second.node);
+ if(sharedLiteral) {
+ explanation = explain(ExplainTask((*find).second, SHARED_LITERAL_OUT));
} else {
theory = theoryOf(atom);
explanation = theory->explain(node);
- }
- // Explain any shared equalities that might be in the explanation
- if (d_sharedTermsExist) {
- NodeBuilder<> nb(kind::AND);
- explainEqualities(theory->getId(), explanation, nb);
- explanation = nb;
+ // Explain any shared equalities that might be in the explanation
+ if (d_sharedTermsExist) {
+ explanation = explain(ExplainTask(explanation, THEORY_EXPLANATION, theory->getId()));
+ }
}
Assert(!explanation.isNull());
return explanation;
}
+Node TheoryEngine::explain(ExplainTask toExplain)
+{
+ Debug("theory") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl;
+
+ std::set<TNode> satAssertions;
+ std::deque<ExplainTask> explainQueue;
+ // TODO: benchmark whether this helps
+ std::hash_set<ExplainTask, ExplainTaskHashFunction> explained;
+ bool value;
+
+ // No need to explain "true"
+ explained.insert(ExplainTask(NodeManager::currentNM()->mkConst<bool>(true), SHARED_DATABASE_EXPLANATION));
+
+ while (true) {
+
+ Debug("theory-explain") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl;
+
+ if (explained.find(toExplain) == explained.end()) {
+
+ explained.insert(toExplain);
+
+ if (toExplain.node.getKind() == kind::AND) {
+ for (unsigned i = 0, i_end = toExplain.node.getNumChildren(); i != i_end; ++ i) {
+ explainQueue.push_back(ExplainTask(toExplain.node[i], toExplain.kind, toExplain.theory));
+ }
+ }
+ else {
+
+ switch (toExplain.kind) {
+
+ // toExplain.node contains a shared literal sent out from theory engine (before being rewritten)
+ case SHARED_LITERAL_OUT: {
+ // Shortcut - see if this came directly from a theory
+ SharedLiteralsInMap::iterator it = d_sharedLiteralsIn.find(toExplain.node);
+ if (it != d_sharedLiteralsIn.end()) {
+ TheoryId id = (*it).second;
+ if (id == theory::THEORY_LAST) {
+ Assert(d_propEngine->isSatLiteral(toExplain.node));
+ Assert(d_propEngine->hasValue(toExplain.node, value) && value);
+ satAssertions.insert(toExplain.node);
+ break;
+ }
+ explainQueue.push_back(ExplainTask(theoryOf((*it).second)->explain(toExplain.node), THEORY_EXPLANATION, (*it).second));
+ }
+ // Otherwise, get explanation from shared terms database
+ else {
+ explainQueue.push_back(ExplainTask(d_sharedTerms.explain(toExplain.node), SHARED_DATABASE_EXPLANATION));
+ }
+ break;
+ }
+
+ // toExplain.node contains explanation from theory, toExplain.theory contains theory that produced explanation
+ case THEORY_EXPLANATION: {
+ AssertedLiteralsOutMap::iterator find = d_assertedLiteralsOut.find(NodeTheoryPair(toExplain.node, toExplain.theory));
+ if (find == d_assertedLiteralsOut.end() || (*find).second.isNull()) {
+ Assert(d_propEngine->isSatLiteral(toExplain.node));
+ Assert(d_propEngine->hasValue(toExplain.node, value) && value);
+ satAssertions.insert(toExplain.node);
+ }
+ else {
+ explainQueue.push_back(ExplainTask((*find).second, SHARED_LITERAL_OUT));
+ }
+ break;
+ }
+
+ // toExplain.node contains an explanation from the shared terms database
+ // Each literal in the explanation should be in the d_sharedLiteralsIn map
+ case SHARED_DATABASE_EXPLANATION: {
+ Assert(d_sharedLiteralsIn.find(toExplain.node) != d_sharedLiteralsIn.end());
+ TheoryId id = d_sharedLiteralsIn[toExplain.node];
+ if (id == theory::THEORY_LAST) {
+ Assert(d_propEngine->isSatLiteral(toExplain.node));
+ Assert(d_propEngine->hasValue(toExplain.node, value) && value);
+ satAssertions.insert(toExplain.node);
+ }
+ else {
+ explainQueue.push_back(ExplainTask(theoryOf(id)->explain(toExplain.node), THEORY_EXPLANATION, id));
+ }
+ break;
+ }
+ default:
+ Unreachable();
+ }
+ }
+ }
+
+ if (explainQueue.empty()) break;
+
+ toExplain = explainQueue.front();
+ explainQueue.pop_front();
+ }
+
+ Assert(satAssertions.size() > 0);
+ if (satAssertions.size() == 1) {
+ return *(satAssertions.begin());
+ }
+
+ // Now build the explanation
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = satAssertions.begin();
+ std::set<TNode>::const_iterator it_end = satAssertions.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+ return conjunction;
+}
+
void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
// Mark that we are in conflict
if (d_sharedTermsExist) {
// In the multiple-theories case, we need to reconstruct the conflict
- NodeBuilder<> nb(kind::AND);
- explainEqualities(theoryId, conflict, nb);
- Node fullConflict = nb;
+ Node fullConflict = explain(ExplainTask(conflict, THEORY_EXPLANATION, theoryId));
Assert(properConflict(fullConflict));
Debug("theory") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): " << fullConflict << std::endl;
lemma(fullConflict, true, false);
lemma(conflict, true, false);
}
}
-
-void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuilder<>& builder) {
- Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl;
- if (literals.getKind() == kind::AND) {
- for (unsigned i = 0, i_end = literals.getNumChildren(); i != i_end; ++ i) {
- TNode literal = literals[i];
- TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
- if (atom.getKind() == kind::EQUAL) {
- explainEquality(theoryId, literal, builder);
- } else if(literal.getKind() == kind::AND){
- explainEqualities(theoryId, literal, builder);
- } else {
- builder << literal;
- }
- }
- } else {
- TNode atom = literals.getKind() == kind::NOT ? literals[0] : literals;
- if (atom.getKind() == kind::EQUAL) {
- explainEquality(theoryId, literals, builder);
- } else {
- builder << literals;
- }
- }
-}
-
-void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder) {
- Assert(eqLiteral.getKind() == kind::EQUAL || (eqLiteral.getKind() == kind::NOT && eqLiteral[0].getKind() == kind::EQUAL));
-
- SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(eqLiteral, theoryId));
- if (find == d_sharedAssertions.end()) {
- // Not a shared assertion, just add it since it must be SAT literal
- builder << Rewriter::rewrite(eqLiteral);
- } else {
- TheoryId explainingTheory = (*find).second.theory;
- if (explainingTheory == theory::THEORY_LAST) {
- // If the theory is from the SAT solver, just take the normalized one
- builder << (*find).second.node;
- } else {
- // Explain it using the theory that propagated it
- Node explanation = theoryOf(explainingTheory)->explain((*find).second.node);
- explainEqualities(explainingTheory, explanation, builder);
- }
- }
-}
*/
context::CDO<theory::Theory::Set> d_activeTheories;
+ // NotifyClass: template helper class for Shared Terms Database
+ class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass {
+ TheoryEngine& d_theoryEngine;
+ public:
+ NotifyClass(TheoryEngine& engine): d_theoryEngine(engine) {}
+ ~NotifyClass() {}
+
+ void notify(TNode literal, TNode original, theory::TheoryId theory) {
+ d_theoryEngine.propagateSharedLiteral(literal, original, theory);
+ }
+ };
+
+ // Instance of NotifyClass
+ NotifyClass d_notify;
+
/**
* The database of shared terms.
*/
typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
/**
- * Cache from proprocessing of atoms.
+ * Cache for theory-preprocessing of assertions
*/
- NodeMap d_atomPreprocessingCache;
+ NodeMap d_ppCache;
/**
* Used for "missed-t-propagations" dumping mode only. A set of all
return theory::Theory::setContains(theory, d_activeTheories);
}
- struct SharedEquality {
+ struct SharedLiteral {
/** The node/theory pair for the assertion */
+ /** THEORY_LAST indicates this is a SAT literal and should be sent to the SAT solver */
NodeTheoryPair toAssert;
- /** This is the node/theory pair that we will use to explain it */
- NodeTheoryPair toExplain;
+ /** This is the node that we will use to explain it */
+ Node toExplain;
- SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory)
+ SharedLiteral(TNode assertion, TNode original, theory::TheoryId receivingTheory)
: toAssert(assertion, receivingTheory),
- toExplain(original, sendingTheory)
+ toExplain(original)
{ }
- };/* struct SharedEquality */
+ };/* struct SharedLiteral */
/**
- * Map from equalities asserted to a theory, to the theory that can explain them.
+ * Map from nodes to theories.
*/
- typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap;
+ typedef context::CDHashMap<Node, theory::TheoryId, NodeHashFunction> SharedLiteralsInMap;
/**
- * A map from asserted facts to where they came from (for explanations).
+ * All shared literals asserted to theory engine.
+ * Maps from literal to the theory that sent the literal (THEORY_LAST means sent from SAT).
*/
- SharedAssertionsMap d_sharedAssertions;
+ SharedLiteralsInMap d_sharedLiteralsIn;
/**
- * Assert a shared equalities propagated by theories.
+ * Map from literals asserted by theory engine to literal that can explain
*/
- void assertSharedEqualities();
+ typedef context::CDHashMap<NodeTheoryPair, Node, NodeTheoryPairHashFunction> AssertedLiteralsOutMap;
+
+ /**
+ * All literals asserted to theories from theory engine.
+ * Maps from literal/theory pair to literal that can explain this assertion.
+ */
+ AssertedLiteralsOutMap d_assertedLiteralsOut;
+
+ /**
+ * Shared literals queud up to be asserted to the individual theories.
+ */
+ std::vector<SharedLiteral> d_propagatedSharedLiterals;
+
+ void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory)
+ {
+ d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
+ }
+
+ /**
+ * Assert the shared literals that are queued up to the theories.
+ */
+ void outputSharedLiterals();
/**
* Literals that are propagated by the theory. Note that these are TNodes.
*/
context::CDO<unsigned> d_propagatedLiteralsIndex;
- /**
- * Shared term equalities that should be asserted to the individual theories.
- */
- std::vector<SharedEquality> d_propagatedEqualities;
-
/**
* Decisions that are requested via propagateAsDecision(). The theory
* can only request decisions on nodes that have an assigned litearl in
return d_propEngine;
}
+private:
+
+ /**
+ * Helper for preprocess
+ */
+ Node ppTheoryRewrite(TNode term);
+
+public:
+
+ /**
+ * Signal the start of a new round of assertion preprocessing
+ */
+ void preprocessStart();
+
/**
* Runs theory specific preprocesssing on the non-Boolean parts of
* the formula. This is only called on input assertions, after ITEs
*/
void preRegister(TNode preprocessed);
- /**
- * Call the theories to perform one last rewrite on the theory atoms
- * if they wish. This last rewrite is only performed on the input atoms.
- * At this point it is ensured that atoms do not contain any Boolean
- * strucure, i.e. there is no ITE nodes in them.
- *
- */
- Node preCheckRewrite(TNode node);
-
/**
* Assert the formula to the appropriate theory.
* @param node the assertion
void getPropagatedLiterals(std::vector<TNode>& literals) {
for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) {
+ Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl;
literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]);
}
}
bool properPropagation(TNode lit) const;
bool properExplanation(TNode node, TNode expl) const;
+ enum ExplainTaskKind {
+ // Literal sent out from the theory engine
+ SHARED_LITERAL_OUT,
+ // Explanation produced by a theory
+ THEORY_EXPLANATION,
+ // Explanation produced by the shared terms database
+ SHARED_DATABASE_EXPLANATION
+ };
+
+ struct ExplainTask {
+ Node node;
+ ExplainTaskKind kind;
+ theory::TheoryId theory;
+ ExplainTask(Node n, ExplainTaskKind k, theory::TheoryId tid = theory::THEORY_LAST) :
+ node(n), kind(k), theory(tid) {}
+ bool operator == (const ExplainTask& other) const {
+ return node == other.node && kind == other.kind && theory == other.theory;
+ }
+ };
+
+ struct ExplainTaskHashFunction {
+ size_t operator () (const ExplainTask& task) const {
+ size_t hash = 0;
+ hash = 0x9e3779b9 + NodeHashFunction().operator()(task.node);
+ hash ^= 0x9e3779b9 + task.kind + (hash << 6) + (hash >> 2);
+ hash ^= 0x9e3779b9 + task.theory + (hash << 6) + (hash >> 2);
+ return hash;
+ }
+ };
+
Node getExplanation(TNode node);
+ Node explain(ExplainTask toExplain);
+
Node getValue(TNode node);
/**
/** The false node */
Node d_false;
+ /**
+ * Adds an equality of terms t1 and t2 to the database.
+ */
+ void addEqualityInternal(TNode t1, TNode t2, TNode reason);
+
public:
/**
*/
bool hasTerm(TNode t) const;
+ /**
+ * Adds aa predicate t with given polarity
+ */
+ void addPredicate(TNode t, bool polarity, TNode reason);
+
/**
* Adds an equality t1 = t2 to the database.
*/
* Check whether the two term are dis-equal.
*/
bool areDisequal(TNode t1, TNode t2);
+
+ /**
+ * Return the number of nodes in the equivalence class contianing t
+ * Adds t if not already there.
+ */
+ size_t getSize(TNode t);
+
};
} // Namespace uf
}
template <typename NotifyClass>
-void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) {
+void EqualityEngine<NotifyClass>::addEqualityInternal(TNode t1, TNode t2, TNode reason) {
- Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+ Debug("equality") << "EqualityEngine::addEqualityInternal(" << t1 << "," << t2 << ")" << std::endl;
// Add the terms if they are not already in the database
addTerm(t1);
EqualityNodeId t1Id = getNodeId(t1);
EqualityNodeId t2Id = getNodeId(t2);
enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason));
+
propagate();
}
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addPredicate(TNode t, bool polarity, TNode reason) {
+
+ Debug("equality") << "EqualityEngine::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
+
+ addEqualityInternal(t, polarity ? d_true : d_false, reason);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) {
+
+ Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+
+ addEqualityInternal(t1, t2, reason);
+
+ Node equality = t1.eqNode(t2);
+ addEqualityInternal(equality, d_true, reason);
+}
+
template <typename NotifyClass>
void EqualityEngine<NotifyClass>::addDisequality(TNode t1, TNode t2, TNode reason) {
Debug("equality") << "EqualityEngine::addDisequality(" << t1 << "," << t2 << ")" << std::endl;
Node equality1 = t1.eqNode(t2);
- addEquality(equality1, d_false, reason);
-
+ addEqualityInternal(equality1, d_false, reason);
+
Node equality2 = t2.eqNode(t1);
- addEquality(equality2, d_false, reason);
+ addEqualityInternal(equality2, d_false, reason);
}
// Don't notify during this check
ScopedBool turnOfNotify(d_performNotify, false);
- // Push the context, so that we can remove the terms later
- d_context->push();
-
// Add the terms (they might not be there)
addTerm(t1);
addTerm(t2);
EqualityNodeId t2Id = getNodeId(t2);
getExplanation(t1Id, t2Id, equalities);
- // Pop the possible extra information
- d_context->pop();
}
template <typename NotifyClass>
// Don't notify during this check
ScopedBool turnOfNotify(d_performNotify, false);
- // Push the context, so that we can remove the terms later
- d_context->push();
-
// Add the terms
addTerm(t1);
addTerm(t2);
EqualityNodeId falseId = getNodeId(d_false);
getExplanation(equalityId, falseId, equalities);
- // Pop the possible extra information
- d_context->pop();
}
}
}
+ if (Debug.isOn("equality::internal")) {
+ debugPrintGraph();
+ }
+
Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
}
// Don't notify during this check
ScopedBool turnOfNotify(d_performNotify, false);
- // Push the context, so that we can remove the terms later
- d_context->push();
-
// Add the terms
addTerm(t1);
addTerm(t2);
bool equal = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
- // Pop the context (triggers new term removal)
- d_context->pop();
-
// Return whether the two terms are equal
return equal;
}
// Don't notify during this check
ScopedBool turnOfNotify(d_performNotify, false);
- // Push the context, so that we can remove the terms later
- d_context->push();
-
// Add the terms
addTerm(t1);
addTerm(t2);
Node equality = t1.eqNode(t2);
addTerm(equality);
if (getEqualityNode(equality).getFind() == getEqualityNode(d_false).getFind()) {
- d_context->pop();
return true;
}
- // Pop the context (triggers new term removal)
- d_context->pop();
-
// Return whether the terms are disequal
return false;
}
+template <typename NotifyClass>
+size_t EqualityEngine<NotifyClass>::getSize(TNode t)
+{
+ // Add the term
+ addTerm(t);
+ return getEqualityNode(getEqualityNode(t).getFind()).getSize();
+}
+
template <typename NotifyClass>
void EqualityEngine<NotifyClass>::addTriggerTerm(TNode t)
{
d_equalityEngine.addEquality(fact[0], fact[1], fact);
break;
case kind::APPLY_UF:
- d_equalityEngine.addEquality(fact, d_true, fact);
+ d_equalityEngine.addPredicate(fact, true, fact);
break;
case kind::NOT:
if (fact[0].getKind() == kind::APPLY_UF) {
- d_equalityEngine.addEquality(fact[0], d_false, fact);
+ d_equalityEngine.addPredicate(fact[0], false, fact);
} else {
// Assert the dis-equality
d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
bool satValue;
- if (!d_valuation.hasSatValue(literal, satValue)) {
+ Node normalized = Rewriter::rewrite(literal);
+ if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
d_out->propagate(literal);
} else {
- if (!satValue) {
- Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl;
- Node negatedLiteral;
- std::vector<TNode> assumptions;
- if (literal != d_false) {
- negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
- assumptions.push_back(negatedLiteral);
- }
- explain(literal, assumptions);
- d_conflictNode = mkAnd(assumptions);
- d_conflict = true;
- break;
- } else {
- Debug("uf") << "TheoryUF::propagate(): already asserted" << std::endl;
+ Debug("uf") << "TheoryUF::propagate(): in conflict, normalized = " << normalized << std::endl;
+ Node negatedLiteral;
+ std::vector<TNode> assumptions;
+ if (normalized != d_false) {
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+ assumptions.push_back(negatedLiteral);
}
+ explain(literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ break;
}
}
}
}
// See if the literal has been asserted already
+ Node normalized = Rewriter::rewrite(literal);
bool satValue = false;
- bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue);
+ bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
// If asserted, we're done or in conflict
if (isAsserted) {
- if (satValue) {
- Debug("uf") << "TheoryUF::propagate(" << literal << ") => already known" << std::endl;
- return true;
- } else {
- Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl;
+ if (!satValue) {
+ Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
std::vector<TNode> assumptions;
Node negatedLiteral;
- if (literal != d_false) {
- negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
+ if (normalized != d_false) {
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
assumptions.push_back(negatedLiteral);
}
explain(literal, assumptions);
d_conflict = true;
return false;
}
+ // Propagate even if already known in SAT - could be a new equation between shared terms
+ // (terms that weren't shared when the literal was asserted!)
}
// Nothing, just enqueue it for propagation and mark it as asserted already
}
bool Valuation::hasSatValue(TNode n, bool& value) const {
- Node normalized = Rewriter::rewrite(n);
- if (d_engine->getPropEngine()->isSatLiteral(normalized)) {
- return d_engine->getPropEngine()->hasValue(normalized, value);
+ // Node normalized = Rewriter::rewrite(n);
+ if (d_engine->getPropEngine()->isSatLiteral(n)) {
+ return d_engine->getPropEngine()->hasValue(n, value);
} else {
return false;
}
BitVector unsignedDiv (const BitVector& y) const {
Assert (d_size == y.d_size);
+ // TODO: decide whether we really want these semantics
+ if (y.d_value == 0) {
+ return BitVector(d_size, Integer(0));
+ }
Assert (d_value >= 0 && y.d_value > 0);
return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
}
BitVector unsignedRem(const BitVector& y) const {
Assert (d_size == y.d_size);
+ // TODO: decide whether we really want these semantics
+ if (y.d_value == 0) {
+ return BitVector(d_size, Integer(0));
+ }
Assert (d_value >= 0 && y.d_value > 0);
return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
}
T1 first;
T2 second;
T3 third;
+ triple() {}
triple(const T1& t1, const T2& t2, const T3& t3) :
first(t1),
second(t2),
T2 second;
T3 third;
T4 fourth;
+ quad() {}
quad(const T1& t1, const T2& t2, const T3& t3, const T4& t4) :
first(t1),
second(t2),
regress/regress0/bv \
regress/regress0/bv/core \
regress/regress0/arrays \
+ regress/regress0/aufbv \
regress/regress0/datatypes \
regress/regress0/lemmas \
regress/regress0/push-pop \
-SUBDIRS = . arith precedence uf uflra uflia bv arrays datatypes lemmas push-pop preprocess
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv datatypes lemmas push-pop preprocess
BINARY = cvc4
if PROOF_REGRESSIONS
incorrect8.minimized.smt \
incorrect9.smt \
incorrect10.smt \
- incorrect11.smt
+ incorrect11.smt \
+ x2.smt \
+ x3.smt
EXTRA_DIST = $(TESTS) \
bug272.smt \
--- /dev/null
+(benchmark read5.smt
+:logic QF_AX
+:status unsat
+:extrafuns ((a Index))
+:extrafuns ((S Array))
+:extrafuns ((SS Array))
+:status unknown
+:formula
+(flet ($n1 (= S SS))
+(let (?n2 (select S a))
+(let (?n3 (store SS a ?n2))
+(flet ($n4 (= S ?n3))
+(flet ($n5 true)
+(flet ($n6 (if_then_else $n1 $n4 $n5))
+(flet ($n7 (not $n6))
+$n7
+))))))))
--- /dev/null
+(benchmark fuzzsmt
+:logic QF_AX
+:status sat
+:extrafuns ((v4 Index))
+:extrafuns ((v2 Index))
+:extrafuns ((v3 Index))
+:extrafuns ((v1 Array))
+:extrafuns ((v6 Element))
+:extrafuns ((v0 Array))
+:extrafuns ((v5 Element))
+:status unknown
+:formula
+(let (?n1 (store v1 v3 v6))
+(flet ($n2 (distinct ?n1 v0))
+(flet ($n3 (= v4 v2))
+(flet ($n4 true)
+(let (?n5 (store v1 v4 v6))
+(let (?n6 (select ?n5 v2))
+(let (?n7 (ite $n4 ?n6 v6))
+(let (?n8 (select v1 v3))
+(let (?n9 (ite $n3 ?n7 ?n8))
+(flet ($n10 (distinct ?n8 ?n8))
+(let (?n11 (ite $n10 v6 ?n6))
+(let (?n12 (ite $n2 ?n9 ?n11))
+(flet ($n13 (= v6 ?n12))
+(flet ($n14 (distinct ?n8 v5))
+(let (?n15 (ite $n2 v1 v0))
+(let (?n16 (ite $n14 v1 ?n15))
+(flet ($n17 (distinct ?n5 ?n16))
+(flet ($n18 (and $n13 $n17))
+(flet ($n19 (distinct v0 ?n5))
+(let (?n20 (ite $n19 v2 v4))
+(flet ($n21 (= v3 v2))
+(flet ($n22 (= v0 v0))
+(flet ($n23 (= v6 ?n8))
+(flet ($n24 false)
+(flet ($n25 (= ?n6 ?n8))
+(let (?n26 (ite $n25 v3 v2))
+(let (?n27 (ite $n24 v4 ?n26))
+(let (?n28 (ite $n23 v3 ?n27))
+(let (?n29 (ite $n22 ?n28 v4))
+(let (?n30 (ite $n21 v3 ?n29))
+(flet ($n31 (distinct ?n20 ?n30))
+(flet ($n32 (or $n18 $n31))
+$n32
+)))))))))))))))))))))))))))))))))
--- /dev/null
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/cvc4
+else
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/cvc4
+endif
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS = \
+ bug00.smt
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+# error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+# error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
--- /dev/null
+(benchmark no_init_multi_member7.smt
+:logic QF_AUFBV
+:status unsat
+:extrafuns ((member_6_curr_2 BitVec[32]))
+:extrafuns ((arr_next_15 Array[32:32]))
+:extrafuns ((member_3_curr_4 BitVec[32]))
+:extrafuns ((main_0_x_3 BitVec[32]))
+:extrafuns ((member_3_curr_5 BitVec[32]))
+:extrafuns ((arr_val_8 Array[32:32]))
+:status unknown
+:formula
+(flet ($n1 true)
+(let (?n2 bv0[32])
+(let (?n3 bv1[32])
+(let (?n4 (select arr_val_8 member_6_curr_2))
+(flet ($n5 (= ?n3 ?n4))
+(let (?n6 (ite $n5 ?n3 ?n2))
+(flet ($n7 (= ?n2 ?n6))
+(let (?n8 (select arr_next_15 member_3_curr_5))
+(flet ($n9 (= ?n2 ?n8))
+(let (?n10 (select arr_next_15 ?n3))
+(flet ($n11 (= ?n10 member_3_curr_4))
+(let (?n12 (select arr_next_15 ?n2))
+(flet ($n13 (= ?n3 ?n12))
+(flet ($n14 (= ?n2 main_0_x_3))
+(flet ($n15 (= ?n3 member_3_curr_4))
+(flet ($n16 (and $n14 $n15))
+(let (?n17 (ite $n16 ?n2 member_3_curr_4))
+(flet ($n18 (= member_3_curr_5 ?n17))
+(flet ($n19 (= member_6_curr_2 ?n12))
+(let (?n20 (select arr_next_15 member_6_curr_2))
+(flet ($n21 (= ?n2 ?n20))
+(flet ($n22 (and $n7 $n9 $n11 $n13 $n18 $n19 $n1 $n21))
+$n22
+)))))))))))))))))))))))
projects / cvc5.git / commitdiff