fix #4662

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

src/api/api_solver.cpp

@@ -727,6 +727,7 @@ extern "C" {
         to_solver_ref(s)->collect_statistics(st->m_stats);
         get_memory_statistics(st->m_stats);
         get_rlimit_statistics(mk_c(c)->m().limit(), st->m_stats);
+        to_solver_ref(s)->collect_timer_stats(st->m_stats);
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
         RETURN_Z3(r);

src/sat/ba/ba_internalize.h

@@ -18,7 +18,7 @@ Author:
 
 #pragma once
 
-#include "sat/smt/sat_smt.h"
+#include "sat/smt/sat_th.h"
 #include "sat/ba/ba_solver.h"
 #include "ast/pb_decl_plugin.h"
 

src/sat/euf/euf_model.cpp

@@ -23,10 +23,8 @@ namespace euf {
 
     model_converter* solver::get_model() {
         sat::th_dependencies deps;
-#if 0
         collect_dependencies(deps);
-        sort_dependencies(deps);
-#endif
+        // deps.sort();
         expr_ref_vector values(m);
         dependencies2values(deps, values);
         return nullptr;
@@ -36,9 +34,6 @@ namespace euf {
 
     }
 
-    void solver::sort_dependencies(sat::th_dependencies& deps) {
-
-    }
 
     void solver::dependencies2values(sat::th_dependencies& deps, expr_ref_vector& values) {
 

src/sat/euf/euf_solver.h

@@ -20,8 +20,8 @@ Author:
 #include "sat/sat_extension.h"
 #include "ast/euf/euf_egraph.h"
 #include "ast/ast_translation.h"
-#include "sat/smt/sat_smt.h"
 #include "sat/smt/atom2bool_var.h"
+#include "sat/smt/sat_th.h"
 #include "tactic/model_converter.h"
 
 namespace euf {

src/sat/smt/sat_smt.h

@@ -19,7 +19,6 @@ Author:
 
 #pragma once
 #include "ast/ast.h"
-#include "ast/euf/euf_egraph.h"
 #include "sat/sat_solver.h"
 
 namespace sat {
@@ -47,38 +46,6 @@ namespace sat {
         virtual void cache(app* t, literal l) = 0;
     };
     
-    class th_internalizer {
-    public:
-        virtual literal internalize(sat_internalizer& si, expr* e, bool sign, bool root) = 0;
-        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:
-
-        virtual ~th_model_builder() {}
-
-        /**
-           \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:

src/sat/smt/sat_th.cpp

@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sat_th.cpp
+
+Abstract:
+
+    Theory plugins
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+#include "sat/smt/sat_th.h"
+#include "util/top_sort.h"
+
+namespace sat {
+    
+    /*
+     * \brief add dependency: dst depends on src.
+     */
+    void th_dependencies::add(euf::enode* src, euf::enode* dst) {
+        
+    }
+    
+    /*
+     * \brief sort dependencies.
+     */
+    void th_dependencies::sort() {
+        top_sort<euf::enode> top;
+        
+    }
+
+}

src/sat/smt/sat_th.h

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sat_th.h
+
+Abstract:
+
+    Theory plugins
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_smt.h"
+#include "ast/euf/euf_egraph.h"
+
+namespace sat {
+    
+
+    class th_dependencies {
+    public:
+        th_dependencies() {}
+        euf::enode * const* begin() const { return nullptr; }
+        euf::enode * const* end() const { return nullptr; }
+
+        /*
+         * \brief add dependency: dst depends on src.
+         */
+        void add(euf::enode* src, euf::enode* dst);
+
+        /*
+         * \brief sort dependencies.
+         */
+        void sort();
+    };
+
+    class th_internalizer {
+    public:
+        virtual literal internalize(sat_internalizer& si, expr* e, bool sign, bool root) = 0;
+        virtual ~th_internalizer() {}
+    };
+
+    class th_model_builder {
+    public:
+
+        virtual ~th_model_builder() {}
+
+        /**
+           \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;
+    };
+
+
+}

src/solver/check_sat_result.h

@@ -22,6 +22,7 @@ Notes:
 #include "util/lbool.h"
 #include "util/statistics.h"
 #include "util/event_handler.h"
+#include "util/timer.h"
 #include "tactic/model_converter.h"
 
 /**
@@ -41,8 +42,9 @@ protected:
     unsigned    m_ref_count;
     lbool       m_status; 
     model_converter_ref m_mc0;
+    double      m_time;
 public:
-    check_sat_result():m_ref_count(0), m_status(l_undef) {}
+    check_sat_result():m_ref_count(0), m_status(l_undef), m_time(0) {}
     virtual ~check_sat_result() {}
     void inc_ref() { m_ref_count++; }
     void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
@@ -64,6 +66,19 @@ public:
     virtual void get_labels(svector<symbol> & r) = 0;
     virtual ast_manager& get_manager() const = 0;
 
+    class scoped_solver_time {
+        check_sat_result& c;
+        timer t;
+    public:
+        scoped_solver_time(check_sat_result& c):c(c) { c.m_time = 0; }
+        ~scoped_solver_time() { c.m_time = t.get_seconds(); }
+    };
+
+    void collect_timer_stats(statistics& st) const {
+        if (m_time != 0) 
+            st.update("time", m_time);
+    }
+
 };
 
 /**
@@ -76,7 +91,6 @@ struct simple_check_sat_result : public check_sat_result {
     proof_ref       m_proof;
     std::string     m_unknown;
     
-
     simple_check_sat_result(ast_manager & m);
     ~simple_check_sat_result() override;
     ast_manager& get_manager() const override { return m_proof.get_manager(); }

src/solver/solver.cpp

@@ -85,6 +85,7 @@ struct scoped_assumption_push {
 };
 
 lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+    scoped_solver_time st(*this);
     try {
         return get_consequences_core(asms, vars, consequences);
     }
@@ -326,6 +327,7 @@ expr_ref_vector solver::get_non_units() {
 
 lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
     lbool r = l_undef;
+    scoped_solver_time _st(*this);
     try {
         r = check_sat_core(num_assumptions, assumptions);
     }