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, Martin Brain <>, Tianyi Liang, Dejan Jovanovic
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-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
  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
  20 #include "options/smt_options.h"
  21 #include "theory/arith/infer_bounds.h"
  22 #include "theory/arith/theory_arith_private.h"
  23
  24 using namespace std;
  25 using namespace CVC4::kind;
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace arith {
  30
  31 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
  32                          OutputChannel& out, Valuation valuation,
  33                          const LogicInfo& logicInfo, SmtGlobals* globals)
  34     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
  35     , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
  36 {}
  37
  38 TheoryArith::~TheoryArith(){
  39   delete d_internal;
  40 }
  41
  42 void TheoryArith::preRegisterTerm(TNode n){
  43   d_internal->preRegisterTerm(n);
  44 }
  45
  46 Node TheoryArith::expandDefinition(LogicRequest &logicRequest, Node node) {
  47   return d_internal->expandDefinition(logicRequest, node);
  48 }
  49
  50 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  51   d_internal->setMasterEqualityEngine(eq);
  52 }
  53
  54 void TheoryArith::setQuantifiersEngine(QuantifiersEngine* qe) {
  55   this->Theory::setQuantifiersEngine(qe);
  56   d_internal->setQuantifiersEngine(qe);
  57 }
  58
  59 void TheoryArith::addSharedTerm(TNode n){
  60   d_internal->addSharedTerm(n);
  61 }
  62
  63 Node TheoryArith::ppRewrite(TNode atom) {
  64   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
  65   return d_internal->ppRewrite(atom);
  66 }
  67
  68 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
  69   return d_internal->ppAssert(in, outSubstitutions);
  70 }
  71
  72 void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
  73   d_internal->ppStaticLearn(n, learned);
  74 }
  75
  76 void TheoryArith::check(Effort effortLevel){
  77   getOutputChannel().spendResource(options::theoryCheckStep());
  78   d_internal->check(effortLevel);
  79 }
  80
  81 Node TheoryArith::explain(TNode n) {
  82   return d_internal->explain(n);
  83 }
  84
  85 void TheoryArith::propagate(Effort e) {
  86   d_internal->propagate(e);
  87 }
  88
  89 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
  90   d_internal->collectModelInfo(m, fullModel);
  91 }
  92
  93 void TheoryArith::notifyRestart(){
  94   d_internal->notifyRestart();
  95 }
  96
  97 void TheoryArith::presolve(){
  98   d_internal->presolve();
  99 }
 100
 101 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
 102   return d_internal->getEqualityStatus(a,b);
 103 }
 104
 105 Node TheoryArith::getModelValue(TNode var) {
 106   return d_internal->getModelValue( var );
 107 }
 108
 109
 110 std::pair<bool, Node> TheoryArith::entailmentCheck (TNode lit,
 111                                                     const EntailmentCheckParameters* params,
 112                                                     EntailmentCheckSideEffects* out)
 113 {
 114   const ArithEntailmentCheckParameters* aparams = NULL;
 115   if(params == NULL){
 116     ArithEntailmentCheckParameters* def = new ArithEntailmentCheckParameters();
 117     def->addLookupRowSumAlgorithms();
 118     aparams = def;
 119   }else{
 120     AlwaysAssert(params->getTheoryId() == getId());
 121     aparams = dynamic_cast<const ArithEntailmentCheckParameters*>(params);
 122   }
 123   Assert(aparams != NULL);
 124
 125   ArithEntailmentCheckSideEffects* ase = NULL;
 126   if(out == NULL){
 127     ase = new ArithEntailmentCheckSideEffects();
 128   }else{
 129     AlwaysAssert(out->getTheoryId() == getId());
 130     ase = dynamic_cast<ArithEntailmentCheckSideEffects*>(out);
 131   }
 132   Assert(ase != NULL);
 133
 134   std::pair<bool, Node> res = d_internal->entailmentCheck(lit, *aparams, *ase);
 135
 136   if(params == NULL){
 137     delete aparams;
 138   }
 139   if(out == NULL){
 140     delete ase;
 141   }
 142
 143   return res;
 144 }
 145
 146 }/* CVC4::theory::arith namespace */
 147 }/* CVC4::theory namespace */
 148 }/* CVC4 namespace */