From 77442e796f0f0997d64b5d44ff8afc831ee5abdd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Dec 2021 18:45:16 +0000 Subject: [PATCH 1/6] fix typo quanitfiers -> quantifiers This fixes a typo in the name of the directory of one of the tests. --- .../{quanitfiers => quantifiers}/quantifier-scoping.desc | 0 .../{quanitfiers => quantifiers}/quantifier-scoping.smt2 | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename regression/smt2_solver/{quanitfiers => quantifiers}/quantifier-scoping.desc (100%) rename regression/smt2_solver/{quanitfiers => quantifiers}/quantifier-scoping.smt2 (100%) diff --git a/regression/smt2_solver/quanitfiers/quantifier-scoping.desc b/regression/smt2_solver/quantifiers/quantifier-scoping.desc similarity index 100% rename from regression/smt2_solver/quanitfiers/quantifier-scoping.desc rename to regression/smt2_solver/quantifiers/quantifier-scoping.desc diff --git a/regression/smt2_solver/quanitfiers/quantifier-scoping.smt2 b/regression/smt2_solver/quantifiers/quantifier-scoping.smt2 similarity index 100% rename from regression/smt2_solver/quanitfiers/quantifier-scoping.smt2 rename to regression/smt2_solver/quantifiers/quantifier-scoping.smt2 From 5828e70dd55d80bf134e92085bb73af3e5b388dc Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 29 Dec 2021 11:00:21 +0000 Subject: [PATCH 2/6] rename instantiate_quantifier function Quantifier instantiation may happen eagerly, or incrementally, and renaming this function clarifies that this function is doing eager instantiation. --- src/solvers/flattening/boolbv_quantifier.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index e7b44f4358d..4beebd3969c 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -138,8 +138,9 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr) return {}; } -static optionalt -instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns) +static optionalt eager_quantifier_instantiation( + const quantifier_exprt &expr, + const namespacet &ns) { const symbol_exprt &var_expr = expr.symbol(); @@ -223,7 +224,7 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src) auto new_src = quantifier_exprt(src.id(), std::move(fresh_symbols), where_replaced); - const auto res = instantiate_quantifier(src, ns); + const auto res = eager_quantifier_instantiation(src, ns); if(res) return convert_bool(*res); From 782beb81dc4b415d7381fec6e662f8330bb1cfc9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Dec 2021 19:23:20 +0000 Subject: [PATCH 3/6] don't fail on quantifiers with more than one symbol This adds support for eager instantiation of forall or exists quantifier expressions that have more than one symbol using the trivial rewrite. --- .../smt2_solver/quantifiers/boolean-quantifier.desc | 7 +++++++ .../smt2_solver/quantifiers/boolean-quantifier.smt2 | 13 +++++++++++++ src/solvers/flattening/boolbv_quantifier.cpp | 12 ++++++++++++ 3 files changed, 32 insertions(+) create mode 100644 regression/smt2_solver/quantifiers/boolean-quantifier.desc create mode 100644 regression/smt2_solver/quantifiers/boolean-quantifier.smt2 diff --git a/regression/smt2_solver/quantifiers/boolean-quantifier.desc b/regression/smt2_solver/quantifiers/boolean-quantifier.desc new file mode 100644 index 00000000000..eb37a4bbf91 --- /dev/null +++ b/regression/smt2_solver/quantifiers/boolean-quantifier.desc @@ -0,0 +1,7 @@ +CORE +boolean-quantifier.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- diff --git a/regression/smt2_solver/quantifiers/boolean-quantifier.smt2 b/regression/smt2_solver/quantifiers/boolean-quantifier.smt2 new file mode 100644 index 00000000000..0d560278a67 --- /dev/null +++ b/regression/smt2_solver/quantifiers/boolean-quantifier.smt2 @@ -0,0 +1,13 @@ +(assert (exists ((b Bool)) b)) +(assert (exists ((b Bool)) (not b))) + +(assert (not (forall ((b Bool)) b))) +(assert (not (forall ((b Bool)) (not b)))) + +(assert (exists ((a Bool) (b Bool)) (= a b))) +(assert (not (forall ((a Bool) (b Bool)) (= a b)))) + +(assert (forall ((a Bool)) (exists ((b Bool)) (= a b)))) + +(check-sat) +(get-model) diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 4beebd3969c..389a184cbe4 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -142,6 +142,18 @@ static optionalt eager_quantifier_instantiation( const quantifier_exprt &expr, const namespacet &ns) { + if(expr.variables().size() > 1) + { + // Qx,y.P(x,y) is the same as Qx.Qy.P(x,y) + auto new_variables = expr.variables(); + new_variables.pop_back(); + auto new_expression = quantifier_exprt( + expr.id(), + expr.variables().back(), + quantifier_exprt(expr.id(), new_variables, expr.where())); + return eager_quantifier_instantiation(new_expression, ns); + } + const symbol_exprt &var_expr = expr.symbol(); /** From fb6b286d6a250a2691c1c06784edaa0eee61c55c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Dec 2021 19:35:44 +0000 Subject: [PATCH 4/6] add expansion for quantifiers over booleans This adds support for eager instantiation of quantifiers over booleans, using George Boole's Proposition II. --- .../quantifiers/boolean-quantifier.desc | 2 +- .../quantifiers/boolean-quantifier.smt2 | 18 +++++----- src/solvers/flattening/boolbv_quantifier.cpp | 36 ++++++++++++++----- 3 files changed, 39 insertions(+), 17 deletions(-) diff --git a/regression/smt2_solver/quantifiers/boolean-quantifier.desc b/regression/smt2_solver/quantifiers/boolean-quantifier.desc index eb37a4bbf91..ef27ee4dbbb 100644 --- a/regression/smt2_solver/quantifiers/boolean-quantifier.desc +++ b/regression/smt2_solver/quantifiers/boolean-quantifier.desc @@ -3,5 +3,5 @@ boolean-quantifier.smt2 ^EXIT=0$ ^SIGNAL=0$ -^sat$ +^unsat$ -- diff --git a/regression/smt2_solver/quantifiers/boolean-quantifier.smt2 b/regression/smt2_solver/quantifiers/boolean-quantifier.smt2 index 0d560278a67..bdc88d48d6f 100644 --- a/regression/smt2_solver/quantifiers/boolean-quantifier.smt2 +++ b/regression/smt2_solver/quantifiers/boolean-quantifier.smt2 @@ -1,13 +1,15 @@ -(assert (exists ((b Bool)) b)) -(assert (exists ((b Bool)) (not b))) +(define-fun q1 () Bool (exists ((b Bool)) b)) +(define-fun q2 () Bool (exists ((b Bool)) (not b))) -(assert (not (forall ((b Bool)) b))) -(assert (not (forall ((b Bool)) (not b)))) +(define-fun q3 () Bool (not (forall ((b Bool)) b))) +(define-fun q4 () Bool (not (forall ((b Bool)) (not b)))) -(assert (exists ((a Bool) (b Bool)) (= a b))) -(assert (not (forall ((a Bool) (b Bool)) (= a b)))) +(define-fun q5 () Bool (exists ((a Bool) (b Bool)) (= a b))) +(define-fun q6 () Bool (not (forall ((a Bool) (b Bool)) (= a b)))) -(assert (forall ((a Bool)) (exists ((b Bool)) (= a b)))) +(define-fun q7 () Bool (forall ((a Bool)) (exists ((b Bool)) (= a b)))) + +; the above are all valid, and we assert one of them is not +(assert (not (and q1 q2 q3 q4 q5 q6 q7))) (check-sat) -(get-model) diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 389a184cbe4..dde352e1a06 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -168,8 +168,30 @@ static optionalt eager_quantifier_instantiation( return re; } - const optionalt min_i = get_quantifier_var_min(var_expr, re); - const optionalt max_i = get_quantifier_var_max(var_expr, re); + if(var_expr.is_boolean()) + { + // Expand in full. + // This grows worst-case exponentially in the quantifier nesting depth. + if(expr.id() == ID_forall) + { + // ∀b.f(b) <===> f(0)∧f(1) + return and_exprt( + expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()})); + } + else if(expr.id() == ID_exists) + { + // ∃b.f(b) <===> f(0)∨f(1) + return or_exprt( + expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()})); + } + else + UNREACHABLE; + } + + const optionalt min_i = + get_quantifier_var_min(var_expr, re); + const optionalt max_i = + get_quantifier_var_max(var_expr, re); if(!min_i.has_value() || !max_i.has_value()) return nullopt; @@ -177,20 +199,18 @@ static optionalt eager_quantifier_instantiation( mp_integer lb = numeric_cast_v(min_i.value()); mp_integer ub = numeric_cast_v(max_i.value()); - if(lb>ub) + if(lb > ub) return nullopt; std::vector expr_insts; - for(mp_integer i=lb; i<=ub; ++i) + for(mp_integer i = lb; i <= ub; ++i) { exprt constraint_expr = re; - replace_expr(var_expr, - from_integer(i, var_expr.type()), - constraint_expr); + replace_expr(var_expr, from_integer(i, var_expr.type()), constraint_expr); expr_insts.push_back(constraint_expr); } - if(expr.id()==ID_forall) + if(expr.id() == ID_forall) { // maintain the domain constraint if it isn't guaranteed by the // instantiations (for a disjunction the domain constraint is implied by the From 68503512707ed0460c6f6eca2fabf28604117726 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Dec 2021 20:17:42 +0000 Subject: [PATCH 5/6] use quantifier_exprt::instantiate instead of replace_expr The quantifier_exprt offers a convenient wrapper for doing the instantiation. --- src/solvers/flattening/boolbv_quantifier.cpp | 36 +++++++++++--------- 1 file changed, 20 insertions(+), 16 deletions(-) diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index dde352e1a06..7283c86c208 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include /// A method to detect equivalence between experts that can contain typecast @@ -161,11 +160,11 @@ static optionalt eager_quantifier_instantiation( * an OR/AND expr. **/ - const exprt re = simplify_expr(expr.where(), ns); + const exprt where_simplified = simplify_expr(expr.where(), ns); - if(re.is_true() || re.is_false()) + if(where_simplified.is_true() || where_simplified.is_false()) { - return re; + return where_simplified; } if(var_expr.is_boolean()) @@ -189,9 +188,9 @@ static optionalt eager_quantifier_instantiation( } const optionalt min_i = - get_quantifier_var_min(var_expr, re); + get_quantifier_var_min(var_expr, where_simplified); const optionalt max_i = - get_quantifier_var_max(var_expr, re); + get_quantifier_var_max(var_expr, where_simplified); if(!min_i.has_value() || !max_i.has_value()) return nullopt; @@ -202,40 +201,45 @@ static optionalt eager_quantifier_instantiation( if(lb > ub) return nullopt; + auto expr_simplified = + quantifier_exprt(expr.id(), expr.variables(), where_simplified); + std::vector expr_insts; for(mp_integer i = lb; i <= ub; ++i) { - exprt constraint_expr = re; - replace_expr(var_expr, from_integer(i, var_expr.type()), constraint_expr); + exprt constraint_expr = + expr_simplified.instantiate({from_integer(i, var_expr.type())}); expr_insts.push_back(constraint_expr); } if(expr.id() == ID_forall) { - // 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) + // maintain the domain constraint if it isn't guaranteed + // by the instantiations (for a disjunction the domain + // constraint is implied by the instantiations) + if(where_simplified.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) { - // 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) + // maintain the domain constraint if it isn't trivially satisfied + // by the instantiations (for a conjunction the instantiations are + // stronger constraints) + if(where_simplified.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); } From e4c5999537d4d702dfb69d3b65d747fdaf72bbe3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Dec 2021 20:17:56 +0000 Subject: [PATCH 6/6] add a test for quantifiers over bit vectors The test currently fails, and will need an implementation. --- .../quantifiers/bv-quantifier-valid.desc | 7 +++++++ .../quantifiers/bv-quantifier-valid.smt2 | 15 +++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 regression/smt2_solver/quantifiers/bv-quantifier-valid.desc create mode 100644 regression/smt2_solver/quantifiers/bv-quantifier-valid.smt2 diff --git a/regression/smt2_solver/quantifiers/bv-quantifier-valid.desc b/regression/smt2_solver/quantifiers/bv-quantifier-valid.desc new file mode 100644 index 00000000000..e5bb1d2ebbb --- /dev/null +++ b/regression/smt2_solver/quantifiers/bv-quantifier-valid.desc @@ -0,0 +1,7 @@ +KNOWNBUG +bv-quantifier-valid.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/quantifiers/bv-quantifier-valid.smt2 b/regression/smt2_solver/quantifiers/bv-quantifier-valid.smt2 new file mode 100644 index 00000000000..06d04920136 --- /dev/null +++ b/regression/smt2_solver/quantifiers/bv-quantifier-valid.smt2 @@ -0,0 +1,15 @@ +(define-fun q1 () Bool (exists ((b (_ BitVec 8))) (= b #x00))) +(define-fun q2 () Bool (exists ((b (_ BitVec 8))) (not (= b #x00)))) + +(define-fun q3 () Bool (not (forall ((b (_ BitVec 8))) (= b #x00)))) +(define-fun q4 () Bool (not (forall ((b (_ BitVec 8))) (not (= b #x00))))) + +(define-fun q5 () Bool (exists ((a (_ BitVec 8)) (b (_ BitVec 8))) (= a b))) +(define-fun q6 () Bool (not (forall ((a (_ BitVec 8)) (b (_ BitVec 8))) (= a b)))) + +(define-fun q7 () Bool (forall ((a (_ BitVec 8))) (exists ((b (_ BitVec 8))) (= a b)))) + +; the above are all valid, and we assert one of them is not +(assert (not (and q1 q2 q3 q4 q5 q6 q7))) + +(check-sat)