euf model

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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')        

src/ast/euf/euf_egraph.h

@@ -130,6 +130,7 @@ namespace euf {
         void explain(ptr_vector<T>& justifications);
         template <typename T>
         void explain_eq(ptr_vector<T>& 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<void*(void*)>& copy_justification);
         std::ostream& display(std::ostream& out) const;        

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

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();
+    }
+}

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<void(unsigned sz, literal const* c, unsigned k)>& card,
                             std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {
         if (m_true)

src/sat/euf/euf_solver.h

@@ -61,8 +61,10 @@ namespace euf {
         unsigned_vector       m_bool_var_lim;
         scoped_ptr_vector<sat::extension> m_extensions;
         ptr_vector<sat::extension>        m_id2extension;
-        ptr_vector<sat::th_internalizer> m_id2internalize;
+        ptr_vector<sat::th_internalizer>  m_id2internalize;
         scoped_ptr_vector<sat::th_internalizer>        m_internalizers;
+        scoped_ptr_vector<sat::th_model_builder>       m_model_builders;
+        ptr_vector<sat::th_model_builder>              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);
+        
 
     };
 };

src/sat/smt/CMakeLists.txt

@@ -4,5 +4,6 @@ z3_add_component(sat_smt
   COMPONENT_DEPENDENCIES
     sat
     ast
+    euf
 )
 

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: