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) 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
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
) {
45 void TheorySets::collectModelInfo(TheoryModel
* m
, bool fullModel
) {
46 d_internal
->collectModelInfo(m
, fullModel
);
49 void TheorySets::computeCareGraph() {
50 d_internal
->computeCareGraph();
53 Node
TheorySets::explain(TNode node
) {
54 return d_internal
->explain(node
);
57 void TheorySets::preRegisterTerm(TNode node
) {
58 d_internal
->preRegisterTerm(node
);
61 void TheorySets::propagate(Effort e
) {
62 d_internal
->propagate(e
);
65 void TheorySets::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
66 d_internal
->setMasterEqualityEngine(eq
);
69 }/* CVC4::theory::sets namespace */
70 }/* CVC4::theory namespace */