From ca498e20d17457b4baa32578a94923cf8e3e105c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Oct 2019 19:48:28 -0700 Subject: [PATCH] move value factories to model Signed-off-by: Nikolaj Bjorner --- src/model/CMakeLists.txt | 5 + .../proto_model => model}/array_factory.cpp | 18 +-- .../proto_model => model}/array_factory.h | 4 +- .../datatype_factory.cpp | 6 +- .../proto_model => model}/datatype_factory.h | 4 +- src/model/model.cpp | 13 +- src/model/model.h | 3 + src/model/model_core.h | 2 + .../proto_model => model}/numeral_factory.cpp | 2 +- .../proto_model => model}/numeral_factory.h | 2 +- .../proto_model => model}/struct_factory.cpp | 6 +- .../proto_model => model}/struct_factory.h | 8 +- .../proto_model => model}/value_factory.cpp | 2 +- .../proto_model => model}/value_factory.h | 0 src/sat/tactic/goal2sat.cpp | 14 +-- src/smt/proto_model/CMakeLists.txt | 5 - src/smt/proto_model/proto_model.cpp | 36 +++--- src/smt/proto_model/proto_model.h | 6 +- src/smt/theory_arith.h | 10 +- src/smt/theory_array_base.h | 2 +- src/smt/theory_bv.h | 6 +- src/smt/theory_datatype.h | 2 +- src/smt/theory_diff_logic.h | 6 +- src/smt/theory_diff_logic_def.h | 6 +- src/smt/theory_dl.cpp | 8 +- src/smt/theory_fpa.h | 2 +- src/smt/theory_lra.cpp | 12 +- src/smt/theory_seq.cpp | 2 +- src/smt/theory_str.h | 2 +- src/tactic/fd_solver/smtfd_solver.cpp | 118 +++++++++++------- 30 files changed, 167 insertions(+), 145 deletions(-) rename src/{smt/proto_model => model}/array_factory.cpp (93%) rename src/{smt/proto_model => model}/array_factory.h (88%) rename src/{smt/proto_model => model}/datatype_factory.cpp (98%) rename src/{smt/proto_model => model}/datatype_factory.h (87%) rename src/{smt/proto_model => model}/numeral_factory.cpp (95%) rename src/{smt/proto_model => model}/numeral_factory.h (96%) rename src/{smt/proto_model => model}/struct_factory.cpp (89%) rename src/{smt/proto_model => model}/struct_factory.h (84%) rename src/{smt/proto_model => model}/value_factory.cpp (98%) rename src/{smt/proto_model => model}/value_factory.h (100%) diff --git a/src/model/CMakeLists.txt b/src/model/CMakeLists.txt index 0e685e07cf5..b46a22e4e82 100644 --- a/src/model/CMakeLists.txt +++ b/src/model/CMakeLists.txt @@ -1,5 +1,7 @@ z3_add_component(model SOURCES + array_factory.cpp + datatype_factory.cpp func_interp.cpp model2expr.cpp model_core.cpp @@ -9,6 +11,9 @@ z3_add_component(model model_pp.cpp model_smt2_pp.cpp model_v2_pp.cpp + numeral_factory.cpp + struct_factory.cpp + value_factory.cpp COMPONENT_DEPENDENCIES rewriter PYG_FILES diff --git a/src/smt/proto_model/array_factory.cpp b/src/model/array_factory.cpp similarity index 93% rename from src/smt/proto_model/array_factory.cpp rename to src/model/array_factory.cpp index 14102100690..4a5d100623e 100644 --- a/src/smt/proto_model/array_factory.cpp +++ b/src/model/array_factory.cpp @@ -20,8 +20,8 @@ Revision History: #include "ast/array_decl_plugin.h" #include "ast/ast_pp.h" #include "model/func_interp.h" -#include "smt/proto_model/array_factory.h" -#include "smt/proto_model/proto_model.h" +#include "model/model_core.h" +#include "model/array_factory.h" func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) { ptr_buffer domain; @@ -33,7 +33,7 @@ func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) { return m.mk_fresh_func_decl(symbol::null, symbol::null, arity, domain.c_ptr(), range); } -array_factory::array_factory(ast_manager & m, proto_model & md): +array_factory::array_factory(ast_manager & m, model_core & md): struct_factory(m, m.mk_family_id("array"), md) { } @@ -67,13 +67,7 @@ expr * array_factory::get_some_value(sort * s) { return *(set->begin()); func_interp * fi; expr * val = mk_array_interp(s, fi); -#if 0 - ptr_buffer args; - get_some_args_for(s, args); - fi->insert_entry(args.c_ptr(), m_model.get_some_value(get_array_range(s))); -#else fi->set_else(m_model.get_some_value(get_array_range(s))); -#endif return val; } @@ -147,13 +141,7 @@ expr * array_factory::get_fresh_value(sort * s) { // easy case func_interp * fi; expr * val = mk_array_interp(s, fi); -#if 0 - ptr_buffer args; - get_some_args_for(s, args); - fi->insert_entry(args.c_ptr(), range_val); -#else fi->set_else(range_val); -#endif return val; } else { diff --git a/src/smt/proto_model/array_factory.h b/src/model/array_factory.h similarity index 88% rename from src/smt/proto_model/array_factory.h rename to src/model/array_factory.h index b59df3f9413..2f9bccb690d 100644 --- a/src/smt/proto_model/array_factory.h +++ b/src/model/array_factory.h @@ -19,7 +19,7 @@ Revision History: #ifndef ARRAY_FACTORY_H_ #define ARRAY_FACTORY_H_ -#include "smt/proto_model/struct_factory.h" +#include "model/struct_factory.h" class func_interp; @@ -30,7 +30,7 @@ class array_factory : public struct_factory { void get_some_args_for(sort * s, ptr_buffer & args); bool mk_two_diff_values_for(sort * s); public: - array_factory(ast_manager & m, proto_model & md); + array_factory(ast_manager & m, model_core & md); ~array_factory() override {} diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/model/datatype_factory.cpp similarity index 98% rename from src/smt/proto_model/datatype_factory.cpp rename to src/model/datatype_factory.cpp index eded55cc356..b181581ec09 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -16,12 +16,12 @@ Module Name: Revision History: --*/ -#include "smt/proto_model/datatype_factory.h" -#include "smt/proto_model/proto_model.h" +#include "model/datatype_factory.h" +#include "model/model_core.h" #include "ast/ast_pp.h" #include "ast/expr_functors.h" -datatype_factory::datatype_factory(ast_manager & m, proto_model & md): +datatype_factory::datatype_factory(ast_manager & m, model_core & md): struct_factory(m, m.mk_family_id("datatype"), md), m_util(m) { } diff --git a/src/smt/proto_model/datatype_factory.h b/src/model/datatype_factory.h similarity index 87% rename from src/smt/proto_model/datatype_factory.h rename to src/model/datatype_factory.h index 85b264382f5..b8463a7061b 100644 --- a/src/smt/proto_model/datatype_factory.h +++ b/src/model/datatype_factory.h @@ -19,7 +19,7 @@ Revision History: #ifndef DATATYPE_FACTORY_H_ #define DATATYPE_FACTORY_H_ -#include "smt/proto_model/struct_factory.h" +#include "model/struct_factory.h" #include "ast/datatype_decl_plugin.h" class datatype_factory : public struct_factory { @@ -32,7 +32,7 @@ class datatype_factory : public struct_factory { bool is_subterm_of_last_value(app* e); public: - datatype_factory(ast_manager & m, proto_model & md); + datatype_factory(ast_manager & m, model_core & md); ~datatype_factory() override {} expr * get_some_value(sort * s) override; expr * get_fresh_value(sort * s) override; diff --git a/src/model/model.cpp b/src/model/model.cpp index 44338fbfa26..c05d9a1f3c5 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -98,7 +98,7 @@ struct model::value_proc : public some_value_proc { return u->get(0); } return nullptr; - } + } }; expr * model::get_some_value(sort * s) { @@ -106,6 +106,17 @@ expr * model::get_some_value(sort * s) { return m.get_some_value(s, &p); } +expr * model::get_fresh_value(sort * s) { + value_proc p(*this); + return m.get_some_value(s, &p); +} + +bool model::get_some_values(sort * s, expr_ref& v1, expr_ref& v2) { + v1 = get_some_value(s); + v2 = get_some_value(s); + return true; +} + ptr_vector const & model::get_universe(sort * s) const { ptr_vector * u = nullptr; m_usort2universe.find(s, u); diff --git a/src/model/model.h b/src/model/model.h index 81ec277656d..13c4f14b3b7 100644 --- a/src/model/model.h +++ b/src/model/model.h @@ -66,6 +66,9 @@ class model : public model_core { bool eval_expr(expr * e, expr_ref & result, bool model_completion = false); expr * get_some_value(sort * s) override; + expr * get_fresh_value(sort * s) override; + bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override; + ptr_vector const & get_universe(sort * s) const override; unsigned get_num_uninterpreted_sorts() const override; sort * get_uninterpreted_sort(unsigned idx) const override; diff --git a/src/model/model_core.h b/src/model/model_core.h index 7f505138658..4d2c8efda33 100644 --- a/src/model/model_core.h +++ b/src/model/model_core.h @@ -71,6 +71,8 @@ class model_core { void unregister_decl(func_decl * d); virtual expr * get_some_value(sort * s) = 0; + virtual expr * get_fresh_value(sort * s) = 0; + virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0; expr * get_some_const_interp(func_decl * d) { expr * r = get_const_interp(d); diff --git a/src/smt/proto_model/numeral_factory.cpp b/src/model/numeral_factory.cpp similarity index 95% rename from src/smt/proto_model/numeral_factory.cpp rename to src/model/numeral_factory.cpp index a5d5ac18a86..ba19ec94176 100644 --- a/src/smt/proto_model/numeral_factory.cpp +++ b/src/model/numeral_factory.cpp @@ -16,8 +16,8 @@ Module Name: Revision History: --*/ -#include "smt/proto_model/numeral_factory.h" #include "ast/ast_pp.h" +#include "model/numeral_factory.h" app * arith_factory::mk_value_core(rational const & val, sort * s) { return m_util.mk_numeral(val, s); diff --git a/src/smt/proto_model/numeral_factory.h b/src/model/numeral_factory.h similarity index 96% rename from src/smt/proto_model/numeral_factory.h rename to src/model/numeral_factory.h index 198ff0d32b5..6e30af65f25 100644 --- a/src/smt/proto_model/numeral_factory.h +++ b/src/model/numeral_factory.h @@ -19,9 +19,9 @@ Revision History: #ifndef NUMERAL_FACTORY_H_ #define NUMERAL_FACTORY_H_ -#include "smt/proto_model/value_factory.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" +#include "model/value_factory.h" class numeral_factory : public simple_factory { public: diff --git a/src/smt/proto_model/struct_factory.cpp b/src/model/struct_factory.cpp similarity index 89% rename from src/smt/proto_model/struct_factory.cpp rename to src/model/struct_factory.cpp index a31dd84dd10..3e63e99deb2 100644 --- a/src/smt/proto_model/struct_factory.cpp +++ b/src/model/struct_factory.cpp @@ -16,8 +16,8 @@ Module Name: Revision History: --*/ -#include "smt/proto_model/struct_factory.h" -#include "smt/proto_model/proto_model.h" +#include "model/struct_factory.h" +#include "model/model_core.h" struct_factory::value_set * struct_factory::get_value_set(sort * s) { value_set * set = nullptr; @@ -31,7 +31,7 @@ struct_factory::value_set * struct_factory::get_value_set(sort * s) { return set; } -struct_factory::struct_factory(ast_manager & m, family_id fid, proto_model & md): +struct_factory::struct_factory(ast_manager & m, family_id fid, model_core & md): value_factory(m, fid), m_model(md), m_values(m), diff --git a/src/smt/proto_model/struct_factory.h b/src/model/struct_factory.h similarity index 84% rename from src/smt/proto_model/struct_factory.h rename to src/model/struct_factory.h index 9fe54392cfa..5776108f8f5 100644 --- a/src/smt/proto_model/struct_factory.h +++ b/src/model/struct_factory.h @@ -19,10 +19,10 @@ Revision History: #ifndef STRUCT_FACTORY_H_ #define STRUCT_FACTORY_H_ -#include "smt/proto_model/value_factory.h" +#include "model/value_factory.h" #include "util/obj_hashtable.h" -class proto_model; +class model_core; /** \brief Abstract factory for structured values such as: arrays and algebraic datatypes. @@ -32,7 +32,7 @@ class struct_factory : public value_factory { typedef obj_hashtable value_set; typedef obj_map sort2value_set; - proto_model & m_model; + model_core & m_model; sort2value_set m_sort2value_set; expr_ref_vector m_values; sort_ref_vector m_sorts; @@ -41,7 +41,7 @@ class struct_factory : public value_factory { value_set * get_value_set(sort * s); public: - struct_factory(ast_manager & m, family_id fid, proto_model & md); + struct_factory(ast_manager & m, family_id fid, model_core & md); ~struct_factory() override; diff --git a/src/smt/proto_model/value_factory.cpp b/src/model/value_factory.cpp similarity index 98% rename from src/smt/proto_model/value_factory.cpp rename to src/model/value_factory.cpp index 5a0d012dc7e..45a6b2429ad 100644 --- a/src/smt/proto_model/value_factory.cpp +++ b/src/model/value_factory.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#include "smt/proto_model/value_factory.h" +#include "model/value_factory.h" value_factory::value_factory(ast_manager & m, family_id fid): m_manager(m), diff --git a/src/smt/proto_model/value_factory.h b/src/model/value_factory.h similarity index 100% rename from src/smt/proto_model/value_factory.h rename to src/model/value_factory.h diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 541fbc47b8d..a3e6b857c0e 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -29,6 +29,7 @@ Module Name: #include "util/ref_util.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" #include "ast/pb_decl_plugin.h" #include "ast/ast_util.h" #include "ast/for_each_expr.h" @@ -142,7 +143,7 @@ struct goal2sat::imp { sat::bool_var v = m_solver.add_var(ext); m_map.insert(t, v); l = sat::literal(v, sign); - TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";); + TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << "\n";); if (ext && !is_uninterp_const(t)) { m_interpreted_atoms.push_back(t); } @@ -228,7 +229,7 @@ struct goal2sat::imp { } void convert_or(app * t, bool root, bool sign) { - TRACE("goal2sat", tout << "convert_or:\n" << mk_ismt2_pp(t, m) << "\n";); + TRACE("goal2sat", tout << "convert_or:\n" << mk_bounded_pp(t, m, 2) << "\n";); unsigned num = t->get_num_args(); if (root) { SASSERT(num == m_result_stack.size()); @@ -348,7 +349,7 @@ struct goal2sat::imp { } void convert_iff2(app * t, bool root, bool sign) { - TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_ismt2_pp(t, m) << "\n";); + TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";); unsigned sz = m_result_stack.size(); SASSERT(sz >= 2); sat::literal l1 = m_result_stack[sz-1]; @@ -381,7 +382,7 @@ struct goal2sat::imp { } void convert_iff(app * t, bool root, bool sign) { - TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_ismt2_pp(t, m) << "\n";); + TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";); unsigned sz = m_result_stack.size(); unsigned num = get_num_args(t); SASSERT(sz >= num && num >= 2); @@ -512,7 +513,6 @@ struct goal2sat::imp { } void convert_pb_eq(app* t, bool root, bool sign) { - //IF_VERBOSE(0, verbose_stream() << "pbeq: " << mk_pp(t, m) << "\n";); rational k = pb.get_k(t); SASSERT(k.is_unsigned()); svector wlits; @@ -741,7 +741,7 @@ struct goal2sat::imp { void process(expr * n) { //SASSERT(m_result_stack.empty()); - TRACE("goal2sat", tout << "converting: " << mk_ismt2_pp(n, m) << "\n";); + TRACE("goal2sat", tout << "converting: " << mk_bounded_pp(n, m, 2) << "\n";); if (visit(n, true, false)) { SASSERT(m_result_stack.empty()); return; @@ -839,7 +839,7 @@ struct goal2sat::imp { } f = m.mk_or(fmls.size(), fmls.c_ptr()); } - TRACE("goal2sat", tout << f << "\n";); + TRACE("goal2sat", tout << mk_bounded_pp(f, m, 2) << "\n";); process(f); skip_dep: ; diff --git a/src/smt/proto_model/CMakeLists.txt b/src/smt/proto_model/CMakeLists.txt index c5f6c4b1875..4ade7e5380c 100644 --- a/src/smt/proto_model/CMakeLists.txt +++ b/src/smt/proto_model/CMakeLists.txt @@ -1,11 +1,6 @@ z3_add_component(proto_model SOURCES - array_factory.cpp - datatype_factory.cpp - numeral_factory.cpp proto_model.cpp - struct_factory.cpp - value_factory.cpp COMPONENT_DEPENDENCIES model rewriter diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 654925f7220..65acaeec878 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -192,9 +192,8 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au void proto_model::remove_aux_decls_not_in_set(ptr_vector & decls, func_decl_set const & s) { unsigned sz = decls.size(); - unsigned i = 0; unsigned j = 0; - for (; i < sz; i++) { + for (unsigned i = 0; i < sz; i++) { func_decl * f = decls[i]; if (!m_aux_decls.contains(f) || s.contains(f)) { decls[j] = f; @@ -280,11 +279,10 @@ expr * proto_model::get_some_value(sort * s) { if (m.is_uninterp(s)) { return m_user_sort_factory->get_some_value(s); } + else if (value_factory * f = get_factory(s->get_family_id())) { + return f->get_some_value(s); + } else { - family_id fid = s->get_family_id(); - value_factory * f = get_factory(fid); - if (f) - return f->get_some_value(s); // there is no factory for the family id, then assume s is uninterpreted. return m_user_sort_factory->get_some_value(s); } @@ -294,13 +292,11 @@ bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { if (m.is_uninterp(s)) { return m_user_sort_factory->get_some_values(s, v1, v2); } + else if (value_factory * f = get_factory(s->get_family_id())) { + return f->get_some_values(s, v1, v2); + } else { - family_id fid = s->get_family_id(); - value_factory * f = get_factory(fid); - if (f) - return f->get_some_values(s, v1, v2); - else - return false; + return false; } } @@ -308,15 +304,13 @@ expr * proto_model::get_fresh_value(sort * s) { if (m.is_uninterp(s)) { return m_user_sort_factory->get_fresh_value(s); } + else if (value_factory * f = get_factory(s->get_family_id())) { + return f->get_fresh_value(s); + } else { - family_id fid = s->get_family_id(); - value_factory * f = get_factory(fid); - if (f) - return f->get_fresh_value(s); - else - // Use user_sort_factory if the theory has no support for model construnction. - // This is needed when dummy theories are used for arithmetic or arrays. - return m_user_sort_factory->get_fresh_value(s); + // Use user_sort_factory if the theory has no support for model construnction. + // This is needed when dummy theories are used for arithmetic or arrays. + return m_user_sort_factory->get_fresh_value(s); } } @@ -336,7 +330,7 @@ void proto_model::register_value(expr * n) { void proto_model::compress() { for (func_decl* f : m_func_decls) { func_interp * fi = get_func_interp(f); - SASSERT(fi != 0); + SASSERT(fi != nullptr); fi->compress(); } } diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index b9ed65fb138..c736657156c 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -30,7 +30,7 @@ Revision History: #include "model/model_core.h" #include "model/model_evaluator.h" -#include "smt/proto_model/value_factory.h" +#include "model/value_factory.h" #include "util/plugin_manager.h" #include "ast/arith_decl_plugin.h" #include "ast/func_decl_dependencies.h" @@ -71,10 +71,10 @@ class proto_model : public model_core { value_factory * get_factory(family_id fid); expr * get_some_value(sort * s) override; + expr * get_fresh_value(sort * s) override; - bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2); + bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override; - expr * get_fresh_value(sort * s); void register_value(expr * n); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index da44c45d6b3..15571aba093 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -20,24 +20,24 @@ Revision History: #ifndef THEORY_ARITH_H_ #define THEORY_ARITH_H_ -#include "smt/smt_theory.h" #include "util/map.h" #include "util/heap.h" #include "util/nat_set.h" #include "util/inf_rational.h" #include "util/s_integer.h" #include "util/inf_s_integer.h" +#include "util/obj_pair_hashtable.h" +#include "util/uint_set.h" #include "ast/arith_decl_plugin.h" +#include "model/numeral_factory.h" +#include "smt/smt_theory.h" #include "smt/params/theory_arith_params.h" #include "smt/arith_eq_adapter.h" -#include "smt/proto_model/numeral_factory.h" #include "smt/smt_context.h" -#include "util/obj_pair_hashtable.h" #include "smt/old_interval.h" -#include "math/grobner/grobner.h" #include "smt/arith_eq_solver.h" #include "smt/theory_opt.h" -#include "util/uint_set.h" +#include "math/grobner/grobner.h" namespace smt { diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index d6b02c9a79a..0bc61edc858 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -22,7 +22,7 @@ Revision History: #include "smt/smt_theory.h" #include "smt/theory_array_bapa.h" #include "ast/array_decl_plugin.h" -#include "smt/proto_model/array_factory.h" +#include "model/array_factory.h" namespace smt { diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 5a4edf4cf1c..edacd1aa25d 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -19,13 +19,13 @@ Revision History: #ifndef THEORY_BV_H_ #define THEORY_BV_H_ -#include "smt/smt_theory.h" -#include "smt/params/theory_bv_params.h" #include "ast/rewriter/bit_blaster/bit_blaster.h" #include "util/trail.h" #include "util/union_find.h" #include "ast/arith_decl_plugin.h" -#include "smt/proto_model/numeral_factory.h" +#include "model/numeral_factory.h" +#include "smt/smt_theory.h" +#include "smt/params/theory_bv_params.h" namespace smt { diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index e5b9b9909e3..e87a2c0e911 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -22,9 +22,9 @@ Revision History: #include "util/union_find.h" #include "ast/array_decl_plugin.h" #include "ast/datatype_decl_plugin.h" +#include "model/datatype_factory.h" #include "smt/smt_theory.h" #include "smt/params/theory_datatype_params.h" -#include "smt/proto_model/datatype_factory.h" namespace smt { class theory_datatype : public theory { diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 5bb6e121bf3..3b5e2cb3fc5 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -27,15 +27,15 @@ Revision History: #include "util/inf_int_rational.h" #include "util/s_integer.h" #include "util/inf_s_integer.h" +#include "util/map.h" +#include "ast/arith_decl_plugin.h" +#include "model/numeral_factory.h" #include "smt/smt_theory.h" #include "smt/diff_logic.h" -#include "ast/arith_decl_plugin.h" #include "smt/smt_justification.h" -#include "util/map.h" #include "smt/params/smt_params.h" #include "smt/arith_eq_adapter.h" #include "smt/smt_model_generator.h" -#include "smt/proto_model/numeral_factory.h" #include "smt/smt_clause.h" #include "smt/theory_opt.h" #include "math/simplex/simplex.h" diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index dbeaaffa0e8..bf50e2428b1 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -22,11 +22,11 @@ Revision History: #ifndef THEORY_DIFF_LOGIC_DEF_H_ #define THEORY_DIFF_LOGIC_DEF_H_ -#include "smt/theory_diff_logic.h" -#include "smt/smt_context.h" #include "util/map.h" -#include "ast/ast_pp.h" #include "util/warning.h" +#include "ast/ast_pp.h" +#include "smt/theory_diff_logic.h" +#include "smt/smt_context.h" #include "smt/smt_model_generator.h" #include "model/model_implicant.h" diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 4b07f208131..37217ae01e3 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -22,14 +22,14 @@ Revision History: --*/ -#include "smt/smt_theory.h" #include "ast/dl_decl_plugin.h" -#include "smt/proto_model/value_factory.h" -#include "smt/smt_model_generator.h" #include "ast/bv_decl_plugin.h" +#include "ast/ast_pp.h" +#include "model/value_factory.h" +#include "smt/smt_theory.h" +#include "smt/smt_model_generator.h" #include "smt/theory_bv.h" #include "smt/smt_context.h" -#include "ast/ast_pp.h" // Basic approach: reduce theory to bit-vectors: // diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index e6ab3797e90..dd9fcfc6530 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -24,7 +24,7 @@ Revision History: #include "ast/fpa/fpa2bv_converter.h" #include "ast/fpa/fpa2bv_rewriter.h" #include "ast/rewriter/th_rewriter.h" -#include "smt/proto_model/value_factory.h" +#include "model/value_factory.h" #include "smt/smt_model_generator.h" namespace smt { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 8e79ca62483..3e9fc283b3d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -28,20 +28,20 @@ #include "util/optional.h" #include "util/lp/lp_params.hpp" #include "util/inf_rational.h" +#include "util/cancel_eh.h" +#include "util/scoped_timer.h" +#include "util/nat_set.h" +#include "util/lp/nra_solver.h" +#include "ast/ast_pp.h" +#include "model/numeral_factory.h" #include "smt/smt_theory.h" #include "smt/smt_context.h" #include "smt/theory_lra.h" -#include "smt/proto_model/numeral_factory.h" #include "smt/smt_model_generator.h" #include "smt/arith_eq_adapter.h" -#include "util/nat_set.h" -#include "util/lp/nra_solver.h" #include "tactic/generic_model_converter.h" #include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/polynomial.h" -#include "ast/ast_pp.h" -#include "util/cancel_eh.h" -#include "util/scoped_timer.h" namespace lp_api { enum bound_kind { lower_t, upper_t }; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 272646f2592..2dfdb16c122 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -92,7 +92,7 @@ Module Name: #include "ast/ast_ll_pp.h" #include "ast/ast_trail.h" #include "ast/for_each_expr.h" -#include "smt/proto_model/value_factory.h" +#include "model/value_factory.h" #include "smt/smt_context.h" #include "smt/smt_model_generator.h" #include "smt/theory_seq.h" diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 9c77134ac00..1d6e712043d 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -26,9 +26,9 @@ #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/seq_decl_plugin.h" +#include "model/value_factory.h" #include "smt/smt_theory.h" #include "smt/params/theory_str_params.h" -#include "smt/proto_model/value_factory.h" #include "smt/smt_model_generator.h" #include "smt/smt_arith_value.h" #include diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index a1aa509c709..c1c9a145277 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -200,6 +200,10 @@ namespace smtfd { } return !is_app(r) || to_app(r)->get_family_id() != m.get_basic_family_id(); } + + bool is_uninterp_atom(expr* a) { + return is_app(a) && to_app(a)->get_num_args() == 0 && to_app(a)->get_family_id() == null_family_id; + } public: smtfd_abs(ast_manager& m): @@ -248,13 +252,27 @@ namespace smtfd { std::ostream& display(std::ostream& out) const { return out << "abs:\n" << m_atoms << "\n"; } + + expr* abs_assumption(expr* e) { + expr* a = abs(e), *b = nullptr; + if (is_uninterp_atom(a) || (m.is_not(a, b) && is_uninterp_atom(b))) { + return a; + } + expr* f = fresh_var(e); + push_trail(m_abs, m_abs_trail, e, f); + push_trail(m_rep, m_rep_trail, f, e); + m_atoms.push_back(f); + m_atom_defs.push_back(m.mk_iff(f, a)); + return f; + } + expr* abs(expr* e) { expr* r = try_abs(e); if (r) return r; m_todo.push_back(e); family_id bvfid = m_butil.get_fid(); - family_id bfid = m.get_basic_family_id(); + family_id bfid = m.get_basic_family_id(); family_id pbfid = m_pb.get_family_id(); while (!m_todo.empty()) { expr* t = m_todo.back(); @@ -311,6 +329,9 @@ namespace smtfd { } push_trail(m_abs, m_abs_trail, t, r); push_trail(m_rep, m_rep_trail, r, t); + if (t != r) { + push_trail(m_abs, m_abs_trail, r, r); + } if (is_atom(r)) { m_atoms.push_back(r); } @@ -353,12 +374,7 @@ namespace smtfd { smtfd_abs& get_abs() { return m_abs; } - void add(expr* f) { - expr_ref _fml(f, m); - // std::cout << "add " << mk_bounded_pp(f, m, 2) << "\n"; - TRACE("smtfd", tout << _fml << "\n";); - m_lemmas.push_back(m_abs.abs(f)); - } + void add(expr* f) { m_lemmas.push_back(f); } ast_manager& get_manager() { return m_lemmas.get_manager(); } @@ -508,9 +524,14 @@ namespace smtfd { return; } m_args.reset(); + SASSERT(t->get_num_args() == f1.m_t->get_num_args()); + SASSERT(t->get_num_args() == f2.m_t->get_num_args()); for (unsigned i = 0; i < t->get_num_args(); ++i) { - m_args.push_back(m.mk_eq(f1.m_t->get_arg(i), f2.m_t->get_arg(i))); + expr* e1 = f1.m_t->get_arg(i); + expr* e2 = f2.m_t->get_arg(i); + if (e1 != e2) m_args.push_back(m.mk_eq(e1, e2)); } + TRACE("smtfd", tout << mk_bounded_pp(f1.m_t, m, 2) << " " << mk_bounded_pp(f2.m_t, m, 2) << "\n";); add_lemma(m.mk_implies(mk_and(m_args), m.mk_eq(f1.m_t, f2.m_t))); } @@ -799,7 +820,7 @@ namespace smtfd { }; - class a_plugin : public theory_plugin { + class ar_plugin : public theory_plugin { array_util m_autil; th_rewriter m_rewriter; @@ -826,7 +847,6 @@ namespace smtfd { add_lemma(m.mk_eq(sel, stored_value)); } m_pinned.push_back(sel); - TRACE("smtfd", tout << mk_bounded_pp(sel, m, 2) << "\n";); check_select(sel); } @@ -854,11 +874,9 @@ namespace smtfd { table& tA = ast2table(vA); // select table of arg if (vT == vA) { - TRACE("smtfd", display(tout << "eq\n", tT);); return; } - TRACE("smtfd", tout << mk_pp(t, m) << "\n" << vT << "\n" << vA << "\n";); m_vargs.reset(); for (unsigned i = 0; i + 1 < t->get_num_args(); ++i) { m_vargs.push_back(eval_abs(t->get_arg(i))); @@ -904,6 +922,7 @@ namespace smtfd { expr_ref sel1(m_autil.mk_select(m_args), m); m_args[0] = a; expr_ref sel2(m_autil.mk_select(m_args), m); + TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << "\n";); add_lemma(m.mk_or(eq, m.mk_eq(sel1, sel2))); } @@ -989,7 +1008,11 @@ namespace smtfd { expr_ref a1(m_autil.mk_select(args), m); args[0] = b; expr_ref b1(m_autil.mk_select(args), m); - add_lemma(m.mk_implies(m.mk_eq(a1, b1), m.mk_eq(a, b))); + TRACE("smtfd", tout << mk_bounded_pp(a, m, 2) << " " << mk_bounded_pp(b, m, 2) << "\n";); + expr_ref ext(m.mk_implies(m.mk_eq(a1, b1), m.mk_eq(a, b)), m); + if (!m.is_true(eval_abs(ext))) { + add_lemma(ext); + } } expr_ref mk_array_value(table& t) { @@ -1019,7 +1042,7 @@ namespace smtfd { public: - a_plugin(plugin_context& context, model_ref& mdl): + ar_plugin(plugin_context& context, model_ref& mdl): theory_plugin(context, mdl), m_autil(m), m_rewriter(m) @@ -1364,7 +1387,7 @@ namespace smtfd { m_not_toggle = abs(m_not_toggle); m_assertions_qhead = m_assertions.size(); fml = m.mk_iff(m_toggle, fml); - assert_fd(abs(fml)); + assert_fd(fml); } } @@ -1436,13 +1459,13 @@ namespace smtfd { bool add_theory_axioms(expr_ref_vector const& core) { plugin_context context(m_abs, m, m_max_lemmas); - a_plugin ap(context, m_model); + ar_plugin ap(context, m_model); uf_plugin uf(context, m_model); for (unsigned round = 0; !context.at_max() && context.add_theory_axioms(core, round); ++round); TRACE("smtfd", context.display(tout);); for (expr* f : context) { - IF_VERBOSE(10, verbose_stream() << "lemma: " << expr_ref(rep(f), m) << "\n"); + IF_VERBOSE(10, verbose_stream() << "lemma: " << expr_ref(f, m) << "\n"); assert_fd(f); } m_stats.m_num_lemmas += context.size(); @@ -1455,7 +1478,7 @@ namespace smtfd { lbool is_decided_sat(expr_ref_vector const& core) { plugin_context context(m_abs, m, m_max_lemmas); uf_plugin uf(context, m_model); - a_plugin ap(context, m_model); + ar_plugin ap(context, m_model); bv_plugin bv(context, m_model); basic_plugin bs(context, m_model); pb_plugin pb(context, m_model); @@ -1473,7 +1496,7 @@ namespace smtfd { } context.populate_model(m_model, core); - TRACE("smtfd", tout << has_q << " " << has_non_covered << "\n";); + TRACE("smtfd", tout << "has quantifier: " << has_q << " has non-converted: " << has_non_covered << "\n";); if (!has_q) { return is_decided; } @@ -1485,7 +1508,7 @@ namespace smtfd { return l_false; } for (expr* f : context) { - IF_VERBOSE(10, verbose_stream() << "lemma: " << expr_ref(rep(f), m) << "\n"); + IF_VERBOSE(10, verbose_stream() << "lemma: " << expr_ref(f, m) << "\n"); assert_fd(f); } m_stats.m_num_mbqi += context.size(); @@ -1496,8 +1519,9 @@ namespace smtfd { asms.reset(); asms.push_back(m_toggle); for (unsigned i = 0; i < sz; ++i) { - asms.push_back(abs(user_asms[i])); + asms.push_back(abs_assumption(user_asms[i])); } + flush_atom_defs(); } void init_model_assumptions(unsigned sz, expr* const* user_asms, expr_ref_vector& asms) { @@ -1525,6 +1549,7 @@ namespace smtfd { expr* rep(expr* e) { return m_abs.rep(e); } expr* abs(expr* e) { return m_abs.abs(e); } + expr* abs_assumption(expr* e) { return m_abs.abs_assumption(e); } expr_ref_vector& rep(expr_ref_vector& v) { for (unsigned i = v.size(); i-- > 0; ) v[i] = rep(v.get(i)); return v; } expr_ref_vector& abs(expr_ref_vector& v) { for (unsigned i = v.size(); i-- > 0; ) v[i] = abs(v.get(i)); return v; } @@ -1539,10 +1564,8 @@ namespace smtfd { std::ostream& display(std::ostream& out, unsigned n = 0, expr * const * assumptions = nullptr) const override { if (!m_fd_sat_solver) return out; - m_fd_sat_solver->display(out); - //m_fd_core_solver->display(out << "core solver\n"); - //m_smt_solver->display(out << "smt solver\n"); - out << m_assumptions << "\n"; + // m_fd_sat_solver->display(out); + // out << m_assumptions << "\n"; m_abs.display(out); return out; } @@ -1613,16 +1636,18 @@ namespace smtfd { } void assert_fd(expr* fml) { - m_fd_sat_solver->assert_expr(fml); - m_fd_core_solver->assert_expr(fml); + expr_ref _fml(fml, m); + _fml = abs(fml); + m_fd_sat_solver->assert_expr(_fml); + m_fd_core_solver->assert_expr(_fml); flush_atom_defs(); } - void block_core(expr_ref_vector& core) { - assert_fd(m.mk_not(mk_and(abs(core)))); + void block_core(expr_ref_vector const& core) { + assert_fd(m.mk_not(mk_and(core))); } -#if 1 +#if 0 lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { init(); flush_assertions(); @@ -1682,22 +1707,23 @@ namespace smtfd { lbool r = l_undef; expr_ref_vector core(m); while (true) { - IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat " << m_stats.m_num_rounds << " " << m_stats.m_num_lemmas << " " << m_stats.m_num_mbqi << ")\n"); + IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat " << m_stats.m_num_rounds + << " " << m_stats.m_num_lemmas << " " << m_stats.m_num_mbqi << ")\n"); m_stats.m_num_rounds++; checkpoint(); - + // phase 1: check sat of abs r = check_abs(num_assumptions, assumptions); if (r != l_true) { break; } - + // phase 2: find prime implicate over FD (abstraction) r = get_prime_implicate(num_assumptions, assumptions, core); if (r != l_false) { break; } - + // phase 3: check if prime implicate is really valid, or add theory lemmas until there is a theory core r = refine_core(core); switch (r) { @@ -1731,14 +1757,15 @@ namespace smtfd { } lbool refine_core(expr_ref_vector & core) { - plugin_context context(m_abs, m, UINT_MAX); - a_plugin ap(context, m_model); - uf_plugin uf(context, m_model); - lbool r = l_undef; unsigned round = 0; - while (context.add_theory_axioms(core, round)) { - std::cout << round << "\n"; + while (true) { + plugin_context context(m_abs, m, UINT_MAX); + ar_plugin ap(context, m_model); + uf_plugin uf(context, m_model); + if (!context.add_theory_axioms(core, round)) { + break; + } round = context.empty() ? round + 1 : 0; r = refine_core(context, core); if (r != l_true) { @@ -1753,15 +1780,12 @@ namespace smtfd { lbool refine_core(plugin_context& context, expr_ref_vector& core) { if (context.empty()) { return l_true; - } - abs(core); + } for (expr* f : context) { - // std::cout << "refine: " << mk_pp(f, m) << "\n"; core.push_back(f); } - flush_atom_defs(); - context.reset_lemmas(); - lbool r = m_fd_sat_solver->check_sat(core); + m_stats.m_num_lemmas += context.size(); + lbool r = check_abs(core.size(), core.c_ptr()); update_reason_unknown(r, m_fd_sat_solver); switch (r) { case l_false: @@ -1770,7 +1794,7 @@ namespace smtfd { break; case l_true: m_fd_sat_solver->get_model(m_model); - rep(core); + m_model->set_model_completion(true); break; default: break;