From e61c6ecf2e8c569d9f1b5f27ec1309371cc45cff Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 15 Sep 2020 21:31:10 -0700 Subject: [PATCH] bv2int: support models in tests (#5068) Previous changes in this preprocessing pass have already enabled model generation when using it. However, the satisfiable tests still had --no-check-models. The changes in this PR: All --no-check-models from current tests for the preprocessing pass are removed. Refactoring of the relevant part of the code. Solves CVC4/cvc4-projects#128. Remark: disabling white-spaces when reviewing this PR is recommended. --- src/preprocessing/passes/bv_to_int.cpp | 70 ++++++++++--------- src/preprocessing/passes/bv_to_int.h | 5 +- test/regress/regress0/bv/bv_to_int1.smt2 | 8 +-- test/regress/regress0/bv/bv_to_int2.smt2 | 6 +- .../regress0/bv/bv_to_int_bitwise.smt2 | 4 +- .../regress/regress0/bv/bv_to_int_bvmul1.smt2 | 7 +- .../regress/regress0/bv/bv_to_int_bvmul2.smt2 | 2 +- .../regress0/bv/bv_to_int_bvuf_to_intuf.smt2 | 2 +- .../bv/bv_to_int_bvuf_to_intuf_sorts.smt2 | 2 +- .../regress0/bv/bv_to_int_elim_err.smt2 | 2 +- test/regress/regress0/bv/bv_to_int_zext.smt2 | 2 +- test/regress/regress2/bv_to_int_ashr.smt2 | 4 +- .../regress2/bv_to_int_mask_array_1.smt2 | 2 +- .../regress2/bv_to_int_mask_array_2.smt2 | 2 +- .../regress2/bv_to_int_mask_array_3.smt2 | 2 +- test/regress/regress2/bv_to_int_shifts.smt2 | 2 +- test/regress/regress3/bv_to_int_and_or.smt2 | 4 +- 17 files changed, 66 insertions(+), 60 deletions(-) diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index e40b828b5..13ad086e8 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -687,11 +687,7 @@ Node BVToInt::translateNoChildren(Node original) uint64_t bvsize = original.getType().getBitVectorSize(); translation = newVar; d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize)); - std::vector args; - Node intToBVOp = d_nm->mkConst(IntToBitVector(bvsize)); - Node newNode = d_nm->mkNode(intToBVOp, newVar); - smt::currentSmtEngine()->defineFunction( - original.toExpr(), args, newNode.toExpr(), true); + defineBVUFAsIntUF(original, newVar); } else if (original.getType().isFunction()) { @@ -756,41 +752,49 @@ Node BVToInt::translateFunctionSymbol(Node bvUF) void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF) { - // This function should only be called after translating - // the function symbol to a new function symbol - // with the right domain and range. - - // get domain and range of the original function - TypeNode tn = bvUF.getType(); - vector bvDomain = tn.getArgTypes(); - TypeNode bvRange = tn.getRangeType(); - + // The resulting term + Node result; + // The type of the resulting term + TypeNode resultType; // symbolic arguments of original function vector args; - // children of the new symbolic application - vector achildren; - achildren.push_back(intUF); - int i = 0; - for (TypeNode d : bvDomain) - { - // Each bit-vector argument is casted to a natural number - // Other arguments are left intact. - Node fresh_bound_var = d_nm->mkBoundVar(d); - args.push_back(fresh_bound_var.toExpr()); - Node castedArg = args[i]; - if (d.isBitVector()) + if (!bvUF.getType().isFunction()) { + // bvUF is a variable. + // in this case, the result is just the original term + // (it will be casted later if needed) + result = intUF; + resultType = bvUF.getType(); + } else { + // bvUF is a function with arguments + // The arguments need to be casted as well. + TypeNode tn = bvUF.getType(); + resultType = tn.getRangeType(); + vector bvDomain = tn.getArgTypes(); + // children of the new symbolic application + vector achildren; + achildren.push_back(intUF); + int i = 0; + for (const TypeNode& d : bvDomain) { - castedArg = castToType(castedArg, d_nm->integerType()); + // Each bit-vector argument is casted to a natural number + // Other arguments are left intact. + Node fresh_bound_var = d_nm->mkBoundVar(d); + args.push_back(fresh_bound_var.toExpr()); + Node castedArg = args[i]; + if (d.isBitVector()) + { + castedArg = castToType(castedArg, d_nm->integerType()); + } + achildren.push_back(castedArg); + i++; } - achildren.push_back(castedArg); - i++; + result = d_nm->mkNode(kind::APPLY_UF, achildren); } - Node intApplication = d_nm->mkNode(kind::APPLY_UF, achildren); - // If the range is BV, the application needs to be casted back. - intApplication = castToType(intApplication, bvRange); + // If the result is BV, it needs to be casted back. + result = castToType(result, resultType); // add the function definition to the smt engine. smt::currentSmtEngine()->defineFunction( - bvUF.toExpr(), args, intApplication.toExpr(), true); + bvUF.toExpr(), args, result.toExpr(), true); } bool BVToInt::childrenTypesChanged(Node n) diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index db2d08b7d..b84726878 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -289,11 +289,12 @@ class BVToInt : public PreprocessingPass * When a UF f is translated to a UF g, * we add a define-fun command to the smt-engine * to relate between f and g. + * We do the same when f and g are just variables. * This is useful, for example, when asking * for a model-value of a term that includes the * original UF f. - * @param bvUF the original function - * @param intUF the translated function + * @param bvUF the original function or variable + * @param intUF the translated function or variable */ void defineBVUFAsIntUF(Node bvUF, Node intUF); diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index f812ccbc8..970a9fd75 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2 index 00fd51baf..d60f4903b 100644 --- a/test/regress/regress0/bv/bv_to_int2.smt2 +++ b/test/regress/regress0/bv/bv_to_int2.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2 index 6f08c2e8d..444551776 100644 --- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 index ec4206812..e21415244 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 @@ -1,10 +1,11 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) (declare-fun b () (_ BitVec 8)) (assert (bvult (bvmul a b) (bvudiv a b))) +(assert (bvugt a (_ bv0 8))) (check-sat) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 index 4e940b5df..4bbe5685e 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun T4_180 () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 index c621aa112..5879542eb 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 index 8fbe96eab..f43c8c860 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) (declare-sort S 0) diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 index b17aeeacf..01ee5dad8 100644 --- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 +++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_BV) (declare-fun _substvar_183_ () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2 index ab09d7341..42e06a940 100644 --- a/test/regress/regress0/bv/bv_to_int_zext.smt2 +++ b/test/regress/regress0/bv/bv_to_int_zext.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun T1_31078 () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2 index 3f2d90a00..11952839f 100644 --- a/test/regress/regress2/bv_to_int_ashr.smt2 +++ b/test/regress/regress2/bv_to_int_ashr.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2 index 394a1d876..970f27fb9 100644 --- a/test/regress/regress2/bv_to_int_mask_array_1.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: unsat (set-logic ALL) (declare-fun A () (Array Int Int)) diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2 index 36eabdb28..0960b9359 100644 --- a/test/regress/regress2/bv_to_int_mask_array_2.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: sat (set-logic ALL) (declare-fun A () (Array Int Int)) diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2 index 7eef1ad4e..329ee715a 100644 --- a/test/regress/regress2/bv_to_int_mask_array_3.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: sat (set-logic ALL) (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4))) diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2 index d213b0c3d..7971b2bfe 100644 --- a/test/regress/regress2/bv_to_int_shifts.smt2 +++ b/test/regress/regress2/bv_to_int_shifts.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: sat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2 index 3dc179aea..2524e8772 100644 --- a/test/regress/regress3/bv_to_int_and_or.smt2 +++ b/test/regress/regress3/bv_to_int_and_or.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 4)) -- 2.30.2