src/theory/arith/arith_prop_manager.cpp

   1
   2 #include "theory/arith/arith_prop_manager.h"
   3
   4 #include "theory/arith/arith_utilities.h"
   5 #include "context/context.h"
   6 #include "context/cdlist.h"
   7 #include "context/cdmap.h"
   8 #include "context/cdo.h"
   9
  10 using namespace CVC4;
  11 using namespace CVC4::theory;
  12 using namespace CVC4::theory::arith;
  13 using namespace CVC4::kind;
  14 using namespace std;
  15
  16
  17 bool ArithPropManager::isAsserted(TNode n) const{
  18   Node satValue = d_valuation.getSatValue(n);
  19   if(satValue.isNull()){
  20     return false;
  21   }else{
  22     //Assert(satValue.getConst<bool>());
  23     return true;
  24   }
  25 }
  26
  27 // Node ArithPropManager::strictlyWeakerAssertedUpperBound(TNode n) const{
  28 //   Node weaker = n;
  29 //   do {
  30 //     weaker = d_propagator.getWeakerImpliedUpperBound(weaker);
  31 //   }while(!weaker.isNull() && !isAsserted(weaker));
  32 //   Assert(weaker != n);
  33 //   return weaker;
  34 // }
  35
  36 // Node ArithPropManager::strictlyWeakerAssertedLowerBound(TNode n) const{
  37 //   Node weaker = n;
  38 //   do {
  39 //     weaker = d_propagator.getWeakerImpliedLowerBound(weaker);
  40 //   }while(!weaker.isNull() && !isAsserted(weaker));
  41 //   Assert(weaker != n);
  42 //   return weaker;
  43 // }
  44
  45 Node ArithPropManager::strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const{
  46   Node bound = boundAsNode(true, v, b);
  47
  48   Assert(b.getInfinitesimalPart() <= 0);
  49   bool largeEpsilon = (b.getInfinitesimalPart() < -1);
  50
  51   Node weaker = bound;
  52   do {
  53     if(largeEpsilon){
  54       weaker = d_propagator.getBestImpliedUpperBound(weaker);
  55       largeEpsilon = false;
  56     }else{
  57       weaker = d_propagator.getWeakerImpliedUpperBound(weaker);
  58     }
  59   }while(!weaker.isNull() && !isAsserted(weaker));
  60   return weaker;
  61 }
  62
  63 Node ArithPropManager::strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaRational& b) const{
  64   Debug("ArithPropManager") << "strictlyWeakerAssertedLowerBound" << endl;
  65   Node bound = boundAsNode(false, v, b);
  66
  67   Assert(b.getInfinitesimalPart() >= 0);
  68   bool largeEpsilon = (b.getInfinitesimalPart() > 1);
  69
  70   Node weaker = bound;
  71   Debug("ArithPropManager") << bound << b << endl;
  72   do {
  73     if(largeEpsilon){
  74       weaker = d_propagator.getBestImpliedLowerBound(weaker);
  75       largeEpsilon = false;
  76     }else{
  77       weaker = d_propagator.getWeakerImpliedLowerBound(weaker);
  78     }
  79   }while(!weaker.isNull() && !isAsserted(weaker));
  80   Debug("ArithPropManager") << "res: " << weaker << endl;
  81   return weaker;
  82 }
  83
  84 Node ArithPropManager::getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const{
  85   Node bound = boundAsNode(false, v, b);
  86   return d_propagator.getBestImpliedLowerBound(bound);
  87 }
  88 Node ArithPropManager::getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const{
  89   Node bound = boundAsNode(true, v, b);
  90   return d_propagator.getBestImpliedUpperBound(bound);
  91 }
  92
  93 bool ArithPropManager::hasStrongerLowerBound(TNode n) const{
  94   bool haveAcompilerWarning;
  95   return true;
  96 }
  97 bool ArithPropManager::hasStrongerUpperBound(TNode n) const{
  98   return true;
  99 }
 100
 101 Node ArithPropManager::boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const {
 102   Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) );
 103   Assert(upperbound || (b.getInfinitesimalPart() >= 0) );
 104
 105   Node varAsNode = d_arithvarNodeMap.asNode(var);
 106   Kind kind;
 107   bool negate;
 108   if(upperbound){
 109     negate = b.getInfinitesimalPart() < 0;
 110     kind = negate ? GEQ : LEQ;
 111   } else{
 112     negate = b.getInfinitesimalPart() > 0;
 113     kind = negate ? LEQ : GEQ;
 114   }
 115
 116   Node righthand = mkRationalNode(b.getNoninfinitesimalPart());
 117   Node bAsNode = NodeBuilder<2>(kind) << varAsNode << righthand;
 118
 119   if(negate){
 120     bAsNode = NodeBuilder<1>(NOT) << bAsNode;
 121   }
 122
 123   return bAsNode;
 124 }
 125
 126 bool ArithPropManager::propagateArithVar(bool upperbound, ArithVar var, const DeltaRational& b, TNode reason){
 127   bool success = false;
 128
 129   ++d_statistics.d_propagateArithVarCalls;
 130
 131   Node bAsNode = boundAsNode(upperbound, var ,b);
 132
 133   Node bestImplied = upperbound ?
 134     d_propagator.getBestImpliedUpperBound(bAsNode):
 135     d_propagator.getBestImpliedLowerBound(bAsNode);
 136
 137   Debug("ArithPropManager") << upperbound <<","<< var <<","<< b <<","<< reason << endl
 138                             << bestImplied << endl;
 139
 140   if(!bestImplied.isNull()){
 141     bool asserted = isAsserted(bestImplied);
 142
 143     if( !asserted && !isPropagated(bestImplied)){
 144       propagate(bestImplied, reason);
 145       ++d_statistics.d_addedPropagation;
 146       success = true;
 147     }else if(!asserted){
 148       ++d_statistics.d_alreadyPropagatedNode;
 149     }else if(!isPropagated(bestImplied)){
 150       ++d_statistics.d_alreadySetSatLiteral;
 151     }
 152   }
 153   return success;
 154 }
 155
 156 ArithPropManager::Statistics::Statistics():
 157   d_propagateArithVarCalls("arith::prop-manager::propagateArithVarCalls",0),
 158   d_addedPropagation("arith::prop-manager::addedPropagation",0),
 159   d_alreadySetSatLiteral("arith::prop-manager::alreadySetSatLiteral",0),
 160   d_alreadyPropagatedNode("arith::prop-manager::alreadyPropagatedNode",0)
 161 {
 162   StatisticsRegistry::registerStat(&d_propagateArithVarCalls);
 163   StatisticsRegistry::registerStat(&d_alreadySetSatLiteral);
 164   StatisticsRegistry::registerStat(&d_alreadyPropagatedNode);
 165   StatisticsRegistry::registerStat(&d_addedPropagation);
 166 }
 167
 168 ArithPropManager::Statistics::~Statistics()
 169 {
 170   StatisticsRegistry::unregisterStat(&d_propagateArithVarCalls);
 171   StatisticsRegistry::unregisterStat(&d_alreadySetSatLiteral);
 172   StatisticsRegistry::unregisterStat(&d_alreadyPropagatedNode);
 173   StatisticsRegistry::unregisterStat(&d_addedPropagation);
 174 }