src/theory/arith/arith_static_learner.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Dejan Jovanovic, Andres Noetzli
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * [[ Add one-line brief description here ]]
  14  *
  15  * [[ Add lengthier description here ]]
  16  * \todo document this file
  17  */
  18
  19 #include <vector>
  20
  21 #include "base/output.h"
  22 #include "expr/node_algorithm.h"
  23 #include "options/arith_options.h"
  24 #include "smt/smt_statistics_registry.h"
  25 #include "theory/arith/arith_static_learner.h"
  26 #include "theory/arith/arith_utilities.h"
  27 #include "theory/arith/normal_form.h"
  28 #include "theory/rewriter.h"
  29
  30 using namespace std;
  31 using namespace cvc5::kind;
  32
  33 namespace cvc5 {
  34 namespace theory {
  35 namespace arith {
  36
  37
  38 ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
  39   d_minMap(userContext),
  40   d_maxMap(userContext),
  41   d_statistics()
  42 {
  43 }
  44
  45 ArithStaticLearner::~ArithStaticLearner(){
  46 }
  47
  48 ArithStaticLearner::Statistics::Statistics()
  49     : d_iteMinMaxApplications(smtStatisticsRegistry().registerInt(
  50         "theory::arith::iteMinMaxApplications")),
  51       d_iteConstantApplications(smtStatisticsRegistry().registerInt(
  52           "theory::arith::iteConstantApplications"))
  53 {
  54 }
  55
  56 void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned)
  57 {
  58   vector<TNode> workList;
  59   workList.push_back(n);
  60   TNodeSet processed;
  61
  62   //Contains an underapproximation of nodes that must hold.
  63   TNodeSet defTrue;
  64
  65   defTrue.insert(n);
  66
  67   while(!workList.empty()) {
  68     n = workList.back();
  69
  70     bool unprocessedChildren = false;
  71     for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
  72       if(processed.find(*i) == processed.end()) {
  73         // unprocessed child
  74         workList.push_back(*i);
  75         unprocessedChildren = true;
  76       }
  77     }
  78     if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
  79       for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
  80         defTrue.insert(*i);
  81       }
  82     }
  83
  84     if(unprocessedChildren) {
  85       continue;
  86     }
  87
  88     workList.pop_back();
  89     // has node n been processed in the meantime ?
  90     if(processed.find(n) != processed.end()) {
  91       continue;
  92     }
  93     processed.insert(n);
  94
  95     process(n,learned, defTrue);
  96
  97   }
  98 }
  99
 100 void ArithStaticLearner::process(TNode n,
 101                                  NodeBuilder& learned,
 102                                  const TNodeSet& defTrue)
 103 {
 104   Debug("arith::static") << "===================== looking at " << n << endl;
 105
 106   switch(n.getKind()){
 107   case ITE:
 108     if (expr::hasBoundVar(n))
 109     {
 110       // Unsafe with non-ground ITEs; do nothing
 111       Debug("arith::static")
 112           << "(potentially) non-ground ITE, ignoring..." << endl;
 113       break;
 114     }
 115
 116     if(n[0].getKind() != EQUAL &&
 117        isRelationOperator(n[0].getKind())  ){
 118       iteMinMax(n, learned);
 119     }
 120
 121     if((d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) ||
 122        (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end())) {
 123       iteConstant(n, learned);
 124     }
 125     break;
 126
 127   case CONST_RATIONAL:
 128     // Mark constants as minmax
 129     d_minMap.insert(n, n.getConst<Rational>());
 130     d_maxMap.insert(n, n.getConst<Rational>());
 131     break;
 132   default: // Do nothing
 133     break;
 134   }
 135 }
 136
 137 void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder& learned)
 138 {
 139   Assert(n.getKind() == kind::ITE);
 140   Assert(n[0].getKind() != EQUAL);
 141   Assert(isRelationOperator(n[0].getKind()));
 142
 143   TNode c = n[0];
 144   Kind k = oldSimplifiedKind(c);
 145   TNode t = n[1];
 146   TNode e = n[2];
 147   TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
 148   TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
 149
 150   if((t == cright) && (e == cleft)){
 151     TNode tmp = t;
 152     t = e;
 153     e = tmp;
 154     k = reverseRelationKind(k);
 155   }
 156   //(ite (< x y) x y)
 157   //(ite (x < y) x y)
 158   //(ite (x - y < 0) x y)
 159   // ----------------
 160   // (ite (x - y < -c) )
 161
 162   if(t == cleft && e == cright){
 163     // t == cleft && e == cright
 164     Assert(t == cleft);
 165     Assert(e == cright);
 166     switch(k){
 167     case LT:   // (ite (< x y) x y)
 168     case LEQ: { // (ite (<= x y) x y)
 169       Node nLeqX = NodeBuilder(LEQ) << n << t;
 170       Node nLeqY = NodeBuilder(LEQ) << n << e;
 171       Debug("arith::static") << n << "is a min =>"  << nLeqX << nLeqY << endl;
 172       learned << nLeqX << nLeqY;
 173       ++(d_statistics.d_iteMinMaxApplications);
 174       break;
 175     }
 176     case GT: // (ite (> x y) x y)
 177     case GEQ: { // (ite (>= x y) x y)
 178       Node nGeqX = NodeBuilder(GEQ) << n << t;
 179       Node nGeqY = NodeBuilder(GEQ) << n << e;
 180       Debug("arith::static") << n << "is a max =>"  << nGeqX << nGeqY << endl;
 181       learned << nGeqX << nGeqY;
 182       ++(d_statistics.d_iteMinMaxApplications);
 183       break;
 184     }
 185     default: Unreachable();
 186     }
 187   }
 188 }
 189
 190 void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned)
 191 {
 192   Assert(n.getKind() == ITE);
 193
 194   Debug("arith::static") << "iteConstant(" << n << ")" << endl;
 195
 196   if (d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) {
 197     const DeltaRational& first = d_minMap[n[1]];
 198     const DeltaRational& second = d_minMap[n[2]];
 199     DeltaRational min = std::min(first, second);
 200     CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
 201     if (minFind == d_minMap.end() || (*minFind).second < min) {
 202       d_minMap.insert(n, min);
 203       NodeManager* nm = NodeManager::currentNM();
 204       Node nGeqMin = nm->mkNode(
 205           min.getInfinitesimalPart() == 0 ? kind::GEQ : kind::GT,
 206           n,
 207           nm->mkConstRealOrInt(n.getType(), min.getNoninfinitesimalPart()));
 208       learned << nGeqMin;
 209       Debug("arith::static") << n << " iteConstant"  << nGeqMin << endl;
 210       ++(d_statistics.d_iteConstantApplications);
 211     }
 212   }
 213
 214   if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) {
 215     const DeltaRational& first = d_maxMap[n[1]];
 216     const DeltaRational& second = d_maxMap[n[2]];
 217     DeltaRational max = std::max(first, second);
 218     CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
 219     if (maxFind == d_maxMap.end() || (*maxFind).second > max) {
 220       d_maxMap.insert(n, max);
 221       NodeManager* nm = NodeManager::currentNM();
 222       Node nLeqMax = nm->mkNode(
 223           max.getInfinitesimalPart() == 0 ? kind::LEQ : kind::LT,
 224           n,
 225           nm->mkConstRealOrInt(n.getType(), max.getNoninfinitesimalPart()));
 226       learned << nLeqMax;
 227       Debug("arith::static") << n << " iteConstant"  << nLeqMax << endl;
 228       ++(d_statistics.d_iteConstantApplications);
 229     }
 230   }
 231 }
 232
 233 std::set<Node> listToSet(TNode l){
 234   std::set<Node> ret;
 235   while(l.getKind() == OR){
 236     Assert(l.getNumChildren() == 2);
 237     ret.insert(l[0]);
 238     l = l[1];
 239   }
 240   return ret;
 241 }
 242
 243 void ArithStaticLearner::addBound(TNode n) {
 244
 245   CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n[0]);
 246   CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n[0]);
 247
 248   Rational constant = n[1].getConst<Rational>();
 249   DeltaRational bound = constant;
 250
 251   switch(Kind k = n.getKind()) {
 252     case kind::LT: bound = DeltaRational(constant, -1); CVC5_FALLTHROUGH;
 253     case kind::LEQ:
 254       if (maxFind == d_maxMap.end() || (*maxFind).second > bound)
 255       {
 256         d_maxMap.insert(n[0], bound);
 257         Debug("arith::static") << "adding bound " << n << endl;
 258       }
 259       break;
 260     case kind::GT: bound = DeltaRational(constant, 1); CVC5_FALLTHROUGH;
 261     case kind::GEQ:
 262       if (minFind == d_minMap.end() || (*minFind).second < bound)
 263       {
 264         d_minMap.insert(n[0], bound);
 265         Debug("arith::static") << "adding bound " << n << endl;
 266       }
 267       break;
 268     default: Unhandled() << k; break;
 269   }
 270 }
 271
 272 }  // namespace arith
 273 }  // namespace theory
 274 }  // namespace cvc5