1 /********************* */
2 /*! \file proof_utils.cpp
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Guy Katz, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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 "proof/proof_utils.h"
19 #include "theory/theory.h"
24 void collectAtoms(TNode node
, std::set
<Node
>& seen
) {
25 if (seen
.find(node
) != seen
.end())
27 if (theory::Theory::theoryOf(node
) != theory::THEORY_BOOL
|| node
.isVar()) {
32 for (unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
33 collectAtoms(node
[i
], seen
);
37 std::string
toLFSCKind(Kind kind
) {
40 case kind::OR
: return "or";
41 case kind::AND
: return "and";
42 case kind::XOR
: return "xor";
43 case kind::EQUAL
: return "=";
44 case kind::IMPLIES
: return "impl";
45 case kind::NOT
: return "not";
48 case kind::BITVECTOR_AND
:
50 case kind::BITVECTOR_OR
:
52 case kind::BITVECTOR_XOR
:
54 case kind::BITVECTOR_NAND
:
56 case kind::BITVECTOR_NOR
:
58 case kind::BITVECTOR_XNOR
:
60 case kind::BITVECTOR_COMP
:
62 case kind::BITVECTOR_MULT
:
64 case kind::BITVECTOR_PLUS
:
66 case kind::BITVECTOR_SUB
:
68 case kind::BITVECTOR_UDIV
:
69 case kind::BITVECTOR_UDIV_TOTAL
:
71 case kind::BITVECTOR_UREM
:
72 case kind::BITVECTOR_UREM_TOTAL
:
74 case kind::BITVECTOR_SDIV
:
76 case kind::BITVECTOR_SREM
:
78 case kind::BITVECTOR_SMOD
:
80 case kind::BITVECTOR_SHL
:
82 case kind::BITVECTOR_LSHR
:
84 case kind::BITVECTOR_ASHR
:
86 case kind::BITVECTOR_CONCAT
:
88 case kind::BITVECTOR_NEG
:
90 case kind::BITVECTOR_NOT
:
92 case kind::BITVECTOR_ROTATE_LEFT
:
94 case kind::BITVECTOR_ROTATE_RIGHT
:
95 return "rotate_right";
96 case kind::BITVECTOR_ULT
:
98 case kind::BITVECTOR_ULE
:
100 case kind::BITVECTOR_UGT
:
102 case kind::BITVECTOR_UGE
:
104 case kind::BITVECTOR_SLT
:
106 case kind::BITVECTOR_SLE
:
108 case kind::BITVECTOR_SGT
:
110 case kind::BITVECTOR_SGE
:
112 case kind::BITVECTOR_EXTRACT
:
114 case kind::BITVECTOR_REPEAT
:
116 case kind::BITVECTOR_ZERO_EXTEND
:
117 return "zero_extend";
118 case kind::BITVECTOR_SIGN_EXTEND
:
119 return "sign_extend";
125 std::string
toLFSCKindTerm(Expr node
) {
126 Kind k
= node
.getKind();
127 if( k
==kind::EQUAL
){
128 if( node
[0].getType().isBoolean() ){
134 return toLFSCKind( k
);
138 } /* namespace CVC4::utils */
139 } /* namespace CVC4 */