From: Liana Hadarean Date: Thu, 17 May 2012 18:42:13 +0000 (+0000) Subject: Fixed bug 338: X-Git-Tag: cvc5-1.0.0~8158 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1703b160511396cd23be5203d9af86641b45766e;p=cvc5.git Fixed bug 338: - fixed buggy rewrite rules assuming certain nodes only had 2 children - added support for bv-rewrite dump - fixed smt2_printer for bv constants --- diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2b686441a..25d3bf35a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -85,11 +85,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::CONST_BITVECTOR: { const BitVector& bv = n.getConst(); const Integer& x = bv.getValue(); - out << "#b"; unsigned n = bv.getSize(); - while(n-- > 0) { - out << (x.testBit(n) ? '1' : '0'); - } + out << "(_ "; + out << "bv" << x <<" " << n; + out << ")"; + // //out << "#b"; + + // while(n-- > 0) { + // out << (x.testBit(n) ? '1' : '0'); + // } break; } case kind::CONST_BOOLEAN: diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 30437a76e..343d4d1f1 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -24,6 +24,7 @@ #include "context/context.h" #include "util/stats.h" #include "theory/bv/theory_bv_utils.h" +#include "expr/command.h" #include namespace CVC4 { @@ -345,6 +346,23 @@ public: Assert(checkApplies || applies(node)); //++ s_statistics->d_ruleApplications; Node result = apply(node); + if (result != node) { + if(Dump.isOn("bv-rewrites")) { + std::ostringstream os; + os << "RewriteRule <"<; expect unsat"; + + Node condition; + if (result.getType().isBoolean()) { + condition = node.iffNode(result).notNode(); + } else { + condition = node.eqNode(result).notNode(); + } + + Dump("bv-rewrites") + << CommentCommand(os.str()) + << CheckSatCommand(condition.toExpr()); + } + } BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl; return result; } else { diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index da3fb6554..3a5a07f1c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -46,10 +46,12 @@ Node RewriteRule::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; unsigned high = utils::getExtractHigh(node); unsigned low = utils::getExtractLow(node); - Node a = utils::mkExtract(node[0][0], high, low); - Node b = utils::mkExtract(node[0][1], high, low); + std::vector children; + for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { + children.push_back(utils::mkExtract(node[0][i], high, low)); + } Kind kind = node[0].getKind(); - return utils::mkNode(kind, a, b); + return utils::mkSortedNode(kind, children); } /** @@ -92,11 +94,12 @@ Node RewriteRule::apply(Node node) { unsigned low = utils::getExtractLow(node); Assert (low == 0); unsigned high = utils::getExtractHigh(node); - Node a = utils::mkExtract(node[0][0], high, low); - Node b = utils::mkExtract(node[0][1], high, low); - + std::vector children; + for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { + children.push_back(utils::mkExtract(node[0][i], high, low)); + } Kind kind = node[0].getKind(); - return utils::mkNode(kind, a, b); + return utils::mkNode(kind, children); } @@ -119,13 +122,14 @@ Node RewriteRule::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; unsigned low = utils::getExtractLow(node); unsigned high = utils::getExtractHigh(node); - Node a = utils::mkExtract(node[0][0], high, 0); - Node b = utils::mkExtract(node[0][1], high, 0); - + std::vector children; + for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { + children.push_back(utils::mkExtract(node[0][i], high, 0)); + } Kind kind = node[0].getKind(); - Node a_op_b = utils::mkNode(kind, a, b); + Node op_children = utils::mkSortedNode(kind, children); - return utils::mkExtract(a_op_b, high, low); + return utils::mkExtract(op_children, high, low); } template<> inline diff --git a/src/util/options.cpp b/src/util/options.cpp index 36033db0b..e41959da2 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -619,7 +619,8 @@ throw(OptionException) { } else if(!strcmp(optarg, "clauses")) { } else if(!strcmp(optarg, "t-conflicts") || !strcmp(optarg, "t-lemmas") || - !strcmp(optarg, "t-explanations")) { + !strcmp(optarg, "t-explanations") || + !strcmp(optarg, "bv-rewrites")) { // These are "non-state-dumping" modes. If state (SAT decisions, // propagations, etc.) is dumped, it will interfere with the validity // of these generated queries. diff --git a/test/regress/regress0/aufbv/bug338.smt2 b/test/regress/regress0/aufbv/bug338.smt2 new file mode 100644 index 000000000..b245228be --- /dev/null +++ b/test/regress/regress0/aufbv/bug338.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_AUFBV) +(declare-sort U 0) +(declare-sort Index 0) +(declare-sort Element 0) +(declare-fun memory_0 () (Array (_ BitVec 32) (_ BitVec 8))) +(set-info :status sat) + +(set-info :notes "RewriteRule ; expect unsat") + +(assert (not (= ((_ extract 7 0) (bvor (_ bv65536 32) (concat (_ bv0 25) ((_ extract 7 1) (select memory_0 (_ bv1 32)))) (concat (_ bv0 24) (select memory_0 (_ bv1 32))))) (bvor ((_ extract 7 0) (_ bv65536 32)) ((_ extract 7 0) (concat (_ bv0 25) ((_ extract 7 1) (select memory_0 (_ bv1 32))))))))) +(check-sat) + + +(exit)