From 13b61d894c0c352b2baa1e3c3cae7a939e97c160 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 9 Sep 2014 14:02:46 -0700 Subject: [PATCH] adding recursion bounds to duality --- src/duality/duality.h | 5 +++-- src/duality/duality_rpfp.cpp | 5 ++++- src/duality/duality_solver.cpp | 23 ++++++++++++++++------- src/muz/base/dl_context.cpp | 8 ++++++-- src/muz/base/dl_context.h | 5 +++-- src/muz/duality/duality_dl_interface.cpp | 17 ++++++++++++++--- src/muz/fp/dl_cmds.cpp | 20 ++++++++++++++------ 7 files changed, 60 insertions(+), 23 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index c1c9797f3..16576dd65 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -488,9 +488,10 @@ protected: std::vector Incoming; Term dual; Node *map; + unsigned recursion_bound; Node(const FuncDecl &_Name, const Transformer &_Annotation, const Transformer &_Bound, const Transformer &_Underapprox, const Term &_dual, RPFP *_owner, int _number) - : Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0;} + : Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0; recursion_bound = UINT_MAX;} }; /** Create a node in the graph. The input is a term R(v_1...v_n) @@ -829,7 +830,7 @@ protected: #ifdef _WINDOWS __declspec(dllexport) #endif - void FromClauses(const std::vector &clauses); + void FromClauses(const std::vector &clauses, const std::vector *bounds = 0); void FromFixpointContext(fixedpoint fp, std::vector &queries); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index ef37dd8a2..8c88dda72 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -3570,7 +3570,7 @@ namespace Duality { #define USE_QE_LITE - void RPFP::FromClauses(const std::vector &unskolemized_clauses){ + void RPFP::FromClauses(const std::vector &unskolemized_clauses, const std::vector *bounds){ hash_map pmap; func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort()); @@ -3663,6 +3663,7 @@ namespace Duality { pmap[R] = node; if (is_query) node->Bound = CreateRelation(std::vector(), ctx.bool_val(false)); + node->recursion_bound = bounds ? 0 : UINT_MAX; } } @@ -3728,6 +3729,8 @@ namespace Duality { Transformer T = CreateTransformer(Relparams,Indparams,body); Edge *edge = CreateEdge(Parent,T,Children); edge->labeled = labeled;; // remember for label extraction + if(bounds) + Parent->recursion_bound = std::max(Parent->recursion_bound,(*bounds)[i]); // edges.push_back(edge); } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 681582415..f54e00693 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -33,6 +33,7 @@ Revision History: #include #include #include +#include // TODO: make these official options or get rid of them @@ -304,7 +305,7 @@ namespace Duality { #ifdef BOUNDED struct Counter { - int val; + unsigned val; Counter(){val = 0;} }; typedef std::map NodeToCounter; @@ -321,6 +322,10 @@ namespace Duality { heuristic = !cex.get_tree() ? (Heuristic *)(new LocalHeuristic(rpfp)) : (Heuristic *)(new ReplayHeuristic(rpfp,cex)); #endif + // determine if we are recursion bounded + for(unsigned i = 0; i < rpfp->nodes.size(); i++) + if(rpfp->nodes[i]->recursion_bound < UINT_MAX) + RecursionBound = 0; cex.clear(); // in case we didn't use it for heuristic if(unwinding) delete unwinding; unwinding = new RPFP(rpfp->ls); @@ -461,7 +466,7 @@ namespace Duality { } return false; } - + /** Create an instance of a node in the unwinding. Set its annotation to true, and mark it unexpanded. */ Node* CreateNodeInstance(Node *node, int number = 0){ @@ -780,10 +785,8 @@ namespace Duality { std::vector &insts = insts_of_node[node]; for(unsigned j = 0; j < insts.size(); j++) if(indset->Contains(insts[j])) - if(NodePastRecursionBound(insts[j])){ + if(NodePastRecursionBound(insts[j],true)) recursionBounded = true; - return; - } } } @@ -801,12 +804,18 @@ namespace Duality { } #ifdef BOUNDED - bool NodePastRecursionBound(Node *node){ + bool NodePastRecursionBound(Node *node, bool report = false){ if(RecursionBound < 0) return false; NodeToCounter &backs = back_edges[node]; for(NodeToCounter::iterator it = backs.begin(), en = backs.end(); it != en; ++it){ - if(it->second.val > RecursionBound) + if(it->second.val > it->first->recursion_bound){ + if(report){ + std::ostringstream os; + os << "cut off " << it->first->Name.name() << " at depth " << it->second.val; + reporter->Message(os.str()); + } return true; + } } return false; } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index fbef46ae3..80af7eeb0 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -246,6 +246,7 @@ namespace datalog { m_rule_fmls_head = 0; m_rule_fmls.reset(); m_rule_names.reset(); + m_rule_bounds.reset(); m_argument_var_names.reset(); m_preds.reset(); m_preds_by_name.reset(); @@ -474,9 +475,10 @@ namespace datalog { return new_pred; } - void context::add_rule(expr* rl, symbol const& name) { + void context::add_rule(expr* rl, symbol const& name, unsigned bound) { m_rule_fmls.push_back(rl); m_rule_names.push_back(name); + m_rule_bounds.push_back(bound); } void context::flush_add_rules() { @@ -1102,12 +1104,13 @@ namespace datalog { } } - void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names){ + void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names, vector &bounds){ for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { expr_ref r = bind_variables(m_rule_fmls[i].get(), true); rules.push_back(r.get()); // rules.push_back(m_rule_fmls[i].get()); names.push_back(m_rule_names[i]); + bounds.push_back(m_rule_bounds[i]); } } @@ -1125,6 +1128,7 @@ namespace datalog { m_rule_names[i] = m_rule_names.back(); m_rule_fmls.pop_back(); m_rule_names.pop_back(); + m_rule_bounds.pop_back(); --i; } } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 7349fa889..cf2c53913 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -194,6 +194,7 @@ namespace datalog { unsigned m_rule_fmls_head; expr_ref_vector m_rule_fmls; svector m_rule_names; + vector m_rule_bounds; expr_ref_vector m_background; model_converter_ref m_mc; proof_converter_ref m_pc; @@ -366,7 +367,7 @@ namespace datalog { rule_set & get_rules() { flush_add_rules(); return m_rule_set; } void get_rules_as_formulas(expr_ref_vector& fmls, svector& names); - void get_raw_rule_formulas(expr_ref_vector& fmls, svector& names); + void get_raw_rule_formulas(expr_ref_vector& fmls, svector& names, vector &bounds); void add_fact(app * head); void add_fact(func_decl * pred, const relation_fact & fact); @@ -383,7 +384,7 @@ namespace datalog { /** Method exposed from API for adding rules. */ - void add_rule(expr* rl, symbol const& name); + void add_rule(expr* rl, symbol const& name, unsigned bound = UINT_MAX); /** diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 849cf94ea..08c57b05e 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -155,8 +155,9 @@ lbool dl_interface::query(::expr * query) { expr_ref_vector rules(m_ctx.get_manager()); svector< ::symbol> names; + vector bounds; // m_ctx.get_rules_as_formulas(rules, names); - m_ctx.get_raw_rule_formulas(rules, names); + m_ctx.get_raw_rule_formulas(rules, names, bounds); // get all the rules as clauses std::vector &clauses = _d->clauses; @@ -200,6 +201,7 @@ lbool dl_interface::query(::expr * query) { expr qc = implies(q,_d->ctx.bool_val(false)); qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc); clauses.push_back(qc); + bounds.push_back(UINT_MAX); // get the background axioms unsigned num_asserts = m_ctx.get_num_assertions(); @@ -243,13 +245,21 @@ lbool dl_interface::query(::expr * query) { expr c = implies(_d->ctx.bool_val(false),f(args)); c = _d->ctx.make_quant(Forall,args,c); clauses.push_back(c); + bounds.push_back(UINT_MAX); } } } } + unsigned rb = m_ctx.get_params().recursion_bound(); + std::vector std_bounds; + for(unsigned i = 0; i < bounds.size(); i++){ + unsigned b = bounds[i]; + if (b == UINT_MAX) b = rb; + std_bounds.push_back(b); + } // creates 1-1 map between clauses and rpfp edges - _d->rpfp->FromClauses(clauses); + _d->rpfp->FromClauses(clauses,&std_bounds); // populate the edge-to-clause map for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i) @@ -271,11 +281,12 @@ lbool dl_interface::query(::expr * query) { rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0"); rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0"); rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file()); - unsigned rb = m_ctx.get_params().recursion_bound(); +#if 0 if(rb != UINT_MAX){ std::ostringstream os; os << rb; rs->SetOption("recursion_bound", os.str()); } +#endif // Solve! bool ans; diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index f9916808c..e2e3680cc 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -100,7 +100,7 @@ struct dl_context { dlctx().set_predicate_representation(pred, num_kinds, kinds); } - void add_rule(expr * rule, symbol const& name) { + void add_rule(expr * rule, symbol const& name, unsigned bound) { init(); if (m_collected_cmds) { expr_ref rl = m_context->bind_variables(rule, true); @@ -110,7 +110,7 @@ struct dl_context { m_trail.push(push_back_vector >(m_collected_cmds->m_names)); } else { - m_context->add_rule(rule, name); + m_context->add_rule(rule, name, bound); } } @@ -151,19 +151,22 @@ class dl_rule_cmd : public cmd { mutable unsigned m_arg_idx; expr* m_t; symbol m_name; + unsigned m_bound; public: dl_rule_cmd(dl_context * dl_ctx): cmd("rule"), m_dl_ctx(dl_ctx), m_arg_idx(0), - m_t(0) {} - virtual char const * get_usage() const { return "(forall (q) (=> (and body) head)) :optional-name"; } + m_t(0), + m_bound(UINT_MAX) {} + virtual char const * get_usage() const { return "(forall (q) (=> (and body) head)) :optional-name :optional-recursion-bound"; } virtual char const * get_descr(cmd_context & ctx) const { return "add a Horn rule."; } virtual unsigned get_arity() const { return VAR_ARITY; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { switch(m_arg_idx) { case 0: return CPK_EXPR; case 1: return CPK_SYMBOL; + case 2: return CPK_UINT; default: return CPK_SYMBOL; } } @@ -173,13 +176,18 @@ public: } virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_name = s; + m_arg_idx++; + } + virtual void set_next_arg(cmd_context & ctx, unsigned bound) { + m_bound = bound; + m_arg_idx++; } virtual void reset(cmd_context & ctx) { m_dl_ctx->reset(); prepare(ctx); } - virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; } + virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; m_bound = UINT_MAX; } virtual void finalize(cmd_context & ctx) { } virtual void execute(cmd_context & ctx) { - m_dl_ctx->add_rule(m_t, m_name); + m_dl_ctx->add_rule(m_t, m_name, m_bound); } };