From: Morgan Deters Date: Wed, 18 Sep 2013 20:53:18 +0000 (-0400) Subject: Support for bv2nat/int2bv in parser and BV rewriter. X-Git-Tag: cvc5-1.0.0~7287^2~10 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aa16fb32ac7a66e327f32ea4c794a3ccf832c587;p=cvc5.git Support for bv2nat/int2bv in parser and BV rewriter. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5aa1e53e4..638c64a69 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1124,6 +1124,11 @@ indexedFunctionName[CVC4::Expr& op] { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } | DIVISIBLE_TOK n=INTEGER_LITERAL { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); } + | INT2BV_TOK n=INTEGER_LITERAL + { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n))); + if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode"); + } } | badIndexedFunctionName ) RPAREN_TOK @@ -1234,6 +1239,11 @@ builtinOp[CVC4::Kind& kind] | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } + | BV2NAT_TOK { $kind = CVC4::kind::BITVECTOR_TO_NAT; + if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode"); + } } + | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } @@ -1601,6 +1611,8 @@ BVSLT_TOK : 'bvslt'; BVSLE_TOK : 'bvsle'; BVSGT_TOK : 'bvsgt'; BVSGE_TOK : 'bvsge'; +BV2NAT_TOK : 'bv2nat'; +INT2BV_TOK : 'int2bv'; //STRING STRCST_TOK : 'str.const'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index db242d101..884502cf2 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -84,6 +84,9 @@ void Smt2::addBitvectorOperators() { addOperator(kind::BITVECTOR_SIGN_EXTEND); addOperator(kind::BITVECTOR_ROTATE_LEFT); addOperator(kind::BITVECTOR_ROTATE_RIGHT); + + addOperator(kind::INT_TO_BITVECTOR); + addOperator(kind::BITVECTOR_TO_NAT); } void Smt2::addStringOperators() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 7b25c6fd9..756e521a6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -304,6 +304,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_SLE: out << "bvsle "; break; case kind::BITVECTOR_SGT: out << "bvsgt "; break; case kind::BITVECTOR_SGE: out << "bvsge "; break; + case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break; case kind::BITVECTOR_EXTRACT: case kind::BITVECTOR_REPEAT: @@ -311,6 +312,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_SIGN_EXTEND: case kind::BITVECTOR_ROTATE_LEFT: case kind::BITVECTOR_ROTATE_RIGHT: + case kind::INT_TO_BITVECTOR: printBvParameterizedOp(out, n); out << ' '; stillNeedToPrintParams = false; @@ -535,6 +537,10 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw() { out << "rotate_right " << n.getOperator().getConst().rotateRightAmount; break; + case kind::INT_TO_BITVECTOR: + out << "int2bv " + << n.getOperator().getConst().size; + break; default: out << n.getKind(); } diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 052e477ea..aeae1073e 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -120,6 +120,14 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign- parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" +constant INT_TO_BITVECTOR_OP \ + ::CVC4::IntToBitVector \ + "::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \ + "util/bitvector.h" \ + "operator for the integer conversion to bit-vector" +parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector" +operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer" + typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule @@ -166,4 +174,7 @@ typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule +typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule +typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule + endtheory diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index baaf7e133..8426afb59 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -66,6 +66,9 @@ enum RewriteRuleId { SremEliminate, ZeroExtendEliminate, SignExtendEliminate, + BVToNatEliminate, + IntToBVEliminate, + /// ground term evaluation EvalEquals, EvalConcat, @@ -173,13 +176,15 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case FailEq: out << "FailEq"; return out; case SimplifyEq: out << "SimplifyEq"; return out; case ReflexivityEq: out << "ReflexivityEq"; return out; - case UgtEliminate: out << "UgtEliminate"; return out; - case SgtEliminate: out << "SgtEliminate"; return out; - case UgeEliminate: out << "UgeEliminate"; return out; - case SgeEliminate: out << "SgeEliminate"; return out; + case UgtEliminate: out << "UgtEliminate"; return out; + case SgtEliminate: out << "SgtEliminate"; return out; + case UgeEliminate: out << "UgeEliminate"; return out; + case SgeEliminate: out << "SgeEliminate"; return out; case RepeatEliminate: out << "RepeatEliminate"; return out; case RotateLeftEliminate: out << "RotateLeftEliminate"; return out; case RotateRightEliminate:out << "RotateRightEliminate";return out; + case BVToNatEliminate: out << "BVToNatEliminate"; return out; + case IntToBVEliminate: out << "IntToBVEliminate"; return out; case NandEliminate: out << "NandEliminate"; return out; case NorEliminate : out << "NorEliminate"; return out; case SdivEliminate : out << "SdivEliminate"; return out; @@ -214,7 +219,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case ExtractBitwise : out << "ExtractBitwise"; return out; case ExtractNot : out << "ExtractNot"; return out; case ExtractArith : out << "ExtractArith"; return out; - case ExtractArith2 : out << "ExtractArith2"; return out; + case ExtractArith2 : out << "ExtractArith2"; return out; case DoubleNeg : out << "DoubleNeg"; return out; case NotConcat : out << "NotConcat"; return out; case NotAnd : out << "NotAnd"; return out; @@ -226,7 +231,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case BitwiseNotOr : out << "BitwiseNotOr"; return out; case XorNot : out << "XorNot"; return out; case LtSelf : out << "LtSelf"; return out; - case LteSelf : out << "LteSelf"; return out; + case LteSelf : out << "LteSelf"; return out; case UltZero : out << "UltZero"; return out; case UleZero : out << "UleZero"; return out; case ZeroUle : out << "ZeroUle"; return out; @@ -491,7 +496,8 @@ struct AllRewriteRules { RewriteRule rule113; RewriteRule rule114; RewriteRule rule115; - + RewriteRule rule116; + RewriteRule rule117; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index cf36633fa..b513dbf90 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -230,6 +230,57 @@ Node RewriteRule::apply(TNode node) { return result; } +template<> +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_TO_NAT); +} + +template<> +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + + const unsigned size = utils::getSize(node[0]); + NodeManager* const nm = NodeManager::currentNM(); + const Node z = nm->mkConst(Rational(0)); + const Node bvone = nm->mkConst(BitVector(1u, 1u)); + + NodeBuilder<> result(kind::PLUS); + Integer i = 1; + for(unsigned bit = 0; bit < size; ++bit, i *= 2) { + Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]), bvone); + result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z); + } + + return Node(result); +} + +template<> +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::INT_TO_BITVECTOR); +} + +template<> +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + + const unsigned size = node.getOperator().getConst().size; + NodeManager* const nm = NodeManager::currentNM(); + const Node bvzero = nm->mkConst(BitVector(1u, 0u)); + const Node bvone = nm->mkConst(BitVector(1u, 1u)); + + std::vector v; + Integer i = 2; + while(v.size() < size) { + Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2))); + v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero)); + i *= 2; + } + + NodeBuilder<> result(kind::BITVECTOR_CONCAT); + result.append(v.rbegin(), v.rend()); + return Node(result); +} + template<> bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_NAND && diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index f698ec83d..2467ae3f1 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -553,11 +553,27 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool prerewrite RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule - >::apply(node); + >::apply(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { + Node resultNode = LinearRewriteStrategy + < RewriteRule + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) { + Node resultNode = LinearRewriteStrategy + < RewriteRule + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) { if (prerewrite) { Node resultNode = LinearRewriteStrategy @@ -640,6 +656,9 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend; d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight; d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft; + + d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat; + d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV; } Node TheoryBVRewriter::eliminateBVSDiv(TNode node) { diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 183b5e8d5..def8e24fe 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -78,6 +78,9 @@ class TheoryBVRewriter { static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false); + static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false); + static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false); + public: static RewriteResponse postRewrite(TNode node); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index effef49e8..67dae0cfa 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -195,6 +195,29 @@ public: } }; +class BitVectorConversionTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if(n.getKind() == kind::BITVECTOR_TO_NAT) { + if(check && !n[0].getType(check).isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + return nodeManager->integerType(); + } + + if(n.getKind() == kind::INT_TO_BITVECTOR) { + size_t bvSize = n.getOperator().getConst(); + if(check && !n[0].getType(check).isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting integer term"); + } + return nodeManager->mkBitVectorType(bvSize); + } + + InternalError("bv-conversion typerule invoked for non-bv-conversion kind"); + } +}; + class CardinalityComputer { public: inline static Cardinality computeCardinality(TypeNode type) { diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 2d5d29339..04e23217b 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -396,7 +396,7 @@ struct CVC4_PUBLIC BitVectorHashFunction { /** * The structure representing the extraction operation for bit-vectors. The - * operation map bit-vectors to bit-vector of size high - low + 1 + * operation maps bit-vectors to bit-vector of size high - low + 1 * by taking the bits at indices high ... low */ struct CVC4_PUBLIC BitVectorExtract { @@ -492,6 +492,13 @@ struct CVC4_PUBLIC BitVectorRotateRight { operator unsigned () const { return rotateRightAmount; } };/* struct BitVectorRotateRight */ +struct CVC4_PUBLIC IntToBitVector { + unsigned size; + IntToBitVector(unsigned size) + : size(size) {} + operator unsigned () const { return size; } +};/* struct IntToBitVector */ + template struct CVC4_PUBLIC UnsignedHashFunction { inline size_t operator()(const T& x) const { @@ -514,6 +521,11 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) { return os << "[" << bv.bitIndex << "]"; } +inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const IntToBitVector& bv) { + return os << "[" << bv.size << "]"; +} + }/* CVC4 namespace */ #endif /* __CVC4__BITVECTOR_H */