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