src/theory/bv/bv_subtheory_core.cpp

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