summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/passes/bv_to_int.cpp42
-rw-r--r--src/preprocessing/passes/bv_to_int.h15
-rw-r--r--src/smt/set_defaults.cpp9
-rw-r--r--test/regress/CMakeLists.txt7
-rw-r--r--test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 (renamed from test/regress/regress0/bv/bvuf_to_intuf.smt2)0
-rw-r--r--test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 (renamed from test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2)0
-rw-r--r--test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 (renamed from test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2)0
-rw-r--r--test/regress/regress2/bv_to_int_inc1.smt230
8 files changed, 67 insertions, 36 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index bb0bde2f9..041312113 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -108,7 +108,7 @@ Node BVToInt::makeBinary(Node n)
d_binarizeCache[current] = Node();
toVisit.insert(toVisit.end(), current.begin(), current.end());
}
- else if (d_binarizeCache[current].isNull())
+ else if (d_binarizeCache[current].get().isNull())
{
/*
* We already visited the sub-dag rooted at the current node,
@@ -137,14 +137,13 @@ Node BVToInt::makeBinary(Node n)
{
// current has children, but we do not binarize it
NodeBuilder<> builder(k);
- if (current.getKind() == kind::BITVECTOR_EXTRACT
- || current.getKind() == kind::APPLY_UF)
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
{
builder << current.getOperator();
}
for (Node child : current)
{
- builder << d_binarizeCache[child];
+ builder << d_binarizeCache[child].get();
}
d_binarizeCache[current] = builder.constructNode();
}
@@ -186,6 +185,7 @@ Node BVToInt::eliminationPass(Node n)
(d_rebuildCache.find(current) != d_rebuildCache.end());
if (!inEliminationCache)
{
+ // current is not the elimination of any previously-visited node
// current hasn't been eliminated yet.
// eliminate operators from it
Node currentEliminated =
@@ -221,7 +221,7 @@ Node BVToInt::eliminationPass(Node n)
if (inRebuildCache)
{
// current was already added to the rebuild cache.
- if (d_rebuildCache[current].isNull())
+ if (d_rebuildCache[current].get().isNull())
{
// current wasn't rebuilt yet.
uint64_t numChildren = current.getNumChildren();
@@ -235,8 +235,7 @@ Node BVToInt::eliminationPass(Node n)
// The main operator is replaced, and the children
// are replaced with their eliminated counterparts.
NodeBuilder<> builder(current.getKind());
- if (current.getKind() == kind::BITVECTOR_EXTRACT
- || current.getKind() == kind::APPLY_UF)
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
{
builder << current.getOperator();
}
@@ -245,8 +244,8 @@ Node BVToInt::eliminationPass(Node n)
Assert(d_eliminationCache.find(child) != d_eliminationCache.end());
Node eliminatedChild = d_eliminationCache[child];
Assert(d_rebuildCache.find(eliminatedChild) != d_eliminationCache.end());
- Assert(!d_rebuildCache[eliminatedChild].isNull());
- builder << d_rebuildCache[eliminatedChild];
+ Assert(!d_rebuildCache[eliminatedChild].get().isNull());
+ builder << d_rebuildCache[eliminatedChild].get();
}
d_rebuildCache[current] = builder.constructNode();
}
@@ -256,7 +255,7 @@ Node BVToInt::eliminationPass(Node n)
Assert(d_eliminationCache.find(n) != d_eliminationCache.end());
Node eliminated = d_eliminationCache[n];
Assert(d_rebuildCache.find(eliminated) != d_rebuildCache.end());
- Assert(!d_rebuildCache[eliminated].isNull());
+ Assert(!d_rebuildCache[eliminated].get().isNull());
return d_rebuildCache[eliminated];
}
@@ -270,6 +269,7 @@ Node BVToInt::bvToInt(Node n)
vector<Node> toVisit;
toVisit.push_back(n);
uint64_t granularity = options::BVAndIntegerGranularity();
+ Assert(0 <= granularity && granularity <= 8);
while (!toVisit.empty())
{
@@ -284,7 +284,7 @@ Node BVToInt::bvToInt(Node n)
else
{
// We already visited this node
- if (!d_bvToIntCache[current].isNull())
+ if (!d_bvToIntCache[current].get().isNull())
{
// We are done computing the translation for current
toVisit.pop_back();
@@ -643,7 +643,7 @@ Node BVToInt::bvToInt(Node n)
Assert(d_bvToIntCache.find(a) != d_bvToIntCache.end());
Assert(i >= j);
Node div = d_nm->mkNode(
- kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a], pow2(j));
+ kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a].get(), pow2(j));
d_bvToIntCache[current] = modpow2(div, i - j + 1);
break;
}
@@ -814,7 +814,7 @@ bool BVToInt::childrenTypesChanged(Node n) {
bool result = false;
for (Node child : n) {
TypeNode originalType = child.getType();
- TypeNode newType = d_bvToIntCache[child].getType();
+ TypeNode newType = d_bvToIntCache[child].get().getType();
if (! newType.isSubtypeOf(originalType)) {
result = true;
break;
@@ -825,10 +825,11 @@ bool BVToInt::childrenTypesChanged(Node n) {
BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "bv-to-int"),
- d_binarizeCache(),
- d_eliminationCache(),
- d_bvToIntCache(),
- d_rangeAssertions()
+ d_binarizeCache(preprocContext->getUserContext()),
+ d_eliminationCache(preprocContext->getUserContext()),
+ d_rebuildCache(preprocContext->getUserContext()),
+ d_bvToIntCache(preprocContext->getUserContext()),
+ d_rangeAssertions(preprocContext->getUserContext())
{
d_nm = NodeManager::currentNM();
d_zero = d_nm->mkConst<Rational>(0);
@@ -838,7 +839,6 @@ BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
PreprocessingPassResult BVToInt::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- AlwaysAssert(!options::incrementalSolving());
for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i)
{
Node bvNode = (*assertionsToPreprocess)[i];
@@ -857,7 +857,11 @@ void BVToInt::addFinalizeRangeAssertions(
AssertionPipeline* assertionsToPreprocess)
{
vector<Node> vec_range;
- vec_range.assign(d_rangeAssertions.begin(), d_rangeAssertions.end());
+ vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end());
+ if (vec_range.size() == 0)
+ {
+ return;
+ }
if (vec_range.size() == 1)
{
assertionsToPreprocess->push_back(vec_range[0]);
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index 5015d1e8e..d8ee69879 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -62,6 +62,9 @@
#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
#define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
+#include "context/cdhashmap.h"
+#include "context/cdo.h"
+#include "context/context.h"
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_context.h"
@@ -69,7 +72,7 @@ namespace CVC4 {
namespace preprocessing {
namespace passes {
-using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
class BVToInt : public PreprocessingPass
{
@@ -245,10 +248,10 @@ class BVToInt : public PreprocessingPass
/**
* Caches for the different functions
*/
- NodeMap d_binarizeCache;
- NodeMap d_eliminationCache;
- NodeMap d_rebuildCache;
- NodeMap d_bvToIntCache;
+ CDNodeMap d_binarizeCache;
+ CDNodeMap d_eliminationCache;
+ CDNodeMap d_rebuildCache;
+ CDNodeMap d_bvToIntCache;
/**
* Node manager that is used throughout the pass
@@ -259,7 +262,7 @@ class BVToInt : public PreprocessingPass
* A set of constraints of the form 0 <= x < 2^k
* These are added for every new integer variable that we introduce.
*/
- unordered_set<Node, NodeHashFunction> d_rangeAssertions;
+ context::CDHashSet<Node, NodeHashFunction> d_rangeAssertions;
/**
* Useful constants
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7d2427015..130f75894 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -151,14 +151,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
{
- // not compatible with incremental
- if (options::incrementalSolving())
- {
- throw OptionException(
- "solving bitvectors as integers is currently not supported "
- "when solving incrementally.");
- }
- else if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+ if (options::boolToBitvector() != options::BoolToBVMode::OFF)
{
throw OptionException(
"solving bitvectors as integers is incompatible with --bool-to-bv.");
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7a1366b3a..0caeafb36 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -213,11 +213,11 @@ set(regress_0_tests
regress0/bv/bv_to_int_bvmul1.smt2
regress0/bv/bv_to_int_bvmul2.smt2
regress0/bv/bv_to_int_bitwise.smt2
+ regress0/bv/bv_to_int_bvuf_to_intuf.smt2
+ regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
+ regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
regress0/bv/bv_to_int_elim_err.smt2
regress0/bv/bv_to_int_zext.smt2
- regress0/bv/bvuf_to_intuf.smt2
- regress0/bv/bvuf_to_intuf_smtlib.smt2
- regress0/bv/bvuf_to_intuf_sorts.smt2
regress0/bv/bv2nat-ground-c.smt2
regress0/bv/bv2nat-simp-range.smt2
regress0/bv/bvmul-pow2-only.smt2
@@ -2075,6 +2075,7 @@ set(regress_2_tests
regress2/bug812.smt2
regress2/bv/opStructure_MBA_6.scrambled.min.smt2
regress2/bv_to_int_ashr.smt2
+ regress2/bv_to_int_inc1.smt2
regress2/bv_to_int_mask_array_1.smt2
regress2/bv_to_int_mask_array_2.smt2
regress2/bv_to_int_shifts.smt2
diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
index c621aa112..c621aa112 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
index 6196b2bb9..6196b2bb9 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
index 8fbe96eab..8fbe96eab 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2
new file mode 100644
index 000000000..0d09a7252
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_inc1.smt2
@@ -0,0 +1,30 @@
+; COMMAND-LINE: --incremental --solve-bv-as-int=sum
+; EXPECT sat
+; EXPECT sat
+; EXPECT unsat
+; EXPECT sat
+(set-logic QF_BV)
+(set-option :incremental true)
+(declare-fun a () (_ BitVec 3))
+(declare-fun b () (_ BitVec 3))
+(declare-fun c () (_ BitVec 3))
+
+(assert (bvult a (bvand b c)))
+(check-sat)
+; EXPECT: sat
+
+(push 1)
+(assert (bvult c b))
+(check-sat)
+; EXPECT: sat
+
+
+(push 1)
+(assert (bvugt c b))
+(check-sat)
+; EXPECT: unsat
+(pop 2)
+
+(check-sat)
+; EXPECT: sat
+(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback