src/theory/arith/theory_arith.cpp

   1 /*********************                                                        */
   2 /*! \file theory_arith.cpp
   3  ** \verbatim
   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
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "theory/arith/theory_arith.h"
  19 #include "theory/arith/theory_arith_private.h"
  20
  21 using namespace std;
  22 using namespace CVC4::kind;
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace arith {
  27
  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))
  31 {}
  32
  33 TheoryArith::~TheoryArith(){
  34   delete d_internal;
  35 }
  36
  37 void TheoryArith::preRegisterTerm(TNode n){
  38   d_internal->preRegisterTerm(n);
  39 }
  40
  41 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  42   d_internal->setMasterEqualityEngine(eq);
  43 }
  44
  45 void TheoryArith::setQuantifiersEngine(QuantifiersEngine* qe) {
  46   this->Theory::setQuantifiersEngine(qe);
  47   d_internal->setQuantifiersEngine(qe);
  48 }
  49
  50 void TheoryArith::addSharedTerm(TNode n){
  51   d_internal->addSharedTerm(n);
  52 }
  53
  54 Node TheoryArith::ppRewrite(TNode atom) {
  55   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
  56   return d_internal->ppRewrite(atom);
  57 }
  58
  59 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
  60   return d_internal->ppAssert(in, outSubstitutions);
  61 }
  62
  63 void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
  64   d_internal->ppStaticLearn(n, learned);
  65 }
  66
  67 void TheoryArith::check(Effort effortLevel){
  68   d_internal->check(effortLevel);
  69 }
  70
  71 Node TheoryArith::explain(TNode n) {
  72   return d_internal->explain(n);
  73 }
  74
  75 void TheoryArith::propagate(Effort e) {
  76   d_internal->propagate(e);
  77 }
  78
  79 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
  80   d_internal->collectModelInfo(m, fullModel);
  81 }
  82
  83 void TheoryArith::notifyRestart(){
  84   d_internal->notifyRestart();
  85 }
  86
  87 void TheoryArith::presolve(){
  88   d_internal->presolve();
  89 }
  90
  91 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
  92   return d_internal->getEqualityStatus(a,b);
  93 }
  94
  95 Node TheoryArith::getModelValue(TNode var) {
  96   return d_internal->getModelValue( var );
  97 }
  98
  99 }/* CVC4::theory::arith namespace */
 100 }/* CVC4::theory namespace */
 101 }/* CVC4 namespace */