From 13b61d894c0c352b2baa1e3c3cae7a939e97c160 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 9 Sep 2014 14:02:46 -0700 Subject: [PATCH 01/12] 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); } }; From 4c71e9479d00048a9a6f8666499d7e1f4b616c73 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 30 Sep 2014 11:21:34 -0700 Subject: [PATCH 02/12] optimizing array final check --- src/smt/theory_array_base.cpp | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 3f96a1d62..6325a2a99 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -376,8 +376,10 @@ namespace smt { enode_vector::const_iterator end = r->end_parents(); for (; it != end; ++it) { enode * parent = *it; +#if 0 if (!ctx.is_relevant(parent)) continue; +#endif unsigned num_args = parent->get_num_args(); if (is_store(parent)) { SET_ARRAY(parent->get_arg(0)); @@ -399,6 +401,7 @@ namespace smt { return false; } +#if 0 void theory_array_base::collect_shared_vars(sbuffer & result) { TRACE("array_shared", tout << "collecting shared vars...\n";); context & ctx = get_context(); @@ -420,6 +423,29 @@ namespace smt { } unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); } +#else + void theory_array_base::collect_shared_vars(sbuffer & result) { + TRACE("array_shared", tout << "collecting shared vars...\n";); + context & ctx = get_context(); + ptr_buffer to_unmark; + unsigned num_vars = get_num_vars(); + for (unsigned i = 0; i < num_vars; i++) { + enode * n = get_enode(i); + if (ctx.is_relevant(n)) { + enode * r = n->get_root(); + if (!r->is_marked() && is_array_sort(r) && ctx.is_shared(r)) { + TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); + theory_var r_th_var = r->get_th_var(get_id()); + SASSERT(r_th_var != null_theory_var); + result.push_back(r_th_var); + } + r->set_mark(); + to_unmark.push_back(r); + } + } + unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); + } +#endif /** \brief Create interface variables for shared array variables. From 47635325014f2951d203897eae4d8120787a283d Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 30 Sep 2014 11:25:47 -0700 Subject: [PATCH 03/12] adding compile-time option to replace arrays with maps in smt (define SPARSE_MAP) --- src/smt/smt_context.h | 7 ++++++- src/smt/smt_enode.cpp | 6 +++--- src/smt/smt_enode.h | 29 ++++++++++++++++++++++++++--- src/util/map.h | 2 +- 4 files changed, 36 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7940b17be..5abdfa5f9 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -54,7 +54,11 @@ Revision History: // the case that each context only references a few expressions. // Using a map instead of a vector for the literals can compress space // consumption. +#ifdef SPARSE_MAP +#define USE_BOOL_VAR_VECTOR 0 +#else #define USE_BOOL_VAR_VECTOR 1 +#endif namespace smt { @@ -69,6 +73,7 @@ namespace smt { std::string last_failure_as_string() const; void set_progress_callback(progress_callback *callback); + protected: ast_manager & m_manager; smt_params & m_fparams; @@ -106,7 +111,7 @@ namespace smt { // ----------------------------------- enode * m_true_enode; enode * m_false_enode; - ptr_vector m_app2enode; // app -> enode + app2enode_t m_app2enode; // app -> enode ptr_vector m_enodes; plugin_manager m_theories; // mapping from theory_id -> theory ptr_vector m_theory_set; // set of theories for fast traversal diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 98b8eaf8b..451577357 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -24,7 +24,7 @@ namespace smt { /** \brief Initialize an enode in the given memory position. */ - enode * enode::init(ast_manager & m, void * mem, ptr_vector const & app2enode, app * owner, + enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); @@ -60,7 +60,7 @@ namespace smt { return n; } - enode * enode::mk(ast_manager & m, region & r, ptr_vector const & app2enode, app * owner, + enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent) { SASSERT(m.is_bool(owner) || !merge_tf); @@ -69,7 +69,7 @@ namespace smt { return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent); } - enode * enode::mk_dummy(ast_manager & m, ptr_vector const & app2enode, app * owner) { + enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) { unsigned sz = get_enode_size(owner->get_num_args()); void * mem = alloc_svect(char, sz); return init(m, mem, app2enode, owner, 0, false, false, 0, true, false); diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 505dea0ee..ca75028c3 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -38,6 +38,29 @@ namespace smt { } }; + /** \ brief Use sparse maps in SMT solver. + + Define this to use hash maps rather than vectors over ast + nodes. This is useful in the case there are many solvers, each + referencing few nodes from a large ast manager. There is some + unknown performance penalty for this. */ + + // #define SPARSE_MAP + +#ifndef SPARSE_MAP + typedef ptr_vector app2enode_t; // app -> enode +#else + class app2enode_t : public u_map { + public: + void setx(unsigned x, enode *val, enode *def){ + if(val == 0) + erase(x); + else + insert(x,val); + } + }; +#endif + class tmp_enode; /** @@ -115,7 +138,7 @@ namespace smt { friend class tmp_enode; - static enode * init(ast_manager & m, void * mem, ptr_vector const & app2enode, app * owner, + static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); public: @@ -124,11 +147,11 @@ namespace smt { return sizeof(enode) + num_args * sizeof(enode*); } - static enode * mk(ast_manager & m, region & r, ptr_vector const & app2enode, app * owner, + static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, bool cgc_enabled, bool update_children_parent); - static enode * mk_dummy(ast_manager & m, ptr_vector const & app2enode, app * owner); + static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner); static void del_dummy(enode * n) { dealloc_svect(reinterpret_cast(n)); } diff --git a/src/util/map.h b/src/util/map.h index 3e8e10891..d659b89c0 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -131,7 +131,7 @@ public: value const& get(key const& k, value const& default_value) const { entry* e = find_core(k); if (e) { - return e->m_value; + return e->get_data().m_value; } else { return default_value; From 301cb51bbb81a3fd8db81e9baa8850dc2d6bc117 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 30 Sep 2014 12:42:30 -0700 Subject: [PATCH 04/12] added restarts options to duality (plus some other disabled features) --- src/duality/duality.h | 6 + src/duality/duality_rpfp.cpp | 67 ++++ src/duality/duality_solver.cpp | 391 +++++++++++++++++++++-- src/muz/base/fixedpoint_params.pyg | 1 + src/muz/duality/duality_dl_interface.cpp | 1 + 5 files changed, 446 insertions(+), 20 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 16576dd65..edd89d78f 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -104,6 +104,8 @@ namespace Duality { FuncDecl RenumberPred(const FuncDecl &f, int n); + FuncDecl NumberPred(const FuncDecl &f, int n); + Term ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming); @@ -903,6 +905,10 @@ protected: int CumulativeDecisions(); + void GreedyReduceNodes(std::vector &nodes); + + check_result CheckWithConstrainedNodes(std::vector &posnodes,std::vector &negnodes); + solver &slvr(){ return *ls->slvr; } diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 8c88dda72..f2824c9b0 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2816,6 +2816,62 @@ namespace Duality { } } + void foobar(){ + } + + void RPFP::GreedyReduceNodes(std::vector &nodes){ + std::vector lits; + for(unsigned i = 0; i < nodes.size(); i++){ + Term b; std::vector v; + RedVars(nodes[i], b, v); + lits.push_back(!b); + expr bv = dualModel.eval(b); + if(eq(bv,ctx.bool_val(true))){ + check_result res = slvr_check(lits.size(),&lits[0]); + if(res == unsat) + lits.pop_back(); + else + foobar(); + } + } + } + + check_result RPFP::CheckWithConstrainedNodes(std::vector &posnodes,std::vector &negnodes){ + timer_start("Check"); + std::vector lits; + for(unsigned i = 0; i < posnodes.size(); i++){ + Term b; std::vector v; + RedVars(posnodes[i], b, v); + lits.push_back(b); + } + for(unsigned i = 0; i < negnodes.size(); i++){ + Term b; std::vector v; + RedVars(negnodes[i], b, v); + lits.push_back(!b); + } + check_result res = slvr_check(lits.size(),&lits[0]); + if(res == unsat && posnodes.size()){ + lits.resize(posnodes.size()); + res = slvr_check(lits.size(),&lits[0]); + } + dualModel = slvr().get_model(); +#if 0 + if(!dualModel.null()){ + std::cout << "posnodes called:\n"; + for(unsigned i = 0; i < posnodes.size(); i++) + if(!Empty(posnodes[i])) + std::cout << posnodes[i]->Name.name() << "\n"; + std::cout << "negnodes called:\n"; + for(unsigned i = 0; i < negnodes.size(); i++) + if(!Empty(negnodes[i])) + std::cout << negnodes[i]->Name.name() << "\n"; + } +#endif + timer_stop("Check"); + return res; + } + + void RPFP_caching::FilterCore(std::vector &core, std::vector &full_core){ hash_set core_set; std::copy(full_core.begin(),full_core.end(),std::inserter(core_set,core_set.begin())); @@ -3333,6 +3389,17 @@ namespace Duality { return ctx.function(name.c_str(), arity, &domain[0], f.range()); } + Z3User::FuncDecl Z3User::NumberPred(const FuncDecl &f, int n) + { + std::string name = f.name().str(); + name = name + "_" + string_of_int(n); + int arity = f.arity(); + std::vector domain; + for(int i = 0; i < arity; i++) + domain.push_back(f.domain(i)); + return ctx.function(name.c_str(), arity, &domain[0], f.range()); + } + // Scan the clause body for occurrences of the predicate unknowns RPFP::Term RPFP::ScanBody(hash_map &memo, diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index f54e00693..49e591be2 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -255,6 +255,13 @@ namespace Duality { /** Called when done expanding a tree */ virtual void Done() {} + + /** Ask whether a node should be used/unused in the tree. Returns, + 1 if yes, -1 if no, and 0 if don't care. */ + + virtual int UseNode(Node *node){ + return 0; + } }; /** The Proposer class proposes conjectures eagerly. These can come @@ -302,6 +309,7 @@ namespace Duality { hash_set overapproxes; std::vector proposers; std::string ConjectureFile; + bool stratified_inlining_done; #ifdef BOUNDED struct Counter { @@ -314,6 +322,13 @@ namespace Duality { /** Solve the problem. */ virtual bool Solve(){ + PreSolve(); + bool res = SolveMain(); // does the actual work + PostSolve(); + return res; + } + + void PreSolve(){ reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp); conj_reporter = ConjectureFile.empty() ? 0 : CreateConjectureFileReporter(rpfp,ConjectureFile); #ifndef LOCALIZE_CONJECTURES @@ -342,9 +357,10 @@ namespace Duality { return false; #endif StratifiedLeafCount = -1; - timer_start("SolveMain"); - bool res = SolveMain(); // does the actual work - timer_stop("SolveMain"); + stratified_inlining_done = false; + } + + void PostSolve(){ // print_profile(std::cout); delete indset; delete heuristic; @@ -354,7 +370,16 @@ namespace Duality { delete conj_reporter; for(unsigned i = 0; i < proposers.size(); i++) delete proposers[i]; - return res; + } + + bool RecheckBounds(){ + for(unsigned i = 0; i < unwinding->nodes.size(); i++){ + Node *node = unwinding->nodes[i]; + node->Bound = node->map->Bound; + if(!SatisfyUpperBound(node)) + return false; + } + return true; } void CreateInitialUnwinding(){ @@ -417,6 +442,7 @@ namespace Duality { bool StratifiedInlining; // Do stratified inlining as preprocessing step int RecursionBound; // Recursion bound for bounded verification bool BatchExpand; + bool EnableRestarts; bool SetBoolOption(bool &opt, const std::string &value){ if(value == "0") { @@ -464,6 +490,9 @@ namespace Duality { if(option == "conjecture_file"){ ConjectureFile = value; } + if(option == "enable_restarts"){ + return SetBoolOption(EnableRestarts,value); + } return false; } @@ -901,6 +930,9 @@ namespace Duality { */ bool DoStratifiedInlining(){ + if(stratified_inlining_done) + return true; + stratified_inlining_done = true; DoTopoSort(); int depth = 1; // TODO: make this an option std::vector > unfolding_levels(depth+1); @@ -1043,10 +1075,17 @@ namespace Duality { h->SetOldNode(node); } + bool SolveMain(){ + timer_start("SolveMain"); + bool res = SolveMainInt(); // does the actual work + timer_stop("SolveMain"); + return res; + } + /** This does the actual solving work. We try to generate candidates for extension. If we succed, we extend the unwinding. If we fail, we have a solution. */ - bool SolveMain(){ + bool SolveMainInt(){ if(StratifiedInlining && !DoStratifiedInlining()) return false; #ifdef BOUNDED @@ -1776,6 +1815,7 @@ namespace Duality { } timer_stop("Propagate"); } + /** This class represents a derivation tree. */ class DerivationTree { @@ -2127,6 +2167,8 @@ namespace Duality { hash_map updates; + int restart_interval; + DerivationTreeSlow(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) : DerivationTree(_duality, rpfp, _reporter, _heuristic, _full_expand) { stack.push_back(stack_entry()); @@ -2135,6 +2177,7 @@ namespace Duality { struct DoRestart {}; virtual bool Build(){ + restart_interval = 3; while (true) { try { return BuildMain(); @@ -2145,15 +2188,47 @@ namespace Duality { while(stack.size() > 1) PopLevel(); reporter->Message("restarted"); + restart_interval += 1; } } } + + // When we check, try to use the same children that were used in the + // previous counterexample. + check_result Check(){ +#if 0 + std::vector posnodes, negnodes; + std::vector &expansions = stack.back().expansions; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + std::vector &chs = node->Outgoing->Children; + for(unsigned j = 0; j < chs.size(); j++){ + Node *ch = chs[j]; + int use = heuristic->UseNode(ch); + if(use == 1) + posnodes.push_back(ch); + else if (use == -1) + negnodes.push_back(ch); + } + } + if(!(posnodes.empty() && negnodes.empty())){ + check_result res = tree->CheckWithConstrainedNodes(posnodes,negnodes); + if(res != unsat){ + reporter->Message("matched previous counterexample"); + return res; + } + } +#endif + return tree->Check(top); + } + bool BuildMain(){ stack.back().level = tree->slvr().get_scope_level(); bool was_sat = true; int update_failures = 0; + int total_updates = 0; while (true) { @@ -2165,7 +2240,7 @@ namespace Duality { reporter->Depth(stack.size()); // res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop - check_result foo = tree->Check(top); + check_result foo = Check(); res = foo == unsat ? l_false : l_true; if (res == l_false) { @@ -2193,11 +2268,18 @@ namespace Duality { throw DoRestart(); } #endif - if(RecordUpdate(node)) + if(RecordUpdate(node)){ update_count++; + total_updates++; + } else heuristic->Update(node->map); // make it less likely to expand this node in future } +#if 1 + if(duality->EnableRestarts) + if(total_updates >= restart_interval) + throw DoRestart(); +#endif if(update_count == 0){ if(was_sat){ update_failures++; @@ -2243,6 +2325,10 @@ namespace Duality { tree->Push(); std::vector &expansions = stack.back().expansions; #ifndef NO_DECISIONS +#if 0 + if(expansions.size() > 0) + tree->GreedyReduceNodes(expansions[0]->Outgoing->Children); // try to reduce number of children +#endif for(unsigned i = 0; i < expansions.size(); i++){ tree->FixCurrentState(expansions[i]->Outgoing); } @@ -2262,15 +2348,42 @@ namespace Duality { if(ExpandSomeNodes(false,expand_max)) continue; tree->Pop(1); + node_order.clear(); while(stack.size() > 1){ tree->Pop(1); + std::vector &expansions = stack.back().expansions; + for(unsigned i = 0; i < expansions.size(); i++) + node_order.push_back(expansions[i]); stack.pop_back(); } +#if 0 + Reduce(); +#endif return true; } } } + std::vector node_order; + + void Reduce(){ + tree->Push(); + // tree->AssertNode(top); // assert the negation of the top-level spec + for(int i = node_order.size()-1; i >= 0; --i){ + Edge *edge = node_order[i]->Outgoing; + if(edge){ + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *ch = edge->Children[j]; + if(!ch->Outgoing) + ch->Annotation.SetEmpty(); + } + tree->AssertEdge(edge,0,true); + } + } + tree->GreedyReduceNodes(node_order); // try to reduce the counterexample size + tree->Pop(1); + } + void PopLevel(){ std::vector &expansions = stack.back().expansions; tree->Pop(1); @@ -2869,17 +2982,7 @@ namespace Duality { return name; } - virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority, bool best_only){ - if(!high_priority || !old_cex.get_tree()){ - Heuristic::ChooseExpand(choices,best,false); - return; - } - // first, try to match the derivatino tree nodes to the old cex - std::set matched, unmatched; - for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it){ - Node *node = (*it); - if(cex_map.empty()) - cex_map[node] = old_cex.get_root(); // match the root nodes + Node *MatchNode(Node *node){ if(cex_map.find(node) == cex_map.end()){ // try to match an unmatched node Node *parent = node->Incoming[0]->Parent; // assumes we are a tree! if(cex_map.find(parent) == cex_map.end()) @@ -2902,7 +3005,30 @@ namespace Duality { cex_map[chs[i]] = 0; } matching_done: - Node *old_node = cex_map[node]; + return cex_map[node]; + } + + int UseNode(Node *node){ + if (!old_cex.get_tree()) + return 0; + Node *old_node = MatchNode(node); + if(!old_node) + return 0; + return old_cex.get_tree()->Empty(old_node) ? -1 : 1; + } + + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority, bool best_only){ + if(cex_map.empty()) + cex_map[*(choices.begin())] = old_cex.get_root(); // match the root nodes + if(!high_priority || !old_cex.get_tree()){ + Heuristic::ChooseExpand(choices,best,false); + return; + } + // first, try to match the derivatino tree nodes to the old cex + std::set matched, unmatched; + for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it){ + Node *node = (*it); + Node *old_node = MatchNode(node); if(!old_node) unmatched.insert(node); else if(old_cex.get_tree()->Empty(old_node)) @@ -3177,8 +3303,233 @@ namespace Duality { }; + + class DualityDepthBounded : public Solver { + + Duality *duality; + context &ctx; // Z3 context + solver &slvr; // Z3 solver + + public: + DualityDepthBounded(RPFP *_rpfp) : + ctx(_rpfp->ctx), + slvr(_rpfp->slvr()){ + rpfp = _rpfp; + DepthBoundRPFP(); + duality = alloc(Duality,drpfp); + } + + ~DualityDepthBounded(){ + dealloc(duality); + delete drpfp; + } + + bool Solve(){ + int depth_bound = 10; + bool res; + SetMaxDepthRPFP(depth_bound); + duality->PreSolve(); + while(true){ + res = duality->SolveMain(); + if(!res || GetSolution()) + break; + depth_bound++; + SetMaxDepthRPFP(depth_bound); + res = duality->RecheckBounds(); + if(!res) + break; + } + duality->PostSolve(); + if(!res) + ConvertCex(); + return res; + } + + Counterexample &GetCounterexample(){ + return cex; + } + + bool SetOption(const std::string &option, const std::string &value){ + return duality->SetOption(option,value); + } + + virtual void LearnFrom(Solver *old_solver){ + DualityDepthBounded *old = dynamic_cast(old_solver); + if(old){ + duality->LearnFrom(old->duality); + } + } + + bool IsResultRecursionBounded(){ + return duality->IsResultRecursionBounded(); + } + + void Cancel(){ + duality->Cancel(); + } + + typedef RPFP::Node Node; + typedef RPFP::Edge Edge; + RPFP *rpfp, *drpfp; + hash_map db_map, db_rev_map; + hash_map db_edge_rev_map; + std::vector db_saved_bounds; + Counterexample cex; + + expr AddParamToRels(hash_map &memo, hash_map &rmap, const expr &p, const expr &t) { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + expr &res = bar.first->second; + if(!bar.second) return res; + + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(AddParamToRels(memo, rmap, p, t.arg(i))); + hash_map::iterator rit = rmap.find(f); + if(rit != rmap.end()){ + args.push_back(p); + res = (rit->second)(args); + res = ctx.make(And,res,ctx.make(Geq,p,ctx.int_val(0))); + } + else + res = f(args); + } + else if (t.is_quantifier()) + { + expr body = AddParamToRels(memo, rmap, p, t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + + void DepthBoundRPFP(){ + drpfp = new RPFP(rpfp->ls); + expr dvar = ctx.int_const("@depth"); + expr dmax = ctx.int_const("@depth_max"); + for(unsigned i = 0; i < rpfp->nodes.size(); i++){ + Node *node = rpfp->nodes[i]; + std::vector arg_sorts; + const std::vector ¶ms = node->Annotation.IndParams; + for(unsigned j = 0; j < params.size(); j++) + arg_sorts.push_back(params[j].get_sort()); + arg_sorts.push_back(ctx.int_sort()); + std::string new_name = std::string("@db@") + node->Name.name().str(); + func_decl f = ctx.function(new_name.c_str(),arg_sorts.size(), &arg_sorts[0],ctx.bool_sort()); + std::vector args = params; + args.push_back(dvar); + expr pat = f(args); + Node *dnode = drpfp->CreateNode(pat); + db_map[node] = dnode; + db_rev_map[dnode] = node; + expr bound_fmla = node->Bound.Formula; + if(!eq(bound_fmla,ctx.bool_val(true))){ + bound_fmla = implies(dvar == dmax,bound_fmla); + dnode->Bound.Formula = bound_fmla; + } + db_saved_bounds.push_back(bound_fmla); + // dnode->Annotation.Formula = ctx.make(And,node->Annotation.Formula,ctx.make(Geq,dvar,ctx.int_val(0))); + } + for(unsigned i = 0; i < rpfp->edges.size(); i++){ + Edge *edge = rpfp->edges[i]; + std::vector new_children; + std::vector new_relparams; + hash_map rmap; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *ch = edge->Children[j]; + Node *nch = db_map[ch]; + func_decl f = nch->Name; + func_decl sf = drpfp->NumberPred(f,j); + new_children.push_back(nch); + new_relparams.push_back(sf); + rmap[edge->F.RelParams[j]] = sf; + } + std::vector new_indparams = edge->F.IndParams; + new_indparams.push_back(dvar); + hash_map memo; + expr new_fmla = AddParamToRels(memo,rmap,ctx.make(Sub,dvar,ctx.int_val(1)),edge->F.Formula); + RPFP::Transformer new_t = drpfp->CreateTransformer(new_relparams,new_indparams,new_fmla); + Node *new_parent = db_map[edge->Parent]; + db_edge_rev_map[drpfp->CreateEdge(new_parent,new_t,new_children)] = edge; + } + } + + void SetMaxDepthRPFP(int depth){ + hash_map subst; + expr dmax = ctx.int_const("@depth_max"); + subst[dmax] = ctx.int_val(depth); + for(unsigned i = 0; i < drpfp->nodes.size(); i++){ + Node *node = drpfp->nodes[i]; + expr fmla = db_saved_bounds[i]; + fmla = drpfp->SubstRec(subst,fmla); + node->Bound.Formula = fmla; + } + } + + void ConvertCex(){ + cex.clear(); + RPFP *tree = new RPFP(rpfp->ls); + Node *root; + Counterexample &dctx = duality->GetCounterexample(); + hash_map ctx_node_map; + for(unsigned i = 0; i < dctx.get_tree()->nodes.size(); i++){ + Node *dnode = dctx.get_tree()->nodes[i]; + Node *onode = db_rev_map[dnode->map->map]; + Node *node = tree->CloneNode(onode); + node->number = dnode->number; // numbers have to match for model to make sense + ctx_node_map[dnode] = node; + if(dnode == dctx.get_root()) + root = node; + } + for(unsigned i = 0; i < dctx.get_tree()->edges.size(); i++){ + Edge *dedge = dctx.get_tree()->edges[i]; + Edge *oedge = db_edge_rev_map[dedge->map]; + Node *parent = ctx_node_map[dedge->Parent]; + std::vector chs; + for(unsigned j = 0; j < dedge->Children.size(); j++) + chs.push_back(ctx_node_map[dedge->Children[j]]); + Edge *edge = tree->CreateEdge(parent,oedge->F,chs); + edge->number = dedge->number; // numbers have to match for model to make sense + edge->map = oedge; + } + tree->dualModel = dctx.get_tree()->dualModel; + cex.set(tree,root); + } + + bool GetSolution(){ + for(unsigned i = 0; i < rpfp->nodes.size(); i++) + if(!drpfp->nodes[i]->Annotation.SubsetEq(rpfp->nodes[i]->Bound)) + return false; + expr dvar = ctx.int_const("@depth"); + hash_map subst; + subst[dvar] = ctx.int_val(INT_MAX); + for(unsigned i = 0; i < rpfp->nodes.size(); i++){ + expr fmla = drpfp->nodes[i]->Annotation.Formula; + fmla = drpfp->SubstRec(subst,fmla); + fmla = fmla.simplify(); + rpfp->nodes[i]->Annotation.Formula = fmla; + } + return true; + } + + void UndoDepthBoundRPFP(){ +#if 0 + if(cex.get_tree()){ + // here, need to map the cex back... + } + // also need to map the proof back, but we don't... +#endif + } + }; + Solver *Solver::Create(const std::string &solver_class, RPFP *rpfp){ - Duality *s = alloc(Duality,rpfp); + // Solver *s = alloc(DualityDepthBounded,rpfp); + Solver *s = alloc(Duality,rpfp); return s; } diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 5bfbba6b2..832e3329e 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -78,6 +78,7 @@ def_module_params('fixedpoint', ('batch_expand', BOOL, False, 'DUALITY: use batch expansion'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), ('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'), + ('enable_restarts', BOOL, False, 'DUALITY: enable restarts'), )) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 08c57b05e..55f6c3747 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -281,6 +281,7 @@ 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()); + rs->SetOption("enable_restarts",m_ctx.get_params().enable_restarts() ? "1" : "0"); #if 0 if(rb != UINT_MAX){ std::ostringstream os; os << rb; From c5f17df310405b2f7718f1eaa93242cfa25e54de Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 1 Oct 2014 18:15:33 -0700 Subject: [PATCH 05/12] fixing an assert caused by previous change in theory_array_base.cpp --- src/smt/theory_array_base.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 6325a2a99..b2c17b4e0 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -433,14 +433,16 @@ namespace smt { enode * n = get_enode(i); if (ctx.is_relevant(n)) { enode * r = n->get_root(); - if (!r->is_marked() && is_array_sort(r) && ctx.is_shared(r)) { - TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); - theory_var r_th_var = r->get_th_var(get_id()); - SASSERT(r_th_var != null_theory_var); - result.push_back(r_th_var); + if (!r->is_marked()){ + if(is_array_sort(r) && ctx.is_shared(r)) { + TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); + theory_var r_th_var = r->get_th_var(get_id()); + SASSERT(r_th_var != null_theory_var); + result.push_back(r_th_var); + } + r->set_mark(); + to_unmark.push_back(r); } - r->set_mark(); - to_unmark.push_back(r); } } unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); From d54d758f45b745ec129db375364d5a00eef23ce5 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 1 Oct 2014 18:16:21 -0700 Subject: [PATCH 06/12] getting duality to recover from incompleteness-related failures by restarting --- src/duality/duality_profiling.cpp | 10 ++++++++++ src/duality/duality_solver.cpp | 25 ++++++++++++++++++------- 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp index d5dac0811..5bcda972a 100755 --- a/src/duality/duality_profiling.cpp +++ b/src/duality/duality_profiling.cpp @@ -125,8 +125,18 @@ namespace Duality { void timer_stop(const char *name){ if(current->name != name || !current->parent){ +#if 0 std::cerr << "imbalanced timer_start and timer_stop"; exit(1); +#endif + // in case we lost a timer stop due to an exception + while(current->name != name && current->parent) + current = current->parent; + if(current->parent){ + current->time += (current_time() - current->start_time); + current = current->parent; + } + return; } current->time += (current_time() - current->start_time); current = current->parent; diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 49e591be2..bbd1ebe0a 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -2252,22 +2252,27 @@ namespace Duality { int update_count = 0; for(unsigned i = 0; i < expansions.size(); i++){ Node *node = expansions[i]; - tree->SolveSingleNode(top,node); -#ifdef NO_GENERALIZE - node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); -#else try { + tree->SolveSingleNode(top,node); +#ifdef NO_GENERALIZE + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); +#else if(expansions.size() == 1 && NodeTooComplicated(node)) SimplifyNode(node); else node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); Generalize(node); +#endif } catch(const RPFP::Bad &){ // bad interpolants can get us here throw DoRestart(); } -#endif + catch(char const *msg){ + // bad interpolants can get us here + reporter->Message(std::string("interpolation failure:") + msg); + throw DoRestart(); + } if(RecordUpdate(node)){ update_count++; total_updates++; @@ -2283,8 +2288,14 @@ namespace Duality { if(update_count == 0){ if(was_sat){ update_failures++; - if(update_failures > 10) - throw Incompleteness(); + if(update_failures > 10){ + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + node->map->Annotation.SetFull(); + reporter->Message("incompleteness: cleared annotation"); + } + throw DoRestart(); + } } reporter->Message("backtracked without learning"); } From 16445569f1a6cfd3fa04c7227d3d724dd16947c7 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 4 Oct 2014 16:31:01 -0700 Subject: [PATCH 07/12] fix for quantifier abstraction --- src/muz/transforms/dl_transforms.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_transforms.cpp b/src/muz/transforms/dl_transforms.cpp index 2cf48d46b..9a4667f2c 100644 --- a/src/muz/transforms/dl_transforms.cpp +++ b/src/muz/transforms/dl_transforms.cpp @@ -71,7 +71,8 @@ namespace datalog { transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, ctx, 32000)); transf.register_plugin(alloc(datalog::mk_bit_blast, ctx, 35000)); - transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 36000)); + if (!ctx.get_params().quantify_arrays()) + transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 36000)); transf.register_plugin(alloc(datalog::mk_karr_invariants, ctx, 36010)); if (ctx.get_params().magic()) { transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020)); From e8985ff33dcb2d9d2705d632468443abb811ee99 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 4 Oct 2014 17:17:33 -0700 Subject: [PATCH 08/12] working on transforms in duality --- src/muz/duality/duality_dl_interface.cpp | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 55f6c3747..c7fa0a08f 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -157,7 +157,27 @@ lbool dl_interface::query(::expr * query) { svector< ::symbol> names; vector bounds; // m_ctx.get_rules_as_formulas(rules, names); - m_ctx.get_raw_rule_formulas(rules, names, bounds); + + expr_ref query_ref(m_ctx.get_manager()); + if(****){ + m_ctx.flush_add_rules(); + datalog::rule_manager& rm = m_ctx.get_rule_manager(); + rm.mk_query(query, m_ctx.get_rules()); + apply_default_transformation(m_ctx); + rule_set &rs = m_ctx.get_rules(); + if(m_ctx.get_rules().get_output_predicates().empty()) + query_ref = m_ctx.get_manager().mk_true(); + else { + query_pred = m_ctx.get_rules().get_output_predicate(); + func_decl_ref query_pred(m_ctx.get_manager()); + query_pred = m_ctx.get_rules().get_output_predicate(); + ptr_vector sorts; + unsi + + } + } + else + m_ctx.get_raw_rule_formulas(rules, names, bounds); // get all the rules as clauses std::vector &clauses = _d->clauses; From ec48f6d129f856f216fc1885593e8d77ab6c89e8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 4 Oct 2014 19:07:14 -0700 Subject: [PATCH 09/12] working on transforms for duality --- src/muz/base/dl_context.cpp | 3 +++ src/muz/duality/duality_dl_interface.cpp | 33 +++++++++++++++++------- 2 files changed, 26 insertions(+), 10 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 80af7eeb0..ca7277d07 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -985,6 +985,9 @@ namespace datalog { flush_add_rules(); break; case DUALITY_ENGINE: + // this lets us use duality with SAS 2013 abstraction + if(quantify_arrays()) + flush_add_rules(); break; default: UNREACHABLE(); diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index c7fa0a08f..7666b39cf 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -37,6 +37,7 @@ Revision History: #include "fixedpoint_params.hpp" #include "used_vars.h" #include "func_decl_dependencies.h" +#include "dl_transforms.h" // template class symbol_table; @@ -158,22 +159,34 @@ lbool dl_interface::query(::expr * query) { vector bounds; // m_ctx.get_rules_as_formulas(rules, names); + + // If using SAS 2013 abstractiion, we need to perform some transforms expr_ref query_ref(m_ctx.get_manager()); - if(****){ - m_ctx.flush_add_rules(); + if(m_ctx.quantify_arrays()){ datalog::rule_manager& rm = m_ctx.get_rule_manager(); rm.mk_query(query, m_ctx.get_rules()); apply_default_transformation(m_ctx); - rule_set &rs = m_ctx.get_rules(); + datalog::rule_set &rs = m_ctx.get_rules(); if(m_ctx.get_rules().get_output_predicates().empty()) - query_ref = m_ctx.get_manager().mk_true(); + query_ref = m_ctx.get_manager().mk_false(); else { - query_pred = m_ctx.get_rules().get_output_predicate(); - func_decl_ref query_pred(m_ctx.get_manager()); - query_pred = m_ctx.get_rules().get_output_predicate(); - ptr_vector sorts; - unsi - + func_decl_ref query_pred(m_ctx.get_manager()); + query_pred = m_ctx.get_rules().get_output_predicate(); + ptr_vector sorts; + unsigned nargs = query_pred.get()->get_arity(); + expr_ref_vector vars(m_ctx.get_manager()); + for(unsigned i = 0; i < nargs; i++){ + ::sort *s = query_pred.get()->get_domain(i); + vars.push_back(m_ctx.get_manager().mk_var(nargs-1-i,s)); + } + query_ref = m_ctx.get_manager().mk_app(query_pred.get(),nargs,vars.c_ptr()); + query = query_ref.get(); + } + unsigned nrules = rs.get_num_rules(); + for(unsigned i = 0; i < nrules; i++){ + expr_ref f(m_ctx.get_manager()); + rs.get_rule(i)->to_formula(f); + rules.push_back(f); } } else From bbdc8b33e0ab4153b2f3782f01025cf355a080df Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 8 Oct 2014 13:56:46 -0700 Subject: [PATCH 10/12] prevent creating some useless solvers in duality --- src/duality/duality_solver.cpp | 29 ++++++++++++++++-------- src/muz/duality/duality_dl_interface.cpp | 21 +---------------- 2 files changed, 21 insertions(+), 29 deletions(-) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index bbd1ebe0a..69759f9bb 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -802,6 +802,15 @@ namespace Duality { annot.Simplify(); } + bool NodeSolutionFromIndSetFull(Node *node){ + std::vector &insts = insts_of_node[node]; + for(unsigned j = 0; j < insts.size(); j++) + if(indset->Contains(insts[j])) + if(insts[j]->Annotation.IsFull()) + return true; + return false; + } + bool recursionBounded; /** See if the solution might be bounded. */ @@ -1453,16 +1462,18 @@ namespace Duality { slvr.pop(1); delete checker; #else - RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/); - gen_cands_rpfp->Push(); - Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp); - if(gen_cands_rpfp->Check(root) != unsat){ - Candidate candidate; - ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate); - reporter->InductionFailure(edge,candidate.Children); - candidates.push_back(candidate); + if(!NodeSolutionFromIndSetFull(edge->Parent)){ + RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/); + gen_cands_rpfp->Push(); + Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp); + if(gen_cands_rpfp->Check(root) != unsat){ + Candidate candidate; + ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate); + reporter->InductionFailure(edge,candidate.Children); + candidates.push_back(candidate); + } + gen_cands_rpfp->Pop(1); } - gen_cands_rpfp->Pop(1); #endif } updated_nodes.clear(); diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index c7fa0a08f..9a6d0c633 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -158,26 +158,7 @@ lbool dl_interface::query(::expr * query) { vector bounds; // m_ctx.get_rules_as_formulas(rules, names); - expr_ref query_ref(m_ctx.get_manager()); - if(****){ - m_ctx.flush_add_rules(); - datalog::rule_manager& rm = m_ctx.get_rule_manager(); - rm.mk_query(query, m_ctx.get_rules()); - apply_default_transformation(m_ctx); - rule_set &rs = m_ctx.get_rules(); - if(m_ctx.get_rules().get_output_predicates().empty()) - query_ref = m_ctx.get_manager().mk_true(); - else { - query_pred = m_ctx.get_rules().get_output_predicate(); - func_decl_ref query_pred(m_ctx.get_manager()); - query_pred = m_ctx.get_rules().get_output_predicate(); - ptr_vector sorts; - unsi - - } - } - else - m_ctx.get_raw_rule_formulas(rules, names, bounds); + m_ctx.get_raw_rule_formulas(rules, names, bounds); // get all the rules as clauses std::vector &clauses = _d->clauses; From 6e18f44d991344fc444b21c13e4c2233334ab6d8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 22 Oct 2014 10:42:23 -0700 Subject: [PATCH 11/12] fixed error check in read_interpolation_problem --- src/api/api_interp.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index dbf68da38..63ecc6c24 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -617,7 +617,7 @@ extern "C" { } for (unsigned j = 0; j < num - 1; j++) - if (read_parents[j] == SHRT_MIN){ + if (read_parents[j] == SHRT_MAX){ read_error << "formula " << j + 1 << ": unreferenced"; goto fail; } @@ -717,4 +717,4 @@ Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx, __in unsigned incremental, __in unsigned num_theory, __in_ecount(num_theory) Z3_ast *theory); -#endif \ No newline at end of file +#endif From 5454e389355f3a98e82ccd03815cf058458190fd Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 22 Oct 2014 10:43:04 -0700 Subject: [PATCH 12/12] replaced check_interpolants option with interp.check --- src/cmd_context/basic_cmds.cpp | 6 ------ src/cmd_context/cmd_context.cpp | 8 -------- src/cmd_context/cmd_context.h | 2 -- src/cmd_context/context_params.cpp | 5 ----- src/cmd_context/context_params.h | 1 - src/cmd_context/interpolant_cmds.cpp | 2 +- src/interp/iz3params.pyg | 1 + 7 files changed, 2 insertions(+), 23 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 836ade9ce..a80c5bc6c 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -241,7 +241,6 @@ protected: symbol m_produce_models; symbol m_produce_assignments; symbol m_produce_interpolants; - symbol m_check_interpolants; symbol m_regular_output_channel; symbol m_diagnostic_output_channel; symbol m_random_seed; @@ -256,7 +255,6 @@ protected: s == m_print_success || s == m_print_warning || s == m_expand_definitions || s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants || - s == m_check_interpolants || s == m_regular_output_channel || s == m_diagnostic_output_channel || s == m_random_seed || s == m_verbosity || s == m_global_decls; } @@ -275,7 +273,6 @@ public: m_produce_models(":produce-models"), m_produce_assignments(":produce-assignments"), m_produce_interpolants(":produce-interpolants"), - m_check_interpolants(":check-interpolants"), m_regular_output_channel(":regular-output-channel"), m_diagnostic_output_channel(":diagnostic-output-channel"), m_random_seed(":random-seed"), @@ -347,9 +344,6 @@ class set_option_cmd : public set_get_option_cmd { check_not_initialized(ctx, m_produce_interpolants); ctx.set_produce_interpolants(to_bool(value)); } - else if (m_option == m_check_interpolants) { - ctx.set_check_interpolants(to_bool(value)); - } else if (m_option == m_produce_unsat_cores) { check_not_initialized(ctx, m_produce_unsat_cores); ctx.set_produce_unsat_cores(to_bool(value)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index ce2838aba..731608524 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -397,10 +397,6 @@ void cmd_context::set_produce_interpolants(bool f) { // set_solver_factory(mk_smt_solver_factory()); } -void cmd_context::set_check_interpolants(bool f) { - m_params.m_check_interpolants = f; -} - bool cmd_context::produce_models() const { return m_params.m_model; } @@ -414,10 +410,6 @@ bool cmd_context::produce_interpolants() const { return m_params.m_proof; } -bool cmd_context::check_interpolants() const { - return m_params.m_check_interpolants; -} - bool cmd_context::produce_unsat_cores() const { return m_params.m_unsat_core; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index e34975183..8ad07e8cc 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -279,7 +279,6 @@ public: bool produce_models() const; bool produce_proofs() const; bool produce_interpolants() const; - bool check_interpolants() const; bool produce_unsat_cores() const; bool well_sorted_check_enabled() const; bool validate_model_enabled() const; @@ -287,7 +286,6 @@ public: void set_produce_unsat_cores(bool flag); void set_produce_proofs(bool flag); void set_produce_interpolants(bool flag); - void set_check_interpolants(bool flag); bool produce_assignments() const { return m_produce_assignments; } void set_produce_assignments(bool flag) { m_produce_assignments = flag; } void set_status(status st) { m_status = st; } diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 254a1d931..f87c8d264 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -61,9 +61,6 @@ void context_params::set(char const * param, char const * value) { else if (p == "proof") { set_bool(m_proof, param, value); } - else if (p == "check_interpolants") { - set_bool(m_check_interpolants, param, value); - } else if (p == "model") { set_bool(m_model, param, value); } @@ -105,7 +102,6 @@ void context_params::updt_params(params_ref const & p) { m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true)); m_auto_config = p.get_bool("auto_config", true); m_proof = p.get_bool("proof", false); - m_check_interpolants = p.get_bool("check_interpolants", false); m_model = p.get_bool("model", true); m_model_validate = p.get_bool("model_validate", false); m_trace = p.get_bool("trace", false); @@ -120,7 +116,6 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("well_sorted_check", CPK_BOOL, "type checker", "true"); d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); - d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false"); d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false"); d.insert("trace", CPK_BOOL, "trace generation for VCC", "false"); d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log"); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index e26fd3fe5..506e559db 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -30,7 +30,6 @@ public: bool m_auto_config; bool m_proof; bool m_interpolants; - bool m_check_interpolants; bool m_debug_ref_count; bool m_trace; std::string m_trace_file_name; diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index cb83b52f6..42646a99d 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -65,7 +65,7 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx, s.cleanup(); // verify, for the paranoid... - if(check || ctx.check_interpolants()){ + if(check || interp_params(m_params).check()){ std::ostringstream err; ast_manager &_m = ctx.m(); diff --git a/src/interp/iz3params.pyg b/src/interp/iz3params.pyg index 5b574c859..3116a18db 100644 --- a/src/interp/iz3params.pyg +++ b/src/interp/iz3params.pyg @@ -2,4 +2,5 @@ def_module_params('interp', description='interpolation parameters', export=True, params=(('profile', BOOL, False, '(INTERP) profile interpolation'), + ('check', BOOL, False, '(INTERP) check interpolants'), ))