From 9f378bb1b985c9d670271ba11613bed7b05e71fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Apr 2020 15:51:18 -0700 Subject: [PATCH] #4099 --- src/smt/theory_array.cpp | 12 +-- src/smt/value_generator.cpp | 204 ++++++++++++++++++++++++++++++++++++ src/smt/value_generator.h | 17 +++ 3 files changed, 227 insertions(+), 6 deletions(-) create mode 100644 src/smt/value_generator.cpp create mode 100644 src/smt/value_generator.h diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 9e341bb7877..8683b59022f 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -53,12 +53,12 @@ namespace smt { var_data * d2 = m_var_data[v2]; if (!d1->m_prop_upward && d2->m_prop_upward) set_prop_upward(v1); - for (enode* n : d2->m_stores) - add_store(v1, n); - for (enode* n : d2->m_parent_stores) - add_parent_store(v1, n); - for (enode* n : d2->m_parent_selects) - add_parent_select(v1, n); + for (unsigned i = 0; i < d2->m_stores.size(); ++i) + add_store(v1, d2->m_stores[i]); + for (unsigned i = 0; i < d2->m_parent_stores.size(); ++i) + add_parent_store(v1, d2->m_parent_stores[i]); + for (unsigned i = 0; i < d2->m_parent_selects.size(); ++i) + add_parent_select(v1, d2->m_parent_selects[i]); TRACE("array", tout << "after merge\n"; display_var(tout, v1);); } diff --git a/src/smt/value_generator.cpp b/src/smt/value_generator.cpp new file mode 100644 index 00000000000..6f24537e47d --- /dev/null +++ b/src/smt/value_generator.cpp @@ -0,0 +1,204 @@ +#include "smt/value_generator.h" +#include + + +class datatype_value_generator : public value_generator_core { + ast_manager& m; + value_generator& g; + datatype_util dt; + sort_ref_vector m_sorts; + obj_map m_values; + obj_map m_constr2seen; + + /* + \brief inverse of the Cantor function. + It converts an unsigned into a pair of unsigned numbers that are not + bigger (and only equal for values 0, 1). + */ + void inverse_cantor(unsigned z, unsigned& x, unsigned& y) { + unsigned w = (sqrt(8*z + 1) - 1)/2; + unsigned t = (w*w + 2)/2; + y = z - t; + x = w - y; + } + + unsigned_vector inf; + void index2vector(unsigned z, func_decl* c, unsigned_vector& v) { + unsigned arity = c->get_arity(); + v.resize(arity); + inf.reset(); + for (unsigned i = 0; i < arity; ++i) { + sort* s = c->get_domain(i); + sort_size const& sz = s->get_num_elements(); + if (sz.is_finite() && sz.size() < (UINT_MAX >> 12)) { + v[i] = z % sz.size(); + z /= sz.size(); + } + else { + inf.push_back(i); + } + } + // fill in values for large domains + for (unsigned i = 0; i + 1 < inf.size(); ++i) { + inverse_cantor(z, v[inf[i]], z); + } + if (!inf.empty()) { + v[inf.back()] = z; + } +} + +public: + datatype_value_generator(value_generator& g, ast_manager& m): + m(m), g(g), dt(m), m_values(m) {} + + ~datatype_value_generator() { + for (auto& kv : m_values) dealloc(kv.m_value); + } + + family_id get_fid() const override { + return dt.get_family_id(); + } + + expr* get_value(sort* s, unsigned index) override { + expr_ref_vector* vp = nullptr; + if (!m_values.contains(s, vp)) { + vp = allocate(expr_ref_vector, m); + for (auto* c : *dt.get_datatype_constructors(s)) { + if (c->get_arity() == 0) + vp->push_back(m.mk_app(c)); + } + m_values.insert(s, vp); + } + auto& v = *vp; + expr_ref_vector args(m); + bool some_valid = true; + while (v.size() <= index && some_valid) { + some_valid = false; + for (auto* c : *dt.get_datatype_constructors(s)) { + unsigned arity = c->get_arity(); + if (arity == 0) + continue; + args.resize(c->get_arity()); + unsigned j = 0; + m_constr2seen.find(c, j); + m_constr2seen.insert(c, j+1); + if (beyond_domain_size(j, c)) + continue; + index2vector(j, c, indices); + bool valid = true; + // still does not ensure non-termination when + // 0 is used on a left-recursive datatype constructor + for (unsigned i = 0; valid && i < args.size(); ++i) { + args[i] = g.get_value(c->get_domain(i), indices[i]); + valid &= args.get(i) != nullptr; + } + if (valid) { + v.push_back(m.mk_app(c, args)); + some_valid = true; + } + } + } + return v.get(index, nullptr); + } +}; + + +class arith_value_generator : public value_generator_core { + ast_manager& m; + arith_util a; + int u2i(unsigned u) { + if (0 == (u % 2)) + return u/2; + else + return -((u+1)/2); + } +public: + arith_value_generator(ast_manager& m): m(m), a(m) {} + + family_id get_fid() const override { + return a.get_family_id(); + } + + expr* get_value(sort* s, unsigned index) override { + if (a.is_int(s)) { + return a.mk_int(u2i(index)); + } + if (index == 0) + return a.mk_real(rational(0)); + unsigned x, y; + // still imperfect as y could divide x + inverse_cantor(index/2, x, y); + x++; + y++; + if (index % 2 == 0) x = -x; + return a.mk_real(rational(x, y)); + } +}; + +class bv_value_generator : public value_generator_core { + ast_manager& m; + bv_util bv; +public: + bv_value_generator(ast_manager& m): m(m), bv(m) {} + + family_id get_fid() const override { + return bv.get_family_id(); + } + + expr* get_value(sort* s, unsigned index) override { + unsigned sz = 0; + bv.get_bv_size(s, sz); + if (sz < 30 && index >= (1 << sz)) + return nullptr; + return bv.mk_numeral(index, s); + } +}; + +class bool_value_generator : public value_generator_core { + ast_manager& m; +public: + bool_value_generator(ast_manager& m): m(m) {} + + family_id get_fid() const override { + return m.get_family_id(); + } + + expr* get_value(sort* s, unsigned index) override { + if (!m.is_bool(s)) + return nullptr; + if (index == 0) + return m.mk_false(); + if (index == 1) + return m.mk_true(); + return nullptr; + } +}; + + +value_generator::value_generator(ast_manager& m): m(m) { +} + +void value_generator::init() { + if (!m_plugins.empty()) + return; + add_plugin(alloc(datatype_value_generator, *this, m)); + add_plugin(alloc(arith_value_generator, m)); + add_plugin(alloc(bv_value_generator, m)); + add_plugin(alloc(bool_value_generator, m)); + // seq_value_generator + // fp_value_generator + // array_value_generator + // uninterp_sort_value_generator +} + +void value_generator::add_plugin(value_generator_core* v) { + m_plugins.reserve(v->get_fid() + 1); + m_plugins.set(v->get_fid(), v); +} + +expr* value_generator::get_value(sort* s, unsigned index) { + init(); + famiily_id fid = s->get_family_id(); + auto* p = m_plugins.get(fid, nullptr); + return p ? p->get_value(s, index) : nullptr; +} diff --git a/src/smt/value_generator.h b/src/smt/value_generator.h new file mode 100644 index 00000000000..01f3cfebdfb --- /dev/null +++ b/src/smt/value_generator.h @@ -0,0 +1,17 @@ +#pragma once + +namespace smt { + + class value_generator_core { + public: + virtual expr* get_value(sort* s, unsigned index) = 0; + }; + + class value_generator { + scoped_ptr_vector m_plugins; + public: + value_generator(ast_manager& m); + expr* get_value(sort* s, unsigned index); + + }; +}