From 839e3fbb7cfe34d388aba4966bad2c5853f9f24d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 May 2015 19:40:34 -0700 Subject: [PATCH] add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 2 +- scripts/mk_project.py | 3 +- src/muz/ddnf/ddnf.cpp | 86 ++- src/muz/ddnf/ddnf.h | 25 + src/muz/rel/tbv.cpp | 14 + src/muz/rel/tbv.h | 1 + src/smt/tactic/smt_tactic.cpp | 9 +- src/tactic/arith/probe_arith.cpp | 63 ++ src/tactic/arith/probe_arith.h | 2 + src/tactic/nlsat_smt/nl_purify_tactic.cpp | 667 ++++++++++++++++++ src/tactic/nlsat_smt/nl_purify_tactic.h | 35 + src/tactic/portfolio/default_tactic.cpp | 4 +- src/tactic/portfolio/smt_strategic_solver.cpp | 3 + src/tactic/smtlogics/qfufnra_tactic.cpp | 46 ++ src/tactic/smtlogics/qfufnra_tactic.h | 31 + src/tactic/tactic.cpp | 2 +- src/tactic/tactical.cpp | 4 + src/tactic/tactical.h | 1 + src/test/ddnf.cpp | 167 +++++ src/test/main.cpp | 1 + 20 files changed, 1158 insertions(+), 8 deletions(-) create mode 100644 src/tactic/nlsat_smt/nl_purify_tactic.cpp create mode 100644 src/tactic/nlsat_smt/nl_purify_tactic.h create mode 100644 src/tactic/smtlogics/qfufnra_tactic.cpp create mode 100644 src/tactic/smtlogics/qfufnra_tactic.h create mode 100644 src/test/ddnf.cpp diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 00d03a8b0..2a90b5a3f 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -2083,7 +2083,7 @@ bool parse_is_sat_line(char const* line, bool& is_sat) { return true; } return false; -} + bool parse_is_sat(char const* filename, bool& is_sat) { std::ifstream is(filename); diff --git a/scripts/mk_project.py b/scripts/mk_project.py index f0c1f8e2f..01d5cfa97 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -69,7 +69,8 @@ def init_project_def(): add_lib('ddnf', ['muz', 'transforms', 'rel'], 'muz/ddnf') add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality') add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp') - add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics') + add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt') + add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index 6c4f79f7c..82cb9d1fa 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -123,6 +123,13 @@ namespace datalog { class ddnf_mgr { + struct stats { + unsigned m_num_inserts; + unsigned m_num_comparisons; + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + unsigned m_num_bits; ddnf_node* m_root; ddnf_node_vector m_noderefs; @@ -131,6 +138,8 @@ namespace datalog { ddnf_node::hash m_hash; ddnf_node::eq m_eq; ddnf_nodes m_nodes; + svector m_marked; + stats m_stats; public: ddnf_mgr(unsigned n): m_num_bits(n), m_noderefs(*this), m_internalized(false), m_tbv(n), m_hash(m_tbv), m_eq(m_tbv), @@ -154,6 +163,31 @@ namespace datalog { n->dec_ref(); } + void reset_accumulate() { + m_marked.resize(m_nodes.size()); + for (unsigned i = 0; i < m_marked.size(); ++i) { + m_marked[i] = false; + } + } + + void accumulate(tbv const& t, unsigned_vector& acc) { + ddnf_node* n = find(t); + ptr_vector todo; + todo.push_back(n); + while (!todo.empty()) { + n = todo.back(); + todo.pop_back(); + unsigned id = n->get_id(); + if (m_marked[id]) continue; + acc.push_back(id); + m_marked[id] = true; + unsigned sz = n->num_children(); + for (unsigned i = 0; i < sz; ++i) { + todo.push_back((*n)[i]); + } + } + } + ddnf_node* insert(tbv const& t) { SASSERT(!m_internalized); ptr_vector new_tbvs; @@ -173,6 +207,9 @@ namespace datalog { return m_tbv.allocate(v, hi, lo); } + tbv_manager& get_tbv_manager() { + return m_tbv; + } unsigned size() const { return m_noderefs.size(); @@ -183,13 +220,21 @@ namespace datalog { return find(t)->descendants(); } - void display(std::ostream& out) const { + void display_statistics(std::ostream& out) const { + std::cout << "Number of insertions: " << m_stats.m_num_inserts << "\n"; + std::cout << "Number of comparisons: " << m_stats.m_num_comparisons << "\n"; + std::cout << "Number of nodes: " << size() << "\n"; + } + + void display(std::ostream& out) const { for (unsigned i = 0; i < m_noderefs.size(); ++i) { m_noderefs[i]->display(out); out << "\n"; } } + + private: ddnf_node* find(tbv const& t) { @@ -207,9 +252,11 @@ namespace datalog { SASSERT(m_tbv.contains(root.get_tbv(), new_tbv)); if (&root == new_n) return; + ++m_stats.m_num_inserts; bool inserted = false; for (unsigned i = 0; i < root.num_children(); ++i) { ddnf_node& child = *(root[i]); + ++m_stats.m_num_comparisons; if (m_tbv.contains(child.get_tbv(), new_tbv)) { inserted = true; insert(child, new_n, new_intersections); @@ -227,11 +274,16 @@ namespace datalog { // checking for subset if (m_tbv.contains(new_tbv, child.get_tbv())) { subset_children.push_back(&child); + ++m_stats.m_num_comparisons; } else if (m_tbv.intersect(child.get_tbv(), new_tbv, *intr)) { // this means there is a non-full intersection new_intersections.push_back(intr); intr = m_tbv.allocate(); + m_stats.m_num_comparisons += 2; + } + else { + m_stats.m_num_comparisons += 2; } } m_tbv.deallocate(intr); @@ -284,10 +336,38 @@ namespace datalog { for (; it != end; ++it) { dst.insert(*it); } - } - + } }; + ddnf_core::ddnf_core(unsigned n) { + m_imp = alloc(ddnf_mgr, n); + } + ddnf_core::~ddnf_core() { + dealloc(m_imp); + } + ddnf_node* ddnf_core::insert(tbv const& t) { + return m_imp->insert(t); + } + tbv_manager& ddnf_core::get_tbv_manager() { + return m_imp->get_tbv_manager(); + } + unsigned ddnf_core::size() const { + return m_imp->size(); + } + void ddnf_core::reset_accumulate() { + return m_imp->reset_accumulate(); + } + void ddnf_core::accumulate(tbv const& t, unsigned_vector& acc) { + return m_imp->accumulate(t, acc); + } + void ddnf_core::display(std::ostream& out) const { + m_imp->display(out); + } + void ddnf_core::display_statistics(std::ostream& out) const { + m_imp->display_statistics(out); + } + + void ddnf_node::add_child(ddnf_node* n) { //SASSERT(!m_tbv.is_subset(n->m_tbv)); m_children.push_back(n); diff --git a/src/muz/ddnf/ddnf.h b/src/muz/ddnf/ddnf.h index 8121dc090..1e5e912ba 100644 --- a/src/muz/ddnf/ddnf.h +++ b/src/muz/ddnf/ddnf.h @@ -24,6 +24,9 @@ Revision History: #include "statistics.h" #include "dl_engine_base.h" +class tbv; +class tbv_manager; + namespace datalog { class context; @@ -41,6 +44,28 @@ namespace datalog { virtual void display_certificate(std::ostream& out) const; virtual expr_ref get_answer(); }; + + class ddnf_node; + class ddnf_mgr; + class ddnf_core { + ddnf_mgr* m_imp; + public: + ddnf_core(unsigned n); + ~ddnf_core(); + ddnf_node* insert(tbv const& t); + tbv_manager& get_tbv_manager(); + unsigned size() const; + + // + // accumulate labels covered by the stream of tbvs, + // such that labels that are covered by the current + // tbv but not the previous tbvs are included. + // + void reset_accumulate(); + void accumulate(tbv const& t, unsigned_vector& labels); + void display(std::ostream& out) const; + void display_statistics(std::ostream& out) const; + }; }; #endif diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index fc3c32390..577817e69 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -99,6 +99,20 @@ tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) { } return r; } +tbv* tbv_manager::allocate(char const* bv) { + tbv* result = allocateX(); + unsigned i = 0, sz = num_tbits(); + while(*bv && i < sz) { + if (*bv == '0') set(*result, i++, tbit::BIT_0); + else if (*bv == '1') set(*result, i++, tbit::BIT_1); + else if (*bv == '*') i++; + else if (i == 0 && (*bv == ' ' || *bv == '\t')) ; + else break; + ++bv; + } + return result; +} + tbv* tbv_manager::project(bit_vector const& to_delete, tbv const& src) { tbv* r = allocate(); unsigned i, j; diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h index ad98b8095..7d20d035c 100644 --- a/src/muz/rel/tbv.h +++ b/src/muz/rel/tbv.h @@ -55,6 +55,7 @@ public: tbv* allocate(rational const& r); tbv* allocate(uint64 n, unsigned hi, unsigned lo); tbv* allocate(tbv const& bv, unsigned const* permutation); + tbv* allocate(char const* bv); void deallocate(tbv* bv); diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 95b150a8c..a83b4a035 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -22,6 +22,7 @@ Notes: #include"smt_params.h" #include"smt_params_helper.hpp" #include"rewriter_types.h" +#include"filter_model_converter.h" class smt_tactic : public tactic { smt_params m_params; @@ -150,6 +151,7 @@ public: scoped_ptr dep2bool; scoped_ptr bool2dep; ptr_vector assumptions; + ref fmc; if (in->unsat_core_enabled()) { if (in->proofs_enabled()) throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores"); @@ -191,6 +193,10 @@ public: dep2bool->insert(d, b); bool2dep->insert(b, d); assumptions.push_back(b); + if (!fmc) { + fmc = alloc(filter_model_converter, m); + } + fmc->insert(to_app(b)->get_decl()); } clause.push_back(m.mk_not(b)); } @@ -229,11 +235,12 @@ public: // the empty assertion set is trivially satifiable. in->reset(); result.push_back(in.get()); - // store the model in a do nothin model converter. + // store the model in a no-op model converter, and filter fresh Booleans if (in->models_enabled()) { model_ref md; m_ctx->get_model(md); mc = model2model_converter(md.get()); + mc = concat(fmc.get(), mc.get()); } pc = 0; core = 0; diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp index 770281923..ae287e2b5 100644 --- a/src/tactic/arith/probe_arith.cpp +++ b/src/tactic/arith/probe_arith.cpp @@ -513,6 +513,53 @@ static bool is_lira(goal const & g) { return !test(g, p); } + +struct is_non_qfufnra_functor { + struct found {}; + ast_manager & m; + arith_util u; + + is_non_qfufnra_functor(ast_manager & _m): m(_m), u(m) {} + + void throw_found() { + throw found(); + } + + void operator()(var * x) { + throw_found(); + } + void operator()(quantifier *) { + throw_found(); + } + void operator()(app * n) { + family_id fid = n->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == u.get_family_id()) { + switch (n->get_decl_kind()) { + case OP_LE: case OP_GE: case OP_LT: case OP_GT: + case OP_ADD: case OP_UMINUS: case OP_SUB: case OP_ABS: + case OP_NUM: case OP_MUL: + case OP_IRRATIONAL_ALGEBRAIC_NUM: + return; + case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD: + case OP_POWER: + if (!u.is_numeral(n->get_arg(1))) + throw_found(); + return; + case OP_IS_INT: + case OP_TO_INT: + case OP_TO_REAL: + throw_found(); + return; + default: + throw_found(); + } + } + } +}; + + class is_qfnia_probe : public probe { public: virtual result operator()(goal const & g) { @@ -569,6 +616,18 @@ public: } }; +static bool is_qfufnra(goal const& g) { + is_non_qfufnra_functor p(g.m()); + return !test(g, p); +} + +class is_qfufnra_probe : public probe { +public: + virtual result operator()(goal const & g) { + return is_qfufnra(g); + } +}; + probe * mk_is_qfnia_probe() { return alloc(is_qfnia_probe); } @@ -600,3 +659,7 @@ probe * mk_is_lra_probe() { probe * mk_is_lira_probe() { return alloc(is_lira_probe); } + +probe* mk_is_qfufnra_probe() { + return alloc(is_qfufnra_probe); +} diff --git a/src/tactic/arith/probe_arith.h b/src/tactic/arith/probe_arith.h index 83179098d..ba95a2837 100644 --- a/src/tactic/arith/probe_arith.h +++ b/src/tactic/arith/probe_arith.h @@ -55,6 +55,7 @@ probe * mk_is_nira_probe(); probe * mk_is_lia_probe(); probe * mk_is_lra_probe(); probe * mk_is_lira_probe(); +probe * mk_is_qfufnra_probe(); /* ADD_PROBE("is-qfnia", "true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).", "mk_is_qfnia_probe()") @@ -65,5 +66,6 @@ probe * mk_is_lira_probe(); ADD_PROBE("is-lia", "true if the goal is in LIA (linear integer arithmetic, formula may have quantifiers).", "mk_is_lia_probe()") ADD_PROBE("is-lra", "true if the goal is in LRA (linear real arithmetic, formula may have quantifiers).", "mk_is_lra_probe()") ADD_PROBE("is-lira", "true if the goal is in LIRA (linear integer and real arithmetic, formula may have quantifiers).", "mk_is_lira_probe()") + ADD_PROBE("is-qfufnra", "true if the goal is QF_UFNRA (quantifier-free nonlinear real arithmetic with other theories).", mk_is_qfufnra_probe()"); */ #endif diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp new file mode 100644 index 000000000..ec3419d2b --- /dev/null +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -0,0 +1,667 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + nl_purify_tactic.cpp + +Abstract: + + Tactic for purifying quantifier-free formulas that mix QF_NRA and other theories. + It is designed to allow cooprating between the nlsat solver and other theories + in a decoupled way. + + Let goal be formula F. + Let NL goal be formula G. + Assume F is in NNF. + Assume F does not contain mix of real/integers. + Assume F is quantifier-free (please, otherwise we need to reprocess from instantiated satisfiable formula) + + For each atomic nl formula f, + - introduce a propositional variable p + - replace f by p + - add clauses p => f to G + + For each interface term t, + - introduce interface variable v (or use t if it is already a variable) + - replace t by v + + Check satisfiability of G. + If satisfiable, then check assignment to p and interface equalities on F + If unsat: + Retrieve core and add core to G. + else: + For interface equalities from model of F that are not equal in G, add + For interface variables that are equal under one model, but not the other model, + create interface predicate p_vw => v = w, add to both F, G. + Add interface equations to assumptions, recheck F. + If unsat retrieve core add to G. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-5. + +Revision History: + +- check for input assumptions +- check for proof mode +- check for quantifiers +- add applicability filter +- add to smtlogics + +--*/ +#include "tactical.h" +#include "nl_purify_tactic.h" +#include "smt_tactic.h" +#include "rewriter.h" +#include "nlsat_tactic.h" +#include "filter_model_converter.h" +#include "obj_pair_hashtable.h" +#include "rewriter_def.h" +#include "ast_pp.h" +#include "trace.h" +#include "smt_solver.h" +#include "solver.h" + +class nl_purify_tactic : public tactic { + + enum polarity_t { + pol_pos, + pol_neg, + pol_dual + }; + + ast_manager & m; + arith_util m_util; + params_ref m_params; + bool m_produce_proofs; + ref m_fmc; + bool m_cancel; + tactic_ref m_nl_tac; // nlsat tactic + ref m_solver; // SMT solver + expr_ref_vector m_eq_preds; // predicates for equality between pairs of interface variables + svector m_eq_values; // truth value of the equality predicates in nlsat + app_ref_vector m_new_reals; // interface real variables + app_ref_vector m_new_preds; // abstraction predicates for smt_solver (hide real constraints) + expr_ref_vector m_asms; // assumptions to pass to SMT solver + obj_pair_map m_eq_pairs; // map pairs of interface variables to auxiliary predicates + obj_map m_interface_cache; // map of compound real expression to interface variable. + obj_map m_polarities; // polarities of sub-expressions + +public: + struct rw_cfg : public default_rewriter_cfg { + enum mode_t { + mode_interface_var, + mode_bool_preds + }; + ast_manager& m; + nl_purify_tactic & m_owner; + app_ref_vector& m_new_reals; + app_ref_vector& m_new_preds; + obj_map& m_polarities; + obj_map& m_interface_cache; + expr_ref_vector m_nl_cnstrs; + proof_ref_vector m_nl_cnstr_prs; + expr_ref_vector m_args; + mode_t m_mode; + + rw_cfg(nl_purify_tactic & o): + m(o.m), + m_owner(o), + m_new_reals(o.m_new_reals), + m_new_preds(o.m_new_preds), + m_polarities(o.m_polarities), + m_interface_cache(o.m_interface_cache), + m_nl_cnstrs(m), + m_nl_cnstr_prs(m), + m_args(m), + m_mode(mode_interface_var) { + } + + virtual ~rw_cfg() {} + + arith_util & u() { return m_owner.m_util; } + + bool produce_proofs() const { return m_owner.m_produce_proofs; } + + expr * mk_interface_var(expr* arg) { + expr* r; + if (m_interface_cache.find(arg, r)) { + return r; + } + if (is_uninterp_const(arg)) { + m_interface_cache.insert(arg, arg); + return arg; + } + r = m.mk_fresh_const(0, u().mk_real()); + m_new_reals.push_back(to_app(r)); + m_interface_cache.insert(arg, r); + return r; + } + + void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result) { + expr_ref old_pred(m.mk_app(f, num, args), m); + polarity_t pol; + TRACE("nlsat_smt", tout << old_pred << "\n";); + VERIFY(m_polarities.find(old_pred, pol)); + result = m.mk_fresh_const(0, m.mk_bool_sort()); + m_polarities.insert(result, pol); + m_new_preds.push_back(to_app(result)); + if (pol != pol_neg) { + m_nl_cnstrs.push_back(m.mk_or(m.mk_not(result), m.mk_app(f, num, args))); + } + if (pol != pol_pos) { + m_nl_cnstrs.push_back(m.mk_or(result, m.mk_not(m.mk_app(f, num, args)))); + } + TRACE("nlsat_smt", tout << result << " : " << mk_pp(m_nl_cnstrs.back(), m) << "\n";); + } + + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + throw tactic_exception("quantifiers are not supported in mixed-mode nlsat engine"); + } + + br_status reduce_app_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { + if (f->get_family_id() == m.get_basic_family_id()) { + // TBD: do we have negated inequalities for strict? + // maybe equalities are already deleted by pre-processor stage, but why depend on this? + if (f->get_decl_kind() == OP_EQ && u().is_real(args[0])) { + mk_interface_bool(f, num, args, result); + return BR_DONE; + } + else { + return BR_FAILED; + } + } + if (f->get_family_id() == u().get_family_id()) { + switch (f->get_decl_kind()) { + case OP_LE: + case OP_GE: + case OP_LT: + case OP_GT: + // these are the only real cases of non-linear atomic formulas besides equality. + mk_interface_bool(f, num, args, result); + return BR_DONE; + default: + return BR_FAILED; + } + } + return BR_FAILED; + } + + br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { + m_args.reset(); + bool has_interface = false; + for (unsigned i = 0; i < num; ++i) { + expr* arg = args[i]; + if (u().is_real(arg)) { + has_interface = true; + m_args.push_back(mk_interface_var(arg)); + } + else { + m_args.push_back(arg); + } + } + if (has_interface) { + result = m.mk_app(f, num, m_args.c_ptr()); + TRACE("nlsat_smt", tout << result << "\n";); + return BR_DONE; + } + else { + return BR_FAILED; + } + } + + br_status reduce_app(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { + if (m_mode == mode_bool_preds) { + return reduce_app_bool(f, num, args, result, pr); + } + else { + return reduce_app_real(f, num, args, result, pr); + } + } + }; +private: + class rw : public rewriter_tpl { + rw_cfg m_cfg; + public: + rw(nl_purify_tactic & o): + rewriter_tpl(o.m, o.m_produce_proofs, m_cfg), + m_cfg(o) { + } + expr_ref_vector const& nl_cnstrs() const { + return m_cfg.m_nl_cnstrs; + } + void set_bool_mode() { + m_cfg.m_mode = rw_cfg::mode_bool_preds; + } + void set_interface_var_mode() { + m_cfg.m_mode = rw_cfg::mode_interface_var; + } + + }; + + arith_util & u() { return m_util; } + + void check_point() { + if (m_cancel) { + throw tactic_exception("canceled"); + } + } + + void display_result(std::ostream& out, goal_ref_buffer const& result) { + for (unsigned i = 0; i < result.size(); ++i) { + result[i]->display(tout << "goal\n"); + } + } + + void update_eq_values(model_ref& mdl) { + expr_ref tmp(m); + for (unsigned i = 0; i < m_eq_preds.size(); ++i) { + expr* pred = m_eq_preds[i].get(); + m_eq_values[i] = l_undef; + if (mdl->eval(pred, tmp)) { + if (m.is_true(tmp)) { + m_eq_values[i] = l_true; + } + else if (m.is_false(tmp)) { + m_eq_values[i] = l_false; + } + } + } + } + + void solve(goal_ref const& nl_g, + goal_ref_buffer& result, + model_converter_ref& mc) { + + while (true) { + check_point(); + TRACE("nlsat_smt", m_solver->display(tout << "SMT:\n"); nl_g->display(tout << "\nNL:\n"); ); + goal_ref tmp_nl = alloc(goal, m, true, false); + model_converter_ref nl_mc; + proof_converter_ref nl_pc; + expr_dependency_ref nl_core(m); + result.reset(); + tmp_nl->copy_from(*nl_g.get()); + (*m_nl_tac)(tmp_nl, result, nl_mc, nl_pc, nl_core); + + if (is_decided_unsat(result)) { + TRACE("nlsat_smt", tout << "unsat\n";); + break; + } + if (!is_decided_sat(result)) { + TRACE("nlsat_smt", tout << "not a unit\n";); + break; + } + // extract evaluation on interface variables. + // assert booleans that evaluate to true. + // assert equalities between equal interface real variables. + + model_ref mdl_nl, mdl_smt; + model_converter2model(m, nl_mc.get(), mdl_nl); + update_eq_values(mdl_nl); + enforce_equalities(mdl_nl, nl_g); + + setup_assumptions(mdl_nl); + + TRACE("nlsat_smt", m_solver->display(tout << "smt goal:\n"); ); + + result.reset(); + lbool r = m_solver->check_sat(m_asms.size(), m_asms.c_ptr()); + if (r == l_false) { + // extract the core from the result + ptr_vector core; + m_solver->get_unsat_core(core); + if (core.empty()) { + goal_ref g = alloc(goal, m); + g->assert_expr(m.mk_false()); + result.push_back(g.get()); + break; + } + expr_ref_vector clause(m); + expr_ref fml(m); + expr* e; + for (unsigned i = 0; i < core.size(); ++i) { + clause.push_back(m.is_not(core[i], e)?e:m.mk_not(core[i])); + } + fml = m.mk_or(clause.size(), clause.c_ptr()); + nl_g->assert_expr(fml); + continue; + } + else if (r == l_true) { + m_solver->get_model(mdl_smt); + if (enforce_equalities(mdl_smt, nl_g)) { + // SMT enforced a new equality that wasn't true for nlsat. + continue; + } + TRACE("nlsat_smt", + m_fmc->display(tout << "joint state is sat\n"); + nl_mc->display(tout << "nl\n");); + merge_models(*mdl_nl.get(), mdl_smt); + mc = m_fmc.get(); + apply(mc, mdl_smt, 0); + mc = model2model_converter(mdl_smt.get()); + result.push_back(alloc(goal, m)); + } + else { + TRACE("nlsat_smt", tout << "unknown\n";); + } + break; + } + TRACE("nlsat_smt", display_result(tout, result);); + } + + void setup_assumptions(model_ref& mdl) { + m_asms.reset(); + app_ref_vector const& fresh_preds = m_new_preds; + expr_ref tmp(m); + for (unsigned i = 0; i < fresh_preds.size(); ++i) { + expr* pred = fresh_preds[i]; + if (mdl->eval(pred, tmp)) { + TRACE("nlsat_smt", tout << "pred: " << mk_pp(pred, m) << "\n";); + polarity_t pol = m_polarities.find(pred); + if (pol != pol_neg && m.is_true(tmp)) { + m_asms.push_back(pred); + } + else if (pol != pol_pos && m.is_false(tmp)) { + m_asms.push_back(m.mk_not(pred)); + } + } + } + for (unsigned i = 0; i < m_eq_preds.size(); ++i) { + expr* pred = m_eq_preds[i].get(); + switch(m_eq_values[i]) { + case l_true: + m_asms.push_back(pred); + break; + case l_false: + m_asms.push_back(m.mk_not(pred)); + break; + default: + break; + } + } + } + + bool enforce_equalities(model_ref& mdl, goal_ref const& nl_g) { + TRACE("nlsat_smt", tout << "Enforce equalities " << m_interface_cache.size() << "\n";); + bool new_equality = false; + expr_ref_vector nums(m); + obj_map num2var; + obj_map::iterator it = m_interface_cache.begin(), end = m_interface_cache.end(); + for (; it != end; ++it) { + expr_ref r(m); + expr* v, *w, *pred; + w = it->m_value; + VERIFY(mdl->eval(w, r)); + TRACE("nlsat_smt", tout << mk_pp(w, m) << " |-> " << r << "\n";); + nums.push_back(r); + if (num2var.find(r, v)) { + if (!m_eq_pairs.find(v, w, pred)) { + pred = m.mk_fresh_const(0, m.mk_bool_sort()); + m_eq_preds.push_back(pred); + m_eq_values.push_back(l_true); + m_fmc->insert(to_app(pred)->get_decl()); + nl_g->assert_expr(m.mk_or(m.mk_not(pred), m.mk_eq(w, v))); + nl_g->assert_expr(m.mk_or(pred, m.mk_not(m.mk_eq(w, v)))); + m_solver->assert_expr(m.mk_iff(pred, m.mk_eq(w, v))); + new_equality = true; + m_eq_pairs.insert(v, w, pred); + } + else { + // interface equality is already enforced. + } + } + else { + num2var.insert(r, w); + } + } + return new_equality; + } + + void merge_models(model const& mdl_nl, model_ref& mdl_smt) { + obj_map num2num; + expr_ref result(m), val2(m); + expr_ref_vector args(m), trail(m); + unsigned sz = mdl_nl.get_num_constants(); + for (unsigned i = 0; i < sz; ++i) { + func_decl* v = mdl_nl.get_constant(i); + if (u().is_real(v->get_range())) { + expr* val = mdl_nl.get_const_interp(v); + if (mdl_smt->eval(v, val2)) { + if (val != val2) { + num2num.insert(val2, val); + trail.push_back(val2); + } + } + } + } + sz = mdl_smt->get_num_functions(); + for (unsigned i = 0; i < sz; ++i) { + func_decl* f = mdl_smt->get_function(i); + if (has_real(f)) { + unsigned arity = f->get_arity(); + func_interp* f1 = mdl_smt->get_func_interp(f); + func_interp* f2 = alloc(func_interp, m, f->get_arity()); + for (unsigned j = 0; j < f1->num_entries(); ++j) { + args.reset(); + func_entry const* entry = f1->get_entry(j); + for (unsigned k = 0; k < arity; ++k) { + args.push_back(translate(num2num, entry->get_arg(k))); + } + result = translate(num2num, entry->get_result()); + f2->insert_entry(args.c_ptr(), result); + } + expr* e = f1->get_else(); + result = translate(num2num, e); + f2->set_else(result); + mdl_smt->register_decl(f, f2); + } + } + mdl_smt->copy_const_interps(mdl_nl); + } + + bool has_real(func_decl* f) { + for (unsigned i = 0; i < f->get_arity(); ++i) { + if (u().is_real(f->get_domain(i))) return true; + } + return u().is_real(f->get_range()); + } + + expr* translate(obj_map const& num2num, expr* e) { + if (!e || !u().is_real(e)) return e; + expr* result = 0; + if (num2num.find(e, result)) return result; + return e; + } + + void get_polarities(goal const& g) { + ptr_vector forms; + svector pols; + unsigned sz = g.size(); + for (unsigned i = 0; i < sz; ++i) { + forms.push_back(g.form(i)); + pols.push_back(pol_pos); + } + polarity_t p, q; + while (!forms.empty()) { + expr* e = forms.back(); + p = pols.back(); + forms.pop_back(); + pols.pop_back(); + if (m_polarities.find(e, q)) { + if (p == q || q == pol_dual) continue; + p = pol_dual; + } + TRACE("nlsat_smt", tout << mk_pp(e, m) << "\n";); + m_polarities.insert(e, p); + if (is_quantifier(e) || is_var(e)) { + throw tactic_exception("nl-purify tactic does not support quantifiers"); + } + SASSERT(is_app(e)); + app* a = to_app(e); + func_decl* f = a->get_decl(); + if (f->get_family_id() == m.get_basic_family_id() && p != pol_dual) { + switch(f->get_decl_kind()) { + case OP_NOT: + p = neg(p); + break; + case OP_AND: + case OP_OR: + break; + default: + p = pol_dual; + break; + } + } + else { + p = pol_dual; + } + for (unsigned i = 0; i < a->get_num_args(); ++i) { + forms.push_back(a->get_arg(i)); + pols.push_back(p); + } + } + } + + polarity_t neg(polarity_t p) { + switch (p) { + case pol_pos: return pol_neg; + case pol_neg: return pol_pos; + case pol_dual: return pol_dual; + } + return pol_dual; + } + + polarity_t join(polarity_t p, polarity_t q) { + if (p == q) return p; + return pol_dual; + } + + void rewrite_goal(rw& r, goal_ref const& g) { + expr_ref new_curr(m); + proof_ref new_pr(m); + unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) { + expr * curr = g->form(i); + r(curr, new_curr, new_pr); + if (m_produce_proofs) { + proof * pr = g->pr(i); + new_pr = m.mk_modus_ponens(pr, new_pr); + } + g->update(i, new_curr, new_pr, g->dep(i)); + } + } + + +public: + nl_purify_tactic(ast_manager & m, params_ref const& p): + m(m), + m_util(m), + m_params(p), + m_nl_tac(mk_nlsat_tactic(m, p)), + m_solver(mk_smt_solver(m, p, symbol::null)), + m_fmc(0), + m_cancel(false), + m_eq_preds(m), + m_new_reals(m), + m_new_preds(m), + m_asms(m) + {} + + virtual ~nl_purify_tactic() {} + + virtual void updt_params(params_ref const & p) { + m_params = p; + } + + virtual tactic * translate(ast_manager& m) { + return alloc(nl_purify_tactic, m, m_params); + } + + virtual void set_cancel(bool f) { + if (f) { + m_nl_tac->cancel(); + m_solver->cancel(); + } + else { + m_solver->reset_cancel(); + m_nl_tac->reset_cancel(); + } + m_cancel = f; + } + + virtual void cleanup() { + m_solver = mk_smt_solver(m, m_params, symbol::null); + m_nl_tac->cleanup(); + m_eq_preds.reset(); + m_eq_values.reset(); + m_new_reals.reset(); + m_new_preds.reset(); + m_eq_pairs.reset(); + m_polarities.reset(); + } + + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + + tactic_report report("qfufnl-purify", *g); + m_produce_proofs = g->proofs_enabled(); + mc = 0; pc = 0; core = 0; + + fail_if_proof_generation("qfufnra-purify", g); + fail_if_unsat_core_generation("qfufnra-purify", g); + rw r(*this); + goal_ref nlg = alloc(goal, m, true, false); + + TRACE("nlsat_smt", g->display(tout);); + + // first hoist interface variables, + // then annotate subformulas by polarities, + // finally extract polynomial inequalities by + // creating a place-holder predicate inside the + // original goal and extracing pure nlsat clauses. + r.set_interface_var_mode(); + rewrite_goal(r, g); + get_polarities(*g.get()); + r.set_bool_mode(); + rewrite_goal(r, g); + + m_fmc = alloc(filter_model_converter, m); + app_ref_vector const& vars1 = m_new_reals; + for (unsigned i = 0; i < vars1.size(); ++i) { + SASSERT(is_uninterp_const(vars1[i])); + m_fmc->insert(vars1[i]->get_decl()); + } + app_ref_vector const& vars2 = m_new_preds; + for (unsigned i = 0; i < vars2.size(); ++i) { + SASSERT(is_uninterp_const(vars2[i])); + m_fmc->insert(vars2[i]->get_decl()); + } + + // add constraints to nlg. + unsigned sz = r.nl_cnstrs().size(); + for (unsigned i = 0; i < sz; i++) { + nlg->assert_expr(r.nl_cnstrs()[i], m_produce_proofs ? r.cfg().m_nl_cnstr_prs.get(i) : 0, 0); + } + g->inc_depth(); + for (unsigned i = 0; i < g->size(); ++i) { + m_solver->assert_expr(g->form(i)); + } + g->inc_depth(); + solve(nlg, result, mc); + } +}; + + +tactic * mk_nl_purify_tactic(ast_manager& m, params_ref const& p) { + return alloc(nl_purify_tactic, m, p); +} diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.h b/src/tactic/nlsat_smt/nl_purify_tactic.h new file mode 100644 index 000000000..9ffc99676 --- /dev/null +++ b/src/tactic/nlsat_smt/nl_purify_tactic.h @@ -0,0 +1,35 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + nl_purify_tactic.h + +Abstract: + + Tactic for purifying quantifier-free formulas that mix QF_NRA and other theories. + It is designed to allow cooprating between the nlsat solver and other theories + in a decoubled way. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-5-5. + +Revision History: + +--*/ +#ifndef _NL_PURIFY_TACTIC_H_ +#define _NL_PURIFY_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_nl_purify_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("nl-purify", "Decompose goal into pure NL-sat formula and formula over other theories.", "mk_nl_purify_tactic(m, p)") +*/ + +#endif + diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 5a18e0830..ad811cc70 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -30,6 +30,7 @@ Notes: #include"qffp_tactic.h" #include"qfaufbv_tactic.h" #include"qfauflia_tactic.h" +#include"qfufnra_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), @@ -43,7 +44,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p), - mk_smt_tactic()))))))))))), + cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), + mk_smt_tactic())))))))))))), p); return st; } diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index dea1081b3..b28c8cf3d 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -34,6 +34,7 @@ Notes: #include"default_tactic.h" #include"ufbv_tactic.h" #include"qffp_tactic.h" +#include"qfufnra_tactic.h" #include"horn_tactic.h" #include"smt_solver.h" @@ -84,6 +85,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); + else if (logic=="QF_UFNRA") + return mk_qfufnra_tactic(m, p); else return mk_default_tactic(m, p); } diff --git a/src/tactic/smtlogics/qfufnra_tactic.cpp b/src/tactic/smtlogics/qfufnra_tactic.cpp new file mode 100644 index 000000000..838573a19 --- /dev/null +++ b/src/tactic/smtlogics/qfufnra_tactic.cpp @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + qfufnra_tactic.cpp + +Abstract: + + Tactic for QF_UFNRA + +Author: + + Nikolaj (nbjorner) 2015-05-05 + +Notes: + +--*/ +#include"tactical.h" +#include"simplify_tactic.h" +#include"propagate_values_tactic.h" +#include"nl_purify_tactic.h" +#include"qfufnra_tactic.h" +#include"purify_arith_tactic.h" +#include"solve_eqs_tactic.h" +#include"elim_term_ite_tactic.h" +#include"elim_uncnstr_tactic.h" +#include"simplify_tactic.h" +#include"nnf_tactic.h" + + +tactic * mk_qfufnra_tactic(ast_manager & m, params_ref const& p) { + + return and_then(and_then(mk_simplify_tactic(m, p), + mk_purify_arith_tactic(m, p), + mk_propagate_values_tactic(m, p), + mk_solve_eqs_tactic(m, p), + mk_elim_uncnstr_tactic(m, p)), + and_then(mk_elim_term_ite_tactic(m, p), + mk_solve_eqs_tactic(m, p), + mk_simplify_tactic(m, p), + mk_nnf_tactic(m, p), + mk_nl_purify_tactic(m, p))); +} + + diff --git a/src/tactic/smtlogics/qfufnra_tactic.h b/src/tactic/smtlogics/qfufnra_tactic.h new file mode 100644 index 000000000..a2ac9b1ea --- /dev/null +++ b/src/tactic/smtlogics/qfufnra_tactic.h @@ -0,0 +1,31 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + qfufnra_tactic.h + +Abstract: + + Tactic for QF_UFNRA + +Author: + + Leonardo (leonardo) 2012-02-28 + +Notes: + +--*/ +#ifndef _QFUFNRA_TACTIC_ +#define _QFUFNRA_TACTIC_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_qfufnra_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfufnra", "builtin strategy for solving QF_UNFRA problems.", "mk_qfufnra_tactic(m, p)") +*/ + +#endif diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 198872cf5..5025b4449 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -207,7 +207,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d TRACE("tactic_mc", mc->display(tout);); TRACE("tactic_check_sat", tout << "r.size(): " << r.size() << "\n"; - for (unsigned i = 0; i < r.size(); i++) r[0]->display(tout);); + for (unsigned i = 0; i < r.size(); i++) r[i]->display(tout);); if (is_decided_sat(r)) { if (models_enabled) { diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index cfb4ec194..9765bced5 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -283,6 +283,10 @@ tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t return and_then(t1, and_then(t2, t3, t4, t5, t6, t7, t8, t9, t10)); } +tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9, tactic * t10, tactic * t11) { + return and_then(t1, and_then(t2, t3, t4, t5, t6, t7, t8, t9, t10, t11)); +} + tactic * and_then(unsigned num, tactic * const * ts) { SASSERT(num > 0); unsigned i = num - 1; diff --git a/src/tactic/tactical.h b/src/tactic/tactical.h index 4ceff2031..e291e6864 100644 --- a/src/tactic/tactical.h +++ b/src/tactic/tactical.h @@ -32,6 +32,7 @@ tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8); tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9); tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9, tactic * t10); +tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9, tactic * t10, tactic * t11); tactic * or_else(unsigned num, tactic * const * ts); tactic * or_else(tactic * t1, tactic * t2); diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp new file mode 100644 index 000000000..3f8014128 --- /dev/null +++ b/src/test/ddnf.cpp @@ -0,0 +1,167 @@ +#include "ddnf.h" +#include "tbv.h" +#include +#include +#include +#include +#include +#include +#include +#include + +/* +TBD: count number of nodes, number of operations accross all insertions +*/ + +void read_nums(std::istream& is, unsigned & x, unsigned& y) { + x = 0; y = 0; + is >> x; + is >> y; + std::string line; + std::getline(is, line); +} + +static bool g_verbose = false; +static char const* g_file = 0; + + +void create_forwarding(char const* file, datalog::ddnf_core& ddnf, ptr_vector& tbvs) { + + if (g_verbose) { + std::cout << "creating (and forgetting) forwarding index\n"; + } + std::ifstream is(file); + if (is.bad() || is.fail()) { + std::cout << "could not load " << file << "\n"; + exit(0); + } + + std::string line; + unsigned W, M; + read_nums(is, W, M); + tbv_manager& tbvm = ddnf.get_tbv_manager(); + tbv* tX = tbvm.allocateX(); + unsigned_vector forwarding_set; + for (unsigned r = 0; r < M; ++r) { + unsigned P, K; + read_nums(is, K, P); + ddnf.reset_accumulate(); + unsigned p; + unsigned_vector forwarding_index; + forwarding_index.resize(ddnf.size()); + for (unsigned g = 0; g < K; ++g) { + is >> p; + std::getline(is, line); + tbv* t = tbvm.allocate(line.c_str()); + if (p > P) { + std::cout << "port number " << p << " too big " << P << "\n"; + tbvm.display(std::cout, *t) << " " << line << "\n"; + exit(0); + } + forwarding_set.reset(); + ddnf.accumulate(*t, forwarding_set); + for (unsigned i = 0; i < forwarding_set.size(); ++i) { + forwarding_index[forwarding_set[i]] = p; + } + tbvs.push_back(t); + if (p == 0 && tbvm.equals(*t, *tX)) break; + } + } + tbvm.deallocate(tX); +} + +datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector& tbvs) { + + if (g_verbose) { + std::cout << "populate ddnf\n"; + } + + std::ifstream is(file); + if (is.bad() || is.fail()) { + std::cout << "could not load " << file << "\n"; + exit(0); + } + + std::string line; + unsigned W, M; + read_nums(is, W, M); + datalog::ddnf_core* ddnf = alloc(datalog::ddnf_core, W); + tbv_manager& tbvm = ddnf->get_tbv_manager(); + tbv* tX = tbvm.allocateX(); + for (unsigned r = 0; r < M; ++r) { + unsigned P, K; + read_nums(is, K, P); + if (g_verbose) { + std::cout << K << " " << P << "\n"; + } + unsigned p; + for (unsigned g = 0; g < K; ++g) { + is >> p; + std::getline(is, line); + tbv* t = tbvm.allocate(line.c_str()); + ddnf->insert(*t); + //tbvm.display(std::cout << line << " ", *t) << "\n"; + tbvs.push_back(t); + if (p > P) { + std::cout << "port number " << p << " too big " << P << "\n"; + tbvm.display(std::cout, *t) << " " << line << "\n"; + exit(0); + } + if (p == 0 && tbvm.equals(*t, *tX)) break; + } + } + + tbvm.deallocate(tX); + + return ddnf; +} + + +static void read_args(char ** argv, int argc) { + if (argc == 3) { + g_file = argv[2]; + return; + } + + for (int i = 2; i < argc; ++i) { + if (argv[i] == "v") { + g_verbose = true; + } + else { + g_file = argv[i]; + } + } + + if (!g_file) { + std::cout << "Need routing table file as argument. Arguments provided: "; + for (int i = 0; i < argc; ++i) { + std::cout << argv[i] << " "; + } + std::cout << "\n"; + exit(0); + } + +} + +void tst_ddnf(char ** argv, int argc, int& i) { + read_args(argv, argc); + ptr_vector tbvs; + datalog::ddnf_core* ddnf = populate_ddnf(g_file, tbvs); + create_forwarding(g_file, *ddnf, tbvs); + std::cout << "resulting size: " << ddnf->size() << "\n"; + ddnf->display_statistics(std::cout); + if (g_verbose) { + ddnf->display(std::cout); + } + std::cout.flush(); + + tbv_manager& tbvm = ddnf->get_tbv_manager(); + for (unsigned i = 0; i < tbvs.size(); ++i) { + tbvm.deallocate(tbvs[i]); + } + dealloc(ddnf); +} + + + + diff --git a/src/test/main.cpp b/src/test/main.cpp index 7b01e35c1..be12286fb 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -225,6 +225,7 @@ int main(int argc, char ** argv) { TST(simplex); TST(sat_user_scope); TST(pdr); + TST_ARGV(ddnf); //TST_ARGV(hs); }