src/theory/combination_care_graph.cpp

   1 /*********************                                                        */
   2 /*! \file combination_care_graph.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Dejan Jovanovic
   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 Management of a care graph based approach for theory combination.
  13  **/
  14
  15 #include "theory/combination_care_graph.h"
  16
  17 #include "expr/node_visitor.h"
  18 #include "theory/care_graph.h"
  19 #include "theory/theory_engine.h"
  20
  21 namespace CVC4 {
  22 namespace theory {
  23
  24 CombinationCareGraph::CombinationCareGraph(
  25     TheoryEngine& te,
  26     const std::vector<Theory*>& paraTheories,
  27     ProofNodeManager* pnm)
  28     : CombinationEngine(te, paraTheories, pnm)
  29 {
  30 }
  31
  32 CombinationCareGraph::~CombinationCareGraph() {}
  33
  34 void CombinationCareGraph::combineTheories()
  35 {
  36   Trace("combineTheories") << "TheoryEngine::combineTheories()" << std::endl;
  37
  38   // Care graph we'll be building
  39   CareGraph careGraph;
  40
  41   // get the care graph from the parametric theories
  42   for (Theory* t : d_paraTheories)
  43   {
  44     t->getCareGraph(&careGraph);
  45   }
  46
  47   Trace("combineTheories")
  48       << "TheoryEngine::combineTheories(): care graph size = "
  49       << careGraph.size() << std::endl;
  50
  51   // Now add splitters for the ones we are interested in
  52   prop::PropEngine* propEngine = d_te.getPropEngine();
  53   for (const CarePair& carePair : careGraph)
  54   {
  55     Debug("combineTheories")
  56         << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = "
  57         << carePair.d_b << " from " << carePair.d_theory << std::endl;
  58
  59     // The equality in question (order for no repetition)
  60     Node equality = carePair.d_a.eqNode(carePair.d_b);
  61
  62     // We need to split on it
  63     Debug("combineTheories")
  64         << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
  65
  66     TrustNode tsplit;
  67     if (isProofEnabled())
  68     {
  69       // make proof of splitting lemma
  70       tsplit = d_cmbsPg->mkTrustNodeSplit(equality);
  71     }
  72     else
  73     {
  74       Node split = equality.orNode(equality.notNode());
  75       tsplit = TrustNode::mkTrustLemma(split, nullptr);
  76     }
  77     sendLemma(tsplit, carePair.d_theory);
  78
  79     // Could check the equality status here:
  80     //   EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
  81     // and only require true phase below if:
  82     //   es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL
  83     // and require false phase below if:
  84     //   es == EQUALITY_FALSE_IN_MODEL
  85     // This is supposed to force preference to follow what the theory models
  86     // already have but it doesn't seem to make a big difference - need to
  87     // explore more -Clark
  88     Node e = d_te.ensureLiteral(equality);
  89     propEngine->requirePhase(e, true);
  90   }
  91 }
  92
  93 bool CombinationCareGraph::buildModel()
  94 {
  95   // building the model happens as a separate step
  96   return d_mmanager->buildModel();
  97 }
  98
  99 }  // namespace theory
 100 }  // namespace CVC4