diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
commit | 89ba584531115b7f6d47088d7614368ea05ab9d8 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/proof/proof_utils.cpp | |
parent | 324ca0376c960c75f621f0102eeaa1186589dda7 (diff) |
Merging proof branch
Diffstat (limited to 'src/proof/proof_utils.cpp')
-rw-r--r-- | src/proof/proof_utils.cpp | 52 |
1 files changed, 26 insertions, 26 deletions
diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp index 5b04c281d..fe0d42242 100644 --- a/src/proof/proof_utils.cpp +++ b/src/proof/proof_utils.cpp @@ -21,14 +21,14 @@ namespace CVC4 { namespace utils { -void collectAtoms(TNode node, CVC4::NodeSet& seen) { +void collectAtoms(TNode node, std::set<Node>& seen) { if (seen.find(node) != seen.end()) return; if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) { seen.insert(node); return; } - + for (unsigned i = 0; i < node.getNumChildren(); ++i) { collectAtoms(node[i], seen); } @@ -47,23 +47,23 @@ std::string toLFSCKind(Kind kind) { // bit-vector kinds case kind::BITVECTOR_AND : - return "bvand"; + return "bvand"; case kind::BITVECTOR_OR : - return "bvor"; + return "bvor"; case kind::BITVECTOR_XOR : - return "bvxor"; + return "bvxor"; case kind::BITVECTOR_NAND : - return "bvnand"; + return "bvnand"; case kind::BITVECTOR_NOR : - return "bvnor"; + return "bvnor"; case kind::BITVECTOR_XNOR : - return "bvxnor"; + return "bvxnor"; case kind::BITVECTOR_COMP : - return "bvcomp"; + return "bvcomp"; case kind::BITVECTOR_MULT : return "bvmul"; case kind::BITVECTOR_PLUS : - return "bvadd"; + return "bvadd"; case kind::BITVECTOR_SUB : return "bvsub"; case kind::BITVECTOR_UDIV : @@ -71,49 +71,49 @@ std::string toLFSCKind(Kind kind) { return "bvudiv"; case kind::BITVECTOR_UREM : case kind::BITVECTOR_UREM_TOTAL : - return "bvurem"; + return "bvurem"; case kind::BITVECTOR_SDIV : - return "bvsdiv"; + return "bvsdiv"; case kind::BITVECTOR_SREM : return "bvsrem"; case kind::BITVECTOR_SMOD : - return "bvsmod"; + return "bvsmod"; case kind::BITVECTOR_SHL : - return "bvshl"; + return "bvshl"; case kind::BITVECTOR_LSHR : return "bvlshr"; case kind::BITVECTOR_ASHR : return "bvashr"; case kind::BITVECTOR_CONCAT : - return "concat"; + return "concat"; case kind::BITVECTOR_NEG : - return "bvneg"; + return "bvneg"; case kind::BITVECTOR_NOT : - return "bvnot"; + return "bvnot"; case kind::BITVECTOR_ROTATE_LEFT : - return "rotate_left"; + return "rotate_left"; case kind::BITVECTOR_ROTATE_RIGHT : return "rotate_right"; case kind::BITVECTOR_ULT : - return "bvult"; + return "bvult"; case kind::BITVECTOR_ULE : - return "bvule"; + return "bvule"; case kind::BITVECTOR_UGT : return "bvugt"; case kind::BITVECTOR_UGE : return "bvuge"; case kind::BITVECTOR_SLT : - return "bvslt"; + return "bvslt"; case kind::BITVECTOR_SLE : - return "bvsle"; + return "bvsle"; case kind::BITVECTOR_SGT : - return "bvsgt"; + return "bvsgt"; case kind::BITVECTOR_SGE : - return "bvsge"; + return "bvsge"; case kind::BITVECTOR_EXTRACT : - return "extract"; + return "extract"; case kind::BITVECTOR_REPEAT : - return "repeat"; + return "repeat"; case kind::BITVECTOR_ZERO_EXTEND : return "zero_extend"; case kind::BITVECTOR_SIGN_EXTEND : |