src/theory/sets/theory_sets.cpp

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