diff options
Diffstat (limited to 'src/proof/proof_utils.cpp')
-rw-r--r-- | src/proof/proof_utils.cpp | 126 |
1 files changed, 0 insertions, 126 deletions
diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp deleted file mode 100644 index cad56db6a..000000000 --- a/src/proof/proof_utils.cpp +++ /dev/null @@ -1,126 +0,0 @@ -/********************* */ -/*! \file proof_utils.cpp - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Guy Katz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** [[ Add lengthier description here ]] - - ** \todo document this file - -**/ - -#include "proof/proof_utils.h" -#include "theory/theory.h" - -namespace CVC4 { -namespace utils { - -std::string toLFSCKind(Kind kind) { - switch(kind) { - // core kinds - case kind::OR : return "or"; - case kind::AND: return "and"; - case kind::XOR: return "xor"; - case kind::EQUAL: return "="; - case kind::IMPLIES: return "impl"; - case kind::NOT: return "not"; - - // bit-vector kinds - case kind::BITVECTOR_AND : - return "bvand"; - case kind::BITVECTOR_OR : - return "bvor"; - case kind::BITVECTOR_XOR : - return "bvxor"; - case kind::BITVECTOR_NAND : - return "bvnand"; - case kind::BITVECTOR_NOR : - return "bvnor"; - case kind::BITVECTOR_XNOR : - return "bvxnor"; - case kind::BITVECTOR_COMP : - return "bvcomp"; - case kind::BITVECTOR_MULT : - return "bvmul"; - case kind::BITVECTOR_PLUS : - return "bvadd"; - case kind::BITVECTOR_SUB : - return "bvsub"; - case kind::BITVECTOR_UDIV : - case kind::BITVECTOR_UDIV_TOTAL : - return "bvudiv"; - case kind::BITVECTOR_UREM : - case kind::BITVECTOR_UREM_TOTAL : - return "bvurem"; - case kind::BITVECTOR_SDIV : - return "bvsdiv"; - case kind::BITVECTOR_SREM : - return "bvsrem"; - case kind::BITVECTOR_SMOD : - return "bvsmod"; - case kind::BITVECTOR_SHL : - return "bvshl"; - case kind::BITVECTOR_LSHR : - return "bvlshr"; - case kind::BITVECTOR_ASHR : - return "bvashr"; - case kind::BITVECTOR_CONCAT : - return "concat"; - case kind::BITVECTOR_NEG : - return "bvneg"; - case kind::BITVECTOR_NOT : - return "bvnot"; - case kind::BITVECTOR_ROTATE_LEFT : - return "rotate_left"; - case kind::BITVECTOR_ROTATE_RIGHT : - return "rotate_right"; - case kind::BITVECTOR_ULT : - return "bvult"; - case kind::BITVECTOR_ULE : - return "bvule"; - case kind::BITVECTOR_UGT : - return "bvugt"; - case kind::BITVECTOR_UGE : - return "bvuge"; - case kind::BITVECTOR_SLT : - return "bvslt"; - case kind::BITVECTOR_SLE : - return "bvsle"; - case kind::BITVECTOR_SGT : - return "bvsgt"; - case kind::BITVECTOR_SGE : - return "bvsge"; - case kind::BITVECTOR_EXTRACT : - return "extract"; - case kind::BITVECTOR_REPEAT : - return "repeat"; - case kind::BITVECTOR_ZERO_EXTEND : - return "zero_extend"; - case kind::BITVECTOR_SIGN_EXTEND : - return "sign_extend"; - default: - Unreachable(); - } -} - -std::string toLFSCKindTerm(Expr node) { - Kind k = node.getKind(); - if( k==kind::EQUAL ){ - if( node[0].getType().isBoolean() ){ - return "iff"; - }else{ - return "="; - } - }else{ - return toLFSCKind( k ); - } -} - -} /* namespace CVC4::utils */ -} /* namespace CVC4 */ |