1 /********************* */
2 /*! \file theory_arith.cpp
4 ** Original author: Tim King
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Andrew Reynolds, Tianyi Liang, Dejan Jovanovic
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 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
)
29 : Theory(THEORY_ARITH
, c
, u
, out
, valuation
, logicInfo
)
30 , d_internal(new TheoryArithPrivate(*this, c
, u
, out
, valuation
, logicInfo
))
33 TheoryArith::~TheoryArith(){
37 void TheoryArith::preRegisterTerm(TNode n
){
38 d_internal
->preRegisterTerm(n
);
41 Node
TheoryArith::expandDefinition(LogicRequest
&logicRequest
, Node node
) {
42 return d_internal
->expandDefinition(logicRequest
, node
);
45 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
46 d_internal
->setMasterEqualityEngine(eq
);
49 void TheoryArith::setQuantifiersEngine(QuantifiersEngine
* qe
) {
50 this->Theory::setQuantifiersEngine(qe
);
51 d_internal
->setQuantifiersEngine(qe
);
54 void TheoryArith::addSharedTerm(TNode n
){
55 d_internal
->addSharedTerm(n
);
58 Node
TheoryArith::ppRewrite(TNode atom
) {
59 CodeTimer
timer(d_ppRewriteTimer
, /* allow_reentrant = */ true);
60 return d_internal
->ppRewrite(atom
);
63 Theory::PPAssertStatus
TheoryArith::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
64 return d_internal
->ppAssert(in
, outSubstitutions
);
67 void TheoryArith::ppStaticLearn(TNode n
, NodeBuilder
<>& learned
) {
68 d_internal
->ppStaticLearn(n
, learned
);
71 void TheoryArith::check(Effort effortLevel
){
72 d_internal
->check(effortLevel
);
75 Node
TheoryArith::explain(TNode n
) {
76 return d_internal
->explain(n
);
79 void TheoryArith::propagate(Effort e
) {
80 d_internal
->propagate(e
);
83 void TheoryArith::collectModelInfo( TheoryModel
* m
, bool fullModel
){
84 d_internal
->collectModelInfo(m
, fullModel
);
87 void TheoryArith::notifyRestart(){
88 d_internal
->notifyRestart();
91 void TheoryArith::presolve(){
92 d_internal
->presolve();
95 EqualityStatus
TheoryArith::getEqualityStatus(TNode a
, TNode b
) {
96 return d_internal
->getEqualityStatus(a
,b
);
99 Node
TheoryArith::getModelValue(TNode var
) {
100 return d_internal
->getModelValue( var
);
103 }/* CVC4::theory::arith namespace */
104 }/* CVC4::theory namespace */
105 }/* CVC4 namespace */