src/theory/sets/theory_sets.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sets.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Kshitij Bansal, Andres Noetzli
   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 Sets theory.
  13  **
  14  ** Sets theory.
  15  **/
  16
  17 #include "theory/sets/theory_sets.h"
  18
  19 #include "options/sets_options.h"
  20 #include "theory/sets/theory_sets_private.h"
  21 #include "theory/sets/theory_sets_rewriter.h"
  22 #include "theory/theory_model.h"
  23
  24 using namespace CVC4::kind;
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace sets {
  29
  30 TheorySets::TheorySets(context::Context* c,
  31                        context::UserContext* u,
  32                        OutputChannel& out,
  33                        Valuation valuation,
  34                        const LogicInfo& logicInfo,
  35                        ProofNodeManager* pnm)
  36     : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
  37       d_internal(new TheorySetsPrivate(*this, c, u))
  38 {
  39   // Do not move me to the header.
  40   // The constructor + destructor are not in the header as d_internal is a
  41   // unique_ptr<TheorySetsPrivate> and TheorySetsPrivate is an opaque type in
  42   // the header (Pimpl). See https://herbsutter.com/gotw/_100/ .
  43 }
  44
  45 TheorySets::~TheorySets()
  46 {
  47   // Do not move me to the header. See explanation in the constructor.
  48 }
  49
  50 TheoryRewriter* TheorySets::getTheoryRewriter()
  51 {
  52   return d_internal->getTheoryRewriter();
  53 }
  54
  55 void TheorySets::finishInit()
  56 {
  57   TheoryModel* tm = d_valuation.getModel();
  58   Assert(tm != nullptr);
  59   tm->setUnevaluatedKind(COMPREHENSION);
  60   // choice is used to eliminate witness
  61   tm->setUnevaluatedKind(WITNESS);
  62 }
  63
  64 void TheorySets::addSharedTerm(TNode n) {
  65   d_internal->addSharedTerm(n);
  66 }
  67
  68 void TheorySets::check(Effort e) {
  69   if (done() && e < Theory::EFFORT_FULL) {
  70     return;
  71   }
  72   TimerStat::CodeTimer checkTimer(d_checkTime);
  73   d_internal->check(e);
  74 }
  75
  76 bool TheorySets::collectModelInfo(TheoryModel* m)
  77 {
  78   return d_internal->collectModelInfo(m);
  79 }
  80
  81 void TheorySets::computeCareGraph() {
  82   d_internal->computeCareGraph();
  83 }
  84
  85 TrustNode TheorySets::explain(TNode node)
  86 {
  87   Node exp = d_internal->explain(node);
  88   return TrustNode::mkTrustPropExp(node, exp, nullptr);
  89 }
  90
  91 EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) {
  92   return d_internal->getEqualityStatus(a, b);
  93 }
  94
  95 Node TheorySets::getModelValue(TNode node) {
  96   return Node::null();
  97 }
  98
  99 void TheorySets::preRegisterTerm(TNode node) {
 100   d_internal->preRegisterTerm(node);
 101 }
 102
 103 TrustNode TheorySets::expandDefinition(Node n)
 104 {
 105   Kind nk = n.getKind();
 106   if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
 107       || nk == COMPREHENSION)
 108   {
 109     if (!options::setsExt())
 110     {
 111       std::stringstream ss;
 112       ss << "Extended set operators are not supported in default mode, try "
 113             "--sets-ext.";
 114       throw LogicException(ss.str());
 115     }
 116   }
 117   if (nk == COMPREHENSION)
 118   {
 119     // set comprehension is an implicit quantifier, require it in the logic
 120     if (!getLogicInfo().isQuantified())
 121     {
 122       std::stringstream ss;
 123       ss << "Set comprehensions require quantifiers in the background logic.";
 124       throw LogicException(ss.str());
 125     }
 126   }
 127   return d_internal->expandDefinition(n);
 128 }
 129
 130 Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
 131   Debug("sets-proc") << "ppAssert : " << in << std::endl;
 132   Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
 133
 134   // this is based off of Theory::ppAssert
 135   if (in.getKind() == kind::EQUAL)
 136   {
 137     if (in[0].isVar() && isLegalElimination(in[0], in[1]))
 138     {
 139       // We cannot solve for sets if setsExt is enabled, since universe set
 140       // may appear when this option is enabled, and solving for such a set
 141       // impacts the semantics of universe set, see
 142       // regress0/sets/pre-proc-univ.smt2
 143       if (!in[0].getType().isSet() || !options::setsExt())
 144       {
 145         outSubstitutions.addSubstitution(in[0], in[1]);
 146         status = Theory::PP_ASSERT_STATUS_SOLVED;
 147       }
 148     }
 149     else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
 150     {
 151       if (!in[0].getType().isSet() || !options::setsExt())
 152       {
 153         outSubstitutions.addSubstitution(in[1], in[0]);
 154         status = Theory::PP_ASSERT_STATUS_SOLVED;
 155       }
 156     }
 157     else if (in[0].isConst() && in[1].isConst())
 158     {
 159       if (in[0] != in[1])
 160       {
 161         status = Theory::PP_ASSERT_STATUS_CONFLICT;
 162       }
 163     }
 164   }
 165   return status;
 166 }
 167
 168 void TheorySets::presolve() {
 169   d_internal->presolve();
 170 }
 171
 172 void TheorySets::propagate(Effort e) {
 173   d_internal->propagate(e);
 174 }
 175
 176 void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 177   d_internal->setMasterEqualityEngine(eq);
 178 }
 179
 180 bool TheorySets::isEntailed( Node n, bool pol ) {
 181   return d_internal->isEntailed( n, pol );
 182 }
 183
 184 }/* CVC4::theory::sets namespace */
 185 }/* CVC4::theory namespace */
 186 }/* CVC4 namespace */