diff --git a/regression/cbmc/Quantifiers-not-exists/main.c b/regression/cbmc-cover/Quantifiers-not-exists/main.c similarity index 66% rename from regression/cbmc/Quantifiers-not-exists/main.c rename to regression/cbmc-cover/Quantifiers-not-exists/main.c index 60a3e7cc2bd..b3f490a1c51 100644 --- a/regression/cbmc/Quantifiers-not-exists/main.c +++ b/regression/cbmc-cover/Quantifiers-not-exists/main.c @@ -1,6 +1,5 @@ int main() { - int a[2][2]; int b[2][2]; int c[2][2]; @@ -25,16 +24,15 @@ int main() assert(0); - assert(a[0][0]>10); - - assert( (b[0][0]<1||b[0][0]>10) && (b[0][1]<1||b[0][1]>10)); - assert( (b[1][0]<1||b[1][0]>10) && (b[1][1]<1||b[1][1]>10)); + assert(a[0][0] > 10); - assert(c[0][0]==0 || c[0][1]==0 || c[1][0]<=10 || c[1][1]<=10); + assert((b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10)); + assert((b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10)); - assert( ((d[0][0]<1||d[0][0]>10) || (d[0][1]<1||d[0][1]>10)) ); - assert( ((d[1][0]<1||d[1][0]>10) || (d[1][1]<1||d[1][1]>10)) ); + assert(c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10); + assert(((d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10))); + assert(((d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10))); return 0; } diff --git a/regression/cbmc-cover/Quantifiers-not-exists/test.desc b/regression/cbmc-cover/Quantifiers-not-exists/test.desc new file mode 100644 index 00000000000..c6bdeab2b1b --- /dev/null +++ b/regression/cbmc-cover/Quantifiers-not-exists/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--cover location +^\*\* 1 of 46 covered \(2.2%\) +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +All assertions are unreachable as each of the __CPROVER_assume evaluate to false +(!exists i. i>=0 && i<2 ==> ... is equivalent to forall i. i>=0 && i<2 && ..., +where neither i>=0 nor i<2 is actually true for all values of i). diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 419831fd273..46ce7f990fa 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-if/main.c b/regression/cbmc/Quantifiers-if/main.c index 66bfe889214..044fe9784ec 100644 --- a/regression/cbmc/Quantifiers-if/main.c +++ b/regression/cbmc/Quantifiers-if/main.c @@ -9,16 +9,16 @@ int main() if(__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 }) __CPROVER_assert(0, "failure 1"); - if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 }) + if(__CPROVER_exists { int i; (i>=0 && i<2) && a[i]>=1 && a[i]<=10 }) __CPROVER_assert(0, "failure 2"); if(__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=2 && a[i]<=10 }) __CPROVER_assert(0, "success 1"); - if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=2 && a[i]<=10 }) + if(__CPROVER_exists { int i; (i>=0 && i<2) && a[i]>=2 && a[i]<=10 }) __CPROVER_assert(0, "failure 3"); - if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 }) + if(__CPROVER_exists { int i; (i>=0 && i<2) && a[i]>=5 && a[i]<=10 }) __CPROVER_assert(0, "success 2"); // clang-format on diff --git a/regression/cbmc/Quantifiers-invalid-var-range/main.c b/regression/cbmc/Quantifiers-invalid-var-range/main.c index 41e0ad38908..b2850470d37 100644 --- a/regression/cbmc/Quantifiers-invalid-var-range/main.c +++ b/regression/cbmc/Quantifiers-invalid-var-range/main.c @@ -4,7 +4,8 @@ int main() int a[3][3]; // clang-format off // clang-format would rewrite the "==>" as "== >" - __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> __CPROVER_exists{int j; (j>=i && j<3) ==> a[i][j]==10} }); + // NOLINTNEXTLINE(whitespace/line_length) + __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> __CPROVER_exists{int j; (j>=i && j<3) && a[i][j]==10} }); // clang-format on assert(a[0][0]==10||a[0][1]==10||a[0][2]==10); diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc deleted file mode 100644 index 62a58c2e4d9..00000000000 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ /dev/null @@ -1,20 +0,0 @@ -KNOWNBUG -main.c - -^\*\* Results:$ -^\[main.assertion.5\] line 28 assertion a\[.*\]\[.*\] > 10: SUCCESS$ -^\[main.assertion.6\] line 30 assertion tmp_if_expr\$\d+: SUCCESS$ -^\[main.assertion.7\] line 31 assertion tmp_if_expr\$\d+: SUCCESS$ -^\[main.assertion.8\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$ -^\[main.assertion.9\] line 35 assertion tmp_if_expr\$\d+: SUCCESS$ -^\[main.assertion.10\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$ -^\*\* 0 of 10 failed -^VERIFICATION SUCCESSFUL$ -^EXIT=0$ -^SIGNAL=0$ --- -^warning: ignoring --- -All assertions are unreachable as each of the __CPROVER_assume evaluate to false -(!exists i. i>=0 && i<2 ==> ... is equivalent to forall i. i>=0 && i<2 && ..., -where neither i>=0 nor i<2 is actually true for all values of i). diff --git a/regression/cbmc/Quantifiers-not/main.c b/regression/cbmc/Quantifiers-not/main.c index 6a2b82e8fb2..844a51ade40 100644 --- a/regression/cbmc/Quantifiers-not/main.c +++ b/regression/cbmc/Quantifiers-not/main.c @@ -9,16 +9,16 @@ int main() if(!__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 }) __CPROVER_assert(0, "success 1"); - if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 }) + if(!__CPROVER_exists { int i; (i>=0 && i<2) && a[i]>=1 && a[i]<=10 }) __CPROVER_assert(0, "success 2"); if(!__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=2 && a[i]<=10 }) __CPROVER_assert(0, "failure 1"); - if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=2 && a[i]<=10 }) + if(!__CPROVER_exists { int i; (i>=0 && i<2) && a[i]>=2 && a[i]<=10 }) __CPROVER_assert(0, "success 3"); - if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 }) + if(!__CPROVER_exists { int i; (i>=0 && i<2) && a[i]>=5 && a[i]<=10 }) __CPROVER_assert(0, "failure 2"); // clang-format on diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index 1ab76094ef1..f12ffbd5519 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^\*\* Results:$ diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 7efd7100cb7..19d9b6453d8 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -238,6 +238,11 @@ class boolbvt:public arrayst class quantifiert { public: + quantifiert(exprt _expr, literalt _l) + : expr(std::move(_expr)), l(std::move(_l)) + { + } + exprt expr; literalt l; }; diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index e2161a4ded6..e6fa39b16a3 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -9,28 +9,23 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" #include +#include #include #include #include #include /// A method to detect equivalence between experts that can contain typecast -bool expr_eq(const exprt &expr1, const exprt &expr2) +static bool expr_eq(const exprt &expr1, const exprt &expr2) { - exprt e1=expr1, e2=expr2; - if(expr1.id()==ID_typecast) - e1=expr1.op0(); - if(expr2.id()==ID_typecast) - e2=expr2.op0(); - return e1==e2; + return skip_typecast(expr1) == skip_typecast(expr2); } /// To obtain the min value for the quantifier variable of the specified /// forall/exists operator. The min variable is in the form of "!(var_expr > /// constant)". -exprt get_quantifier_var_min( - const exprt &var_expr, - const exprt &quantifier_expr) +static exprt +get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr) { PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and); @@ -75,9 +70,8 @@ exprt get_quantifier_var_min( /// To obtain the max value for the quantifier variable of the specified /// forall/exists operator. -exprt get_quantifier_var_max( - const exprt &var_expr, - const exprt &quantifier_expr) +static exprt +get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr) { PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and); exprt res = false_exprt(); @@ -132,11 +126,9 @@ exprt get_quantifier_var_max( return res; } -optionalt +static optionalt instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns) { - PRECONDITION(expr.id() == ID_forall || expr.id() == ID_exists); - const symbol_exprt &var_expr = expr.symbol(); /** @@ -144,15 +136,15 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns) * an OR/AND expr. **/ - const exprt &re = simplify_expr(expr.where(), ns); + const exprt re = simplify_expr(expr.where(), ns); if(re.is_true() || re.is_false()) { return re; } - const exprt &min_i = get_quantifier_var_min(var_expr, re); - const exprt &max_i = get_quantifier_var_max(var_expr, re); + const exprt min_i = get_quantifier_var_min(var_expr, re); + const exprt max_i = get_quantifier_var_max(var_expr, re); if(min_i.is_false() || max_i.is_false()) return nullopt; @@ -175,50 +167,57 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns) if(expr.id()==ID_forall) { - return conjunction(expr_insts); + // maintain the domain constraint if it isn't guaranteed by the + // instantiations (for a disjunction the domain constraint is implied by the + // instantiations) + if(re.id() == ID_and) + { + expr_insts.push_back(binary_predicate_exprt( + var_expr, ID_gt, from_integer(lb, var_expr.type()))); + expr_insts.push_back(binary_predicate_exprt( + var_expr, ID_le, from_integer(ub, var_expr.type()))); + } + return simplify_expr(conjunction(expr_insts), ns); } else if(expr.id() == ID_exists) { - return disjunction(expr_insts); + // maintain the domain constraint if it isn't trivially satisfied by the + // instantiations (for a conjunction the instantiations are stronger + // constraints) + if(re.id() == ID_or) + { + expr_insts.push_back(binary_predicate_exprt( + var_expr, ID_gt, from_integer(lb, var_expr.type()))); + expr_insts.push_back(binary_predicate_exprt( + var_expr, ID_le, from_integer(ub, var_expr.type()))); + } + return simplify_expr(disjunction(expr_insts), ns); } UNREACHABLE; - return nullopt; } literalt boolbvt::convert_quantifier(const quantifier_exprt &src) { PRECONDITION(src.id() == ID_forall || src.id() == ID_exists); - quantifier_exprt expr(src); - const auto res = instantiate_quantifier(expr, ns); + const auto res = instantiate_quantifier(src, ns); - if(!res) - { - return SUB::convert_rest(src); - } - - quantifiert quantifier; - quantifier.expr = *res; - quantifier_list.push_back(quantifier); + if(res) + return convert_bool(*res); - literalt l=prop.new_variable(); - quantifier_list.back().l=l; + // we failed to instantiate here, need to pass to post-processing + quantifier_list.emplace_back(quantifiert(src, prop.new_variable())); - return l; + return quantifier_list.back().l; } void boolbvt::post_process_quantifiers() { - std::set instances; - if(quantifier_list.empty()) return; - for(auto it=quantifier_list.begin(); - it!=quantifier_list.end(); - ++it) - { - prop.set_equal(convert_bool(it->expr), it->l); - } + // we do not yet have any elaborate post-processing + for(const auto &q : quantifier_list) + conversion_failed(q.expr); }