1 /********************* */
2 /*! \file theory_sets.cpp
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) 2009-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
12 ** \brief Sets theory.
17 #include "theory/sets/theory_sets.h"
18 #include "theory/sets/theory_sets_private.h"
24 TheorySets::TheorySets(context::Context
* c
,
25 context::UserContext
* u
,
28 const LogicInfo
& logicInfo
) :
29 Theory(THEORY_SETS
, c
, u
, out
, valuation
, logicInfo
),
30 d_internal(new TheorySetsPrivate(*this, c
, u
)) {
33 TheorySets::~TheorySets() {
37 void TheorySets::addSharedTerm(TNode n
) {
38 d_internal
->addSharedTerm(n
);
41 void TheorySets::check(Effort e
) {
42 if (done() && !fullEffort(e
)) {
48 void TheorySets::collectModelInfo(TheoryModel
* m
, bool fullModel
) {
49 d_internal
->collectModelInfo(m
, fullModel
);
52 void TheorySets::computeCareGraph() {
53 d_internal
->computeCareGraph();
56 Node
TheorySets::explain(TNode node
) {
57 return d_internal
->explain(node
);
60 EqualityStatus
TheorySets::getEqualityStatus(TNode a
, TNode b
) {
61 return d_internal
->getEqualityStatus(a
, b
);
64 Node
TheorySets::getModelValue(TNode node
) {
65 return d_internal
->getModelValue(node
);
68 void TheorySets::preRegisterTerm(TNode node
) {
69 d_internal
->preRegisterTerm(node
);
72 void TheorySets::propagate(Effort e
) {
73 d_internal
->propagate(e
);
76 void TheorySets::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
77 d_internal
->setMasterEqualityEngine(eq
);
80 }/* CVC4::theory::sets namespace */
81 }/* CVC4::theory namespace */