From 70a1155d711e38895174ada51d6568ae3af3b7ce Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 18 Aug 2014 17:13:16 -0700 Subject: [PATCH] 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: