src/theory/theory_inference_manager.cpp

   1 /*********************                                                        */
   2 /*! \file theory_inference_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Gereon Kremer
   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 An inference manager for Theory
  13  **/
  14
  15 #include "theory/theory_inference_manager.h"
  16
  17 #include "theory/theory.h"
  18 #include "theory/uf/equality_engine.h"
  19
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23 namespace theory {
  24
  25 TheoryInferenceManager::TheoryInferenceManager(Theory& t,
  26                                                TheoryState& state,
  27                                                ProofNodeManager* pnm)
  28     : d_theory(t),
  29       d_theoryState(state),
  30       d_out(t.getOutputChannel()),
  31       d_ee(nullptr),
  32       d_pnm(pnm),
  33       d_keep(t.getSatContext()),
  34       d_lemmasSent(t.getUserContext()),
  35       d_numConflicts(0),
  36       d_numCurrentLemmas(0),
  37       d_numCurrentFacts(0)
  38 {
  39 }
  40
  41 void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
  42 {
  43   d_ee = ee;
  44   // if proofs are enabled, also make a proof equality engine to wrap ee
  45   if (d_pnm != nullptr)
  46   {
  47     d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
  48                                        d_theoryState.getUserContext(),
  49                                        *d_ee,
  50                                        d_pnm));
  51   }
  52 }
  53
  54 bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }
  55
  56 void TheoryInferenceManager::reset()
  57 {
  58   d_numConflicts = 0;
  59   d_numCurrentLemmas = 0;
  60   d_numCurrentFacts = 0;
  61 }
  62
  63 bool TheoryInferenceManager::hasSent() const
  64 {
  65   return d_theoryState.isInConflict() || d_numCurrentLemmas > 0
  66          || d_numCurrentFacts > 0;
  67 }
  68
  69 eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine()
  70 {
  71   return d_pfee.get();
  72 }
  73
  74 void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
  75 {
  76   if (!d_theoryState.isInConflict())
  77   {
  78     TrustNode tconf = explainConflictEqConstantMerge(a, b);
  79     d_theoryState.notifyInConflict();
  80     d_out.trustedConflict(tconf);
  81   }
  82 }
  83
  84 void TheoryInferenceManager::conflict(TNode conf)
  85 {
  86   if (!d_theoryState.isInConflict())
  87   {
  88     d_theoryState.notifyInConflict();
  89     d_out.conflict(conf);
  90     ++d_numConflicts;
  91   }
  92 }
  93
  94 void TheoryInferenceManager::trustedConflict(TrustNode tconf)
  95 {
  96   if (!d_theoryState.isInConflict())
  97   {
  98     d_theoryState.notifyInConflict();
  99     d_out.trustedConflict(tconf);
 100   }
 101 }
 102
 103 void TheoryInferenceManager::conflictExp(PfRule id,
 104                                          const std::vector<Node>& exp,
 105                                          const std::vector<Node>& args)
 106 {
 107   if (!d_theoryState.isInConflict())
 108   {
 109     // make the trust node
 110     TrustNode tconf = mkConflictExp(id, exp, args);
 111     // send it on the output channel
 112     trustedConflict(tconf);
 113   }
 114 }
 115
 116 TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
 117                                                 const std::vector<Node>& exp,
 118                                                 const std::vector<Node>& args)
 119 {
 120   if (d_pfee != nullptr)
 121   {
 122     // use proof equality engine to construct the trust node
 123     return d_pfee->assertConflict(id, exp, args);
 124   }
 125   // version without proofs
 126   Node conf = mkExplainPartial(exp, {});
 127   return TrustNode::mkTrustConflict(conf, nullptr);
 128 }
 129
 130 void TheoryInferenceManager::conflictExp(const std::vector<Node>& exp,
 131                                          ProofGenerator* pg)
 132 {
 133   if (!d_theoryState.isInConflict())
 134   {
 135     // make the trust node
 136     TrustNode tconf = mkConflictExp(exp, pg);
 137     // send it on the output channel
 138     trustedConflict(tconf);
 139   }
 140 }
 141
 142 TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
 143                                                 ProofGenerator* pg)
 144 {
 145   if (d_pfee != nullptr)
 146   {
 147     Assert(pg != nullptr);
 148     // use proof equality engine to construct the trust node
 149     return d_pfee->assertConflict(exp, pg);
 150   }
 151   // version without proofs
 152   Node conf = mkExplainPartial(exp, {});
 153   return TrustNode::mkTrustConflict(conf, nullptr);
 154 }
 155
 156 bool TheoryInferenceManager::propagateLit(TNode lit)
 157 {
 158   // If already in conflict, no more propagation
 159   if (d_theoryState.isInConflict())
 160   {
 161     return false;
 162   }
 163   // Propagate out
 164   bool ok = d_out.propagate(lit);
 165   if (!ok)
 166   {
 167     d_theoryState.notifyInConflict();
 168   }
 169   return ok;
 170 }
 171
 172 TrustNode TheoryInferenceManager::explainLit(TNode lit)
 173 {
 174   if (d_pfee != nullptr)
 175   {
 176     return d_pfee->explain(lit);
 177   }
 178   if (d_ee != nullptr)
 179   {
 180     Node exp = d_ee->mkExplainLit(lit);
 181     return TrustNode::mkTrustPropExp(lit, exp, nullptr);
 182   }
 183   Unimplemented() << "Inference manager for " << d_theory.getId()
 184                   << " was asked to explain a propagation but doesn't have an "
 185                      "equality engine or implement the "
 186                      "TheoryInferenceManager::explainLit interface!";
 187 }
 188
 189 TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
 190                                                                  TNode b)
 191 {
 192   Node lit = a.eqNode(b);
 193   if (d_pfee != nullptr)
 194   {
 195     return d_pfee->assertConflict(lit);
 196   }
 197   if (d_ee != nullptr)
 198   {
 199     Node conf = d_ee->mkExplainLit(lit);
 200     return TrustNode::mkTrustConflict(conf, nullptr);
 201   }
 202   Unimplemented() << "Inference manager for " << d_theory.getId()
 203                   << " mkTrustedConflictEqConstantMerge";
 204 }
 205
 206 bool TheoryInferenceManager::lemma(TNode lem, LemmaProperty p, bool doCache)
 207 {
 208   TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
 209   return trustedLemma(tlem, p, doCache);
 210 }
 211
 212 bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
 213                                           LemmaProperty p,
 214                                           bool doCache)
 215 {
 216   if (doCache)
 217   {
 218     if (!cacheLemma(tlem.getNode(), p))
 219     {
 220       return false;
 221     }
 222   }
 223   d_numCurrentLemmas++;
 224   d_out.trustedLemma(tlem, p);
 225   return true;
 226 }
 227
 228 bool TheoryInferenceManager::lemmaExp(Node conc,
 229                                       PfRule id,
 230                                       const std::vector<Node>& exp,
 231                                       const std::vector<Node>& noExplain,
 232                                       const std::vector<Node>& args,
 233                                       LemmaProperty p,
 234                                       bool doCache)
 235 {
 236   // make the trust node
 237   TrustNode trn = mkLemmaExp(conc, id, exp, noExplain, args);
 238   // send it on the output channel
 239   return trustedLemma(trn, p, doCache);
 240 }
 241
 242 TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
 243                                              PfRule id,
 244                                              const std::vector<Node>& exp,
 245                                              const std::vector<Node>& noExplain,
 246                                              const std::vector<Node>& args)
 247 {
 248   if (d_pfee != nullptr)
 249   {
 250     // make the trust node from the proof equality engine
 251     return d_pfee->assertLemma(conc, id, exp, noExplain, args);
 252   }
 253   // otherwise, not using proofs, explain and make trust node
 254   Node ant = mkExplainPartial(exp, noExplain);
 255   Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
 256   return TrustNode::mkTrustLemma(lem, nullptr);
 257 }
 258
 259 bool TheoryInferenceManager::lemmaExp(Node conc,
 260                                       const std::vector<Node>& exp,
 261                                       const std::vector<Node>& noExplain,
 262                                       ProofGenerator* pg,
 263                                       LemmaProperty p,
 264                                       bool doCache)
 265 {
 266   // make the trust node
 267   TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
 268   // send it on the output channel
 269   return trustedLemma(trn, p, doCache);
 270 }
 271
 272 TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
 273                                              const std::vector<Node>& exp,
 274                                              const std::vector<Node>& noExplain,
 275                                              ProofGenerator* pg)
 276 {
 277   if (d_pfee != nullptr)
 278   {
 279     // make the trust node from the proof equality engine
 280     return d_pfee->assertLemma(conc, exp, noExplain, pg);
 281   }
 282   // otherwise, not using proofs, explain and make trust node
 283   Node ant = mkExplainPartial(exp, noExplain);
 284   Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
 285   return TrustNode::mkTrustLemma(lem, nullptr);
 286 }
 287
 288 bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
 289 {
 290   return d_lemmasSent.find(lem) != d_lemmasSent.end();
 291 }
 292
 293 uint32_t TheoryInferenceManager::numSentLemmas() const
 294 {
 295   return d_numCurrentLemmas;
 296 }
 297
 298 bool TheoryInferenceManager::hasSentLemma() const
 299 {
 300   return d_numCurrentLemmas != 0;
 301 }
 302
 303 bool TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp)
 304 {
 305   return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
 306 }
 307
 308 bool TheoryInferenceManager::assertInternalFact(TNode atom,
 309                                                 bool pol,
 310                                                 PfRule id,
 311                                                 const std::vector<Node>& exp,
 312                                                 const std::vector<Node>& args)
 313 {
 314   Assert(id != PfRule::UNKNOWN);
 315   return processInternalFact(atom, pol, id, exp, args, nullptr);
 316 }
 317
 318 bool TheoryInferenceManager::assertInternalFact(TNode atom,
 319                                                 bool pol,
 320                                                 const std::vector<Node>& exp,
 321                                                 ProofGenerator* pg)
 322 {
 323   Assert(pg != nullptr);
 324   return processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg);
 325 }
 326
 327 bool TheoryInferenceManager::processInternalFact(TNode atom,
 328                                                  bool pol,
 329                                                  PfRule id,
 330                                                  const std::vector<Node>& exp,
 331                                                  const std::vector<Node>& args,
 332                                                  ProofGenerator* pg)
 333 {
 334   // make the node corresponding to the explanation
 335   Node expn = NodeManager::currentNM()->mkAnd(exp);
 336   // call the pre-notify fact method with preReg = false, isInternal = true
 337   if (d_theory.preNotifyFact(atom, pol, expn, false, true))
 338   {
 339     // Handled in a theory-specific way that doesn't require equality engine,
 340     // notice we return true, indicating that the fact was processed.
 341     return true;
 342   }
 343   Assert(d_ee != nullptr);
 344   Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
 345                          << expn << std::endl;
 346   d_numCurrentFacts++;
 347   // Now, assert the fact. How to do so depends on whether proofs are enabled.
 348   // If no proof production, or no proof rule was given
 349   bool ret = false;
 350   if (d_pfee == nullptr || id == PfRule::UNKNOWN)
 351   {
 352     if (atom.getKind() == kind::EQUAL)
 353     {
 354       ret = d_ee->assertEquality(atom, pol, expn);
 355     }
 356     else
 357     {
 358       ret = d_ee->assertPredicate(atom, pol, expn);
 359     }
 360     // Must reference count the equality and its explanation, which is not done
 361     // by the equality engine. Notice that we do *not* need to do this for
 362     // external assertions, which enter as facts in theory check. This is also
 363     // not done if we are asserting to the proof equality engine, which does
 364     // this caching itself within ProofEqEngine::assertFact.
 365     d_keep.insert(atom);
 366     d_keep.insert(expn);
 367   }
 368   else
 369   {
 370     // Note that we reconstruct the original literal lit here, since both the
 371     // original literal is needed for bookkeeping proofs. It is possible to
 372     // optimize this so that a few less nodes are created, but at the cost
 373     // of a more verbose interface to proof equality engine.
 374     Node lit = pol ? Node(atom) : atom.notNode();
 375     if (pg != nullptr)
 376     {
 377       // use the proof generator interface
 378       ret = d_pfee->assertFact(lit, expn, pg);
 379     }
 380     else
 381     {
 382       // use the explict proof step interface
 383       ret = d_pfee->assertFact(lit, id, expn, args);
 384     }
 385   }
 386   // call the notify fact method with isInternal = true
 387   d_theory.notifyFact(atom, pol, expn, true);
 388   Trace("infer-manager")
 389       << "TheoryInferenceManager::finished assertInternalFact" << std::endl;
 390   return ret;
 391 }
 392
 393 void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
 394 {
 395   if (n.getKind() == kind::AND)
 396   {
 397     for (const Node& nc : n)
 398     {
 399       d_ee->explainLit(nc, assumptions);
 400     }
 401   }
 402   else
 403   {
 404     d_ee->explainLit(n, assumptions);
 405   }
 406 }
 407
 408 Node TheoryInferenceManager::mkExplain(TNode n)
 409 {
 410   std::vector<TNode> assumptions;
 411   explain(n, assumptions);
 412   return NodeManager::currentNM()->mkAnd(assumptions);
 413 }
 414
 415 Node TheoryInferenceManager::mkExplainPartial(
 416     const std::vector<Node>& exp, const std::vector<Node>& noExplain)
 417 {
 418   std::vector<TNode> assumps;
 419   for (const Node& e : exp)
 420   {
 421     if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end())
 422     {
 423       if (std::find(assumps.begin(), assumps.end(), e) == assumps.end())
 424       {
 425         // a non-explained literal
 426         assumps.push_back(e);
 427       }
 428       continue;
 429     }
 430     // otherwise, explain it
 431     explain(e, assumps);
 432   }
 433   return NodeManager::currentNM()->mkAnd(assumps);
 434 }
 435
 436 uint32_t TheoryInferenceManager::numSentFacts() const
 437 {
 438   return d_numCurrentFacts;
 439 }
 440
 441 bool TheoryInferenceManager::hasSentFact() const
 442 {
 443   return d_numCurrentFacts != 0;
 444 }
 445
 446 bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 447 {
 448   if (d_lemmasSent.find(lem) != d_lemmasSent.end())
 449   {
 450     return false;
 451   }
 452   d_lemmasSent.insert(lem);
 453   return true;
 454 }
 455
 456 void TheoryInferenceManager::requirePhase(TNode n, bool pol)
 457 {
 458   return d_out.requirePhase(n, pol);
 459 }
 460
 461 void TheoryInferenceManager::spendResource(ResourceManager::Resource r)
 462 {
 463   d_out.spendResource(r);
 464 }
 465
 466 void TheoryInferenceManager::safePoint(ResourceManager::Resource r)
 467 {
 468   d_out.safePoint(r);
 469 }
 470
 471 void TheoryInferenceManager::setIncomplete() { d_out.setIncomplete(); }
 472
 473 }  // namespace theory
 474 }  // namespace CVC4