From ee0abfbfe9e9f743eaf7ac9b154b6a4c700876cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Nov 2013 21:25:02 -0800 Subject: [PATCH] rename card->pb Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 2 +- src/api/api_context.cpp | 2 +- src/api/api_pb.cpp | 6 ++-- ...ard_decl_plugin.cpp => pb_decl_plugin.cpp} | 26 +++++++-------- .../{card_decl_plugin.h => pb_decl_plugin.h} | 26 +++++++-------- src/ast/reg_decl_plugins.cpp | 6 ++-- src/cmd_context/cmd_context.cpp | 4 +-- src/opt/core_maxsat.cpp | 6 ++-- src/smt/theory_card.cpp | 20 ++++++------ src/smt/theory_card.h | 4 +-- src/smt/theory_pb.cpp | 32 +++++++++---------- src/smt/theory_pb.h | 4 +-- src/tactic/arith/lia2card_tactic.cpp | 20 ++++++------ 13 files changed, 79 insertions(+), 79 deletions(-) rename src/ast/{card_decl_plugin.cpp => pb_decl_plugin.cpp} (78%) rename src/ast/{card_decl_plugin.h => pb_decl_plugin.h} (81%) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index d8227a152..29c492368 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -24,7 +24,7 @@ Revision History: #include"bv_decl_plugin.h" #include"datatype_decl_plugin.h" #include"array_decl_plugin.h" -#include"card_decl_plugin.h" +#include"pb_decl_plugin.h" #include"ast_translation.h" #include"ast_pp.h" #include"ast_ll_pp.h" diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 49fa1ab99..8c89740ad 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -109,7 +109,7 @@ namespace api { m_basic_fid = m().get_basic_family_id(); m_arith_fid = m().mk_family_id("arith"); m_bv_fid = m().mk_family_id("bv"); - m_pb_fid = m().mk_family_id("card"); + m_pb_fid = m().mk_family_id("pb"); m_array_fid = m().mk_family_id("array"); m_dt_fid = m().mk_family_id("datatype"); m_datalog_fid = m().mk_family_id("datalog_relation"); diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp index 52290d28a..17fe2f93e 100644 --- a/src/api/api_pb.cpp +++ b/src/api/api_pb.cpp @@ -20,7 +20,7 @@ Revision History: #include"api_log_macros.h" #include"api_context.h" #include"api_util.h" -#include"card_decl_plugin.h" +#include"pb_decl_plugin.h" extern "C" { @@ -30,7 +30,7 @@ extern "C" { LOG_Z3_mk_atmost(c, num_args, args, k); RESET_ERROR_CODE(); parameter param(k); - card_util util(mk_c(c)->m()); + pb_util util(mk_c(c)->m()); ast* a = util.mk_at_most_k(num_args, to_exprs(args), k); mk_c(c)->save_ast_trail(a); check_sorts(c, a); @@ -45,7 +45,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_pble(c, num_args, args, coeffs, k); RESET_ERROR_CODE(); - card_util util(mk_c(c)->m()); + pb_util util(mk_c(c)->m()); ast* a = util.mk_le(num_args, coeffs, to_exprs(args), k); mk_c(c)->save_ast_trail(a); check_sorts(c, a); diff --git a/src/ast/card_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp similarity index 78% rename from src/ast/card_decl_plugin.cpp rename to src/ast/pb_decl_plugin.cpp index 6a15792e5..0f9f479dd 100644 --- a/src/ast/card_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -3,7 +3,7 @@ Copyright (c) 2013 Microsoft Corporation Module Name: - card_decl_plugin.cpp + pb_decl_plugin.cpp Abstract: @@ -17,14 +17,14 @@ Revision History: --*/ -#include "card_decl_plugin.h" +#include "pb_decl_plugin.h" -card_decl_plugin::card_decl_plugin(): +pb_decl_plugin::pb_decl_plugin(): m_at_most_sym("at-most"), m_pble_sym("pble") {} -func_decl * card_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { SASSERT(m_manager); ast_manager& m = *m_manager; @@ -59,7 +59,7 @@ func_decl * card_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, } } -void card_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { +void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { if (logic == symbol::null) { op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K)); op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE)); @@ -67,12 +67,12 @@ 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) { +app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) { parameter param(k); return m.mk_app(m_fid, OP_AT_MOST_K, 1, ¶m, num_args, args, m.mk_bool_sort()); } -app * card_util::mk_le(unsigned num_args, int const * coeffs, expr * const * args, int k) { +app * pb_util::mk_le(unsigned num_args, int const * coeffs, expr * const * args, int k) { vector params; params.push_back(parameter(k)); for (unsigned i = 0; i < num_args; ++i) { @@ -82,11 +82,11 @@ app * card_util::mk_le(unsigned num_args, int const * coeffs, expr * const * arg } -bool card_util::is_at_most_k(app *a) const { +bool pb_util::is_at_most_k(app *a) const { return is_app_of(a, m_fid, OP_AT_MOST_K); } -bool card_util::is_at_most_k(app *a, unsigned& k) const { +bool pb_util::is_at_most_k(app *a, unsigned& k) const { if (is_at_most_k(a)) { k = get_k(a); return true; @@ -96,17 +96,17 @@ bool card_util::is_at_most_k(app *a, unsigned& k) const { } } -int card_util::get_k(app *a) const { +int pb_util::get_k(app *a) const { SASSERT(is_at_most_k(a) || is_le(a)); return a->get_decl()->get_parameter(0).get_int(); } -bool card_util::is_le(app *a) const { +bool pb_util::is_le(app *a) const { return is_app_of(a, m_fid, OP_PB_LE); } -bool card_util::is_le(app* a, int& k) const { +bool pb_util::is_le(app* a, int& k) const { if (is_le(a)) { k = get_k(a); return true; @@ -116,7 +116,7 @@ bool card_util::is_le(app* a, int& k) const { } } -int card_util::get_le_coeff(app* a, unsigned index) { +int pb_util::get_le_coeff(app* a, unsigned index) { if (is_at_most_k(a)) { return 1; } diff --git a/src/ast/card_decl_plugin.h b/src/ast/pb_decl_plugin.h similarity index 81% rename from src/ast/card_decl_plugin.h rename to src/ast/pb_decl_plugin.h index 3ac681284..093236218 100644 --- a/src/ast/card_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -3,11 +3,11 @@ Copyright (c) 2013 Microsoft Corporation Module Name: - card_decl_plugin.h + pb_decl_plugin.h Abstract: - Cardinality Constraints plugin + Pseudo-Boolean and Cardinality Constraints plugin Author: @@ -24,26 +24,26 @@ hence: --*/ -#ifndef _CARD_DECL_PLUGIN_H_ -#define _CARD_DECL_PLUGIN_H_ +#ifndef _PB_DECL_PLUGIN_H_ +#define _PB_DECL_PLUGIN_H_ #include"ast.h" -enum card_op_kind { +enum pb_op_kind { OP_AT_MOST_K, // at most K Booleans are true. OP_PB_LE, // pseudo-Boolean <= (generalizes at_most_k) - LAST_CARD_OP + LAST_PB_OP }; -class card_decl_plugin : public decl_plugin { +class pb_decl_plugin : public decl_plugin { symbol m_at_most_sym; symbol m_pble_sym; func_decl * mk_at_most(unsigned arity, unsigned k); func_decl * mk_le(unsigned arity, int const* coeffs, int k); public: - card_decl_plugin(); - virtual ~card_decl_plugin() {} + pb_decl_plugin(); + virtual ~pb_decl_plugin() {} virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { UNREACHABLE(); @@ -51,7 +51,7 @@ public: } virtual decl_plugin * mk_fresh() { - return alloc(card_decl_plugin); + return alloc(pb_decl_plugin); } // @@ -65,11 +65,11 @@ public: }; -class card_util { +class pb_util { ast_manager & m; family_id m_fid; public: - card_util(ast_manager& m):m(m), m_fid(m.mk_family_id("card")) {} + pb_util(ast_manager& m):m(m), m_fid(m.mk_family_id("pb")) {} ast_manager & get_manager() const { return m; } family_id get_family_id() const { return m_fid; } app * mk_at_most_k(unsigned num_args, expr * const * args, unsigned k); @@ -83,5 +83,5 @@ public: }; -#endif /* _CARD_DECL_PLUGIN_H_ */ +#endif /* _PB_DECL_PLUGIN_H_ */ diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index 541964038..6a996d288 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -25,7 +25,7 @@ Revision History: #include"dl_decl_plugin.h" #include"seq_decl_plugin.h" #include"float_decl_plugin.h" -#include"card_decl_plugin.h" +#include"pb_decl_plugin.h" void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("arith")))) { @@ -49,7 +49,7 @@ void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("float")))) { m.register_plugin(symbol("float"), alloc(float_decl_plugin)); } - if (!m.get_plugin(m.mk_family_id(symbol("card")))) { - m.register_plugin(symbol("card"), alloc(card_decl_plugin)); + if (!m.get_plugin(m.mk_family_id(symbol("pb")))) { + m.register_plugin(symbol("pb"), alloc(pb_decl_plugin)); } } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 626272412..976a66664 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -25,7 +25,7 @@ Notes: #include"datatype_decl_plugin.h" #include"seq_decl_plugin.h" #include"float_decl_plugin.h" -#include"card_decl_plugin.h" +#include"pb_decl_plugin.h" #include"ast_pp.h" #include"var_subst.h" #include"pp.h" @@ -573,7 +573,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype()); register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq()); register_plugin(symbol("float"), alloc(float_decl_plugin), logic_has_floats()); - register_plugin(symbol("card"), alloc(card_decl_plugin), !has_logic()); + register_plugin(symbol("pb"), alloc(pb_decl_plugin), !has_logic()); } else { // the manager was created by an external module, we must register all plugins available in the manager. diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp index b386595d3..b6da58aa0 100644 --- a/src/opt/core_maxsat.cpp +++ b/src/opt/core_maxsat.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "core_maxsat.h" -#include "card_decl_plugin.h" +#include "pb_decl_plugin.h" #include "ast_pp.h" namespace opt { @@ -120,10 +120,10 @@ namespace opt { } expr_ref core_maxsat::mk_at_most(expr_set const& set, unsigned k) { - card_util card(m); + pb_util pb(m); ptr_vector es; set2vector(set, es); - return expr_ref(card.mk_at_most_k(es.size(), es.c_ptr(), k), m); + return expr_ref(pb.mk_at_most_k(es.size(), es.c_ptr(), k), m); } expr* core_maxsat::get_not(expr* e) const { diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp index a2706bb4b..f0f156c99 100644 --- a/src/smt/theory_card.cpp +++ b/src/smt/theory_card.cpp @@ -53,7 +53,7 @@ Notes: namespace smt { theory_card::theory_card(ast_manager& m): - theory(m.mk_family_id("card")), + theory(m.mk_family_id("pb")), m_util(m) {} @@ -79,7 +79,7 @@ namespace smt { m_stats.m_num_predicates++; - TRACE("card", tout << "internalize: " << mk_pp(atom, m) << "\n";); + TRACE("pb", tout << "internalize: " << mk_pp(atom, m) << "\n";); SASSERT(!ctx.b_internalized(atom)); bool_var abv = ctx.mk_bool_var(atom); @@ -370,7 +370,7 @@ namespace smt { int max = c.m_current_max; int k = c.m_k; - TRACE("card", + TRACE("pb", tout << mk_pp(c.m_app, m) << " min: " << min << " max: " << max << "\n";); @@ -474,7 +474,7 @@ namespace smt { ast_manager& m = get_manager(); ptr_vector* cards = 0; card* c = 0; - TRACE("card", tout << "assign: " << mk_pp(ctx.bool_var2expr(v), m) << " <- " << is_true << "\n";); + TRACE("pb", tout << "assign: " << mk_pp(ctx.bool_var2expr(v), m) << " <- " << is_true << "\n";); if (m_watch.find(v, cards)) { for (unsigned i = 0; i < cards->size(); ++i) { @@ -618,7 +618,7 @@ namespace smt { add_clause(~l, a, c); add_clause(l, ~a, ~b); add_clause(l, a, ~c); - TRACE("card", tout << p << " ::= (if "; + TRACE("pb", tout << p << " ::= (if "; ctx.display_detailed_literal(tout, a); ctx.display_detailed_literal(tout << " ", b); ctx.display_detailed_literal(tout << " ", c); @@ -635,7 +635,7 @@ namespace smt { if (b != null_literal) lits.push_back(b); if (c != null_literal) lits.push_back(c); justification* js = 0; - TRACE("card", + TRACE("pb", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX, 0); } @@ -656,7 +656,7 @@ namespace smt { ++log; n *= 2; } - TRACE("card", tout << "threshold:" << (num_args*log) << "\n";); + TRACE("pb", tout << "threshold:" << (num_args*log) << "\n";); return num_args*log; } @@ -696,12 +696,12 @@ namespace smt { } sn(in, out); atmostk = ~se.internalize(c, out[k].get()); // k'th output is 0. - TRACE("card", tout << "~atmost: " << mk_pp(out[k].get(), m) << "\n";); + TRACE("pb", tout << "~atmost: " << mk_pp(out[k].get(), m) << "\n";); } literal thl = literal(c.m_bv); se.add_clause(~thl, atmostk); se.add_clause(thl, ~atmostk); - TRACE("card", tout << mk_pp(a, m) << "\n";); + TRACE("pb", tout << mk_pp(a, m) << "\n";); // auxiliary clauses get removed when popping scopes. // we have to recompile the circuit after back-tracking. ctx.push_trail(value_trail(c.m_compiled)); @@ -760,7 +760,7 @@ namespace smt { ++c.m_num_propagations; m_stats.m_num_axioms++; context& ctx = get_context(); - TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); + TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); justification* js = 0; ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(), diff --git a/src/smt/theory_card.h b/src/smt/theory_card.h index a432ea5a3..0f425c103 100644 --- a/src/smt/theory_card.h +++ b/src/smt/theory_card.h @@ -21,7 +21,7 @@ Notes: --*/ #include "smt_theory.h" -#include "card_decl_plugin.h" +#include "pb_decl_plugin.h" #include "smt_clause.h" namespace smt { @@ -69,7 +69,7 @@ namespace smt { unsigned_vector m_watch_trail; unsigned_vector m_watch_lim; literal_vector m_literals; - card_util m_util; + pb_util m_util; stats m_stats; void add_watch(bool_var bv, card* c); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index a52d4b93b..be83d446f 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -208,7 +208,7 @@ namespace smt { } theory_pb::theory_pb(ast_manager& m): - theory(m.mk_family_id("card")), + theory(m.mk_family_id("pb")), m_util(m), m_lemma(null_literal) {} @@ -263,7 +263,7 @@ namespace smt { // fall-through case l_true: ctx.mk_th_axiom(get_id(), 1, &lit); - TRACE("card", tout << mk_pp(atom, m) << " := " << lit << "\n";); + TRACE("pb", tout << mk_pp(atom, m) << " := " << lit << "\n";); dealloc(c); return true; case l_undef: @@ -293,7 +293,7 @@ namespace smt { } unsigned th = 10*args.size()*log; c->m_compilation_threshold = th; - TRACE("card", tout << "compilation threshold: " << th << "\n";); + TRACE("pb", tout << "compilation threshold: " << th << "\n";); } else { c->m_compilation_threshold = UINT_MAX; @@ -301,7 +301,7 @@ namespace smt { m_ineqs.insert(abv, c); m_ineqs_trail.push_back(abv); - TRACE("card", display(tout, *c);); + TRACE("pb", display(tout, *c);); return true; } @@ -431,7 +431,7 @@ namespace smt { } final_check_status theory_pb::final_check_eh() { - TRACE("card", display(tout);); + TRACE("pb", display(tout);); DEBUG_CODE(validate_final_check();); return FC_DONE; } @@ -459,7 +459,7 @@ namespace smt { break; } } - TRACE("card", display(tout << "validate: ", c); + TRACE("pb", display(tout << "validate: ", c); tout << "sum: " << sum << " " << maxsum << " " << ctx.get_assignment(c.lit()) << "\n"; ); @@ -472,7 +472,7 @@ namespace smt { void theory_pb::assign_eh(bool_var v, bool is_true) { context& ctx = get_context(); ptr_vector* ineqs = 0; - TRACE("card", tout << "assign: " << literal(v, !is_true) << "\n";); + TRACE("pb", tout << "assign: " << literal(v, !is_true) << "\n";); if (m_watch.find(v, ineqs)) { for (unsigned i = 0; i < ineqs->size(); ++i) { @@ -538,7 +538,7 @@ namespace smt { } } - TRACE("card", + TRACE("pb", tout << "assign: " << c.lit() << " <- " << is_true << "\n"; display(tout, c); ); @@ -636,7 +636,7 @@ namespace smt { // // else: the current set of watch remain a potentially feasible assignment. // - TRACE("card", + TRACE("pb", tout << "assign: " << literal(v) << " <- " << is_true << "\n"; display(tout, c); ); @@ -748,7 +748,7 @@ namespace smt { add_clause(~l, a, c); add_clause(l, ~a, ~b); add_clause(l, a, ~c); - TRACE("card", tout << mk_pp(t, m) << " ::= (if "; + TRACE("pb", tout << mk_pp(t, m) << " ::= (if "; ctx.display_detailed_literal(tout, a); ctx.display_detailed_literal(tout << " ", b); ctx.display_detailed_literal(tout << " ", c); @@ -765,7 +765,7 @@ namespace smt { if (b != null_literal) lits.push_back(b); if (c != null_literal) lits.push_back(c); justification* js = 0; - TRACE("card", + TRACE("pb", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX, 0); } @@ -815,12 +815,12 @@ namespace smt { } sn(in, out); literal at_least_k = se.internalize(c, out[k-1].get()); // first k outputs are 1. - TRACE("card", tout << "at_least: " << mk_pp(out[k-1].get(), m) << "\n";); + TRACE("pb", tout << "at_least: " << mk_pp(out[k-1].get(), m) << "\n";); literal thl = c.lit(); se.add_clause(~thl, at_least_k); se.add_clause(thl, ~at_least_k); - TRACE("card", tout << c.lit() << "\n";); + TRACE("pb", tout << c.lit() << "\n";); // auxiliary clauses get removed when popping scopes. // we have to recompile the circuit after back-tracking. c.m_compiled = l_false; @@ -938,7 +938,7 @@ namespace smt { inc_propagations(c); m_stats.m_num_propagations++; context& ctx = get_context(); - TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; + TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - "; for (unsigned i = 0; i < lits.size(); ++i) { tout << lits[i] << " "; } @@ -956,7 +956,7 @@ namespace smt { inc_propagations(c); m_stats.m_num_conflicts++; context& ctx = get_context(); - TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; + TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - "; for (unsigned i = 0; i < lits.size(); ++i) { tout << lits[i] << " "; } @@ -1110,7 +1110,7 @@ namespace smt { } - TRACE("card", display(tout, m_lemma);); + TRACE("pb", display(tout, m_lemma);); IF_VERBOSE(1, display(verbose_stream(), m_lemma);); } diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 2d23b97d6..b477e6bb7 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -21,7 +21,7 @@ Notes: --*/ #include "smt_theory.h" -#include "card_decl_plugin.h" +#include "pb_decl_plugin.h" #include "smt_clause.h" namespace smt { @@ -105,7 +105,7 @@ namespace smt { ptr_vector m_assign_ineqs_trail; unsigned_vector m_assign_ineqs_lim; literal_vector m_literals; // temporary vector - card_util m_util; + pb_util m_util; stats m_stats; ptr_vector m_to_compile; // inequalities to compile. diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 5130eea9d..ec2368ba8 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -22,7 +22,7 @@ Notes: #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"pb_decl_plugin.h" #include"arith_decl_plugin.h" class lia2card_tactic : public tactic { @@ -31,7 +31,7 @@ class lia2card_tactic : public tactic { typedef obj_hashtable expr_set; ast_manager & m; arith_util a; - card_util m_card; + pb_util m_pb; obj_map > m_uses; obj_map m_converted; expr_set m_01s; @@ -39,7 +39,7 @@ class lia2card_tactic : public tactic { imp(ast_manager & _m, params_ref const & p): m(_m), a(m), - m_card(m) { + m_pb(m) { } void set_cancel(bool f) { @@ -73,7 +73,7 @@ class lia2card_tactic : public tactic { 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";); + TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";); } } if (m_01s.empty()) { @@ -117,7 +117,7 @@ class lia2card_tactic : public tactic { } g->inc_depth(); result.push_back(g.get()); - TRACE("card", g->display(tout);); + TRACE("pb", g->display(tout);); SASSERT(g->is_well_sorted()); // TBD: convert models for 0-1 variables. @@ -181,13 +181,13 @@ class lia2card_tactic : public tactic { sub.insert(fml, mk_ge(y, n)); } else 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)); + sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k)); } else 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))); + sub.insert(fml, m.mk_not(m_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1))); } else { UNREACHABLE(); @@ -204,10 +204,10 @@ class lia2card_tactic : public tactic { 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)); + sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1)); } else 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))); + sub.insert(fml, m.mk_not(m_pb.mk_at_most_k(args.size(), args.c_ptr(), k))); } else { UNREACHABLE(); @@ -304,7 +304,7 @@ class lia2card_tactic : public tactic { } return true; } - TRACE("card", tout << "Use not validated: " << mk_pp(fml, m) << "\n";); + TRACE("pb", tout << "Use not validated: " << mk_pp(fml, m) << "\n";); return false; }