src/theory/bv/bv_subtheory_core.cpp

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