src/proof/proof_utils.h

   1 /*********************                                                        */
   2 /*! \file proof_utils.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Guy Katz, 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  ** [[ Add lengthier description here ]]
  13
  14  ** \todo document this file
  15
  16 **/
  17
  18 #include "cvc4_private.h"
  19
  20 #pragma once
  21
  22 #include <set>
  23 #include <sstream>
  24 #include <unordered_set>
  25 #include <vector>
  26
  27 #include "expr/node_manager.h"
  28
  29 namespace CVC4 {
  30
  31 typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
  32 typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
  33
  34 typedef std::pair<Node, Node> NodePair;
  35 typedef std::set<NodePair> NodePairSet;
  36
  37
  38 class ProofLetCount {
  39 public:
  40   static unsigned counter;
  41   static void resetCounter() { counter = 0; }
  42   static unsigned newId() { return ++counter; }
  43
  44   unsigned count;
  45   unsigned id;
  46   ProofLetCount()
  47     : count(0)
  48     , id(-1)
  49   {}
  50
  51   void increment() { ++count; }
  52   ProofLetCount(unsigned i)
  53     : count(1)
  54     , id(i)
  55   {}
  56
  57   ProofLetCount(const ProofLetCount& other)
  58     : count(other.count)
  59     , id (other.id)
  60   {}
  61
  62   bool operator==(const ProofLetCount &other) const {
  63     return other.id == id && other.count == count;
  64   }
  65
  66   ProofLetCount& operator=(const ProofLetCount &rhs) {
  67     if (&rhs == this) return *this;
  68     id = rhs.id;
  69     count = rhs.count;
  70     return *this;
  71   }
  72 };
  73
  74 struct LetOrderElement {
  75   Expr expr;
  76   unsigned id;
  77   LetOrderElement(Expr e, unsigned i)
  78     : expr(e)
  79     , id(i)
  80   {}
  81
  82   LetOrderElement()
  83     : expr()
  84     , id(-1)
  85   {}
  86 };
  87
  88 typedef std::vector<LetOrderElement> Bindings;
  89
  90 namespace utils {
  91
  92 std::string toLFSCKind(Kind kind);
  93 std::string toLFSCKindTerm(Expr node);
  94
  95 inline unsigned getExtractHigh(Expr node) {
  96   return node.getOperator().getConst<BitVectorExtract>().d_high;
  97 }
  98
  99 inline unsigned getExtractLow(Expr node) {
 100   return node.getOperator().getConst<BitVectorExtract>().d_low;
 101 }
 102
 103 inline unsigned getSize(Type type) {
 104   BitVectorType bv(type);
 105   return bv.getSize();
 106 }
 107
 108
 109 inline unsigned getSize(Expr node) {
 110   Assert(node.getType().isBitVector());
 111   return getSize(node.getType());
 112 }
 113
 114 inline Expr mkTrue() {
 115   return NodeManager::currentNM()->toExprManager()->mkConst<bool>(true);
 116 }
 117
 118 inline Expr mkFalse() {
 119   return NodeManager::currentNM()->toExprManager()->mkConst<bool>(false);
 120 }
 121
 122 inline Expr mkExpr(Kind k , Expr expr) {
 123   return NodeManager::currentNM()->toExprManager()->mkExpr(k, expr);
 124 }
 125 inline Expr mkExpr(Kind k , Expr e1, Expr e2) {
 126   return NodeManager::currentNM()->toExprManager()->mkExpr(k, e1, e2);
 127 }
 128 inline Expr mkExpr(Kind k , std::vector<Expr>& children) {
 129   return NodeManager::currentNM()->toExprManager()->mkExpr(k, children);
 130 }
 131
 132
 133 inline Expr mkOnes(unsigned size) {
 134   BitVector val = BitVector::mkOnes(size);
 135   return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
 136 }
 137
 138 inline Expr mkConst(unsigned size, unsigned int value) {
 139   BitVector val(size, value);
 140   return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
 141 }
 142
 143 inline Expr mkConst(const BitVector& value) {
 144   return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(value);
 145 }
 146
 147 inline Expr mkOr(const std::vector<Expr>& nodes) {
 148   std::set<Expr> all;
 149   all.insert(nodes.begin(), nodes.end());
 150   Assert(all.size() != 0);
 151
 152   if (all.size() == 1) {
 153     // All the same, or just one
 154     return nodes[0];
 155   }
 156
 157
 158   NodeBuilder<> disjunction(kind::OR);
 159   std::set<Expr>::const_iterator it = all.begin();
 160   std::set<Expr>::const_iterator it_end = all.end();
 161   while (it != it_end) {
 162     disjunction << Node::fromExpr(*it);
 163     ++ it;
 164   }
 165
 166   Node res = disjunction;
 167   return res.toExpr();
 168 }/* mkOr() */
 169
 170
 171 inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
 172   std::set<Expr> all;
 173   all.insert(conjunctions.begin(), conjunctions.end());
 174
 175   if (all.size() == 0) {
 176     return mkTrue();
 177   }
 178
 179   if (all.size() == 1) {
 180     // All the same, or just one
 181     return conjunctions[0];
 182   }
 183
 184
 185   NodeBuilder<> conjunction(kind::AND);
 186   std::set<Expr>::const_iterator it = all.begin();
 187   std::set<Expr>::const_iterator it_end = all.end();
 188   while (it != it_end) {
 189     conjunction << Node::fromExpr(*it);
 190     ++ it;
 191   }
 192
 193   Node res = conjunction;
 194   return res.toExpr();
 195 }/* mkAnd() */
 196
 197 inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) {
 198   std::set<Expr> all;
 199   all.insert(children.begin(), children.end());
 200
 201   if (all.size() == 0) {
 202     return mkTrue();
 203   }
 204
 205   if (all.size() == 1) {
 206     // All the same, or just one
 207     return children[0];
 208   }
 209
 210
 211   NodeBuilder<> res(kind);
 212   std::set<Expr>::const_iterator it = all.begin();
 213   std::set<Expr>::const_iterator it_end = all.end();
 214   while (it != it_end) {
 215     res << Node::fromExpr(*it);
 216     ++ it;
 217   }
 218
 219   return ((Node)res).toExpr();
 220 }/* mkSortedNode() */
 221
 222 inline const bool getBit(Expr expr, unsigned i) {
 223   Assert(i < utils::getSize(expr) && expr.isConst());
 224   Integer bit = expr.getConst<BitVector>().extract(i, i).getValue();
 225   return (bit == 1u);
 226 }
 227
 228 }
 229 }