From 872fd5e9ffb5c464218ed2a026608e535d6cbff9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Aug 2020 15:05:35 -0700 Subject: [PATCH] fix #4662 Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 1 + src/sat/ba/ba_internalize.h | 2 +- src/sat/euf/euf_model.cpp | 7 +--- src/sat/euf/euf_solver.h | 2 +- src/sat/smt/sat_smt.h | 33 ------------------ src/sat/smt/sat_th.cpp | 37 ++++++++++++++++++++ src/sat/smt/sat_th.h | 66 +++++++++++++++++++++++++++++++++++ src/solver/check_sat_result.h | 18 ++++++++-- src/solver/solver.cpp | 2 ++ 9 files changed, 125 insertions(+), 43 deletions(-) create mode 100644 src/sat/smt/sat_th.cpp create mode 100644 src/sat/smt/sat_th.h diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index cb7473d82..9c9c3d642 100644 --- a/src/api/api_solver.cpp +++ b/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); diff --git a/src/sat/ba/ba_internalize.h b/src/sat/ba/ba_internalize.h index 6591e5968..71ab20614 100644 --- a/src/sat/ba/ba_internalize.h +++ b/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" diff --git a/src/sat/euf/euf_model.cpp b/src/sat/euf/euf_model.cpp index 9223844a7..9c789140e 100644 --- a/src/sat/euf/euf_model.cpp +++ b/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) { diff --git a/src/sat/euf/euf_solver.h b/src/sat/euf/euf_solver.h index b2a56bb86..f2aa26059 100644 --- a/src/sat/euf/euf_solver.h +++ b/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 { diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index ed085c07b..013515d94 100644 --- a/src/sat/smt/sat_smt.h +++ b/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: diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp new file mode 100644 index 000000000..22c59fd2e --- /dev/null +++ b/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 top; + + } + +} diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h new file mode 100644 index 000000000..9c0f92dd7 --- /dev/null +++ b/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; + }; + + +} diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 1a52e2d3c..53ffd2a1d 100644 --- a/src/solver/check_sat_result.h +++ b/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 & 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(); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 0c69da779..32cb0b940 100644 --- a/src/solver/solver.cpp +++ b/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); }