src/theory/arith/theory_arith.cpp

   1 /*********************                                                        */
   2 /*! \file theory_arith.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Andrew Reynolds, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 "smt/smt_statistics_registry.h"
  22 #include "theory/arith/arith_rewriter.h"
  23 #include "theory/arith/infer_bounds.h"
  24 #include "theory/arith/theory_arith_private.h"
  25 #include "theory/ext_theory.h"
  26
  27 using namespace std;
  28 using namespace CVC4::kind;
  29
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace arith {
  33
  34 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
  35                          OutputChannel& out, Valuation valuation,
  36                          const LogicInfo& logicInfo)
  37     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
  38     , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
  39     , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
  40     , d_proofRecorder(nullptr)
  41 {
  42   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
  43   if (options::nlExt()) {
  44     setupExtTheory();
  45     getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT);
  46     getExtTheory()->addFunctionKind(kind::EXPONENTIAL);
  47     getExtTheory()->addFunctionKind(kind::SINE);
  48     getExtTheory()->addFunctionKind(kind::PI);
  49   }
  50 }
  51
  52 TheoryArith::~TheoryArith(){
  53   smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer);
  54   delete d_internal;
  55 }
  56
  57 TheoryRewriter* TheoryArith::getTheoryRewriter()
  58 {
  59   return d_internal->getTheoryRewriter();
  60 }
  61
  62 void TheoryArith::preRegisterTerm(TNode n){
  63   d_internal->preRegisterTerm(n);
  64 }
  65
  66 void TheoryArith::finishInit()
  67 {
  68   TheoryModel* tm = d_valuation.getModel();
  69   Assert(tm != nullptr);
  70   if (getLogicInfo().isTheoryEnabled(THEORY_ARITH)
  71       && getLogicInfo().areTranscendentalsUsed())
  72   {
  73     // witness is used to eliminate square root
  74     tm->setUnevaluatedKind(kind::WITNESS);
  75     // we only need to add the operators that are not syntax sugar
  76     tm->setUnevaluatedKind(kind::EXPONENTIAL);
  77     tm->setUnevaluatedKind(kind::SINE);
  78     tm->setUnevaluatedKind(kind::PI);
  79   }
  80 }
  81
  82 Node TheoryArith::expandDefinition(Node node)
  83 {
  84   return d_internal->expandDefinition(node);
  85 }
  86
  87 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  88   d_internal->setMasterEqualityEngine(eq);
  89 }
  90
  91 void TheoryArith::addSharedTerm(TNode n){
  92   d_internal->addSharedTerm(n);
  93 }
  94
  95 Node TheoryArith::ppRewrite(TNode atom) {
  96   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
  97   return d_internal->ppRewrite(atom);
  98 }
  99
 100 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
 101   return d_internal->ppAssert(in, outSubstitutions);
 102 }
 103
 104 void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 105   d_internal->ppStaticLearn(n, learned);
 106 }
 107
 108 void TheoryArith::check(Effort effortLevel){
 109   getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
 110   d_internal->check(effortLevel);
 111 }
 112
 113 bool TheoryArith::needsCheckLastEffort() {
 114   return d_internal->needsCheckLastEffort();
 115 }
 116
 117 Node TheoryArith::explain(TNode n) {
 118   return d_internal->explain(n);
 119 }
 120
 121 bool TheoryArith::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
 122   return d_internal->getCurrentSubstitution( effort, vars, subs, exp );
 123 }
 124
 125 bool TheoryArith::isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ) {
 126   return d_internal->isExtfReduced( effort, n, on, exp );
 127 }
 128
 129 void TheoryArith::propagate(Effort e) {
 130   d_internal->propagate(e);
 131 }
 132 bool TheoryArith::collectModelInfo(TheoryModel* m)
 133 {
 134   return d_internal->collectModelInfo(m);
 135 }
 136
 137 void TheoryArith::notifyRestart(){
 138   d_internal->notifyRestart();
 139 }
 140
 141 void TheoryArith::presolve(){
 142   d_internal->presolve();
 143 }
 144
 145 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
 146   return d_internal->getEqualityStatus(a,b);
 147 }
 148
 149 Node TheoryArith::getModelValue(TNode var) {
 150   return d_internal->getModelValue( var );
 151 }
 152
 153
 154 std::pair<bool, Node> TheoryArith::entailmentCheck (TNode lit,
 155                                                     const EntailmentCheckParameters* params,
 156                                                     EntailmentCheckSideEffects* out)
 157 {
 158   const ArithEntailmentCheckParameters* aparams = NULL;
 159   if(params == NULL){
 160     ArithEntailmentCheckParameters* def = new ArithEntailmentCheckParameters();
 161     def->addLookupRowSumAlgorithms();
 162     aparams = def;
 163   }else{
 164     AlwaysAssert(params->getTheoryId() == getId());
 165     aparams = dynamic_cast<const ArithEntailmentCheckParameters*>(params);
 166   }
 167   Assert(aparams != NULL);
 168
 169   ArithEntailmentCheckSideEffects* ase = NULL;
 170   if(out == NULL){
 171     ase = new ArithEntailmentCheckSideEffects();
 172   }else{
 173     AlwaysAssert(out->getTheoryId() == getId());
 174     ase = dynamic_cast<ArithEntailmentCheckSideEffects*>(out);
 175   }
 176   Assert(ase != NULL);
 177
 178   std::pair<bool, Node> res = d_internal->entailmentCheck(lit, *aparams, *ase);
 179
 180   if(params == NULL){
 181     delete aparams;
 182   }
 183   if(out == NULL){
 184     delete ase;
 185   }
 186
 187   return res;
 188 }
 189
 190 }/* CVC4::theory::arith namespace */
 191 }/* CVC4::theory namespace */
 192 }/* CVC4 namespace */