src/theory/bv/bv_subtheory_core.cpp

   1 /*********************                                                        */
   2 /*! \file bv_subtheory_eq.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): lianah
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Algebraic solver.
  13  **
  14  ** Algebraic solver.
  15  **/
  16
  17 #include "theory/bv/bv_subtheory_core.h"
  18
  19 #include "theory/bv/theory_bv.h"
  20 #include "theory/bv/theory_bv_utils.h"
  21 #include "theory/bv/slicer.h"
  22 #include "theory/model.h"
  23
  24 using namespace std;
  25 using namespace CVC4;
  26 using namespace CVC4::context;
  27 using namespace CVC4::theory;
  28 using namespace CVC4::theory::bv;
  29 using namespace CVC4::theory::bv::utils;
  30
  31 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
  32   : SubtheorySolver(c, bv),
  33     d_notify(*this),
  34     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
  35     d_slicer(new Slicer(c, this)),
  36     d_isCoreTheory(c, true),
  37     d_reasons(c)
  38 {
  39   if (d_useEqualityEngine) {
  40
  41     // The kinds we are treating as function application in congruence
  42     d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
  43     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
  44     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
  45     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
  46     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
  47     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
  48     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
  49     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
  50     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
  51     d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
  52     d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
  53     d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
  54     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
  55     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
  56     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
  57     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
  58     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
  59     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
  60     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
  61     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
  62     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
  63     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
  64     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
  65     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
  66     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
  67     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
  68     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
  69     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
  70     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
  71     //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
  72   }
  73 }
  74
  75 CoreSolver::~CoreSolver() {
  76   delete d_slicer;
  77 }
  78 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  79   d_equalityEngine.setMasterEqualityEngine(eq);
  80 }
  81
  82 void CoreSolver::preRegister(TNode node) {
  83   if (!d_useEqualityEngine)
  84     return;
  85
  86   if (node.getKind() == kind::EQUAL) {
  87       d_equalityEngine.addTriggerEquality(node);
  88       // d_slicer->processEquality(node);
  89   } else {
  90     d_equalityEngine.addTerm(node);
  91   }
  92 }
  93
  94
  95 void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
  96   bool polarity = literal.getKind() != kind::NOT;
  97   TNode atom = polarity ? literal : literal[0];
  98   if (atom.getKind() == kind::EQUAL) {
  99     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
 100   } else {
 101     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
 102   }
 103 }
 104
 105 Node CoreSolver::getBaseDecomposition(TNode a, std::vector<TNode>& explanation) {
 106   std::vector<Node> a_decomp;
 107   d_slicer->getBaseDecomposition(a, a_decomp, explanation);
 108   Node new_a = utils::mkConcat(a_decomp);
 109   Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n";
 110   return new_a;
 111 }
 112
 113 bool CoreSolver::decomposeFact(TNode fact) {
 114   Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
 115   // assert decompositions since the equality engine does not know the semantics of
 116   // concat:
 117   //   a == a_1 concat ... concat a_k
 118   //   b == b_1 concat ... concat b_k
 119
 120   if (fact.getKind() == kind::EQUAL) {
 121     TNode a = fact[0];
 122     TNode b = fact[1];
 123
 124     d_slicer->processEquality(fact);
 125     std::vector<TNode> explanation_a;
 126     Node new_a = getBaseDecomposition(a, explanation_a);
 127     Node reason_a = mkAnd(explanation_a);
 128     d_reasons.insert(reason_a);
 129
 130     std::vector<TNode> explanation_b;
 131     Node new_b = getBaseDecomposition(b, explanation_b);
 132     Node reason_b = mkAnd(explanation_b);
 133     d_reasons.insert(reason_b);
 134
 135     std::vector<Node> explanation;
 136     explanation.push_back(fact);
 137     explanation.insert(explanation.end(), explanation_a.begin(), explanation_a.end());
 138     explanation.insert(explanation.end(), explanation_b.begin(), explanation_b.end());
 139
 140     Node reason = utils::mkAnd(explanation);
 141     d_reasons.insert(reason);
 142
 143     Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
 144             utils::getSize(new_a) == utils::getSize(a));
 145
 146     NodeManager* nm = NodeManager::currentNM();
 147     Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
 148     Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
 149
 150     bool ok = true;
 151     ok = assertFactToEqualityEngine(a_eq_new_a, reason_a);
 152     if (!ok) return false;
 153     ok = assertFactToEqualityEngine(b_eq_new_b, reason_a);
 154     if (!ok) return false;
 155     // assert the individual equalities as well
 156     //    a_i == b_i
 157     if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
 158         new_b.getKind() == kind::BITVECTOR_CONCAT) {
 159       Assert (new_a.getNumChildren() == new_b.getNumChildren());
 160       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
 161         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
 162         // this reason is not very precise!!
 163         ok = assertFactToEqualityEngine(eq_i, reason);
 164         d_reasons.insert(eq_i);
 165         if (!ok) return false;
 166       }
 167     }
 168     // merge the two terms in the slicer as well
 169     d_slicer->assertEquality(fact);
 170   } else {
 171     // still need to register the terms
 172     d_slicer->processEquality(fact[0]);
 173     TNode a = fact[0][0];
 174     TNode b = fact[0][1];
 175     std::vector<TNode> explanation_a;
 176     Node new_a = getBaseDecomposition(a, explanation_a);
 177     Node reason_a = explanation_a.empty()? mkTrue() : mkAnd(explanation_a);
 178     assertFactToEqualityEngine(utils::mkNode(kind::EQUAL, a, new_a), reason_a);
 179
 180     std::vector<TNode> explanation_b;
 181     Node new_b = getBaseDecomposition(b, explanation_b);
 182     Node reason_b = explanation_b.empty()? mkTrue() : mkAnd(explanation_b);
 183     assertFactToEqualityEngine(utils::mkNode(kind::EQUAL, b, new_b), reason_b);
 184
 185     d_reasons.insert(reason_a);
 186     d_reasons.insert(reason_b);
 187   }
 188   // finally assert the actual fact to the equality engine
 189   return assertFactToEqualityEngine(fact, fact);
 190 }
 191
 192 bool CoreSolver::check(Theory::Effort e) {
 193   Trace("bitvector::core") << "CoreSolver::check \n";
 194   Assert (!d_bv->inConflict());
 195   ++(d_statistics.d_numCallstoCheck);
 196   bool ok = true;
 197   std::vector<Node> core_eqs;
 198   while (! done()) {
 199     TNode fact = get();
 200
 201     // update whether we are in the core fragment
 202     if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
 203       d_isCoreTheory = false;
 204     }
 205
 206     // only reason about equalities
 207     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
 208       // ok = decomposeFact(fact);
 209       ok = assertFactToEqualityEngine(fact, fact);
 210     } else {
 211       ok = assertFactToEqualityEngine(fact, fact);
 212     }
 213     if (!ok)
 214       return false;
 215   }
 216
 217   // make sure to assert the new splits
 218   // std::vector<Node> new_splits;
 219   // d_slicer->getNewSplits(new_splits);
 220   // for (unsigned i = 0; i < new_splits.size(); ++i) {
 221   //   ok = assertFactToEqualityEngine(new_splits[i], utils::mkTrue());
 222   //   if (!ok)
 223   //     return false;
 224   // }
 225
 226   // if we are sat and in full check attempt to construct a model
 227   if (Theory::fullEffort(e) && isComplete()) {
 228     buildModel();
 229   }
 230
 231   return true;
 232 }
 233
 234 void CoreSolver::buildModel() {
 235   Debug("bv-core") << "CoreSolver::buildModel() \n";
 236   d_modelValues.clear();
 237   TNodeSet constants;
 238   TNodeSet constants_in_eq_engine;
 239   // collect constants in equality engine
 240   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
 241   while (!eqcs_i.isFinished()) {
 242     TNode repr = *eqcs_i;
 243     if  (repr.getKind() == kind::CONST_BITVECTOR) {
 244       // must check if it's just the constant
 245       eq::EqClassIterator it(repr, &d_equalityEngine);
 246       if (!(++it).isFinished()) {
 247         constants.insert(repr);
 248         constants_in_eq_engine.insert(repr);
 249       }
 250     }
 251     ++eqcs_i;
 252   }
 253   // build repr to value map
 254
 255   eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
 256   while (!eqcs_i.isFinished()) {
 257     TNode repr = *eqcs_i;
 258     ++eqcs_i;
 259     TypeNode type = repr.getType();
 260     if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
 261       Debug("bv-core-model") << "   processing " << repr <<"\n";
 262       // we need to assign a value for it
 263       TypeEnumerator te(type);
 264       Node val;
 265       do {
 266         val = *te;
 267         ++te;
 268         // Debug("bv-core-model") << "  trying value " << val << "\n";
 269         // Debug("bv-core-model") << "  is in set? " << constants.count(val) << "\n";
 270         // Debug("bv-core-model") << "  enumerator done? " << te.isFinished() << "\n";
 271       } while (constants.count(val) != 0 && !(te.isFinished()));
 272
 273       if (te.isFinished() && constants.count(val) != 0) {
 274         // if we cannot enumerate anymore values we just return the lemma stating that
 275         // at least two of the representatives are equal.
 276         std::vector<TNode> representatives;
 277         representatives.push_back(repr);
 278
 279         for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
 280              it != constants_in_eq_engine.end(); ++it) {
 281           TNode constant = *it;
 282           if (utils::getSize(constant) == utils::getSize(repr)) {
 283             representatives.push_back(constant);
 284           }
 285         }
 286         for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
 287           representatives.push_back(it->first);
 288         }
 289         std::vector<Node> equalities;
 290         for (unsigned i = 0; i < representatives.size(); ++i) {
 291           for (unsigned j = i + 1; j < representatives.size(); ++j) {
 292             TNode a = representatives[i];
 293             TNode b = representatives[j];
 294             if (utils::getSize(a) == utils::getSize(b)) {
 295               equalities.push_back(utils::mkNode(kind::EQUAL, a, b));
 296             }
 297           }
 298         }
 299         Node lemma = utils::mkOr(equalities);
 300         d_bv->lemma(lemma);
 301         Debug("bv-core") << "  lemma: " << lemma << "\n";
 302         return;
 303       }
 304       Debug("bv-core-model") << "   " << repr << " => " << val <<"\n" ;
 305       constants.insert(val);
 306       d_modelValues[repr] = val;
 307     }
 308   }
 309 }
 310
 311 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
 312   // Notify the equality engine
 313   if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
 314     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
 315     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
 316     bool negated = fact.getKind() == kind::NOT;
 317     TNode predicate = negated ? fact[0] : fact;
 318     if (predicate.getKind() == kind::EQUAL) {
 319       if (negated) {
 320         // dis-equality
 321         d_equalityEngine.assertEquality(predicate, false, reason);
 322       } else {
 323         // equality
 324         d_equalityEngine.assertEquality(predicate, true, reason);
 325       }
 326     } else {
 327       // Adding predicate if the congruence over it is turned on
 328       if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
 329         d_equalityEngine.assertPredicate(predicate, !negated, reason);
 330       }
 331     }
 332   }
 333
 334   // checking for a conflict
 335   if (d_bv->inConflict()) {
 336     return false;
 337   }
 338   return true;
 339 }
 340
 341 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
 342   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
 343   if (value) {
 344     return d_solver.storePropagation(equality);
 345   } else {
 346     return d_solver.storePropagation(equality.notNode());
 347   }
 348 }
 349
 350 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
 351   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
 352   if (value) {
 353     return d_solver.storePropagation(predicate);
 354   } else {
 355     return d_solver.storePropagation(predicate.notNode());
 356   }
 357 }
 358
 359 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 360   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 361   if (value) {
 362     return d_solver.storePropagation(t1.eqNode(t2));
 363   } else {
 364     return d_solver.storePropagation(t1.eqNode(t2).notNode());
 365   }
 366 }
 367
 368 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 369   d_solver.conflict(t1, t2);
 370 }
 371
 372 bool CoreSolver::storePropagation(TNode literal) {
 373   return d_bv->storePropagation(literal, SUB_CORE);
 374 }
 375
 376 void CoreSolver::conflict(TNode a, TNode b) {
 377   std::vector<TNode> assumptions;
 378   d_equalityEngine.explainEquality(a, b, true, assumptions);
 379   Node conflict = flattenAnd(assumptions);
 380   d_bv->setConflict(conflict);
 381 }
 382
 383 void CoreSolver::collectModelInfo(TheoryModel* m) {
 384   if (Debug.isOn("bitvector-model")) {
 385     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
 386     for (; it!= d_assertionQueue.end(); ++it) {
 387       Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
 388                                << *it << ")\n";
 389     }
 390   }
 391   set<Node> termSet;
 392   d_bv->computeRelevantTerms(termSet);
 393   m->assertEqualityEngine(&d_equalityEngine, &termSet);
 394   if (isComplete()) {
 395     Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
 396     for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
 397       Node a = it->first;
 398       Node b = it->second;
 399       m->assertEquality(a, b, true);
 400     }
 401   }
 402 }
 403
 404 Node CoreSolver::getModelValue(TNode var) {
 405   Assert (isComplete());
 406   TNode repr = d_equalityEngine.getRepresentative(var);
 407   if (repr.getKind() == kind::CONST_BITVECTOR) {
 408     return repr;
 409   }
 410   Assert (d_modelValues.find(repr) != d_modelValues.end());
 411   return d_modelValues[repr];
 412 }
 413
 414 CoreSolver::Statistics::Statistics()
 415   : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
 416 {
 417   StatisticsRegistry::registerStat(&d_numCallstoCheck);
 418 }
 419 CoreSolver::Statistics::~Statistics() {
 420   StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
 421 }