From 4ab35a9bb5a29fc6a904cdebd09f3678f654b8a1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Aug 2020 15:55:12 -0700 Subject: [PATCH] euf model Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- src/ast/euf/euf_egraph.h | 1 + src/sat/euf/CMakeLists.txt | 1 + src/sat/euf/euf_model.cpp | 77 ++++++++++++++++++++++++++++++++++++++ src/sat/euf/euf_solver.cpp | 11 +++--- src/sat/euf/euf_solver.h | 14 +++++-- src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/sat_smt.h | 26 ++++++++++++- 8 files changed, 123 insertions(+), 10 deletions(-) create mode 100644 src/sat/euf/euf_model.cpp diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 979566614..07fa172f6 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -38,7 +38,7 @@ def init_project_def(): add_lib('proofs', ['rewriter', 'util'], 'ast/proofs') add_lib('solver', ['model', 'tactic', 'proofs']) add_lib('cmd_context', ['solver', 'rewriter']) - add_lib('sat_smt', ['sat', 'tactic'], 'sat/smt') + add_lib('sat_smt', ['sat', 'euf', 'tactic'], 'sat/smt') add_lib('sat_ba', ['sat', 'sat_smt'], 'sat/ba') add_lib('sat_euf', ['sat', 'euf', 'sat_ba'], 'sat/euf') add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_euf'], 'sat/tactic') diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index e52f44da5..4988ebb32 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -130,6 +130,7 @@ namespace euf { void explain(ptr_vector& justifications); template void explain_eq(ptr_vector& justifications, enode* a, enode* b, bool comm); + enode_vector const& nodes() const { return m_nodes; } void invariant(); void copy_from(egraph const& src, std::function& copy_justification); std::ostream& display(std::ostream& out) const; diff --git a/src/sat/euf/CMakeLists.txt b/src/sat/euf/CMakeLists.txt index 4ee444de4..b716ea015 100644 --- a/src/sat/euf/CMakeLists.txt +++ b/src/sat/euf/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(sat_euf SOURCES euf_solver.cpp + euf_model.cpp COMPONENT_DEPENDENCIES sat sat_smt diff --git a/src/sat/euf/euf_model.cpp b/src/sat/euf/euf_model.cpp new file mode 100644 index 000000000..9223844a7 --- /dev/null +++ b/src/sat/euf/euf_model.cpp @@ -0,0 +1,77 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + euf_model.cpp + +Abstract: + + Model building for EUF solver plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-25 + +--*/ + +#include "ast/ast_pp.h" +#include "sat/euf/euf_solver.h" +#include "model/value_factory.h" + +namespace euf { + + model_converter* solver::get_model() { + sat::th_dependencies deps; +#if 0 + collect_dependencies(deps); + sort_dependencies(deps); +#endif + expr_ref_vector values(m); + dependencies2values(deps, values); + return nullptr; + } + + void solver::collect_dependencies(sat::th_dependencies& deps) { + + } + + void solver::sort_dependencies(sat::th_dependencies& deps) { + + } + + void solver::dependencies2values(sat::th_dependencies& deps, expr_ref_vector& values) { + + user_sort_factory user_sort(m); + for (enode* n : deps) { + unsigned id = n->get_root()->get_owner_id(); + if (values.get(id) != nullptr) + continue; + expr* e = n->get_owner(); + values.reserve(id + 1); + if (m.is_bool(e)) { + switch (s().value(m_expr2var.to_bool_var(e))) { + case l_true: + values.set(id, m.mk_true()); + break; + default: + values.set(id, m.mk_false()); + break; + } + continue; + } + auto* mb = get_model_builder(e); + if (mb) + mb->add_value(n, values); + else if (m.is_uninterp(m.get_sort(e))) { + expr* v = user_sort.get_fresh_value(m.get_sort(e)); + values.set(id, v); + } + else { + IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n"); + } + + } + NOT_IMPLEMENTED_YET(); + } +} diff --git a/src/sat/euf/euf_solver.cpp b/src/sat/euf/euf_solver.cpp index 7a7e4e73f..ed5129a52 100644 --- a/src/sat/euf/euf_solver.cpp +++ b/src/sat/euf/euf_solver.cpp @@ -334,6 +334,12 @@ namespace euf { } return nullptr; } + + sat::th_model_builder* solver::get_model_builder(expr* e) { + if (is_app(e)) + return m_id2model_builder.get(to_app(e)->get_family_id(), nullptr); + return nullptr; + } sat::literal solver::internalize(sat::sat_internalizer& si, expr* e, bool sign, bool root) { auto* ext = get_internalizer(e); @@ -414,11 +420,6 @@ namespace euf { m_bool_var_trail.push_back(v); } - model_converter* solver::get_model() { - NOT_IMPLEMENTED_YET(); - return nullptr; - } - bool solver::extract_pb(std::function& card, std::function& pb) { if (m_true) diff --git a/src/sat/euf/euf_solver.h b/src/sat/euf/euf_solver.h index 90ccdf23e..b2a56bb86 100644 --- a/src/sat/euf/euf_solver.h +++ b/src/sat/euf/euf_solver.h @@ -61,8 +61,10 @@ namespace euf { unsigned_vector m_bool_var_lim; scoped_ptr_vector m_extensions; ptr_vector m_id2extension; - ptr_vector m_id2internalize; + ptr_vector m_id2internalize; scoped_ptr_vector m_internalizers; + scoped_ptr_vector m_model_builders; + ptr_vector m_id2model_builder; euf_base m_conflict_idx, m_eq_idx, m_lit_idx; sat::solver& s() { return *m_solver; } @@ -72,12 +74,19 @@ namespace euf { void attach_bool_var(sat::bool_var v, bool sign, euf::enode* n); solver* copy_core(); sat::extension* get_extension(sat::bool_var v); + sat::extension* get_extension(expr* e); void add_extension(family_id fid, sat::extension* e); sat::th_internalizer* get_internalizer(expr* e); + sat::th_model_builder* get_model_builder(expr* e); + void propagate(); void get_antecedents(literal l, euf_base& j, literal_vector& r); + void dependencies2values(sat::th_dependencies& deps, expr_ref_vector& values); + void collect_dependencies(sat::th_dependencies& deps); + void sort_dependencies(sat::th_dependencies& deps); + public: solver(ast_manager& m, atom2bool_var& expr2var): m(m), @@ -138,8 +147,7 @@ namespace euf { sat::literal internalize(sat::sat_internalizer& si, expr* e, bool sign, bool root) override; model_converter* get_model(); - - sat::extension* get_extension(expr* e); + }; }; diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 495917065..b6c0a3ae5 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -4,5 +4,6 @@ z3_add_component(sat_smt COMPONENT_DEPENDENCIES sat ast + euf ) diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index fe0f7e11d..0937c34bb 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -18,8 +18,9 @@ Author: #pragma once -#include "sat/sat_solver.h" #include "ast/ast.h" +#include "ast/euf/euf_egraph.h" +#include "sat/sat_solver.h" namespace sat { @@ -52,6 +53,29 @@ namespace sat { virtual ~th_internalizer() {} }; + class th_dependencies { + public: + th_dependencies() {} + euf::enode * const* begin() const { return nullptr; } + euf::enode * const* end() const { return nullptr; } + }; + + + class th_model_builder { + public: + /** + \brief compute the value for enode \c n and store the value in \c values + for the root of the class of \c n. + */ + virtual void add_value(euf::enode* n, expr_ref_vector& values) = 0; + + /** + \brief compute dependencies for node n + */ + virtual void add_dep(euf::enode* n, th_dependencies& dep) = 0; + }; + + class index_base { extension* ex; public: