diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-03-24 10:53:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-24 12:53:18 -0500 |
commit | d19b800ac00feb44bfc6302f02695c8700e15c12 (patch) | |
tree | 4272602a77c69b5ecc4a82c83561b20e02679e76 /src/preprocessing/passes | |
parent | e648859c74339fb1b5838c6d439e9dfa1f490bcc (diff) |
Int2BV fail on demand (#4079)
This PR delays error on unsupported symbols as much as possible, by only throwing the error when actually constructing the node.
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/int_to_bv.cpp | 64 |
1 files changed, 38 insertions, 26 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( |