src/theory/datatypes/inference_manager.cpp

   1 /*********************                                                        */
   2 /*! \file inference_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   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 Datatypes inference manager
  13  **/
  14
  15 #include "theory/datatypes/inference_manager.h"
  16
  17 #include "expr/dtype.h"
  18 #include "options/datatypes_options.h"
  19 #include "theory/theory.h"
  20
  21 using namespace CVC4::kind;
  22
  23 namespace CVC4 {
  24 namespace theory {
  25 namespace datatypes {
  26
  27 DatatypesInference::DatatypesInference(Node conc, Node exp, ProofGenerator* pg)
  28     : SimpleTheoryInternalFact(conc, exp, pg)
  29 {
  30   // false is not a valid explanation
  31   Assert(d_exp.isNull() || !d_exp.isConst() || d_exp.getConst<bool>());
  32 }
  33
  34 bool DatatypesInference::mustCommunicateFact(Node n, Node exp)
  35 {
  36   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
  37   bool addLemma = false;
  38   if (options::dtInferAsLemmas() && !exp.isConst())
  39   {
  40     // all units are lemmas
  41     addLemma = true;
  42   }
  43   else if (n.getKind() == EQUAL)
  44   {
  45     TypeNode tn = n[0].getType();
  46     if (!tn.isDatatype())
  47     {
  48       addLemma = true;
  49     }
  50     else
  51     {
  52       const DType& dt = tn.getDType();
  53       addLemma = dt.involvesExternalType();
  54     }
  55   }
  56   else if (n.getKind() == LEQ || n.getKind() == OR)
  57   {
  58     addLemma = true;
  59   }
  60   if (addLemma)
  61   {
  62     Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
  63     return true;
  64   }
  65   Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
  66   return false;
  67 }
  68
  69 bool DatatypesInference::process(TheoryInferenceManager* im)
  70 {
  71   // check to see if we have to communicate it to the rest of the system
  72   if (mustCommunicateFact(d_conc, d_exp))
  73   {
  74     // send it as an (explained) lemma
  75     std::vector<Node> exp;
  76     if (!d_exp.isNull() && !d_exp.isConst())
  77     {
  78       exp.push_back(d_exp);
  79     }
  80     return im->lemmaExp(d_conc, exp, {});
  81   }
  82   // assert the internal fact
  83   bool polarity = d_conc.getKind() != NOT;
  84   TNode atom = polarity ? d_conc : d_conc[0];
  85   im->assertInternalFact(atom, polarity, d_exp);
  86   return true;
  87 }
  88
  89 InferenceManager::InferenceManager(Theory& t,
  90                                    TheoryState& state,
  91                                    ProofNodeManager* pnm)
  92     : InferenceManagerBuffered(t, state, pnm)
  93 {
  94 }
  95
  96 void InferenceManager::addPendingInference(Node conc,
  97                                            Node exp,
  98                                            ProofGenerator* pg)
  99 {
 100   d_pendingFact.push_back(std::make_shared<DatatypesInference>(conc, exp, pg));
 101 }
 102
 103 void InferenceManager::process()
 104 {
 105   // process pending lemmas, used infrequently, only for definitional lemmas
 106   doPendingLemmas();
 107   // now process the pending facts
 108   doPendingFacts();
 109 }
 110
 111 bool InferenceManager::sendLemmas(const std::vector<Node>& lemmas)
 112 {
 113   bool ret = false;
 114   for (const Node& lem : lemmas)
 115   {
 116     if (lemma(lem))
 117     {
 118       ret = true;
 119     }
 120   }
 121   return ret;
 122 }
 123
 124 }  // namespace datatypes
 125 }  // namespace theory
 126 }  // namespace CVC4