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 #include "theory/sets/theory_sets_private.h"
  19
  20 namespace CVC4 {
  21 namespace theory {
  22 namespace sets {
  23
  24 TheorySets::TheorySets(context::Context* c,
  25                        context::UserContext* u,
  26                        OutputChannel& out,
  27                        Valuation valuation,
  28                        const LogicInfo& logicInfo)
  29     : Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
  30       d_internal(new TheorySetsPrivate(*this, c, u))
  31 {
  32   // Do not move me to the header.
  33   // The constructor + destructor are not in the header as d_internal is a
  34   // unique_ptr<TheorySetsPrivate> and TheorySetsPrivate is an opaque type in
  35   // the header (Pimpl). See https://herbsutter.com/gotw/_100/ .
  36 }
  37
  38 TheorySets::~TheorySets()
  39 {
  40   // Do not move me to the header. See explanation in the constructor.
  41 }
  42
  43 void TheorySets::addSharedTerm(TNode n) {
  44   d_internal->addSharedTerm(n);
  45 }
  46
  47 void TheorySets::check(Effort e) {
  48   if (done() && e < Theory::EFFORT_FULL) {
  49     return;
  50   }
  51   TimerStat::CodeTimer checkTimer(d_checkTime);
  52   d_internal->check(e);
  53 }
  54
  55 bool TheorySets::collectModelInfo(TheoryModel* m)
  56 {
  57   return d_internal->collectModelInfo(m);
  58 }
  59
  60 void TheorySets::computeCareGraph() {
  61   d_internal->computeCareGraph();
  62 }
  63
  64 Node TheorySets::explain(TNode node) {
  65   return d_internal->explain(node);
  66 }
  67
  68 EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) {
  69   return d_internal->getEqualityStatus(a, b);
  70 }
  71
  72 Node TheorySets::getModelValue(TNode node) {
  73   return Node::null();
  74 }
  75
  76 void TheorySets::preRegisterTerm(TNode node) {
  77   d_internal->preRegisterTerm(node);
  78 }
  79
  80 Node TheorySets::expandDefinition(LogicRequest &logicRequest, Node n) {
  81   return d_internal->expandDefinition(logicRequest, n);
  82 }
  83
  84 Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
  85   return d_internal->ppAssert( in, outSubstitutions );
  86 }
  87
  88 void TheorySets::presolve() {
  89   d_internal->presolve();
  90 }
  91
  92 void TheorySets::propagate(Effort e) {
  93   d_internal->propagate(e);
  94 }
  95
  96 void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  97   d_internal->setMasterEqualityEngine(eq);
  98 }
  99
 100 bool TheorySets::isEntailed( Node n, bool pol ) {
 101   return d_internal->isEntailed( n, pol );
 102 }
 103
 104 }/* CVC4::theory::sets namespace */
 105 }/* CVC4::theory namespace */
 106 }/* CVC4 namespace */