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-2021 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 #include "theory/trust_substitutions.h"
  24
  25 using namespace CVC4::kind;
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace sets {
  30
  31 TheorySets::TheorySets(context::Context* c,
  32                        context::UserContext* u,
  33                        OutputChannel& out,
  34                        Valuation valuation,
  35                        const LogicInfo& logicInfo,
  36                        ProofNodeManager* pnm)
  37     : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
  38       d_skCache(),
  39       d_state(c, u, valuation, d_skCache),
  40       d_im(*this, d_state, nullptr),
  41       d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)),
  42       d_notify(*d_internal.get(), d_im)
  43 {
  44   // use the official theory state and inference manager objects
  45   d_theoryState = &d_state;
  46   d_inferManager = &d_im;
  47 }
  48
  49 TheorySets::~TheorySets()
  50 {
  51 }
  52
  53 TheoryRewriter* TheorySets::getTheoryRewriter()
  54 {
  55   return d_internal->getTheoryRewriter();
  56 }
  57
  58 bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
  59 {
  60   esi.d_notify = &d_notify;
  61   esi.d_name = "theory::sets::ee";
  62   return true;
  63 }
  64
  65 void TheorySets::finishInit()
  66 {
  67   Assert(d_equalityEngine != nullptr);
  68
  69   d_valuation.setUnevaluatedKind(COMPREHENSION);
  70   // choice is used to eliminate witness
  71   d_valuation.setUnevaluatedKind(WITNESS);
  72   // Universe set is not evaluated. This is moreover important for ensuring that
  73   // we do not eliminate terms whose value involves the universe set.
  74   d_valuation.setUnevaluatedKind(UNIVERSE_SET);
  75
  76   // functions we are doing congruence over
  77   d_equalityEngine->addFunctionKind(SINGLETON);
  78   d_equalityEngine->addFunctionKind(UNION);
  79   d_equalityEngine->addFunctionKind(INTERSECTION);
  80   d_equalityEngine->addFunctionKind(SETMINUS);
  81   d_equalityEngine->addFunctionKind(MEMBER);
  82   d_equalityEngine->addFunctionKind(SUBSET);
  83   // relation operators
  84   d_equalityEngine->addFunctionKind(PRODUCT);
  85   d_equalityEngine->addFunctionKind(JOIN);
  86   d_equalityEngine->addFunctionKind(TRANSPOSE);
  87   d_equalityEngine->addFunctionKind(TCLOSURE);
  88   d_equalityEngine->addFunctionKind(JOIN_IMAGE);
  89   d_equalityEngine->addFunctionKind(IDEN);
  90   d_equalityEngine->addFunctionKind(APPLY_CONSTRUCTOR);
  91   // we do congruence over cardinality
  92   d_equalityEngine->addFunctionKind(CARD);
  93
  94   // finish initialization internally
  95   d_internal->finishInit();
  96 }
  97
  98 void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
  99
 100 void TheorySets::notifyFact(TNode atom,
 101                             bool polarity,
 102                             TNode fact,
 103                             bool isInternal)
 104 {
 105   d_internal->notifyFact(atom, polarity, fact);
 106 }
 107
 108 bool TheorySets::collectModelValues(TheoryModel* m,
 109                                     const std::set<Node>& termSet)
 110 {
 111   return d_internal->collectModelValues(m, termSet);
 112 }
 113
 114 void TheorySets::computeCareGraph() {
 115   d_internal->computeCareGraph();
 116 }
 117
 118 TrustNode TheorySets::explain(TNode node)
 119 {
 120   Node exp = d_internal->explain(node);
 121   return TrustNode::mkTrustPropExp(node, exp, nullptr);
 122 }
 123
 124 Node TheorySets::getModelValue(TNode node) {
 125   return Node::null();
 126 }
 127
 128 void TheorySets::preRegisterTerm(TNode node)
 129 {
 130   d_internal->preRegisterTerm(node);
 131 }
 132
 133 TrustNode TheorySets::expandDefinition(Node n)
 134 {
 135   // we currently do not expand any set operators
 136   return TrustNode::null();
 137 }
 138
 139 TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
 140 {
 141   Kind nk = n.getKind();
 142   if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
 143       || nk == COMPREHENSION)
 144   {
 145     if (!options::setsExt())
 146     {
 147       std::stringstream ss;
 148       ss << "Extended set operators are not supported in default mode, try "
 149             "--sets-ext.";
 150       throw LogicException(ss.str());
 151     }
 152   }
 153   if (nk == COMPREHENSION)
 154   {
 155     // set comprehension is an implicit quantifier, require it in the logic
 156     if (!getLogicInfo().isQuantified())
 157     {
 158       std::stringstream ss;
 159       ss << "Set comprehensions require quantifiers in the background logic.";
 160       throw LogicException(ss.str());
 161     }
 162   }
 163   return d_internal->ppRewrite(n, lems);
 164 }
 165
 166 Theory::PPAssertStatus TheorySets::ppAssert(
 167     TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 168 {
 169   TNode in = tin.getNode();
 170   Debug("sets-proc") << "ppAssert : " << in << std::endl;
 171   Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
 172
 173   // this is based off of Theory::ppAssert
 174   if (in.getKind() == EQUAL)
 175   {
 176     if (in[0].isVar() && isLegalElimination(in[0], in[1]))
 177     {
 178       // We cannot solve for sets if setsExt is enabled, since universe set
 179       // may appear when this option is enabled, and solving for such a set
 180       // impacts the semantics of universe set, see
 181       // regress0/sets/pre-proc-univ.smt2
 182       if (!in[0].getType().isSet() || !options::setsExt())
 183       {
 184         outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
 185         status = Theory::PP_ASSERT_STATUS_SOLVED;
 186       }
 187     }
 188     else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
 189     {
 190       if (!in[0].getType().isSet() || !options::setsExt())
 191       {
 192         outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
 193         status = Theory::PP_ASSERT_STATUS_SOLVED;
 194       }
 195     }
 196     else if (in[0].isConst() && in[1].isConst())
 197     {
 198       if (in[0] != in[1])
 199       {
 200         status = Theory::PP_ASSERT_STATUS_CONFLICT;
 201       }
 202     }
 203   }
 204   return status;
 205 }
 206
 207 void TheorySets::presolve() {
 208   d_internal->presolve();
 209 }
 210
 211 bool TheorySets::isEntailed( Node n, bool pol ) {
 212   return d_internal->isEntailed( n, pol );
 213 }
 214
 215 /**************************** eq::NotifyClass *****************************/
 216
 217 void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
 218 {
 219   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:"
 220                    << " t = " << t << std::endl;
 221   d_theory.eqNotifyNewClass(t);
 222 }
 223
 224 void TheorySets::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
 225 {
 226   Debug("sets-eq") << "[sets-eq] eqNotifyMerge:"
 227                    << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 228   d_theory.eqNotifyMerge(t1, t2);
 229 }
 230
 231 void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
 232 {
 233   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:"
 234                    << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
 235                    << std::endl;
 236   d_theory.eqNotifyDisequal(t1, t2, reason);
 237 }
 238
 239 }/* CVC4::theory::sets namespace */
 240 }/* CVC4::theory namespace */
 241 }/* CVC4 namespace */