From 9467806a5caa2310a94c4c79ee666d7639c3887e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Nov 2013 09:39:28 -0800 Subject: [PATCH] debugging cardinality theory Signed-off-by: Nikolaj Bjorner --- src/ast/card_decl_plugin.cpp | 8 ++++---- src/ast/card_decl_plugin.h | 5 ----- src/ast/reg_decl_plugins.cpp | 4 ++++ src/cmd_context/cmd_context.cpp | 3 +++ src/smt/smt_setup.cpp | 6 ++++++ src/smt/smt_setup.h | 2 +- src/{opt => smt}/theory_card.cpp | 16 +++++++++++----- src/{opt => smt}/theory_card.h | 0 8 files changed, 29 insertions(+), 15 deletions(-) rename src/{opt => smt}/theory_card.cpp (94%) rename src/{opt => smt}/theory_card.h (100%) diff --git a/src/ast/card_decl_plugin.cpp b/src/ast/card_decl_plugin.cpp index bbf4b28bd..20c9af09f 100644 --- a/src/ast/card_decl_plugin.cpp +++ b/src/ast/card_decl_plugin.cpp @@ -20,7 +20,7 @@ Revision History: #include "card_decl_plugin.h" card_decl_plugin::card_decl_plugin(): - m_at_most_sym("at_most") + m_at_most_sym("at-most") {} func_decl * card_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -29,11 +29,11 @@ func_decl * card_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, ast_manager& m = *m_manager; for (unsigned i = 0; i < arity; ++i) { if (!m.is_bool(domain[i])) { - m.raise_exception("invalid non-Boolean sort applied to 'at_most_k'"); + m.raise_exception("invalid non-Boolean sort applied to 'at-most'"); } } if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) { - m.raise_exception("function 'at_most_k' expects one non-negative integer parameter"); + m.raise_exception("function 'at-most' expects one non-negative integer parameter"); } func_decl_info info(m_family_id, OP_AT_MOST_K, 1, parameters); return m.mk_func_decl(m_at_most_sym, arity, domain, m.mk_bool_sort(), info); @@ -41,7 +41,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) { if (logic == symbol::null) { - op_names.push_back(builtin_name("at-most-k", OP_AT_MOST_K)); + op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K)); } } diff --git a/src/ast/card_decl_plugin.h b/src/ast/card_decl_plugin.h index 9d4e95b13..3529a1a04 100644 --- a/src/ast/card_decl_plugin.h +++ b/src/ast/card_decl_plugin.h @@ -28,8 +28,6 @@ hence: #define _CARD_DECL_PLUGIN_H_ #include"ast.h" - - enum card_op_kind { OP_AT_MOST_K, @@ -60,9 +58,6 @@ public: virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); virtual void get_op_names(svector & op_names, symbol const & logic); - virtual void get_sort_names(svector & sort_names, symbol const & logic); - virtual expr * get_some_value(sort * s); - virtual bool is_fully_interp(sort const * s) const; }; diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index ab1844e07..541964038 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -25,6 +25,7 @@ Revision History: #include"dl_decl_plugin.h" #include"seq_decl_plugin.h" #include"float_decl_plugin.h" +#include"card_decl_plugin.h" void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("arith")))) { @@ -48,4 +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)); + } } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 01536d78e..626272412 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -25,6 +25,7 @@ Notes: #include"datatype_decl_plugin.h" #include"seq_decl_plugin.h" #include"float_decl_plugin.h" +#include"card_decl_plugin.h" #include"ast_pp.h" #include"var_subst.h" #include"pp.h" @@ -529,6 +530,7 @@ bool cmd_context::logic_has_floats() const { return !has_logic() || m_logic == "QF_FPA" || m_logic == "QF_FPABV"; } + bool cmd_context::logic_has_array_core(symbol const & s) const { return s == "QF_AX" || @@ -571,6 +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()); } else { // the manager was created by an external module, we must register all plugins available in the manager. diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 52ad14155..90694b29a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -31,6 +31,7 @@ Revision History: #include"theory_dummy.h" #include"theory_dl.h" #include"theory_seq_empty.h" +#include"theory_card.h" namespace smt { @@ -790,6 +791,10 @@ namespace smt { m_context.register_plugin(alloc(theory_seq_empty, m_manager)); } + void setup::setup_card() { + m_context.register_plugin(alloc(theory_card, m_manager)); + } + void setup::setup_unknown() { setup_arith(); setup_arrays(); @@ -797,6 +802,7 @@ namespace smt { setup_datatypes(); setup_dl(); setup_seq(); + setup_card(); } void setup::setup_unknown(static_features & st) { diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index e0188537e..91b48dbe3 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -92,7 +92,7 @@ namespace smt { void setup_arith(); void setup_dl(); void setup_seq(); - void setup_instgen(); + void setup_card(); void setup_i_arith(); void setup_mi_arith(); public: diff --git a/src/opt/theory_card.cpp b/src/smt/theory_card.cpp similarity index 94% rename from src/opt/theory_card.cpp rename to src/smt/theory_card.cpp index f303306b3..13b9e93c3 100644 --- a/src/opt/theory_card.cpp +++ b/src/smt/theory_card.cpp @@ -67,7 +67,12 @@ namespace smt { else { bv = ctx.get_bool_var(arg); } - ctx.set_var_theory(bv, get_id()); + if (null_theory_var == ctx.get_var_theory(bv)) { + ctx.set_var_theory(bv, get_id()); + } + else { + SASSERT(ctx.get_var_theory(bv) == get_id()); // TBD, fishy + } add_watch(bv, c); } return true; @@ -122,11 +127,11 @@ namespace smt { case l_true: case l_undef: { literal_vector& lits = get_lits(); - lits.push_back(literal(v)); - for (unsigned i = 0; i < atm->get_num_args() && lits.size() <= k + 1; ++i) { + lits.push_back(~literal(c->m_bv)); + for (unsigned i = 0; i < atm->get_num_args() && lits.size() < k + 1; ++i) { expr* arg = atm->get_arg(i); if (ctx.get_assignment(arg) == l_true) { - lits.push_back(literal(ctx.get_bool_var(arg))); + lits.push_back(~literal(ctx.get_bool_var(arg))); } } SASSERT(lits.size() == k + 1); @@ -143,7 +148,7 @@ namespace smt { case l_false: case l_undef: { literal_vector& lits = get_lits(); - lits.push_back(~literal(v)); + lits.push_back(~literal(c->m_bv)); for (unsigned i = 0; i < atm->get_num_args(); ++i) { expr* arg = atm->get_arg(i); if (ctx.get_assignment(arg) == l_false) { @@ -266,6 +271,7 @@ namespace smt { void theory_card::add_clause(literal_vector const& lits) { context& ctx = get_context(); + TRACE("card", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } diff --git a/src/opt/theory_card.h b/src/smt/theory_card.h similarity index 100% rename from src/opt/theory_card.h rename to src/smt/theory_card.h