From 08d892bbdbf1f40d0ebca0d7e9c7479b75b1bd37 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 27 Feb 2014 17:21:47 -0800 Subject: [PATCH 1/5] interpolation fixes --- src/duality/duality.h | 2 ++ src/duality/duality_rpfp.cpp | 19 ++++++++++++ src/duality/duality_solver.cpp | 9 ++++-- src/interp/iz3proof_itp.cpp | 55 ++++++++++++++++++++++------------ 4 files changed, 64 insertions(+), 21 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index e1d058f10..12ba21516 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -82,6 +82,8 @@ namespace Duality { Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); + Term CloneQuantAndSimp(const expr &t, const expr &body); + Term RemoveRedundancy(const Term &t); Term IneqToEq(const Term &t); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 5751fa890..e09278dd4 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -523,6 +523,25 @@ namespace Duality { return foo; } + Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){ + if(t.is_quantifier_forall() && body.is_app() && body.decl().get_decl_kind() == And){ + int nargs = body.num_args(); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = CloneQuantAndSimp(t, body.arg(i)); + return ctx.make(And,args); + } + if(!t.is_quantifier_forall() && body.is_app() && body.decl().get_decl_kind() == Or){ + int nargs = body.num_args(); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = CloneQuantAndSimp(t, body.arg(i)); + return ctx.make(Or,args); + } + return clone_quantifier(t,body); + } + + Z3User::Term Z3User::SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val){ std::pair foo(t,expr(ctx)); std::pair::iterator, bool> bar = memo.insert(foo); diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 1c2f2c927..c7eec7e9f 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1916,6 +1916,7 @@ namespace Duality { stack.back().level = tree->slvr().get_scope_level(); bool was_sat = true; + int update_failures = 0; while (true) { @@ -1954,10 +1955,14 @@ namespace Duality { heuristic->Update(node->map); // make it less likely to expand this node in future } if(update_count == 0){ - if(was_sat) - throw Incompleteness(); + if(was_sat){ + update_failures++; + if(update_failures > 10) + throw Incompleteness(); + } reporter->Message("backtracked without learning"); } + else update_failures = 0; } tree->ComputeProofCore(); // need to compute the proof core before popping solver bool propagated = false; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 1eb4fcc84..a1a332005 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -369,11 +369,17 @@ class iz3proof_itp_impl : public iz3proof_itp { } default: { - symb s = sym(itp2); - if(s == sforall || s == sexists) - res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1))); - else + opr o = op(itp2); + if(o == Uninterpreted){ + symb s = sym(itp2); + if(s == sforall || s == sexists) + res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1))); + else + res = itp2; + } + else { res = itp2; + } } } } @@ -405,11 +411,17 @@ class iz3proof_itp_impl : public iz3proof_itp { } default: { - symb s = sym(itp1); - if(s == sforall || s == sexists) - res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2)); - else + opr o = op(itp1); + if(o == Uninterpreted){ + symb s = sym(itp1); + if(s == sforall || s == sexists) + res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2)); + else + res = itp1; + } + else { res = itp1; + } } } } @@ -464,18 +476,20 @@ class iz3proof_itp_impl : public iz3proof_itp { std::pair::iterator,bool> bar = subst_memo.insert(foo); ast &res = bar.first->second; if(bar.second){ - symb g = sym(e); - if(g == rotate_sum){ - if(var == get_placeholder(arg(e,0))){ - res = e; + if(op(e) == Uninterpreted){ + symb g = sym(e); + if(g == rotate_sum){ + if(var == get_placeholder(arg(e,0))){ + res = e; + } + else + res = make(rotate_sum,arg(e,0),subst_term_and_simp_rec(var,t,arg(e,1))); + return res; + } + if(g == concat){ + res = e; + return res; } - else - res = make(rotate_sum,arg(e,0),subst_term_and_simp_rec(var,t,arg(e,1))); - return res; - } - if(g == concat){ - res = e; - return res; } int nargs = num_args(e); std::vector args(nargs); @@ -794,6 +808,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return simplify_sum(args); } + ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){ if(pl == arg(pf,1)){ ast cond = mk_true(); @@ -1036,6 +1051,8 @@ class iz3proof_itp_impl : public iz3proof_itp { ast mc = z3_simplify(chain_side_proves(LitA,pref)); Aproves = my_and(Aproves,mc); } + if(is_true(nc)) + return itp; return make_normal(itp,nc); } From 19dbd02e1344c22552da196e52e9d0b0ba413d0a Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 28 Feb 2014 10:38:35 -0800 Subject: [PATCH 2/5] interpolation fix --- src/interp/iz3proof_itp.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index a1a332005..e66bda5f3 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2635,6 +2635,11 @@ class iz3proof_itp_impl : public iz3proof_itp { } hash_map::iterator it = localization_map.find(e); + + if(it != localization_map.end() && is_bool_type(get_type(e)) + && !pv->ranges_intersect(pv->ast_scope(it->second),rng)) + it = localization_map.end(); // prevent quantifiers over booleans + if(it != localization_map.end()){ pf = localization_pf_map[e]; e = it->second; From 83a774ac7934f40940c7f23424fced2c1a0ba590 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 4 Mar 2014 18:38:08 -0800 Subject: [PATCH 3/5] duality fix plus mbqi option --- src/duality/duality_rpfp.cpp | 21 ++++++++++++++++++++- src/duality/duality_wrapper.cpp | 3 ++- src/duality/duality_wrapper.h | 1 + src/muz/base/fixedpoint_params.pyg | 1 + src/muz/duality/duality_dl_interface.cpp | 1 + 5 files changed, 25 insertions(+), 2 deletions(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index e09278dd4..550f94f2d 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2847,7 +2847,12 @@ namespace Duality { } void RPFP::InterpolateByCases(Node *root, Node *node){ + timer_start("InterpolateByCases"); bool axioms_added = false; + hash_set axioms_needed; + const std::vector &theory = ls->get_axioms(); + for(unsigned i = 0; i < theory.size(); i++) + axioms_needed.insert(theory[i]); aux_solver.push(); AddEdgeToSolver(node->Outgoing); node->Annotation.SetEmpty(); @@ -2869,7 +2874,17 @@ namespace Duality { check_result foo = Check(root); if(foo != unsat) throw "should be unsat"; - AddToProofCore(*core); + + std::vector assumps, axioms_to_add; + slvr().get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++){ + (*core).insert(assumps[i]); + if(axioms_needed.find(assumps[i]) != axioms_needed.end()){ + axioms_to_add.push_back(assumps[i]); + axioms_needed.erase(assumps[i]); + } + } + // AddToProofCore(*core); Transformer old_annot = node->Annotation; SolveSingleNode(root,node); @@ -2882,6 +2897,9 @@ namespace Duality { node->Annotation.Formula = node->Annotation.Formula.simplify(); } + for(unsigned i = 0; i < axioms_to_add.size(); i++) + aux_solver.add(axioms_to_add[i]); + if(node->Annotation.IsEmpty()){ if(!axioms_added){ // add the axioms in the off chance they are useful @@ -2906,6 +2924,7 @@ namespace Duality { delete proof_core; // shouldn't happen proof_core = core; aux_solver.pop(1); + timer_stop("InterpolateByCases"); } void RPFP::Generalize(Node *root, Node *node){ diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index cf2c803cb..345fef562 100755 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -43,7 +43,8 @@ namespace Duality { if(models) p.set_bool("model", true); p.set_bool("unsat_core", true); - p.set_bool("mbqi",true); + bool mbqi = c.get_config().get().get_bool("mbqi",true); + p.set_bool("mbqi",mbqi); // just to test p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants if(true || extensional) diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 2b0045023..febc3f1f1 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -182,6 +182,7 @@ namespace Duality { void set(char const * param, char const * value) { m_config.set(param,value); } void set(char const * param, bool value) { m_config.set(param,value); } void set(char const * param, int value) { m_config.set(param,value); } + config &get_config() {return m_config;} symbol str_symbol(char const * s); symbol int_symbol(int n); diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index e09e1307b..5eec77f39 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -74,6 +74,7 @@ def_module_params('fixedpoint', ('stratified_inlining', BOOL, False, 'DUALITY: Use stratified inlining'), ('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'), ('profile', BOOL, False, 'DUALITY: profile run time'), + ('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), )) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 248aca163..e7c7976f6 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -141,6 +141,7 @@ lbool dl_interface::query(::expr * query) { // make a new problem and solver _d = alloc(duality_data,m_ctx.get_manager()); + _d->ctx.set("mbqi",m_ctx.get_params().mbqi()); _d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx); _d->rpfp = alloc(RPFP,_d->ls); From 180f55bbdaaec6f2eee07c6c973cef2af2558add Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 11 Mar 2014 18:20:42 -0700 Subject: [PATCH 4/5] adding support for non-extensional arrays in duality --- src/duality/duality.h | 15 +- src/duality/duality_rpfp.cpp | 183 ++++++++++++++++++----- src/duality/duality_solver.cpp | 22 ++- src/duality/duality_wrapper.cpp | 17 ++- src/duality/duality_wrapper.h | 3 + src/muz/base/fixedpoint_params.pyg | 1 + src/muz/duality/duality_dl_interface.cpp | 1 + 7 files changed, 196 insertions(+), 46 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 12ba21516..137279899 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -31,6 +31,8 @@ using namespace stl_ext; namespace Duality { + class implicant_solver; + /* Generic operations on Z3 formulas */ struct Z3User { @@ -104,6 +106,9 @@ namespace Duality { FuncDecl RenumberPred(const FuncDecl &f, int n); + Term ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming); + + protected: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); @@ -602,6 +607,8 @@ protected: void FixCurrentState(Edge *root); void FixCurrentStateFull(Edge *edge, const expr &extra); + + void FixCurrentStateFull(Edge *edge, const std::vector &assumps, const hash_map &renaming); /** Declare a constant in the background theory. */ @@ -944,10 +951,12 @@ protected: Term UnderapproxFormula(const Term &f, hash_set &dont_cares); void ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, - hash_set &done, hash_set &dont_cares); + hash_set &done, hash_set &dont_cares, bool extensional = true); - Term UnderapproxFullFormula(const Term &f, hash_set &dont_cares); + public: + Term UnderapproxFullFormula(const Term &f, bool extensional = true); + protected: Term ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants); hash_map resolve_ite_memo; @@ -988,6 +997,8 @@ protected: void AddEdgeToSolver(Edge *edge); + void AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge); + void AddToProofCore(hash_set &core); void GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 550f94f2d..2d871c324 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -410,6 +410,33 @@ namespace Duality { return res; } + Z3User::Term Z3User::ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &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(ExtractStores(memo, t.arg(i),cnstrs,renaming)); + res = f(args.size(),&args[0]); + if(f.get_decl_kind() == Store){ + func_decl fresh = ctx.fresh_func_decl("@arr", res.get_sort()); + expr y = fresh(); + expr equ = ctx.make(Equal,y,res); + cnstrs.push_back(equ); + renaming[y] = res; + res = y; + } + } + else res = t; + return res; + } + + bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ if(!(lit.is_quantifier() && IsClosedFormula(lit))){ if(!lit.is_app()) @@ -1851,7 +1878,7 @@ namespace Duality { } void RPFP::ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, - hash_set &done, hash_set &dont_cares){ + hash_set &done, hash_set &dont_cares, bool extensional){ if(done.find(f) != done.end()) return; /* already processed */ if(f.is_app()){ @@ -1859,7 +1886,7 @@ namespace Duality { decl_kind k = f.decl().get_decl_kind(); if(k == Implies || k == Iff || k == And || k == Or || k == Not){ for(int i = 0; i < nargs; i++) - ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares); + ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares, extensional); goto done; } } @@ -1867,6 +1894,15 @@ namespace Duality { if(dont_cares.find(f) == dont_cares.end()){ int b = SubtermTruth(memo,f); if(b != 0 && b != 1) goto done; + if(f.is_app() && f.decl().get_decl_kind() == Equal && f.arg(0).is_array()){ + if(b == 1 && !extensional){ + expr x = dualModel.eval(f.arg(0)); expr y = dualModel.eval(f.arg(1)); + if(!eq(x,y)) + b = 0; + } + if(b == 0) + goto done; + } expr bv = (b==1) ? f : !f; lits.push_back(bv); } @@ -1988,12 +2024,16 @@ namespace Duality { return conjoin(lits); } - RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set &dont_cares){ + RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, bool extensional){ + hash_set dont_cares; + resolve_ite_memo.clear(); + timer_start("UnderapproxFormula"); /* first compute truth values of subterms */ hash_map memo; hash_set done; std::vector lits; - ImplicantFullRed(memo,f,lits,done,dont_cares); + ImplicantFullRed(memo,f,lits,done,dont_cares, extensional); + timer_stop("UnderapproxFormula"); /* return conjunction of literals */ return conjoin(lits); } @@ -2538,22 +2578,6 @@ namespace Duality { ConstrainEdgeLocalized(edge,eu); } - void RPFP::FixCurrentStateFull(Edge *edge, const expr &extra){ - hash_set dont_cares; - resolve_ite_memo.clear(); - timer_start("UnderapproxFormula"); - Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual; - for(unsigned i = 0; i < edge->constraints.size(); i++) - dual = dual && edge->constraints[i]; - // dual = dual && extra; - Term eu = UnderapproxFullFormula(dual,dont_cares); - timer_stop("UnderapproxFormula"); - ConstrainEdgeLocalized(edge,eu); - } - - - - void RPFP::GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under){ if(memo[under].find(f) != memo[under].end()) return; @@ -2836,7 +2860,91 @@ namespace Duality { return ctx.make(And,lits); } - // set up edge constraint in aux solver + + /* This is a wrapper for a solver that is intended to compute + implicants from models. It works around a problem in Z3 with + models in the non-extensional array theory. It does this by + naming all of the store terms in a formula. That is, (store ...) + is replaced by "name" with an added constraint name = (store + ...). This allows us to determine from the model whether an array + equality is true or false (it is false if the two sides are + mapped to different function symbols, even if they have the same + contents). + */ + + struct implicant_solver { + RPFP *owner; + solver &aux_solver; + std::vector assumps, namings; + std::vector assump_stack, naming_stack; + hash_map renaming, renaming_memo; + + void add(const expr &e){ + expr t = e; + if(!aux_solver.extensional_array_theory()){ + unsigned i = namings.size(); + t = owner->ExtractStores(renaming_memo,t,namings,renaming); + for(; i < namings.size(); i++) + aux_solver.add(namings[i]); + } + assumps.push_back(t); + aux_solver.add(t); + } + + void push() { + assump_stack.push_back(assumps.size()); + naming_stack.push_back(namings.size()); + aux_solver.push(); + } + + // When we pop the solver, we have to re-add any namings that were lost + + void pop(int n) { + aux_solver.pop(n); + int new_assumps = assump_stack[assump_stack.size()-n]; + int new_namings = naming_stack[naming_stack.size()-n]; + for(unsigned i = new_namings; i < namings.size(); i++) + aux_solver.add(namings[i]); + assumps.resize(new_assumps); + namings.resize(new_namings); + assump_stack.resize(assump_stack.size()-1); + naming_stack.resize(naming_stack.size()-1); + } + + check_result check() { + return aux_solver.check(); + } + + model get_model() { + return aux_solver.get_model(); + } + + expr get_implicant() { + owner->dualModel = aux_solver.get_model(); + expr dual = owner->ctx.make(And,assumps); + bool ext = aux_solver.extensional_array_theory(); + expr eu = owner->UnderapproxFullFormula(dual,ext); + // if we renamed store terms, we have to undo + if(!ext) + eu = owner->SubstRec(renaming,eu); + return eu; + } + + implicant_solver(RPFP *_owner, solver &_aux_solver) + : owner(_owner), aux_solver(_aux_solver) + {} + }; + + // set up edge constraint in aux solver + void RPFP::AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge){ + if(!edge->dual.null()) + aux_solver.add(edge->dual); + for(unsigned i = 0; i < edge->constraints.size(); i++){ + expr tl = edge->constraints[i]; + aux_solver.add(tl); + } + } + void RPFP::AddEdgeToSolver(Edge *edge){ if(!edge->dual.null()) aux_solver.add(edge->dual); @@ -2853,28 +2961,29 @@ namespace Duality { const std::vector &theory = ls->get_axioms(); for(unsigned i = 0; i < theory.size(); i++) axioms_needed.insert(theory[i]); - aux_solver.push(); - AddEdgeToSolver(node->Outgoing); + implicant_solver is(this,aux_solver); + is.push(); + AddEdgeToSolver(is,node->Outgoing); node->Annotation.SetEmpty(); hash_set *core = new hash_set; core->insert(node->Outgoing->dual); while(1){ - aux_solver.push(); + is.push(); expr annot = !GetAnnotation(node); - aux_solver.add(annot); - if(aux_solver.check() == unsat){ - aux_solver.pop(1); + is.add(annot); + if(is.check() == unsat){ + is.pop(1); break; } - dualModel = aux_solver.get_model(); - aux_solver.pop(1); + is.pop(1); Push(); - FixCurrentStateFull(node->Outgoing,annot); - ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + ConstrainEdgeLocalized(node->Outgoing,is.get_implicant()); + ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this? check_result foo = Check(root); - if(foo != unsat) + if(foo != unsat){ + slvr().print("should_be_unsat.smt2"); throw "should be unsat"; - + } std::vector assumps, axioms_to_add; slvr().get_proof().get_assumptions(assumps); for(unsigned i = 0; i < assumps.size(); i++){ @@ -2890,7 +2999,7 @@ namespace Duality { { expr itp = GetAnnotation(node); - dualModel = aux_solver.get_model(); + dualModel = is.get_model(); // TODO: what does this mean? std::vector case_lits; itp = StrengthenFormulaByCaseSplitting(itp, case_lits); SetAnnotation(node,itp); @@ -2898,14 +3007,14 @@ namespace Duality { } for(unsigned i = 0; i < axioms_to_add.size(); i++) - aux_solver.add(axioms_to_add[i]); + is.add(axioms_to_add[i]); if(node->Annotation.IsEmpty()){ if(!axioms_added){ // add the axioms in the off chance they are useful const std::vector &theory = ls->get_axioms(); for(unsigned i = 0; i < theory.size(); i++) - aux_solver.add(theory[i]); + is.add(theory[i]); axioms_added = true; } else { @@ -2923,7 +3032,7 @@ namespace Duality { if(proof_core) delete proof_core; // shouldn't happen proof_core = core; - aux_solver.pop(1); + is.pop(1); timer_stop("InterpolateByCases"); } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index c7eec7e9f..3c69d79c0 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -131,6 +131,7 @@ namespace Duality { Report = false; StratifiedInlining = false; RecursionBound = -1; + BatchExpand = false; { scoped_no_proof no_proofs_please(ctx.m()); #ifdef USE_RPFP_CLONE @@ -365,6 +366,7 @@ namespace Duality { bool Report; // spew on stdout bool StratifiedInlining; // Do stratified inlining as preprocessing step int RecursionBound; // Recursion bound for bounded verification + bool BatchExpand; bool SetBoolOption(bool &opt, const std::string &value){ if(value == "0") { @@ -403,6 +405,9 @@ namespace Duality { if(option == "stratified_inlining"){ return SetBoolOption(StratifiedInlining,value); } + if(option == "batch_expand"){ + return SetBoolOption(BatchExpand,value); + } if(option == "recursion_bound"){ return SetIntOption(RecursionBound,value); } @@ -2016,7 +2021,7 @@ namespace Duality { } else { was_sat = true; - tree->Push(); + tree->Push(); std::vector &expansions = stack.back().expansions; #ifndef NO_DECISIONS for(unsigned i = 0; i < expansions.size(); i++){ @@ -2027,11 +2032,16 @@ namespace Duality { if(tree->slvr().check() == unsat) throw "help!"; #endif - stack.push_back(stack_entry()); - stack.back().level = tree->slvr().get_scope_level(); - if(ExpandSomeNodes(false,1)){ - continue; + int expand_max = 1; + if(0&&duality->BatchExpand){ + int thing = stack.size() * 0.1; + expand_max = std::max(1,thing); + if(expand_max > 1) + std::cout << "foo!\n"; } + + if(ExpandSomeNodes(false,expand_max)) + continue; while(stack.size() > 1){ tree->Pop(1); stack.pop_back(); @@ -2090,6 +2100,8 @@ namespace Duality { std::list updated_nodes; virtual void ExpandNode(RPFP::Node *p){ + stack.push_back(stack_entry()); + stack.back().level = tree->slvr().get_scope_level(); stack.back().expansions.push_back(p); DerivationTree::ExpandNode(p); std::vector &new_nodes = p->Outgoing->Children; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 345fef562..0f6198edd 100755 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -37,7 +37,7 @@ Revision History: namespace Duality { - solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) { + solver::solver(Duality::context& c, bool _extensional, bool models) : object(c), the_model(c) { params_ref p; p.set_bool("proof", true); // this is currently useless if(models) @@ -47,7 +47,8 @@ namespace Duality { p.set_bool("mbqi",mbqi); // just to test p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants - if(true || extensional) + extensional = mbqi && (true || _extensional); + if(extensional) p.set_bool("array.extensional",true); scoped_ptr sf = mk_smt_solver_factory(); m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); @@ -657,6 +658,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st pp.display_smt2(std::cout, m_solver->get_assertion(n-1)); } + void solver::print(const char *filename) { + std::ofstream f(filename); + unsigned n = m_solver->get_num_assertions(); + if(!n) + return; + ast_smt_pp pp(m()); + for (unsigned i = 0; i < n-1; ++i) + pp.add_assumption(m_solver->get_assertion(i)); + pp.display_smt2(f, m_solver->get_assertion(n-1)); + } + + void solver::show_assertion_ids() { #if 0 unsigned n = m_solver->get_num_assertions(); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index febc3f1f1..ccc0800b2 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -819,6 +819,7 @@ namespace Duality { model the_model; bool canceled; proof_gen_mode m_mode; + bool extensional; public: solver(context & c, bool extensional = false, bool models = true); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} @@ -922,6 +923,7 @@ namespace Duality { unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} void show(); + void print(const char *filename); void show_assertion_ids(); proof get_proof(){ @@ -929,6 +931,7 @@ namespace Duality { return proof(ctx(),m_solver->get_proof()); } + bool extensional_array_theory() {return extensional;} }; #if 0 diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 5eec77f39..e201c2a19 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -75,6 +75,7 @@ def_module_params('fixedpoint', ('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'), ('profile', BOOL, False, 'DUALITY: profile run time'), ('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'), + ('batch_expand', BOOL, False, 'DUALITY: use batch expansion'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), )) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index e7c7976f6..0c2a9e48a 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -205,6 +205,7 @@ lbool dl_interface::query(::expr * query) { rs->SetOption("feasible_edges",m_ctx.get_params().feasible_edges() ? "1" : "0"); rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0"); rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0"); + rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0"); unsigned rb = m_ctx.get_params().recursion_bound(); if(rb != UINT_MAX){ std::ostringstream os; os << rb; From bbab6be280c687fce57eee84bd1161356dd76853 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 14 Mar 2014 13:40:31 -0700 Subject: [PATCH 5/5] duality: eager deduction and history-based conjectures --- src/duality/duality.h | 41 ++- src/duality/duality_rpfp.cpp | 2 +- src/duality/duality_solver.cpp | 418 +++++++++++++++++++---- src/duality/duality_wrapper.h | 17 + src/muz/duality/duality_dl_interface.cpp | 70 ++-- 5 files changed, 440 insertions(+), 108 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 137279899..b1171a698 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -204,6 +204,9 @@ protected: /** Is this a background constant? */ virtual bool is_constant(const func_decl &f) = 0; + /** Get the constants in the background vocabulary */ + virtual hash_set &get_constants() = 0; + /** Assert a background axiom. */ virtual void assert_axiom(const expr &axiom) = 0; @@ -297,6 +300,11 @@ protected: return bckg.find(f) != bckg.end(); } + /** Get the constants in the background vocabulary */ + virtual hash_set &get_constants(){ + return bckg; + } + ~iZ3LogicSolver(){ // delete ictx; delete islvr; @@ -1064,13 +1072,40 @@ protected: public: - struct Counterexample { + class Counterexample { + private: RPFP *tree; RPFP::Node *root; + public: Counterexample(){ tree = 0; root = 0; } + Counterexample(RPFP *_tree, RPFP::Node *_root){ + tree = _tree; + root = _root; + } + ~Counterexample(){ + if(tree) delete tree; + } + void swap(Counterexample &other){ + std::swap(tree,other.tree); + std::swap(root,other.root); + } + void set(RPFP *_tree, RPFP::Node *_root){ + if(tree) delete tree; + tree = _tree; + root = _root; + } + void clear(){ + if(tree) delete tree; + tree = 0; + } + RPFP *get_tree() const {return tree;} + RPFP::Node *get_root() const {return root;} + private: + Counterexample &operator=(const Counterexample &); + Counterexample(const Counterexample &); }; /** Solve the problem. You can optionally give an old @@ -1080,7 +1115,7 @@ protected: virtual bool Solve() = 0; - virtual Counterexample GetCounterexample() = 0; + virtual Counterexample &GetCounterexample() = 0; virtual bool SetOption(const std::string &option, const std::string &value) = 0; @@ -1088,7 +1123,7 @@ protected: is chiefly useful for abstraction refinement, when we want to solve a series of similar problems. */ - virtual void LearnFrom(Counterexample &old_cex) = 0; + virtual void LearnFrom(Solver *old_solver) = 0; virtual ~Solver(){} diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 2d871c324..f3deee225 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -3334,7 +3334,7 @@ namespace Duality { func_decl f = t.decl(); std::vector args; int nargs = t.num_args(); - if(nargs == 0) + if(nargs == 0 && f.get_decl_kind() == Uninterpreted) ls->declare_constant(f); // keep track of background constants for(int i = 0; i < nargs; i++) args.push_back(SubstBoundRec(memo, subst, level, t.arg(i))); diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 3c69d79c0..d59309c00 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -54,6 +54,7 @@ Revision History: // #define KEEP_EXPANSIONS // #define USE_CACHING_RPFP // #define PROPAGATE_BEFORE_CHECK +#define NEW_STRATIFIED_INLINING #define USE_RPFP_CLONE #define USE_NEW_GEN_CANDS @@ -82,7 +83,7 @@ namespace Duality { rpfp = _rpfp; } virtual void Extend(RPFP::Node *node){} - virtual void Update(RPFP::Node *node, const RPFP::Transformer &update){} + virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){} virtual void Bound(RPFP::Node *node){} virtual void Expand(RPFP::Edge *edge){} virtual void AddCover(RPFP::Node *covered, std::vector &covering){} @@ -94,6 +95,7 @@ namespace Duality { virtual void UpdateUnderapprox(RPFP::Node *node, const RPFP::Transformer &update){} virtual void Reject(RPFP::Edge *edge, const std::vector &Children){} virtual void Message(const std::string &msg){} + virtual void Depth(int){} virtual ~Reporter(){} }; @@ -124,6 +126,7 @@ namespace Duality { rpfp = _rpfp; reporter = 0; heuristic = 0; + unwinding = 0; FullExpand = false; NoConj = false; FeasibleEdges = true; @@ -152,6 +155,7 @@ namespace Duality { #ifdef USE_NEW_GEN_CANDS delete gen_cands_rpfp; #endif + if(unwinding) delete unwinding; } #ifdef USE_RPFP_CLONE @@ -250,6 +254,19 @@ namespace Duality { virtual void Done() {} }; + /** The Proposer class proposes conjectures eagerly. These can come + from any source, including predicate abstraction, templates, or + previous solver runs. The proposed conjectures are checked + with low effort when the unwinding is expanded. + */ + + class Proposer { + public: + /** Given a node in the unwinding, propose some conjectures */ + virtual std::vector &Propose(Node *node) = 0; + virtual ~Proposer(){}; + }; + class Covering; // see below @@ -279,6 +296,7 @@ namespace Duality { hash_map underapprox_map; // maps underapprox nodes to the nodes they approximate int last_decisions; hash_set overapproxes; + std::vector proposers; #ifdef BOUNDED struct Counter { @@ -293,24 +311,22 @@ namespace Duality { virtual bool Solve(){ reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp); #ifndef LOCALIZE_CONJECTURES - heuristic = !cex.tree ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex); + heuristic = !cex.get_tree() ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex); #else - heuristic = !cex.tree ? (Heuristic *)(new LocalHeuristic(rpfp)) + heuristic = !cex.get_tree() ? (Heuristic *)(new LocalHeuristic(rpfp)) : (Heuristic *)(new ReplayHeuristic(rpfp,cex)); #endif - cex.tree = 0; // heuristic now owns it + cex.clear(); // in case we didn't use it for heuristic + if(unwinding) delete unwinding; unwinding = new RPFP(rpfp->ls); unwinding->HornClauses = rpfp->HornClauses; indset = new Covering(this); last_decisions = 0; CreateEdgesByChildMap(); - CreateLeaves(); #ifndef TOP_DOWN - if(!StratifiedInlining){ - if(FeasibleEdges)NullaryCandidates(); - else InstantiateAllEdges(); - } + void CreateInitialUnwinding(); #else + CreateLeaves(); for(unsigned i = 0; i < leaves.size(); i++) if(!SatisfyUpperBound(leaves[i])) return false; @@ -322,11 +338,29 @@ namespace Duality { // print_profile(std::cout); delete indset; delete heuristic; - delete unwinding; + // delete unwinding; // keep the unwinding for future mining of predicates delete reporter; + for(unsigned i = 0; i < proposers.size(); i++) + delete proposers[i]; return res; } + void CreateInitialUnwinding(){ + if(!StratifiedInlining){ + CreateLeaves(); + if(FeasibleEdges)NullaryCandidates(); + else InstantiateAllEdges(); + } + else { +#ifdef NEW_STRATIFIED_INLINING + +#else + CreateLeaves(); +#endif + } + + } + void Cancel(){ // TODO } @@ -347,15 +381,19 @@ namespace Duality { } #endif - virtual void LearnFrom(Counterexample &old_cex){ - cex = old_cex; + virtual void LearnFrom(Solver *other_solver){ + // get the counterexample as a guide + cex.swap(other_solver->GetCounterexample()); + + // propose conjectures based on old unwinding + Duality *old_duality = dynamic_cast(other_solver); + if(old_duality) + proposers.push_back(new HistoryProposer(old_duality,this)); } - /** Return the counterexample */ - virtual Counterexample GetCounterexample(){ - Counterexample res = cex; - cex.tree = 0; // Cex now belongs to caller - return res; + /** Return a reference to the counterexample */ + virtual Counterexample &GetCounterexample(){ + return cex; } // options @@ -519,7 +557,11 @@ namespace Duality { c.Children.resize(edge->Children.size()); for(unsigned j = 0; j < c.Children.size(); j++) c.Children[j] = leaf_map[edge->Children[j]]; - Extend(c); + Node *new_node; + Extend(c,new_node); +#ifdef EARLY_EXPAND + TryExpandNode(new_node); +#endif } for(Unexpanded::iterator it = unexpanded.begin(), en = unexpanded.end(); it != en; ++it) indset->Add(*it); @@ -771,16 +813,14 @@ namespace Duality { } - /* For stratified inlining, we need a topological sort of the - nodes. */ - hash_map TopoSort; int TopoSortCounter; + std::vector SortedEdges; void DoTopoSortRec(Node *node){ if(TopoSort.find(node) != TopoSort.end()) return; - TopoSort[node] = TopoSortCounter++; // just to break cycles + TopoSort[node] = INT_MAX; // just to break cycles Edge *edge = node->Outgoing; // note, this is just *one* outgoing edge if(edge){ std::vector &chs = edge->Children; @@ -788,22 +828,81 @@ namespace Duality { DoTopoSortRec(chs[i]); } TopoSort[node] = TopoSortCounter++; + SortedEdges.push_back(edge); } void DoTopoSort(){ TopoSort.clear(); + SortedEdges.clear(); TopoSortCounter = 0; for(unsigned i = 0; i < nodes.size(); i++) DoTopoSortRec(nodes[i]); } + + int StratifiedLeafCount; + +#ifdef NEW_STRATIFIED_INLINING + + /** Stratified inlining builds an initial layered unwinding before + switching to the LAWI strategy. Currently the number of layers + is one. Only nodes that are the targets of back edges are + consider to be leaves. This assumes we have already computed a + topological sort. + */ + + bool DoStratifiedInlining(){ + DoTopoSort(); + int depth = 1; // TODO: make this an option + std::vector > unfolding_levels(depth+1); + for(int level = 1; level <= depth; level++) + for(unsigned i = 0; i < SortedEdges.size(); i++){ + Edge *edge = SortedEdges[i]; + Node *parent = edge->Parent; + std::vector &chs = edge->Children; + std::vector my_chs(chs.size()); + for(unsigned j = 0; j < chs.size(); j++){ + Node *child = chs[j]; + int ch_level = TopoSort[child] >= TopoSort[parent] ? level-1 : level; + if(unfolding_levels[ch_level].find(child) == unfolding_levels[ch_level].end()){ + if(ch_level == 0) + unfolding_levels[0][child] = CreateLeaf(child); + else + throw InternalError("in levelized unwinding"); + } + my_chs[j] = unfolding_levels[ch_level][child]; + } + Candidate cand; cand.edge = edge; cand.Children = my_chs; + Node *new_node; + bool ok = Extend(cand,new_node); + MarkExpanded(new_node); // we don't expand here -- just mark it done + if(!ok) return false; // got a counterexample + unfolding_levels[level][parent] = new_node; + } + return true; + } + + Node *CreateLeaf(Node *node){ + RPFP::Node *nchild = CreateNodeInstance(node); + MakeLeaf(nchild, /* do_not_expand = */ true); + nchild->Annotation.SetEmpty(); + return nchild; + } + + void MarkExpanded(Node *node){ + if(unexpanded.find(node) != unexpanded.end()){ + unexpanded.erase(node); + insts_of_node[node->map].push_back(node); + } + } + +#else + /** In stratified inlining, we build the unwinding from the bottom down, trying to satisfy the node bounds. We do this as a pre-pass, limiting the expansion. If we get a counterexample, we are done, else we continue as usual expanding the unwinding upward. */ - - int StratifiedLeafCount; bool DoStratifiedInlining(){ timer_start("StratifiedInlining"); @@ -826,6 +925,8 @@ namespace Duality { return true; } +#endif + /** Here, we do the downward expansion for stratified inlining */ hash_map LeafMap, StratifiedLeafMap; @@ -912,9 +1013,14 @@ namespace Duality { } Candidate cand = candidates.front(); candidates.pop_front(); - if(CandidateFeasible(cand)) - if(!Extend(cand)) + if(CandidateFeasible(cand)){ + Node *new_node; + if(!Extend(cand,new_node)) return false; +#ifdef EARLY_EXPAND + TryExpandNode(new_node); +#endif + } } } @@ -934,9 +1040,9 @@ namespace Duality { Node *CreateUnderapproxNode(Node *node){ - // cex.tree->ComputeUnderapprox(cex.root,0); + // cex.get_tree()->ComputeUnderapprox(cex.get_root(),0); RPFP::Node *under_node = CreateNodeInstance(node->map /* ,StratifiedLeafCount-- */); - under_node->Annotation.IntersectWith(cex.root->Underapprox); + under_node->Annotation.IntersectWith(cex.get_root()->Underapprox); AddThing(under_node->Annotation.Formula); Edge *e = unwinding->CreateLowerBoundEdge(under_node); under_node->Annotation.SetFull(); // allow this node to cover others @@ -972,9 +1078,8 @@ namespace Duality { ExpandNodeFromCoverFail(node); } #endif - if(_cex) *_cex = cex; - else delete cex.tree; // delete the cex if not required - cex.tree = 0; + if(_cex) (*_cex).swap(cex); // return the cex if asked + cex.clear(); // throw away the useless cex node->Bound = save; // put back original bound timer_stop("ProveConjecture"); return false; @@ -1354,16 +1459,20 @@ namespace Duality { } } - bool UpdateNodeToNode(Node *node, Node *top){ - if(!node->Annotation.SubsetEq(top->Annotation)){ - reporter->Update(node,top->Annotation); - indset->Update(node,top->Annotation); + bool Update(Node *node, const RPFP::Transformer &fact, bool eager=false){ + if(!node->Annotation.SubsetEq(fact)){ + reporter->Update(node,fact,eager); + indset->Update(node,fact); updated_nodes.insert(node->map); - node->Annotation.IntersectWith(top->Annotation); + node->Annotation.IntersectWith(fact); return true; } return false; } + + bool UpdateNodeToNode(Node *node, Node *top){ + return Update(node,top->Annotation); + } /** Update the unwinding solution, using an interpolant for the derivation tree. */ @@ -1405,8 +1514,7 @@ namespace Duality { // std::cout << "decisions: " << (end_decs - start_decs) << std::endl; last_decisions = end_decs - start_decs; if(res){ - cex.tree = dt.tree; - cex.root = dt.top; + cex.set(dt.tree,dt.top); // note tree is now owned by cex if(UseUnderapprox){ UpdateWithCounterexample(node,dt.tree,dt.top); } @@ -1418,6 +1526,64 @@ namespace Duality { delete dtp; return !res; } + + /* For a given nod in the unwinding, get conjectures from the + proposers and check them locally. Update the node with any true + conjectures. + */ + + void DoEagerDeduction(Node *node){ + for(unsigned i = 0; i < proposers.size(); i++){ + const std::vector &conjectures = proposers[i]->Propose(node); + for(unsigned j = 0; j < conjectures.size(); j++){ + const RPFP::Transformer &conjecture = conjectures[j]; + RPFP::Transformer bound(conjecture); + std::vector conj_vec; + unwinding->CollectConjuncts(bound.Formula,conj_vec); + for(unsigned k = 0; k < conj_vec.size(); k++){ + bound.Formula = conj_vec[k]; + if(CheckEdgeCaching(node->Outgoing,bound) == unsat) + Update(node,bound, /* eager = */ true); + //else + //std::cout << "conjecture failed\n"; + } + } + } + } + + + check_result CheckEdge(RPFP *checker, Edge *edge){ + Node *root = edge->Parent; + checker->Push(); + checker->AssertNode(root); + checker->AssertEdge(edge,1,true); + check_result res = checker->Check(root); + checker->Pop(1); + return res; + } + + check_result CheckEdgeCaching(Edge *unwinding_edge, const RPFP::Transformer &bound){ + + // use a dedicated solver for this edge + // TODO: can this mess be hidden somehow? + + RPFP_caching *checker = gen_cands_rpfp; // TODO: a good choice? + Edge *edge = unwinding_edge->map; // get the edge in the original RPFP + RPFP_caching::scoped_solver_for_edge ssfe(checker,edge,true /* models */, true /*axioms*/); + Edge *checker_edge = checker->GetEdgeClone(edge); + + // copy the annotations and bound to the clone + Node *root = checker_edge->Parent; + root->Bound = bound; + for(unsigned j = 0; j < checker_edge->Children.size(); j++){ + Node *oc = unwinding_edge->Children[j]; + Node *nc = checker_edge->Children[j]; + nc->Annotation = oc->Annotation; + } + + return CheckEdge(checker,checker_edge); + } + /* If the counterexample derivation is partial due to use of underapproximations, complete it. */ @@ -1426,10 +1592,7 @@ namespace Duality { DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); bool res = dt.Derive(unwinding,node,UseUnderapprox,true); // build full tree if(!res) throw "Duality internal error in BuildFullCex"; - if(cex.tree) - delete cex.tree; - cex.tree = dt.tree; - cex.root = dt.top; + cex.set(dt.tree,dt.top); } void UpdateBackEdges(Node *node){ @@ -1452,25 +1615,23 @@ namespace Duality { } /** Extend the unwinding, keeping it solved. */ - bool Extend(Candidate &cand){ + bool Extend(Candidate &cand, Node *&node){ timer_start("Extend"); - Node *node = CreateNodeInstance(cand.edge->Parent); + node = CreateNodeInstance(cand.edge->Parent); CreateEdgeInstance(cand.edge,node,cand.Children); UpdateBackEdges(node); reporter->Extend(node); - bool res = SatisfyUpperBound(node); + DoEagerDeduction(node); // first be eager... + bool res = SatisfyUpperBound(node); // then be lazy if(res) indset->CloseDescendants(node); else { #ifdef UNDERAPPROX_NODES - ExpandUnderapproxNodes(cex.tree, cex.root); + ExpandUnderapproxNodes(cex.get_tree(), cex.get_root()); #endif if(UseUnderapprox) BuildFullCex(node); timer_stop("Extend"); return res; } -#ifdef EARLY_EXPAND - TryExpandNode(node); -#endif timer_stop("Extend"); return res; } @@ -1930,6 +2091,7 @@ namespace Duality { unsigned slvr_level = tree->slvr().get_scope_level(); if(slvr_level != stack.back().level) throw "stacks out of sync!"; + reporter->Depth(stack.size()); // res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop check_result foo = tree->Check(top); @@ -2459,7 +2621,7 @@ namespace Duality { } bool ContainsCex(Node *node, Counterexample &cex){ - expr val = cex.tree->Eval(cex.root->Outgoing,node->Annotation.Formula); + expr val = cex.get_tree()->Eval(cex.get_root()->Outgoing,node->Annotation.Formula); return eq(val,parent->ctx.bool_val(true)); } @@ -2478,15 +2640,15 @@ namespace Duality { Node *other = insts[i]; if(CouldCover(node,other)){ reporter()->Forcing(node,other); - if(cex.tree && !ContainsCex(other,cex)) + if(cex.get_tree() && !ContainsCex(other,cex)) continue; - if(cex.tree) {delete cex.tree; cex.tree = 0;} + cex.clear(); if(parent->ProveConjecture(node,other->Annotation,other,&cex)) if(CloseDescendants(node)) return true; } } - if(cex.tree) {delete cex.tree; cex.tree = 0;} + cex.clear(); return false; } #else @@ -2585,13 +2747,12 @@ namespace Duality { Counterexample old_cex; public: ReplayHeuristic(RPFP *_rpfp, Counterexample &_old_cex) - : Heuristic(_rpfp), old_cex(_old_cex) + : Heuristic(_rpfp) { + old_cex.swap(_old_cex); // take ownership from caller } ~ReplayHeuristic(){ - if(old_cex.tree) - delete old_cex.tree; } // Maps nodes of derivation tree into old cex @@ -2599,9 +2760,7 @@ namespace Duality { void Done() { cex_map.clear(); - if(old_cex.tree) - delete old_cex.tree; - old_cex.tree = 0; // only replay once! + old_cex.clear(); } void ShowNodeAndChildren(Node *n){ @@ -2623,7 +2782,7 @@ namespace Duality { } virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority, bool best_only){ - if(!high_priority || !old_cex.tree){ + if(!high_priority || !old_cex.get_tree()){ Heuristic::ChooseExpand(choices,best,false); return; } @@ -2632,7 +2791,7 @@ namespace Duality { 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.root; // match the root nodes + cex_map[node] = old_cex.get_root(); // match the root nodes 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()) @@ -2658,7 +2817,7 @@ namespace Duality { Node *old_node = cex_map[node]; if(!old_node) unmatched.insert(node); - else if(old_cex.tree->Empty(old_node)) + else if(old_cex.get_tree()->Empty(old_node)) unmatched.insert(node); else matched.insert(node); @@ -2732,7 +2891,120 @@ namespace Duality { } }; + /** This proposer class generates conjectures based on the + unwinding generated by a previous solver. The assumption is + that the provious solver was working on a different + abstraction of the same system. The trick is to adapt the + annotations in the old unwinding to the new predicates. We + start by generating a map from predicates and parameters in + the old problem to the new. + HACK: mapping is done by cheesy name comparison. + */ + + class HistoryProposer : public Proposer + { + Duality *old_solver; + Duality *new_solver; + hash_map > conjectures; + + public: + /** Construct a history solver. */ + HistoryProposer(Duality *_old_solver, Duality *_new_solver) + : old_solver(_old_solver), new_solver(_new_solver) { + + // tricky: names in the axioms may have changed -- map them + hash_set &old_constants = old_solver->unwinding->ls->get_constants(); + hash_set &new_constants = new_solver->rpfp->ls->get_constants(); + hash_map cmap; + for(hash_set::iterator it = new_constants.begin(), en = new_constants.end(); it != en; ++it) + cmap[GetKey(*it)] = *it; + hash_map bckg_map; + for(hash_set::iterator it = old_constants.begin(), en = old_constants.end(); it != en; ++it){ + func_decl f = new_solver->ctx.translate(*it); // move to new context + if(cmap.find(GetKey(f)) != cmap.end()) + bckg_map[f] = cmap[GetKey(f)]; + // else + // std::cout << "constant not matched\n"; + } + + RPFP *old_unwinding = old_solver->unwinding; + hash_map > pred_match; + + // index all the predicates in the old unwinding + for(unsigned i = 0; i < old_unwinding->nodes.size(); i++){ + Node *node = old_unwinding->nodes[i]; + std::string key = GetKey(node); + pred_match[key].push_back(node); + } + + // match with predicates in the new RPFP + RPFP *rpfp = new_solver->rpfp; + for(unsigned i = 0; i < rpfp->nodes.size(); i++){ + Node *node = rpfp->nodes[i]; + std::string key = GetKey(node); + std::vector &matches = pred_match[key]; + for(unsigned j = 0; j < matches.size(); j++) + MatchNodes(node,matches[j],bckg_map); + } + } + + virtual std::vector &Propose(Node *node){ + return conjectures[node->map]; + } + + virtual ~HistoryProposer(){ + }; + + private: + void MatchNodes(Node *new_node, Node *old_node, hash_map &bckg_map){ + if(old_node->Annotation.IsFull()) + return; // don't conjecture true! + hash_map var_match; + std::vector &new_params = new_node->Annotation.IndParams; + // Index the new parameters by their keys + for(unsigned i = 0; i < new_params.size(); i++) + var_match[GetKey(new_params[i])] = new_params[i]; + RPFP::Transformer &old = old_node->Annotation; + std::vector from_params = old.IndParams; + for(unsigned j = 0; j < from_params.size(); j++) + from_params[j] = new_solver->ctx.translate(from_params[j]); // get in new context + std::vector to_params = from_params; + for(unsigned j = 0; j < to_params.size(); j++){ + std::string key = GetKey(to_params[j]); + if(var_match.find(key) == var_match.end()){ + // std::cout << "unmatched parameter!\n"; + return; + } + to_params[j] = var_match[key]; + } + expr fmla = new_solver->ctx.translate(old.Formula); // get in new context + fmla = new_solver->rpfp->SubstParams(old.IndParams,to_params,fmla); // substitute parameters + hash_map memo; + fmla = new_solver->rpfp->SubstRec(memo,bckg_map,fmla); // substitute background constants + RPFP::Transformer new_annot = new_node->Annotation; + new_annot.Formula = fmla; + conjectures[new_node].push_back(new_annot); + } + + // We match names by removing suffixes beginning with double at sign + + std::string GetKey(Node *node){ + return GetKey(node->Name); + } + + std::string GetKey(const expr &var){ + return GetKey(var.decl()); + } + + std::string GetKey(const func_decl &f){ + std::string name = f.name().str(); + int idx = name.find("@@"); + if(idx >= 0) + name.erase(idx); + return name; + } + }; }; @@ -2740,8 +3012,9 @@ namespace Duality { std::ostream &s; public: StreamReporter(RPFP *_rpfp, std::ostream &_s) - : Reporter(_rpfp), s(_s) {event = 0;} + : Reporter(_rpfp), s(_s) {event = 0; depth = -1;} int event; + int depth; void ev(){ s << "[" << event++ << "]" ; } @@ -2752,23 +3025,30 @@ namespace Duality { s << " " << rps[i]->number; s << std::endl; } - virtual void Update(RPFP::Node *node, const RPFP::Transformer &update){ + virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){ ev(); s << "update " << node->number << " " << node->Name.name() << ": "; rpfp->Summarize(update.Formula); - std::cout << std::endl; + if(depth > 0) s << " (depth=" << depth << ")"; + if(eager) s << " (eager)"; + s << std::endl; } virtual void Bound(RPFP::Node *node){ ev(); s << "check " << node->number << std::endl; } virtual void Expand(RPFP::Edge *edge){ RPFP::Node *node = edge->Parent; - ev(); s << "expand " << node->map->number << " " << node->Name.name() << std::endl; + ev(); s << "expand " << node->map->number << " " << node->Name.name(); + if(depth > 0) s << " (depth=" << depth << ")"; + s << std::endl; + } + virtual void Depth(int d){ + depth = d; } virtual void AddCover(RPFP::Node *covered, std::vector &covering){ ev(); s << "cover " << covered->Name.name() << ": " << covered->number << " by "; for(unsigned i = 0; i < covering.size(); i++) - std::cout << covering[i]->number << " "; - std::cout << std::endl; + s << covering[i]->number << " "; + s << std::endl; } virtual void RemoveCover(RPFP::Node *covered, RPFP::Node *covering){ ev(); s << "uncover " << covered->Name.name() << ": " << covered->number << " by " << covering->number << std::endl; @@ -2779,7 +3059,7 @@ namespace Duality { virtual void Conjecture(RPFP::Node *node, const RPFP::Transformer &t){ ev(); s << "conjecture " << node->number << " " << node->Name.name() << ": "; rpfp->Summarize(t.Formula); - std::cout << std::endl; + s << std::endl; } virtual void Dominates(RPFP::Node *node, RPFP::Node *other){ ev(); s << "dominates " << node->Name.name() << ": " << node->number << " > " << other->number << std::endl; diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index ccc0800b2..a7497318a 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -244,6 +244,9 @@ namespace Duality { sort_kind get_sort_kind(const sort &s); + expr translate(const expr &e); + func_decl translate(const func_decl &); + void print_expr(std::ostream &s, const ast &e); fixedpoint mk_fixedpoint(); @@ -1374,6 +1377,20 @@ namespace Duality { return to_expr(a.raw()); } + inline expr context::translate(const expr &e) { + ::expr *f = to_expr(e.raw()); + if(&e.ctx().m() != &m()) // same ast manager -> no translation + throw "ast manager mismatch"; + return cook(f); + } + + inline func_decl context::translate(const func_decl &e) { + ::func_decl *f = to_func_decl(e.raw()); + if(&e.ctx().m() != &m()) // same ast manager -> no translation + throw "ast manager mismatch"; + return func_decl(*this,f); + } + typedef double clock_t; clock_t current_time(); inline void output_time(std::ostream &os, clock_t time){os << time;} diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 0c2a9e48a..587a184bc 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -64,20 +64,22 @@ namespace Duality { std::vector clauses; std::vector > clause_labels; hash_map map; // edges to clauses + Solver *old_rs; Solver::Counterexample cex; duality_data(ast_manager &_m) : ctx(_m,config(params_ref())) { ls = 0; rpfp = 0; status = StatusNull; + old_rs = 0; } ~duality_data(){ + if(old_rs) + dealloc(old_rs); if(rpfp) dealloc(rpfp); if(ls) dealloc(ls); - if(cex.tree) - delete cex.tree; } }; @@ -132,10 +134,12 @@ lbool dl_interface::query(::expr * query) { m_ctx.ensure_opened(); // if there is old data, get the cex and dispose (later) - Solver::Counterexample old_cex; duality_data *old_data = _d; - if(old_data) - old_cex = old_data->cex; + Solver *old_rs = 0; + if(old_data){ + old_rs = old_data->old_rs; + old_rs->GetCounterexample().swap(old_data->cex); + } scoped_proof generate_proofs_please(m_ctx.get_manager()); @@ -196,8 +200,9 @@ lbool dl_interface::query(::expr * query) { Solver *rs = Solver::Create("duality", _d->rpfp); - rs->LearnFrom(old_cex); // new solver gets hints from old cex - + if(old_rs) + rs->LearnFrom(old_rs); // new solver gets hints from old solver + // set its options IF_VERBOSE(1, rs->SetOption("report","1");); rs->SetOption("full_expand",m_ctx.get_params().full_expand() ? "1" : "0"); @@ -231,15 +236,14 @@ lbool dl_interface::query(::expr * query) { // save the result and counterexample if there is one _d->status = ans ? StatusModel : StatusRefutation; - _d->cex = rs->GetCounterexample(); + _d->cex.swap(rs->GetCounterexample()); // take ownership of cex + _d->old_rs = rs; // save this for later hints if(old_data){ - old_data->cex.tree = 0; // we own it now - dealloc(old_data); + dealloc(old_data); // this deallocates the old solver if there is one } - - dealloc(rs); + // 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; @@ -267,18 +271,16 @@ void dl_interface::reset_statistics() { static hash_set *local_func_decls; -static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexample &cex) { + static void print_proof(dl_interface *d, std::ostream& out, RPFP *tree, RPFP::Node *root) { context &ctx = d->dd()->ctx; - RPFP::Node &node = *cex.root; + RPFP::Node &node = *root; RPFP::Edge &edge = *node.Outgoing; // first, prove the children (that are actually used) for(unsigned i = 0; i < edge.Children.size(); i++){ - if(!cex.tree->Empty(edge.Children[i])){ - Solver::Counterexample foo = cex; - foo.root = edge.Children[i]; - print_proof(d,out,foo); + if(!tree->Empty(edge.Children[i])){ + print_proof(d,out,tree,edge.Children[i]); } } @@ -287,7 +289,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp out << "(step s!" << node.number; out << " (" << node.Name.name(); for(unsigned i = 0; i < edge.F.IndParams.size(); i++) - out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]); + out << " " << tree->Eval(&edge,edge.F.IndParams[i]); out << ")\n"; // print the rule number @@ -309,8 +311,8 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp sort the_sort = t.get_quantifier_bound_sort(j); symbol name = t.get_quantifier_bound_name(j); expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort)); - out << " (= " << skolem << " " << cex.tree->Eval(&edge,skolem) << ")\n"; - expr local_skolem = cex.tree->Localize(&edge,skolem); + out << " (= " << skolem << " " << tree->Eval(&edge,skolem) << ")\n"; + expr local_skolem = tree->Localize(&edge,skolem); (*local_func_decls).insert(local_skolem.decl()); } } @@ -318,7 +320,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp out << " (labels"; std::vector labels; - cex.tree->GetLabels(&edge,labels); + tree->GetLabels(&edge,labels); for(unsigned j = 0; j < labels.size(); j++){ out << " " << labels[j]; } @@ -330,7 +332,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp out << " (ref "; for(unsigned i = 0; i < edge.Children.size(); i++){ - if(!cex.tree->Empty(edge.Children[i])) + if(!tree->Empty(edge.Children[i])) out << " s!" << edge.Children[i]->number; else out << " true"; @@ -355,11 +357,11 @@ void dl_interface::display_certificate_non_const(std::ostream& out) { // negation of the query is the last clause -- prove it hash_set locals; local_func_decls = &locals; - print_proof(this,out,_d->cex); + print_proof(this,out,_d->cex.get_tree(),_d->cex.get_root()); out << ")\n"; out << "(model \n\""; ::model mod(m_ctx.get_manager()); - model orig_model = _d->cex.tree->dualModel; + model orig_model = _d->cex.get_tree()->dualModel; for(unsigned i = 0; i < orig_model.num_consts(); i++){ func_decl cnst = orig_model.get_const_decl(i); if(locals.find(cnst) == locals.end()){ @@ -430,10 +432,10 @@ model_ref dl_interface::get_model() { return md; } -static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) { + static proof_ref extract_proof(dl_interface *d, RPFP *tree, RPFP::Node *root) { context &ctx = d->dd()->ctx; ast_manager &mgr = ctx.m(); - RPFP::Node &node = *cex.root; + RPFP::Node &node = *root; RPFP::Edge &edge = *node.Outgoing; RPFP::Edge *orig_edge = edge.map; @@ -455,21 +457,19 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) { sort the_sort = t.get_quantifier_bound_sort(j); symbol name = t.get_quantifier_bound_name(j); expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort)); - expr val = cex.tree->Eval(&edge,skolem); + expr val = tree->Eval(&edge,skolem); expr_ref thing(ctx.uncook(val),mgr); substs[0].push_back(thing); - expr local_skolem = cex.tree->Localize(&edge,skolem); + expr local_skolem = tree->Localize(&edge,skolem); (*local_func_decls).insert(local_skolem.decl()); } } svector > pos; for(unsigned i = 0; i < edge.Children.size(); i++){ - if(!cex.tree->Empty(edge.Children[i])){ + if(!tree->Empty(edge.Children[i])){ pos.push_back(std::pair(i+1,0)); - Solver::Counterexample foo = cex; - foo.root = edge.Children[i]; - proof_ref prem = extract_proof(d,foo); + proof_ref prem = extract_proof(d,tree,edge.Children[i]); prems.push_back(prem); substs.push_back(expr_ref_vector(mgr)); } @@ -478,7 +478,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) { func_decl f = node.Name; std::vector args; for(unsigned i = 0; i < edge.F.IndParams.size(); i++) - args.push_back(cex.tree->Eval(&edge,edge.F.IndParams[i])); + args.push_back(tree->Eval(&edge,edge.F.IndParams[i])); expr conc = f(args); @@ -495,7 +495,7 @@ proof_ref dl_interface::get_proof() { if(_d->status == StatusRefutation){ hash_set locals; local_func_decls = &locals; - return extract_proof(this,_d->cex); + return extract_proof(this,_d->cex.get_tree(),_d->cex.get_root()); } else return proof_ref(m_ctx.get_manager());