1 /********************* */
2 /*! \file theory_arith.cpp
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 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 [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/arith/theory_arith.h"
19 #include "theory/arith/theory_arith_private.h"
22 using namespace CVC4::kind
;
28 TheoryArith::TheoryArith(context::Context
* c
, context::UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
, QuantifiersEngine
* qe
)
29 : Theory(THEORY_ARITH
, c
, u
, out
, valuation
, logicInfo
, qe
)
30 , d_internal(new TheoryArithPrivate(*this, c
, u
, out
, valuation
, logicInfo
, qe
))
33 TheoryArith::~TheoryArith(){
37 void TheoryArith::preRegisterTerm(TNode n
){
38 d_internal
->preRegisterTerm(n
);
41 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
42 d_internal
->setMasterEqualityEngine(eq
);
45 void TheoryArith::addSharedTerm(TNode n
){
46 d_internal
->addSharedTerm(n
);
49 Node
TheoryArith::ppRewrite(TNode atom
) {
50 CodeTimer
timer(d_ppRewriteTimer
);
51 return d_internal
->ppRewrite(atom
);
54 Theory::PPAssertStatus
TheoryArith::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
55 return d_internal
->ppAssert(in
, outSubstitutions
);
58 void TheoryArith::ppStaticLearn(TNode n
, NodeBuilder
<>& learned
) {
59 d_internal
->ppStaticLearn(n
, learned
);
62 void TheoryArith::check(Effort effortLevel
){
63 d_internal
->check(effortLevel
);
66 Node
TheoryArith::explain(TNode n
) {
67 return d_internal
->explain(n
);
70 void TheoryArith::propagate(Effort e
) {
71 d_internal
->propagate(e
);
74 void TheoryArith::collectModelInfo( TheoryModel
* m
, bool fullModel
){
75 d_internal
->collectModelInfo(m
, fullModel
);
78 void TheoryArith::notifyRestart(){
79 d_internal
->notifyRestart();
82 void TheoryArith::presolve(){
83 d_internal
->presolve();
86 EqualityStatus
TheoryArith::getEqualityStatus(TNode a
, TNode b
) {
87 return d_internal
->getEqualityStatus(a
,b
);
90 }/* CVC4::theory::arith namespace */
91 }/* CVC4::theory namespace */