From a8b65ebb360168c9659e943e3f264690c5d8e3f8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 23 Apr 2014 20:10:53 +0100 Subject: [PATCH] added stubs for theory_fpa Signed-off-by: Christoph M. Wintersteiger --- examples/c/test_capi.c | 36 +++++++++++++++++++++++++++++++++++ src/ast/fpa/fpa2bv_rewriter.h | 6 ++---- src/smt/smt_setup.cpp | 15 +++++++++++++++ src/smt/smt_setup.h | 6 +++++- src/smt/theory_fpa.cpp | 19 ++++++++++++++++-- src/smt/theory_fpa.h | 8 +++++--- 6 files changed, 80 insertions(+), 10 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 27bf6de2c..4363ee382 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -2595,6 +2595,42 @@ void substitute_vars_example() { Z3_del_context(ctx); } +void fpa_example() { + Z3_config cfg; + Z3_context ctx; + Z3_sort double_sort, rm_sort; + Z3_symbol symbol_rm, symbol_x, symbol_y; + Z3_ast rm, x, y, n, c; + + printf("\nFPA-example\n"); + LOG_MSG("FPA-example"); + + enable_trace("fpa"); + + cfg = Z3_mk_config(); + ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + double_sort = Z3_mk_fpa_sort(ctx, 11, 53); + rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx); + + symbol_rm = Z3_mk_string_symbol(ctx, "rm"); + rm = Z3_mk_const(ctx, symbol_rm, rm_sort); + symbol_x = Z3_mk_string_symbol(ctx, "x"); + symbol_y = Z3_mk_string_symbol(ctx, "y"); + x = Z3_mk_const(ctx, symbol_x, double_sort); + y = Z3_mk_const(ctx, symbol_y, double_sort); + n = Z3_mk_double(ctx, 42.0, double_sort); + + c = Z3_mk_eq(ctx, Z3_mk_fpa_add(ctx, rm, x, y), n); + + Z3_assert_cnstr(ctx, c); + if (Z3_check(ctx) != Z3_L_TRUE) + printf("FPA-example not satisfied!\n"); + + Z3_del_context(ctx); +} + /*@}*/ /*@}*/ diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index b2e3da939..bdfa6ca3f 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -64,9 +64,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { } bool max_steps_exceeded(unsigned num_steps) const { - cooperate("fpa2bv"); - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + cooperate("fpa2bv"); return num_steps > m_max_steps; } @@ -147,7 +145,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); - throw tactic_exception("NYI"); + NOT_IMPLEMENTED_YET(); } } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 51b83d61c..64477164a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -30,6 +30,7 @@ Revision History: #include"theory_dummy.h" #include"theory_dl.h" #include"theory_seq_empty.h" +#include"theory_fpa.h" namespace smt { @@ -679,6 +680,15 @@ namespace smt { setup_mi_arith(); } + void setup::setup_QF_FPA() { + m_context.register_plugin(alloc(smt::theory_fpa, m_manager)); + } + + void setup::setup_QF_FPABV() { + setup_QF_BV(); + m_context.register_plugin(alloc(smt::theory_fpa, m_manager)); + } + bool is_arith(static_features const & st) { return st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0; } @@ -780,6 +790,10 @@ namespace smt { m_context.register_plugin(alloc(theory_seq_empty, m_manager)); } + void setup::setup_fpa() { + m_context.register_plugin(alloc(theory_fpa, m_manager)); + } + void setup::setup_unknown() { setup_arith(); setup_arrays(); @@ -787,6 +801,7 @@ namespace smt { setup_datatypes(); setup_dl(); setup_seq(); + setup_fpa(); } void setup::setup_unknown(static_features & st) { diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index e0188537e..299ce7834 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -75,6 +75,8 @@ namespace smt { void setup_QF_AX(static_features const & st); void setup_QF_AUFLIA(); void setup_QF_AUFLIA(static_features const & st); + void setup_QF_FPA(); + void setup_QF_FPABV(); void setup_LRA(); void setup_AUFLIA(bool simple_array = true); void setup_AUFLIA(static_features const & st); @@ -91,10 +93,12 @@ namespace smt { void setup_bv(); void setup_arith(); void setup_dl(); - void setup_seq(); + void setup_seq(); void setup_instgen(); void setup_i_arith(); void setup_mi_arith(); + void setup_fpa(); + public: setup(context & c, smt_params & params); void mark_already_configured() { m_already_configured = true; } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 147d87496..e235dbb06 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -17,14 +17,29 @@ Revision History: --*/ #include"ast_smt2_pp.h" +#include"smt_context.h" #include"theory_fpa.h" namespace smt { + theory_fpa::theory_fpa(ast_manager & m) : + theory(m.mk_family_id("float")), + m_converter(m), + m_rw(m, m_converter, params_ref()) + { + } + bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) { - TRACE("bv", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";); + TRACE("fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";); SASSERT(atom->get_family_id() == get_family_id()); - NOT_IMPLEMENTED_YET(); + + ast_manager & m = get_manager(); + context & ctx = get_context(); + + expr_ref res(m); + m_rw(atom, res); + SASSERT(res.get() != atom); + ctx.internalize(res, gate_ctx); return true; } diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 3716247d3..bb3a8b786 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -21,14 +21,16 @@ Revision History: #include"smt_theory.h" #include"fpa2bv_converter.h" +#include"fpa2bv_rewriter.h" namespace smt { class theory_fpa : public theory { fpa2bv_converter m_converter; + fpa2bv_rewriter m_rw; virtual final_check_status final_check_eh() { return FC_DONE; } - virtual bool internalize_atom(app*, bool); - virtual bool internalize_term(app*) { return internalize_atom(0, false); } + virtual bool internalize_atom(app * a, bool); + virtual bool internalize_term(app * a) { return internalize_atom(a, false); } virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); virtual void push_scope_eh(); @@ -36,7 +38,7 @@ namespace smt { virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); } virtual char const * get_name() const { return "fpa"; } public: - theory_fpa(ast_manager& m) : theory(m.mk_family_id("fpa")), m_converter(m) {} + theory_fpa(ast_manager& m); }; };