src/theory/sets/theory_sets.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sets.cpp
   3  ** \verbatim
   4  ** Original author: Kshitij Bansal
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2013-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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
  33 TheorySets::~TheorySets() {
  34   delete d_internal;
  35 }
  36
  37 void TheorySets::addSharedTerm(TNode n) {
  38   d_internal->addSharedTerm(n);
  39 }
  40
  41 void TheorySets::check(Effort e) {
  42   d_internal->check(e);
  43 }
  44
  45 void TheorySets::collectModelInfo(TheoryModel* m, bool fullModel) {
  46   d_internal->collectModelInfo(m, fullModel);
  47 }
  48
  49 void TheorySets::propagate(Effort e) {
  50   d_internal->propagate(e);
  51 }
  52
  53 Node TheorySets::explain(TNode node) {
  54   return d_internal->explain(node);
  55 }
  56
  57 void TheorySets::preRegisterTerm(TNode node) {
  58   return d_internal->preRegisterTerm(node);
  59 }
  60
  61 }/* CVC4::theory::sets namespace */
  62 }/* CVC4::theory namespace */
  63 }/* CVC4 namespace */