src/theory/arith/theory_arith.cpp

   1 /*********************                                                        */
   2 /*! \file theory_arith.cpp
   3  ** \verbatim
   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
  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, QuantifiersEngine* qe)
  29   : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe)
  30   , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, qe))
  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::addSharedTerm(TNode n){
  46   d_internal->addSharedTerm(n);
  47 }
  48
  49 Node TheoryArith::ppRewrite(TNode atom) {
  50   CodeTimer timer(d_ppRewriteTimer);
  51   return d_internal->ppRewrite(atom);
  52 }
  53
  54 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
  55   return d_internal->ppAssert(in, outSubstitutions);
  56 }
  57
  58 void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
  59   d_internal->ppStaticLearn(n, learned);
  60 }
  61
  62 void TheoryArith::check(Effort effortLevel){
  63   d_internal->check(effortLevel);
  64 }
  65
  66 Node TheoryArith::explain(TNode n) {
  67   return d_internal->explain(n);
  68 }
  69
  70 void TheoryArith::propagate(Effort e) {
  71   d_internal->propagate(e);
  72 }
  73
  74 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
  75   d_internal->collectModelInfo(m, fullModel);
  76 }
  77
  78 void TheoryArith::notifyRestart(){
  79   d_internal->notifyRestart();
  80 }
  81
  82 void TheoryArith::presolve(){
  83   d_internal->presolve();
  84 }
  85
  86 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
  87   return d_internal->getEqualityStatus(a,b);
  88 }
  89
  90 }/* CVC4::theory::arith namespace */
  91 }/* CVC4::theory namespace */
  92 }/* CVC4 namespace */