From 60054ce469c3e2bc8c34e7b9285c8450e4232812 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2014 21:20:56 -0700 Subject: [PATCH 1/2] fix cache bug in PDR reported by Phillip Ruemmer Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 38 +++++++++++++++++++++++++------------ src/muz/pdr/pdr_context.h | 13 ++++++++----- 2 files changed, 34 insertions(+), 17 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index b09280d35..94dd5d0a0 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -736,6 +736,11 @@ namespace pdr { m_closed = true; } + void model_node::reopen() { + SASSERT(m_closed); + m_closed = false; + } + static bool is_ini(datalog::rule const& r) { return r.get_uninterpreted_tail_size() == 0; } @@ -745,6 +750,7 @@ namespace pdr { return const_cast(m_rule); } // only initial states are not set by the PDR search. + SASSERT(m_model.get()); datalog::rule const& rl1 = pt().find_rule(*m_model); if (is_ini(rl1)) { set_rule(&rl1); @@ -864,9 +870,10 @@ namespace pdr { } void model_search::add_leaf(model_node& n) { - unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value; - ++count; - if (count == 1 || is_repeated(n)) { + model_nodes ns; + model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value; + nodes.push_back(&n); + if (nodes.size() == 1 || is_repeated(n)) { set_leaf(n); } else { @@ -875,7 +882,7 @@ namespace pdr { } void model_search::set_leaf(model_node& n) { - erase_children(n); + erase_children(n, true); SASSERT(n.is_open()); enqueue_leaf(n); } @@ -897,7 +904,7 @@ namespace pdr { set_leaf(*root); } - obj_map& model_search::cache(model_node const& n) { + obj_map >& model_search::cache(model_node const& n) { unsigned l = n.orig_level(); if (l >= m_cache.size()) { m_cache.resize(l + 1); @@ -905,7 +912,7 @@ namespace pdr { return m_cache[l]; } - void model_search::erase_children(model_node& n) { + void model_search::erase_children(model_node& n, bool backtrack) { ptr_vector todo, nodes; todo.append(n.children()); erase_leaf(n); @@ -916,13 +923,20 @@ namespace pdr { nodes.push_back(m); todo.append(m->children()); erase_leaf(*m); - remove_node(*m); + remove_node(*m, backtrack); } std::for_each(nodes.begin(), nodes.end(), delete_proc()); } - void model_search::remove_node(model_node& n) { - if (0 == --cache(n).find(n.state())) { + void model_search::remove_node(model_node& n, bool backtrack) { + model_nodes& nodes = cache(n).find(n.state()); + nodes.erase(&n); + if (nodes.size() > 0 && n.is_open() && backtrack) { + for (unsigned i = 0; i < nodes.size(); ++i) { + nodes[i]->reopen(); + } + } + if (nodes.empty()) { cache(n).remove(n.state()); } } @@ -1203,8 +1217,8 @@ namespace pdr { void model_search::reset() { if (m_root) { - erase_children(*m_root); - remove_node(*m_root); + erase_children(*m_root, false); + remove_node(*m_root, false); dealloc(m_root); m_root = 0; } @@ -1240,7 +1254,7 @@ namespace pdr { m_pm(m_fparams, params.max_num_contexts(), m), m_query_pred(m), m_query(0), - m_search(m_params.bfs_model_search()), + m_search(m_params.bfs_model_search(), m), m_last_result(l_undef), m_inductive_lvl(0), m_expanded_lvl(0), diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 8a4f3e438..a85011600 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -231,6 +231,7 @@ namespace pdr { } void set_closed(); + void reopen(); void set_pre_closed() { m_closed = true; } void reset() { m_children.reset(); } @@ -243,19 +244,21 @@ namespace pdr { }; class model_search { + typedef ptr_vector model_nodes; + ast_manager& m; bool m_bfs; model_node* m_root; std::deque m_leaves; - vector > m_cache; + vector > m_cache; - obj_map& cache(model_node const& n); - void erase_children(model_node& n); + obj_map& cache(model_node const& n); + void erase_children(model_node& n, bool backtrack); void erase_leaf(model_node& n); - void remove_node(model_node& n); + void remove_node(model_node& n, bool backtrack); void enqueue_leaf(model_node& n); // add leaf to priority queue. void update_models(); public: - model_search(bool bfs): m_bfs(bfs), m_root(0) {} + model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {} ~model_search(); void reset(); From 70a1155d711e38895174ada51d6568ae3af3b7ce Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 18 Aug 2014 17:13:16 -0700 Subject: [PATCH 2/2] fixed duality bug and added some code for returning bounded status (not yet used) --- src/duality/duality.h | 7 +++ src/duality/duality_solver.cpp | 24 +++++++++++ src/muz/base/dl_context.h | 3 ++ src/muz/duality/duality_dl_interface.cpp | 55 +++++++++++++++++++++++- src/muz/fp/dl_cmds.cpp | 5 +++ 5 files changed, 93 insertions(+), 1 deletion(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index c315c5431..c1c9797f3 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1152,6 +1152,13 @@ protected: virtual void LearnFrom(Solver *old_solver) = 0; + /** Return true if the solution be incorrect due to recursion bounding. + That is, the returned "solution" might contain all derivable facts up to the + given recursion bound, but not be actually a fixed point. + */ + + virtual bool IsResultRecursionBounded() = 0; + virtual ~Solver(){} static Solver *Create(const std::string &solver_class, RPFP *rpfp); diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 59611c814..681582415 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -768,6 +768,29 @@ namespace Duality { annot.Simplify(); } + bool recursionBounded; + + /** See if the solution might be bounded. */ + void TestRecursionBounded(){ + recursionBounded = false; + if(RecursionBound == -1) + return; + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + std::vector &insts = insts_of_node[node]; + for(unsigned j = 0; j < insts.size(); j++) + if(indset->Contains(insts[j])) + if(NodePastRecursionBound(insts[j])){ + recursionBounded = true; + return; + } + } + } + + bool IsResultRecursionBounded(){ + return recursionBounded; + } + /** Generate a proposed solution of the input RPFP from the unwinding, by unioning the instances of each node. */ void GenSolutionFromIndSet(bool with_markers = false){ @@ -1026,6 +1049,7 @@ namespace Duality { timer_stop("ProduceCandidatesForExtension"); if(candidates.empty()){ GenSolutionFromIndSet(); + TestRecursionBounded(); return true; } Candidate cand = candidates.front(); diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 1952cc42f..7349fa889 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -53,6 +53,7 @@ namespace datalog { MEMOUT, INPUT_ERROR, APPROX, + BOUNDED, CANCELED }; @@ -304,6 +305,8 @@ namespace datalog { \brief Retrieve predicates */ func_decl_set const& get_predicates() const { return m_preds; } + ast_ref_vector const &get_pinned() const {return m_pinned; } + bool is_predicate(func_decl* pred) const { return m_preds.contains(pred); } bool is_predicate(expr * e) const { return is_app(e) && is_predicate(to_app(e)->get_decl()); } diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 0584e6b58..849cf94ea 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -36,6 +36,7 @@ Revision History: #include "model_v2_pp.h" #include "fixedpoint_params.hpp" #include "used_vars.h" +#include "func_decl_dependencies.h" // template class symbol_table; @@ -207,6 +208,46 @@ lbool dl_interface::query(::expr * query) { _d->rpfp->AssertAxiom(e); } + // make sure each predicate is the head of at least one clause + func_decl_set heads; + for(unsigned i = 0; i < clauses.size(); i++){ + expr cl = clauses[i]; + + while(true){ + if(cl.is_app()){ + decl_kind k = cl.decl().get_decl_kind(); + if(k == Implies) + cl = cl.arg(1); + else { + heads.insert(cl.decl()); + break; + } + } + else if(cl.is_quantifier()) + cl = cl.body(); + else break; + } + } + ast_ref_vector const &pinned = m_ctx.get_pinned(); + for(unsigned i = 0; i < pinned.size(); i++){ + ::ast *fa = pinned[i]; + if(is_func_decl(fa)){ + ::func_decl *fd = to_func_decl(fa); + if(m_ctx.is_predicate(fd)) { + func_decl f(_d->ctx,fd); + if(!heads.contains(fd)){ + int arity = f.arity(); + std::vector args; + for(int j = 0; j < arity; j++) + args.push_back(_d->ctx.fresh_func_decl("X",f.domain(j))()); + expr c = implies(_d->ctx.bool_val(false),f(args)); + c = _d->ctx.make_quant(Forall,args,c); + clauses.push_back(c); + } + } + } + } + // creates 1-1 map between clauses and rpfp edges _d->rpfp->FromClauses(clauses); @@ -265,7 +306,19 @@ lbool dl_interface::query(::expr * query) { // dealloc(rs); this is now owned by data // true means the RPFP problem is SAT, so the query is UNSAT - return ans ? l_false : l_true; + // but we return undef if the UNSAT result is bounded + if(ans){ + if(rs->IsResultRecursionBounded()){ +#if 0 + m_ctx.set_status(datalog::BOUNDED); + return l_undef; +#else + return l_false; +#endif + } + return l_false; + } + return l_true; } expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) { diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 827b90e60..f9916808c 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -252,6 +252,11 @@ public: print_certificate(ctx); break; case l_undef: + if(dlctx.get_status() == datalog::BOUNDED){ + ctx.regular_stream() << "bounded\n"; + print_certificate(ctx); + break; + } ctx.regular_stream() << "unknown\n"; switch(dlctx.get_status()) { case datalog::INPUT_ERROR: