From b46f31211505688c3f8702558a5c55ba6a53d0d9 Mon Sep 17 00:00:00 2001 From: mikolas Date: Mon, 11 Jan 2016 17:18:22 +0000 Subject: [PATCH] A proper model converter for the lazy mode. --- src/ackr/lackr_model_constructor.cpp | 80 ++++++++++++++++++++++--- src/ackr/lackr_model_constructor.h | 29 +++++++-- src/ackr/lackr_model_converter_lazy.cpp | 60 +++++++++++++++++++ src/ackr/lackr_model_converter_lazy.h | 23 +++++++ 4 files changed, 179 insertions(+), 13 deletions(-) create mode 100644 src/ackr/lackr_model_converter_lazy.cpp create mode 100644 src/ackr/lackr_model_converter_lazy.h diff --git a/src/ackr/lackr_model_constructor.cpp b/src/ackr/lackr_model_constructor.cpp index 3f727cd92..bcc036d2e 100644 --- a/src/ackr/lackr_model_constructor.cpp +++ b/src/ackr/lackr_model_constructor.cpp @@ -68,6 +68,57 @@ struct lackr_model_constructor::imp { } return run(); } + + + void make_model(model_ref& destination) { + { + for (unsigned i = 0; i < m_abstr_model->get_num_uninterpreted_sorts(); i++) { + sort * const s = m_abstr_model->get_uninterpreted_sort(i); + ptr_vector u = m_abstr_model->get_universe(s); + destination->register_usort(s, u.size(), u.c_ptr()); + } + } + { + const app2val_t::iterator e = m_app2val.end(); + app2val_t::iterator i = m_app2val.end(); + for (; i != e; ++i) { + app * a = i->m_key; + if (a->get_num_args()) continue; + destination->register_decl(a->get_decl(), i->m_value); + } + } + + obj_map interpretations; + { + const values2val_t::iterator e = m_values2val.end(); + values2val_t::iterator i = m_values2val.end(); + for (; i != e; ++i) add_entry(i->m_key, i->m_value.value, interpretations); + } + + { + obj_map::iterator ie = interpretations.end(); + obj_map::iterator ii = interpretations.begin(); + for (; ii != ie; ++ii) { + func_decl* const fd = ii->m_key; + func_interp* const fi = ii->get_value(); + fi->set_else(m_m.get_some_value(fd->get_range())); + destination->register_decl(fd, fi); + } + } + } + + void add_entry(app* term, expr* value, + obj_map& interpretations) { + func_interp* fi = 0; + func_decl * const declaration = term->get_decl(); + const unsigned sz = declaration->get_arity(); + SASSERT(sz == term->get_num_args()); + if (!interpretations.find(declaration, fi)) { + fi = alloc(func_interp, m_m, sz); + interpretations.insert(declaration, fi); + } + fi->insert_new_entry(term->get_args(), value); + } private: ast_manager& m_m; ackr_info_ref m_info; @@ -299,15 +350,30 @@ struct lackr_model_constructor::imp { }; lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref info) - : m(m) - , state(UNKNOWN) - , info(info) + : m_imp(0) + , m_m(m) + , m_state(UNKNOWN) + , m_info(info) + , m_ref_count(0) {} +lackr_model_constructor::~lackr_model_constructor() { + if (m_imp) dealloc(m_imp); +} + bool lackr_model_constructor::check(model_ref& abstr_model) { - conflicts.reset(); - lackr_model_constructor::imp i(m, info, abstr_model, conflicts); - const bool rv = i.check(); - state = rv ? CHECKED : CONFLICT; + m_conflicts.reset(); + if (m_imp) { + dealloc(m_imp); + m_imp = 0; + } + m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts); + const bool rv = m_imp->check(); + m_state = rv ? CHECKED : CONFLICT; return rv; } + +void lackr_model_constructor::make_model(model_ref& model) { + SASSERT(m_state == CHECKED); + m_imp->make_model(model); +} diff --git a/src/ackr/lackr_model_constructor.h b/src/ackr/lackr_model_constructor.h index 5b2385c2c..478efe97f 100644 --- a/src/ackr/lackr_model_constructor.h +++ b/src/ackr/lackr_model_constructor.h @@ -25,16 +25,33 @@ class lackr_model_constructor { typedef std::pair app_pair; typedef vector conflict_list; lackr_model_constructor(ast_manager& m, ackr_info_ref info); + ~lackr_model_constructor(); bool check(model_ref& abstr_model); const conflict_list& get_conflicts() { - SASSERT(state == CONFLICT); - return conflicts; + SASSERT(m_state == CONFLICT); + return m_conflicts; + } + void make_model(model_ref& model); + + // + // Reference counting + // + void inc_ref() { ++m_ref_count; } + void dec_ref() { + --m_ref_count; + if (m_ref_count == 0) { + dealloc(this); + } } private: struct imp; - enum {CHECKED, CONFLICT, UNKNOWN} state; - conflict_list conflicts; - ast_manager& m; - const ackr_info_ref info; + imp * m_imp; + enum {CHECKED, CONFLICT, UNKNOWN} m_state; + conflict_list m_conflicts; + ast_manager& m_m; + const ackr_info_ref m_info; + unsigned m_ref_count; // reference counting }; + +typedef ref lackr_model_constructor_ref; #endif /* MODEL_CONSTRUCTOR_H_626 */ diff --git a/src/ackr/lackr_model_converter_lazy.cpp b/src/ackr/lackr_model_converter_lazy.cpp new file mode 100644 index 000000000..dc3a2b40e --- /dev/null +++ b/src/ackr/lackr_model_converter_lazy.cpp @@ -0,0 +1,60 @@ +/*++ + Copyright (c) 2015 Microsoft Corporation + + Module Name: + + lackr_model_converter_lazy.cpp + + Abstract: + + + Author: + + Mikolas Janota + + Revision History: +--*/ +#include"lackr_model_converter_lazy.h" +#include"model_evaluator.h" +#include"ast_smt2_pp.h" +#include"ackr_info.h" +#include"lackr_model_constructor.h" + + +class lackr_model_converter_lazy : public model_converter { +public: + lackr_model_converter_lazy(ast_manager & m, + const lackr_model_constructor_ref& lmc) + : m(m) + , model_constructor(lmc) + { } + + virtual ~lackr_model_converter_lazy() { } + + virtual void operator()(model_ref & md, unsigned goal_idx) { + SASSERT(goal_idx == 0); + SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions())); + SASSERT(model_constructor.get()); + model * new_model = alloc(model, m); + md = new_model; + model_constructor->make_model(md); + } + + virtual void operator()(model_ref & md) { + operator()(md, 0); + } + + //void display(std::ostream & out); + + virtual model_converter * translate(ast_translation & translator) { + NOT_IMPLEMENTED_YET(); + } +protected: + ast_manager& m; + const lackr_model_constructor_ref model_constructor; +}; + +model_converter * mk_lackr_model_converter_lazy(ast_manager & m, + const lackr_model_constructor_ref& model_constructor) { + return alloc(lackr_model_converter_lazy, m, model_constructor); +} diff --git a/src/ackr/lackr_model_converter_lazy.h b/src/ackr/lackr_model_converter_lazy.h new file mode 100644 index 000000000..354e1c40b --- /dev/null +++ b/src/ackr/lackr_model_converter_lazy.h @@ -0,0 +1,23 @@ + /*++ + Copyright (c) 2015 Microsoft Corporation + + Module Name: + + lackr_model_converter_lazy.h + + Abstract: + + + Author: + + Mikolas Janota + + Revision History: + --*/ +#ifndef LACKR_MODEL_CONVERTER_LAZY_H_14201 +#define LACKR_MODEL_CONVERTER_LAZY_H_14201 +#include"model_converter.h" +#include"ackr_info.h" + +model_converter * mk_lackr_model_converter_lazy(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); +#endif /* LACKR_MODEL_CONVERTER_LAZY_H_14201 */