From 521d975c84c40195d55ebe2560320fd2a6761898 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Nov 2012 14:18:20 -0800 Subject: [PATCH] additional array handling routines Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_context.cpp | 11 +++-- src/muz_qe/pdr_util.cpp | 1 + src/smt/smt_implied_equalities.cpp | 42 ++--------------- src/smt/smt_value_sort.cpp | 74 ++++++++++++++++++++++++++++++ src/smt/smt_value_sort.h | 37 +++++++++++++++ 5 files changed, 121 insertions(+), 44 deletions(-) create mode 100644 src/smt/smt_value_sort.cpp create mode 100644 src/smt/smt_value_sort.h diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 909a42625..227b1aee7 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -43,6 +43,7 @@ Notes: #include "qe_lite.h" #include "ast_ll_pp.h" #include "proof_checker.h" +#include "smt_value_sort.h" namespace pdr { @@ -1827,14 +1828,14 @@ namespace pdr { if (!vars.empty()) { // also fresh names for auxiliary variables in body? expr_substitution sub(m); - expr_ref_vector refs(m); expr_ref tmp(m); proof_ref pr(m); pr = m.mk_asserted(m.mk_true()); - for (unsigned i = 0; i < vars.size(); ++i) { - VERIFY (M->eval(vars[i].get(), tmp, true)); - refs.push_back(tmp); - sub.insert(vars[i].get(), tmp, pr); + for (unsigned i = 0; i < vars.size(); ++i) { + if (smt::is_value_sort(m, vars[i].get())) { + VERIFY (M->eval(vars[i].get(), tmp, true)); + sub.insert(vars[i].get(), tmp, pr); + } } if (!rep) rep = mk_expr_simp_replacer(m); rep->set_substitution(&sub); diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 0840f1d73..6907d82a0 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -904,6 +904,7 @@ namespace pdr { return !has_x; } + void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { ast_manager& m = fml.get_manager(); expr_ref_vector conjs(m); diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index ef8d27e2f..91784f5f5 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -29,6 +29,7 @@ Revision History: #include "array_decl_plugin.h" #include "uint_set.h" #include "model_v2_pp.h" +#include "smt_value_sort.h" namespace smt { @@ -134,44 +135,7 @@ namespace smt { } } } - } - - bool is_simple_type(sort* s) { - arith_util arith(m); - datatype_util data(m); - - ptr_vector sorts; - ast_mark mark; - sorts.push_back(s); - - while (!sorts.empty()) { - s = sorts.back(); - sorts.pop_back(); - if (mark.is_marked(s)) { - continue; - } - mark.mark(s, true); - if (arith.is_int_real(s)) { - // simple - } - else if (m.is_bool(s)) { - // simple - } - else if (data.is_datatype(s)) { - ptr_vector const& cs = *data.get_datatype_constructors(s); - for (unsigned i = 0; i < cs.size(); ++i) { - func_decl* f = cs[i]; - for (unsigned j = 0; j < f->get_arity(); ++j) { - sorts.push_back(f->get_domain(j)); - } - } - } - else { - return false; - } - } - return true; - } + } /** \brief Extract implied equalities for a collection of terms in the current context. @@ -216,7 +180,7 @@ namespace smt { uint_set non_values; - if (!is_simple_type(srt)) { + if (!is_value_sort(m, srt)) { for (unsigned i = 0; i < terms.size(); ++i) { non_values.insert(i); } diff --git a/src/smt/smt_value_sort.cpp b/src/smt/smt_value_sort.cpp new file mode 100644 index 000000000..a840b77b7 --- /dev/null +++ b/src/smt/smt_value_sort.cpp @@ -0,0 +1,74 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + smt_value_sort.cpp + +Abstract: + + Determine if elements of a given sort can be values. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-25 + +Revision History: + + +--*/ + +#include "smt_value_sort.h" +#include "bv_decl_plugin.h" +#include "arith_decl_plugin.h" +#include "datatype_decl_plugin.h" + +namespace smt { + + + bool is_value_sort(ast_manager& m, sort* s) { + arith_util arith(m); + datatype_util data(m); + bv_util bv(m); + + ptr_vector sorts; + ast_mark mark; + sorts.push_back(s); + + while (!sorts.empty()) { + s = sorts.back(); + sorts.pop_back(); + if (mark.is_marked(s)) { + continue; + } + mark.mark(s, true); + if (arith.is_int_real(s)) { + // simple + } + else if (m.is_bool(s)) { + // simple + } + else if (bv.is_bv_sort(s)) { + // simple + } + else if (data.is_datatype(s)) { + ptr_vector const& cs = *data.get_datatype_constructors(s); + for (unsigned i = 0; i < cs.size(); ++i) { + func_decl* f = cs[i]; + for (unsigned j = 0; j < f->get_arity(); ++j) { + sorts.push_back(f->get_domain(j)); + } + } + } + else { + return false; + } + } + return true; + } + + bool is_value_sort(ast_manager& m, expr* e) { + return is_value_sort(m, m.get_sort(e)); + } + +} diff --git a/src/smt/smt_value_sort.h b/src/smt/smt_value_sort.h new file mode 100644 index 000000000..ae32be62a --- /dev/null +++ b/src/smt/smt_value_sort.h @@ -0,0 +1,37 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + smt_value_sort.h + +Abstract: + + Determine if elements of a given sort can be values. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-25 + +Revision History: + + +--*/ + + +#ifndef __SMT_VALUE_SORT_H__ +#define __SMT_VALUE_SORT_H__ + +#include "ast.h" + + +namespace smt { + + bool is_value_sort(ast_manager& m, sort* s); + + bool is_value_sort(ast_manager& m, expr* e); + +}; + + +#endif