diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 85 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.h | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 1 |
3 files changed, 61 insertions, 27 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 75136913c..cb78b0897 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -23,6 +23,7 @@ #include <vector> #include "expr/node.h" +#include "options/uf_options.h" #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" @@ -315,9 +316,7 @@ Node BVToInt::bvToInt(Node n) } else { - // Boolean variables are left unchanged. - AlwaysAssert(current.getType() == d_nm->booleanType() - || current.getType().isSort()); + // variables other than bit-vector variables are left intact d_bvToIntCache[current] = current; } } @@ -696,6 +695,8 @@ Node BVToInt::bvToInt(Node n) * We cache both the term itself (e.g., f(a)) and the function * symbol f. */ + + //Construct the function itself Node bvUF = current.getOperator(); Node intUF; TypeNode tn = current.getOperator().getType(); @@ -729,38 +730,57 @@ Node BVToInt::bvToInt(Node n) // Insert the function symbol itself to the cache d_bvToIntCache[bvUF] = intUF; } - translated_children.insert(translated_children.begin(), intUF); - // Insert the term to the cache - d_bvToIntCache[current] = - d_nm->mkNode(kind::APPLY_UF, translated_children); + if (childrenTypesChanged(current) && options::ufHo()) { /** - * Add range constraints if necessary. - * If the original range was a BV sort, the current application of - * the fucntion Must be within the range determined by the - * bitwidth. + * higher order logic allows comparing between functions + * The current translation does not support this, + * as the translated functions may be different outside + * of the bounds that were relevant for the original + * bit-vectors. */ - if (bvRange.isBitVector()) - { - d_rangeAssertions.insert( - mkRangeConstraint(d_bvToIntCache[current], - current.getType().getBitVectorSize())); + throw TypeCheckingException( + current.toExpr(), + string("Cannot translate to Int: ") + current.toString()); } - break; + else { + translated_children.insert(translated_children.begin(), intUF); + // Insert the term to the cache + d_bvToIntCache[current] = + d_nm->mkNode(kind::APPLY_UF, translated_children); + /** + * Add range constraints if necessary. + * If the original range was a BV sort, the current application of + * the function Must be within the range determined by the + * bitwidth. + */ + if (bvRange.isBitVector()) + { + d_rangeAssertions.insert( + mkRangeConstraint(d_bvToIntCache[current], + current.getType().getBitVectorSize())); + } + } + break; } default: { - if (Theory::theoryOf(current) == THEORY_BOOL) - { + if (childrenTypesChanged(current)) { + /** + * This is "failing on demand": + * We throw an exception if we encounter a case + * that we do not know how to translate, + * only if we actually need to construct a new + * node for such a case. + */ + throw TypeCheckingException( + current.toExpr(), + string("Cannot translate to Int: ") + current.toString()); + } + else { d_bvToIntCache[current] = d_nm->mkNode(oldKind, translated_children); - break; - } - else - { - // Currently, only QF_UFBV formulas are handled. - // In the future, more theories should be supported, e.g., arrays. - Unimplemented(); } + break; } } } @@ -771,6 +791,19 @@ Node BVToInt::bvToInt(Node n) return d_bvToIntCache[n]; } +bool BVToInt::childrenTypesChanged(Node n) { + bool result = false; + for (Node child : n) { + TypeNode originalType = child.getType(); + TypeNode newType = d_bvToIntCache[child].getType(); + if (! newType.isSubtypeOf(originalType)) { + result = true; + break; + } + } + return result; +} + BVToInt::BVToInt(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-to-int"), d_binarizeCache(), diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index dd02d98ec..f0e0ea02e 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -231,6 +231,8 @@ class BVToInt : public PreprocessingPass */ Node modpow2(Node n, uint64_t exponent); + bool childrenTypesChanged(Node n); + /** * Add the range assertions collected in d_rangeAssertions * (using mkRangeConstraint) to the assertion pipeline. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1d096e1fe..d3ba34b6c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1206,7 +1206,6 @@ void SmtEngine::setDefaults() { if (d_logic.isTheoryEnabled(THEORY_BV)) { d_logic = d_logic.getUnlockedCopy(); - d_logic.disableTheory(THEORY_BV); d_logic.enableTheory(THEORY_ARITH); d_logic.arithNonLinear(); d_logic.lock(); |