From aed4619066f24546ff8370fc86e9be1773a68c4b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 17 Mar 2016 13:14:43 +0000 Subject: [PATCH 1/3] reduce-args: fixed unsoundness introduced in my previous commit skip an UF arg if it's quantified e.g. forall a . f(a, b) -> f(b) (but not f) --- src/tactic/core/reduce_args_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 4f6f4c3d7..aee136284 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -96,10 +96,10 @@ struct reduce_args_tactic::imp { expr *lhs, *rhs; if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) { base = rhs; - } else { - base = e; + return true; } - return true; + base = e; + return !is_var(e); } static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { From facb42139856fb995fbb0586eac56db351f78483 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 17 Mar 2016 13:27:07 +0000 Subject: [PATCH 2/3] reduce-args: fix unsoundness 2: f(v + 2), where b is quantified --- src/tactic/core/reduce_args_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index aee136284..cfb9a1eb8 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -96,10 +96,10 @@ struct reduce_args_tactic::imp { expr *lhs, *rhs; if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) { base = rhs; - return true; + } else { + base = e; } - base = e; - return !is_var(e); + return !is_var(base); } static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { From f5c4800eecbfcbc94ce0ce491670f96a9fd6ea3c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 17 Mar 2016 15:29:48 +0000 Subject: [PATCH 3/3] reduce-args: last fix for may_be_unique to support quantified variables in arbitrary exprs --- src/tactic/core/reduce_args_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index cfb9a1eb8..ec7353044 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -19,6 +19,7 @@ Notes: #include"tactical.h" #include"cooperate.h" #include"ast_smt2_pp.h" +#include"has_free_vars.h" #include"map.h" #include"rewriter_def.h" #include"extension_model_converter.h" @@ -99,7 +100,7 @@ struct reduce_args_tactic::imp { } else { base = e; } - return !is_var(base); + return !has_free_vars(base); } static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {