summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xcontrib/competitions/smt-comp/run-script-smtcomp-current10
-rw-r--r--src/preprocessing/passes/int_to_bv.cpp64
-rw-r--r--src/smt/smt_engine.cpp10
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/bv/bv-abstr-bug2.smt22
-rw-r--r--test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt211
6 files changed, 59 insertions, 39 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 4c781d47c..b46253851 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -39,11 +39,11 @@ QF_NIA)
trywith 60 --nl-ext-tplanes --decision=justification
trywith 60 --no-nl-ext-tplanes --decision=internal
# this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail
- trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
- trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
- trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
- trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
- trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+ trywith 600 --solve-int-as-bv=2 --bv-sat-solver=cadical --no-bv-abstraction
+ trywith 600 --solve-int-as-bv=4 --bv-sat-solver=cadical --no-bv-abstraction
+ trywith 600 --solve-int-as-bv=8 --bv-sat-solver=cadical --no-bv-abstraction
+ trywith 600 --solve-int-as-bv=16 --bv-sat-solver=cadical --no-bv-abstraction
+ trywith 1200 --solve-int-as-bv=32 --bv-sat-solver=cadical --no-bv-abstraction
finishwith --nl-ext-tplanes --decision=internal
;;
QF_NRA)
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 372df90ce..9fa9a0c05 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -44,6 +44,20 @@ struct intToBV_stack_element
intToBV_stack_element(TNode node) : d_node(node), d_children_added(false) {}
}; /* struct intToBV_stack_element */
+bool childrenTypesChanged(Node n, NodeMap& cache) {
+ bool result = false;
+ for (Node child : n) {
+ TypeNode originalType = child.getType();
+ TypeNode newType = cache[child].getType();
+ if (! newType.isSubtypeOf(originalType)) {
+ result = true;
+ break;
+ }
+ }
+ return result;
+}
+
+
Node intToBVMakeBinary(TNode n, NodeMap& cache)
{
// Do a topological sort of the subexpressions and substitute them
@@ -84,6 +98,10 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache)
else
{
NodeBuilder<> builder(current.getKind());
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << current.getOperator();
+ }
+
for (unsigned i = 0; i < current.getNumChildren(); ++i)
{
Assert(cache.find(current[i]) != cache.end());
@@ -203,13 +221,12 @@ Node intToBV(TNode n, NodeMap& cache)
case kind::EQUAL:
case kind::ITE: break;
default:
- if (Theory::theoryOf(current) == THEORY_BOOL)
- {
- break;
- }
- throw TypeCheckingException(
+ if (childrenTypesChanged(current, cache)) {
+ throw TypeCheckingException(
current.toExpr(),
string("Cannot translate to BV: ") + current.toString());
+ }
+ break;
}
for (unsigned i = 0; i < children.size(); ++i)
{
@@ -229,6 +246,9 @@ Node intToBV(TNode n, NodeMap& cache)
}
}
NodeBuilder<> builder(newKind);
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << current.getOperator();
+ }
for (unsigned i = 0; i < children.size(); ++i)
{
builder << children[i];
@@ -271,10 +291,6 @@ Node intToBV(TNode n, NodeMap& cache)
nm->mkBitVectorType(size),
"Variable introduced in intToBV pass");
}
- else
- {
- AlwaysAssert(current.getType() == nm->booleanType());
- }
}
else if (current.isConst())
{
@@ -283,25 +299,21 @@ Node intToBV(TNode n, NodeMap& cache)
case kind::CONST_RATIONAL:
{
Rational constant = current.getConst<Rational>();
- AlwaysAssert(constant.isIntegral());
- AlwaysAssert(constant >= 0);
- BitVector bv(size, constant.getNumerator());
- if (bv.toSignedInteger() != constant.getNumerator())
- {
- throw TypeCheckingException(
- current.toExpr(),
- string("Not enough bits for constant in intToBV: ")
- + current.toString());
+ if (constant.isIntegral()) {
+ AlwaysAssert(constant >= 0);
+ BitVector bv(size, constant.getNumerator());
+ if (bv.toSignedInteger() != constant.getNumerator())
+ {
+ throw TypeCheckingException(
+ current.toExpr(),
+ string("Not enough bits for constant in intToBV: ")
+ + current.toString());
+ }
+ result = nm->mkConst(bv);
}
- result = nm->mkConst(bv);
break;
}
- case kind::CONST_BOOLEAN: break;
- default:
- throw TypeCheckingException(
- current.toExpr(),
- string("Cannot translate const to BV: ")
- + current.toString());
+ default: break;
}
}
else
@@ -325,7 +337,7 @@ IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
PreprocessingPassResult IntToBV::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- unordered_map<Node, Node, NodeHashFunction> cache;
+ NodeMap cache;
for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
{
assertionsToPreprocess->replace(
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a367c8469..7d78e93f9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1192,13 +1192,9 @@ void SmtEngine::setDefaults() {
if (options::solveIntAsBV() > 0)
{
- if (!(d_logic <= LogicInfo("QF_NIA")))
- {
- throw OptionException(
- "--solve-int-as-bv=X only supported for pure integer logics (QF_NIA, "
- "QF_LIA, QF_IDL)");
- }
- d_logic = LogicInfo("QF_BV");
+ d_logic = d_logic.getUnlockedCopy();
+ d_logic.enableTheory(THEORY_BV);
+ d_logic.lock();
}
if (options::solveBVAsInt() > 0)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4cd3c70d2..0eb6bc2d2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -358,6 +358,7 @@ set(regress_0_tests
regress0/bv/fuzz40.smtv1.smt2
regress0/bv/fuzz41.smtv1.smt2
regress0/bv/issue3621.smt2
+ regress0/bv/int_to_bv_err_on_demand_1.smt2
regress0/bv/mul-neg-unsat.smt2
regress0/bv/mul-negpow2.smt2
regress0/bv/mult-pow2-negative.smt2
diff --git a/test/regress/regress0/bv/bv-abstr-bug2.smt2 b/test/regress/regress0/bv/bv-abstr-bug2.smt2
index 939439adf..1c8f9b1df 100644
--- a/test/regress/regress0/bv/bv-abstr-bug2.smt2
+++ b/test/regress/regress0/bv/bv-abstr-bug2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-int-as-bv=32 --bitblast=eager
+; COMMAND-LINE: --solve-int-as-bv=32
(set-logic QF_NIA)
(set-info :status sat)
(declare-fun _substvar_7_ () Bool)
diff --git a/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2 b/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2
new file mode 100644
index 000000000..1ef63f365
--- /dev/null
+++ b/test/regress/regress0/bv/int_to_bv_err_on_demand_1.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort S 0)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun A () (Array S S))
+(declare-fun f ((_ BitVec 4)) S)
+
+(assert (distinct (select A (f (_ bv0 4))) (select A (f (_ bv1 4)))))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback