diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/int_to_bv.cpp | 64 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 10 |
2 files changed, 41 insertions, 33 deletions
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) |