diff --git a/src/muz_qe/dl_mk_scale.cpp b/src/muz_qe/dl_mk_scale.cpp new file mode 100644 index 000000000..bcd19d0a4 --- /dev/null +++ b/src/muz_qe/dl_mk_scale.cpp @@ -0,0 +1,128 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_scale.cpp + +Abstract: + + +Author: + + Nikolaj Bjorner (nbjorner) 2013-08-19 + +Revision History: + +--*/ + +#include"dl_mk_scale.h" +#include"dl_context.h" + +namespace datalog { + + + mk_scale::mk_scale(context & ctx, unsigned priority): + plugin(priority), + m(ctx.get_manager()), + m_ctx(ctx), + a(m), + m_trail(m) { + } + + mk_scale::~mk_scale() { } + + rule_set * mk_scale::operator()(rule_set const & source) { + if (!m_ctx.get_params().scale()) { + return 0; + } + context& ctx = source.get_context(); + rule_manager& rm = source.get_rule_manager(); + rule_set * result = alloc(rule_set, ctx); + unsigned sz = source.get_num_rules(); + rule_ref new_rule(rm); + app_ref_vector tail(m); + app_ref head(m); + svector neg; + ptr_vector vars; + for (unsigned i = 0; i < sz; ++i) { + rule & r = *source.get_rule(i); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + tail.reset(); + neg.reset(); + vars.reset(); + r.get_vars(vars); + m_cache.reset(); + m_trail.reset(); + unsigned num_vars = vars.size(); + for (unsigned j = utsz; j < tsz; ++j) { + tail.push_back(mk_pred(num_vars, r.get_tail(j))); + neg.push_back(false); + } + for (unsigned j = 0; j < utsz; ++j) { + tail.push_back(mk_constraint(num_vars, r.get_tail(j))); + neg.push_back(false); + } + tail.push_back(a.mk_gt(m.mk_var(num_vars, a.mk_real()), a.mk_numeral(rational(0), false))); + neg.push_back(false); + new_rule = rm.mk(mk_pred(num_vars, r.get_head()), tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); + result->add_rule(new_rule); + if (source.is_output_predicate(r.get_decl())) { + result->set_output_predicate(new_rule->get_decl()); + } + } + TRACE("dl", result->display(tout);); + return result; + } + + app_ref mk_scale::mk_pred(unsigned num_vars, app* q) { + func_decl* f = q->get_decl(); + ptr_vector domain(f->get_arity(), f->get_domain()); + domain.push_back(a.mk_real()); + func_decl_ref g(m); + g = m.mk_func_decl(f->get_name(), f->get_arity() + 1, domain.c_ptr(), f->get_range()); + ptr_vector args(q->get_num_args(), q->get_args()); + args.push_back(m.mk_var(num_vars, a.mk_real())); + m_ctx.register_predicate(g, false); + return app_ref(m.mk_app(g, q->get_num_args() + 1, args.c_ptr()), m); + } + + app_ref mk_scale::mk_constraint(unsigned num_vars, app* q) { + expr* r = linearize(num_vars, q); + SASSERT(is_app(r)); + return app_ref(to_app(r), m); + } + + expr* mk_scale::linearize(unsigned num_vars, expr* e) { + expr* r; + if (m_cache.find(e, r)) { + return expr_ref(r, m); + } + if (!is_app(e)) { + return expr_ref(e, m); + } + expr_ref result(m); + app* ap = to_app(e); + if (ap->get_family_id() == m.get_basic_family_id() || + a.is_add(e) || a.is_sub(e) || + a.is_le(e) || a.is_ge(e) || + a.is_lt(e) || a.is_gt(e)) { + expr_ref_vector args(m); + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + args.push_back(linearize(num_vars, ap->get_arg(i))); + } + result = m.mk_app(ap->get_decl(), args.size(), args.c_ptr()); + } + else if (a.is_numeral(e)) { + result = a.mk_mul(m.mk_var(num_vars, a.mk_real()), e); + } + else { + result = e; + } + m_trail.push_back(result); + m_cache.insert(e, result); + return result; + } + +}; diff --git a/src/muz_qe/dl_mk_scale.h b/src/muz_qe/dl_mk_scale.h new file mode 100644 index 000000000..cff226321 --- /dev/null +++ b/src/muz_qe/dl_mk_scale.h @@ -0,0 +1,47 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_scale.h + +Abstract: + + Add scale factor to linear (Real) arithemetic Horn clauses. + The transformation replaces occurrences of isolated constants by + a scale multiplied to each constant. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-08-19 + +Revision History: + +--*/ +#ifndef _DL_MK_SCALE_H_ +#define _DL_MK_SCALE_H_ + +#include"dl_rule_transformer.h" +#include"arith_decl_plugin.h" + +namespace datalog { + + class mk_scale : public rule_transformer::plugin { + ast_manager& m; + context& m_ctx; + arith_util a; + expr_ref_vector m_trail; + obj_map m_cache; + expr* linearize(unsigned num_vars, expr* e); + app_ref mk_pred(unsigned num_vars, app* q); + app_ref mk_constraint(unsigned num_vars, app* q); + public: + mk_scale(context & ctx, unsigned priority = 33039); + ~mk_scale(); + rule_set * operator()(rule_set const & source); + }; + +}; + +#endif /* _DL_MK_SCALE_H_ */ + diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index 555c44df2..46f4fce99 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -11,6 +11,7 @@ def_module_params('fixedpoint', ('explanations_on_relation_level', BOOL, False, '(DATALOG) if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect)'), ('magic_sets_for_queries', BOOL, False, "(DATALOG) magic set transformation will be used for queries"), ('magic', BOOL, False, "perform symbolic magic set transformation"), + ('scale', BOOL, False, "add scaling variable to linear real arithemtic clauses"), ('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"), ('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"), ('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"),