summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/printer/smt2/smt2_printer.cpp12
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h18
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_normalization.h28
-rw-r--r--src/util/options.cpp3
-rw-r--r--test/regress/regress0/aufbv/bug338.smt214
5 files changed, 58 insertions, 17 deletions
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<BitVector>();
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 <sstream>
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 <"<<rule<<">; 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<ExtractBitwise>::apply(Node node) {
BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << 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<Node> 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<ExtractArith>::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<Node> 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<ExtractArith2>::apply(Node node) {
BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << 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<Node> 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 <ExtractBitwise>; 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback