1 /********************* */
2 /*! \file proof_utils.h
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Guy Katz, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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
12 ** [[ Add lengthier description here ]]
14 ** \todo document this file
18 #include "cvc4_private.h"
24 #include <unordered_set>
27 #include "expr/node_manager.h"
31 typedef std::unordered_set
<Expr
, ExprHashFunction
> ExprSet
;
32 typedef std::unordered_set
<Node
, NodeHashFunction
> NodeSet
;
34 typedef std::pair
<Node
, Node
> NodePair
;
35 typedef std::set
<NodePair
> NodePairSet
;
40 static unsigned counter
;
41 static void resetCounter() { counter
= 0; }
42 static unsigned newId() { return ++counter
; }
51 void increment() { ++count
; }
52 ProofLetCount(unsigned i
)
57 ProofLetCount(const ProofLetCount
& other
)
62 bool operator==(const ProofLetCount
&other
) const {
63 return other
.id
== id
&& other
.count
== count
;
66 ProofLetCount
& operator=(const ProofLetCount
&rhs
) {
67 if (&rhs
== this) return *this;
74 struct LetOrderElement
{
77 LetOrderElement(Expr e
, unsigned i
)
88 typedef std::vector
<LetOrderElement
> Bindings
;
92 std::string
toLFSCKind(Kind kind
);
93 std::string
toLFSCKindTerm(Expr node
);
95 inline unsigned getExtractHigh(Expr node
) {
96 return node
.getOperator().getConst
<BitVectorExtract
>().high
;
99 inline unsigned getExtractLow(Expr node
) {
100 return node
.getOperator().getConst
<BitVectorExtract
>().low
;
103 inline unsigned getSize(Type type
) {
104 BitVectorType
bv(type
);
109 inline unsigned getSize(Expr node
) {
110 Assert (node
.getType().isBitVector());
111 return getSize(node
.getType());
114 inline Expr
mkTrue() {
115 return NodeManager::currentNM()->toExprManager()->mkConst
<bool>(true);
118 inline Expr
mkFalse() {
119 return NodeManager::currentNM()->toExprManager()->mkConst
<bool>(false);
122 inline Expr
mkExpr(Kind k
, Expr expr
) {
123 return NodeManager::currentNM()->toExprManager()->mkExpr(k
, expr
);
125 inline Expr
mkExpr(Kind k
, Expr e1
, Expr e2
) {
126 return NodeManager::currentNM()->toExprManager()->mkExpr(k
, e1
, e2
);
128 inline Expr
mkExpr(Kind k
, std::vector
<Expr
>& children
) {
129 return NodeManager::currentNM()->toExprManager()->mkExpr(k
, children
);
133 inline Expr
mkOnes(unsigned size
) {
134 BitVector val
= BitVector::mkOnes(size
);
135 return NodeManager::currentNM()->toExprManager()->mkConst
<BitVector
>(val
);
138 inline Expr
mkConst(unsigned size
, unsigned int value
) {
139 BitVector
val(size
, value
);
140 return NodeManager::currentNM()->toExprManager()->mkConst
<BitVector
>(val
);
143 inline Expr
mkConst(const BitVector
& value
) {
144 return NodeManager::currentNM()->toExprManager()->mkConst
<BitVector
>(value
);
147 inline Expr
mkOr(const std::vector
<Expr
>& nodes
) {
149 all
.insert(nodes
.begin(), nodes
.end());
150 Assert(all
.size() != 0 );
152 if (all
.size() == 1) {
153 // All the same, or just one
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
);
166 Node res
= disjunction
;
171 inline Expr
mkAnd(const std::vector
<Expr
>& conjunctions
) {
173 all
.insert(conjunctions
.begin(), conjunctions
.end());
175 if (all
.size() == 0) {
179 if (all
.size() == 1) {
180 // All the same, or just one
181 return conjunctions
[0];
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
);
193 Node res
= conjunction
;
197 inline Expr
mkSortedExpr(Kind kind
, const std::vector
<Expr
>& children
) {
199 all
.insert(children
.begin(), children
.end());
201 if (all
.size() == 0) {
205 if (all
.size() == 1) {
206 // All the same, or just one
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
);
219 return ((Node
)res
).toExpr();
220 }/* mkSortedNode() */
222 inline const bool getBit(Expr expr
, unsigned i
) {
223 Assert (i
< utils::getSize(expr
) &&
225 Integer bit
= expr
.getConst
<BitVector
>().extract(i
, i
).getValue();
229 void collectAtoms(TNode node
, std::set
<Node
>& seen
);