diff --git a/scripts/mk_project.py b/scripts/mk_project.py index ccae41dcb..e92899436 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -58,7 +58,7 @@ def init_project_def(): add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base') add_lib('transforms', ['muz', 'hilbert'], 'muz/transforms') add_lib('rel', ['muz', 'transforms'], 'muz/rel') - add_lib('pdr', ['muz', 'transforms', 'arith_tactics', 'smt_tactic'], 'muz/pdr') + add_lib('pdr', ['muz', 'transforms', 'arith_tactics', 'core_tactics', 'smt_tactic'], 'muz/pdr') add_lib('clp', ['muz', 'transforms'], 'muz/clp') add_lib('tab', ['muz', 'transforms'], 'muz/tab') add_lib('bmc', ['muz', 'transforms'], 'muz/bmc') diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index aab7b1388..d2ac29689 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -47,6 +47,7 @@ Notes: #include "dl_boogie_proof.h" #include "qe_util.h" #include "scoped_proof.h" +#include "blast_term_ite_tactic.h" namespace pdr { @@ -601,7 +602,7 @@ namespace pdr { th_rewriter rw(m); rw(fml); if (ctx.is_dl() || ctx.is_utvpi()) { - hoist_non_bool_if(fml); + blast_term_ite(fml); } TRACE("pdr", tout << mk_pp(fml, m) << "\n";); SASSERT(is_ground(fml)); diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp index f122f1e2c..33c98fae4 100644 --- a/src/muz/pdr/pdr_util.cpp +++ b/src/muz/pdr/pdr_util.cpp @@ -1030,68 +1030,6 @@ namespace pdr { fml = m.mk_and(conjs.size(), conjs.c_ptr()); } - // - // (f (if c1 (if c2 e1 e2) e3) b c) -> - // (if c1 (if c2 (f e1 b c) - - class ite_hoister { - ast_manager& m; - public: - ite_hoister(ast_manager& m): m(m) {} - - br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { - if (m.is_ite(f)) { - return BR_FAILED; - } - for (unsigned i = 0; i < num_args; ++i) { - expr* c, *t, *e; - if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) { - expr_ref e1(m), e2(m); - ptr_vector args1(num_args, args); - args1[i] = t; - e1 = m.mk_app(f, num_args, args1.c_ptr()); - if (t == e) { - result = e1; - return BR_REWRITE1; - } - args1[i] = e; - e2 = m.mk_app(f, num_args, args1.c_ptr()); - result = m.mk_app(f, num_args, args); - result = m.mk_ite(c, e1, e2); - return BR_REWRITE3; - } - } - return BR_FAILED; - } - }; - - struct ite_hoister_cfg: public default_rewriter_cfg { - ite_hoister m_r; - bool rewrite_patterns() const { return false; } - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - return m_r.mk_app_core(f, num, args, result); - } - ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {} - }; - - class ite_hoister_star : public rewriter_tpl { - ite_hoister_cfg m_cfg; - public: - ite_hoister_star(ast_manager & m, params_ref const & p): - rewriter_tpl(m, false, m_cfg), - m_cfg(m, p) {} - }; - - void hoist_non_bool_if(expr_ref& fml) { - ast_manager& m = fml.get_manager(); - scoped_no_proof _sp(m); - params_ref p; - ite_hoister_star ite_rw(m, p); - expr_ref tmp(m); - ite_rw(fml, tmp); - fml = tmp; - } - class test_diff_logic { ast_manager& m; arith_util a; @@ -1441,7 +1379,6 @@ namespace pdr { } -template class rewriter_tpl; template class rewriter_tpl; diff --git a/src/muz/pdr/pdr_util.h b/src/muz/pdr/pdr_util.h index 446bde8aa..150cf2bb5 100644 --- a/src/muz/pdr/pdr_util.h +++ b/src/muz/pdr/pdr_util.h @@ -143,12 +143,6 @@ namespace pdr { */ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml); - /** - \brief hoist non-boolean if expressions. - */ - void hoist_non_bool_if(expr_ref& fml); - - /** \brief normalize coefficients in polynomials so that least coefficient is 1. */ diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 07d256d9e..10fbc05c5 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -71,14 +71,15 @@ namespace opt { * add at-most-one constraint with blocking */ - bool step() { + lbool step() { + IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step)\n";); expr_ref_vector assumptions(m), block_vars(m); for (unsigned i = 0; i < m_soft.size(); ++i) { assumptions.push_back(m.mk_not(m_aux[i].get())); } lbool is_sat = s.check_sat(assumptions.size(), assumptions.c_ptr()); if (is_sat != l_false) { - return true; + return is_sat; } ptr_vector core; @@ -102,7 +103,7 @@ namespace opt { s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get())); } assert_at_most_one(block_vars); - return false; + return l_false; } private: @@ -139,23 +140,28 @@ namespace opt { s.push(); fu_malik fm(m, s, soft_constraints); - while (!fm.step()); - - // Get a list of satisfying soft_constraints - model_ref model; - s.get_model(model); - - expr_ref_vector result(m); - for (unsigned i = 0; i < soft_constraints.size(); ++i) { - expr_ref val(m); - VERIFY(model->eval(soft_constraints[i].get(), val)); - if (!m.is_false(val)) { - result.push_back(soft_constraints[i].get()); - } - } - soft_constraints.reset(); - soft_constraints.append(result); + lbool is_sat = l_true; + do { + is_sat = fm.step(); + } + while (is_sat == l_false); + + if (is_sat == l_true) { + // Get a list of satisfying soft_constraints + model_ref model; + s.get_model(model); + expr_ref_vector result(m); + for (unsigned i = 0; i < soft_constraints.size(); ++i) { + expr_ref val(m); + VERIFY(model->eval(soft_constraints[i].get(), val)); + if (!m.is_false(val)) { + result.push_back(soft_constraints[i].get()); + } + } + soft_constraints.reset(); + soft_constraints.append(result); + } s.pop(1); } // We are done and soft_constraints has diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index cf0d5f5a6..ff01a4792 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -935,13 +935,13 @@ public: // Return true if there is an edge source --> target (also counting disabled edges). // If there is such edge, return its edge_id in parameter id. - bool get_edge_id(dl_var source, dl_var target, edge_id & id) { - edge_id_vector & edges = m_out_edges[source]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); + bool get_edge_id(dl_var source, dl_var target, edge_id & id) const { + edge_id_vector const & edges = m_out_edges[source]; + typename edge_id_vector::const_iterator it = edges.begin(); + typename edge_id_vector::const_iterator end = edges.end(); for (; it != end; ++it) { id = *it; - edge & e = m_edges[id]; + edge const & e = m_edges[id]; if (e.get_target() == target) { return true; } diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index a19cae0a2..8d3a9a75b 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -93,7 +93,7 @@ namespace smt { // Initialize the network with a feasible spanning tree void initialize(); - edge_id get_edge_id(dl_var source, dl_var target); + edge_id get_edge_id(dl_var source, dl_var target) const; void update_potentials(); @@ -112,6 +112,9 @@ namespace smt { std::string display_spanning_tree(); + bool edge_in_tree(edge_id id) const; + bool edge_in_tree(node src, node dst) const; + bool check_well_formed(); public: diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 3b4b93d51..25ff6ee0c 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -137,7 +137,7 @@ namespace smt { } template - edge_id network_flow::get_edge_id(dl_var source, dl_var target) { + edge_id network_flow::get_edge_id(dl_var source, dl_var target) const { // m_upwards[source] decides which node is the real source edge_id id; VERIFY(m_upwards[source] ? m_graph.get_edge_id(source, target, id) : m_graph.get_edge_id(target, source, id)); @@ -234,6 +234,7 @@ namespace smt { m_delta = m_flows[e_id]; src = u; tgt = m_pred[u]; + SASSERT(edge_in_tree(src,tgt)); m_in_edge_dir = true; } } @@ -245,6 +246,7 @@ namespace smt { m_delta = m_flows[e_id]; src = u; tgt = m_pred[u]; + SASSERT(edge_in_tree(src,tgt)); m_in_edge_dir = false; } } @@ -267,10 +269,12 @@ namespace smt { node q = m_graph.get_target(m_entering_edge); node u = m_graph.get_source(m_leaving_edge); node v = m_graph.get_target(m_leaving_edge); + // v is parent of u so T_u does not contain root node if (m_pred[u] == v) { std::swap(u, v); } + SASSERT(m_pred[v] == u); for (node n = p; n != -1; n = m_pred[n]) { // q should be in T_v so swap p and q @@ -285,13 +289,10 @@ namespace smt { tout << u << ", " << v << ") leaves\n"; }); - node x = m_final[p]; - node y = m_thread[x]; - node z = m_final[q]; // Update m_pred (for nodes in the stem from q to v) node n = q; - node last = m_pred[v]; + node last = m_pred[v]; // review: m_pred[v] == u holds, so why not 'u'? node prev = p; while (n != last && n != -1) { node next = m_pred[n]; @@ -303,6 +304,11 @@ namespace smt { TRACE("network_flow", tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Upwards", m_upwards);); + node x = m_final[p]; + node y = m_thread[x]; + node z = m_final[q]; + + // Do this before updating data structures node gamma_p = m_pred[m_thread[m_final[p]]]; node gamma_v = m_pred[m_thread[m_final[v]]]; @@ -430,6 +436,8 @@ namespace smt { if (!bounded) return false; update_flows(); if (m_entering_edge != m_leaving_edge) { + SASSERT(edge_in_tree(m_leaving_edge)); + SASSERT(!edge_in_tree(m_entering_edge)); m_states[m_entering_edge] = BASIS; m_states[m_leaving_edge] = (m_flows[m_leaving_edge].is_zero()) ? LOWER : UPPER; update_spanning_tree(); @@ -494,6 +502,7 @@ namespace smt { } static int get_final(int root, svector const & thread, svector const & depth) { + // really final or should one take into account connected tree? int n = root; while (depth[thread[n]] > depth[root]) { n = thread[n]; @@ -501,19 +510,76 @@ namespace smt { return n; } + template + bool network_flow::edge_in_tree(edge_id id) const { + return m_states[id] == BASIS; + } + + template + bool network_flow::edge_in_tree(node src, node dst) const { + return edge_in_tree(get_edge_id(src,dst)); + } + + /** + \brief Check invariants of main data-structures. + + Spanning tree of m_graph + root is represented using: + + svector m_states; edge_id |-> edge_state + svector m_upwards; node |-> bool + svector m_pred; node |-> node + svector m_depth; node |-> int + svector m_thread; node |-> node + svector m_rev_thread; node |-> node + svector m_final; node |-> node + + m_thread[m_rev_thread[n]] == n for each node n + + Tree is determined by m_pred: + - m_pred[root] == -1 + - m_pred[n] = m != n for each node n, acyclic until reaching root. + - m_depth[m_pred[n]] + 1 == m_depth[n] for each n != root + + m_thread is a linked list traversing all nodes. + Furthermore, the nodes linked in m_thread follows a + depth-first traversal order. + + m_final[n] is deepest most node in a sub-tree rooted at n. + + */ + template bool network_flow::check_well_formed() { node root = m_pred.size()-1; + // Check that m_thread traverses each node. + // This gets checked using union-find as well. + svector found(m_thread.size(), false); + found[root] = true; + for (node x = m_thread[root]; x != root; x = m_thread[x]) { + found[x] = true; + } + for (unsigned i = 0; i < found.size(); ++i) { + SASSERT(found[i]); + } + + // m_pred is acyclic, and points to root. + SASSERT(m_pred[root] == -1); + SASSERT(m_depth[root] == 0); + for (node i = 0; i < root; ++i) { + SASSERT(m_depth[m_pred[i]] < m_depth[i]); + } + // m_upwards show correct direction for (unsigned i = 0; i < m_upwards.size(); ++i) { node p = m_pred[i]; edge_id id; - SASSERT(m_upwards[i] == m_graph.get_edge_id(i, p, id)); + SASSERT(!m_upwards[i] || m_graph.get_edge_id(i, p, id)); } // m_depth[x] denotes distance from x to the root node for (node x = m_thread[root]; x != root; x = m_thread[x]) { + SASSERT(m_depth[x] > 0); SASSERT(m_depth[x] == m_depth[m_pred[x]] + 1); } @@ -540,7 +606,7 @@ namespace smt { // All nodes belong to the same spanning tree for (unsigned i = 0; i < roots.size(); ++i) { - SASSERT(i == 0 ? roots[i] + roots.size() == 0 : roots[i] == 0); + SASSERT(roots[i] + roots.size() == 0 || roots[i] >= 0); } // m_flows are zero on non-basic edges diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp new file mode 100644 index 000000000..c69849253 --- /dev/null +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -0,0 +1,221 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + blast_term_ite_tactic.cpp + +Abstract: + + Blast term if-then-else by hoisting them up. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-4 + +Notes: + +--*/ +#include"tactical.h" +#include"defined_names.h" +#include"rewriter_def.h" +#include"filter_model_converter.h" +#include"cooperate.h" +#include"scoped_proof.h" + + + +// +// (f (if c1 (if c2 e1 e2) e3) b c) -> +// (if c1 (if c2 (f e1 b c) +// + + +class blast_term_ite_tactic : public tactic { + + struct rw_cfg : public default_rewriter_cfg { + ast_manager& m; + unsigned long long m_max_memory; // in bytes + unsigned m_num_fresh; // number of expansions + + rw_cfg(ast_manager & _m, params_ref const & p): + m(_m), + m_num_fresh(0) { + updt_params(p); + } + + void updt_params(params_ref const & p) { + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + } + + bool max_steps_exceeded(unsigned num_steps) const { + cooperate("blast term ite"); + if (memory::get_allocation_size() > m_max_memory) + throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + return false; + } + + br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { + if (m.is_ite(f)) { + return BR_FAILED; + } + for (unsigned i = 0; i < num_args; ++i) { + expr* c, *t, *e; + if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) { + expr_ref e1(m), e2(m); + ptr_vector args1(num_args, args); + args1[i] = t; + ++m_num_fresh; + e1 = m.mk_app(f, num_args, args1.c_ptr()); + if (t == e) { + result = e1; + return BR_REWRITE1; + } + args1[i] = e; + e2 = m.mk_app(f, num_args, args1.c_ptr()); + result = m.mk_app(f, num_args, args); + result = m.mk_ite(c, e1, e2); + return BR_REWRITE3; + } + } + return BR_FAILED; + } + + bool rewrite_patterns() const { return false; } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + return mk_app_core(f, num, args, result); + } + + }; + + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + + rw(ast_manager & m, params_ref const & p): + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(m, p) { + } + }; + + struct imp { + ast_manager & m; + rw m_rw; + + imp(ast_manager & _m, params_ref const & p): + m(_m), + m_rw(m, p) { + } + + void set_cancel(bool f) { + m_rw.set_cancel(f); + } + + void updt_params(params_ref const & p) { + m_rw.cfg().updt_params(p); + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(g->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("blast-term-ite", *g); + bool produce_proofs = g->proofs_enabled(); + + expr_ref new_curr(m); + proof_ref new_pr(m); + unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + expr * curr = g->form(idx); + m_rw(curr, new_curr, new_pr); + if (produce_proofs) { + proof * pr = g->pr(idx); + new_pr = m.mk_modus_ponens(pr, new_pr); + } + g->update(idx, new_curr, new_pr, g->dep(idx)); + } + report_tactic_progress(":blast-term-ite-consts", m_rw.m_cfg.m_num_fresh); + g->inc_depth(); + result.push_back(g.get()); + TRACE("blast_term_ite", g->display(tout);); + SASSERT(g->is_well_sorted()); + } + }; + + imp * m_imp; + params_ref m_params; +public: + blast_term_ite_tactic(ast_manager & m, params_ref const & p): + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(blast_term_ite_tactic, m, m_params); + } + + virtual ~blast_term_ite_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->m_rw.cfg().updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + insert_max_steps(r); + r.insert("max_args", CPK_UINT, + "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic."); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m; + imp * d = m_imp; + #pragma omp critical (tactic_cancel) + { + m_imp = 0; + } + dealloc(d); + d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) + { + m_imp = d; + } + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } + + static void blast_term_ite(expr_ref& fml) { + ast_manager& m = fml.get_manager(); + scoped_no_proof _sp(m); + params_ref p; + rw ite_rw(m, p); + expr_ref tmp(m); + ite_rw(fml, tmp); + fml = tmp; + } +}; + +tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(blast_term_ite_tactic, m, p)); +} + +void blast_term_ite(expr_ref& fml) { + blast_term_ite_tactic::blast_term_ite(fml); +} diff --git a/src/tactic/core/blast_term_ite_tactic.h b/src/tactic/core/blast_term_ite_tactic.h new file mode 100644 index 000000000..6756b29d3 --- /dev/null +++ b/src/tactic/core/blast_term_ite_tactic.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + blast_term_ite_tactic.h + +Abstract: + + Blast term if-then-else by hoisting them up. + This is expensive but useful in some cases, such as + for enforcing constraints being in difference logic. + Use elim-term-ite elsewhere when possible. + + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-4 + +Notes: + +--*/ +#ifndef _BLAST_TERM_ITE_TACTIC_H_ +#define _BLAST_TERM_ITE_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_blast_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("blast-term-ite", "blast term if-then-else by hoisting them.", "mk_blast_term_ite_tactic(m, p)") +*/ + +void blast_term_ite(expr_ref& fml); + +#endif