diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 680b59c68..c4b5c97d7 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -46,7 +46,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_int_symbol(c, i); RESET_ERROR_CODE(); - if (i < 0 || (unsigned)i >= (SIZE_MAX >> PTR_ALIGNMENT)) { + if (i < 0 || (size_t)i >= (SIZE_MAX >> PTR_ALIGNMENT)) { SET_ERROR_CODE(Z3_IOB); return 0; } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index d048bb2f7..cd33c7782 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -268,6 +268,8 @@ public: bool is_int_real(expr const * n) const { return is_int_real(get_sort(n)); } MATCH_UNARY(is_uminus); + MATCH_UNARY(is_to_real); + MATCH_UNARY(is_to_int); MATCH_BINARY(is_sub); MATCH_BINARY(is_add); MATCH_BINARY(is_mul); diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 5819e3930..f684879ae 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -260,6 +260,7 @@ class smt_printer { else { m_out << sym << "["; } + for (unsigned i = 0; i < num_params; ++i) { parameter const& p = params[i]; if (p.is_ast()) { @@ -642,9 +643,7 @@ class smt_printer { m_out << m_var_names[m_num_var_names - idx - 1]; } else { - if (!m_is_smt2) { - m_out << "?" << idx; - } + m_out << "?" << idx; } } diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp index 6deb4bf45..0569eb360 100644 --- a/src/ast/expr_abstract.cpp +++ b/src/ast/expr_abstract.cpp @@ -20,52 +20,50 @@ Notes: #include "expr_abstract.h" #include "map.h" -void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { - ast_ref_vector pinned(m); - ptr_vector stack; - obj_map map; +void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { + expr * curr = 0, *b = 0; SASSERT(n->get_ref_count() > 0); - stack.push_back(n); + m_stack.push_back(n); for (unsigned i = 0; i < num_bound; ++i) { b = bound[i]; expr* v = m.mk_var(base + num_bound - i - 1, m.get_sort(b)); - pinned.push_back(v); - map.insert(b, v); + m_pinned.push_back(v); + m_map.insert(b, v); } - while(!stack.empty()) { - curr = stack.back(); - if (map.contains(curr)) { - stack.pop_back(); + while(!m_stack.empty()) { + curr = m_stack.back(); + if (m_map.contains(curr)) { + m_stack.pop_back(); continue; } switch(curr->get_kind()) { case AST_VAR: { - map.insert(curr, curr); - stack.pop_back(); + m_map.insert(curr, curr); + m_stack.pop_back(); break; } case AST_APP: { app* a = to_app(curr); bool all_visited = true; - ptr_vector args; + m_args.reset(); for (unsigned i = 0; i < a->get_num_args(); ++i) { - if (!map.find(a->get_arg(i), b)) { - stack.push_back(a->get_arg(i)); + if (!m_map.find(a->get_arg(i), b)) { + m_stack.push_back(a->get_arg(i)); all_visited = false; } else { - args.push_back(b); + m_args.push_back(b); } } if (all_visited) { - b = m.mk_app(a->get_decl(), args.size(), args.c_ptr()); - pinned.push_back(b); - map.insert(curr, b); - stack.pop_back(); + b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr()); + m_pinned.push_back(b); + m_map.insert(curr, b); + m_stack.pop_back(); } break; } @@ -81,17 +79,24 @@ void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* cons } expr_abstract(m, new_base, num_bound, bound, q->get_expr(), result1); b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get()); - pinned.push_back(b); - map.insert(curr, b); - stack.pop_back(); + m_pinned.push_back(b); + m_map.insert(curr, b); + m_stack.pop_back(); break; } default: UNREACHABLE(); } } - if (!map.find(n, b)) { - UNREACHABLE(); - } + VERIFY (m_map.find(n, b)); result = b; + m_pinned.reset(); + m_map.reset(); + m_stack.reset(); + m_args.reset(); +} + +void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { + expr_abstractor abs(m); + abs(base, num_bound, bound, n, result); } diff --git a/src/ast/expr_abstract.h b/src/ast/expr_abstract.h index c6ec7973b..3d9f3960f 100644 --- a/src/ast/expr_abstract.h +++ b/src/ast/expr_abstract.h @@ -21,6 +21,17 @@ Notes: #include"ast.h" +class expr_abstractor { + ast_manager& m; + expr_ref_vector m_pinned; + ptr_vector m_stack, m_args; + obj_map m_map; + +public: + expr_abstractor(ast_manager& m): m(m), m_pinned(m) {} + void operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result); +}; + void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result); #endif diff --git a/src/ast/rewriter/ast_counter.cpp b/src/ast/rewriter/ast_counter.cpp index c542abb60..a807237c5 100644 --- a/src/ast/rewriter/ast_counter.cpp +++ b/src/ast/rewriter/ast_counter.cpp @@ -93,7 +93,9 @@ void var_counter::count_vars(ast_manager & m, const app * pred, int coef) { unsigned n = pred->get_num_args(); for (unsigned i = 0; i < n; i++) { m_sorts.reset(); - ::get_free_vars(pred->get_arg(i), m_sorts); + m_todo.reset(); + m_mark.reset(); + ::get_free_vars(m_mark, m_todo, pred->get_arg(i), m_sorts); for (unsigned j = 0; j < m_sorts.size(); ++j) { if (m_sorts[j]) { update(j, coef); @@ -108,24 +110,27 @@ unsigned var_counter::get_max_var(bool& has_var) { unsigned max_var = 0; while (!m_todo.empty()) { expr* e = m_todo.back(); - unsigned scope = m_scopes.back(); m_todo.pop_back(); - m_scopes.pop_back(); if (m_visited.is_marked(e)) { continue; } m_visited.mark(e, true); switch(e->get_kind()) { case AST_QUANTIFIER: { + var_counter aux_counter; quantifier* q = to_quantifier(e); - m_todo.push_back(q->get_expr()); - m_scopes.push_back(scope + q->get_num_decls()); + bool has_var1 = false; + unsigned max_v = aux_counter.get_max_var(has_var1); + if (max_v > max_var + q->get_num_decls()) { + max_var = max_v - q->get_num_decls(); + has_var = true; + } break; } case AST_VAR: { - if (to_var(e)->get_idx() >= scope + max_var) { + if (to_var(e)->get_idx() >= max_var) { has_var = true; - max_var = to_var(e)->get_idx() - scope; + max_var = to_var(e)->get_idx(); } break; } @@ -133,7 +138,6 @@ unsigned var_counter::get_max_var(bool& has_var) { app* a = to_app(e); for (unsigned i = 0; i < a->get_num_args(); ++i) { m_todo.push_back(a->get_arg(i)); - m_scopes.push_back(scope); } break; } @@ -150,14 +154,12 @@ unsigned var_counter::get_max_var(bool& has_var) { unsigned var_counter::get_max_var(expr* e) { bool has_var = false; m_todo.push_back(e); - m_scopes.push_back(0); return get_max_var(has_var); } unsigned var_counter::get_next_var(expr* e) { bool has_var = false; m_todo.push_back(e); - m_scopes.push_back(0); unsigned mv = get_max_var(has_var); if (has_var) mv++; return mv; diff --git a/src/ast/rewriter/ast_counter.h b/src/ast/rewriter/ast_counter.h index 2a581c302..e7251079f 100644 --- a/src/ast/rewriter/ast_counter.h +++ b/src/ast/rewriter/ast_counter.h @@ -38,6 +38,7 @@ public: counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {} + void reset() { m_data.reset(); } iterator begin() const { return m_data.begin(); } iterator end() const { return m_data.end(); } void update(unsigned el, int delta); @@ -71,6 +72,7 @@ protected: ptr_vector m_sorts; expr_fast_mark1 m_visited; ptr_vector m_todo; + ast_mark m_mark; unsigned_vector m_scopes; unsigned get_max_var(bool & has_var); public: diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index 3ebc0b573..930267dad 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include"var_subst.h" -#include"used_vars.h" #include"ast_ll_pp.h" #include"ast_pp.h" #include"ast_smt2_pp.h" @@ -40,7 +39,7 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";); } -void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { +void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { SASSERT(is_well_sorted(m, q)); if (is_ground(q->get_expr())) { // ignore patterns if the body is a ground formula. @@ -51,17 +50,17 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { result = q; return; } - used_vars used; - used.process(q->get_expr()); + m_used.reset(); + m_used.process(q->get_expr()); unsigned num_patterns = q->get_num_patterns(); for (unsigned i = 0; i < num_patterns; i++) - used.process(q->get_pattern(i)); + m_used.process(q->get_pattern(i)); unsigned num_no_patterns = q->get_num_no_patterns(); for (unsigned i = 0; i < num_no_patterns; i++) - used.process(q->get_no_pattern(i)); + m_used.process(q->get_no_pattern(i)); unsigned num_decls = q->get_num_decls(); - if (used.uses_all_vars(num_decls)) { + if (m_used.uses_all_vars(num_decls)) { q->set_no_unused_vars(); result = q; return; @@ -70,7 +69,7 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { ptr_buffer used_decl_sorts; buffer used_decl_names; for (unsigned i = 0; i < num_decls; ++i) { - if (used.contains(num_decls - i - 1)) { + if (m_used.contains(num_decls - i - 1)) { used_decl_sorts.push_back(q->get_decl_sort(i)); used_decl_names.push_back(q->get_decl_name(i)); } @@ -79,10 +78,10 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { unsigned num_removed = 0; expr_ref_buffer var_mapping(m); int next_idx = 0; - unsigned sz = used.get_max_found_var_idx_plus_1(); + unsigned sz = m_used.get_max_found_var_idx_plus_1(); for (unsigned i = 0; i < num_decls; ++i) { - sort * s = used.contains(i); + sort * s = m_used.contains(i); if (s) { var_mapping.push_back(m.mk_var(next_idx, s)); next_idx++; @@ -95,7 +94,7 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { // (VAR 0) is in the first position of var_mapping. for (unsigned i = num_decls; i < sz; i++) { - sort * s = used.contains(i); + sort * s = m_used.contains(i); if (s) var_mapping.push_back(m.mk_var(i - num_removed, s)); else @@ -110,9 +109,8 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { std::reverse(var_mapping.c_ptr(), var_mapping.c_ptr() + var_mapping.size()); expr_ref new_expr(m); - var_subst subst(m); - subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr); + m_subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr); if (num_removed == num_decls) { result = new_expr; @@ -124,11 +122,11 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { expr_ref_buffer new_no_patterns(m); for (unsigned i = 0; i < num_patterns; i++) { - subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp); + m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp); new_patterns.push_back(tmp); } for (unsigned i = 0; i < num_no_patterns; i++) { - subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp); + m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp); new_no_patterns.push_back(tmp); } @@ -145,7 +143,12 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { num_no_patterns, new_no_patterns.c_ptr()); to_quantifier(result)->set_no_unused_vars(); - SASSERT(is_well_sorted(m, result)); + SASSERT(is_well_sorted(m, result)); +} + +void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { + unused_vars_eliminator el(m); + el(q, result); } void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref & result) { @@ -161,9 +164,7 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";); } -static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector& sorts) { - ast_mark mark; - ptr_vector todo; +static void get_free_vars_offset(ast_mark& mark, ptr_vector& todo, unsigned offset, expr* e, ptr_vector& sorts) { todo.push_back(e); while (!todo.empty()) { e = todo.back(); @@ -175,7 +176,9 @@ static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector& sor switch(e->get_kind()) { case AST_QUANTIFIER: { quantifier* q = to_quantifier(e); - get_free_vars_offset(q->get_expr(), offset+q->get_num_decls(), sorts); + ast_mark mark1; + ptr_vector todo1; + get_free_vars_offset(mark1, todo1, offset+q->get_num_decls(), q->get_expr(), sorts); break; } case AST_VAR: { @@ -207,5 +210,11 @@ static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector& sor void get_free_vars(expr* e, ptr_vector& sorts) { - get_free_vars_offset(e, 0, sorts); + ast_mark mark; + ptr_vector todo; + get_free_vars_offset(mark, todo, 0, e, sorts); +} + +void get_free_vars(ast_mark& mark, ptr_vector& todo, expr* e, ptr_vector& sorts) { + get_free_vars_offset(mark, todo, 0, e, sorts); } diff --git a/src/ast/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h index 9f3c13c0c..ffc21e691 100644 --- a/src/ast/rewriter/var_subst.h +++ b/src/ast/rewriter/var_subst.h @@ -20,6 +20,7 @@ Notes: #define _VAR_SUBST_H_ #include"rewriter.h" +#include"used_vars.h" /** \brief Alias for var_shifter class. @@ -53,6 +54,15 @@ public: /** \brief Eliminate the unused variables from \c q. Store the result in \c r. */ +class unused_vars_eliminator { + ast_manager& m; + var_subst m_subst; + used_vars m_used; +public: + unused_vars_eliminator(ast_manager& m): m(m), m_subst(m) {} + void operator()(quantifier* q, expr_ref& r); +}; + void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & r); /** @@ -73,6 +83,8 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref */ void get_free_vars(expr* e, ptr_vector& sorts); +void get_free_vars(ast_mark& mark, ptr_vector& todo, expr* e, ptr_vector& sorts); + #endif diff --git a/src/muz_qe/clp_context.cpp b/src/muz_qe/clp_context.cpp new file mode 100644 index 000000000..25ea1455b --- /dev/null +++ b/src/muz_qe/clp_context.cpp @@ -0,0 +1,226 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + clp_context.cpp + +Abstract: + + Bounded CLP (symbolic simulation using Z3) context. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-26 + +Revision History: + +--*/ + +#include "clp_context.h" +#include "dl_context.h" +#include "unifier.h" +#include "var_subst.h" +#include "substitution.h" + +namespace datalog { + + class clp::imp { + struct stats { + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + unsigned m_num_unfold; + unsigned m_num_no_unfold; + unsigned m_num_subsumed; + }; + + context& m_ctx; + ast_manager& m; + rule_manager& rm; + smt_params m_fparams; + smt::kernel m_solver; + var_subst m_var_subst; + expr_ref_vector m_ground; + app_ref_vector m_goals; + volatile bool m_cancel; + stats m_stats; + public: + imp(context& ctx): + m_ctx(ctx), + m(ctx.get_manager()), + rm(ctx.get_rule_manager()), + m_solver(m, m_fparams), // TBD: can be replaced by efficient BV solver. + m_var_subst(m, false), + m_ground(m), + m_goals(m), + m_cancel(false) + { + // m_fparams.m_relevancy_lvl = 0; + m_fparams.m_mbqi = false; + m_fparams.m_soft_timeout = 1000; + } + + ~imp() {} + + lbool query(expr* query) { + m_ctx.ensure_opened(); + m_solver.reset(); + m_goals.reset(); + rm.mk_query(query, m_ctx.get_rules()); + expr_ref head(m); + head = m_ctx.get_rules().last()->get_head(); + ground(head); + m_goals.push_back(to_app(head)); + return search(20, 0); + } + + void cancel() { + m_cancel = true; + m_solver.cancel(); + } + + void cleanup() { + m_cancel = false; + m_goals.reset(); + m_solver.reset_cancel(); + } + + void reset_statistics() { + m_stats.reset(); + } + + void collect_statistics(statistics& st) const { + //st.update("tab.num_unfold", m_stats.m_num_unfold); + //st.update("tab.num_unfold_fail", m_stats.m_num_no_unfold); + //st.update("tab.num_subsumed", m_stats.m_num_subsumed); + } + + void display_certificate(std::ostream& out) const { + expr_ref ans = get_answer(); + out << mk_pp(ans, m) << "\n"; + + } + + expr_ref get_answer() const { + return expr_ref(m.mk_true(), m); + } + + private: + + void reset_ground() { + m_ground.reset(); + } + + void ground(expr_ref& e) { + ptr_vector sorts; + get_free_vars(e, sorts); + if (m_ground.size() < sorts.size()) { + m_ground.resize(sorts.size()); + } + for (unsigned i = 0; i < sorts.size(); ++i) { + if (sorts[i] && !m_ground[i].get()) { + m_ground[i] = m.mk_fresh_const("c",sorts[i]); + } + } + m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e); + } + + lbool search(unsigned depth, unsigned index) { + if (index == m_goals.size()) { + return l_true; + } + if (depth == 0) { + return l_undef; + } + IF_VERBOSE(1, verbose_stream() << "search " << depth << " " << index << "\n";); + unsigned num_goals = m_goals.size(); + app* head = m_goals[index].get(); + rule_vector const& rules = m_ctx.get_rules().get_predicate_rules(head->get_decl()); + lbool status = l_false; + for (unsigned i = 0; i < rules.size(); ++i) { + rule* r = rules[i]; + m_solver.push(); + reset_ground(); + expr_ref tmp(m); + tmp = r->get_head(); + IF_VERBOSE(2, verbose_stream() << index << " " << mk_pp(tmp, m) << "\n";); + ground(tmp); + for (unsigned j = 0; j < head->get_num_args(); ++j) { + expr_ref eq(m); + eq = m.mk_eq(head->get_arg(j), to_app(tmp)->get_arg(j)); + m_solver.assert_expr(eq); + } + for (unsigned j = r->get_uninterpreted_tail_size(); j < r->get_tail_size(); ++j) { + tmp = r->get_tail(j); + ground(tmp); + m_solver.assert_expr(tmp); + } + lbool is_sat = m_solver.check(); + switch (is_sat) { + case l_false: + break; + case l_true: + if (depth == 1 && (index+1 > m_goals.size() || r->get_uninterpreted_tail_size() > 0)) { + status = l_undef; + break; + } + for (unsigned j = 0; j < r->get_uninterpreted_tail_size(); ++j) { + tmp = r->get_tail(j); + ground(tmp); + m_goals.push_back(to_app(tmp)); + } + switch(search(depth-1, index+1)) { + case l_undef: + status = l_undef; + // fallthrough + case l_false: + m_goals.resize(num_goals); + break; + case l_true: + return l_true; + } + break; + case l_undef: + status = l_undef; + throw default_exception("undef"); + } + m_solver.pop(1); + } + return status; + } + + + proof_ref get_proof() const { + return proof_ref(0, m); + } + }; + + clp::clp(context& ctx): + m_imp(alloc(imp, ctx)) { + } + clp::~clp() { + dealloc(m_imp); + } + lbool clp::query(expr* query) { + return m_imp->query(query); + } + void clp::cancel() { + m_imp->cancel(); + } + void clp::cleanup() { + m_imp->cleanup(); + } + void clp::reset_statistics() { + m_imp->reset_statistics(); + } + void clp::collect_statistics(statistics& st) const { + m_imp->collect_statistics(st); + } + void clp::display_certificate(std::ostream& out) const { + m_imp->display_certificate(out); + } + expr_ref clp::get_answer() { + return m_imp->get_answer(); + } + +}; diff --git a/src/muz_qe/clp_context.h b/src/muz_qe/clp_context.h new file mode 100644 index 000000000..635891205 --- /dev/null +++ b/src/muz_qe/clp_context.h @@ -0,0 +1,45 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + clp_context.h + +Abstract: + + Bounded CLP (symbolic simulation using Z3) context. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-26 + +Revision History: + +--*/ +#ifndef _CLP_CONTEXT_H_ +#define _CLP_CONTEXT_H_ + +#include "ast.h" +#include "lbool.h" +#include "statistics.h" + +namespace datalog { + class context; + + class clp { + class imp; + imp* m_imp; + public: + clp(context& ctx); + ~clp(); + lbool query(expr* query); + void cancel(); + void cleanup(); + void reset_statistics(); + void collect_statistics(statistics& st) const; + void display_certificate(std::ostream& out) const; + expr_ref get_answer(); + }; +}; + +#endif diff --git a/src/muz_qe/dl_base.h b/src/muz_qe/dl_base.h index e7243cb70..491bb261d 100644 --- a/src/muz_qe/dl_base.h +++ b/src/muz_qe/dl_base.h @@ -656,6 +656,7 @@ namespace datalog { typedef sort * relation_sort; typedef ptr_vector relation_signature_base0; + typedef ptr_hash relation_sort_hash; typedef app * relation_element; typedef app_ref relation_element_ref; @@ -739,8 +740,8 @@ namespace datalog { struct hash { unsigned operator()(relation_signature const& s) const { - relation_sort const* sorts = s.c_ptr(); - return string_hash(reinterpret_cast(sorts), sizeof(*sorts)*s.size(), 12); } + return obj_vector_hash(s); + } }; struct eq { @@ -816,9 +817,11 @@ namespace datalog { typedef uint64 table_sort; typedef svector table_signature_base0; + typedef uint64_hash table_sort_hash; typedef uint64 table_element; typedef svector table_fact; + typedef uint64_hash table_element_hash; struct table_traits { typedef table_plugin plugin; @@ -881,8 +884,8 @@ namespace datalog { public: struct hash { unsigned operator()(table_signature const& s) const { - table_sort const* sorts = s.c_ptr(); - return string_hash(reinterpret_cast(sorts), sizeof(*sorts)*s.size(), 12); } + return svector_hash()(s); + } }; struct eq { diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index 15876b631..c313f7d7b 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -1004,7 +1004,6 @@ namespace datalog { symbol is_name(_name.str().c_str()); std::stringstream _name2; _name2 << "get_succ#" << i; - symbol acc_name(_name2.str().c_str()); ptr_vector accs; type_ref tr(0); accs.push_back(mk_accessor_decl(name, tr)); diff --git a/src/muz_qe/dl_check_table.h b/src/muz_qe/dl_check_table.h index 7126bde66..40a3d5207 100644 --- a/src/muz_qe/dl_check_table.h +++ b/src/muz_qe/dl_check_table.h @@ -89,15 +89,6 @@ namespace datalog { class check_table : public table_base { friend class check_table_plugin; - friend class check_table_plugin::join_fn; - friend class check_table_plugin::union_fn; - friend class check_table_plugin::transformer_fn; - friend class check_table_plugin::rename_fn; - friend class check_table_plugin::project_fn; - friend class check_table_plugin::filter_equal_fn; - friend class check_table_plugin::filter_identical_fn; - friend class check_table_plugin::filter_interpreted_fn; - friend class check_table_plugin::filter_by_negation_fn; table_base* m_checker; table_base* m_tocheck; diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 80b9dee5a..57d9880c0 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -36,7 +36,7 @@ namespace datalog { } void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) { - pred2idx::entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX); + pred2idx::obj_map_entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX); if(e->get_data().m_value!=UINT_MAX) { //predicate is already loaded return; @@ -421,6 +421,7 @@ namespace datalog { void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, reg_idx delta_reg, bool use_widening, instruction_block & acc) { + ast_manager & m = m_context.get_manager(); m_instruction_observer.start_rule(r); const app * h = r->get_head(); @@ -433,7 +434,7 @@ namespace datalog { SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin reg_idx single_res; - ptr_vector single_res_expr; + expr_ref_vector single_res_expr(m); //used to save on filter_identical instructions where the check is already done //by the join operation @@ -536,7 +537,7 @@ namespace datalog { unsigned srlen=single_res_expr.size(); SASSERT((single_res==execution_context::void_register) ? (srlen==0) : (srlen==m_reg_signatures[single_res].size())); for(unsigned i=0; iget_tail_size(); //full tail for(unsigned tail_index=ut_len; tail_indexget_tail(tail_index); - var_idx_set t_vars; - ast_manager & m = m_context.get_manager(); - collect_vars(m, t, t_vars); - + ptr_vector t_vars; + ::get_free_vars(t, t_vars); + if(t_vars.empty()) { expr_ref simplified(m); m_context.get_rewriter()(t, simplified); @@ -639,40 +639,23 @@ namespace datalog { } //determine binding size - unsigned max_var=0; - var_idx_set::iterator vit = t_vars.begin(); - var_idx_set::iterator vend = t_vars.end(); - for(; vit!=vend; ++vit) { - unsigned v = *vit; - if(v>max_var) { max_var = v; } + while (!t_vars.back()) { + t_vars.pop_back(); } + unsigned max_var = t_vars.size(); //create binding expr_ref_vector binding(m); binding.resize(max_var+1); - vit = t_vars.begin(); - for(; vit!=vend; ++vit) { - unsigned v = *vit; + + for(unsigned v = 0; v < t_vars.size(); ++v) { + if (!t_vars[v]) { + continue; + } int2ints::entry * e = var_indexes.find_core(v); if(!e) { //we have an unbound variable, so we add an unbound column for it - relation_sort unbound_sort = 0; - - for(unsigned hindex = 0; hindexget_arg(hindex); - if(!is_var(harg) || to_var(harg)->get_idx()!=v) { - continue; - } - unbound_sort = to_var(harg)->get_sort(); - } - if(!unbound_sort) { - // the variable in the interpreted tail is neither bound in the - // uninterpreted tail nor present in the head - std::stringstream sstm; - sstm << "rule with unbound variable #" << v << " in interpreted tail: "; - r->display(m_context, sstm); - throw default_exception(sstm.str()); - } + relation_sort unbound_sort = t_vars[v]; reg_idx new_reg; TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";); @@ -759,7 +742,7 @@ namespace datalog { m_instruction_observer.finish_rule(); } - void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, ptr_vector& single_res_expr, + void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, bool & dealloc, instruction_block & acc) { uint_set pos_vars; u_map neg_vars; @@ -782,7 +765,7 @@ namespace datalog { } // populate positive variables: for (unsigned i = 0; i < single_res_expr.size(); ++i) { - expr* e = single_res_expr[i]; + expr* e = single_res_expr[i].get(); if (is_var(e)) { pos_vars.insert(to_var(e)->get_idx()); } @@ -849,19 +832,19 @@ namespace datalog { typedef rule_dependencies::item_set item_set; //set of T rule_dependencies & m_deps; - rule_set const& m_rules; - context& m_context; item_set & m_removed; svector m_stack; + ast_mark m_stack_content; ast_mark m_visited; void traverse(T v) { - SASSERT(!m_visited.is_marked(v)); - if (m_removed.contains(v)) { + SASSERT(!m_stack_content.is_marked(v)); + if(m_visited.is_marked(v) || m_removed.contains(v)) { return; } m_stack.push_back(v); + m_stack_content.mark(v, true); m_visited.mark(v, true); const item_set & deps = m_deps.get_deps(v); @@ -869,49 +852,22 @@ namespace datalog { item_set::iterator end = deps.end(); for(; it!=end; ++it) { T d = *it; - if (m_visited.is_marked(d)) { + if(m_stack_content.is_marked(d)) { //TODO: find the best vertex to remove in the cycle - remove_from_stack(); - continue; + m_removed.insert(v); + break; } traverse(d); } SASSERT(m_stack.back()==v); m_stack.pop_back(); - m_visited.mark(v, false); - } - - void remove_from_stack() { - for (unsigned i = 0; i < m_stack.size(); ++i) { - func_decl* p = m_stack[i]; - if (m_context.has_facts(p)) { - m_removed.insert(p); - return; - } - - rule_vector const& rules = m_rules.get_predicate_rules(p); - unsigned stratum = m_rules.get_predicate_strat(p); - for (unsigned j = 0; j < rules.size(); ++j) { - rule const& r = *rules[j]; - bool ok = true; - for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) { - ok = m_rules.get_predicate_strat(r.get_decl(k)) < stratum; - } - if (ok) { - m_removed.insert(p); - return; - } - } - } - - // nothing was found. - m_removed.insert(m_stack.back()); + m_stack_content.mark(v, false); } public: - cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed) - : m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); } + cycle_breaker(rule_dependencies & deps, item_set & removed) + : m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); } void operator()() { rule_dependencies::iterator it = m_deps.begin(); @@ -933,7 +889,7 @@ namespace datalog { rule_dependencies deps(m_rule_set.get_dependencies()); deps.restrict(preds); - cycle_breaker(deps, m_rule_set, m_context, global_deltas)(); + cycle_breaker(deps, global_deltas)(); VERIFY( deps.sort_deps(ordered_preds) ); //the predicates that were removed to get acyclic induced subgraph are put last @@ -1069,12 +1025,17 @@ namespace datalog { } func_decl_vector preds_vector; - func_decl_set global_deltas; + func_decl_set global_deltas_dummy; - detect_chains(head_preds, preds_vector, global_deltas); + detect_chains(head_preds, preds_vector, global_deltas_dummy); + /* + FIXME: right now we use all preds as global deltas for correctness purposes func_decl_set local_deltas(head_preds); set_difference(local_deltas, global_deltas); + */ + func_decl_set local_deltas; + func_decl_set global_deltas(head_preds); pred2idx d_global_src; //these deltas serve as sources of tuples for rule evaluation inside the loop get_fresh_registers(global_deltas, d_global_src); diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h index 1dfb7c7d8..78b4623de 100644 --- a/src/muz_qe/dl_compiler.h +++ b/src/muz_qe/dl_compiler.h @@ -41,7 +41,7 @@ namespace datalog { typedef hashtable int_set; typedef u_map int2int; typedef u_map int2ints; - typedef map,ptr_eq > pred2idx; + typedef obj_map pred2idx; typedef unsigned_vector var_vector; typedef ptr_vector func_decl_vector; @@ -177,7 +177,7 @@ namespace datalog { void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, instruction_block & acc); - void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, ptr_vector& single_res_expr, + void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, bool & dealloc, instruction_block& acc); void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, instruction_block & acc); diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index df293aeba..dfcaac791 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -41,7 +41,6 @@ Revision History: #include"for_each_expr.h" #include"ast_smt_pp.h" #include"ast_smt2_pp.h" -#include"expr_functors.h" #include"dl_mk_partial_equiv.h" #include"dl_mk_bit_blast.h" #include"dl_mk_array_blast.h" @@ -49,7 +48,6 @@ Revision History: #include"dl_mk_quantifier_abstraction.h" #include"dl_mk_quantifier_instantiation.h" #include"datatype_decl_plugin.h" -#include"expr_abstract.h" namespace datalog { @@ -226,6 +224,10 @@ namespace datalog { m_rewriter(m), m_var_subst(m), m_rule_manager(*this), + m_elim_unused_vars(m), + m_abstractor(m), + m_contains_p(*this), + m_check_pred(m_contains_p, m), m_transf(*this), m_trail(*this), m_pinned(m), @@ -301,18 +303,19 @@ namespace datalog { expr_ref context::bind_variables(expr* fml, bool is_forall) { expr_ref result(m); app_ref_vector const & vars = m_vars; + rule_manager& rm = get_rule_manager(); if (vars.empty()) { result = fml; } else { - ptr_vector sorts; - expr_abstract(m, 0, vars.size(), reinterpret_cast(vars.c_ptr()), fml, result); - get_free_vars(result, sorts); + m_names.reset(); + m_abstractor(0, vars.size(), reinterpret_cast(vars.c_ptr()), fml, result); + rm.collect_vars(result); + ptr_vector& sorts = rm.get_var_sorts(); if (sorts.empty()) { result = fml; } else { - svector names; for (unsigned i = 0; i < sorts.size(); ++i) { if (!sorts[i]) { if (i < vars.size()) { @@ -323,16 +326,16 @@ namespace datalog { } } if (i < vars.size()) { - names.push_back(vars[i]->get_decl()->get_name()); + m_names.push_back(vars[i]->get_decl()->get_name()); } else { - names.push_back(symbol(i)); + m_names.push_back(symbol(i)); } } quantifier_ref q(m); sorts.reverse(); - q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result); - elim_unused_vars(m, q, result); + q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), m_names.c_ptr(), result); + m_elim_unused_vars(q, result); } } return result; @@ -544,6 +547,8 @@ namespace datalog { throw default_exception("get_num_levels is not supported for bmc"); case TAB_ENGINE: throw default_exception("get_num_levels is not supported for tab"); + case CLP_ENGINE: + throw default_exception("get_num_levels is not supported for clp"); default: throw default_exception("unknown engine"); } @@ -562,6 +567,8 @@ namespace datalog { throw default_exception("operation is not supported for BMC engine"); case TAB_ENGINE: throw default_exception("operation is not supported for TAB engine"); + case CLP_ENGINE: + throw default_exception("operation is not supported for CLP engine"); default: throw default_exception("unknown engine"); } @@ -581,6 +588,8 @@ namespace datalog { throw default_exception("operation is not supported for BMC engine"); case TAB_ENGINE: throw default_exception("operation is not supported for TAB engine"); + case CLP_ENGINE: + throw default_exception("operation is not supported for CLP engine"); default: throw default_exception("unknown engine"); } @@ -607,28 +616,16 @@ namespace datalog { } } - class context::contains_pred : public i_expr_pred { - context const& ctx; - public: - contains_pred(context& ctx): ctx(ctx) {} - virtual ~contains_pred() {} - - virtual bool operator()(expr* e) { - return ctx.is_predicate(e); - } - }; void context::check_existential_tail(rule_ref& r) { unsigned ut_size = r->get_uninterpreted_tail_size(); unsigned t_size = r->get_tail_size(); - contains_pred contains_p(*this); - check_pred check_pred(contains_p, get_manager()); TRACE("dl", r->display_smt2(get_manager(), tout); tout << "\n";); for (unsigned i = ut_size; i < t_size; ++i) { app* t = r->get_tail(i); TRACE("dl", tout << "checking: " << mk_ismt2_pp(t, get_manager()) << "\n";); - if (check_pred(t)) { + if (m_check_pred(t)) { std::ostringstream out; out << "interpreted body " << mk_ismt2_pp(t, get_manager()) << " contains recursive predicate"; throw default_exception(out.str()); @@ -720,6 +717,10 @@ namespace datalog { check_existential_tail(r); check_positive_predicates(r); break; + case CLP_ENGINE: + check_existential_tail(r); + check_positive_predicates(r); + break; default: UNREACHABLE(); break; @@ -813,9 +814,8 @@ namespace datalog { void context::transform_rules() { m_transf.reset(); - if (get_params().filter_rules()) { - m_transf.register_plugin(alloc(mk_filter_rules, *this)); - } + m_transf.register_plugin(alloc(mk_coi_filter, *this)); + m_transf.register_plugin(alloc(mk_filter_rules, *this)); m_transf.register_plugin(alloc(mk_simple_joins, *this)); if (unbound_compressor()) { m_transf.register_plugin(alloc(mk_unbound_compressor, *this)); @@ -823,7 +823,14 @@ namespace datalog { if (similarity_compressor()) { m_transf.register_plugin(alloc(mk_similarity_compressor, *this)); } - m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this)); + m_transf.register_plugin(alloc(mk_partial_equivalence_transformer, *this)); + m_transf.register_plugin(alloc(mk_rule_inliner, *this)); + m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this)); + + if (get_params().bit_blast()) { + m_transf.register_plugin(alloc(mk_bit_blast, *this, 22000)); + m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this, 21000)); + } transform_rules(m_transf); } @@ -988,6 +995,9 @@ namespace datalog { else if (e == symbol("tab")) { m_engine = TAB_ENGINE; } + else if (e == symbol("clp")) { + m_engine = CLP_ENGINE; + } if (m_engine == LAST_ENGINE) { expr_fast_mark1 mark; @@ -1023,6 +1033,8 @@ namespace datalog { return bmc_query(query); case TAB_ENGINE: return tab_query(query); + case CLP_ENGINE: + return clp_query(query); default: UNREACHABLE(); return rel_query(query); @@ -1087,11 +1099,22 @@ namespace datalog { } } + void context::ensure_clp() { + if (!m_clp.get()) { + m_clp = alloc(clp, *this); + } + } + lbool context::tab_query(expr* query) { ensure_tab(); return m_tab->query(query); } + lbool context::clp_query(expr* query) { + ensure_clp(); + return m_clp->query(query); + } + void context::ensure_rel() { if (!m_rel.get()) { m_rel = alloc(rel_context, *this); @@ -1132,6 +1155,10 @@ namespace datalog { ensure_tab(); m_last_answer = m_tab->get_answer(); return m_last_answer.get(); + case CLP_ENGINE: + ensure_clp(); + m_last_answer = m_clp->get_answer(); + return m_last_answer.get(); default: UNREACHABLE(); } @@ -1157,6 +1184,10 @@ namespace datalog { ensure_tab(); m_tab->display_certificate(out); return true; + case CLP_ENGINE: + ensure_clp(); + m_clp->display_certificate(out); + return true; default: return false; } diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 74449940c..0a01b3e01 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -45,6 +45,9 @@ Revision History: #include"model2expr.h" #include"smt_params.h" #include"dl_rule_transformer.h" +#include"expr_abstract.h" +#include"expr_functors.h" +#include"clp_context.h" namespace datalog { @@ -76,6 +79,18 @@ namespace datalog { typedef obj_map > pred2syms; typedef obj_map sort_domain_map; + class contains_pred : public i_expr_pred { + context const& ctx; + public: + contains_pred(context& ctx): ctx(ctx) {} + virtual ~contains_pred() {} + + virtual bool operator()(expr* e) { + return ctx.is_predicate(e); + } + }; + + ast_manager & m; smt_params & m_fparams; params_ref m_params_ref; @@ -84,10 +99,15 @@ namespace datalog { th_rewriter m_rewriter; var_subst m_var_subst; rule_manager m_rule_manager; + unused_vars_eliminator m_elim_unused_vars; + expr_abstractor m_abstractor; + contains_pred m_contains_p; + check_pred m_check_pred; rule_transformer m_transf; trail_stack m_trail; ast_ref_vector m_pinned; app_ref_vector m_vars; + svector m_names; sort_domain_map m_sorts; func_decl_set m_preds; sym2decl m_preds_by_name; @@ -104,6 +124,7 @@ namespace datalog { scoped_ptr m_bmc; scoped_ptr m_rel; scoped_ptr m_tab; + scoped_ptr m_clp; bool m_closed; bool m_saturation_was_run; @@ -457,6 +478,8 @@ namespace datalog { void ensure_tab(); + void ensure_clp(); + void ensure_rel(); void new_query(); @@ -469,6 +492,8 @@ namespace datalog { lbool tab_query(expr* query); + lbool clp_query(expr* query); + void check_quantifier_free(rule_ref& r); void check_uninterpreted_free(rule_ref& r); void check_existential_tail(rule_ref& r); diff --git a/src/muz_qe/dl_finite_product_relation.cpp b/src/muz_qe/dl_finite_product_relation.cpp index 4880e6068..86fef433b 100644 --- a/src/muz_qe/dl_finite_product_relation.cpp +++ b/src/muz_qe/dl_finite_product_relation.cpp @@ -1291,8 +1291,8 @@ namespace datalog { m_renaming_for_inner_rel(m_manager) { relation_manager & rmgr = r.get_manager(); - idx_set cond_columns; - collect_vars(m_manager, m_cond, cond_columns); + rule_manager& rm = r.get_context().get_rule_manager(); + idx_set& cond_columns = rm.collect_vars(m_cond); unsigned sig_sz = r.get_signature().size(); for(unsigned i=0; i()(o.m_table_cols); } }; }; diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index 296fa95f3..b103d743e 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -359,21 +359,7 @@ namespace datalog { r2.get_signature().output(ctx.get_rel_context().get_manager(), tout); tout<<":"<\n";); - try { - ctx.set_reg(m_res, (*fn)(r1, r2)); - } - catch(...) - { - std::string annotation; - unsigned sz; - ctx.get_register_annotation(m_rel1, annotation); - sz = ctx.reg(m_rel1)?ctx.reg(m_rel1)->get_size_estimate_rows():0; - std::cout << m_rel1 << "\t" << sz << "\t" << annotation << "\n"; - ctx.get_register_annotation(m_rel2, annotation); - sz = ctx.reg(m_rel2)?ctx.reg(m_rel2)->get_size_estimate_rows():0; - std::cout << m_rel2 << "\t" << sz << "\t" << annotation << "\n"; - throw; - } + ctx.set_reg(m_res, (*fn)(r1, r2)); TRACE("dl", ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout); diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index f0fdc6ab2..c1f0912c0 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -145,7 +145,6 @@ namespace datalog { expr_ref_vector conjs(m), new_conjs(m); expr_ref tmp(m); expr_safe_replace sub(m); - uint_set lhs_vars, rhs_vars; bool change = false; bool inserted = false; @@ -161,10 +160,8 @@ namespace datalog { if (is_store_def(e, x, y)) { // enforce topological order consistency: - uint_set lhs; - collect_vars(m, x, lhs_vars); - collect_vars(m, y, rhs_vars); - lhs = lhs_vars; + uint_set lhs = rm.collect_vars(x); + uint_set rhs_vars = rm.collect_vars(y); lhs &= rhs_vars; if (!lhs.empty()) { TRACE("dl", tout << "unusable equality " << mk_pp(e, m) << "\n";); diff --git a/src/muz_qe/dl_mk_backwards.cpp b/src/muz_qe/dl_mk_backwards.cpp new file mode 100644 index 000000000..b1d8b7d36 --- /dev/null +++ b/src/muz_qe/dl_mk_backwards.cpp @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_backwards.cpp + +Abstract: + + Create Horn clauses for backwards flow. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-17 + +Revision History: + +--*/ + +#include"dl_mk_backwards.h" +#include"dl_context.h" + +namespace datalog { + + mk_backwards::mk_backwards(context & ctx, unsigned priority): + plugin(priority), + m(ctx.get_manager()), + m_ctx(ctx) { + } + + mk_backwards::~mk_backwards() { } + + rule_set * mk_backwards::operator()(rule_set const & source) { + 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; + app_ref query(m); + query = m.mk_fresh_const("Q", m.mk_bool_sort()); + result->set_output_predicate(query->get_decl()); + m_ctx.register_predicate(query->get_decl(), false); + for (unsigned i = 0; i < sz; ++i) { + tail.reset(); + neg.reset(); + rule & r = *source.get_rule(i); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + if (!source.is_output_predicate(r.get_decl())) { + tail.push_back(r.get_head()); + neg.push_back(false); + } + for (unsigned j = utsz; j < tsz; ++j) { + tail.push_back(r.get_tail(j)); + neg.push_back(false); + } + for (unsigned j = 0; j <= utsz; ++j) { + if (j == utsz && j > 0) { + break; + } + if (j == utsz) { + head = query; + } + else { + head = r.get_tail(j); + } + new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); + result->add_rule(new_rule); + } + } + TRACE("dl", result->display(tout);); + return result; + } + +}; diff --git a/src/muz_qe/dl_mk_backwards.h b/src/muz_qe/dl_mk_backwards.h new file mode 100644 index 000000000..4e546c848 --- /dev/null +++ b/src/muz_qe/dl_mk_backwards.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_backwards.h + +Abstract: + + Create Horn clauses for backwards flow. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-17 + +Revision History: + +--*/ +#ifndef _DL_MK_BACKWARDS_H_ +#define _DL_MK_BACKWARDS_H_ + +#include"dl_rule_transformer.h" + +namespace datalog { + + class mk_backwards : public rule_transformer::plugin { + ast_manager& m; + context& m_ctx; + public: + mk_backwards(context & ctx, unsigned priority = 33000); + ~mk_backwards(); + rule_set * operator()(rule_set const & source); + }; + +}; + +#endif /* _DL_MK_BACKWARDS_H_ */ + diff --git a/src/muz_qe/dl_mk_filter_rules.cpp b/src/muz_qe/dl_mk_filter_rules.cpp index 8ab8412c0..ef89c9ffa 100644 --- a/src/muz_qe/dl_mk_filter_rules.cpp +++ b/src/muz_qe/dl_mk_filter_rules.cpp @@ -27,9 +27,10 @@ namespace datalog { mk_filter_rules::mk_filter_rules(context & ctx): plugin(2000), m_context(ctx), - m_manager(ctx.get_manager()), + m(ctx.get_manager()), + rm(ctx.get_rule_manager()), m_result(0), - m_pinned(m_manager) { + m_pinned(m) { } mk_filter_rules::~mk_filter_rules() { @@ -52,14 +53,14 @@ namespace datalog { */ bool mk_filter_rules::is_candidate(app * pred) { if (!m_context.is_predicate(pred)) { - TRACE("mk_filter_rules", tout << mk_pp(pred, m_manager) << "\nis not a candidate because it is interpreted.\n";); + TRACE("mk_filter_rules", tout << mk_pp(pred, m) << "\nis not a candidate because it is interpreted.\n";); return false; } var_idx_set used_vars; unsigned n = pred->get_num_args(); for (unsigned i = 0; i < n; i++) { expr * arg = pred->get_arg(i); - if (m_manager.is_value(arg)) + if (m.is_value(arg)) return true; SASSERT(is_var(arg)); unsigned vidx = to_var(arg)->get_idx(); @@ -74,10 +75,10 @@ namespace datalog { \brief Create a "filter" (if it doesn't exist already) for the given predicate. */ func_decl * mk_filter_rules::mk_filter_decl(app * pred, var_idx_set const & non_local_vars) { - sort_ref_buffer filter_domain(m_manager); + sort_ref_buffer filter_domain(m); - filter_key * key = alloc(filter_key, m_manager); - mk_new_rule_tail(m_manager, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred); + filter_key * key = alloc(filter_key, m); + mk_new_rule_tail(m, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred); func_decl * filter_decl = 0; if (!m_tail2filter.find(key, filter_decl)) { filter_decl = m_context.mk_fresh_head_predicate(pred->get_decl()->get_name(), symbol("filter"), @@ -85,8 +86,8 @@ namespace datalog { m_pinned.push_back(filter_decl); m_tail2filter.insert(key, filter_decl); - app_ref filter_head(m_manager); - filter_head = m_manager.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr()); + app_ref filter_head(m); + filter_head = m.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr()); app * filter_tail = key->new_pred; rule * filter_rule = m_context.get_rule_manager().mk(filter_head, 1, &filter_tail, (const bool *)0); filter_rule->set_accounting_parent_object(m_context, m_current); @@ -104,16 +105,15 @@ namespace datalog { void mk_filter_rules::process(rule * r) { m_current = r; app * new_head = r->get_head(); - app_ref_vector new_tail(m_manager); + app_ref_vector new_tail(m); svector new_is_negated; unsigned sz = r->get_tail_size(); bool rule_modified = false; for (unsigned i = 0; i < sz; i++) { app * tail = r->get_tail(i); if (is_candidate(tail)) { - TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m_manager) << "\n";); - var_idx_set non_local_vars; - collect_non_local_vars(m_manager, r, tail, non_local_vars); + TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m) << "\n";); + var_idx_set non_local_vars = rm.collect_rule_vars_ex(r, tail); func_decl * filter_decl = mk_filter_decl(tail, non_local_vars); ptr_buffer new_args; var_idx_set used_vars; @@ -129,7 +129,7 @@ namespace datalog { } } SASSERT(new_args.size() == filter_decl->get_arity()); - new_tail.push_back(m_manager.mk_app(filter_decl, new_args.size(), new_args.c_ptr())); + new_tail.push_back(m.mk_app(filter_decl, new_args.size(), new_args.c_ptr())); rule_modified = true; } else { @@ -152,9 +152,6 @@ namespace datalog { } rule_set * mk_filter_rules::operator()(rule_set const & source) { - if (!m_context.get_params().filter_rules()) { - return 0; - } m_tail2filter.reset(); m_result = alloc(rule_set, m_context); m_modified = false; diff --git a/src/muz_qe/dl_mk_filter_rules.h b/src/muz_qe/dl_mk_filter_rules.h index 4a247fdb5..b51cb8e24 100644 --- a/src/muz_qe/dl_mk_filter_rules.h +++ b/src/muz_qe/dl_mk_filter_rules.h @@ -45,17 +45,22 @@ namespace datalog { filter_key(ast_manager & m) : new_pred(m), filter_args(m) {} unsigned hash() const { - return new_pred->hash() ^ int_vector_hash(filter_args); + unsigned r = new_pred->hash(); + for (unsigned i = 0; i < filter_args.size(); ++i) { + r ^= filter_args[i]->hash(); + } + return r; } bool operator==(const filter_key & o) const { return o.new_pred==new_pred && vectors_equal(o.filter_args, filter_args); } }; - typedef map, deref_eq > filter_cache; + typedef obj_map filter_cache; context & m_context; - ast_manager & m_manager; + ast_manager & m; + rule_manager & rm; filter_cache m_tail2filter; rule_set * m_result; rule * m_current; diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp index d0b94f582..afd586627 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp @@ -67,24 +67,23 @@ namespace datalog { void mk_interp_tail_simplifier::rule_substitution::get_result(rule_ref & res) { SASSERT(m_rule); - app_ref new_head(m); - apply(m_rule->get_head(), new_head); + apply(m_rule->get_head(), m_head); - app_ref_vector tail(m); - svector tail_neg; + m_tail.reset(); + m_neg.reset(); unsigned tail_len = m_rule->get_tail_size(); for (unsigned i=0; iget_tail(i), new_tail_el); - tail.push_back(new_tail_el); - tail_neg.push_back(m_rule->is_neg_tail(i)); + m_tail.push_back(new_tail_el); + m_neg.push_back(m_rule->is_neg_tail(i)); } - mk_rule_inliner::remove_duplicate_tails(tail, tail_neg); + mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg); - SASSERT(tail.size() == tail_neg.size()); - res = m_context.get_rule_manager().mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); + SASSERT(m_tail.size() == m_neg.size()); + res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr()); res->set_accounting_parent_object(m_context, m_rule); res->norm_vars(res.get_manager()); } @@ -362,14 +361,37 @@ namespace datalog { } }; + class mk_interp_tail_simplifier::normalizer_rw : public rewriter_tpl { + public: + normalizer_rw(ast_manager& m, normalizer_cfg& cfg): rewriter_tpl(m, false, cfg) {} + }; + + + mk_interp_tail_simplifier::mk_interp_tail_simplifier(context & ctx, unsigned priority) + : plugin(priority), + m(ctx.get_manager()), + m_context(ctx), + m_simp(ctx.get_rewriter()), + a(m), + m_rule_subst(ctx), + m_tail(m), + m_itail_members(m), + m_conj(m) { + m_cfg = alloc(normalizer_cfg, m); + m_rw = alloc(normalizer_rw, m, *m_cfg); + } + + mk_interp_tail_simplifier::~mk_interp_tail_simplifier() { + dealloc(m_rw); + dealloc(m_cfg); + } + + void mk_interp_tail_simplifier::simplify_expr(app * a, expr_ref& res) { expr_ref simp1_res(m); m_simp(a, simp1_res); - normalizer_cfg r_cfg(m); - rewriter_tpl rwr(m, false, r_cfg); - expr_ref dl_form_e(m); - rwr(simp1_res.get(), res); + (*m_rw)(simp1_res.get(), res); /*if (simp1_res.get()!=res.get()) { std::cout<<"pre norm:\n"< todo; + m_todo.reset(); + m_leqs.reset(); for (unsigned i = u_len; i < len; i++) { - todo.push_back(r->get_tail(i)); + m_todo.push_back(r->get_tail(i)); SASSERT(!r->is_neg_tail(i)); } m_rule_subst.reset(r); - obj_hashtable leqs; expr_ref_vector trail(m); expr_ref tmp1(m), tmp2(m); bool found_something = false; @@ -401,10 +423,10 @@ namespace datalog { #define TRY_UNIFY(_x,_y) if (m_rule_subst.unify(_x,_y)) { found_something = true; } #define IS_FLEX(_x) (is_var(_x) || m.is_value(_x)) - while (!todo.empty()) { + while (!m_todo.empty()) { expr * arg1, *arg2; - expr * t0 = todo.back(); - todo.pop_back(); + expr * t0 = m_todo.back(); + m_todo.pop_back(); expr* t = t0; bool neg = m.is_not(t, t); if (is_var(t)) { @@ -412,7 +434,7 @@ namespace datalog { } else if (!neg && m.is_and(t)) { app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); + m_todo.append(a->get_num_args(), a->get_args()); } else if (!neg && m.is_eq(t, arg1, arg2) && IS_FLEX(arg1) && IS_FLEX(arg2)) { TRY_UNIFY(arg1, arg2); @@ -440,12 +462,12 @@ namespace datalog { else if (!neg && (a.is_le(t, arg1, arg2) || a.is_ge(t, arg2, arg1))) { tmp1 = a.mk_sub(arg1, arg2); tmp2 = a.mk_sub(arg2, arg1); - if (false && leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) { + if (false && m_leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) { TRY_UNIFY(arg1, arg2); } else { trail.push_back(tmp1); - leqs.insert(tmp1); + m_leqs.insert(tmp1); } } } @@ -485,12 +507,12 @@ namespace datalog { } app_ref head(r->get_head(), m); - app_ref_vector tail(m); - svector tail_neg; + m_tail.reset(); + m_tail_neg.reset(); for (unsigned i=0; iget_tail(i)); - tail_neg.push_back(r->is_neg_tail(i)); + m_tail.push_back(r->get_tail(i)); + m_tail_neg.push_back(r->is_neg_tail(i)); } bool modified = false; @@ -502,12 +524,12 @@ namespace datalog { SASSERT(!r->is_neg_tail(u_len)); } else { - expr_ref_vector itail_members(m); + m_itail_members.reset(); for (unsigned i=u_len; iget_tail(i)); + m_itail_members.push_back(r->get_tail(i)); SASSERT(!r->is_neg_tail(i)); } - itail = m.mk_and(itail_members.size(), itail_members.c_ptr()); + itail = m.mk_and(m_itail_members.size(), m_itail_members.c_ptr()); modified = true; } @@ -523,21 +545,21 @@ namespace datalog { SASSERT(m.is_bool(simp_res)); if (modified) { - expr_ref_vector conjs(m); - flatten_and(simp_res, conjs); - for (unsigned i = 0; i < conjs.size(); ++i) { - expr* e = conjs[i].get(); + m_conj.reset(); + flatten_and(simp_res, m_conj); + for (unsigned i = 0; i < m_conj.size(); ++i) { + expr* e = m_conj[i].get(); if (is_app(e)) { - tail.push_back(to_app(e)); + m_tail.push_back(to_app(e)); } else { - tail.push_back(m.mk_eq(e, m.mk_true())); + m_tail.push_back(m.mk_eq(e, m.mk_true())); } - tail_neg.push_back(false); + m_tail_neg.push_back(false); } - SASSERT(tail.size() == tail_neg.size()); - res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); + SASSERT(m_tail.size() == m_tail_neg.size()); + res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr()); res->set_accounting_parent_object(m_context, r); } else { diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h index 247b20755..5047e1c6e 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.h +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.h @@ -34,15 +34,17 @@ namespace datalog { { ast_manager& m; context& m_context; - substitution m_subst; - unifier m_unif; - - rule * m_rule; + substitution m_subst; + unifier m_unif; + app_ref m_head; + app_ref_vector m_tail; + svector m_neg; + rule * m_rule; void apply(app * a, app_ref& res); public: rule_substitution(context & ctx) - : m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_rule(0) {} + : m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_head(m), m_tail(m), m_rule(0) {} /** Reset substitution and get it ready for working with rule r. @@ -61,13 +63,23 @@ namespace datalog { } }; + class normalizer_cfg; + class normalizer_rw; + ast_manager & m; context & m_context; th_rewriter & m_simp; arith_util a; rule_substitution m_rule_subst; + ptr_vector m_todo; + obj_hashtable m_leqs; + app_ref_vector m_tail; + expr_ref_vector m_itail_members; + expr_ref_vector m_conj; + svector m_tail_neg; + normalizer_cfg* m_cfg; + normalizer_rw* m_rw; - class normalizer_cfg; void simplify_expr(app * a, expr_ref& res); @@ -77,13 +89,8 @@ namespace datalog { /** Return true if something was modified */ bool transform_rules(const rule_set & orig, rule_set & tgt); public: - mk_interp_tail_simplifier(context & ctx, unsigned priority=40000) - : plugin(priority), - m(ctx.get_manager()), - m_context(ctx), - m_simp(ctx.get_rewriter()), - a(m), - m_rule_subst(ctx) {} + mk_interp_tail_simplifier(context & ctx, unsigned priority=40000); + virtual ~mk_interp_tail_simplifier(); /**If rule should be retained, assign transformed version to res and return true; if rule can be deleted, return false. diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index 9109f1bda..d676c3dd4 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -35,6 +35,8 @@ Revision History: #include"dl_mk_karr_invariants.h" #include"expr_safe_replace.h" #include"bool_rewriter.h" +#include"dl_mk_backwards.h" +#include"dl_mk_loop_counter.h" namespace datalog { @@ -199,6 +201,29 @@ namespace datalog { return 0; } } + + mk_loop_counter lc(m_ctx); + mk_backwards bwd(m_ctx); + + scoped_ptr src_loop = lc(source); + TRACE("dl", src_loop->display(tout << "source loop\n");); + + // run propagation forwards, then backwards + scoped_ptr src_annot = update_using_propagation(*src_loop, *src_loop); + TRACE("dl", src_annot->display(tout << "updated using propagation\n");); + +#if 0 + // figure out whether to update same rules as used for saturation. + scoped_ptr rev_source = bwd(*src_annot); + src_annot = update_using_propagation(*src_annot, *rev_source); +#endif + rule_set* rules = lc.revert(*src_annot); + rules->inherit_predicates(source); + TRACE("dl", rules->display(tout);); + return rules; + } + + rule_set* mk_karr_invariants::update_using_propagation(rule_set const& src, rule_set const& srcref) { m_inner_ctx.reset(); rel_context& rctx = m_inner_ctx.get_rel_context(); ptr_vector heads; @@ -207,24 +232,24 @@ namespace datalog { m_inner_ctx.register_predicate(*fit, false); } m_inner_ctx.ensure_opened(); - m_inner_ctx.replace_rules(source); + m_inner_ctx.replace_rules(srcref); m_inner_ctx.close(); - rule_set::decl2rules::iterator dit = source.begin_grouped_rules(); - rule_set::decl2rules::iterator dend = source.end_grouped_rules(); + rule_set::decl2rules::iterator dit = srcref.begin_grouped_rules(); + rule_set::decl2rules::iterator dend = srcref.end_grouped_rules(); for (; dit != dend; ++dit) { heads.push_back(dit->m_key); } m_inner_ctx.rel_query(heads.size(), heads.c_ptr()); - rule_set* rules = alloc(rule_set, m_ctx); - it = source.begin(); + rule_set* dst = alloc(rule_set, m_ctx); + rule_set::iterator it = src.begin(), end = src.end(); for (; it != end; ++it) { - update_body(rctx, *rules, **it); + update_body(rctx, *dst, **it); } if (m_ctx.get_model_converter()) { add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m); - rule_set::decl2rules::iterator git = source.begin_grouped_rules(); - rule_set::decl2rules::iterator gend = source.end_grouped_rules(); + rule_set::decl2rules::iterator git = src.begin_grouped_rules(); + rule_set::decl2rules::iterator gend = src.end_grouped_rules(); for (; git != gend; ++git) { func_decl* p = git->m_key; expr_ref fml(m); @@ -236,9 +261,9 @@ namespace datalog { } m_ctx.add_model_converter(kmc); } - TRACE("dl", rules->display(tout);); - rules->inherit_predicates(source); - return rules; + + dst->inherit_predicates(src); + return dst; } void mk_karr_invariants::update_body(rel_context& rctx, rule_set& rules, rule& r) { diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h index 414953e4f..330260671 100644 --- a/src/muz_qe/dl_mk_karr_invariants.h +++ b/src/muz_qe/dl_mk_karr_invariants.h @@ -56,7 +56,7 @@ namespace datalog { context m_inner_ctx; arith_util a; void update_body(rel_context& rctx, rule_set& result, rule& r); - + rule_set* update_using_propagation(rule_set const& src, rule_set const& srcref); public: mk_karr_invariants(context & ctx, unsigned priority); diff --git a/src/muz_qe/dl_mk_loop_counter.cpp b/src/muz_qe/dl_mk_loop_counter.cpp index 144826639..678bfc5a3 100644 --- a/src/muz_qe/dl_mk_loop_counter.cpp +++ b/src/muz_qe/dl_mk_loop_counter.cpp @@ -32,7 +32,7 @@ namespace datalog { mk_loop_counter::~mk_loop_counter() { } - app_ref mk_loop_counter::add_arg(app* fn, unsigned idx) { + app_ref mk_loop_counter::add_arg(rule_set const& src, rule_set& dst, app* fn, unsigned idx) { expr_ref_vector args(m); func_decl* new_fn, *old_fn = fn->get_decl(); args.append(fn->get_num_args(), fn->get_args()); @@ -46,17 +46,29 @@ namespace datalog { m_old2new.insert(old_fn, new_fn); m_new2old.insert(new_fn, old_fn); m_refs.push_back(new_fn); + m_ctx.register_predicate(new_fn, false); + if (src.is_output_predicate(old_fn)) { + dst.set_output_predicate(new_fn); + } } return app_ref(m.mk_app(new_fn, args.size(), args.c_ptr()), m); } + + app_ref mk_loop_counter::del_arg(app* fn) { + expr_ref_vector args(m); + func_decl* old_fn, *new_fn = fn->get_decl(); + SASSERT(fn->get_num_args() > 0); + args.append(fn->get_num_args()-1, fn->get_args()); + VERIFY (m_new2old.find(new_fn, old_fn)); + return app_ref(m.mk_app(old_fn, args.size(), args.c_ptr()), m); + } rule_set * mk_loop_counter::operator()(rule_set const & source) { m_refs.reset(); m_old2new.reset(); m_new2old.reset(); - context& ctx = source.get_context(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, ctx); + rule_set * result = alloc(rule_set, m_ctx); unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); app_ref_vector tail(m); @@ -71,16 +83,14 @@ namespace datalog { unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); for (unsigned j = 0; j < utsz; ++j, ++cnt) { - tail.push_back(add_arg(r.get_tail(j), cnt)); + tail.push_back(add_arg(source, *result, r.get_tail(j), cnt)); neg.push_back(r.is_neg_tail(j)); - m_ctx.register_predicate(tail.back()->get_decl(), false); } for (unsigned j = utsz; j < tsz; ++j) { tail.push_back(r.get_tail(j)); neg.push_back(false); } - head = add_arg(r.get_head(), cnt); - m_ctx.register_predicate(head->get_decl(), false); + head = add_arg(source, *result, r.get_head(), cnt); // set the loop counter to be an increment of the previous bool found = false; unsigned last = head->get_num_args()-1; @@ -108,9 +118,41 @@ namespace datalog { // model converter: remove references to extra argument. // proof converter: remove references to extra argument as well. - result->inherit_predicates(source); - return result; } + rule_set * mk_loop_counter::revert(rule_set const & source) { + 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; + for (unsigned i = 0; i < sz; ++i) { + tail.reset(); + neg.reset(); + rule & r = *source.get_rule(i); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + for (unsigned j = 0; j < utsz; ++j) { + tail.push_back(del_arg(r.get_tail(j))); + neg.push_back(r.is_neg_tail(j)); + } + for (unsigned j = utsz; j < tsz; ++j) { + tail.push_back(r.get_tail(j)); + neg.push_back(false); + } + head = del_arg(r.get_head()); + new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); + result->add_rule(new_rule); + } + + // model converter: ... + // proof converter: ... + + return result; + + } }; diff --git a/src/muz_qe/dl_mk_loop_counter.h b/src/muz_qe/dl_mk_loop_counter.h index fc4d7e32f..d67c88e0e 100644 --- a/src/muz_qe/dl_mk_loop_counter.h +++ b/src/muz_qe/dl_mk_loop_counter.h @@ -32,7 +32,8 @@ namespace datalog { obj_map m_new2old; obj_map m_old2new; - app_ref add_arg(app* fn, unsigned idx); + app_ref add_arg(rule_set const& src, rule_set& dst, app* fn, unsigned idx); + app_ref del_arg(app* fn); public: mk_loop_counter(context & ctx, unsigned priority = 33000); ~mk_loop_counter(); @@ -40,6 +41,8 @@ namespace datalog { rule_set * operator()(rule_set const & source); func_decl* get_old(func_decl* f) const { return m_new2old.find(f); } + + rule_set * revert(rule_set const& source); }; }; diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp index 54ffdc805..f6f79f348 100644 --- a/src/muz_qe/dl_mk_magic_sets.cpp +++ b/src/muz_qe/dl_mk_magic_sets.cpp @@ -28,6 +28,7 @@ namespace datalog { plugin(10000, true), m_context(ctx), m(ctx.get_manager()), + rm(ctx.get_rule_manager()), m_pinned(m), m_goal(goal, m) { } @@ -259,7 +260,7 @@ namespace datalog { } new_tail.push_back(curr); negations.push_back(r->is_neg_tail(curr_index)); - collect_vars(m, curr, bound_vars); + bound_vars |= rm.collect_vars(curr); } diff --git a/src/muz_qe/dl_mk_magic_sets.h b/src/muz_qe/dl_mk_magic_sets.h index 507f6c2bf..3496a5967 100644 --- a/src/muz_qe/dl_mk_magic_sets.h +++ b/src/muz_qe/dl_mk_magic_sets.h @@ -47,6 +47,11 @@ namespace datalog { AD_BOUND }; + struct a_flag_hash { + typedef a_flag data; + unsigned operator()(a_flag x) const { return x; } + }; + struct adornment : public svector { void populate(app * lit, const var_idx_set & bound_vars); @@ -71,7 +76,7 @@ namespace datalog { return m_pred==o.m_pred && m_adornment==o.m_adornment; } unsigned hash() const { - return m_pred->hash()^int_vector_hash(m_adornment); + return m_pred->hash()^svector_hash()(m_adornment); } }; @@ -90,6 +95,7 @@ namespace datalog { context & m_context; ast_manager & m; + rule_manager& rm; ast_ref_vector m_pinned; /** \brief Predicates from the original set that appear in a head of a rule diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index 8428d9049..4afc1d323 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -505,9 +505,6 @@ namespace datalog { unsigned head_arity = head_pred->get_arity(); - //var_idx_set head_vars; - //var_idx_set same_strat_vars; - //collect_vars(m, r->get_head(), head_vars); unsigned pt_len = r->get_positive_tail_size(); for (unsigned ti=0; tiget_head(), same_strat_vars); if (pred->get_arity()>head_arity || (pred->get_arity()==head_arity && pred->get_id()>=head_pred->get_id()) ) { return false; @@ -709,8 +705,7 @@ namespace datalog { #define PRT(_x_) ((_x_)?"T":"F") - bool mk_rule_inliner::inline_linear(rule_set const& source, scoped_ptr& rules) { - scoped_ptr res = alloc(rule_set, m_context); + bool mk_rule_inliner::inline_linear(scoped_ptr& rules) { bool done_something = false; unsigned sz = rules->get_num_rules(); @@ -731,7 +726,7 @@ namespace datalog { svector& can_expand = m_head_visitor.can_expand(); for (unsigned i = 0; i < sz; ++i) { - add_rule(source, acc[i].get(), i); + add_rule(*rules, acc[i].get(), i); } // initialize substitution. @@ -808,7 +803,7 @@ namespace datalog { TRACE("dl", r->display(m_context, tout); r2->display(m_context, tout); rl_res->display(m_context, tout); ); del_rule(r, i); - add_rule(source, rl_res.get(), i); + add_rule(*rules, rl_res.get(), i); r = rl_res; @@ -828,13 +823,15 @@ namespace datalog { } } if (done_something) { - rules = alloc(rule_set, m_context); + scoped_ptr res = alloc(rule_set, m_context); for (unsigned i = 0; i < sz; ++i) { if (valid.get(i)) { - rules->add_rule(acc[i].get()); + res->add_rule(acc[i].get()); } } - TRACE("dl", rules->display(tout);); + res->inherit_predicates(*rules); + TRACE("dl", res->display(tout);); + rules = res.detach(); } return done_something; } @@ -871,11 +868,17 @@ namespace datalog { // try eager inlining if (do_eager_inlining(res)) { something_done = true; - } + } TRACE("dl", res->display(tout << "after eager inlining\n");); + } + if (something_done) { + res->inherit_predicates(source); + } + else { + res = alloc(rule_set, source); } - if (m_context.get_params().inline_linear() && inline_linear(source, res)) { + if (m_context.get_params().inline_linear() && inline_linear(res)) { something_done = true; } @@ -883,7 +886,6 @@ namespace datalog { res = 0; } else { - res->inherit_predicates(source); m_context.add_model_converter(hsmc.get()); } diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h index 476c6b4b0..3a933f990 100644 --- a/src/muz_qe/dl_mk_rule_inliner.h +++ b/src/muz_qe/dl_mk_rule_inliner.h @@ -172,7 +172,7 @@ namespace datalog { /** Inline predicates that are known to not be join-points. */ - bool inline_linear(rule_set const& source, scoped_ptr& rules); + bool inline_linear(scoped_ptr& rules); void add_rule(rule_set const& rule_set, rule* r, unsigned i); void del_rule(rule* r, unsigned i); diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp index 8e77785b8..b600811f0 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.cpp +++ b/src/muz_qe/dl_mk_similarity_compressor.cpp @@ -29,6 +29,7 @@ namespace datalog { m_manager(ctx.get_manager()), m_threshold_count(ctx.similarity_compressor_threshold()), m_result_rules(ctx.get_rule_manager()), + m_modified(false), m_pinned(m_manager) { SASSERT(m_threshold_count>1); } @@ -55,6 +56,9 @@ namespace datalog { return (a>b) ? 1 : ( (a==b) ? 0 : -1); } + template + static int aux_compare(T* a, T* b); + static int compare_var_args(app* t1, app* t2) { SASSERT(t1->get_num_args()==t2->get_num_args()); int res; @@ -88,7 +92,7 @@ namespace datalog { if ((skip_countdown--) == 0) { continue; } - res = aux_compare(t1->get_arg(i), t2->get_arg(i)); + res = aux_compare(t1->get_arg(i)->get_id(), t2->get_arg(i)->get_id()); if (res!=0) { return res; } } return 0; @@ -113,7 +117,7 @@ namespace datalog { for (int i=-1; iget_decl(), t2->get_decl()); + res = aux_compare(t1->get_decl()->get_id(), t2->get_decl()->get_id()); if (res!=0) { return res; } res = compare_var_args(t1, t2); if (res!=0) { return res; } @@ -121,7 +125,7 @@ namespace datalog { unsigned tail_sz = r1->get_tail_size(); for (unsigned i=pos_tail_sz; iget_tail(i), r2->get_tail(i)); + res = aux_compare(r1->get_tail(i)->get_id(), r2->get_tail(i)->get_id()); if (res!=0) { return res; } } diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp index 2fec78066..990125475 100644 --- a/src/muz_qe/dl_mk_simple_joins.cpp +++ b/src/muz_qe/dl_mk_simple_joins.cpp @@ -29,7 +29,8 @@ namespace datalog { mk_simple_joins::mk_simple_joins(context & ctx): plugin(1000), - m_context(ctx) { + m_context(ctx), + rm(ctx.get_rule_manager()) { } class join_planner { @@ -120,6 +121,7 @@ namespace datalog { context & m_context; ast_manager & m; + rule_manager & rm; var_subst & m_var_subst; rule_set & m_rs_aux_copy; //reference to a rule_set that will allow to ask for stratum levels @@ -130,10 +132,13 @@ namespace datalog { ptr_hashtable, ptr_eq > m_modified_rules; ast_ref_vector m_pinned; + mutable ptr_vector m_vars; public: join_planner(context & ctx, rule_set & rs_aux_copy) - : m_context(ctx), m(ctx.get_manager()), m_var_subst(ctx.get_var_subst()), + : m_context(ctx), m(ctx.get_manager()), + rm(ctx.get_rule_manager()), + m_var_subst(ctx.get_var_subst()), m_rs_aux_copy(rs_aux_copy), m_introduced_rules(ctx.get_rule_manager()), m_pinned(ctx.get_manager()) @@ -175,9 +180,7 @@ namespace datalog { unsigned max_var_idx = 0; { - var_idx_set orig_var_set; - collect_vars(m, t1, orig_var_set); - collect_vars(m, t2, orig_var_set); + var_idx_set& orig_var_set = rm.collect_vars(t1, t2); var_idx_set::iterator ovit = orig_var_set.begin(); var_idx_set::iterator ovend = orig_var_set.end(); for(; ovit!=ovend; ++ovit) { @@ -323,14 +326,13 @@ namespace datalog { } for(unsigned i=0; iget_tail(i); - var_idx_set t1_vars; - collect_vars(m, t1, t1_vars); + var_idx_set t1_vars = rm.collect_vars(t1); counter.count_vars(m, t1, -1); //temporarily remove t1 variables from counter for(unsigned j=i+1; jget_tail(j); counter.count_vars(m, t2, -1); //temporarily remove t2 variables from counter - var_idx_set scope_vars(t1_vars); - collect_vars(m, t2, scope_vars); + var_idx_set scope_vars = rm.collect_vars(t2); + scope_vars |= t1_vars; var_idx_set non_local_vars; counter.collect_positive(non_local_vars); counter.count_vars(m, t2, 1); //restore t2 variables in counter @@ -472,8 +474,7 @@ namespace datalog { while(!added_tails.empty()) { app * a_tail = added_tails.back(); //added tail - var_idx_set a_tail_vars; - collect_vars(m, a_tail, a_tail_vars); + var_idx_set a_tail_vars = rm.collect_vars(a_tail); counter.count_vars(m, a_tail, -1); //temporarily remove a_tail variables from counter for(unsigned i=0; iadd_predicate(p, f); } } + else if (src.is_output_predicate(p)) { + dst.set_output_predicate(p); + } } } diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp index 0e94ba3b9..8c9e7e69f 100644 --- a/src/muz_qe/dl_mk_subsumption_checker.cpp +++ b/src/muz_qe/dl_mk_subsumption_checker.cpp @@ -241,6 +241,7 @@ namespace datalog { tgt.add_rule(new_rule); subs_index.add(new_rule); } + tgt.inherit_predicates(orig); TRACE("dl", tout << "original set size: "<inherit_predicates(source); return res; } diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp index eec0b991d..7eb6f829d 100644 --- a/src/muz_qe/dl_mk_unbound_compressor.cpp +++ b/src/muz_qe/dl_mk_unbound_compressor.cpp @@ -27,7 +27,8 @@ namespace datalog { plugin(500), m_context(ctx), m(ctx.get_manager()), - m_rules(ctx.get_rule_manager()), + rm(ctx.get_rule_manager()), + m_rules(rm), m_pinned(m) { } @@ -47,10 +48,7 @@ namespace datalog { } unsigned var_idx = to_var(head_arg)->get_idx(); - var_idx_set tail_vars; - collect_tail_vars(m, r, tail_vars); - - return tail_vars.contains(var_idx); + return rm.collect_tail_vars(r).contains(var_idx); } void mk_unbound_compressor::add_task(func_decl * pred, unsigned arg_index) { @@ -83,8 +81,7 @@ namespace datalog { void mk_unbound_compressor::detect_tasks(rule_set const& source, unsigned rule_index) { rule * r = m_rules.get(rule_index); - var_idx_set tail_vars; - collect_tail_vars(m, r, tail_vars); + var_idx_set& tail_vars = rm.collect_tail_vars(r); app * head = r->get_head(); func_decl * head_pred = head->get_decl(); @@ -94,9 +91,9 @@ namespace datalog { } unsigned n = head_pred->get_arity(); - - var_counter head_var_counter; - head_var_counter.count_vars(m, head, 1); + + rm.get_counter().reset(); + rm.get_counter().count_vars(m, head, 1); for (unsigned i=0; iget_arg(i); @@ -107,7 +104,7 @@ namespace datalog { if (!tail_vars.contains(var_idx)) { //unbound - unsigned occurence_cnt = head_var_counter.get(var_idx); + unsigned occurence_cnt = rm.get_counter().get(var_idx); SASSERT(occurence_cnt>0); if (occurence_cnt == 1) { TRACE("dl", r->display(m_context, tout << "Compress: ");); @@ -121,15 +118,14 @@ namespace datalog { void mk_unbound_compressor::try_compress(rule_set const& source, unsigned rule_index) { start: rule * r = m_rules.get(rule_index); - var_idx_set tail_vars; - collect_tail_vars(m, r, tail_vars); + var_idx_set& tail_vars = rm.collect_tail_vars(r); app * head = r->get_head(); func_decl * head_pred = head->get_decl(); unsigned head_arity = head_pred->get_arity(); - var_counter head_var_counter; - head_var_counter.count_vars(m, head); + rm.get_counter().reset(); + rm.get_counter().count_vars(m, head); unsigned arg_index; for (arg_index = 0; arg_index < head_arity; arg_index++) { @@ -140,7 +136,7 @@ namespace datalog { unsigned var_idx = to_var(arg)->get_idx(); if (!tail_vars.contains(var_idx)) { //unbound - unsigned occurence_cnt = head_var_counter.get(var_idx); + unsigned occurence_cnt = rm.get_counter().get(var_idx); SASSERT(occurence_cnt>0); if ( occurence_cnt==1 && m_in_progress.contains(c_info(head_pred, arg_index)) ) { //we have found what to compress diff --git a/src/muz_qe/dl_mk_unbound_compressor.h b/src/muz_qe/dl_mk_unbound_compressor.h index 4e56a74fc..4e2ff0b3c 100644 --- a/src/muz_qe/dl_mk_unbound_compressor.h +++ b/src/muz_qe/dl_mk_unbound_compressor.h @@ -52,6 +52,7 @@ namespace datalog { context & m_context; ast_manager & m; + rule_manager & rm; rule_ref_vector m_rules; bool m_modified; todo_stack m_todo; diff --git a/src/muz_qe/dl_product_relation.h b/src/muz_qe/dl_product_relation.h index c5e755939..91c2286a7 100644 --- a/src/muz_qe/dl_product_relation.h +++ b/src/muz_qe/dl_product_relation.h @@ -40,8 +40,12 @@ namespace datalog { class filter_equal_fn; class filter_identical_fn; class filter_interpreted_fn; + struct fid_hash { + typedef family_id data; + unsigned operator()(data x) const { return static_cast(x); } + }; - rel_spec_store m_spec_store; + rel_spec_store > m_spec_store; family_id get_relation_kind(const product_relation & r); diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp index ef8e6ddd4..986a1f2c4 100644 --- a/src/muz_qe/dl_relation_manager.cpp +++ b/src/muz_qe/dl_relation_manager.cpp @@ -740,7 +740,6 @@ namespace datalog { relation_transformer_fn * relation_manager::mk_select_equal_and_project_fn(const relation_base & t, const relation_element & value, unsigned col) { relation_transformer_fn * res = t.get_plugin().mk_select_equal_and_project_fn(t, value, col); - TRACE("dl", tout << t.get_plugin().get_name() << " " << value << " " << col << "\n";); if(!res) { relation_mutator_fn * selector = mk_filter_equal_fn(t, value, col); if(selector) { diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h index 26008a830..f22ae7923 100644 --- a/src/muz_qe/dl_relation_manager.h +++ b/src/muz_qe/dl_relation_manager.h @@ -605,7 +605,7 @@ namespace datalog { /** This is a helper class for relation_plugins whose relations can be of various kinds. */ - template, class Eq=vector_eq_proc > + template > class rel_spec_store { typedef relation_signature::hash r_hash; typedef relation_signature::eq r_eq; diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index 92f504bcc..ac683eca9 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -40,15 +40,20 @@ Revision History: #include"quant_hoist.h" #include"expr_replacer.h" #include"bool_rewriter.h" -#include"qe_lite.h" #include"expr_safe_replace.h" -#include"hnf.h" namespace datalog { rule_manager::rule_manager(context& ctx) : m(ctx.get_manager()), - m_ctx(ctx) {} + m_ctx(ctx), + m_body(m), + m_head(m), + m_args(m), + m_hnf(m), + m_qe(m), + m_cfg(m), + m_rwr(m, false, m_cfg) {} void rule_manager::inc_ref(rule * r) { if (r) { @@ -67,29 +72,23 @@ namespace datalog { } } - class remove_label_cfg : public default_rewriter_cfg { - family_id m_label_fid; - public: - remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {} - virtual ~remove_label_cfg() {} + rule_manager::remove_label_cfg::~remove_label_cfg() {} - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, - proof_ref & result_pr) - { - if (is_decl_of(f, m_label_fid, OP_LABEL)) { - SASSERT(num == 1); - result = args[0]; - return BR_DONE; - } - return BR_FAILED; + br_status rule_manager::remove_label_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, + proof_ref & result_pr) + { + if (is_decl_of(f, m_label_fid, OP_LABEL)) { + SASSERT(num == 1); + result = args[0]; + return BR_DONE; } - }; + return BR_FAILED; + } + void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) { expr_ref tmp(m); - remove_label_cfg r_cfg(m); - rewriter_tpl rwr(m, false, r_cfg); - rwr(fml, tmp); + m_rwr(fml, tmp); if (pr && fml != tmp) { pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp)); @@ -97,6 +96,67 @@ namespace datalog { fml = tmp; } + var_idx_set& rule_manager::collect_vars(expr* e) { + return collect_vars(e, 0); + } + + var_idx_set& rule_manager::collect_vars(expr* e1, expr* e2) { + reset_collect_vars(); + if (e1) accumulate_vars(e1); + if (e2) accumulate_vars(e2); + return finalize_collect_vars(); + } + + void rule_manager::reset_collect_vars() { + m_vars.reset(); + m_var_idx.reset(); + m_todo.reset(); + m_mark.reset(); + } + + var_idx_set& rule_manager::finalize_collect_vars() { + unsigned sz = m_vars.size(); + for (unsigned i=0; iget_tail_size(); + for (unsigned i=0;iget_tail(i)); + } + return finalize_collect_vars(); + } + + var_idx_set& rule_manager::collect_rule_vars_ex(rule * r, app* t) { + reset_collect_vars(); + unsigned n = r->get_tail_size(); + accumulate_vars(r->get_head()); + for (unsigned i=0;iget_tail(i) != t) { + accumulate_vars(r->get_tail(i)); + } + } + return finalize_collect_vars(); + } + + var_idx_set& rule_manager::collect_rule_vars(rule * r) { + reset_collect_vars(); + unsigned n = r->get_tail_size(); + accumulate_vars(r->get_head()); + for (unsigned i=0;iget_tail(i)); + } + return finalize_collect_vars(); + } + + void rule_manager::accumulate_vars(expr* e) { + ::get_free_vars(m_mark, m_todo, e, m_vars); + } + void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) { scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED); @@ -125,13 +185,13 @@ namespace datalog { } void rule_manager::mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name) { - hnf h(m); expr_ref_vector fmls(m); proof_ref_vector prs(m); - h.set_name(name); - h(fml, p, fmls, prs); - for (unsigned i = 0; i < h.get_fresh_predicates().size(); ++i) { - m_ctx.register_predicate(h.get_fresh_predicates()[i], false); + m_hnf.reset(); + m_hnf.set_name(name); + m_hnf(fml, p, fmls, prs); + for (unsigned i = 0; i < m_hnf.get_fresh_predicates().size(); ++i) { + m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false); } for (unsigned i = 0; i < fmls.size(); ++i) { mk_horn_rule(fmls[i].get(), prs[i].get(), rules, name); @@ -140,24 +200,23 @@ namespace datalog { void rule_manager::mk_horn_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) { - app_ref_vector body(m); - app_ref head(m); - svector is_negated; - unsigned index = extract_horn(fml, body, head); - hoist_compound_predicates(index, head, body); + m_body.reset(); + m_neg.reset(); + unsigned index = extract_horn(fml, m_body, m_head); + hoist_compound_predicates(index, m_head, m_body); TRACE("dl_rule", - tout << mk_pp(head, m) << " :- "; - for (unsigned i = 0; i < body.size(); ++i) { - tout << mk_pp(body[i].get(), m) << " "; + tout << mk_pp(m_head, m) << " :- "; + for (unsigned i = 0; i < m_body.size(); ++i) { + tout << mk_pp(m_body[i].get(), m) << " "; } tout << "\n";); - mk_negations(body, is_negated); - check_valid_rule(head, body.size(), body.c_ptr()); + mk_negations(m_body, m_neg); + check_valid_rule(m_head, m_body.size(), m_body.c_ptr()); rule_ref r(*this); - r = mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name); + r = mk(m_head.get(), m_body.size(), m_body.c_ptr(), m_neg.c_ptr(), name); expr_ref fml1(m); if (p) { @@ -326,28 +385,28 @@ namespace datalog { fml = m.mk_not(fml); return; } - expr_ref_vector args(m); if (!m_ctx.is_predicate(fml)) { return; } + m_args.reset(); for (unsigned i = 0; i < fml->get_num_args(); ++i) { e = fml->get_arg(i); if (!is_app(e)) { - args.push_back(e); + m_args.push_back(e); continue; } app* b = to_app(e); if (m.is_value(b)) { - args.push_back(e); + m_args.push_back(e); } else { var* v = m.mk_var(num_bound++, m.get_sort(b)); - args.push_back(v); + m_args.push_back(v); body.push_back(m.mk_eq(v, b)); } } - fml = m.mk_app(fml->get_decl(), args.size(), args.c_ptr()); + fml = m.mk_app(fml->get_decl(), m_args.size(), m_args.c_ptr()); TRACE("dl_rule", tout << mk_pp(fml.get(), m) << "\n";); } @@ -511,29 +570,22 @@ namespace datalog { void rule_manager::reduce_unbound_vars(rule_ref& r) { unsigned ut_len = r->get_uninterpreted_tail_size(); unsigned t_len = r->get_tail_size(); - ptr_vector vars; - uint_set index_set; - qe_lite qe(m); expr_ref_vector conjs(m); if (ut_len == t_len) { return; } - get_free_vars(r->get_head(), vars); + reset_collect_vars(); + accumulate_vars(r->get_head()); for (unsigned i = 0; i < ut_len; ++i) { - get_free_vars(r->get_tail(i), vars); + accumulate_vars(r->get_tail(i)); } + var_idx_set& index_set = finalize_collect_vars(); for (unsigned i = ut_len; i < t_len; ++i) { conjs.push_back(r->get_tail(i)); } - - for (unsigned i = 0; i < vars.size(); ++i) { - if (vars[i]) { - index_set.insert(i); - } - } - qe(index_set, false, conjs); + m_qe(index_set, false, conjs); bool change = conjs.size() != t_len - ut_len; for (unsigned i = 0; !change && i < conjs.size(); ++i) { change = r->get_tail(ut_len+i) != conjs[i].get(); @@ -570,15 +622,14 @@ namespace datalog { return; } - ptr_vector free_rule_vars; var_counter vctr; app_ref_vector tail(m); svector tail_neg; app_ref head(r->get_head(), m); - get_free_vars(r, free_rule_vars); + collect_rule_vars(r); vctr.count_vars(m, head); - + ptr_vector& free_rule_vars = m_vars; for (unsigned i = 0; i < ut_len; i++) { app * t = r->get_tail(i); @@ -906,7 +957,7 @@ namespace datalog { } void rule::norm_vars(rule_manager & rm) { - used_vars used; + used_vars& used = rm.reset_used(); get_used_vars(used); unsigned first_unsused = used.get_max_found_var_idx_plus_1(); @@ -1004,16 +1055,14 @@ namespace datalog { } svector names; used_symbols<> us; - - us(fml); - sorts.reverse(); - for (unsigned i = 0; i < sorts.size(); ++i) { if (!sorts[i]) { sorts[i] = m.mk_bool_sort(); } } - + + us(fml); + sorts.reverse(); for (unsigned j = 0, i = 0; i < sorts.size(); ++j) { for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) { func_decl_ref f(m); @@ -1067,6 +1116,8 @@ namespace datalog { } - + }; +template class rewriter_tpl; + diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h index 666ddbd50..77bf9ac74 100644 --- a/src/muz_qe/dl_rule.h +++ b/src/muz_qe/dl_rule.h @@ -27,6 +27,9 @@ Revision History: #include"proof_converter.h" #include"model_converter.h" #include"ast_counter.h" +#include"rewriter.h" +#include"hnf.h" +#include"qe_lite.h" namespace datalog { @@ -47,9 +50,33 @@ namespace datalog { */ class rule_manager { + class remove_label_cfg : public default_rewriter_cfg { + family_id m_label_fid; + public: + remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {} + virtual ~remove_label_cfg(); + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, + proof_ref & result_pr); + }; + ast_manager& m; context& m_ctx; rule_counter m_counter; + used_vars m_used; + ptr_vector m_vars; + var_idx_set m_var_idx; + ptr_vector m_todo; + ast_mark m_mark; + app_ref_vector m_body; + app_ref m_head; + expr_ref_vector m_args; + svector m_neg; + hnf m_hnf; + qe_lite m_qe; + remove_label_cfg m_cfg; + rewriter_tpl m_rwr; + // only the context can create a rule_manager friend class context; @@ -90,6 +117,10 @@ namespace datalog { */ void reduce_unbound_vars(rule_ref& r); + void reset_collect_vars(); + + var_idx_set& finalize_collect_vars(); + public: ast_manager& get_manager() const { return m; } @@ -98,6 +129,24 @@ namespace datalog { void dec_ref(rule * r); + used_vars& reset_used() { m_used.reset(); return m_used; } + + var_idx_set& collect_vars(expr * pred); + + var_idx_set& collect_vars(expr * e1, expr* e2); + + var_idx_set& collect_rule_vars(rule * r); + + var_idx_set& collect_rule_vars_ex(rule * r, app* t); + + var_idx_set& collect_tail_vars(rule * r); + + void accumulate_vars(expr* pred); + + ptr_vector& get_var_sorts() { return m_vars; } + + var_idx_set& get_var_idx() { return m_var_idx; } + /** \brief Create a Datalog rule from a Horn formula. The formula is of the form (forall (...) (forall (...) (=> (and ...) head))) diff --git a/src/muz_qe/dl_rule_set.cpp b/src/muz_qe/dl_rule_set.cpp index cb129ab37..ad3b512a3 100644 --- a/src/muz_qe/dl_rule_set.cpp +++ b/src/muz_qe/dl_rule_set.cpp @@ -409,9 +409,10 @@ namespace datalog { } void rule_set::reopen() { - SASSERT(is_closed()); - m_stratifier = 0; - m_deps.reset(); + if (is_closed()) { + m_stratifier = 0; + m_deps.reset(); + } } /** diff --git a/src/muz_qe/dl_sieve_relation.cpp b/src/muz_qe/dl_sieve_relation.cpp index c3ea5a3d0..e80462900 100644 --- a/src/muz_qe/dl_sieve_relation.cpp +++ b/src/muz_qe/dl_sieve_relation.cpp @@ -567,8 +567,7 @@ namespace datalog { const relation_signature sig = r.get_signature(); unsigned sz = sig.size(); - var_idx_set cond_vars; - collect_vars(m, condition, cond_vars); + var_idx_set& cond_vars = get_context().get_rule_manager().collect_vars(condition); expr_ref_vector subst_vect(m); subst_vect.resize(sz); unsigned subst_ofs = sz-1; diff --git a/src/muz_qe/dl_sieve_relation.h b/src/muz_qe/dl_sieve_relation.h index d6df3af55..551f5d705 100644 --- a/src/muz_qe/dl_sieve_relation.h +++ b/src/muz_qe/dl_sieve_relation.h @@ -52,7 +52,7 @@ namespace datalog { struct hash { unsigned operator()(const rel_spec & s) const { - return int_vector_hash(s.m_inner_cols)^s.m_inner_kind; + return svector_hash()(s.m_inner_cols)^s.m_inner_kind; } }; }; diff --git a/src/muz_qe/dl_sparse_table.h b/src/muz_qe/dl_sparse_table.h index 3920836e6..010277b6b 100644 --- a/src/muz_qe/dl_sparse_table.h +++ b/src/muz_qe/dl_sparse_table.h @@ -359,7 +359,7 @@ namespace datalog { typedef svector key_spec; //sequence of columns in a key typedef svector key_value; //values of key columns - typedef map, + typedef map, vector_eq_proc > key_index_map; static const store_offset NO_RESERVE = UINT_MAX; diff --git a/src/muz_qe/dl_table.h b/src/muz_qe/dl_table.h index 8dc0a355b..3a240c337 100644 --- a/src/muz_qe/dl_table.h +++ b/src/muz_qe/dl_table.h @@ -73,7 +73,7 @@ namespace datalog { class our_iterator_core; - typedef hashtable, + typedef hashtable, vector_eq_proc > storage; storage m_data; diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp index 95d268510..1b1042345 100644 --- a/src/muz_qe/dl_util.cpp +++ b/src/muz_qe/dl_util.cpp @@ -158,36 +158,7 @@ namespace datalog { ::get_free_vars(trm, vars); return var_idx < vars.size() && vars[var_idx] != 0; } - - - void collect_vars(ast_manager & m, expr * e, var_idx_set & result) { - ptr_vector vars; - ::get_free_vars(e, vars); - unsigned sz = vars.size(); - for(unsigned i=0; iget_tail_size(); - for(unsigned i=0;iget_tail(i), result); - } - } - - void get_free_tail_vars(rule * r, ptr_vector& sorts) { - unsigned n = r->get_tail_size(); - for(unsigned i=0;iget_tail(i), sorts); - } - } - - void get_free_vars(rule * r, ptr_vector& sorts) { - get_free_vars(r->get_head(), sorts); - get_free_tail_vars(r, sorts); - } - unsigned count_variable_arguments(app * pred) { SASSERT(is_uninterp(pred)); @@ -202,26 +173,6 @@ namespace datalog { return res; } - void collect_non_local_vars(ast_manager & m, rule const * r, app * t, var_idx_set & result) { - collect_vars(m, r->get_head(), result); - unsigned sz = r->get_tail_size(); - for (unsigned i = 0; i < sz; i++) { - app * curr = r->get_tail(i); - if (curr != t) - collect_vars(m, curr, result); - } - } - - void collect_non_local_vars(ast_manager & m, rule const * r, app * t_1, app * t_2, var_idx_set & result) { - collect_vars(m, r->get_head(), result); - unsigned sz = r->get_tail_size(); - for (unsigned i = 0; i < sz; i++) { - app * curr = r->get_tail(i); - if (curr != t_1 && curr != t_2) - collect_vars(m, curr, result); - } - } - void mk_new_rule_tail(ast_manager & m, app * pred, var_idx_set const & non_local_vars, unsigned & next_idx, varidx2var_map & varidx2var, sort_ref_buffer & new_rule_domain, expr_ref_buffer & new_rule_args, app_ref & new_pred) { expr_ref_buffer new_args(m); @@ -404,6 +355,7 @@ namespace datalog { void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) { + reset(); count_vars(m, r->get_head(), 1); unsigned n = r->get_tail_size(); for (unsigned i = 0; i < n; i++) { diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index 974ab5862..ea2def025 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -54,6 +54,7 @@ namespace datalog { BMC_ENGINE, QBMC_ENGINE, TAB_ENGINE, + CLP_ENGINE, LAST_ENGINE }; @@ -81,33 +82,13 @@ namespace datalog { void flatten_or(expr* fml, expr_ref_vector& result); - - bool contains_var(expr * trm, unsigned var_idx); - /** - \brief Collect the variables in \c pred. - \pre \c pred must be a valid head or tail. - */ - void collect_vars(ast_manager & m, expr * pred, var_idx_set & result); - void collect_tail_vars(ast_manager & m, rule * r, var_idx_set & result); - - void get_free_vars(rule * r, ptr_vector& sorts); - /** \brief Return number of arguments of \c pred that are variables */ unsigned count_variable_arguments(app * pred); - /** - \brief Store in \c result the set of variables used by \c r when ignoring the tail \c t. - */ - void collect_non_local_vars(ast_manager & m, rule const * r, app * t, var_idx_set & result); - - /** - \brief Store in \c result the set of variables used by \c r when ignoring the tail elements \c t_1 and \c t_2. - */ - void collect_non_local_vars(ast_manager & m, rule const * r, app * t_1, app * t_2, var_idx_set & result); template void copy_nonvariables(app * src, T& tgt) @@ -207,7 +188,9 @@ namespace datalog { static unsigned expr_cont_get_size(app * a) { return a->get_num_args(); } static expr * expr_cont_get(app * a, unsigned i) { return a->get_arg(i); } static unsigned expr_cont_get_size(const ptr_vector & v) { return v.size(); } + static unsigned expr_cont_get_size(const expr_ref_vector & v) { return v.size(); } static expr * expr_cont_get(const ptr_vector & v, unsigned i) { return v[i]; } + static expr * expr_cont_get(const expr_ref_vector & v, unsigned i) { return v[i]; } public: variable_intersection(ast_manager & m) : m_consts(m) {} @@ -585,17 +568,31 @@ namespace datalog { } template - unsigned int_vector_hash(const T & cont) { - return string_hash(reinterpret_cast(cont.c_ptr()), - cont.size()*sizeof(typename T::data), 0); + struct default_obj_chash { + unsigned operator()(T const& cont, unsigned i) const { + return cont[i]->hash(); + } + }; + template + unsigned obj_vector_hash(const T & cont) { + return get_composite_hash(cont, cont.size(),default_kind_hash_proc(), default_obj_chash()); } template - struct int_vector_hash_proc { + struct obj_vector_hash_proc { unsigned operator()(const T & cont) const { - return int_vector_hash(cont); + return obj_vector_hash(cont); } }; + + template + struct svector_hash_proc { + unsigned operator()(const svector & cont) const { + return svector_hash()(cont); + } + }; + + template struct vector_eq_proc { bool operator()(const T & c1, const T & c2) const { return vectors_equal(c1, c2); } @@ -763,11 +760,6 @@ namespace datalog { // // ----------------------------------- - struct uint64_hash { - typedef uint64 data; - unsigned operator()(uint64 x) const { return hash_ull(x); } - }; - template void universal_delete(T* ptr) { dealloc(ptr); diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index fd7dbdcae..c516806a6 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -13,7 +13,6 @@ def_module_params('fixedpoint', ('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"), - ('filter_rules', BOOL, True, "(DATALOG) apply filter compression on rules"), ('all_or_nothing_deltas', BOOL, False, "(DATALOG) compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not"), ('compile_with_widening', BOOL, False, "(DATALOG) widening will be used to compile recursive rules"), ('eager_emptiness_checking', BOOL, True, "(DATALOG) emptiness of affected relations will be checked after each instruction, so that we may ommit unnecessary instructions"), @@ -61,6 +60,7 @@ def_module_params('fixedpoint', ('print_answer', BOOL, False, 'print answer instance(s) to query'), ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'), ('print_statistics', BOOL, False, 'print statistics'), + ('use_utvpi', BOOL, False, 'experimental use UTVPI strategy'), ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'), )) diff --git a/src/muz_qe/hnf.cpp b/src/muz_qe/hnf.cpp index 5a7d1c4ba..bcc3501de 100644 --- a/src/muz_qe/hnf.cpp +++ b/src/muz_qe/hnf.cpp @@ -71,6 +71,9 @@ class hnf::imp { obj_map m_memoize_disj; obj_map m_memoize_proof; func_decl_ref_vector m_fresh_predicates; + expr_ref_vector m_body; + proof_ref_vector m_defs; + public: imp(ast_manager & m): @@ -82,7 +85,9 @@ public: m_refs(m), m_name("P"), m_qh(m), - m_fresh_predicates(m) { + m_fresh_predicates(m), + m_body(m), + m_defs(m) { } void operator()(expr * n, @@ -181,14 +186,15 @@ private: void mk_horn(expr_ref& fml, proof_ref& premise) { + SASSERT(!premise || fml == m.get_fact(premise)); expr* e1, *e2; - expr_ref_vector body(m); - proof_ref_vector defs(m); expr_ref fml0(m), fml1(m), fml2(m), head(m); proof_ref p(m); fml0 = fml; m_names.reset(); m_sorts.reset(); + m_body.reset(); + m_defs.reset(); m_qh.pull_quantifier(true, fml0, &m_sorts, &m_names); if (premise){ fml1 = bind_variables(fml0); @@ -199,12 +205,12 @@ private: } head = fml0; while (m.is_implies(head, e1, e2)) { - body.push_back(e1); + m_body.push_back(e1); head = e2; } - datalog::flatten_and(body); + datalog::flatten_and(m_body); if (premise) { - p = m.mk_rewrite(fml0, mk_implies(body, head)); + p = m.mk_rewrite(fml0, mk_implies(m_body, head)); } // @@ -214,8 +220,8 @@ private: // A -> C // B -> C // - if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) { - app* _or = to_app(body[0].get()); + if (m_body.size() == 1 && m.is_or(m_body[0].get()) && contains_predicate(m_body[0].get())) { + app* _or = to_app(m_body[0].get()); unsigned sz = _or->get_num_args(); expr* const* args = _or->get_args(); for (unsigned i = 0; i < sz; ++i) { @@ -224,7 +230,7 @@ private: } if (premise) { - expr_ref f1 = bind_variables(mk_implies(body, head)); + expr_ref f1 = bind_variables(mk_implies(m_body, head)); expr* f2 = m.mk_and(sz, m_todo.c_ptr()+m_todo.size()-sz); proof_ref p2(m), p3(m); p2 = m.mk_def_axiom(m.mk_iff(f1, f2)); @@ -240,13 +246,13 @@ private: } - eliminate_disjunctions(body, defs); - p = mk_congruence(p, body, head, defs); + eliminate_disjunctions(m_body, m_defs); + p = mk_congruence(p, m_body, head, m_defs); - eliminate_quantifier_body(body, defs); - p = mk_congruence(p, body, head, defs); + eliminate_quantifier_body(m_body, m_defs); + p = mk_congruence(p, m_body, head, m_defs); - fml2 = mk_implies(body, head); + fml2 = mk_implies(m_body, head); fml = bind_variables(fml2); diff --git a/src/muz_qe/horn_subsume_model_converter.cpp b/src/muz_qe/horn_subsume_model_converter.cpp index 374333a9c..ced4e657b 100644 --- a/src/muz_qe/horn_subsume_model_converter.cpp +++ b/src/muz_qe/horn_subsume_model_converter.cpp @@ -28,10 +28,8 @@ Revision History: #include "well_sorted.h" void horn_subsume_model_converter::insert(app* head, expr* body) { - func_decl_ref pred(m); - expr_ref body_res(m); - VERIFY(mk_horn(head, body, pred, body_res)); - insert(pred.get(), body_res.get()); + m_delay_head.push_back(head); + m_delay_body.push_back(body); } void horn_subsume_model_converter::insert(app* head, unsigned sz, expr* const* body) { @@ -148,6 +146,7 @@ bool horn_subsume_model_converter::mk_horn( } void horn_subsume_model_converter::add_default_proc::operator()(app* n) { + // // predicates that have not been assigned values // in the Horn model are assumed false. @@ -174,6 +173,16 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod void horn_subsume_model_converter::operator()(model_ref& mr) { + + func_decl_ref pred(m); + expr_ref body_res(m); + for (unsigned i = 0; i < m_delay_head.size(); ++i) { + VERIFY(mk_horn(m_delay_head[i].get(), m_delay_body[i].get(), pred, body_res)); + insert(pred.get(), body_res.get()); + } + m_delay_head.reset(); + m_delay_body.reset(); + TRACE("mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0);); for (unsigned i = m_funcs.size(); i > 0; ) { --i; diff --git a/src/muz_qe/horn_subsume_model_converter.h b/src/muz_qe/horn_subsume_model_converter.h index edde02b19..993f29cc9 100644 --- a/src/muz_qe/horn_subsume_model_converter.h +++ b/src/muz_qe/horn_subsume_model_converter.h @@ -43,6 +43,8 @@ class horn_subsume_model_converter : public model_converter { func_decl_ref_vector m_funcs; expr_ref_vector m_bodies; th_rewriter m_rewrite; + app_ref_vector m_delay_head; + expr_ref_vector m_delay_body; void add_default_false_interpretation(expr* e, model_ref& md); @@ -56,7 +58,9 @@ class horn_subsume_model_converter : public model_converter { public: - horn_subsume_model_converter(ast_manager& m): m(m), m_funcs(m), m_bodies(m), m_rewrite(m) {} + horn_subsume_model_converter(ast_manager& m): + m(m), m_funcs(m), m_bodies(m), m_rewrite(m), + m_delay_head(m), m_delay_body(m) {} bool mk_horn(expr* clause, func_decl_ref& pred, expr_ref& body); diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 1a8f562d9..5db4f1a00 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -125,12 +125,13 @@ class horn_tactic : public tactic { enum formula_kind { IS_RULE, IS_QUERY, IS_NONE }; formula_kind get_formula_kind(expr_ref& f) { - normalize(f); + expr_ref tmp(f); + normalize(tmp); ast_mark mark; expr_ref_vector args(m), body(m); expr_ref head(m); expr* a = 0, *a1 = 0; - datalog::flatten_or(f, args); + datalog::flatten_or(tmp, args); for (unsigned i = 0; i < args.size(); ++i) { a = args[i].get(); check_predicate(mark, a); @@ -147,12 +148,12 @@ class horn_tactic : public tactic { body.push_back(m.mk_not(a)); } } - f = m.mk_and(body.size(), body.c_ptr()); if (head) { - f = m.mk_implies(f, head); + // f = m.mk_implies(f, head); return IS_RULE; } else { + f = m.mk_and(body.size(), body.c_ptr()); return IS_QUERY; } } @@ -171,7 +172,7 @@ class horn_tactic : public tactic { tactic_report report("horn", *g); bool produce_proofs = g->proofs_enabled(); - if (produce_proofs) { + if (produce_proofs) { if (!m_ctx.get_params().generate_proof_trace()) { params_ref params = m_ctx.get_params().p; params.set_bool("generate_proof_trace", true); @@ -239,10 +240,13 @@ class horn_tactic : public tactic { switch (is_reachable) { case l_true: { // goal is unsat - g->assert_expr(m.mk_false()); if (produce_proofs) { proof_ref proof = m_ctx.get_proof(); pc = proof2proof_converter(m, proof); + g->assert_expr(m.mk_false(), proof, 0); + } + else { + g->assert_expr(m.mk_false()); } break; } diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index a240a9aef..dcfbcca2b 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -43,6 +43,7 @@ Notes: #include "ast_ll_pp.h" #include "proof_checker.h" #include "smt_value_sort.h" +#include "proof_utils.h" namespace pdr { @@ -275,7 +276,7 @@ namespace pdr { src.pop_back(); } else if (is_invariant(tgt_level, curr, false, assumes_level)) { - + add_property(curr, assumes_level?tgt_level:infty_level); TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";); src[i] = src.back(); @@ -596,7 +597,7 @@ namespace pdr { expr_ref fml = pm.mk_and(conj); th_rewriter rw(m); rw(fml); - if (ctx.is_dl()) { + if (ctx.is_dl() || ctx.is_utvpi()) { hoist_non_bool_if(fml); } TRACE("pdr", tout << mk_pp(fml, m) << "\n";); @@ -1225,6 +1226,7 @@ namespace pdr { m_search(m_params.bfs_model_search()), m_last_result(l_undef), m_inductive_lvl(0), + m_expanded_lvl(0), m_cancel(false) { } @@ -1357,9 +1359,10 @@ namespace pdr { bool m_is_bool_arith; bool m_has_arith; bool m_is_dl; + bool m_is_utvpi; public: classifier_proc(ast_manager& m, datalog::rule_set& rules): - m(m), a(m), m_is_bool(true), m_is_bool_arith(true), m_has_arith(false), m_is_dl(false) { + m(m), a(m), m_is_bool(true), m_is_bool_arith(true), m_has_arith(false), m_is_dl(false), m_is_utvpi(false) { classify(rules); } void operator()(expr* e) { @@ -1405,6 +1408,7 @@ namespace pdr { bool is_dl() const { return m_is_dl; } + bool is_utvpi() const { return m_is_utvpi; } private: @@ -1425,6 +1429,7 @@ namespace pdr { mark.reset(); m_is_dl = false; + m_is_utvpi = false; if (m_has_arith) { ptr_vector forms; for (it = rules.begin(); it != end; ++it) { @@ -1436,6 +1441,7 @@ namespace pdr { } } m_is_dl = is_difference_logic(m, forms.size(), forms.c_ptr()); + m_is_utvpi = m_is_dl || is_utvpi_logic(m, forms.size(), forms.c_ptr()); } } @@ -1555,7 +1561,12 @@ namespace pdr { m_fparams.m_arith_auto_config_simplex = true; m_fparams.m_arith_propagate_eqs = false; m_fparams.m_arith_eager_eq_axioms = false; - if (classify.is_dl()) { + if (classify.is_utvpi() && m_params.use_utvpi()) { + IF_VERBOSE(1, verbose_stream() << "UTVPI\n";); + m_fparams.m_arith_mode = AS_UTVPI; + m_fparams.m_arith_expand_eqs = true; + } + else if (classify.is_dl()) { m_fparams.m_arith_mode = AS_DIFF_LOGIC; m_fparams.m_arith_expand_eqs = true; } @@ -1680,6 +1691,9 @@ namespace pdr { proof = m_search.get_proof_trace(*this); TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); apply(m, m_pc.get(), proof); + TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); + // proof_utils::push_instantiations_up(proof); + // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";); return proof; } @@ -1711,6 +1725,7 @@ namespace pdr { bool reachable; while (true) { checkpoint(); + m_expanded_lvl = lvl; reachable = check_reachability(lvl); if (reachable) { throw model_exception(); @@ -1769,6 +1784,10 @@ namespace pdr { void context::expand_node(model_node& n) { SASSERT(n.is_open()); expr_ref_vector cube(m); + + if (n.level() < m_expanded_lvl) { + m_expanded_lvl = n.level(); + } if (n.pt().is_reachable(n.state())) { TRACE("pdr", tout << "reachable\n";); @@ -1835,7 +1854,7 @@ namespace pdr { if (m_params.simplify_formulas_pre()) { simplify_formulas(); } - for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) { + for (unsigned lvl = m_expanded_lvl; lvl <= max_prop_lvl; lvl++) { checkpoint(); bool all_propagated = true; decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 6aa02ef10..1785991c6 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -303,6 +303,7 @@ namespace pdr { mutable model_search m_search; lbool m_last_result; unsigned m_inductive_lvl; + unsigned m_expanded_lvl; ptr_vector m_core_generalizers; stats m_stats; volatile bool m_cancel; @@ -366,7 +367,7 @@ namespace pdr { expr_ref get_answer(); bool is_dl() const { return m_fparams.m_arith_mode == AS_DIFF_LOGIC; } - + bool is_utvpi() const { return m_fparams.m_arith_mode == AS_UTVPI; } void collect_statistics(statistics& st) const; void reset_statistics(); diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index 393090299..71404ab12 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -216,6 +216,9 @@ namespace pdr { } res = m.mk_not(res); th_rewriter rw(m); + params_ref params; + params.set_bool("gcd_rounding", true); + rw.updt_params(params); proof_ref pr(m); expr_ref tmp(m); rw(res, tmp, pr); diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp index 863e5c03e..e3cd0d9c5 100644 --- a/src/muz_qe/pdr_prop_solver.cpp +++ b/src/muz_qe/pdr_prop_solver.cpp @@ -383,26 +383,32 @@ namespace pdr { fl.get_lemmas(pr, bs, lemmas); safe.elim_proxies(lemmas); fl.simplify_lemmas(lemmas); // redundant? - if (m_fparams.m_arith_mode == AS_DIFF_LOGIC && - !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) { - IF_VERBOSE(1, - verbose_stream() << "not diff\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; - }); - extract_subset_core(safe); - return; + + bool outside_of_logic = + (m_fparams.m_arith_mode == AS_DIFF_LOGIC && + !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) || + (m_fparams.m_arith_mode == AS_UTVPI && + !is_utvpi_logic(m, lemmas.size(), lemmas.c_ptr())); + + if (outside_of_logic) { + IF_VERBOSE(2, + verbose_stream() << "not diff\n"; + for (unsigned i = 0; i < lemmas.size(); ++i) { + verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; + }); + extract_subset_core(safe); + } + else { + + IF_VERBOSE(2, + verbose_stream() << "Lemmas\n"; + for (unsigned i = 0; i < lemmas.size(); ++i) { + verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; + }); + + m_core->reset(); + m_core->append(lemmas); } - - - IF_VERBOSE(2, - verbose_stream() << "Lemmas\n"; - for (unsigned i = 0; i < lemmas.size(); ++i) { - verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n"; - }); - - m_core->reset(); - m_core->append(lemmas); } lbool prop_solver::check_assumptions(const expr_ref_vector & atoms) { diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 237cf9415..9711cffc2 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -1081,6 +1081,7 @@ namespace pdr { arith_util a; bv_util bv; bool m_is_dl; + bool m_test_for_utvpi; bool is_numeric(expr* e) const { if (a.is_numeral(e)) { @@ -1115,6 +1116,16 @@ namespace pdr { } return false; } + if (m_test_for_utvpi) { + if (a.is_mul(e, e1, e2)) { + if (is_minus_one(e1)) { + return is_offset(e2); + } + if (is_minus_one(e2)) { + return is_offset(e1); + } + } + } return !is_arith_expr(e); } @@ -1140,6 +1151,9 @@ namespace pdr { if (!a.is_add(lhs, arg1, arg2)) return false; // x + if (m_test_for_utvpi) { + return is_offset(arg1) && is_offset(arg2); + } if (is_arith_expr(arg1)) std::swap(arg1, arg2); if (is_arith_expr(arg1)) @@ -1209,8 +1223,10 @@ namespace pdr { } public: - test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true) {} - + test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {} + + void test_for_utvpi() { m_test_for_utvpi = true; } + void operator()(expr* e) { if (!m_is_dl) { return; @@ -1232,7 +1248,11 @@ namespace pdr { } if (!m_is_dl) { - IF_VERBOSE(1, verbose_stream() << "non-diff: " << mk_pp(e, m) << "\n";); + char const* msg = "non-diff: "; + if (m_test_for_utvpi) { + msg = "non-utvpi: "; + } + IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";); } } @@ -1248,6 +1268,16 @@ namespace pdr { return test.is_dl(); } + bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { + test_diff_logic test(m); + test.test_for_utvpi(); + expr_fast_mark1 mark; + for (unsigned i = 0; i < num_fmls; ++i) { + quick_for_each_expr(test, mark, fmls[i]); + } + return test.is_dl(); + } + } template class rewriter_tpl; diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h index ddbf0d122..5f2d22b76 100644 --- a/src/muz_qe/pdr_util.h +++ b/src/muz_qe/pdr_util.h @@ -151,6 +151,8 @@ namespace pdr { bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); + bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); + } #endif diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp index 369c3aae6..36e721b5c 100644 --- a/src/muz_qe/proof_utils.cpp +++ b/src/muz_qe/proof_utils.cpp @@ -1,6 +1,7 @@ #include "dl_util.h" #include "proof_utils.h" #include "ast_smt2_pp.h" +#include "var_subst.h" class reduce_hypotheses { typedef obj_hashtable expr_set; @@ -517,3 +518,93 @@ void proof_utils::permute_unit_resolution(proof_ref& pr) { obj_map cache; ::permute_unit_resolution(refs, cache, pr); } + +class push_instantiations_up_cl { + ast_manager& m; +public: + push_instantiations_up_cl(ast_manager& m): m(m) {} + + void operator()(proof_ref& p) { + expr_ref_vector s0(m); + p = push(p, s0); + } + +private: + + proof* push(proof* p, expr_ref_vector const& sub) { + proof_ref_vector premises(m); + expr_ref conclusion(m); + svector > positions; + vector substs; + + if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) { + for (unsigned i = 0; i < premises.size(); ++i) { + compose(substs[i], sub); + premises[i] = push(premises[i].get(), substs[i]); + substs[i].reset(); + } + instantiate(sub, conclusion); + return + m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, + positions, + substs); + } + if (sub.empty()) { + return p; + } + if (m.is_modus_ponens(p)) { + SASSERT(m.get_num_parents(p) == 2); + proof* p0 = m.get_parent(p, 0); + proof* p1 = m.get_parent(p, 1); + if (m.get_fact(p0) == m.get_fact(p)) { + return push(p0, sub); + } + expr* e1, *e2; + if (m.is_rewrite(p1, e1, e2) && + is_quantifier(e1) && is_quantifier(e2) && + to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) { + expr_ref r1(e1,m), r2(e2,m); + instantiate(sub, r1); + instantiate(sub, r2); + p1 = m.mk_rewrite(r1, r2); + return m.mk_modus_ponens(push(p0, sub), p1); + } + } + premises.push_back(p); + substs.push_back(sub); + conclusion = m.get_fact(p); + instantiate(sub, conclusion); + return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs); + } + + void compose(expr_ref_vector& sub, expr_ref_vector const& s0) { + for (unsigned i = 0; i < sub.size(); ++i) { + expr_ref e(m); + var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e); + sub[i] = e; + } + } + + void instantiate(expr_ref_vector const& sub, expr_ref& fml) { + if (sub.empty()) { + return; + } + if (!is_forall(fml)) { + return; + } + quantifier* q = to_quantifier(fml); + if (q->get_num_decls() != sub.size()) { + TRACE("proof_utils", tout << "quantifier has different number of variables than substitution"; + tout << mk_pp(q, m) << "\n"; + tout << sub.size() << "\n";); + return; + } + var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml); + } + +}; + +void proof_utils::push_instantiations_up(proof_ref& pr) { + push_instantiations_up_cl push(pr.get_manager()); + push(pr); +} diff --git a/src/muz_qe/proof_utils.h b/src/muz_qe/proof_utils.h index 53a38592e..dc3cdc3ef 100644 --- a/src/muz_qe/proof_utils.h +++ b/src/muz_qe/proof_utils.h @@ -36,6 +36,12 @@ public: */ static void permute_unit_resolution(proof_ref& pr); + /** + \brief Push instantiations created in hyper-resolutions up to leaves. + This produces a "ground" proof where leaves are annotated by instantiations. + */ + static void push_instantiations_up(proof_ref& pr); + }; #endif diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index ff49584ff..50c3347ee 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -2525,15 +2525,15 @@ public: m_params(p) { m_imp = alloc(imp, m, p); } - - virtual tactic * translate(ast_manager & m) { - return alloc(qe_lite_tactic, m, m_params); - } virtual ~qe_lite_tactic() { dealloc(m_imp); } + virtual tactic * translate(ast_manager & m) { + return alloc(qe_lite_tactic, m, m_params); + } + virtual void updt_params(params_ref const & p) { m_params = p; // m_imp->updt_params(p); diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index ef5639279..b42adca79 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -40,7 +40,9 @@ namespace datalog { rule_set m_rules; decl_set m_preds; bool m_was_closed; + public: + scoped_query(context& ctx): m_ctx(ctx), m_rules(ctx.get_rules()), @@ -51,6 +53,7 @@ namespace datalog { ctx.reopen(); } } + ~scoped_query() { m_ctx.reopen(); m_ctx.restrict_predicates(m_preds); @@ -179,9 +182,7 @@ namespace datalog { scoped_query.reset(); } m_context.record_transformed_rules(); - TRACE("dl", m_ectx.report_big_relations(100, tout);); - m_code.process_all_costs(); - m_code.make_annotations(m_ectx); + TRACE("dl", display_profile(tout);); return result; } @@ -236,7 +237,6 @@ namespace datalog { query_pred = rm.mk_query(query, m_context.get_rules()); } catch (default_exception& exn) { - m_context.close(); m_context.set_status(INPUT_ERROR); throw exn; } @@ -480,7 +480,10 @@ namespace datalog { get_rmanager().display(out); } - void rel_context::display_profile(std::ostream& out) const { + void rel_context::display_profile(std::ostream& out) { + m_code.make_annotations(m_ectx); + m_code.process_all_costs(); + out << "\n--------------\n"; out << "Instructions\n"; m_code.display(*this, out); diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 3e019cb50..8e4c6f2de 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -105,7 +105,7 @@ namespace datalog { void display_output_facts(rule_set const& rules, std::ostream & out) const; void display_facts(std::ostream & out) const; - void display_profile(std::ostream& out) const; + void display_profile(std::ostream& out); lbool saturate(); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 0698f4eaf..b5af6353e 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1159,7 +1159,7 @@ namespace smt2 { m_num_expr_frames++; unsigned num_vars = parse_sorted_vars(); if (num_vars == 0) - throw parser_exception("invalied quantifier, list of sorted variables is empty"); + throw parser_exception("invalid quantifier, list of sorted variables is empty"); } symbol parse_indexed_identifier_core() { diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 49d7313d1..f6576a41f 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -118,7 +118,7 @@ const edge_id null_edge_id = -1; template class dl_graph { - struct statistics { + struct stats { unsigned m_propagation_cost; unsigned m_implied_literal_cost; unsigned m_num_implied_literals; @@ -131,16 +131,16 @@ class dl_graph { m_num_helpful_implied_literals = 0; m_num_relax = 0; } - statistics() { reset(); } - void display(std::ostream& out) const { - out << "num. prop. steps. " << m_propagation_cost << "\n"; - out << "num. impl. steps. " << m_implied_literal_cost << "\n"; - out << "num. impl. lits. " << m_num_implied_literals << "\n"; - out << "num. impl. conf lits. " << m_num_helpful_implied_literals << "\n"; - out << "num. bound relax. " << m_num_relax << "\n"; + stats() { reset(); } + void collect_statistics(::statistics& st) const { + st.update("dl prop steps", m_propagation_cost); + st.update("dl impl steps", m_implied_literal_cost); + st.update("dl impl lits", m_num_implied_literals); + st.update("dl impl conf lits", m_num_helpful_implied_literals); + st.update("dl bound relax", m_num_relax); } }; - statistics m_stats; + stats m_stats; typedef typename Ext::numeral numeral; typedef typename Ext::explanation explanation; typedef vector assignment; @@ -264,7 +264,6 @@ class dl_graph { m_assignment[e.get_target()] - m_assignment[e.get_source()] <= e.get_weight(); } - public: // An assignment is feasible if all edges are feasible. bool is_feasible() const { @@ -472,8 +471,9 @@ public: m_bw(m_mark) { } - void display_statistics(std::ostream& out) const { - m_stats.display(out); + + void collect_statistics(::statistics& st) const { + m_stats.collect_statistics(st); } // Create/Initialize a variable with the given id. @@ -655,10 +655,8 @@ public: throw default_exception("edges are not inconsistent"); } -#if 1 - // experimental feature: + // allow theory to introduce shortcut lemmas. prune_edges(edges, f); -#endif for (unsigned i = 0; i < edges.size(); ++i) { edge const& e = m_edges[edges[i]]; @@ -752,7 +750,6 @@ public: f.new_edge(src, dst, idx2-idx1+1, edges.begin()+idx1); } - // Create a new scope. // That is, save the number of edges in the graph. void push() { @@ -1643,7 +1640,3 @@ public: #endif /* _DIFF_LOGIC_H_ */ -#if 0 - - -#endif diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 52fef8ca4..30bc65b6d 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -26,7 +26,9 @@ enum arith_solver_id { AS_NO_ARITH, AS_DIFF_LOGIC, AS_ARITH, - AS_DENSE_DIFF_LOGIC + AS_DENSE_DIFF_LOGIC, + AS_UTVPI, + AS_HORN }; enum bound_prop_mode { diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 1f020cdd3..f91a58f87 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -22,6 +22,8 @@ Revision History: #include"theory_arith.h" #include"theory_dense_diff_logic.h" #include"theory_diff_logic.h" +#include"theory_horn_ineq.h" +#include"theory_utvpi.h" #include"theory_array.h" #include"theory_array_full.h" #include"theory_bv.h" @@ -723,6 +725,18 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params)); } break; + case AS_HORN: + if (m_params.m_arith_int_only) + m_context.register_plugin(alloc(smt::theory_ihi, m_manager)); + else + m_context.register_plugin(alloc(smt::theory_rhi, m_manager)); + break; + case AS_UTVPI: + if (m_params.m_arith_int_only) + m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager)); + else + m_context.register_plugin(alloc(smt::theory_rutvpi, m_manager)); + break; default: if (m_params.m_arith_int_only) m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 4140f683c..7302ccfd4 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -46,7 +46,6 @@ namespace smt { unsigned m_num_conflicts; unsigned m_num_assertions; unsigned m_num_th2core_eqs; - unsigned m_num_th2core_prop; unsigned m_num_core2th_eqs; unsigned m_num_core2th_diseqs; @@ -59,109 +58,30 @@ namespace smt { } }; - class dl_conflict : public simple_justification { - public: - dl_conflict(region & r, unsigned nls, literal const * lits): simple_justification(r, nls, lits) { } - - virtual proof * mk_proof(conflict_resolution & cr) { - NOT_IMPLEMENTED_YET(); - return 0; - } - }; - - template class theory_diff_logic : public theory, private Ext { typedef typename Ext::numeral numeral; - class implied_eq_justification : public justification { - theory_diff_logic & m_theory; - theory_var m_v1; - theory_var m_v2; - unsigned m_timestamp; - public: - implied_eq_justification(theory_diff_logic & theory, theory_var v1, theory_var v2, unsigned ts): - m_theory(theory), - m_v1(v1), - m_v2(v2), - m_timestamp(ts) { - } - - virtual void get_antecedents(conflict_resolution & cr) { - m_theory.get_eq_antecedents(m_v1, m_v2, m_timestamp, cr); - } - - virtual proof * mk_proof(conflict_resolution & cr) { NOT_IMPLEMENTED_YET(); return 0; } - }; - - class implied_bound_justification : public justification { - theory_diff_logic& m_theory; - edge_id m_subsumed_edge; - edge_id m_bridge_edge; - public: - implied_bound_justification(theory_diff_logic & theory, edge_id se, edge_id be): - m_theory(theory), - m_subsumed_edge(se), - m_bridge_edge(be) { - } - - virtual void get_antecedents(conflict_resolution & cr) { - m_theory.get_implied_bound_antecedents(m_bridge_edge, m_subsumed_edge, cr); - } - - virtual proof * mk_proof(conflict_resolution & cr) { NOT_IMPLEMENTED_YET(); return 0; } - }; - - enum atom_kind { - LE_ATOM, - EQ_ATOM - }; - class atom { - protected: - atom_kind m_kind; bool_var m_bvar; bool m_true; + int m_pos; + int m_neg; public: - atom(atom_kind k, bool_var bv) : m_kind(k), m_bvar(bv), m_true(false) {} - virtual ~atom() {} - atom_kind kind() const { return m_kind; } - bool_var get_bool_var() const { return m_bvar; } - bool is_true() const { return m_true; } - void assign_eh(bool is_true) { m_true = is_true; } - virtual std::ostream& display(theory_diff_logic const& th, std::ostream& out) const; - }; - - class le_atom : public atom { - int m_pos; - int m_neg; - public: - le_atom(bool_var bv, int pos, int neg): - atom(LE_ATOM, bv), + atom(bool_var bv, int pos, int neg): + m_bvar(bv), m_true(false), m_pos(pos), m_neg(neg) { } - virtual ~le_atom() {} + ~atom() {} + bool_var get_bool_var() const { return m_bvar; } + bool is_true() const { return m_true; } + void assign_eh(bool is_true) { m_true = is_true; } int get_asserted_edge() const { return this->m_true?m_pos:m_neg; } int get_pos() const { return m_pos; } int get_neg() const { return m_neg; } - virtual std::ostream& display(theory_diff_logic const& th, std::ostream& out) const; - }; - - class eq_atom : public atom { - app_ref m_le; - app_ref m_ge; - public: - eq_atom(bool_var bv, app_ref& le, app_ref& ge): - atom(EQ_ATOM, bv), - m_le(le), - m_ge(ge) - {} - virtual ~eq_atom() {} - virtual std::ostream& display(theory_diff_logic const& th, std::ostream& out) const; - app* get_le() const { return m_le.get(); } - app* get_ge() const { return m_ge.get(); } + std::ostream& display(theory_diff_logic const& th, std::ostream& out) const; }; typedef ptr_vector atoms; @@ -239,19 +159,7 @@ namespace smt { unsigned m_asserted_qhead_old; }; - class theory_diff_logic_del_eh : public clause_del_eh { - theory_diff_logic& m_super; - public: - theory_diff_logic_del_eh(theory_diff_logic& s) : m_super(s) {} - virtual ~theory_diff_logic_del_eh() {} - virtual void operator()(ast_manager&, clause* cls) { - TRACE("dl_activity", tout << "deleting " << cls << "\n";); - m_super.del_clause_eh(cls); - dealloc(this); - } - }; - - smt_params & m_params; + smt_params & m_params; arith_util m_util; arith_eq_adapter m_arith_eq_adapter; theory_diff_logic_statistics m_stats; @@ -259,8 +167,6 @@ namespace smt { theory_var m_zero_int; // cache the variable representing the zero variable. theory_var m_zero_real; // cache the variable representing the zero variable. int_vector m_scc_id; // Cheap equality propagation - bool m_modified_since_eq_prop; // true if new constraints were asserted - // since last eq propagation. eq_prop_info_set m_eq_prop_info_set; // set of existing equality prop infos ptr_vector m_eq_prop_infos; @@ -289,20 +195,14 @@ namespace smt { virtual theory_var mk_var(enode* n); virtual theory_var mk_var(app* n); - - void mark_as_modified_since_eq_prop(); - - void unmark_as_modified_since_eq_prop(); - - bool propagate_cheap_equalities(); - + void compute_delta(); void found_non_diff_logic_expr(expr * n); - bool is_interpreted(app* n) const; - - void del_clause_eh(clause* cls); + bool is_interpreted(app* n) const { + return get_family_id() == n->get_family_id(); + } public: theory_diff_logic(ast_manager& m, smt_params & params): @@ -312,7 +212,6 @@ namespace smt { m_arith_eq_adapter(*this, params, m_util), m_zero_int(null_theory_var), m_zero_real(null_theory_var), - m_modified_since_eq_prop(false), m_asserted_qhead(0), m_num_core_conflicts(0), m_num_propagation_calls(0), @@ -323,7 +222,7 @@ namespace smt { m_nc_functor(*this) { } - ~theory_diff_logic() { + virtual ~theory_diff_logic() { reset_eh(); } @@ -360,7 +259,7 @@ namespace smt { m_arith_eq_adapter.restart_eh(); } - virtual void relevant_eh(app* e); + virtual void relevant_eh(app* e) {} virtual void init_search_eh() { m_arith_eq_adapter.init_search_eh(); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 9f2c97a84..20448dc74 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -31,34 +31,15 @@ Revision History: using namespace smt; + template -std::ostream& theory_diff_logic::atom::display(theory_diff_logic const& th, std::ostream& out) const { +std::ostream& theory_diff_logic::atom::display(theory_diff_logic const& th, std::ostream& out) const { context& ctx = th.get_context(); lbool asgn = ctx.get_assignment(m_bvar); //SASSERT(asgn == l_undef || ((asgn == l_true) == m_true)); bool sign = (l_undef == asgn) || m_true; return out << literal(m_bvar, sign) << " " << mk_pp(ctx.bool_var2expr(m_bvar), th.get_manager()) << " "; -} - -template -std::ostream& theory_diff_logic::eq_atom::display(theory_diff_logic const& th, std::ostream& out) const { - atom::display(th, out); - lbool asgn = th.get_context().get_assignment(this->m_bvar); - if (l_undef == asgn) { - out << "unassigned\n"; - } - else { - out << mk_pp(m_le.get(), m_le.get_manager()) << " " - << mk_pp(m_ge.get(), m_ge.get_manager()) << "\n"; - } - return out; -} - -template -std::ostream& theory_diff_logic::le_atom::display(theory_diff_logic const& th, std::ostream& out) const { - atom::display(th, out); - lbool asgn = th.get_context().get_assignment(this->m_bvar); if (l_undef == asgn) { out << "unassigned\n"; } @@ -94,7 +75,6 @@ void theory_diff_logic::init(context * ctx) { e = ctx->mk_enode(zero, false, false, true); SASSERT(!is_attached_to_var(e)); m_zero_real = mk_var(e); - } @@ -277,7 +257,7 @@ bool theory_diff_logic::internalize_atom(app * n, bool gate_ctx) { k -= this->m_epsilon; } edge_id neg = m_graph.add_edge(target, source, k, ~l); - le_atom * a = alloc(le_atom, bv, pos, neg); + atom * a = alloc(atom, bv, pos, neg); m_atoms.push_back(a); m_bool_var2atom.insert(bv, a); @@ -318,7 +298,7 @@ template void theory_diff_logic::assign_eh(bool_var v, bool is_true) { m_stats.m_num_assertions++; atom * a = 0; - m_bool_var2atom.find(v, a); + VERIFY (m_bool_var2atom.find(v, a)); SASSERT(a); SASSERT(get_context().get_assignment(v) != l_undef); SASSERT((get_context().get_assignment(v) == l_true) == is_true); @@ -330,10 +310,11 @@ void theory_diff_logic::assign_eh(bool_var v, bool is_true) { template void theory_diff_logic::collect_statistics(::statistics & st) const { st.update("dl conflicts", m_stats.m_num_conflicts); - st.update("dl propagations", m_stats.m_num_th2core_prop); st.update("dl asserts", m_stats.m_num_assertions); st.update("core->dl eqs", m_stats.m_num_core2th_eqs); + st.update("core->dl diseqs", m_stats.m_num_core2th_diseqs); m_arith_eq_adapter.collect_statistics(st); + m_graph.collect_statistics(st); } template @@ -374,15 +355,6 @@ final_check_status theory_diff_logic::final_check_eh() { // either will already be zero (as we don't do mixed constraints). m_graph.set_to_zero(m_zero_int, m_zero_real); SASSERT(is_consistent()); - - -#if 0 - TBD: - if (propagate_cheap_equalities()) { - return FC_CONTINUE; - } -#endif - if (m_non_diff_logic_exprs) { return FC_GIVEUP; } @@ -506,61 +478,14 @@ bool theory_diff_logic::propagate_atom(atom* a) { if (ctx.inconsistent()) { return false; } - switch(a->kind()) { - case LE_ATOM: { - int edge_id = dynamic_cast(a)->get_asserted_edge(); - if (!m_graph.enable_edge(edge_id)) { - set_neg_cycle_conflict(); - return false; - } -#if 0 - if (m_params.m_arith_bound_prop != BP_NONE) { - svector subsumed; - m_graph.find_subsumed1(edge_id, subsumed); - for (unsigned i = 0; i < subsumed.size(); ++i) { - int subsumed_edge_id = subsumed[i]; - literal l = m_graph.get_explanation(subsumed_edge_id); - context & ctx = get_context(); - region& r = ctx.get_region(); - ++m_stats.m_num_th2core_prop; - ctx.assign(l, new (r) implied_bound_justification(*this, subsumed_edge_id, edge_id)); - } - - } -#endif - break; - } - case EQ_ATOM: - if (!a->is_true()) { - SASSERT(ctx.get_assignment(a->get_bool_var()) == l_false); - // eq_atom * ea = dynamic_cast(a); - } - break; + int edge_id = a->get_asserted_edge(); + if (!m_graph.enable_edge(edge_id)) { + set_neg_cycle_conflict(); + return false; } return true; } - - -template -void theory_diff_logic::mark_as_modified_since_eq_prop() { - if (!m_modified_since_eq_prop) { - get_context().push_trail(value_trail(m_modified_since_eq_prop)); - m_modified_since_eq_prop = true; - } -} - -template -void theory_diff_logic::unmark_as_modified_since_eq_prop() { - get_context().push_trail(value_trail(m_modified_since_eq_prop)); - m_modified_since_eq_prop = false; -} - -template -void theory_diff_logic::del_clause_eh(clause* cls) { - -} - template void theory_diff_logic::new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) { @@ -609,7 +534,7 @@ void theory_diff_logic::new_edge(dl_var src, dl_var dst, unsigned num_edges atom* a = 0; m_bool_var2atom.find(bv, a); SASSERT(a); - edge_id e_id = static_cast(a)->get_pos(); + edge_id e_id = a->get_pos(); literal_vector lits; for (unsigned i = 0; i < num_edges; ++i) { @@ -633,11 +558,7 @@ void theory_diff_logic::new_edge(dl_var src, dl_var dst, unsigned num_edges lits.size(), lits.c_ptr(), params.size(), params.c_ptr()); } - clause_del_eh* del_eh = alloc(theory_diff_logic_del_eh, *this); - clause* cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, del_eh); - if (!cls) { - dealloc(del_eh); - } + clause* cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); if (dump_lemmas()) { char const * logic = m_is_lia ? "QF_LIA" : "QF_LRA"; ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic); @@ -677,7 +598,6 @@ void theory_diff_logic::set_neg_cycle_conflict() { literal_vector const& lits = m_nc_functor.get_lits(); context & ctx = get_context(); TRACE("arith_conflict", - //display(tout); tout << "conflict: "; for (unsigned i = 0; i < lits.size(); ++i) { ctx.display_literal_info(tout, lits[i]); @@ -802,7 +722,6 @@ theory_var theory_diff_logic::mk_num(app* n, rational const& r) { template theory_var theory_diff_logic::mk_var(enode* n) { - mark_as_modified_since_eq_prop(); theory_var v = theory::mk_var(n); TRACE("diff_logic_vars", tout << "mk_var: " << v << "\n";); m_graph.init_var(v); @@ -810,10 +729,6 @@ theory_var theory_diff_logic::mk_var(enode* n) { return v; } -template -bool theory_diff_logic::is_interpreted(app* n) const { - return n->get_family_id() == get_family_id(); -} template theory_var theory_diff_logic::mk_var(app* n) { @@ -854,7 +769,6 @@ void theory_diff_logic::reset_eh() { m_asserted_atoms .reset(); m_stats .reset(); m_scopes .reset(); - m_modified_since_eq_prop = false; m_asserted_qhead = 0; m_num_core_conflicts = 0; m_num_propagation_calls = 0; @@ -865,70 +779,6 @@ void theory_diff_logic::reset_eh() { } -template -bool theory_diff_logic::propagate_cheap_equalities() { - bool result = false; - TRACE("dl_new_eq", get_context().display(tout);); - context& ctx = get_context(); - region& reg = ctx.get_region(); - SASSERT(m_eq_prop_info_set.empty()); - SASSERT(m_eq_prop_infos.empty()); - if (m_modified_since_eq_prop) { - m_graph.compute_zero_edge_scc(m_scc_id); - int n = get_num_vars(); - for (theory_var v = 0; v < n; v++) { - rational delta_r; - theory_var x_v = expand(true, v, delta_r); - numeral delta(delta_r); - int scc_id = m_scc_id[x_v]; - if (scc_id != -1) { - delta += m_graph.get_assignment(x_v); - TRACE("eq_scc", tout << v << " " << x_v << " " << scc_id << " " << delta << "\n";); - eq_prop_info info(scc_id, delta); - typename eq_prop_info_set::entry * entry = m_eq_prop_info_set.find_core(&info); - if (entry == 0) { - eq_prop_info * new_info = alloc(eq_prop_info, scc_id, delta, v); - m_eq_prop_info_set.insert(new_info); - m_eq_prop_infos.push_back(new_info); - } - else { - // new equality found - theory_var r = entry->get_data()->get_root(); - - enode * n1 = get_enode(v); - enode * n2 = get_enode(r); - if (n1->get_root() != n2->get_root()) { - // r may be an alias (i.e., it is not realy in the graph). So, I should expand it. - // nsb: ?? - rational r_delta; - theory_var x_r = expand(true, r, r_delta); - - justification* j = new (reg) implied_eq_justification(*this, x_v, x_r, m_graph.get_timestamp()); - (void)j; - - m_stats.m_num_th2core_eqs++; - // TBD: get equality into core. - - NOT_IMPLEMENTED_YET(); - // new_eq_eh(x_v, x_r, *j); - result = true; - } - } - } - } - m_eq_prop_info_set.reset(); - std::for_each(m_eq_prop_infos.begin(), m_eq_prop_infos.end(), delete_proc()); - m_eq_prop_infos.reset(); - unmark_as_modified_since_eq_prop(); - } - - TRACE("dl_new_eq", get_context().display(tout);); - SASSERT(!m_modified_since_eq_prop); - - return result; -} - - template void theory_diff_logic::compute_delta() { m_delta = rational(1); @@ -1001,30 +851,9 @@ bool theory_diff_logic::is_consistent() const { lbool asgn = ctx.get_assignment(bv); if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) { SASSERT((asgn == l_true) == a->is_true()); - switch(a->kind()) { - case LE_ATOM: { - le_atom* le = dynamic_cast(a); - int edge_id = le->get_asserted_edge(); - SASSERT(m_graph.is_enabled(edge_id)); - SASSERT(m_graph.is_feasible(edge_id)); - break; - } - case EQ_ATOM: { - eq_atom* ea = dynamic_cast(a); - bool_var bv1 = ctx.get_bool_var(ea->get_le()); - bool_var bv2 = ctx.get_bool_var(ea->get_ge()); - lbool val1 = ctx.get_assignment(bv1); - lbool val2 = ctx.get_assignment(bv2); - if (asgn == l_true) { - SASSERT(val1 == l_true); - SASSERT(val2 == l_true); - } - else { - SASSERT(val1 == l_false || val2 == l_false); - } - break; - } - } + int edge_id = a->get_asserted_edge(); + SASSERT(m_graph.is_enabled(edge_id)); + SASSERT(m_graph.is_feasible(edge_id)); } } return m_graph.is_feasible(); @@ -1087,7 +916,6 @@ void theory_diff_logic::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v // assign the corresponding equality literal. // - mark_as_modified_since_eq_prop(); app_ref eq(m), s2(m), t2(m); app* s1 = get_enode(s)->get_owner(); @@ -1142,10 +970,6 @@ void theory_diff_logic::new_diseq_eh(theory_var v1, theory_var v2) { } -template -void theory_diff_logic::relevant_eh(app* e) { -} - struct imp_functor { conflict_resolution & m_cr; diff --git a/src/smt/theory_horn_ineq.cpp b/src/smt/theory_horn_ineq.cpp new file mode 100644 index 000000000..978b5b003 --- /dev/null +++ b/src/smt/theory_horn_ineq.cpp @@ -0,0 +1,236 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_horn_ineq.h + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-18 + +Revision History: + + The implementaton is derived from theory_diff_logic. + +--*/ +#include "theory_horn_ineq.h" +#include "theory_horn_ineq_def.h" + +namespace smt { + + template class theory_horn_ineq; + template class theory_horn_ineq; + + // similar to test_diff_logic: + + horn_ineq_tester::horn_ineq_tester(ast_manager& m): m(m), a(m) {} + + bool horn_ineq_tester::operator()(expr* e) { + m_todo.reset(); + m_pols.reset(); + pos_mark.reset(); + neg_mark.reset(); + m_todo.push_back(e); + m_pols.push_back(l_true); + while (!m_todo.empty()) { + expr* e = m_todo.back(); + lbool p = m_pols.back(); + m_todo.pop_back(); + m_pols.pop_back(); + switch (p) { + case l_true: + if (pos_mark.is_marked(e)) { + continue; + } + pos_mark.mark(e, true); + break; + case l_false: + if (neg_mark.is_marked(e)) { + continue; + } + neg_mark.mark(e, true); + break; + case l_undef: + if (pos_mark.is_marked(e) && neg_mark.is_marked(e)) { + continue; + } + pos_mark.mark(e, true); + neg_mark.mark(e, true); + break; + } + if (!test_expr(p, e)) { + return false; + } + } + return true; + } + + vector > const& horn_ineq_tester::get_linearization() const { + return m_terms; + } + + bool horn_ineq_tester::test_expr(lbool p, expr* e) { + expr* e1, *e2, *e3; + if (is_var(e)) { + return true; + } + if (!is_app(e)) { + return false; + } + app* ap = to_app(e); + if (m.is_and(ap) || m.is_or(ap)) { + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + m_todo.push_back(ap->get_arg(i)); + m_pols.push_back(p); + } + } + else if (m.is_not(e, e1)) { + m_todo.push_back(e); + m_pols.push_back(~p); + } + else if (m.is_ite(e, e1, e2, e3)) { + m_todo.push_back(e1); + m_pols.push_back(l_undef); + m_todo.push_back(e2); + m_pols.push_back(p); + m_todo.push_back(e3); + m_pols.push_back(p); + } + else if (m.is_iff(e, e1, e2)) { + m_todo.push_back(e1); + m_pols.push_back(l_undef); + m_todo.push_back(e2); + m_pols.push_back(l_undef); + m_todo.push_back(e2); + } + else if (m.is_implies(e, e1, e2)) { + m_todo.push_back(e1); + m_pols.push_back(~p); + m_todo.push_back(e2); + m_pols.push_back(p); + } + else if (m.is_eq(e, e1, e2)) { + return linearize(e1, e2) == diff; + } + else if (m.is_true(e) || m.is_false(e)) { + // no-op + } + else if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1) || + a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) { + if (p == l_false) { + std::swap(e2, e1); + } + classify_t cl = linearize(e1, e2); + switch(p) { + case l_undef: + return cl == diff; + case l_true: + case l_false: + return cl == horn || cl == diff; + } + } + else if (!is_uninterp_const(e)) { + return false; + } + return true; + } + + bool horn_ineq_tester::operator()(unsigned num_fmls, expr* const* fmls) { + for (unsigned i = 0; i < num_fmls; ++i) { + if (!(*this)(fmls[i])) { + return false; + } + } + return true; + } + + horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e) { + m_terms.reset(); + m_terms.push_back(std::make_pair(e, rational(1))); + return linearize(); + } + + horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e1, expr* e2) { + m_terms.reset(); + m_terms.push_back(std::make_pair(e1, rational(1))); + m_terms.push_back(std::make_pair(e2, rational(-1))); + return linearize(); + } + + horn_ineq_tester::classify_t horn_ineq_tester::linearize() { + + m_weight.reset(); + m_coeff_map.reset(); + + while (!m_terms.empty()) { + expr* e1, *e2; + rational num; + rational mul = m_terms.back().second; + expr* e = m_terms.back().first; + m_terms.pop_back(); + if (a.is_add(e)) { + for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { + m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul)); + } + } + else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) { + m_terms.push_back(std::make_pair(e2, mul*num)); + } + else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) { + m_terms.push_back(std::make_pair(e2, mul*num)); + } + else if (a.is_sub(e, e1, e2)) { + m_terms.push_back(std::make_pair(e1, mul)); + m_terms.push_back(std::make_pair(e2, -mul)); + } + else if (a.is_uminus(e, e1)) { + m_terms.push_back(std::make_pair(e1, -mul)); + } + else if (a.is_numeral(e, num)) { + m_weight += num*mul; + } + else if (a.is_to_real(e, e1)) { + m_terms.push_back(std::make_pair(e1, mul)); + } + else if (!is_uninterp_const(e)) { + return non_horn; + } + else { + m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul; + } + } + unsigned num_negative = 0; + unsigned num_positive = 0; + bool is_unit_pos = true, is_unit_neg = true; + obj_map::iterator it = m_coeff_map.begin(); + obj_map::iterator end = m_coeff_map.end(); + for (; it != end; ++it) { + rational r = it->m_value; + if (r.is_zero()) { + continue; + } + m_terms.push_back(std::make_pair(it->m_key, r)); + if (r.is_pos()) { + is_unit_pos = is_unit_pos && r.is_one(); + num_positive++; + } + else { + is_unit_neg = is_unit_neg && r.is_minus_one(); + num_negative++; + } + } + if (num_negative <= 1 && is_unit_pos && is_unit_neg && num_positive <= 1) { + return diff; + } + if (num_positive <= 1 && is_unit_pos) { + return horn; + } + if (num_negative <= 1 && is_unit_neg) { + return co_horn; + } + return non_horn; + } + + +} diff --git a/src/smt/theory_horn_ineq.h b/src/smt/theory_horn_ineq.h new file mode 100644 index 000000000..fac6e96df --- /dev/null +++ b/src/smt/theory_horn_ineq.h @@ -0,0 +1,329 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_horn_ineq.h + +Abstract: + + A*x <= weight + D*x, coefficients to A and D are non-negative, + D is a diagonal matrix. + Coefficients to weight may have both signs. + + Label variables by weight. + Select inequality that is not satisfied. + Set delta(LHS) := 0 + Set delta(RHS(x)) := weight(x) - b + Propagate weight increment through inequalities. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-18 + +Revision History: + + The implementaton is derived from theory_diff_logic. + +--*/ + +#ifndef _THEORY_HORN_INEQ_H_ +#define _THEORY_HORN_INEQ_H_ + +#include"rational.h" +#include"inf_rational.h" +#include"inf_int_rational.h" +#include"inf_eps_rational.h" +#include"smt_theory.h" +#include"arith_decl_plugin.h" +#include"smt_justification.h" +#include"map.h" +#include"smt_params.h" +#include"arith_eq_adapter.h" +#include"smt_model_generator.h" +#include"numeral_factory.h" +#include"smt_clause.h" + +namespace smt { + + class horn_ineq_tester { + ast_manager& m; + arith_util a; + ptr_vector m_todo; + svector m_pols; + ast_mark pos_mark, neg_mark; + obj_map m_coeff_map; + rational m_weight; + vector > m_terms; + + public: + enum classify_t { + co_horn, + horn, + diff, + non_horn + }; + horn_ineq_tester(ast_manager& m); + + // test if formula is in the Horn inequality fragment: + bool operator()(expr* fml); + bool operator()(unsigned num_fmls, expr* const* fmls); + + // linearize inequality/equality + classify_t linearize(expr* e); + classify_t linearize(expr* e1, expr* e2); + + // retrieve linearization + vector > const& get_linearization() const; + rational const& get_weight() const { return m_weight; } + private: + bool test_expr(lbool p, expr* e); + classify_t linearize(); + }; + + template + class theory_horn_ineq : public theory, private Ext { + + typedef typename Ext::numeral numeral; + typedef typename Ext::inf_numeral inf_numeral; + typedef literal explanation; + typedef theory_var th_var; + typedef svector th_var_vector; + typedef unsigned clause_id; + typedef vector > coeffs; + static const clause_id null_clause_id = UINT_MAX; + + class clause; + class graph; + class assignment_trail; + class parent_trail; + + class atom { + protected: + bool_var m_bvar; + bool m_true; + int m_pos; + int m_neg; + public: + atom(bool_var bv, int pos, int neg) : + m_bvar(bv), m_true(false), + m_pos(pos), m_neg(neg) {} + virtual ~atom() {} + bool_var get_bool_var() const { return m_bvar; } + bool is_true() const { return m_true; } + void assign_eh(bool is_true) { m_true = is_true; } + int get_asserted_edge() const { return this->m_true?m_pos:m_neg; } + int get_pos() const { return m_pos; } + int get_neg() const { return m_neg; } + std::ostream& display(theory_horn_ineq const& th, std::ostream& out) const; + }; + typedef svector atoms; + + struct scope { + unsigned m_atoms_lim; + unsigned m_asserted_atoms_lim; + unsigned m_asserted_qhead_old; + }; + + struct stats { + unsigned m_num_conflicts; + unsigned m_num_assertions; + unsigned m_num_core2th_eqs; + unsigned m_num_core2th_diseqs; + + void reset() { + memset(this, 0, sizeof(*this)); + } + + stats() { + reset(); + } + }; + + stats m_stats; + smt_params m_params; + arith_util a; + arith_eq_adapter m_arith_eq_adapter; + th_var m_zero_int; // cache the variable representing the zero variable. + th_var m_zero_real; // cache the variable representing the zero variable. + + graph* m_graph; + atoms m_atoms; + unsigned_vector m_asserted_atoms; // set of asserted atoms + unsigned m_asserted_qhead; + u_map m_bool_var2atom; + svector m_scopes; + + double m_agility; + bool m_lia; + bool m_lra; + bool m_non_horn_ineq_exprs; + + horn_ineq_tester m_test; + + + arith_factory * m_factory; + rational m_delta; + rational m_lambda; + + + // Set a conflict due to a negative cycle. + void set_neg_cycle_conflict(); + + // Create a new theory variable. + virtual th_var mk_var(enode* n); + + virtual th_var mk_var(expr* n); + + void compute_delta(); + + void found_non_horn_ineq_expr(expr * n); + + bool is_interpreted(app* n) const { + return n->get_family_id() == get_family_id(); + } + + public: + theory_horn_ineq(ast_manager& m); + + virtual ~theory_horn_ineq(); + + virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_horn_ineq, get_manager()); } + + virtual char const * get_name() const { return "horn-inequality-logic"; } + + /** + \brief See comment in theory::mk_eq_atom + */ + virtual app * mk_eq_atom(expr * lhs, expr * rhs) { return a.mk_eq(lhs, rhs); } + + virtual void init(context * ctx); + + virtual bool internalize_atom(app * atom, bool gate_ctx); + + virtual bool internalize_term(app * term); + + virtual void internalize_eq_eh(app * atom, bool_var v); + + virtual void assign_eh(bool_var v, bool is_true); + + virtual void new_eq_eh(th_var v1, th_var v2) { + m_arith_eq_adapter.new_eq_eh(v1, v2); + } + + virtual bool use_diseqs() const { return true; } + + virtual void new_diseq_eh(th_var v1, th_var v2) { + m_arith_eq_adapter.new_diseq_eh(v1, v2); + } + + virtual void push_scope_eh(); + + virtual void pop_scope_eh(unsigned num_scopes); + + virtual void restart_eh() { + m_arith_eq_adapter.restart_eh(); + } + + virtual void relevant_eh(app* e) {} + + virtual void init_search_eh() { + m_arith_eq_adapter.init_search_eh(); + } + + virtual final_check_status final_check_eh(); + + virtual bool is_shared(th_var v) const { + return false; + } + + virtual bool can_propagate() { + SASSERT(m_asserted_qhead <= m_asserted_atoms.size()); + return m_asserted_qhead != m_asserted_atoms.size(); + } + + virtual void propagate(); + + virtual justification * why_is_diseq(th_var v1, th_var v2) { + UNREACHABLE(); + return 0; + } + + virtual void reset_eh(); + + virtual void init_model(model_generator & m); + + virtual model_value_proc * mk_value(enode * n, model_generator & mg); + + virtual bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const { + return true; + } + + virtual void display(std::ostream & out) const; + + virtual void collect_statistics(::statistics & st) const; + + private: + + virtual void new_eq_eh(th_var v1, th_var v2, justification& j) { + m_stats.m_num_core2th_eqs++; + new_eq_or_diseq(true, v1, v2, j); + } + + virtual void new_diseq_eh(th_var v1, th_var v2, justification& j) { + m_stats.m_num_core2th_diseqs++; + new_eq_or_diseq(false, v1, v2, j); + } + + void negate(coeffs& coeffs, rational& weight); + numeral mk_weight(bool is_real, bool is_strict, rational const& w) const; + void mk_coeffs(vector >const& terms, coeffs& coeffs, rational& w); + + void del_atoms(unsigned old_size); + + void propagate_core(); + + bool propagate_atom(atom const& a); + + th_var mk_term(app* n); + + th_var mk_num(app* n, rational const& r); + + bool is_consistent() const; + + th_var expand(bool pos, th_var v, rational & k); + + void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just); + + th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; } + + th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); } + + void inc_conflicts(); + + }; + + struct rhi_ext { + typedef inf_rational inf_numeral; + typedef inf_eps_rational numeral; + numeral m_epsilon; + numeral m_minus_infty; + rhi_ext() : m_epsilon(inf_rational(rational(), true)), m_minus_infty(rational(-1),inf_rational()) {} + }; + + struct ihi_ext { + typedef rational inf_numeral; + typedef inf_eps_rational numeral; + numeral m_epsilon; + numeral m_minus_infty; + ihi_ext() : m_epsilon(rational(1)), m_minus_infty(rational(-1),rational(0)) {} + }; + + typedef theory_horn_ineq theory_rhi; + typedef theory_horn_ineq theory_ihi; +}; + + + + +#endif /* _THEORY_HORN_INEQ_H_ */ diff --git a/src/smt/theory_horn_ineq_def.h b/src/smt/theory_horn_ineq_def.h new file mode 100644 index 000000000..505815b4f --- /dev/null +++ b/src/smt/theory_horn_ineq_def.h @@ -0,0 +1,1164 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_horn_ineq_def.h + +Abstract: + + A*x <= b + D*x, coefficients to A and D are non-negative, + D is a diagonal matrix. + Coefficients to b may have both signs. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-18 + +Revision History: + +--*/ + +#ifndef _THEORY_HORN_INEQ_DEF_H_ +#define _THEORY_HORN_INEQ_DEF_H_ +#include "theory_horn_ineq.h" +#include "ast_pp.h" +#include "smt_context.h" + +namespace smt { + + /** + A clause represents an inequality of the form + + v1*c1 + v2*c2 + .. + v_n*c_n + w <= v*c + + where + - m_vars: [v1,v2,...,v_n] + - m_coeffs: [c1,c2,...,c_n] + - m_var: v + - m_coeff: c + - m_weight: w + + */ + template + class theory_horn_ineq::clause { + vector m_coeffs; // coefficients of body. + svector m_vars; // variables of body. + rational m_coeff; // coefficient of head. + th_var m_var; // head variable. + numeral m_weight; // constant to add + literal m_explanation; + bool m_enabled; + public: + clause(unsigned sz, rational const* coeffs, th_var const* vars, + rational const& coeff, th_var var, numeral const& w, + const literal& ex): + m_coeffs(sz, coeffs), + m_vars(sz, vars), + m_coeff(coeff), + m_var(var), + m_weight(w), + m_explanation(ex), + m_enabled(false) { + DEBUG_CODE( + { + for (unsigned i = 0; i < size(); ++i) { + SASSERT(coeffs[i].is_pos()); + } + SASSERT(coeff.is_pos()); + }); + } + + th_var vars(unsigned i) const { return m_vars[i]; } + rational const& coeffs(unsigned i) const { return m_coeffs[i]; } + th_var var() const { return m_var; } + rational const& coeff() const { return m_coeff; } + const numeral & get_weight() const { return m_weight; } + const literal & get_explanation() const { return m_explanation; } + bool is_enabled() const { return m_enabled; } + unsigned size() const { return m_vars.size(); } + + void enable() { m_enabled = true; } + void disable() { m_enabled = false; } + + void display(std::ostream& out) const { + out << (is_enabled()?"+ ":"- "); + for (unsigned i = 0; i < size(); ++i) { + if (i > 0 && coeffs(i).is_pos()) { + out << " + "; + } + display(out, coeffs(i), vars(i)); + } + if (!get_weight().is_zero()) { + out << " + " << get_weight(); + } + display(out << " <= ", coeff(), var()); + out << "\n"; + } + + private: + + void display(std::ostream& out, rational const& c, th_var v) const { + if (!c.is_one()) { + out << c << "*"; + } + out << "v" << v; + } + }; + + template + class theory_horn_ineq::assignment_trail { + th_var m_var; + numeral m_old_value; + public: + assignment_trail(th_var v, const numeral & val): + m_var(v), + m_old_value(val) {} + th_var get_var() const { return m_var; } + const numeral & get_old_value() const { return m_old_value; } + }; + + template + class theory_horn_ineq::parent_trail { + th_var m_var; + clause_id m_old_value; + public: + parent_trail(th_var v, clause_id val): + m_var(v), + m_old_value(val) {} + th_var get_var() const { return m_var; } + clause_id get_old_value() const { return m_old_value; } + }; + + + template + class theory_horn_ineq::graph : private Ext { + + typedef vector assignment_stack; + typedef vector parent_stack; + typedef unsigned_vector clause_id_vector; + + struct stats { + unsigned m_propagation_cost; + + void reset() { + memset(this, 0, sizeof(*this)); + } + }; + + struct scope { + unsigned m_clauses_lim; + unsigned m_enabled_clauses_lim; + unsigned m_assignment_lim; + unsigned m_parent_lim; + scope(unsigned e, unsigned enabled, unsigned alim, unsigned plim): + m_clauses_lim(e), + m_enabled_clauses_lim(enabled), + m_assignment_lim(alim), + m_parent_lim(plim) { + } + }; + + stats m_stats; + vector m_clauses; + vector m_assignment; // per var + clause_id_vector m_parent; // per var + assignment_stack m_assignment_stack; // stack for restoring the assignment + parent_stack m_parent_stack; // stack for restoring parents + clause_id_vector m_enabled_clauses; + vector m_out_clauses; // use-list for clauses. + vector m_in_clauses; // clauses that have variable in head. + // forward reachability + unsigned_vector m_onstack; + unsigned m_ts; + unsigned_vector m_todo; + literal_vector m_lits; + vector m_coeffs; + th_var m_zero; + clause_id m_unsat_clause; + svector m_trail_stack; + + + public: + + graph(): m_ts(0), m_zero(null_theory_var), m_unsat_clause(null_clause_id) {} + + void reset() { + m_clauses .reset(); + m_assignment .reset(); + m_parent .reset(); + m_assignment_stack .reset(); + m_parent_stack .reset(); + m_out_clauses .reset(); + m_in_clauses .reset(); + m_enabled_clauses .reset(); + m_onstack .reset(); + m_ts = 0; + m_lits .reset(); + m_trail_stack .reset(); + m_unsat_clause = null_clause_id; + } + + + void traverse_neg_cycle1(bool /*stronger_lemmas*/) { + TRACE("horn_ineq", display(tout);); + SASSERT(!m_enabled_clauses.empty()); + clause_id id = m_unsat_clause; + SASSERT(id != null_clause_id); + SASSERT(!is_feasible(m_clauses[id])); + clause_id_vector todo; + vector muls; + todo.push_back(id); + muls.push_back(rational(1)); + u_map lits; + while (!todo.empty()) { + id = todo.back(); + rational mul = muls.back(); + todo.pop_back(); + muls.pop_back(); + clause const& cl = m_clauses[id]; + literal lit = cl.get_explanation(); + if (lit != null_literal) { + lits.insert_if_not_there2(id, rational(0))->get_data().m_value += mul; + } + for (unsigned i = 0; i < cl.size(); ++i) { + id = m_parent[cl.vars(i)]; + if (id != null_clause_id) { + todo.push_back(id); + muls.push_back(mul*cl.coeffs(i)); + } + } + } + u_map::iterator it = lits.begin(), end = lits.end(); + m_lits.reset(); + m_coeffs.reset(); + for (; it != end; ++it) { + m_lits.push_back(m_clauses[it->m_key].get_explanation()); + m_coeffs.push_back(it->m_value); + } + + // TODO: use topological sort to tune traversal of parents to linear. + // (current traversal can be exponential). + // TODO: negative cycle traversal with inline resolution to find + // stronger conflict clauses. + // follow heuristic used in theory_diff_logic_def.h: + } + + unsigned get_num_clauses() const { + return m_clauses.size(); + } + + literal_vector const& get_lits() const { + return m_lits; + } + + vector const& get_coeffs() const { + return m_coeffs; + } + + numeral get_assignment(th_var v) const { + return m_assignment[v]; + } + + numeral eval_body(clause const& cl) const { + numeral v(0); + for (unsigned i = 0; i < cl.size(); ++i) { + v += cl.coeffs(i)*m_assignment[cl.vars(i)]; + } + v += cl.get_weight(); + return v; + } + + numeral eval_body(clause_id id) const { + return eval_body(m_clauses[id]); + } + + numeral eval_head(clause_id id) const { + return eval_head(m_clauses[id]); + } + + numeral eval_head(clause const& cl) const { + return cl.coeff()*m_assignment[cl.var()]; + } + + clause const& get_clause(clause_id id) const { + return m_clauses[id]; + } + + void display_clause(std::ostream& out, clause_id id) const { + if (id == null_clause_id) { + out << "null\n"; + } + else { + m_clauses[id].display(out); + } + } + + void display(std::ostream& out) const { + for (unsigned i = 0; i < m_clauses.size(); ++i) { + display_clause(out, i); + } + for (unsigned i = 0; i < m_assignment.size(); ++i) { + out << m_assignment[i] << "\n"; + } + } + + void collect_statistics(::statistics& st) const { + st.update("hi_propagation_cst", m_stats.m_propagation_cost); + } + + void push() { + m_trail_stack.push_back(scope(m_clauses.size(), m_enabled_clauses.size(), + m_assignment_stack.size(), m_parent_stack.size())); + } + + void pop(unsigned num_scopes) { + unsigned lvl = m_trail_stack.size(); + SASSERT(num_scopes <= lvl); + unsigned new_lvl = lvl - num_scopes; + scope & s = m_trail_stack[new_lvl]; + // restore enabled clauses + for (unsigned i = m_enabled_clauses.size(); i > s.m_enabled_clauses_lim; ) { + --i; + m_clauses[m_enabled_clauses[i]].disable(); + } + m_enabled_clauses.shrink(s.m_enabled_clauses_lim); + + // restore assignment stack + for (unsigned i = m_assignment_stack.size(); i > s.m_assignment_lim; ) { + --i; + m_assignment[m_assignment_stack[i].get_var()] = m_assignment_stack[i].get_old_value(); + } + m_assignment_stack.shrink(s.m_assignment_lim); + + // restore parent stack + for (unsigned i = m_parent_stack.size(); i > s.m_parent_lim; ) { + --i; + m_parent[m_parent_stack[i].get_var()] = m_parent_stack[i].get_old_value(); + } + m_assignment_stack.shrink(s.m_assignment_lim); + + // restore clauses + unsigned old_num_clauses = s.m_clauses_lim; + unsigned num_clauses = m_clauses.size(); + SASSERT(old_num_clauses <= num_clauses); + unsigned to_delete = num_clauses - old_num_clauses; + for (unsigned i = 0; i < to_delete; i++) { + const clause & cl = m_clauses.back(); + TRACE("horn_ineq", tout << "deleting clause:\n"; cl.display(tout);); + for (unsigned j = 0; j < cl.size(); ++j) { + m_out_clauses[cl.vars(j)].pop_back(); + } + m_in_clauses[cl.var()].pop_back(); + m_clauses.pop_back(); + } + m_trail_stack.shrink(new_lvl); + SASSERT(check_invariant()); + } + + /** + \brief Add clause z <= z and the assignment z := 0 + Then z cannot be incremented without causing a loop (and therefore a contradiction). + */ + void set_to_zero(th_var z) { + m_zero = z; + } + + bool enable_clause(clause_id id) { + if (id == null_clause_id) { + return true; + } + clause& cl = m_clauses[id]; + bool r = true; + if (!cl.is_enabled()) { + cl.enable(); + if (!is_feasible(cl)) { + r = make_feasible(id); + } + m_enabled_clauses.push_back(id); + } + return r; + } + + void init_var(th_var v) { + unsigned sz = static_cast(v); + while (m_assignment.size() <= sz) { + m_assignment.push_back(Ext::m_minus_infty); + m_out_clauses.push_back(clause_id_vector()); + m_in_clauses.push_back(clause_id_vector()); + m_parent.push_back(null_clause_id); + m_onstack.push_back(0); + } + m_assignment[v] = Ext::m_minus_infty; + SASSERT(m_out_clauses[v].empty()); + SASSERT(m_in_clauses[v].empty()); + SASSERT(check_invariant()); + } + + clause_id add_ineq(vector > const& terms, numeral const& weight, literal l) { + vector coeffs; + svector vars; + rational coeff(1); + th_var var = null_theory_var; + bool found_negative = false; + for (unsigned i = 0; i < terms.size(); ++i) { + rational const& r = terms[i].second; + if (r.is_pos()) { + coeffs.push_back(terms[i].second); + vars.push_back(terms[i].first); + } + else if (found_negative) { + return null_clause_id; + } + else { + SASSERT(r.is_neg()); + found_negative = true; + coeff = -r; + var = terms[i].first; + } + } + if (!found_negative) { + coeff = rational(1); + var = m_zero; + } + if (!coeff.is_one()) { + // so far just support unit coefficients on right. + return null_clause_id; + } + clause_id id = m_clauses.size(); + m_clauses.push_back(clause(coeffs.size(), coeffs.c_ptr(), vars.c_ptr(), coeff, var, weight, l)); + for (unsigned i = 0; i < vars.size(); ++i) { + m_out_clauses[vars[i]].push_back(id); + } + m_in_clauses[var].push_back(id); + + return id; + } + + bool is_feasible() const { + for (unsigned i = 0; i < m_clauses.size(); ++i) { + if (!is_feasible(m_clauses[i])) { + return false; + } + } + return true; + } + + private: + + bool check_invariant() { + return true; + } + + /** + assignments are fully retraced on backtracking. + This is not always necessary. + */ + + void acc_assignment(th_var v, const numeral & inc) { + m_assignment_stack.push_back(assignment_trail(v, m_assignment[v])); + m_assignment[v] += inc; + } + + void acc_parent(th_var v, clause_id parent) { + m_parent[v] = parent; + m_parent_stack.push_back(parent_trail(v, parent)); + } + + numeral get_delta(const clause & cl) const { + SASSERT(cl.coeff().is_one() && "Not yet support for non-units"); + return eval_body(cl) - eval_head(cl); + } + + void set_onstack(th_var v) { + SASSERT(m_ts != 0); + m_onstack[v] = m_ts; + } + + void reset_onstack(th_var v) { + m_onstack[v] = 0; + } + + bool is_onstack(th_var v) const { + return m_onstack[v] == m_ts; + } + + void inc_ts() { + m_ts++; + if (m_ts == 0) { + m_ts++; + m_onstack.reset(); + m_onstack.resize(m_assignment.size(), 0); + } + } + + // Make the assignment feasible. An assignment is feasible if + // Forall clause cl. eval_body(cl) <= eval_head(cl) + // + // This method assumes that if the assignment is not feasible, + // then the only infeasible clause is the last added clause. + // + // Traversal is by naive DFS search. + // + bool make_feasible(clause_id id) { + SASSERT(is_almost_feasible(id)); + SASSERT(!m_clauses.empty()); + SASSERT(!is_feasible(m_clauses[id])); + const clause & cl0 = m_clauses[id]; + inc_ts(); + for (unsigned i = 0; i < cl0.size(); ++i) { + set_onstack(cl0.vars(i)); + } + th_var source = cl0.var(); + numeral delta = get_delta(cl0); + acc_parent(source, id); + SASSERT(delta.is_pos()); + acc_assignment(source, delta); + m_todo.reset(); + m_todo.push_back(source); + + TRACE("horn_ineq", cl0.display(tout);); + + do { + ++m_stats.m_propagation_cost; + + typename clause_id_vector::iterator it = m_out_clauses[source].begin(); + typename clause_id_vector::iterator end = m_out_clauses[source].end(); + for (; it != end; ++it) { + clause & cl = m_clauses[*it]; + if (!cl.is_enabled()) { + continue; + } + delta = get_delta(cl); + + if (delta.is_pos()) { + TRACE("horn_ineq", cl.display(tout);); + th_var target = cl.var(); + if (is_onstack(target)) { + m_unsat_clause = *it; + return false; + } + else { + acc_assignment(target, delta); + acc_parent(target, *it); + m_todo.push_back(target); + } + } + } + set_onstack(source); + source = m_todo.back(); + // pop stack until there is a new variable to process. + while (is_onstack(source)) { + m_todo.pop_back(); + reset_onstack(source); + if (m_todo.empty()) { + break; + } + source = m_todo.back(); + } + } + while (!m_todo.empty()); + return true; + } + + bool is_almost_feasible(clause_id id) const { + for (unsigned i = 0; i < m_clauses.size(); ++i) { + if (id != static_cast(i) && !is_feasible(m_clauses[i])) { + return false; + } + } + return true; + } + + bool is_feasible(const clause & cl) const { + return !cl.is_enabled() || get_delta(cl).is_nonpos(); + } + + }; + + template + theory_horn_ineq::theory_horn_ineq(ast_manager& m): + theory(m.mk_family_id("arith")), + a(m), + m_arith_eq_adapter(*this, m_params, a), + m_zero_int(null_theory_var), + m_zero_real(null_theory_var), + m_graph(0), + m_asserted_qhead(0), + m_agility(0.5), + m_lia(false), + m_lra(false), + m_non_horn_ineq_exprs(false), + m_test(m), + m_factory(0) { + m_graph = alloc(graph); + } + + template + theory_horn_ineq::~theory_horn_ineq() { + reset_eh(); + dealloc(m_graph); + } + + template + std::ostream& theory_horn_ineq::atom::display(theory_horn_ineq const& th, std::ostream& out) const { + context& ctx = th.get_context(); + lbool asgn = ctx.get_assignment(m_bvar); + bool sign = (l_undef == asgn) || m_true; + return out << literal(m_bvar, sign) << " " << mk_pp(ctx.bool_var2expr(m_bvar), th.get_manager()) << " "; + if (l_undef == asgn) { + out << "unassigned\n"; + } + else { + th.m_graph->display_clause(out, get_asserted_edge()); + } + return out; + } + + template + theory_var theory_horn_ineq::mk_var(enode* n) { + th_var v = theory::mk_var(n); + m_graph->init_var(v); + get_context().attach_th_var(n, this, v); + return v; + } + + template + theory_var theory_horn_ineq::mk_var(expr* n) { + context & ctx = get_context(); + enode* e = 0; + th_var v = null_theory_var; + m_lia |= a.is_int(n); + m_lra |= a.is_real(n); + if (!is_app(n)) { + return v; + } + if (ctx.e_internalized(n)) { + e = ctx.get_enode(n); + v = e->get_th_var(get_id()); + } + else { + ctx.internalize(n, false); + e = ctx.get_enode(n); + } + if (v == null_theory_var) { + v = mk_var(e); + } + if (is_interpreted(to_app(n))) { + found_non_horn_ineq_expr(n); + } + return v; + } + + template + void theory_horn_ineq::reset_eh() { + m_graph ->reset(); + m_zero_int = null_theory_var; + m_zero_real = null_theory_var; + m_atoms .reset(); + m_asserted_atoms .reset(); + m_stats .reset(); + m_scopes .reset(); + m_asserted_qhead = 0; + m_agility = 0.5; + m_lia = false; + m_lra = false; + m_non_horn_ineq_exprs = false; + theory::reset_eh(); + } + + + + template + void theory_horn_ineq::new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just) { + rational k; + th_var s = expand(true, v1, k); + th_var t = expand(false, v2, k); + context& ctx = get_context(); + ast_manager& m = get_manager(); + + if (s == t) { + if (is_eq != k.is_zero()) { + // conflict 0 /= k; + inc_conflicts(); + ctx.set_conflict(&eq_just); + } + } + else { + // + // Create equality ast, internalize_atom + // assign the corresponding equality literal. + // + + app_ref eq(m), s2(m), t2(m); + app* s1 = get_enode(s)->get_owner(); + app* t1 = get_enode(t)->get_owner(); + s2 = a.mk_sub(t1, s1); + t2 = a.mk_numeral(k, m.get_sort(s2.get())); + // t1 - s1 = k + eq = m.mk_eq(s2.get(), t2.get()); + + TRACE("horn_ineq", + tout << v1 << " .. " << v2 << "\n"; + tout << mk_pp(eq.get(), m) <<"\n";); + + if (!internalize_atom(eq.get(), false)) { + UNREACHABLE(); + } + + literal l(ctx.get_literal(eq.get())); + if (!is_eq) { + l = ~l; + } + + ctx.assign(l, b_justification(&eq_just), false); + } + } + + template + void theory_horn_ineq::inc_conflicts() { + m_stats.m_num_conflicts++; + if (m_params.m_arith_adaptive) { + double g = m_params.m_arith_adaptive_propagation_threshold; + m_agility = m_agility*g + 1 - g; + } + } + + template + void theory_horn_ineq::set_neg_cycle_conflict() { + m_graph->traverse_neg_cycle1(m_params.m_arith_stronger_lemmas); + inc_conflicts(); + literal_vector const& lits = m_graph->get_lits(); + context & ctx = get_context(); + TRACE("horn_ineq", + tout << "conflict: "; + for (unsigned i = 0; i < lits.size(); ++i) { + ctx.display_literal_info(tout, lits[i]); + } + tout << "\n"; + ); + + if (m_params.m_arith_dump_lemmas) { + char const * logic = m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA"; + ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic); + } + + vector params; + if (get_manager().proofs_enabled()) { + params.push_back(parameter(symbol("farkas"))); + vector const& coeffs = m_graph->get_coeffs(); + for (unsigned i = 0; i < coeffs.size(); ++i) { + params.push_back(parameter(coeffs[i])); + } + } + + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification( + get_id(), ctx.get_region(), + lits.size(), lits.c_ptr(), 0, 0, params.size(), params.c_ptr()))); + } + + template + void theory_horn_ineq::found_non_horn_ineq_expr(expr* n) { + if (!m_non_horn_ineq_exprs) { + TRACE("horn_ineq", tout << "found non horn logic expression:\n" << mk_pp(n, get_manager()) << "\n";); + get_context().push_trail(value_trail(m_non_horn_ineq_exprs)); + m_non_horn_ineq_exprs = true; + } + } + + template + void theory_horn_ineq::init(context* ctx) { + theory::init(ctx); + m_zero_int = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true)); + m_zero_real = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), false), false, false, true)); + m_graph->set_to_zero(m_zero_int); + m_graph->set_to_zero(m_zero_real); + } + + /** + \brief Create negated literal. + + The negation of: E <= 0 + + -E + epsilon <= 0 + or + -E + 1 <= 0 + */ + template + void theory_horn_ineq::negate(coeffs& coeffs, rational& weight) { + for (unsigned i = 0; i < coeffs.size(); ++i) { + coeffs[i].second.neg(); + } + weight.neg(); + } + + template + typename theory_horn_ineq::numeral theory_horn_ineq::mk_weight(bool is_real, bool is_strict, rational const& w) const { + if (is_strict) { + return numeral(inf_numeral(w)) + (is_real?Ext::m_epsilon:numeral(1)); + } + else { + return numeral(inf_numeral(w)); + } + } + + template + void theory_horn_ineq::mk_coeffs(vector > const& terms, coeffs& coeffs, rational& w) { + coeffs.reset(); + w = m_test.get_weight(); + for (unsigned i = 0; i < terms.size(); ++i) { + coeffs.push_back(std::make_pair(mk_var(terms[i].first), terms[i].second)); + } + } + + template + bool theory_horn_ineq::internalize_atom(app * n, bool) { + context & ctx = get_context(); + if (!a.is_le(n) && !a.is_ge(n) && !a.is_lt(n) && !a.is_gt(n)) { + found_non_horn_ineq_expr(n); + return false; + } + SASSERT(!ctx.b_internalized(n)); + expr* e1 = n->get_arg(0), *e2 = n->get_arg(1); + if (a.is_ge(n) || a.is_gt(n)) { + std::swap(e1, e2); + } + bool is_strict = a.is_gt(n) || a.is_lt(n); + + horn_ineq_tester::classify_t cl = m_test.linearize(e1, e2); + if (cl == horn_ineq_tester::non_horn) { + found_non_horn_ineq_expr(n); + return false; + } + + rational w; + coeffs coeffs; + mk_coeffs(m_test.get_linearization(), coeffs, w); + bool_var bv = ctx.mk_bool_var(n); + ctx.set_var_theory(bv, get_id()); + literal l(bv); + numeral w1 = mk_weight(a.is_real(e1), is_strict, w); + clause_id pos = m_graph->add_ineq(coeffs, w1, l); + negate(coeffs, w); + numeral w2 = mk_weight(a.is_real(e1), !is_strict, w); + clause_id neg = m_graph->add_ineq(coeffs, w2, ~l); + m_bool_var2atom.insert(bv, m_atoms.size()); + m_atoms.push_back(atom(bv, pos, neg)); + + TRACE("horn_ineq", + tout << mk_pp(n, get_manager()) << "\n"; + m_graph->display_clause(tout << "pos: ", pos); + m_graph->display_clause(tout << "neg: ", neg); + ); + + return true; + } + + template + bool theory_horn_ineq::internalize_term(app * term) { + bool result = null_theory_var != mk_term(term); + CTRACE("horn_ineq", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";); + TRACE("horn_ineq", tout << "Terms may not be internalized " << mk_pp(term, get_manager()) << "\n";); + found_non_horn_ineq_expr(term); + return result; + } + + template + void theory_horn_ineq::internalize_eq_eh(app * atom, bool_var) { + // noop + } + + template + void theory_horn_ineq::assign_eh(bool_var v, bool is_true) { + m_stats.m_num_assertions++; + unsigned idx = m_bool_var2atom.find(v); + SASSERT(get_context().get_assignment(v) != l_undef); + SASSERT((get_context().get_assignment(v) == l_true) == is_true); + m_atoms[idx].assign_eh(is_true); + m_asserted_atoms.push_back(idx); + } + + template + void theory_horn_ineq::push_scope_eh() { + theory::push_scope_eh(); + m_graph->push(); + m_scopes.push_back(scope()); + scope & s = m_scopes.back(); + s.m_atoms_lim = m_atoms.size(); + s.m_asserted_atoms_lim = m_asserted_atoms.size(); + s.m_asserted_qhead_old = m_asserted_qhead; + } + + template + void theory_horn_ineq::pop_scope_eh(unsigned num_scopes) { + unsigned lvl = m_scopes.size(); + SASSERT(num_scopes <= lvl); + unsigned new_lvl = lvl - num_scopes; + scope & s = m_scopes[new_lvl]; + del_atoms(s.m_atoms_lim); + m_asserted_atoms.shrink(s.m_asserted_atoms_lim); + m_asserted_qhead = s.m_asserted_qhead_old; + m_scopes.shrink(new_lvl); + m_graph->pop(num_scopes); + theory::pop_scope_eh(num_scopes); + } + + template + final_check_status theory_horn_ineq::final_check_eh() { + SASSERT(is_consistent()); + TRACE("horn_ineq", display(tout);); + if (can_propagate()) { + propagate_core(); + return FC_CONTINUE; + } + else if (m_non_horn_ineq_exprs) { + return FC_GIVEUP; + } + else { + return FC_DONE; + } + } + + template + void theory_horn_ineq::propagate() { + propagate_core(); + } + + template + void theory_horn_ineq::display(std::ostream& out) const { + for (unsigned i = 0; i < m_atoms.size(); ++i) { + m_atoms[i].display(*this, out); + } + out << "\n"; + m_graph->display(out); + } + + template + void theory_horn_ineq::collect_statistics(::statistics& st) const { + st.update("horn ineq conflicts", m_stats.m_num_conflicts); + st.update("horn ineq assertions", m_stats.m_num_assertions); + m_arith_eq_adapter.collect_statistics(st); + m_graph->collect_statistics(st); + } + + template + void theory_horn_ineq::del_atoms(unsigned old_size) { + typename atoms::iterator begin = m_atoms.begin() + old_size; + typename atoms::iterator it = m_atoms.end(); + while (it != begin) { + --it; + m_bool_var2atom.erase(it->get_bool_var()); + } + m_atoms.shrink(old_size); + } + + template + void theory_horn_ineq::propagate_core() { + bool consistent = true; + while (consistent && can_propagate()) { + unsigned idx = m_asserted_atoms[m_asserted_qhead]; + m_asserted_qhead++; + consistent = propagate_atom(m_atoms[idx]); + } + } + + template + bool theory_horn_ineq::propagate_atom(atom const& a) { + context& ctx = get_context(); + TRACE("horn_ineq", a.display(*this, tout); tout << "\n";); + if (ctx.inconsistent()) { + return false; + } + int clause_id = a.get_asserted_edge(); + if (!m_graph->enable_clause(clause_id)) { + set_neg_cycle_conflict(); + return false; + } + return true; + } + + template + theory_var theory_horn_ineq::mk_term(app* n) { + context& ctx = get_context(); + + horn_ineq_tester::classify_t cl = m_test.linearize(n); + if (cl == horn_ineq_tester::non_horn) { + found_non_horn_ineq_expr(n); + return null_theory_var; + } + + coeffs coeffs; + rational w; + mk_coeffs(m_test.get_linearization(), coeffs, w); + if (coeffs.empty()) { + return mk_num(n, w); + } + if (coeffs.size() == 1 && coeffs[0].second.is_one()) { + return coeffs[0].first; + } + th_var target = mk_var(ctx.mk_enode(n, false, false, true)); + coeffs.push_back(std::make_pair(target, rational(-1))); + + VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal))); + negate(coeffs, w); + VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal))); + return target; + } + + template + theory_var theory_horn_ineq::mk_num(app* n, rational const& r) { + theory_var v = null_theory_var; + context& ctx = get_context(); + if (r.is_zero()) { + v = a.is_int(n)?m_zero_int:m_zero_real; + } + else if (ctx.e_internalized(n)) { + enode* e = ctx.get_enode(n); + v = e->get_th_var(get_id()); + SASSERT(v != null_theory_var); + } + else { + v = mk_var(ctx.mk_enode(n, false, false, true)); + // v = k: v <= k k <= v + coeffs coeffs; + coeffs.push_back(std::make_pair(v, rational(1))); + VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(r)), null_literal))); + coeffs.back().second.neg(); + VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(-r)), null_literal))); + } + return v; + } + + template + theory_var theory_horn_ineq::expand(bool pos, th_var v, rational & k) { + context& ctx = get_context(); + enode* e = get_enode(v); + expr* x, *y; + rational r; + for (;;) { + app* n = e->get_owner(); + if (a.is_add(n, x, y)) { + if (a.is_numeral(x, r)) { + e = ctx.get_enode(y); + } + else if (a.is_numeral(y, r)) { + e = ctx.get_enode(x); + } + v = e->get_th_var(get_id()); + SASSERT(v != null_theory_var); + if (v == null_theory_var) { + break; + } + if (pos) { + k += r; + } + else { + k -= r; + } + } + else { + break; + } + } + return v; + } + + template + bool theory_horn_ineq::is_consistent() const { + return m_graph->is_feasible(); + } + + // models: + template + void theory_horn_ineq::init_model(model_generator & m) { + m_factory = alloc(arith_factory, get_manager()); + m.register_factory(m_factory); + compute_delta(); + } + + template + model_value_proc * theory_horn_ineq::mk_value(enode * n, model_generator & mg) { + theory_var v = n->get_th_var(get_id()); + SASSERT(v != null_theory_var); + numeral val = m_graph->get_assignment(v); + rational num = val.get_infinity()*m_lambda + val.get_rational() + val.get_infinitesimal()*m_delta; + TRACE("horn_ineq", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); + return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner()))); + } + + /** + \brief Compute numeral values for the infinitesimals to satisfy the inequalities. + */ + + template + void theory_horn_ineq::compute_delta() { + m_delta = rational(1); + m_lambda = rational(0); + unsigned sz = m_graph->get_num_clauses(); + + for (unsigned i = 0; i < sz; ++i) { + if (!m_graph->get_clause(i).is_enabled()) { + continue; + } + numeral b = m_graph->eval_body(i); + numeral h = m_graph->eval_head(i); + + if (b.get_infinity() < h.get_infinity()) { + continue; + } + SASSERT(b.get_infinity() == h.get_infinity()); + + // b <= h + // suppose that h.eps < b.eps + // then we have h.num > b.num + // but also h.num + delta*h.eps >= b.num + delta*b.eps + // <=> + // (h.num - b.num)/(b.eps - h.eps) >= delta + rational num_r = h.get_rational() - b.get_rational(); + rational eps_r = b.get_infinitesimal() - h.get_infinitesimal(); + if (eps_r.is_pos()) { + SASSERT(num_r.is_pos()); + rational new_delta = num_r/eps_r; + if (new_delta < m_delta) { + m_delta = new_delta; + } + } + } + + for (unsigned i = 0; i < sz; ++i) { + if (!m_graph->get_clause(i).is_enabled()) { + continue; + } + numeral b = m_graph->eval_body(i); + numeral h = m_graph->eval_head(i); + + rational ir = h.get_infinity() - b.get_infinity(); + rational hr = b.get_rational() - h.get_rational(); + rational num_r = hr + m_delta*(b.get_infinitesimal() - h.get_infinitesimal()); + + SASSERT(b.get_infinity() <= h.get_infinity()); + + // b <= h + // suppose that h.finite < b.finite + // then we have h.infinite > b.infinite + // but also + // h.infinite*lambda + h.finite >= b.infinite*lambda + b.finite + // <=> + // lambda >= (b.finite - h.finite) / (h.infinite - b.infinite) + if (num_r.is_pos()) { + SASSERT(ir.is_pos()); + rational new_lambda = num_r/ir; + if (new_lambda > m_lambda) { + m_lambda = new_lambda; + } + } + } + } + + + +}; + +#endif diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp new file mode 100644 index 000000000..c45cfe74a --- /dev/null +++ b/src/smt/theory_utvpi.cpp @@ -0,0 +1,160 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_utvpi.h + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-26 + +Revision History: + + The implementaton is derived from theory_diff_logic. + +--*/ +#include "theory_utvpi.h" +#include "theory_utvpi_def.h" + +namespace smt { + + template class theory_utvpi; + template class theory_utvpi; + + // similar to test_diff_logic: + + utvpi_tester::utvpi_tester(ast_manager& m): m(m), a(m) {} + + bool utvpi_tester::operator()(expr* e) { + m_todo.reset(); + m_mark.reset(); + m_todo.push_back(e); + expr* e1, *e2; + + while (!m_todo.empty()) { + expr* e = m_todo.back(); + m_todo.pop_back(); + if (!m_mark.is_marked(e)) { + m_mark.mark(e, true); + if (is_var(e)) { + continue; + } + if (!is_app(e)) { + return false; + } + app* ap = to_app(e); + if (m.is_eq(ap, e1, e2)) { + if (!linearize(e1, e2)) { + return false; + } + } + else if (ap->get_family_id() == m.get_basic_family_id()) { + continue; + } + else if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1) || + a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) { + if (!linearize(e1, e2)) { + return false; + } + } + else if (is_uninterp_const(e)) { + continue; + } + else { + return false; + } + } + } + return true; + } + + vector > const& utvpi_tester::get_linearization() const { + SASSERT(m_terms.size() <= 2); + return m_terms; + } + + bool utvpi_tester::operator()(unsigned num_fmls, expr* const* fmls) { + for (unsigned i = 0; i < num_fmls; ++i) { + if (!(*this)(fmls[i])) { + return false; + } + } + return true; + } + + bool utvpi_tester::linearize(expr* e) { + m_terms.reset(); + m_terms.push_back(std::make_pair(e, rational(1))); + return linearize(); + } + + bool utvpi_tester::linearize(expr* e1, expr* e2) { + m_terms.reset(); + m_terms.push_back(std::make_pair(e1, rational(1))); + m_terms.push_back(std::make_pair(e2, rational(-1))); + return linearize(); + } + + bool utvpi_tester::linearize() { + + m_weight.reset(); + m_coeff_map.reset(); + + while (!m_terms.empty()) { + expr* e1, *e2; + rational num; + rational mul = m_terms.back().second; + expr* e = m_terms.back().first; + m_terms.pop_back(); + if (a.is_add(e)) { + for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { + m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul)); + } + } + else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) { + m_terms.push_back(std::make_pair(e2, mul*num)); + } + else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) { + m_terms.push_back(std::make_pair(e2, mul*num)); + } + else if (a.is_sub(e, e1, e2)) { + m_terms.push_back(std::make_pair(e1, mul)); + m_terms.push_back(std::make_pair(e2, -mul)); + } + else if (a.is_uminus(e, e1)) { + m_terms.push_back(std::make_pair(e1, -mul)); + } + else if (a.is_numeral(e, num)) { + m_weight += num*mul; + } + else if (a.is_to_real(e, e1)) { + m_terms.push_back(std::make_pair(e1, mul)); + } + else if (!is_uninterp_const(e)) { + return false; + } + else { + m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul; + } + } + obj_map::iterator it = m_coeff_map.begin(); + obj_map::iterator end = m_coeff_map.end(); + for (; it != end; ++it) { + rational r = it->m_value; + if (r.is_zero()) { + continue; + } + m_terms.push_back(std::make_pair(it->m_key, r)); + if (m_terms.size() > 2) { + return false; + } + if (!r.is_one() && !r.is_minus_one()) { + return false; + } + } + return true; + } + + +} diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h new file mode 100644 index 000000000..8b19bdab8 --- /dev/null +++ b/src/smt/theory_utvpi.h @@ -0,0 +1,336 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_utvpi.h + +Abstract: + + use Bellman Ford traversal algorithm for UTVPI. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-26 + +Revision History: + + The implementaton is derived from theory_diff_logic. + +--*/ + +#ifndef _THEORY_UTVPI_H_ +#define _THEORY_UTVPI_H_ + +#include"theory_diff_logic.h" + +namespace smt { + + class utvpi_tester { + ast_manager& m; + arith_util a; + ptr_vector m_todo; + ast_mark m_mark; + obj_map m_coeff_map; + rational m_weight; + vector > m_terms; + + public: + utvpi_tester(ast_manager& m); + + // test if formula is in the Horn inequality fragment: + bool operator()(expr* fml); + bool operator()(unsigned num_fmls, expr* const* fmls); + + // linearize inequality/equality + bool linearize(expr* e); + bool linearize(expr* e1, expr* e2); + + // retrieve linearization + vector > const& get_linearization() const; + rational const& get_weight() const { return m_weight; } + private: + bool linearize(); + }; + + template + class theory_utvpi : public theory, private Ext { + + typedef typename Ext::numeral numeral; + typedef theory_var th_var; + typedef svector th_var_vector; + typedef vector > coeffs; + + class assignment_trail; + class parent_trail; + + struct GExt : public Ext { + typedef literal explanation; + }; + + class atom { + protected: + bool_var m_bvar; + bool m_true; + int m_pos; + int m_neg; + public: + atom(bool_var bv, int pos, int neg) : + m_bvar(bv), m_true(false), + m_pos(pos), m_neg(neg) {} + virtual ~atom() {} + bool_var get_bool_var() const { return m_bvar; } + void assign_eh(bool is_true) { m_true = is_true; } + int get_asserted_edge() const { return this->m_true?m_pos:m_neg; } + int get_pos() const { return m_pos; } + int get_neg() const { return m_neg; } + std::ostream& display(theory_utvpi const& th, std::ostream& out) const; + }; + typedef svector atoms; + + struct scope { + unsigned m_atoms_lim; + unsigned m_asserted_atoms_lim; + unsigned m_asserted_qhead_old; + }; + + struct stats { + unsigned m_num_conflicts; + unsigned m_num_assertions; + unsigned m_num_core2th_eqs; + unsigned m_num_core2th_diseqs; + + void reset() { + memset(this, 0, sizeof(*this)); + } + + stats() { + reset(); + } + }; + + // Functor used to collect the proofs for a conflict due to + // a negative cycle. + class nc_functor { + literal_vector m_antecedents; + theory_utvpi& m_super; + public: + nc_functor(theory_utvpi& s) : m_super(s) {} + void reset() { m_antecedents.reset(); } + literal_vector const& get_lits() const { return m_antecedents; } + + void operator()(literal const & ex) { + if (ex != null_literal) { + m_antecedents.push_back(ex); + } + } + + void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) { + m_super.new_edge(src, dst, num_edges, edges); + } + }; + + + stats m_stats; + smt_params m_params; + arith_util a; + arith_eq_adapter m_arith_eq_adapter; + th_var m_zero_int; // cache the variable representing the zero variable. + th_var m_zero_real; // cache the variable representing the zero variable. + + dl_graph m_graph; + nc_functor m_nc_functor; + atoms m_atoms; + unsigned_vector m_asserted_atoms; // set of asserted atoms + unsigned m_asserted_qhead; + u_map m_bool_var2atom; + svector m_scopes; + + double m_agility; + bool m_lia; + bool m_lra; + bool m_non_utvpi_exprs; + + utvpi_tester m_test; + + + arith_factory * m_factory; + rational m_delta; + + + // Set a conflict due to a negative cycle. + void set_conflict(); + + void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {} + + // Create a new theory variable. + virtual th_var mk_var(enode* n); + + virtual th_var mk_var(expr* n); + + void compute_delta(); + + void found_non_utvpi_expr(expr * n); + + bool is_interpreted(app* n) const { + return n->get_family_id() == get_family_id(); + } + + public: + theory_utvpi(ast_manager& m); + + virtual ~theory_utvpi(); + + virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, get_manager()); } + + virtual char const * get_name() const { return "utvpi-logic"; } + + /** + \brief See comment in theory::mk_eq_atom + */ + virtual app * mk_eq_atom(expr * lhs, expr * rhs) { return a.mk_eq(lhs, rhs); } + + virtual void init(context * ctx); + + virtual bool internalize_atom(app * atom, bool gate_ctx); + + virtual bool internalize_term(app * term); + + virtual void internalize_eq_eh(app * atom, bool_var v); + + virtual void assign_eh(bool_var v, bool is_true); + + virtual void new_eq_eh(th_var v1, th_var v2) { + m_stats.m_num_core2th_eqs++; + m_arith_eq_adapter.new_eq_eh(v1, v2); + } + + virtual bool use_diseqs() const { return true; } + + virtual void new_diseq_eh(th_var v1, th_var v2) { + m_arith_eq_adapter.new_diseq_eh(v1, v2); + } + + virtual void push_scope_eh(); + + virtual void pop_scope_eh(unsigned num_scopes); + + virtual void restart_eh() { + m_arith_eq_adapter.restart_eh(); + } + + virtual void relevant_eh(app* e) {} + + virtual void init_search_eh() { + m_arith_eq_adapter.init_search_eh(); + } + + virtual final_check_status final_check_eh(); + + virtual bool is_shared(th_var v) const { + return false; + } + + virtual bool can_propagate() { + SASSERT(m_asserted_qhead <= m_asserted_atoms.size()); + return m_asserted_qhead != m_asserted_atoms.size(); + } + + virtual void propagate(); + + virtual justification * why_is_diseq(th_var v1, th_var v2) { + UNREACHABLE(); + return 0; + } + + virtual void reset_eh(); + + virtual void init_model(model_generator & m); + + virtual model_value_proc * mk_value(enode * n, model_generator & mg); + + virtual bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const { + return true; + } + + virtual void display(std::ostream & out) const; + + virtual void collect_statistics(::statistics & st) const; + + private: + + rational mk_value(theory_var v); + + void validate_model(); + + bool eval(expr* e); + + rational eval_num(expr* e); + + bool check_z_consistency(); + + virtual void new_eq_eh(th_var v1, th_var v2, justification& j) { + m_stats.m_num_core2th_eqs++; + new_eq_or_diseq(true, v1, v2, j); + } + + virtual void new_diseq_eh(th_var v1, th_var v2, justification& j) { + m_stats.m_num_core2th_diseqs++; + new_eq_or_diseq(false, v1, v2, j); + } + + void negate(coeffs& coeffs, rational& weight); + numeral mk_weight(bool is_real, bool is_strict, rational const& w) const; + void mk_coeffs(vector >const& terms, coeffs& coeffs, rational& w); + + void del_atoms(unsigned old_size); + + bool propagate_atom(atom const& a); + + th_var mk_term(app* n); + + th_var mk_num(app* n, rational const& r); + + bool is_consistent() const; + + th_var expand(bool pos, th_var v, rational & k); + + void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just); + + th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; } + + th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); } + + void inc_conflicts(); + + edge_id add_ineq(vector > const& terms, numeral const& weight, literal l); + + bool enable_edge(edge_id id); + + th_var to_var(th_var v) const { + return 2*v; + } + + th_var from_var(th_var v) const { + return v/2; + } + + th_var pos(th_var v) const { + return v & 0xFFFFFFFE; + } + + th_var neg(th_var v) const { + return v | 0x1; + } + + }; + + + typedef theory_utvpi theory_rutvpi; + typedef theory_utvpi theory_iutvpi; +}; + + + + +#endif /* _THEORY_UTVPI_H_ */ diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h new file mode 100644 index 000000000..905270a46 --- /dev/null +++ b/src/smt/theory_utvpi_def.h @@ -0,0 +1,814 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_utvpi_def.h + +Abstract: + + Implementation of UTVPI solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-04-26 + +Revision History: + + 1. introduce x^+ and x^-, such that 2*x := x^+ - x^- + 2. rewrite constraints as follows: + + x - y <= k => x^+ - y^+ <= k + y^- - x^- <= k + + x <= k => x^+ - x^- <= 2k + + + x + y <= k => x^+ - y^- <= k + y^+ - x^- <= k + + + - x - y <= k => x^- - y^+ <= k + y^- - x^+ <= k + + 3. Solve for x^+ and x^- + 4. Check parity condition for integers (see Lahiri and Musuvathi 05) + 5. extract model for M(x) := (M(x^+)- M(x^-))/2 + +--*/ + +#ifndef _THEORY_UTVPI_DEF_H_ +#define _THEORY_UTVPI_DEF_H_ +#include "theory_utvpi.h" +#include "heap.h" +#include "ast_pp.h" +#include "smt_context.h" + +namespace smt { + + + template + theory_utvpi::theory_utvpi(ast_manager& m): + theory(m.mk_family_id("arith")), + a(m), + m_arith_eq_adapter(*this, m_params, a), + m_zero_int(null_theory_var), + m_zero_real(null_theory_var), + m_asserted_qhead(0), + m_nc_functor(*this), + m_agility(0.5), + m_lia(false), + m_lra(false), + m_non_utvpi_exprs(false), + m_test(m), + m_factory(0) { + } + + template + theory_utvpi::~theory_utvpi() { + reset_eh(); + } + + template + std::ostream& theory_utvpi::atom::display(theory_utvpi const& th, std::ostream& out) const { + context& ctx = th.get_context(); + lbool asgn = ctx.get_assignment(m_bvar); + bool sign = (l_undef == l_false); + return out << literal(m_bvar, sign) << " " << mk_pp(ctx.bool_var2expr(m_bvar), th.get_manager()) << " "; + if (l_undef == asgn) { + out << "unassigned\n"; + } + else { + th.m_graph.display_edge(out, get_asserted_edge()); + } + return out; + } + + template + theory_var theory_utvpi::mk_var(enode* n) { + th_var v = theory::mk_var(n); + TRACE("utvpi", tout << v << " " << mk_pp(n->get_owner(), get_manager()) << "\n";); + m_graph.init_var(to_var(v)); + m_graph.init_var(neg(to_var(v))); + get_context().attach_th_var(n, this, v); + return v; + } + + template + theory_var theory_utvpi::mk_var(expr* n) { + context & ctx = get_context(); + enode* e = 0; + th_var v = null_theory_var; + m_lia |= a.is_int(n); + m_lra |= a.is_real(n); + if (!is_app(n)) { + return v; + } + if (ctx.e_internalized(n)) { + e = ctx.get_enode(n); + v = e->get_th_var(get_id()); + } + else { + ctx.internalize(n, false); + e = ctx.get_enode(n); + } + if (v == null_theory_var) { + v = mk_var(e); + } + if (is_interpreted(to_app(n))) { + found_non_utvpi_expr(n); + } + return v; + } + + template + void theory_utvpi::reset_eh() { + m_graph .reset(); + m_zero_int = null_theory_var; + m_zero_real = null_theory_var; + m_atoms .reset(); + m_asserted_atoms .reset(); + m_stats .reset(); + m_scopes .reset(); + m_asserted_qhead = 0; + m_agility = 0.5; + m_lia = false; + m_lra = false; + m_non_utvpi_exprs = false; + theory::reset_eh(); + } + + template + void theory_utvpi::new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just) { + rational k; + th_var s = expand(true, v1, k); + th_var t = expand(false, v2, k); + context& ctx = get_context(); + ast_manager& m = get_manager(); + + if (s == t) { + if (is_eq != k.is_zero()) { + // conflict 0 /= k; + inc_conflicts(); + ctx.set_conflict(&eq_just); + } + } + else { + // + // Create equality ast, internalize_atom + // assign the corresponding equality literal. + // + + app_ref eq(m), s2(m), t2(m); + app* s1 = get_enode(s)->get_owner(); + app* t1 = get_enode(t)->get_owner(); + s2 = a.mk_sub(t1, s1); + t2 = a.mk_numeral(k, m.get_sort(s2.get())); + // t1 - s1 = k + eq = m.mk_eq(s2.get(), t2.get()); + + TRACE("utvpi", + tout << v1 << " .. " << v2 << "\n"; + tout << mk_pp(eq.get(), m) <<"\n";); + + if (!internalize_atom(eq.get(), false)) { + UNREACHABLE(); + } + + literal l(ctx.get_literal(eq.get())); + if (!is_eq) { + l = ~l; + } + ctx.assign(l, b_justification(&eq_just), false); + } + } + + template + void theory_utvpi::inc_conflicts() { + m_stats.m_num_conflicts++; + if (m_params.m_arith_adaptive) { + double g = m_params.m_arith_adaptive_propagation_threshold; + m_agility = m_agility*g + 1 - g; + } + } + + template + void theory_utvpi::set_conflict() { + inc_conflicts(); + literal_vector const& lits = m_nc_functor.get_lits(); + context & ctx = get_context(); + TRACE("utvpi", + tout << "conflict: "; + for (unsigned i = 0; i < lits.size(); ++i) { + ctx.display_literal_info(tout, lits[i]); + } + tout << "\n"; + ); + + if (m_params.m_arith_dump_lemmas) { + char const * logic = m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA"; + ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic); + } + + vector params; + if (get_manager().proofs_enabled()) { + params.push_back(parameter(symbol("farkas"))); + params.resize(lits.size()+1, parameter(rational(1))); + } + + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification( + get_id(), ctx.get_region(), + lits.size(), lits.c_ptr(), 0, 0, params.size(), params.c_ptr()))); + + m_nc_functor.reset(); + } + + template + void theory_utvpi::found_non_utvpi_expr(expr* n) { + if (!m_non_utvpi_exprs) { + std::stringstream msg; + msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n"; + TRACE("utvpi", tout << msg.str();); + warning_msg(msg.str().c_str()); + get_context().push_trail(value_trail(m_non_utvpi_exprs)); + m_non_utvpi_exprs = true; + } + } + + template + void theory_utvpi::init(context* ctx) { + theory::init(ctx); + m_zero_int = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true)); + m_zero_real = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), false), false, false, true)); + } + + /** + \brief Create negated literal. + + The negation of: E <= 0 + + -E + epsilon <= 0 + or + -E + 1 <= 0 + */ + template + void theory_utvpi::negate(coeffs& coeffs, rational& weight) { + for (unsigned i = 0; i < coeffs.size(); ++i) { + coeffs[i].second.neg(); + } + weight.neg(); + } + + template + typename theory_utvpi::numeral theory_utvpi::mk_weight(bool is_real, bool is_strict, rational const& w) const { + if (is_strict) { + return numeral(w) + (is_real?Ext::m_epsilon:numeral(1)); + } + else { + return numeral(w); + } + } + + template + void theory_utvpi::mk_coeffs(vector > const& terms, coeffs& coeffs, rational& w) { + coeffs.reset(); + w = m_test.get_weight(); + for (unsigned i = 0; i < terms.size(); ++i) { + coeffs.push_back(std::make_pair(mk_var(terms[i].first), terms[i].second)); + } + } + + template + void theory_utvpi::internalize_eq_eh(app * atom, bool_var v) { + context & ctx = get_context(); + app * lhs = to_app(atom->get_arg(0)); + app * rhs = to_app(atom->get_arg(1)); + if (a.is_numeral(rhs)) { + std::swap(rhs, lhs); + } + if (!a.is_numeral(rhs)) { + return; + } + if (a.is_add(lhs) || a.is_sub(lhs)) { + // force axioms for (= (+ x y) k) + // this is necessary because (+ x y) is not expressible as a utvpi term. + m_arith_eq_adapter.mk_axioms(ctx.get_enode(lhs), ctx.get_enode(rhs)); + } + } + + template + bool theory_utvpi::internalize_atom(app * n, bool) { + context & ctx = get_context(); + if (!a.is_le(n) && !a.is_ge(n) && !a.is_lt(n) && !a.is_gt(n)) { + found_non_utvpi_expr(n); + return false; + } + SASSERT(!ctx.b_internalized(n)); + expr* e1 = n->get_arg(0), *e2 = n->get_arg(1); + if (a.is_ge(n) || a.is_gt(n)) { + std::swap(e1, e2); + } + bool is_strict = a.is_gt(n) || a.is_lt(n); + + bool cl = m_test.linearize(e1, e2); + if (!cl) { + found_non_utvpi_expr(n); + return false; + } + + rational w; + coeffs coeffs; + mk_coeffs(m_test.get_linearization(), coeffs, w); + bool_var bv = ctx.mk_bool_var(n); + ctx.set_var_theory(bv, get_id()); + literal l(bv); + numeral w1 = mk_weight(a.is_real(e1), is_strict, w); + edge_id pos = add_ineq(coeffs, w1, l); + negate(coeffs, w); + numeral w2 = mk_weight(a.is_real(e1), !is_strict, w); + edge_id neg = add_ineq(coeffs, w2, ~l); + m_bool_var2atom.insert(bv, m_atoms.size()); + m_atoms.push_back(atom(bv, pos, neg)); + + TRACE("utvpi", + tout << mk_pp(n, get_manager()) << "\n"; + m_graph.display_edge(tout << "pos: ", pos); + m_graph.display_edge(tout << "neg: ", neg); + ); + + return true; + } + + template + bool theory_utvpi::internalize_term(app * term) { + bool result = null_theory_var != mk_term(term); + CTRACE("utvpi", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";); + return result; + } + + template + void theory_utvpi::assign_eh(bool_var v, bool is_true) { + m_stats.m_num_assertions++; + unsigned idx = m_bool_var2atom.find(v); + SASSERT(get_context().get_assignment(v) != l_undef); + SASSERT((get_context().get_assignment(v) == l_true) == is_true); + m_atoms[idx].assign_eh(is_true); + m_asserted_atoms.push_back(idx); + } + + template + void theory_utvpi::push_scope_eh() { + theory::push_scope_eh(); + m_graph.push(); + m_scopes.push_back(scope()); + scope & s = m_scopes.back(); + s.m_atoms_lim = m_atoms.size(); + s.m_asserted_atoms_lim = m_asserted_atoms.size(); + s.m_asserted_qhead_old = m_asserted_qhead; + } + + template + void theory_utvpi::pop_scope_eh(unsigned num_scopes) { + unsigned lvl = m_scopes.size(); + SASSERT(num_scopes <= lvl); + unsigned new_lvl = lvl - num_scopes; + scope & s = m_scopes[new_lvl]; + del_atoms(s.m_atoms_lim); + m_asserted_atoms.shrink(s.m_asserted_atoms_lim); + m_asserted_qhead = s.m_asserted_qhead_old; + m_scopes.shrink(new_lvl); + m_graph.pop(num_scopes); + theory::pop_scope_eh(num_scopes); + } + + template + final_check_status theory_utvpi::final_check_eh() { + SASSERT(is_consistent()); + TRACE("utvpi", display(tout);); + if (can_propagate()) { + propagate(); + return FC_CONTINUE; + } + else if (!check_z_consistency()) { + return FC_CONTINUE; + } + else if (m_non_utvpi_exprs) { + return FC_GIVEUP; + } + else { + m_graph.set_to_zero(to_var(m_zero_int), to_var(m_zero_real)); + m_graph.set_to_zero(neg(to_var(m_zero_int)), neg(to_var(m_zero_real))); + m_graph.set_to_zero(to_var(m_zero_int), neg(to_var(m_zero_int))); + return FC_DONE; + } + } + + template + bool theory_utvpi::check_z_consistency() { + int_vector scc_id; + m_graph.compute_zero_edge_scc(scc_id); + + unsigned sz = get_num_vars(); + for (unsigned i = 0; i < sz; ++i) { + enode* e = get_enode(i); + if (a.is_int(e->get_owner())) { + continue; + } + th_var v1 = to_var(i); + th_var v2 = neg(v1); + rational r1 = m_graph.get_assignment(v1).get_rational(); + rational r2 = m_graph.get_assignment(v2).get_rational(); + SASSERT(r1.is_int()); + SASSERT(r2.is_int()); + if (r1.is_even() == r2.is_even()) { + continue; + } + if (scc_id[v1] != scc_id[v2]) { + continue; + } + if (scc_id[v1] == -1) { + continue; + } + // they are in the same SCC and have different parities => contradiction. + m_nc_functor.reset(); + VERIFY(m_graph.find_shortest_zero_edge_path(v1, v2, UINT_MAX, m_nc_functor)); + VERIFY(m_graph.find_shortest_zero_edge_path(v2, v1, UINT_MAX, m_nc_functor)); + IF_VERBOSE(1, verbose_stream() << "parity conflict " << mk_pp(e->get_owner(), get_manager()) << "\n";); + set_conflict(); + + return false; + } + return true; + } + + template + void theory_utvpi::display(std::ostream& out) const { + for (unsigned i = 0; i < m_atoms.size(); ++i) { + m_atoms[i].display(*this, out); out << "\n"; + } + m_graph.display(out); + } + + template + void theory_utvpi::collect_statistics(::statistics& st) const { + st.update("utvpi conflicts", m_stats.m_num_conflicts); + st.update("utvpi asserts", m_stats.m_num_assertions); + st.update("core->utvpi eqs", m_stats.m_num_core2th_eqs); + st.update("core->utvpi diseqs", m_stats.m_num_core2th_diseqs); + m_arith_eq_adapter.collect_statistics(st); + m_graph.collect_statistics(st); + } + + template + void theory_utvpi::del_atoms(unsigned old_size) { + typename atoms::iterator begin = m_atoms.begin() + old_size; + typename atoms::iterator it = m_atoms.end(); + while (it != begin) { + --it; + m_bool_var2atom.erase(it->get_bool_var()); + } + m_atoms.shrink(old_size); + } + + template + void theory_utvpi::propagate() { + bool consistent = true; + while (consistent && can_propagate()) { + unsigned idx = m_asserted_atoms[m_asserted_qhead]; + m_asserted_qhead++; + consistent = propagate_atom(m_atoms[idx]); + } + } + + template + bool theory_utvpi::propagate_atom(atom const& a) { + context& ctx = get_context(); + TRACE("utvpi", a.display(*this, tout); tout << "\n";); + if (ctx.inconsistent()) { + return false; + } + int edge_id = a.get_asserted_edge(); + if (!enable_edge(edge_id)) { + m_graph.traverse_neg_cycle2(m_params.m_arith_stronger_lemmas, m_nc_functor); + set_conflict(); + return false; + } + return true; + } + + template + theory_var theory_utvpi::mk_term(app* n) { + TRACE("utvpi", tout << mk_pp(n, get_manager()) << "\n";); + context& ctx = get_context(); + + bool cl = m_test.linearize(n); + if (!cl) { + found_non_utvpi_expr(n); + return null_theory_var; + } + + coeffs coeffs; + rational w; + mk_coeffs(m_test.get_linearization(), coeffs, w); + if (coeffs.empty()) { + return mk_num(n, w); + } + if (coeffs.size() == 1 && coeffs[0].second.is_one()) { + return coeffs[0].first; + } + if (coeffs.size() == 2) { + // do not create an alias. + return null_theory_var; + } + for (unsigned i = 0; i < n->get_num_args(); ++i) { + mk_term(to_app(n->get_arg(i))); + } + th_var target = mk_var(ctx.mk_enode(n, false, false, true)); + coeffs.push_back(std::make_pair(target, rational(-1))); + + VERIFY(enable_edge(add_ineq(coeffs, numeral(w), null_literal))); + negate(coeffs, w); + VERIFY(enable_edge(add_ineq(coeffs, numeral(w), null_literal))); + return target; + } + + template + theory_var theory_utvpi::mk_num(app* n, rational const& r) { + theory_var v = null_theory_var; + context& ctx = get_context(); + if (r.is_zero()) { + v = a.is_int(n)?m_zero_int:m_zero_real; + } + else if (ctx.e_internalized(n)) { + enode* e = ctx.get_enode(n); + v = e->get_th_var(get_id()); + SASSERT(v != null_theory_var); + } + else { + v = mk_var(ctx.mk_enode(n, false, false, true)); + // v = k: v <= k k <= v + coeffs coeffs; + coeffs.push_back(std::make_pair(v, rational(-1))); + VERIFY(enable_edge(add_ineq(coeffs, numeral(r), null_literal))); + coeffs.back().second.neg(); + VERIFY(enable_edge(add_ineq(coeffs, numeral(-r), null_literal))); + } + return v; + } + + template + theory_var theory_utvpi::expand(bool pos, th_var v, rational & k) { + context& ctx = get_context(); + enode* e = get_enode(v); + expr* x, *y; + rational r; + for (;;) { + app* n = e->get_owner(); + if (a.is_add(n, x, y)) { + if (a.is_numeral(x, r)) { + e = ctx.get_enode(y); + } + else if (a.is_numeral(y, r)) { + e = ctx.get_enode(x); + } + v = e->get_th_var(get_id()); + SASSERT(v != null_theory_var); + if (v == null_theory_var) { + break; + } + if (pos) { + k += r; + } + else { + k -= r; + } + } + else { + break; + } + } + return v; + } + + // m_graph(source, target, weight, ex); + // target - source <= weight + + template + edge_id theory_utvpi::add_ineq(vector > const& terms, numeral const& weight, literal l) { + + SASSERT(terms.size() <= 2); + SASSERT(terms.size() < 1 || terms[0].second.is_one() || terms[0].second.is_minus_one()); + SASSERT(terms.size() < 2 || terms[1].second.is_one() || terms[1].second.is_minus_one()); + + th_var v1 = null_theory_var, v2 = null_theory_var; + bool pos1 = true, pos2 = true; + if (terms.size() >= 1) { + v1 = terms[0].first; + pos1 = terms[0].second.is_one(); + SASSERT(v1 != null_theory_var); + SASSERT(pos1 || terms[0].second.is_minus_one()); + } + if (terms.size() >= 2) { + v2 = terms[1].first; + pos2 = terms[1].second.is_one(); + SASSERT(v1 != null_theory_var); + SASSERT(pos2 || terms[1].second.is_minus_one()); + } +// TRACE("utvpi", tout << (pos1?"$":"-$") << v1 << (pos2?" + $":" - $") << v2 << " + " << weight << " <= 0\n";); + edge_id id = m_graph.get_num_edges(); + th_var w1 = to_var(v1), w2 = to_var(v2); + if (terms.size() == 1 && pos1) { + m_graph.add_edge(neg(w1), pos(w1), -weight-weight, l); + m_graph.add_edge(neg(w1), pos(w1), -weight-weight, l); + } + else if (terms.size() == 1 && !pos1) { + m_graph.add_edge(pos(w1), neg(w1), -weight-weight, l); + m_graph.add_edge(pos(w1), neg(w1), -weight-weight, l); + } + else if (pos1 && pos2) { + m_graph.add_edge(neg(w2), pos(w1), -weight, l); + m_graph.add_edge(neg(w1), pos(w2), -weight, l); + } + else if (pos1 && !pos2) { + m_graph.add_edge(pos(w2), pos(w1), -weight, l); + m_graph.add_edge(neg(w1), neg(w2), -weight, l); + } + else if (!pos1 && pos2) { + m_graph.add_edge(neg(w2), neg(w1), -weight, l); + m_graph.add_edge(pos(w1), pos(w2), -weight, l); + } + else { + m_graph.add_edge(pos(w1), neg(w2), -weight, l); + m_graph.add_edge(pos(w2), neg(w1), -weight, l); + } + return id; + } + + template + bool theory_utvpi::enable_edge(edge_id id) { + return (id == null_edge_id) || (m_graph.enable_edge(id) && m_graph.enable_edge(id+1)); + } + + template + bool theory_utvpi::is_consistent() const { + return m_graph.is_feasible(); + } + + // models: + template + void theory_utvpi::init_model(model_generator & m) { + m_factory = alloc(arith_factory, get_manager()); + m.register_factory(m_factory); + // TBD: enforce strong or tight coherence? + compute_delta(); + DEBUG_CODE(validate_model();); + } + + template + void theory_utvpi::validate_model() { + context& ctx = get_context(); + unsigned sz = m_atoms.size(); + for (unsigned i = 0; i < sz; ++i) { + bool_var b = m_atoms[i].get_bool_var(); + if (!ctx.is_relevant(b)) { + continue; + } + bool ok = true; + expr* e = ctx.bool_var2expr(b); + switch(ctx.get_assignment(b)) { + case l_true: + ok = eval(e); + break; + case l_false: + ok = !eval(e); + break; + default: + break; + } + CTRACE("utvpi", !ok, tout << "validation failed: " << mk_pp(e, get_manager()) << "\n";); + // CTRACE("utvpi", ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";); + SASSERT(ok); + } + } + + template + bool theory_utvpi::eval(expr* e) { + expr* e1, *e2; + if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1)) { + return eval_num(e1) <= eval_num(e2); + } + if (a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) { + return eval_num(e1) < eval_num(e2); + } + if (get_manager().is_eq(e, e1, e2)) { + return eval_num(e1) == eval_num(e2); + } + TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";); + return false; + } + + template + rational theory_utvpi::eval_num(expr* e) { + rational r; + expr* e1, *e2; + if (a.is_numeral(e, r)) { + return r; + } + if (a.is_sub(e, e1, e2)) { + return eval_num(e1) - eval_num(e2); + } + if (a.is_add(e)) { + r.reset(); + for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { + r += eval_num(to_app(e)->get_arg(i)); + } + return r; + } + if (a.is_mul(e)) { + r = rational(1); + for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { + r *= eval_num(to_app(e)->get_arg(i)); + } + return r; + } + if (a.is_uminus(e, e1)) { + return -eval_num(e1); + } + if (a.is_to_real(e, e1)) { + return eval_num(e1); + } + if (is_uninterp_const(e)) { + return mk_value(mk_var(e)); + } + TRACE("utvpi", tout << "expression not handled: " << mk_pp(e, get_manager()) << "\n";); + UNREACHABLE(); + return rational(0); + } + + + template + rational theory_utvpi::mk_value(th_var v) { + SASSERT(v != null_theory_var); + numeral val1 = m_graph.get_assignment(to_var(v)); + numeral val2 = m_graph.get_assignment(neg(to_var(v))); + numeral val = val1 - val2; + rational num = val.get_rational() + (m_delta * val.get_infinitesimal().to_rational()); + num = num/rational(2); + num = floor(num); + return num; + } + + template + model_value_proc * theory_utvpi::mk_value(enode * n, model_generator & mg) { + theory_var v = n->get_th_var(get_id()); + rational num = mk_value(v); + TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); + return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner()))); + } + + /** + \brief Compute numeral values for the infinitesimals to satisfy the inequalities. + */ + + template + void theory_utvpi::compute_delta() { + m_delta = rational(1); + unsigned sz = m_graph.get_num_edges(); + + for (unsigned i = 0; i < sz; ++i) { + if (!m_graph.is_enabled(i)) { + continue; + } + numeral w = m_graph.get_weight(i); + numeral tgt = m_graph.get_assignment(m_graph.get_target(i)); + numeral src = m_graph.get_assignment(m_graph.get_source(i)); + numeral b = tgt - src - w; + SASSERT(b.is_nonpos()); + rational eps_r = b.get_infinitesimal(); + + // Given: b <= 0 + // suppose that 0 < b.eps + // then we have 0 > b.num + // then delta must ensure: + // 0 >= b.num + delta*b.eps + // <=> + // -b.num/b.eps >= delta + if (eps_r.is_pos()) { + rational num_r = -b.get_rational(); + SASSERT(num_r.is_pos()); + rational new_delta = num_r/eps_r; + if (new_delta < m_delta) { + m_delta = new_delta; + } + } + } + } + + + +}; + +#endif + diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 831efa087..2c2afab6f 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -371,6 +371,12 @@ struct ctx_simplify_tactic::imp { if (!modified) { r = t; } + else if (new_new_args.empty()) { + r = OR?m.mk_false():m.mk_true(); + } + else if (new_new_args.size() == 1) { + r = new_new_args[0]; + } else { std::reverse(new_new_args.c_ptr(), new_new_args.c_ptr() + new_new_args.size()); m_mk_app(t->get_decl(), new_new_args.size(), new_new_args.c_ptr(), r); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 55512f677..ae79446e3 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -94,7 +94,6 @@ public: smt_strategic_solver_factory(symbol const & logic):m_logic(logic) {} virtual ~smt_strategic_solver_factory() {} - virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) { symbol l; if (m_logic != symbol::null) diff --git a/src/util/hash.h b/src/util/hash.h index 3c7e50a6c..4232dd2af 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -20,6 +20,7 @@ Revision History: #define _HASH_H_ #include +#include"util.h" #ifndef __fallthrough #define __fallthrough @@ -142,6 +143,11 @@ struct size_t_hash { unsigned operator()(size_t x) const { return static_cast(x); } }; +struct uint64_hash { + typedef uint64 data; + unsigned operator()(uint64 x) const { return static_cast(x); } +}; + struct bool_hash { typedef bool data; unsigned operator()(bool x) const { return static_cast(x); } diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h new file mode 100644 index 000000000..659fdc400 --- /dev/null +++ b/src/util/inf_eps_rational.h @@ -0,0 +1,409 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + inf_eps_rational.h + +Abstract: + + Rational numbers with infinity and epsilon. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-4-23. + +Revision History: + +--*/ +#ifndef _INF_EPS_RATIONAL_H_ +#define _INF_EPS_RATIONAL_H_ +#include +#include +#include"debug.h" +#include"vector.h" +#include"rational.h" + +template +class inf_eps_rational { + rational m_infty; + Numeral m_r; + public: + + unsigned hash() const { + return m_infty.hash() ^ m_r.hash(); + } + + struct hash_proc { unsigned operator()(inf_eps_rational const& r) const { return r.hash(); } }; + + struct eq_proc { bool operator()(inf_eps_rational const& r1, inf_eps_rational const& r2) const { return r1 == r2; } }; + + void swap(inf_eps_rational & n) { + m_infty.swap(n.m_infty); + m_r.swap(n.m_r); + } + + std::string to_string() const { + if (m_infty.is_zero()) { + return m_r.to_string(); + } + std::string si; + if (m_infty.is_one()) { + si = "oo"; + } + else if (m_infty.is_minus_one()) { + si = "-oo"; + } + else { + si = m_infty.to_string() += "*oo"; + } + if (m_r.is_zero()) { + return si; + } + std::string s = "("; + s += si; + s += " + "; + s += m_r.to_string(); + s += ")"; + return s; + } + + inf_eps_rational(): + m_infty(), + m_r() + {} + + inf_eps_rational(const inf_eps_rational & r): + m_infty(r.m_infty), + m_r(r.m_r) + {} + + explicit inf_eps_rational(int n): + m_infty(), + m_r(n) + {} + + explicit inf_eps_rational(Numeral const& r): + m_infty(), + m_r(r) + {} + + explicit inf_eps_rational(rational const& i, Numeral const& r): + m_infty(i), + m_r(r) { + } + + ~inf_eps_rational() {} + + /** + \brief Set inf_eps_rational to 0. + */ + void reset() { + m_infty.reset(); + m_r.reset(); + } + + bool is_int() const { + return m_infty.is_zero() && m_r.is_int(); + } + + bool is_int64() const { + return m_infty.is_zero() && m_r.is_int64(); + } + + bool is_uint64() const { + return m_infty.is_zero() && m_r.is_uint64(); + } + + bool is_rational() const { return m_infty.is_zero() && m_r.is_rational(); } + + int64 get_int64() const { + SASSERT(is_int64()); + return m_r.get_int64(); + } + + uint64 get_uint64() const { + SASSERT(is_uint64()); + return m_r.get_uint64(); + } + + rational const& get_rational() const { + return m_r.get_rational(); + } + + rational const& get_infinitesimal() const { + return m_r.get_infinitesimal(); + } + + rational const& get_infinity() const { + return m_infty; + } + + inf_eps_rational & operator=(const inf_eps_rational & r) { + m_infty = r.m_infty; + m_r = r.m_r; + return *this; + } + + inf_eps_rational & operator=(const rational & r) { + m_infty.reset(); + m_r = r; + return *this; + } + + inf_eps_rational & operator+=(const inf_eps_rational & r) { + m_infty += r.m_infty; + m_r += r.m_r; + return *this; + } + + inf_eps_rational & operator-=(const inf_eps_rational & r) { + m_infty -= r.m_infty; + m_r -= r.m_r; + return *this; + } + + inf_eps_rational & operator+=(const rational & r) { + m_r += r; + return *this; + } + + inf_eps_rational & operator-=(const rational & r) { + m_r -= r; + return *this; + } + + inf_eps_rational & operator*=(const rational & r1) { + m_infty *= r1; + m_r *= r1; + return *this; + } + + inf_eps_rational & operator/=(const rational & r) { + m_infty /= r; + m_r /= r; + return *this; + } + + + inf_eps_rational & operator++() { + ++m_r; + return *this; + } + + const inf_eps_rational operator++(int) { inf_eps_rational tmp(*this); ++(*this); return tmp; } + + inf_eps_rational & operator--() { + --m_r; + return *this; + } + + const inf_eps_rational operator--(int) { inf_eps_rational tmp(*this); --(*this); return tmp; } + + friend inline bool operator==(const inf_eps_rational & r1, const inf_eps_rational & r2) { + return r1.m_infty == r2.m_infty && r1.m_r == r2.m_r; + } + + friend inline bool operator==(const rational & r1, const inf_eps_rational & r2) { + return r1 == r2.m_infty && r2.m_r.is_zero(); + } + + friend inline bool operator==(const inf_eps_rational & r1, const rational & r2) { + return r1.m_infty == r2 && r1.m_r.is_zero(); + } + + friend inline bool operator<(const inf_eps_rational & r1, const inf_eps_rational & r2) { + return + (r1.m_infty < r2.m_infty) || + (r1.m_infty == r2.m_infty && r1.m_r < r2.m_r); + } + + friend inline bool operator<(const rational & r1, const inf_eps_rational & r2) { + return + r2.m_infty.is_pos() || + (r2.m_infty.is_zero() && r1 < r2.m_r); + } + + friend inline bool operator<(const inf_eps_rational & r1, const rational & r2) { + return + r1.m_infty.is_neg() || + (r1.m_infty.is_zero() && r1.m_r < r2); + } + + void neg() { + m_infty.neg(); + m_r.neg(); + } + + bool is_zero() const { + return m_infty.is_zero() && m_r.is_zero(); + } + + bool is_one() const { + return m_infty.is_zero() && m_r.is_one(); + } + + bool is_minus_one() const { + return m_infty.is_zero() && m_r.is_minus_one(); + } + + bool is_neg() const { + return + m_infty.is_neg() || + (m_infty.is_zero() && m_r.is_neg()); + } + + bool is_pos() const { + return + m_infty.is_pos() || + (m_infty.is_zero() && m_r.is_pos()); + } + + bool is_nonneg() const { + return + m_infty.is_pos() || + (m_infty.is_zero() && m_r.is_nonneg()); + } + + bool is_nonpos() const { + return + m_infty.is_neg() || + (m_infty.is_zero() && m_r.is_nonpos()); + } + + friend inline rational floor(const inf_eps_rational & r) { + SASSERT(r.m_infty.is_zero()); + return floor(r.m_r); + } + + friend inline rational ceil(const inf_eps_rational & r) { + SASSERT(r.m_infty.is_zero()); + return ceil(r.m_r); + } + + + // Perform: this += c * k + void addmul(const rational & c, const inf_eps_rational & k) { + m_infty.addmul(c, k.m_infty); + m_r.addmul(c, k.m_r); + } + + // Perform: this += c * k + void submul(const rational & c, const inf_eps_rational & k) { + m_infty.submul(c, k.m_infty); + m_r.submul(c, k.m_r); + } +}; + +template +inline bool operator!=(const inf_eps_rational & r1, const inf_eps_rational & r2) { + return !operator==(r1, r2); +} + +template +inline bool operator!=(const rational & r1, const inf_eps_rational & r2) { + return !operator==(r1, r2); +} + +template +inline bool operator!=(const inf_eps_rational & r1, const rational & r2) { + return !operator==(r1, r2); +} + +template +inline bool operator>(const inf_eps_rational & r1, const inf_eps_rational & r2) { + return operator<(r2, r1); +} + +template +inline bool operator>(const inf_eps_rational & r1, const rational & r2) { + return operator<(r2, r1); +} + +template +inline bool operator>(const rational & r1, const inf_eps_rational & r2) { + return operator<(r2, r1); +} + +template +inline bool operator<=(const inf_eps_rational & r1, const inf_eps_rational & r2) { + return !operator>(r1, r2); +} + +template +inline bool operator<=(const rational & r1, const inf_eps_rational & r2) { + return !operator>(r1, r2); +} + +template +inline bool operator<=(const inf_eps_rational & r1, const rational & r2) { + return !operator>(r1, r2); +} + +template +inline bool operator>=(const inf_eps_rational & r1, const inf_eps_rational & r2) { + return !operator<(r1, r2); +} + +template +inline bool operator>=(const rational & r1, const inf_eps_rational & r2) { + return !operator<(r1, r2); +} + +template +inline bool operator>=(const inf_eps_rational & r1, const rational & r2) { + return !operator<(r1, r2); +} + +template +inline inf_eps_rational operator+(const inf_eps_rational & r1, const inf_eps_rational & r2) { + return inf_eps_rational(r1) += r2; +} + +template +inline inf_eps_rational operator-(const inf_eps_rational & r1, const inf_eps_rational & r2) { + return inf_eps_rational(r1) -= r2; +} + +template +inline inf_eps_rational operator-(const inf_eps_rational & r) { + inf_eps_rational result(r); + result.neg(); + return result; +} + +template +inline inf_eps_rational operator*(const rational & r1, const inf_eps_rational & r2) { + inf_eps_rational result(r2); + result *= r1; + return result; +} + +template +inline inf_eps_rational operator*(const inf_eps_rational & r1, const rational & r2) { + return r2 * r1; +} + +template +inline inf_eps_rational operator/(const inf_eps_rational & r1, const rational & r2) { + inf_eps_rational result(r1); + result /= r2; + return result; +} + +template +inline std::ostream & operator<<(std::ostream & target, const inf_eps_rational & r) { + target << r.to_string(); + return target; +} + +template +inline inf_eps_rational abs(const inf_eps_rational & r) { + inf_eps_rational result(r); + if (result.is_neg()) { + result.neg(); + } + return result; +} + +#endif /* _INF_EPS_RATIONAL_H_ */ diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index 9e1753484..5cdfe9e93 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -223,6 +223,7 @@ class inf_rational { } friend inline inf_rational operator*(const rational & r1, const inf_rational & r2); + friend inline inf_rational operator*(const inf_rational & r1, const rational & r2); friend inline inf_rational operator/(const inf_rational & r1, const rational & r2); inf_rational & operator++() { @@ -426,6 +427,10 @@ inline inf_rational operator*(const rational & r1, const inf_rational & r2) { return result; } +inline inf_rational operator*(const inf_rational & r1, const rational & r2) { + return r2 * r1; +} + inline inf_rational operator/(const inf_rational & r1, const rational & r2) { inf_rational result(r1); result.m_first /= r2; diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index f5e5fa9fa..3f2e224d9 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -231,9 +231,8 @@ void * memory::allocate(size_t s) { return 0; s = s + sizeof(size_t); // we allocate an extra field! void * r = malloc(s); - if (r == 0) { + if (r == 0) throw_out_of_memory(); - } *(static_cast(r)) = s; g_memory_thread_alloc_size += s; if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) { diff --git a/src/util/vector.h b/src/util/vector.h index 704452d0f..c9ed900a9 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -432,24 +432,29 @@ typedef svector unsigned_vector; typedef svector char_vector; typedef svector double_vector; -template -struct vector_hash { +template +struct vector_hash_tpl { Hash m_hash; - typedef vector data; + typedef Vec data; unsigned operator()(data const& v, unsigned idx) const { return m_hash(v[idx]); } - vector_hash(Hash const& h = Hash()):m_hash(h) {} + vector_hash_tpl(Hash const& h = Hash()):m_hash(h) {} unsigned operator()(data const& v) const { if (v.empty()) { return 778; } - return get_composite_hash, vector_hash>(v, v.size()); + return get_composite_hash, vector_hash_tpl>(v, v.size()); } - }; +template +struct vector_hash : public vector_hash_tpl > {}; + +template +struct svector_hash : public vector_hash_tpl > {}; + #endif /* _VECTOR_H_ */