From d1ba1ccd5a3c55ba7a0e63b33fd921642e44752d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 18 Apr 2011 19:08:11 +0000 Subject: [PATCH] more work on CVC language --- src/expr/command.cpp | 4 +-- src/parser/cvc/Cvc.g | 25 +++++++++++------ src/printer/cvc/cvc_printer.cpp | 39 ++++++++++++++++++++------- test/regress/regress0/bv/Makefile.am | 5 ++-- test/regress/regress0/bv/bvsimple.cvc | 21 +++++++++++++++ 5 files changed, 71 insertions(+), 23 deletions(-) create mode 100644 test/regress/regress0/bv/bvsimple.cvc diff --git a/src/expr/command.cpp b/src/expr/command.cpp index bcc96637f..48cf4ea93 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -155,9 +155,7 @@ void QueryCommand::printResult(std::ostream& out) const { } void QueryCommand::toStream(std::ostream& out) const { - out << "Query("; - d_expr.printAst(out, 0); - out << ")"; + out << "Query(" << d_expr << ')'; } /* class CommandSequence */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 96a8346b0..30866eddb 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -597,7 +597,7 @@ arrayType[CVC4::Type& t] Type t2; } : baseType[t] - | ARRAY_TOK baseType[t] OF_TOK baseType[t2] + | ARRAY_TOK bitvectorType[t] OF_TOK bitvectorType[t2] { t = EXPR_MANAGER->mkArrayType(t, t2); } ; @@ -927,10 +927,14 @@ bvUminusTerm[CVC4::Expr& f] { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); } | SX_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + unsigned n = BitVectorType(f.getType()).getSize(); + // sign extension in TheoryBitVector is defined as in SMT-LIBv2 + f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); } | BVZEROEXTEND_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + unsigned n = BitVectorType(f.getType()).getSize(); + // also zero extension + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k - n)), f); } | BVREPEAT_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); } @@ -945,14 +949,19 @@ bvUminusTerm[CVC4::Expr& f] bvShiftTerm[CVC4::Expr& f] @init { - std::vector expressions; - std::vector operators; - unsigned op; + bool left = false; } : bvComparison[f] - ( ( LEFTSHIFT_TOK | RIGHTSHIFT_TOK) INTEGER_LITERAL + ( (LEFTSHIFT_TOK { left = true; } | RIGHTSHIFT_TOK) INTEGER_LITERAL { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); } + if(left) { + f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k))); + } else { + unsigned n = BitVectorType(f.getType()).getSize(); + f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)), + MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f)); + } + } )? ; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index c3253d05a..97f434e9b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -144,13 +144,36 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, return; } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { - out << n.getOperator(); - if(n.getNumChildren() > 0) { - out << '('; - if(n.getNumChildren() > 1) { - copy(n.begin(), n.end() - 1, ostream_iterator(out, ", ")); + switch(n.getKind()) { + case kind::BITVECTOR_EXTRACT: + out << n[0] << n.getOperator().getConst(); + break; + case kind::BITVECTOR_REPEAT: + out << "BVREPEAT(" << n[0] << "," << n.getOperator() << ')'; + break; + case kind::BITVECTOR_ZERO_EXTEND: + out << "BVZEROEXTEND(" << n[0] << "," << n.getOperator() << ')'; + break; + case kind::BITVECTOR_SIGN_EXTEND: + out << "SX(" << n[0] << "," << n.getOperator() << ')'; + break; + case kind::BITVECTOR_ROTATE_LEFT: + out << "BVROTL(" << n[0] << "," << n.getOperator() << ')'; + break; + case kind::BITVECTOR_ROTATE_RIGHT: + out << "BVROTR(" << n[0] << "," << n.getOperator() << ')'; + break; + + + default: + out << n.getOperator(); + if(n.getNumChildren() > 0) { + out << '('; + if(n.getNumChildren() > 1) { + copy(n.begin(), n.end() - 1, ostream_iterator(out, ", ")); + } + out << n[n.getNumChildren() - 1] << ')'; } - out << n[n.getNumChildren() - 1] << ')'; } return; } else if(n.getMetaKind() == kind::metakind::OPERATOR) { @@ -220,10 +243,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << n.getOperator() << '(' << n[0] << ',' << n[1] << ')'; break; - case kind::BITVECTOR_EXTRACT: - out << n[0] << '[' << n.getOperator().getConst() << ']'; - break; - default: if(k == kind::NOT && n[0].getKind() == kind::EQUAL) { // collapse NOT-over-EQUAL diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index dd4246e16..92db8d453 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -14,12 +14,13 @@ SMT_TESTS = SMT2_TESTS = # Regression tests for PL inputs -CVC_TESTS = +CVC_TESTS = bvsimple.cvc # Regression tests derived from bug reports BUG_TESTS = TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + test00.smt diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc new file mode 100644 index 000000000..f1cb8ff01 --- /dev/null +++ b/test/regress/regress0/bv/bvsimple.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 + +% Some tests from the CVC3 user manual. +% http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html + +QUERY +( 0bin01@0bin0 = 0bin010 ) AND +( 0bin1000 >> 3 = 0bin0001 ) AND +( 0bin0011 << 3 = 0bin0011000 ) AND +( 0bin1000 >> 3 = 0bin0001 ) AND + +TRUE + +% these not working yet.. +%( BVZEROEXTEND(0bin100, 5) = 0bin00100 ) AND +%( SX(0bin100, 5) = 0bin11100 ) AND +% +%( BVZEROEXTEND(0bin100, 3) = 0bin100 ) AND +%( SX(0bin100, 3) = 0bin100 ) +; -- 2.30.2