diff --git a/src/duality/duality.h b/src/duality/duality.h index fb3761626..7a1e88f3c 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -79,9 +79,12 @@ namespace Duality { int CumulativeDecisions(); + int CountOperators(const Term &t); + private: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); + int CountOperatorsRec(hash_set &memo, const Term &t); }; @@ -280,7 +283,7 @@ namespace Duality { public: std::list edges; std::list nodes; - std::list constraints; + std::list > constraints; }; @@ -556,6 +559,7 @@ namespace Duality { edge to their values in the current assignment. */ void FixCurrentState(Edge *root); + void FixCurrentStateFull(Edge *edge); /** Declare a constant in the background theory. */ @@ -653,7 +657,11 @@ namespace Duality { Term ComputeUnderapprox(Node *root, int persist); /** Try to strengthen the annotation of a node by removing disjuncts. */ - void Generalize(Node *node); + void Generalize(Node *root, Node *node); + + + /** Compute disjunctive interpolant for node by case splitting */ + void InterpolateByCases(Node *root, Node *node); /** Push a scope. Assertions made after Push can be undone by Pop. */ @@ -687,6 +695,10 @@ namespace Duality { void Pop(int num_scopes); + /** Erase the proof by performing a Pop, Push and re-assertion of + all the popped constraints */ + void PopPush(); + /** Return true if the given edge is used in the proof of unsat. Can be called only after Solve or Check returns an unsat result. */ @@ -861,6 +873,11 @@ namespace Duality { 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); + + Term UnderapproxFullFormula(const Term &f, hash_set &dont_cares); + Term ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants); hash_map resolve_ite_memo; @@ -896,6 +913,11 @@ namespace Duality { expr SimplifyOr(std::vector &lits); void SetAnnotation(Node *root, const expr &t); + + void AddEdgeToSolver(Edge *edge); + + void AddToProofCore(hash_set &core); + }; /** RPFP solver base class. */ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 6b32bb080..c582e19fc 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -125,6 +125,32 @@ namespace Duality { } } + int Z3User::CountOperatorsRec(hash_set &memo, const Term &t){ + if(memo.find(t) != memo.end()) + return 0; + memo.insert(t); + if(t.is_app()){ + decl_kind k = t.decl().get_decl_kind(); + if(k == And || k == Or){ + int count = 1; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + count += CountOperatorsRec(memo,t.arg(i)); + return count; + } + return 0; + } + if(t.is_quantifier()) + return CountOperatorsRec(memo,t.body())+1; + return 0; + } + + int Z3User::CountOperators(const Term &t){ + hash_set memo; + return CountOperatorsRec(memo,t); + } + + Z3User::Term Z3User::conjoin(const std::vector &args){ return ctx.make(And,args); } @@ -329,7 +355,15 @@ namespace Duality { res = f(args.size(),&args[0]); } else if (t.is_quantifier()) - res = CloneQuantifier(t,SubstRec(memo, t.body())); + { + std::vector pats; + t.get_patterns(pats); + for(unsigned i = 0; i < pats.size(); i++) + pats[i] = SubstRec(memo,pats[i]); + Term body = SubstRec(memo,t.body()); + res = clone_quantifier(t, body, pats); + } + // res = CloneQuantifier(t,SubstRec(memo, t.body())); else res = t; return res; } @@ -552,7 +586,7 @@ namespace Duality { void RPFP::ConstrainEdgeLocalized(Edge *e, const Term &tl) { e->constraints.push_back(tl); - stack.back().constraints.push_back(e); + stack.back().constraints.push_back(std::pair(e,tl)); slvr.add(tl); } @@ -1142,7 +1176,8 @@ namespace Duality { } } /* Unreachable! */ - std::cerr << "error in RPFP::ImplicantRed"; + // TODO: need to indicate this failure to caller + // std::cerr << "error in RPFP::ImplicantRed"; goto done; } else if(k == Not) { @@ -1161,6 +1196,31 @@ namespace Duality { done[truth].insert(f); } + void RPFP::ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set &done, hash_set &dont_cares){ + if(done.find(f) != done.end()) + return; /* already processed */ + if(f.is_app()){ + int nargs = f.num_args(); + 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); + goto done; + } + } + { + if(dont_cares.find(f) == dont_cares.end()){ + int b = SubtermTruth(memo,f); + if(b != 0 && b != 1) goto done; + expr bv = (b==1) ? f : !f; + lits.push_back(bv); + } + } + done: + done.insert(f); + } + RPFP::Term RPFP::ResolveIte(hash_map &memo, const Term &t, std::vector &lits, hash_set *done, hash_set &dont_cares){ if(resolve_ite_memo.find(t) != resolve_ite_memo.end()) @@ -1223,6 +1283,16 @@ namespace Duality { return conjoin(lits); } + RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set &dont_cares){ + /* first compute truth values of subterms */ + hash_map memo; + hash_set done; + std::vector lits; + ImplicantFullRed(memo,f,lits,done,dont_cares); + /* return conjunction of literals */ + return conjoin(lits); + } + struct VariableProjector : Z3User { struct elim_cand { @@ -1759,6 +1829,17 @@ namespace Duality { ConstrainEdgeLocalized(edge,eu); } + void RPFP::FixCurrentStateFull(Edge *edge){ + 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]; + Term eu = UnderapproxFullFormula(dual,dont_cares); + timer_stop("UnderapproxFormula"); + ConstrainEdgeLocalized(edge,eu); + } RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){ @@ -1803,6 +1884,7 @@ namespace Duality { res = CreateRelation(p->Annotation.IndParams,funder); } +#if 0 void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ // verify s.push(); @@ -1829,6 +1911,36 @@ namespace Duality { } } } +#endif + + void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ + std::vector lits(conjuncts.size()); + for(unsigned i = 0; i < lits.size(); i++){ + func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort()); + lits[i] = pred(); + s.add(ctx.make(Implies,lits[i],conjuncts[i])); + } + + // verify + check_result res = s.check(lits.size(),&lits[0]); + if(res != unsat) + throw "should be unsat"; + + for(unsigned i = 0; i < conjuncts.size(); ){ + std::swap(conjuncts[i],conjuncts.back()); + std::swap(lits[i],lits.back()); + check_result res = s.check(lits.size()-1,&lits[0]); + if(res != unsat){ + std::swap(conjuncts[i],conjuncts.back()); + std::swap(lits[i],lits.back()); + i++; + } + else { + conjuncts.pop_back(); + lits.pop_back(); + } + } + } void RPFP::NegateLits(std::vector &lits){ for(unsigned i = 0; i < lits.size(); i++){ @@ -1848,20 +1960,56 @@ namespace Duality { return ctx.make(Or,lits); } - void RPFP::Generalize(Node *node){ - std::vector conjuncts; - expr fmla = GetAnnotation(node); - CollectConjuncts(fmla,conjuncts,false); - // try to remove conjuncts one at a tme - aux_solver.push(); - Edge *edge = node->Outgoing; + // set up edge constraint in aux solver + void RPFP::AddEdgeToSolver(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); } - GreedyReduce(aux_solver,conjuncts); + } + + void RPFP::InterpolateByCases(Node *root, Node *node){ + aux_solver.push(); + AddEdgeToSolver(node->Outgoing); + node->Annotation.SetEmpty(); + hash_set *core = new hash_set; + core->insert(node->Outgoing->dual); + while(1){ + aux_solver.push(); + aux_solver.add(!GetAnnotation(node)); + if(aux_solver.check() == unsat){ + aux_solver.pop(1); + break; + } + dualModel = aux_solver.get_model(); + aux_solver.pop(1); + Push(); + FixCurrentStateFull(node->Outgoing); + ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + check_result foo = Check(root); + if(foo != unsat) + throw "should be unsat"; + AddToProofCore(*core); + Transformer old_annot = node->Annotation; + SolveSingleNode(root,node); + Pop(1); + node->Annotation.UnionWith(old_annot); + } + if(proof_core) + delete proof_core; // shouldn't happen + proof_core = core; + aux_solver.pop(1); + } + + void RPFP::Generalize(Node *root, Node *node){ + aux_solver.push(); + AddEdgeToSolver(node->Outgoing); + expr fmla = GetAnnotation(node); + std::vector conjuncts; + CollectConjuncts(fmla,conjuncts,false); + GreedyReduce(aux_solver,conjuncts); // try to remove conjuncts one at a tme aux_solver.pop(1); NegateLits(conjuncts); SetAnnotation(node,SimplifyOr(conjuncts)); @@ -1887,12 +2035,26 @@ namespace Duality { (*it)->dual = expr(ctx,NULL); for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) (*it)->dual = expr(ctx,NULL); - for(std::list::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) - (*it)->constraints.pop_back(); + for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + (*it).first->constraints.pop_back(); stack.pop_back(); } } + /** Erase the proof by performing a Pop, Push and re-assertion of + all the popped constraints */ + + void RPFP::PopPush(){ + slvr.pop(1); + slvr.push(); + stack_entry &back = stack.back(); + for(std::list::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it) + slvr.add((*it)->dual); + for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) + slvr.add((*it)->dual); + for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + slvr.add((*it).second); + } @@ -2325,13 +2487,17 @@ namespace Duality { } + void RPFP::AddToProofCore(hash_set &core){ + std::vector assumps; + slvr.get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++) + core.insert(assumps[i]); + } + void RPFP::ComputeProofCore(){ if(!proof_core){ - std::vector assumps; - slvr.get_proof().get_assumptions(assumps); proof_core = new hash_set; - for(unsigned i = 0; i < assumps.size(); i++) - proof_core->insert(assumps[i]); + AddToProofCore(*proof_core); } } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 86b95a657..40ddf25b1 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1754,12 +1754,14 @@ namespace Duality { for(unsigned i = 0; i < expansions.size(); i++){ Node *node = expansions[i]; tree->SolveSingleNode(top,node); - tree->Generalize(node); + if(expansions.size() == 1 && NodeTooComplicated(node)) + SimplifyNode(node); + tree->Generalize(top,node); if(RecordUpdate(node)) update_count++; } if(update_count == 0) - std::cout << "backtracked without learning\n"; + reporter->Message("backtracked without learning"); } tree->ComputeProofCore(); // need to compute the proof core before popping solver while(1) { @@ -1816,6 +1818,16 @@ namespace Duality { } } + bool NodeTooComplicated(Node *node){ + return tree->CountOperators(node->Annotation.Formula) > 5; + } + + void SimplifyNode(Node *node){ + // have to destroy the old proof to get a new interpolant + tree->PopPush(); + tree->InterpolateByCases(top,node); + } + bool LevelUsedInProof(unsigned level){ std::vector &expansions = stack[level].expansions; for(unsigned i = 0; i < expansions.size(); i++) diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index e70847d47..988b03d6d 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -34,8 +34,12 @@ namespace Duality { p.set_bool("proof", true); // this is currently useless p.set_bool("model", true); p.set_bool("unsat_core", true); + p.set_bool("mbqi",true); + 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 scoped_ptr sf = mk_smt_solver_factory(); m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); + m_solver->updt_params(p); // why do we have to do this? canceled = false; } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index fc94e53f2..c9860941b 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -413,6 +413,7 @@ namespace Duality { expr operator()(unsigned n, expr const * args) const; expr operator()(const std::vector &args) const; + expr operator()() const; expr operator()(expr const & a) const; expr operator()(int a) const; expr operator()(expr const & a1, expr const & a2) const; @@ -1184,6 +1185,9 @@ namespace Duality { inline expr func_decl::operator()(const std::vector &args) const { return operator()(args.size(),&args[0]); } + inline expr func_decl::operator()() const { + return operator()(0,0); + } inline expr func_decl::operator()(expr const & a) const { return operator()(1,&a); } diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 24df25f4e..f35dae93f 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -190,7 +190,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ op == Forall, names.size(), &types[0], &names[0], abs_body.get(), 0, - symbol(), + symbol("itp"), symbol(), 0, 0, 0, 0 @@ -761,6 +761,19 @@ int iz3mgr::occurs_in(ast var, ast e){ } +bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){ + if(op(x) == Plus){ + int n = num_args(x); + for(int i = 0; i < n; i++){ + if(arg(x,i) == v){ + res = z3_simplify(make(Sub, y, make(Sub, x, v))); + return true; + } + } + } + return false; +} + // find a controlling equality for a given variable v in a term // a controlling equality is of the form v = t, which, being // false would force the formula to have the specifid truth value @@ -774,6 +787,9 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, as if(!truth && op(e) == Equal){ if(arg(e,0) == v) return(arg(e,1)); if(arg(e,1) == v) return(arg(e,0)); + ast res; + if(solve_arith(v,arg(e,0),arg(e,1),res)) return res; + if(solve_arith(v,arg(e,1),arg(e,0),res)) return res; } if((!truth && op(e) == And) || (truth && op(e) == Or)){ int nargs = num_args(e); @@ -836,6 +852,14 @@ iz3mgr::ast iz3mgr::subst(stl_ext::hash_map &subst_memo,ast e){ // 2) bound variable must be equal to some term -> substitute iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){ + if((quantifier == Forall && op(e) == And) + || (quantifier == Exists && op(e) == Or)){ + int n = num_args(e); + std::vector args(n); + for(int i = 0; i < n; i++) + args[i] = apply_quant(quantifier,var,arg(e,i)); + return make(op(e),args); + } if(!occurs_in(var,e))return e; hash_set cont_eq_memo; ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e); diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 6d0daa89a..7bdc2ecce 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -692,13 +692,14 @@ class iz3mgr { protected: ast_manager &m_manager; + int occurs_in(ast var, ast e); private: ast mki(family_id fid, decl_kind sk, int n, raw_ast **args); ast make(opr op, int n, raw_ast **args); ast make(symb sym, int n, raw_ast **args); int occurs_in1(stl_ext::hash_map &occurs_in_memo, ast var, ast e); - int occurs_in(ast var, ast e); + bool solve_arith(const ast &v, const ast &x, const ast &y, ast &res); ast cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, ast v, ast e); ast subst(stl_ext::hash_map &subst_memo, ast var, ast t, ast e); diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index f8537d6eb..75d14bca1 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -135,10 +135,12 @@ class iz3proof_itp_impl : public iz3proof_itp { /* If p is a proof of Q and c is a normalization chain, then normal(p,c) is a proof of Q(c) (that is, Q with all substitutions in c performed). */ - + symb normal; - + /** Stand-ins for quantifiers */ + + symb sforall, sexists; ast get_placeholder(ast t){ @@ -231,6 +233,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast neg_pivot_lit = mk_not(atom); if(op(pivot) != Not) std::swap(premise1,premise2); + if(op(pivot) == Equal && op(arg(pivot,0)) == Select && op(arg(pivot,1)) == Select){ + neg_pivot_lit = mk_not(neg_pivot_lit); + std::swap(premise1,premise2); + } return resolve_arith_rec1(memo, neg_pivot_lit, premise1, premise2); } @@ -355,7 +361,13 @@ class iz3proof_itp_impl : public iz3proof_itp { break; } default: - res = itp2; + { + 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; + } } } return res; @@ -385,7 +397,13 @@ class iz3proof_itp_impl : public iz3proof_itp { break; } default: - res = itp1; + { + 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; + } } } return res; @@ -1897,6 +1915,20 @@ class iz3proof_itp_impl : public iz3proof_itp { return itp; } + ast capture_localization(ast e){ + // #define CAPTURE_LOCALIZATION +#ifdef CAPTURE_LOCALIZATION + for(int i = localization_vars.size() - 1; i >= 0; i--){ + LocVar &lv = localization_vars[i]; + if(occurs_in(lv.var,e)){ + symb q = (pv->in_range(lv.frame,rng)) ? sexists : sforall; + e = make(q,make(Equal,lv.var,lv.term),e); // use Equal because it is polymorphic + } + } +#endif + return e; + } + /** Make an axiom node. The conclusion must be an instance of an axiom. */ virtual node make_axiom(const std::vector &conclusion, prover::range frng){ int nargs = conclusion.size(); @@ -1920,7 +1952,7 @@ class iz3proof_itp_impl : public iz3proof_itp { for(unsigned i = 0; i < eqs.size(); i++) itp = make_mp(eqs[i],itp,pfs[i]); - return itp; + return capture_localization(itp); } virtual node make_axiom(const std::vector &conclusion){ @@ -2405,12 +2437,89 @@ class iz3proof_itp_impl : public iz3proof_itp { return new_var; } + ast delete_quant(hash_map &memo, const ast &v, const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + opr o = op(e); + switch(o){ + case Or: + case And: + case Implies: { + unsigned nargs = num_args(e); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = delete_quant(memo, v, arg(e,i)); + res = make(o,args); + break; + } + case Uninterpreted: { + symb s = sym(e); + ast w = arg(arg(e,0),0); + if(s == sforall || s == sexists){ + res = delete_quant(memo,v,arg(e,1)); + if(w != v) + res = make(s,w,res); + break; + } + } + default: + res = e; + } + } + return res; + } + + ast insert_quants(hash_map &memo, const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + opr o = op(e); + switch(o){ + case Or: + case And: + case Implies: { + unsigned nargs = num_args(e); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = insert_quants(memo, arg(e,i)); + res = make(o,args); + break; + } + case Uninterpreted: { + symb s = sym(e); + if(s == sforall || s == sexists){ + opr q = (s == sforall) ? Forall : Exists; + ast v = arg(arg(e,0),0); + hash_map dmemo; + ast body = delete_quant(dmemo,v,arg(e,1)); + body = insert_quants(memo,body); + res = apply_quant(q,v,body); + break; + } + } + default: + res = e; + } + } + return res; + } + ast add_quants(ast e){ +#ifdef CAPTURE_LOCALIZATION + if(!localization_vars.empty()){ + hash_map memo; + e = insert_quants(memo,e); + } +#else for(int i = localization_vars.size() - 1; i >= 0; i--){ LocVar &lv = localization_vars[i]; opr quantifier = (pv->in_range(lv.frame,rng)) ? Exists : Forall; e = apply_quant(quantifier,lv.var,e); } +#endif return e; } @@ -2446,7 +2555,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast npP = make_mp(make(Iff,nPloc,nP),npPloc,neqpf); ast nrP = make_resolution(nP,conj2,npP); ast res = make_resolution(Ploc,rP,nrP); - return res; + return capture_localization(res); } ast get_contra_coeff(const ast &f){ @@ -2538,6 +2647,10 @@ public: m().inc_ref(normal_chain); normal = function("@normal",2,boolbooldom,bool_type()); m().inc_ref(normal); + sforall = function("@sforall",2,boolbooldom,bool_type()); + m().inc_ref(sforall); + sexists = function("@sexists",2,boolbooldom,bool_type()); + m().inc_ref(sexists); } ~iz3proof_itp_impl(){ diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index f5506d35b..60fcd6fc4 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -27,6 +27,7 @@ void qi_params::updt_params(params_ref const & _p) { m_mbqi_max_iterations = p.mbqi_max_iterations(); m_mbqi_trace = p.mbqi_trace(); m_mbqi_force_template = p.mbqi_force_template(); + m_mbqi_id = p.mbqi_id(); m_qi_profile = p.qi_profile(); m_qi_profile_freq = p.qi_profile_freq(); m_qi_max_instances = p.qi_max_instances(); diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h index 0cd817f22..bca3ad3fc 100644 --- a/src/smt/params/qi_params.h +++ b/src/smt/params/qi_params.h @@ -51,6 +51,7 @@ struct qi_params { unsigned m_mbqi_max_iterations; bool m_mbqi_trace; unsigned m_mbqi_force_template; + const char * m_mbqi_id; qi_params(params_ref const & p = params_ref()): /* @@ -97,7 +98,9 @@ struct qi_params { m_mbqi_max_cexs_incr(1), m_mbqi_max_iterations(1000), m_mbqi_trace(false), - m_mbqi_force_template(10) { + m_mbqi_force_template(10), + m_mbqi_id(0) + { updt_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 07c68f759..50bb6422b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -21,6 +21,7 @@ def_module_params(module_name='smt', ('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'), ('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'), ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'), + ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'), ('qi.profile', BOOL, False, 'profile quantifier instantiation'), ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'), ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'), diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 53f3af961..526447f9f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -322,6 +322,7 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; + if(!m_qm->mbqi_enabled(q)) continue; if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n"; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index d56fe0cff..8fd0e08bc 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -335,6 +335,10 @@ namespace smt { return m_imp->m_plugin->model_based(); } + bool quantifier_manager::mbqi_enabled(quantifier *q) const { + return m_imp->m_plugin->mbqi_enabled(q); + } + void quantifier_manager::adjust_model(proto_model * m) { m_imp->m_plugin->adjust_model(m); } @@ -434,10 +438,24 @@ namespace smt { virtual bool model_based() const { return m_fparams->m_mbqi; } + virtual bool mbqi_enabled(quantifier *q) const { + if(!m_fparams->m_mbqi_id) return true; + const symbol &s = q->get_qid(); + unsigned len = strlen(m_fparams->m_mbqi_id); + if(s == symbol::null || s.is_numerical()) + return len == 0; + return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0; + } + + /* Quantifier id's must begin with the prefix specified by + parameter mbqi.id to be instantiated with MBQI. The default + value is the empty string, so all quantifiers are + instantiated. + */ virtual void add(quantifier * q) { - if (m_fparams->m_mbqi) { - m_model_finder->register_quantifier(q); - } + if (m_fparams->m_mbqi && mbqi_enabled(q)) { + m_model_finder->register_quantifier(q); + } } virtual void del(quantifier * q) { diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 19113229c..e3d626157 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -75,6 +75,7 @@ namespace smt { }; bool model_based() const; + bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? void adjust_model(proto_model * m); check_model_result check_model(proto_model * m, obj_map const & root2value); @@ -144,6 +145,11 @@ namespace smt { */ virtual bool model_based() const = 0; + /** + \brief Is "model based" instantiate allowed to instantiate this quantifier? + */ + virtual bool mbqi_enabled(quantifier *q) const {return true;} + /** \brief Give a change to the plugin to adjust the interpretation of unintepreted functions. It can basically change the "else" of each uninterpreted function.