diff options
Diffstat (limited to 'src/proof/proof_utils.h')
-rw-r--r-- | src/proof/proof_utils.h | 105 |
1 files changed, 80 insertions, 25 deletions
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index da10c33a0..546d419fc 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -17,7 +17,7 @@ #include "cvc4_private.h" -#pragma once +#pragma once #include <set> #include <vector> @@ -29,6 +29,61 @@ namespace CVC4 { typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet; typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::pair<Node, Node> NodePair; +typedef std::set<NodePair> NodePairSet; + + +struct ProofLetCount { + static unsigned counter; + static void resetCounter() { counter = 0; } + static unsigned newId() { return ++counter; } + + unsigned count; + unsigned id; + ProofLetCount() + : count(0) + , id(-1) + {} + + void increment() { ++count; } + ProofLetCount(unsigned i) + : count(1) + , id(i) + {} + + ProofLetCount(const ProofLetCount& other) + : count(other.count) + , id (other.id) + {} + + bool operator==(const ProofLetCount &other) const { + return other.id == id && other.count == count; + } + + ProofLetCount& operator=(const ProofLetCount &rhs) { + if (&rhs == this) return *this; + id = rhs.id; + count = rhs.count; + return *this; + } +}; + +struct LetOrderElement { + Expr expr; + unsigned id; + LetOrderElement(Expr e, unsigned i) + : expr(e) + , id(i) + {} + + LetOrderElement() + : expr() + , id(-1) + {} +}; + +typedef std::vector<LetOrderElement> Bindings; + namespace utils { std::string toLFSCKind(Kind kind); @@ -42,7 +97,7 @@ inline unsigned getExtractLow(Expr node) { } inline unsigned getSize(Type type) { - BitVectorType bv(type); + BitVectorType bv(type); return bv.getSize(); } @@ -60,8 +115,8 @@ inline Expr mkFalse() { return NodeManager::currentNM()->toExprManager()->mkConst<bool>(false); } inline BitVector mkBitVectorOnes(unsigned size) { - Assert(size > 0); - return BitVector(1, Integer(1)).signExtend(size - 1); + Assert(size > 0); + return BitVector(1, Integer(1)).signExtend(size - 1); } inline Expr mkExpr(Kind k , Expr expr) { @@ -73,16 +128,16 @@ inline Expr mkExpr(Kind k , Expr e1, Expr e2) { inline Expr mkExpr(Kind k , std::vector<Expr>& children) { return NodeManager::currentNM()->toExprManager()->mkExpr(k, children); } - - + + inline Expr mkOnes(unsigned size) { - BitVector val = mkBitVectorOnes(size); - return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); + BitVector val = mkBitVectorOnes(size); + return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); } inline Expr mkConst(unsigned size, unsigned int value) { BitVector val(size, value); - return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); + return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); } inline Expr mkConst(const BitVector& value) { @@ -92,14 +147,14 @@ inline Expr mkConst(const BitVector& value) { inline Expr mkOr(const std::vector<Expr>& nodes) { std::set<Expr> all; all.insert(nodes.begin(), nodes.end()); - Assert(all.size() != 0 ); + Assert(all.size() != 0 ); if (all.size() == 1) { // All the same, or just one return nodes[0]; } - - + + NodeBuilder<> disjunction(kind::OR); std::set<Expr>::const_iterator it = all.begin(); std::set<Expr>::const_iterator it_end = all.end(); @@ -109,23 +164,23 @@ inline Expr mkOr(const std::vector<Expr>& nodes) { } Node res = disjunction; - return res.toExpr(); + return res.toExpr(); }/* mkOr() */ - + inline Expr mkAnd(const std::vector<Expr>& conjunctions) { std::set<Expr> all; all.insert(conjunctions.begin(), conjunctions.end()); if (all.size() == 0) { - return mkTrue(); + return mkTrue(); } - + if (all.size() == 1) { // All the same, or just one return conjunctions[0]; } - + NodeBuilder<> conjunction(kind::AND); std::set<Expr>::const_iterator it = all.begin(); @@ -135,7 +190,7 @@ inline Expr mkAnd(const std::vector<Expr>& conjunctions) { ++ it; } - Node res = conjunction; + Node res = conjunction; return res.toExpr(); }/* mkAnd() */ @@ -144,14 +199,14 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) { all.insert(children.begin(), children.end()); if (all.size() == 0) { - return mkTrue(); + return mkTrue(); } - + if (all.size() == 1) { // All the same, or just one return children[0]; } - + NodeBuilder<> res(kind); std::set<Expr>::const_iterator it = all.begin(); @@ -165,13 +220,13 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) { }/* mkSortedNode() */ inline const bool getBit(Expr expr, unsigned i) { - Assert (i < utils::getSize(expr) && - expr.isConst()); + Assert (i < utils::getSize(expr) && + expr.isConst()); Integer bit = expr.getConst<BitVector>().extract(i, i).getValue(); - return (bit == 1u); + return (bit == 1u); } -void collectAtoms(TNode node, NodeSet& seen); +void collectAtoms(TNode node, std::set<Node>& seen); } |