src/proof/proof_utils.cpp

   1 /*********************                                                        */
   2 /*! \file proof_utils.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Andrew Reynolds, Guy Katz
   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
  11  **
  12  ** [[ Add lengthier description here ]]
  13
  14  ** \todo document this file
  15
  16 **/
  17
  18 #include "proof/proof_utils.h"
  19 #include "theory/theory.h"
  20
  21 namespace CVC4 {
  22 namespace utils {
  23
  24 void collectAtoms(TNode node, std::set<Node>& seen) {
  25   if (seen.find(node) != seen.end())
  26     return;
  27   if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) {
  28       seen.insert(node);
  29       return;
  30   }
  31
  32   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
  33     collectAtoms(node[i], seen);
  34   }
  35 }
  36
  37 std::string toLFSCKind(Kind kind) {
  38   switch(kind) {
  39     // core kinds
  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";
  46
  47     // bit-vector kinds
  48   case kind::BITVECTOR_AND :
  49     return "bvand";
  50   case kind::BITVECTOR_OR :
  51     return "bvor";
  52   case kind::BITVECTOR_XOR :
  53     return "bvxor";
  54   case kind::BITVECTOR_NAND :
  55     return "bvnand";
  56   case kind::BITVECTOR_NOR :
  57     return "bvnor";
  58   case kind::BITVECTOR_XNOR :
  59     return "bvxnor";
  60   case kind::BITVECTOR_COMP :
  61     return "bvcomp";
  62   case kind::BITVECTOR_MULT :
  63     return "bvmul";
  64   case kind::BITVECTOR_PLUS :
  65     return "bvadd";
  66   case kind::BITVECTOR_SUB :
  67     return "bvsub";
  68   case kind::BITVECTOR_UDIV :
  69   case kind::BITVECTOR_UDIV_TOTAL :
  70     return "bvudiv";
  71   case kind::BITVECTOR_UREM :
  72   case kind::BITVECTOR_UREM_TOTAL :
  73     return "bvurem";
  74   case kind::BITVECTOR_SDIV :
  75     return "bvsdiv";
  76   case kind::BITVECTOR_SREM :
  77     return "bvsrem";
  78   case kind::BITVECTOR_SMOD :
  79     return "bvsmod";
  80   case kind::BITVECTOR_SHL :
  81     return "bvshl";
  82   case kind::BITVECTOR_LSHR :
  83     return "bvlshr";
  84   case kind::BITVECTOR_ASHR :
  85     return "bvashr";
  86   case kind::BITVECTOR_CONCAT :
  87     return "concat";
  88   case kind::BITVECTOR_NEG :
  89     return "bvneg";
  90   case kind::BITVECTOR_NOT :
  91     return "bvnot";
  92   case kind::BITVECTOR_ROTATE_LEFT :
  93     return "rotate_left";
  94   case kind::BITVECTOR_ROTATE_RIGHT :
  95     return "rotate_right";
  96   case kind::BITVECTOR_ULT :
  97     return "bvult";
  98   case kind::BITVECTOR_ULE :
  99     return "bvule";
 100   case kind::BITVECTOR_UGT :
 101     return "bvugt";
 102   case kind::BITVECTOR_UGE :
 103     return "bvuge";
 104   case kind::BITVECTOR_SLT :
 105     return "bvslt";
 106   case kind::BITVECTOR_SLE :
 107     return "bvsle";
 108   case kind::BITVECTOR_SGT :
 109     return "bvsgt";
 110   case kind::BITVECTOR_SGE :
 111     return "bvsge";
 112   case kind::BITVECTOR_EXTRACT :
 113     return "extract";
 114   case kind::BITVECTOR_REPEAT :
 115     return "repeat";
 116   case kind::BITVECTOR_ZERO_EXTEND :
 117     return "zero_extend";
 118   case kind::BITVECTOR_SIGN_EXTEND :
 119     return "sign_extend";
 120   default:
 121     Unreachable();
 122   }
 123 }
 124
 125 std::string toLFSCKindTerm(Expr node) {
 126   Kind k = node.getKind();
 127   if( k==kind::EQUAL ){
 128     if( node[0].getType().isBoolean() ){
 129       return "iff";
 130     }else{
 131       return "=";
 132     }
 133   }else{
 134     return toLFSCKind( k );
 135   }
 136 }
 137
 138 } /* namespace CVC4::utils */
 139 } /* namespace CVC4 */