diff --git a/src/ast/card_decl_plugin.cpp b/src/ast/card_decl_plugin.cpp index 20c9af09f..acb6d8adb 100644 --- a/src/ast/card_decl_plugin.cpp +++ b/src/ast/card_decl_plugin.cpp @@ -47,7 +47,7 @@ void card_decl_plugin::get_op_names(svector & op_names, symbol con app * card_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) { - parameter param(1); + parameter param(k); return m.mk_app(m_fid, OP_AT_MOST_K, 1, ¶m, num_args, args, m.mk_bool_sort()); } diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp index ecba59f1c..edae63108 100644 --- a/src/smt/theory_card.cpp +++ b/src/smt/theory_card.cpp @@ -54,24 +54,22 @@ namespace smt { TRACE("card", tout << "internalize: " << mk_pp(atom, m) << "\n";); - if (k >= atom->get_num_args()) { - - NOT_IMPLEMENTED_YET(); - } - if (k == 0) { - NOT_IMPLEMENTED_YET(); - } - SASSERT(0 < k && k < atom->get_num_args()); SASSERT(!ctx.b_internalized(atom)); - bool_var bv = ctx.mk_bool_var(atom); - card* c = alloc(card, bv, k); - add_card(c); + bool_var abv = ctx.mk_bool_var(atom); + + if (k >= atom->get_num_args()) { + literal lit(abv); + ctx.mk_th_axiom(get_id(), 1, &lit); + return true; + } + + card* c = alloc(card, abv, k); for (unsigned i = 0; i < num_args; ++i) { expr* arg = atom->get_arg(i); if (!ctx.b_internalized(arg)) { ctx.internalize(arg, false); } - + bool_var bv; bool has_bv = false; if (!m.is_not(arg) && ctx.b_internalized(arg)) { bv = ctx.get_bool_var(arg); @@ -100,7 +98,23 @@ namespace smt { ctx.mark_as_relevant(tmp); } c->m_args.push_back(bv); - add_watch(bv, c); + if (0 < k) { + add_watch(bv, c); + } + } + if (0 < k) { + add_card(c); + } + else { + // bv <=> (and (not bv1) ... (not bv_n)) + literal_vector& lits = get_lits(); + lits.push_back(literal(abv)); + for (unsigned i = 0; i < c->m_args.size(); ++i) { + ctx.mk_th_axiom(get_id(), ~literal(abv), ~literal(c->m_args[i])); + lits.push_back(literal(c->m_args[i])); + } + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + dealloc(c); } return true; } @@ -309,7 +323,12 @@ namespace smt { #if 0 -class sorting { +class sorting_network { + ast_manager& m; + expr_ref_vector m_es; + expr_ref_vector* m_current; + expr_ref_vector* m_next; + void exchange(unsigned i, unsigned j, expr_ref_vector& es) { SASSERT(i <= j); if (i == j) { @@ -338,7 +357,7 @@ class sorting { next((k * i) + (k / 2) + j) = current((k * i) + (2 * j) + 1); } } - + std::swap(m_current, m_next); sort(k / 2); for (unsigned i = 0; i < m_es.size() / k; ++i) { @@ -346,7 +365,7 @@ class sorting { next((k * i) + (2 * j)) = current((k * i) + j); next((k * i) + (2 * j) + 1) = current((k * i) + (k / 2) + j); } - + for (unsigned j = 0; j < (k / 2) - 1; ++j) { exchange(next((k * i) + (2 * j) + 1), next((k * i) + (2 * (j + 1)))); } @@ -355,105 +374,99 @@ class sorting { } } - private Term[] Merge(Term[] l1, Term[] l2) - { - if (l1.Length == 0) - { - return l2; - } - else if (l2.Length == 0) - { - return l1; - } - else if (l1.Length == 1 && l2.Length == 1) - { - var merged = new Term[2]; - merged[0] = l1[0]; - merged[1] = l2[0]; - Exchange(0, 1, merged); - return merged; - } - - var l1o = l1.Length / 2; - var l2o = l2.Length / 2; - var l1e = (l1.Length % 2 == 1) ? l1o + 1 : l1o; - var l2e = (l2.Length % 2 == 1) ? l2o + 1 : l2o; - - Term[] evenl1 = new Term[l1e]; - Term[] oddl1 = new Term[l1o]; - for (int i = 0; i < l1.Length; ++i) - { - if (i % 2 == 0) - { - evenl1[i / 2] = l1[i]; - } - else - { - oddl1[i / 2] = l1[i]; - } - } - - Term[] evenl2 = new Term[l2e]; - Term[] oddl2 = new Term[l2o]; - for (int i = 0; i < l2.Length; ++i) - { - if (i % 2 == 0) - { - evenl2[i / 2] = l2[i]; - } - else - { - oddl2[i / 2] = l2[i]; - } - } - - var even = Merge(evenl1, evenl2); - var odd = Merge(oddl1, oddl2); - - Term[] merge = new Term[l1.Length + l2.Length]; - - for (int i = 0; i < merge.Length; ++i) - { - if (i % 2 == 0) - { - merge[i] = even[i / 2]; - if (i > 0) - { - Exchange(i - 1, i, merge); - } - } - else - { - if (i / 2 < odd.Length) - { - merge[i] = odd[i / 2]; - } - else - { - merge[i] = even[(i / 2) + 1]; - } - } - } - - return merge; + expr_ref_vector merge(expr_ref_vector const& l1, expr_ref_vector& l2) { + if (l1.empty()) { + return l2; } + if (l2.empty()) { + return l1; + } + expr_ref_vector result(m); + if (l1.size() == 1 && l2.size() == 1) { + result.push_back(l1[0]); + result.push_back(l2[0]); + exchange(0, 1, result); + return result; + } + unsigned l1o = l1.size()/2; + unsigned l2o = l2.size()/2; + unsigned l1e = (l1.size() % 2 == 1) ? l1o + 1 : l1o; + unsigned l2e = (l2.size() % 2 == 1) ? l2o + 1 : l2o; + expr_ref_vector evenl1(m, l1e); + expr_ref_vector oddl1(m, l1o); + expr_ref_vector evenl2(m, l2e); + expr_ref_vector oddl2(m, l2o); + for (unsigned i = 0; i < l1.size(); ++i) { + if (i % 2 == 0) { + evenl1[i/2] = l1[i]; + } + else { + oddl1[i/2] = l1[i]; + } + } + for (unsigned i = 0; i < l2.size(); ++i) { + if (i % 2 == 0) { + evenl2[i/2] = l2[i]; + } + else { + oddl2[i/2] = l2[i]; + } + } + expr_ref_vector even = merge(evenl1, evenl2); + expr_ref_vector odd = merge(oddl1, oddl2); + result.resize(l1.size() + l2.size()); + for (unsigned i = 0; i < result.size(); ++i) { + if (i % 2 == 0) { + result[i] = even[i/2].get(); + if (i > 0) { + exchange(i - 1, i, result); + } + } + else { + if (i /2 < odd.size()) { + result[i] = odd[i/2].get(); + } + else { + result[i] = even[(i/2)+1].get(); + } + } + } + return result; + } + +public: + sorting_network(ast_manager& m): + m(m), + m_es(m), + m_current(0), + m_next(0) + {} + + expr_ref_vector operator()(expr_ref_vector const& inputs) { + if (inputs.size() <= 1) { + return inputs; + } + m_es.reset(); + m_es.append(inputs); + while (!is_power_of2(m_es.size())) { + m_es.push_back(m.mk_false()); + } + m_es.reverse(); + for (unsigned i = 0; i < m_es.size(); ++i) { + current(i) = i; + } + unsigned k = 2; + while (k <= m_es.size()) { + sort(k); + // TBD + k *= 2; + } + } }; Sorting networks used in Formula: -namespace Microsoft.Formula.Execution -{ - using System; - using System.Diagnostics.Contracts; - using Microsoft.Z3; - - internal class SortingNetwork - { - private Term[] elements; - private int[] current; - private int[] next; - public SortingNetwork(SymbolicState owner, Term[] inputs, Sort sortingDomain) { Contract.Requires(owner != null && inputs != null && sortingDomain != null); @@ -506,114 +519,7 @@ namespace Microsoft.Formula.Execution } } - public Term[] Outputs - { - get { return elements; } - } - public int Size - { - get; - private set; - } - - public SymbolicState Owner - { - get; - private set; - } - - - private void Swap() - { - var tmp = current; - current = next; - next = tmp; - } - - private Term[] Merge(Term[] l1, Term[] l2) - { - if (l1.Length == 0) - { - return l2; - } - else if (l2.Length == 0) - { - return l1; - } - else if (l1.Length == 1 && l2.Length == 1) - { - var merged = new Term[2]; - merged[0] = l1[0]; - merged[1] = l2[0]; - Exchange(0, 1, merged); - return merged; - } - - var l1o = l1.Length / 2; - var l2o = l2.Length / 2; - var l1e = (l1.Length % 2 == 1) ? l1o + 1 : l1o; - var l2e = (l2.Length % 2 == 1) ? l2o + 1 : l2o; - - Term[] evenl1 = new Term[l1e]; - Term[] oddl1 = new Term[l1o]; - for (int i = 0; i < l1.Length; ++i) - { - if (i % 2 == 0) - { - evenl1[i / 2] = l1[i]; - } - else - { - oddl1[i / 2] = l1[i]; - } - } - - Term[] evenl2 = new Term[l2e]; - Term[] oddl2 = new Term[l2o]; - for (int i = 0; i < l2.Length; ++i) - { - if (i % 2 == 0) - { - evenl2[i / 2] = l2[i]; - } - else - { - oddl2[i / 2] = l2[i]; - } - } - - var even = Merge(evenl1, evenl2); - var odd = Merge(oddl1, oddl2); - - Term[] merge = new Term[l1.Length + l2.Length]; - - for (int i = 0; i < merge.Length; ++i) - { - if (i % 2 == 0) - { - merge[i] = even[i / 2]; - if (i > 0) - { - Exchange(i - 1, i, merge); - } - } - else - { - if (i / 2 < odd.Length) - { - merge[i] = odd[i / 2]; - } - else - { - merge[i] = even[(i / 2) + 1]; - } - } - } - - return merge; - } - } } diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp new file mode 100644 index 000000000..7d257d86e --- /dev/null +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -0,0 +1,431 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + lia2card_tactic.cpp + +Abstract: + + Convert 0-1 integer variables cardinality constraints to built-in cardinality operator. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-5 + +Notes: + +--*/ +#include"tactical.h" +#include"cooperate.h" +#include"bound_manager.h" +#include"ast_pp.h" +#include"expr_safe_replace.h" // NB: should use proof-producing expr_substitute in polished version. + +#include"card_decl_plugin.h" +#include"arith_decl_plugin.h" + +class lia2card_tactic : public tactic { + + struct imp { + typedef obj_hashtable expr_set; + ast_manager & m; + arith_util a; + card_util m_card; + obj_map > m_uses; + obj_map m_converted; + expr_set m_01s; + + imp(ast_manager & _m, params_ref const & p): + m(_m), + a(m), + m_card(m) { + } + + void set_cancel(bool f) { + } + + void updt_params(params_ref const & 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; + m_01s.reset(); + m_uses.reset(); + m_converted.reset(); + + tactic_report report("cardinality-intro", *g); + + bound_manager bounds(m); + bounds(*g); + + bound_manager::iterator bit = bounds.begin(), bend = bounds.end(); + for (; bit != bend; ++bit) { + expr* x = *bit; + bool s1, s2; + rational lo, hi; + if (a.is_int(x) && + bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() && + bounds.has_upper(x, hi, s2) && !s2 && hi.is_one()) { + m_01s.insert(x); + TRACE("card", tout << "add bound " << mk_pp(x, m) << "\n";); + } + } + if (m_01s.empty()) { + result.push_back(g.get()); + return; + } + expr_set::iterator it = m_01s.begin(), end = m_01s.end(); + for (; it != end; ++it) { + m_uses.insert(*it, ptr_vector()); + } + for (unsigned j = 0; j < g->size(); ++j) { + ast_mark mark; + collect_uses(mark, g->form(j)); + } + + it = m_01s.begin(), end = m_01s.end(); + for (; it != end; ++it) { + if (!validate_uses(m_uses.find(*it))) { + m_uses.remove(*it); + m_01s.remove(*it); + it = m_01s.begin(); + end = m_01s.end(); + } + } + if (m_01s.empty()) { + result.push_back(g.get()); + return; + } + + expr_safe_replace sub(m); + extract_substitution(sub); + + expr_ref new_curr(m); + proof_ref new_pr(m); + + for (unsigned i = 0; i < g->size(); i++) { + expr * curr = g->form(i); + sub(curr, new_curr); + g->update(i, new_curr, new_pr, g->dep(i)); + } + g->inc_depth(); + result.push_back(g.get()); + TRACE("card", g->display(tout);); + SASSERT(g->is_well_sorted()); + + // TBD: convert models for 0-1 variables. + // TBD: support proof conversion (or not..) + } + + void extract_substitution(expr_safe_replace& sub) { + expr_set::iterator it = m_01s.begin(), end = m_01s.end(); + for (; it != end; ++it) { + extract_substitution(sub, *it); + } + } + + void extract_substitution(expr_safe_replace& sub, expr* x) { + ptr_vector const& use_list = m_uses.find(x); + for (unsigned i = 0; i < use_list.size(); ++i) { + expr* u = use_list[i]; + convert_01(sub, u); + } + } + + expr_ref mk_le(expr* x, rational const& bound) { + if (bound.is_pos()) { + return expr_ref(m.mk_true(), m); + } + else if (bound.is_zero()) { + return expr_ref(m.mk_not(mk_01(x)), m); + } + else { + return expr_ref(m.mk_false(), m); + } + } + + expr_ref mk_ge(expr* x, rational const& bound) { + if (bound.is_one()) { + return expr_ref(mk_01(x), m); + } + else if (bound.is_pos()) { + return expr_ref(m.mk_false(), m); + } + else { + return expr_ref(m.mk_true(), m); + } + } + + bool is_01var(expr* x) const { + return m_01s.contains(x); + } + + void convert_01(expr_safe_replace& sub, expr* fml) { + rational n; + unsigned k; + expr_ref_vector args(m); + expr_ref result(m); + expr* x, *y; + if (a.is_le(fml, x, y) || a.is_ge(fml, y, x)) { + if (is_01var(x) && a.is_numeral(y, n)) { + sub.insert(fml, mk_le(x, n)); + return; + } + if (is_01var(y) && a.is_numeral(x, n)) { + sub.insert(fml, mk_ge(y, n)); + return; + } + if (is_add(x, args) && is_unsigned(y, k)) { // x <= k + sub.insert(fml, m_card.mk_at_most_k(args.size(), args.c_ptr(), k)); + return; + } + if (is_add(y, args) && is_unsigned(x, k)) { // k <= y <=> not (y <= k-1) + if (k == 0) + sub.insert(fml, m.mk_true()); + else + sub.insert(fml, m.mk_not(m_card.mk_at_most_k(args.size(), args.c_ptr(), k-1))); + return; + } + UNREACHABLE(); + } + + if (a.is_lt(fml, x, y) || a.is_gt(fml, y, x)) { + if (is_01var(x) && a.is_numeral(y, n)) { + sub.insert(fml, mk_le(x, n-rational(1))); + return; + } + if (is_01var(y) && a.is_numeral(x, n)) { + sub.insert(fml, mk_ge(y, n+rational(1))); + return; + } + if (is_add(x, args) && is_unsigned(y, k)) { // x < k + if (k == 0) + sub.insert(fml, m.mk_false()); + else + sub.insert(fml, m_card.mk_at_most_k(args.size(), args.c_ptr(), k-1)); + return; + } + + if (is_add(y, args) && is_unsigned(x, k)) { // k < y <=> not (y <= k) + sub.insert(fml, m.mk_not(m_card.mk_at_most_k(args.size(), args.c_ptr(), k))); + return; + } + UNREACHABLE(); + } + if (m.is_eq(fml, x, y)) { + if (!is_01var(x)) { + std::swap(x, y); + } + if (is_01var(x) && a.is_numeral(y, n)) { + if (n.is_one()) { + sub.insert(fml, mk_01(x)); + } + else if (n.is_zero()) { + sub.insert(fml, m.mk_not(mk_01(x))); + } + else { + sub.insert(fml, m.mk_false()); + } + return; + } + UNREACHABLE(); + } + if (is_sum(fml)) { + SASSERT(m_uses.contains(fml)); + ptr_vector const& u = m_uses.find(fml); + for (unsigned i = 0; i < u.size(); ++i) { + convert_01(sub, u[i]); + } + return; + } + UNREACHABLE(); + } + + expr_ref mk_01(expr* x) { + expr* r; + SASSERT(is_01var(x)); + if (!m_converted.find(x, r)) { + symbol name = to_app(x)->get_decl()->get_name(); + r = m.mk_fresh_const(name.str().c_str(), m.mk_bool_sort()); + m_converted.insert(x, r); + } + return expr_ref(r, m); + } + + + bool is_add(expr* x, expr_ref_vector& args) { + if (a.is_add(x)) { + app* ap = to_app(x); + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + args.push_back(mk_01(ap->get_arg(i))); + } + return true; + } + else { + return false; + } + } + + bool validate_uses(ptr_vector const& use_list) { + for (unsigned i = 0; i < use_list.size(); ++i) { + if (!validate_use(use_list[i])) { + return false; + } + } + return true; + } + + bool validate_use(expr* fml) { + expr* x, *y; + if (a.is_le(fml, x, y) || + a.is_ge(fml, x, y) || + a.is_lt(fml, x, y) || + a.is_gt(fml, x, y) || + m.is_eq(fml, x, y)) { + if (a.is_numeral(x)) { + std::swap(x,y); + } + if ((is_one(y) || a.is_zero(y)) && is_01var(x)) + return true; + if (a.is_numeral(y) && is_sum(x) && !m.is_eq(fml)) { + return true; + } + } + if (is_sum(fml)) { + SASSERT(m_uses.contains(fml)); + ptr_vector const& u = m_uses.find(fml); + for (unsigned i = 0; i < u.size(); ++i) { + if (!validate_use(u[i])) { + return false; + } + } + return true; + } + TRACE("card", tout << "Use not validated: " << mk_pp(fml, m) << "\n";); + + return false; + } + + bool is_sum(expr* x) const { + if (a.is_add(x)) { + app* ap = to_app(x); + for (unsigned i = 0; i < ap->get_num_args(); ++i) { + if (!is_01var(ap->get_arg(i))) { + return false; + } + } + return true; + } + return false; + } + + bool is_unsigned(expr* x, unsigned& k) { + rational r; + if (a.is_numeral(x, r) && r.is_unsigned()) { + k = r.get_unsigned(); + SASSERT(rational(k) == r); + return true; + } + else { + return false; + } + } + + bool is_one(expr* x) { + rational r; + return a.is_numeral(x, r) && r.is_one(); + } + + void collect_uses(ast_mark& mark, expr* f) { + ptr_vector todo; + todo.push_back(f); + while (!todo.empty()) { + f = todo.back(); + todo.pop_back(); + if (mark.is_marked(f)) { + continue; + } + mark.mark(f, true); + if (is_var(f)) { + continue; + } + if (is_quantifier(f)) { + todo.push_back(to_quantifier(f)->get_expr()); + continue; + } + app* a = to_app(f); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr* arg = a->get_arg(i); + if (!m_uses.contains(arg)) { + m_uses.insert(arg, ptr_vector()); + } + m_uses.find(arg).push_back(a); + todo.push_back(arg); + } + } + } + }; + + imp * m_imp; + params_ref m_params; +public: + lia2card_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(lia2card_tactic, m, m_params); + } + + virtual ~lia2card_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + } + + 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); + } +}; + +tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(lia2card_tactic, m, p)); +} + diff --git a/src/tactic/arith/lia2card_tactic.h b/src/tactic/arith/lia2card_tactic.h new file mode 100644 index 000000000..69a5f3f60 --- /dev/null +++ b/src/tactic/arith/lia2card_tactic.h @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + lia2card_tactic.h + +Abstract: + + Extract 0-1 integer variables used in + cardinality constraints and replace them by Booleans. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-5 + +Notes: + +--*/ +#ifndef _LIA2CARD_TACTIC_H_ +#define _LIA2CARD_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("lia2card", "introduce cardinality constraints from 0-1 integer.", "mk_lia2card_tactic(m, p)") +*/ + +#endif