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