diff --git a/src/duality/duality.h b/src/duality/duality.h old mode 100644 new mode 100755 index 8c469b9e4..e1d058f10 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1184,7 +1184,13 @@ namespace Duality { hash_map EdgeCloneMap; std::vector alit_stack; std::vector alit_stack_sizes; - hash_map > edge_solvers; + + // to let us use one solver per edge + struct edge_solver { + hash_map AssumptionLits; + uptr slvr; + }; + hash_map edge_solvers; #ifdef LIMIT_STACK_WEIGHT struct weight_counter { @@ -1236,19 +1242,23 @@ namespace Duality { void GetTermTreeAssertionLiteralsRec(TermTree *assumptions); - LogicSolver *SolverForEdge(Edge *edge, bool models); + edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms); public: struct scoped_solver_for_edge { - LogicSolver *orig_ls; + solver *orig_slvr; RPFP_caching *rpfp; - scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){ + edge_solver *es; + scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){ rpfp = _rpfp; - orig_ls = rpfp->ls; - rpfp->ls = rpfp->SolverForEdge(edge,models); + orig_slvr = rpfp->ls->slvr; + es = &(rpfp->SolverForEdge(edge,models,axioms)); + rpfp->ls->slvr = es->slvr.get(); + rpfp->AssumptionLits.swap(es->AssumptionLits); } ~scoped_solver_for_edge(){ - rpfp->ls = orig_ls; + rpfp->ls->slvr = orig_slvr; + rpfp->AssumptionLits.swap(es->AssumptionLits); } }; diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp old mode 100644 new mode 100755 index 2d52ab283..5751fa890 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2711,10 +2711,12 @@ namespace Duality { const std::vector &theory = ls->get_axioms(); for(unsigned i = 0; i < theory.size(); i++) s.add(theory[i]); - if(s.check(lits.size(),&lits[0]) != unsat) - throw "should be unsat"; + for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something! + if(s.check(lits.size(),&lits[0]) == unsat) + goto is_unsat; + throw "should be unsat"; } - + is_unsat: for(unsigned i = 0; i < conjuncts.size(); ){ std::swap(conjuncts[i],conjuncts.back()); std::swap(lits[i],lits.back()); @@ -2747,8 +2749,20 @@ namespace Duality { // verify check_result res = CheckCore(lits,full_core); - if(res != unsat) + if(res != unsat){ + // 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++) + GetAssumptionLits(theory[i],assumps); + lits = assumps; + std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); + + for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something! + if((res = CheckCore(lits,full_core)) == unsat) + goto is_unsat; throw "should be unsat"; + } + is_unsat: FilterCore(core,full_core); std::vector dummy; @@ -2889,13 +2903,20 @@ namespace Duality { timer_stop("Generalize"); } - RPFP::LogicSolver *RPFP_caching::SolverForEdge(Edge *edge, bool models){ - uptr &p = edge_solvers[edge]; + RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models, bool axioms){ + edge_solver &es = edge_solvers[edge]; + uptr &p = es.slvr; if(!p.get()){ scoped_no_proof no_proofs_please(ctx.m()); // no proofs - p.set(new iZ3LogicSolver(ctx,models)); // no models + p.set(new solver(ctx,true,models)); // no models + if(axioms){ + RPFP::LogicSolver *ls = edge->owner->ls; + const std::vector &axs = ls->get_axioms(); + for(unsigned i = 0; i < axs.size(); i++) + p.get()->add(axs[i]); + } } - return p.get(); + return es; } @@ -3362,6 +3383,8 @@ namespace Duality { } } + bool some_labels = false; + // create the edges for(unsigned i = 0; i < clauses.size(); i++){ @@ -3397,17 +3420,23 @@ namespace Duality { Term labeled = body; std::vector lbls; // TODO: throw this away for now body = RemoveLabels(body,lbls); + if(!eq(labeled,body)) + some_labels = true; // remember if there are labels, as we then can't do qe_lite // body = IneqToEq(body); // UFO converts x=y to (x<=y & x >= y). Undo this. body = body.simplify(); #ifdef USE_QE_LITE std::set idxs; - for(unsigned j = 0; j < Indparams.size(); j++) - if(Indparams[j].is_var()) - idxs.insert(Indparams[j].get_index_value()); - body = body.qe_lite(idxs,false); + if(!some_labels){ // can't do qe_lite if we have to reconstruct labels + for(unsigned j = 0; j < Indparams.size(); j++) + if(Indparams[j].is_var()) + idxs.insert(Indparams[j].get_index_value()); + body = body.qe_lite(idxs,false); + } hash_map > sb_memo; body = SubstBoundRec(sb_memo,substs[i],0,body); + if(some_labels) + labeled = SubstBoundRec(sb_memo,substs[i],0,labeled); for(unsigned j = 0; j < Indparams.size(); j++) Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]); #endif diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp old mode 100644 new mode 100755 index 973ad769c..1c2f2c927 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -51,12 +51,17 @@ Revision History: // #define TOP_DOWN // #define EFFORT_BOUNDED_STRAT #define SKIP_UNDERAPPROX_NODES -#define USE_RPFP_CLONE // #define KEEP_EXPANSIONS // #define USE_CACHING_RPFP // #define PROPAGATE_BEFORE_CHECK + +#define USE_RPFP_CLONE #define USE_NEW_GEN_CANDS +//#define NO_PROPAGATE +//#define NO_GENERALIZE +//#define NO_DECISIONS + namespace Duality { // TODO: must be a better place for this... @@ -129,13 +134,11 @@ namespace Duality { { scoped_no_proof no_proofs_please(ctx.m()); #ifdef USE_RPFP_CLONE - clone_ls = new RPFP::iZ3LogicSolver(ctx, false); // no models needed for this one - clone_rpfp = new RPFP_caching(clone_ls); + clone_rpfp = new RPFP_caching(rpfp->ls); clone_rpfp->Clone(rpfp); #endif #ifdef USE_NEW_GEN_CANDS - gen_cands_ls = new RPFP::iZ3LogicSolver(ctx); - gen_cands_rpfp = new RPFP_caching(gen_cands_ls); + gen_cands_rpfp = new RPFP_caching(rpfp->ls); gen_cands_rpfp->Clone(rpfp); #endif } @@ -144,20 +147,16 @@ namespace Duality { ~Duality(){ #ifdef USE_RPFP_CLONE delete clone_rpfp; - delete clone_ls; #endif #ifdef USE_NEW_GEN_CANDS delete gen_cands_rpfp; - delete gen_cands_ls; #endif } #ifdef USE_RPFP_CLONE - RPFP::LogicSolver *clone_ls; RPFP_caching *clone_rpfp; #endif #ifdef USE_NEW_GEN_CANDS - RPFP::LogicSolver *gen_cands_ls; RPFP_caching *gen_cands_rpfp; #endif @@ -1255,7 +1254,7 @@ namespace Duality { slvr.pop(1); delete checker; #else - RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */); + 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){ @@ -1940,11 +1939,15 @@ namespace Duality { 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 if(expansions.size() == 1 && NodeTooComplicated(node)) SimplifyNode(node); else node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); Generalize(node); +#endif if(RecordUpdate(node)) update_count++; else @@ -1984,7 +1987,9 @@ namespace Duality { if(stack.size() == 1)break; if(prev_level_used){ Node *node = stack.back().expansions[0]; +#ifndef NO_PROPAGATE if(!Propagate(node)) break; +#endif if(!RecordUpdate(node)) break; // shouldn't happen! RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list propagated = true; @@ -2006,11 +2011,13 @@ 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++){ tree->FixCurrentState(expansions[i]->Outgoing); } +#endif #if 0 if(tree->slvr().check() == unsat) throw "help!"; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp old mode 100644 new mode 100755 diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp old mode 100644 new mode 100755 index 6664cd2fe..35dc67bcd --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -249,6 +249,9 @@ iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector &_args){ void iz3mgr::show(ast t){ + if(t.null()){ + std::cout << "(null)" << std::endl; + } params_ref p; p.set_bool("flat_assoc",false); std::cout << mk_pp(t.raw(), m(), p) << std::endl; @@ -693,10 +696,13 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){ throw "not an inequality"; } } - Qrhs = make(Times,c,Qrhs); - bool pstrict = op(P) == Lt, strict = pstrict || qstrict; - if(pstrict && qstrict && round_off) + bool pstrict = op(P) == Lt; + if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){ Qrhs = make(Sub,Qrhs,make_int(rational(1))); + qstrict = false; + } + Qrhs = make(Times,c,Qrhs); + bool strict = pstrict || qstrict; if(strict) P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs)); else @@ -881,3 +887,14 @@ iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){ std::vector bvs; bvs.push_back(var); return make_quant(quantifier,bvs,e); } + +#if 0 +void iz3mgr::get_bound_substitutes(stl_ext::hash_map &memo, const ast &e, const ast &var, std::vector &substs){ + std::pair foo(e,false); + std::pair::iterator,bool> bar = memo.insert(foo); + if(bar.second){ + if(op(e) == + } + +} +#endif diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h old mode 100644 new mode 100755 diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp old mode 100644 new mode 100755 index 61ed78463..303d90b1b --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -579,18 +579,36 @@ class iz3proof_itp_impl : public iz3proof_itp { return is_ineq(ineq); } + ast destruct_cond_ineq(const ast &ineq, ast &Aproves, ast &Bproves){ + ast res = ineq; + opr o = op(res); + if(o == And){ + Aproves = my_and(Aproves,arg(res,0)); + res = arg(res,1); + o = op(res); + } + if(o == Implies){ + Bproves = my_and(Bproves,arg(res,0)); + res = arg(res,1); + } + return res; + } + ast simplify_sum(std::vector &args){ ast Aproves = mk_true(), Bproves = mk_true(); - ast ineq = args[0]; + ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves); if(!is_normal_ineq(ineq)) throw cannot_simplify(); sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves); return my_and(Aproves,my_implies(Bproves,ineq)); } ast simplify_rotate_sum(const ast &pl, const ast &pf){ - ast cond = mk_true(); + ast Aproves = mk_true(), Bproves = mk_true(); ast ineq = make(Leq,make_int("0"),make_int("0")); - return rotate_sum_rec(pl,pf,cond,ineq); + ineq = rotate_sum_rec(pl,pf,Aproves,Bproves,ineq); + if(is_true(Aproves) && is_true(Bproves)) + return ineq; + return my_and(Aproves,my_implies(Bproves,ineq)); } bool is_rewrite_chain(const ast &chain){ @@ -623,7 +641,11 @@ class iz3proof_itp_impl : public iz3proof_itp { void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){ opr o = op(ineq2); - if(o == Implies){ + if(o == And){ + sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves); + Aproves = my_and(Aproves,arg(ineq2,0)); + } + else if(o == Implies){ sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves); Bproves = my_and(Bproves,arg(ineq2,0)); } @@ -683,23 +705,20 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor)); } - ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){ - if(pf == pl) - return my_implies(Bproves,simplify_ineq(ineq)); + ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Aproves, ast &Bproves, ast &ineq){ + if(pf == pl){ + if(sym(ineq) == normal) + return ineq; + return simplify_ineq(ineq); + } if(op(pf) == Uninterpreted && sym(pf) == sum){ if(arg(pf,2) == pl){ - ast Aproves = mk_true(); sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves); - if(!is_true(Aproves)) - throw "help!"; ineq = idiv_ineq(ineq,arg(pf,1)); - return my_implies(Bproves,ineq); + return ineq; } - ast Aproves = mk_true(); sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves); - if(!is_true(Aproves)) - throw "help!"; - return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq); + return rotate_sum_rec(pl,arg(pf,0),Aproves,Bproves,ineq); } throw cannot_simplify(); } @@ -749,6 +768,28 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; } + ast unmixed_eq2ineq(const ast &lhs, const ast &rhs, opr comp_op, const ast &equa, ast &cond){ + ast ineqs= chain_ineqs(comp_op,LitA,equa,lhs,rhs); // chain must be from lhs to rhs + cond = my_and(cond,chain_conditions(LitA,equa)); + ast Bconds = z3_simplify(chain_conditions(LitB,equa)); + if(is_true(Bconds) && op(ineqs) != And) + return my_implies(cond,ineqs); + if(op(ineqs) != And) + return my_and(Bconds,my_implies(cond,ineqs)); + throw "help!"; + } + + ast add_mixed_eq2ineq(const ast &lhs, const ast &rhs, const ast &equa, const ast &itp){ + if(is_true(equa)) + return itp; + std::vector args(3); + args[0] = itp; + args[1] = make_int("1"); + ast ineq = make(Leq,make_int(rational(0)),make_int(rational(0))); + args[2] = make_normal(ineq,cons_normal(fix_normal(lhs,rhs,equa),mk_true())); + 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(); @@ -756,20 +797,21 @@ class iz3proof_itp_impl : public iz3proof_itp { if(is_equivrel_chain(equa)){ ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs); - if(lhst != LitMixed && rhst != LitMixed){ - ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs - cond = my_and(cond,chain_conditions(LitA,equa)); - ast Bconds = z3_simplify(chain_conditions(LitB,equa)); - if(is_true(Bconds) && op(ineqs) != And) - return my_implies(cond,ineqs); - } + if(lhst != LitMixed && rhst != LitMixed) + return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond); else { - ast itp = make(Leq,make_int(rational(0)),make_int(rational(0))); - return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true())); + ast left, left_term, middle, right_term, right; + left = get_left_movers(equa,lhs,middle,left_term); + middle = get_right_movers(middle,rhs,right,right_term); + ast itp = unmixed_eq2ineq(left_term, right_term, op(arg(neg_equality,0)), middle, cond); + // itp = my_implies(cond,itp); + itp = add_mixed_eq2ineq(lhs, left_term, left, itp); + itp = add_mixed_eq2ineq(right_term, rhs, right, itp); + return itp; } } } - throw cannot_simplify(); + throw "help!"; } void reverse_modpon(std::vector &args){ @@ -836,6 +878,8 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equa = sep_cond(args[0],cond); if(is_equivrel_chain(equa)) return my_implies(cond,reverse_chain(equa)); + if(is_negation_chain(equa)) + return commute_negation_chain(equa); throw cannot_simplify(); } @@ -909,7 +953,9 @@ class iz3proof_itp_impl : public iz3proof_itp { get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves); ast itp; if(is_rewrite_side(LitA,head)){ - itp = ineq1; + itp = make(Leq,make_int("0"),make_int("0")); + linear_comb(itp,make_int("1"),ineq1); // make sure it is normal form + //itp = ineq1; ast mc = z3_simplify(chain_side_proves(LitB,pref)); Bproves = my_and(Bproves,mc); } @@ -951,7 +997,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast simplify_modpon(const std::vector &args){ ast Aproves = mk_true(), Bproves = mk_true(); ast chain = simplify_modpon_fwd(args,Bproves); - ast Q2 = sep_cond(args[2],Bproves); + ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves); ast interp; if(is_normal_ineq(Q2)){ // inequalities are special ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves); @@ -1450,6 +1496,50 @@ class iz3proof_itp_impl : public iz3proof_itp { return is_negation_chain(rest); } + ast commute_negation_chain(const ast &chain){ + if(is_true(chain)) + return chain; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + if(is_true(rest)){ + ast old = rewrite_rhs(last); + if(!(op(old) == Not)) + throw "bad negative equality chain"; + ast equ = arg(old,0); + if(!is_equivrel(equ)) + throw "bad negative equality chain"; + last = rewrite_update_rhs(last,top_pos,make(Not,make(op(equ),arg(equ,1),arg(equ,0))),make(True)); + return chain_cons(rest,last); + } + ast pos = rewrite_pos(last); + if(pos == top_pos) + throw "bad negative equality chain"; + int idx = pos_arg(pos); + if(idx != 0) + throw "bad negative equality chain"; + pos = arg(pos,1); + if(pos == top_pos){ + ast lhs = rewrite_lhs(last); + ast rhs = rewrite_rhs(last); + if(op(lhs) != Equal || op(rhs) != Equal) + throw "bad negative equality chain"; + last = make_rewrite(rewrite_side(last),rewrite_pos(last),rewrite_cond(last), + make(Iff,make(Equal,arg(lhs,1),arg(lhs,0)),make(Equal,arg(rhs,1),arg(rhs,0)))); + } + else { + idx = pos_arg(pos); + if(idx == 0) + idx = 1; + else if(idx == 1) + idx = 0; + else + throw "bad negative equality chain"; + pos = pos_add(0,pos_add(idx,arg(pos,1))); + last = make_rewrite(rewrite_side(last),pos,rewrite_cond(last),rewrite_equ(last)); + } + return chain_cons(commute_negation_chain(rest),last); + } + // split a rewrite chain into head and tail at last top-level rewrite ast get_head_chain(const ast &chain, ast &tail, bool is_not = true){ ast last = chain_last(chain); @@ -1466,6 +1556,47 @@ class iz3proof_itp_impl : public iz3proof_itp { return head; } + // split a rewrite chain into head and tail at last non-mixed term + ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){ + if(is_true(chain) || get_term_type(rhs) != LitMixed){ + mid = rhs; + tail = mk_true(); + return chain; + } + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast mm = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last)); + ast res = get_right_movers(rest,mm,tail,mid); + tail = chain_cons(tail,last); + return res; + } + + // split a rewrite chain into head and tail at first non-mixed term + ast get_left_movers(const ast &chain, const ast &lhs, ast &tail, ast &mid){ + if(is_true(chain)){ + mid = lhs; + if(get_term_type(lhs) != LitMixed){ + tail = mk_true(); + return chain; + } + return ast(); + } + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast res = get_left_movers(rest,lhs,tail,mid); + if(res.null()){ + mid = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last)); + if(get_term_type(mid) != LitMixed){ + tail = mk_true(); + return chain; + } + return ast(); + } + tail = chain_cons(tail,last); + return res; + } + + struct cannot_split {}; /** Split a chain of rewrites two chains, operating on positions 0 and 1. @@ -1668,11 +1799,13 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){ + LitType lhst = get_term_type(lhs); LitType rhst = get_term_type(rhs); - if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs)) + if(lhst == LitMixed && (rhst != LitMixed || ast_id(lhs) < ast_id(rhs))) return make_normal_step(lhs,rhs,proof); - else + if(rhst == LitMixed && (lhst != LitMixed || ast_id(rhs) < ast_id(lhs))) return make_normal_step(rhs,lhs,reverse_chain(proof)); + throw "help!"; } ast chain_side_proves(LitType side, const ast &chain){ @@ -1692,8 +1825,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast lhs2 = normal_lhs(f2); int id1 = ast_id(lhs1); int id2 = ast_id(lhs2); - if(id1 < id2) return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves)); - if(id2 < id1) return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves)); + if(id1 < id2) + return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves)); + if(id2 < id1) + return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves)); ast rhs1 = normal_rhs(f1); ast rhs2 = normal_rhs(f2); LitType t1 = get_term_type(rhs1); @@ -1719,9 +1854,13 @@ class iz3proof_itp_impl : public iz3proof_itp { Aproves = my_and(Aproves,mcB); ast rep = apply_rewrite_chain(rhs1,Aproof); new_proof = concat_rewrite_chain(pf1,Aproof); - new_normal = make_normal_step(rhs1,rep,new_proof); + new_normal = make_normal_step(lhs1,rep,new_proof); + ast A_normal = make_normal_step(rhs1,rep,Aproof); + ast res = cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves)); + res = merge_normal_chains_rec(res,cons_normal(A_normal,make(True)),trans,Aproves,Bproves); + return res; } - else if(t1 == LitA && t2 == LitB) + else if(t1 == LitB && t2 == LitA) return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); else if(t1 == LitA) { ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); @@ -1743,17 +1882,20 @@ class iz3proof_itp_impl : public iz3proof_itp { return chain; ast f = normal_first(chain); ast r = normal_rest(chain); + r = trans_normal_chain(r,trans); ast rhs = normal_rhs(f); hash_map::iterator it = trans.find(rhs); ast new_normal; - if(it != trans.end()){ + if(it != trans.end() && get_term_type(normal_lhs(f)) == LitMixed){ const ast &f2 = it->second; ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2)); new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf); } else new_normal = f; - return cons_normal(new_normal,trans_normal_chain(r,trans)); + if(get_term_type(normal_lhs(f)) == LitMixed) + trans[normal_lhs(f)] = new_normal; + return cons_normal(new_normal,r); } ast merge_normal_chains(const ast &chain1, const ast &chain2, ast &Aproves, ast &Bproves){ @@ -2011,8 +2153,14 @@ class iz3proof_itp_impl : public iz3proof_itp { /** Make a Reflexivity node. This rule produces |- x = x */ virtual node make_reflexivity(ast con){ - throw proof_error(); -} + if(get_term_type(con) == LitA) + return mk_false(); + if(get_term_type(con) == LitB) + return mk_true(); + ast itp = make(And,make(contra,no_proof,mk_false()), + make(contra,mk_true(),mk_not(con))); + return itp; + } /** Make a Symmetry node. This takes a derivation of |- x = y and produces | y = x. Ditto for ~(x=y) */ @@ -2247,10 +2395,19 @@ class iz3proof_itp_impl : public iz3proof_itp { throw proof_error(); } } - Qrhs = make(Times,c,Qrhs); +#if 0 bool pstrict = op(P) == Lt, strict = pstrict || qstrict; if(pstrict && qstrict && round_off) Qrhs = make(Sub,Qrhs,make_int(rational(1))); +#else + bool pstrict = op(P) == Lt; + if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){ + Qrhs = make(Sub,Qrhs,make_int(rational(1))); + qstrict = false; + } + Qrhs = make(Times,c,Qrhs); + bool strict = pstrict || qstrict; +#endif if(strict) P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs)); else @@ -2269,8 +2426,14 @@ class iz3proof_itp_impl : public iz3proof_itp { itp = mk_true(); break; default: { // mixed equality - if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed) - std::cerr << "WARNING: mixed term in leq2eq\n"; + if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed){ + // std::cerr << "WARNING: mixed term in leq2eq\n"; + std::vector lits; + lits.push_back(con); + lits.push_back(make(Not,xleqy)); + lits.push_back(make(Not,yleqx)); + return make_axiom(lits); + } std::vector conjs; conjs.resize(3); conjs[0] = mk_not(con); conjs[1] = xleqy; @@ -2405,7 +2568,15 @@ class iz3proof_itp_impl : public iz3proof_itp { frng = srng; // this term will be localized } else if(o == Plus || o == Times){ // don't want bound variables inside arith ops - frng = erng; // this term will be localized + // std::cout << "WARNING: non-local arithmetic\n"; + // frng = erng; // this term will be localized + } + else if(o == Select){ // treat the array term like a function symbol + prover::range srng = pv->ast_scope(arg(e,0)); + if(!(srng.lo > srng.hi) && pv->ranges_intersect(srng,rng)) // localize to desired range if possible + frng = pv->range_glb(srng,rng); + else + frng = srng; // this term will be localized } std::vector largs(nargs); std::vector eqs; @@ -2434,7 +2605,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return e; // this term occurs in range, so it's O.K. if(is_array_type(get_type(e))) - throw "help!"; + std::cerr << "WARNING: array quantifier\n"; // choose a frame for the constraint that is close to range int frame = pv->range_near(pv->ast_scope(e),rng); diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 6a1b665cf..9eac5f040 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -188,6 +188,15 @@ public: get_Z3_lits(con, lits); iproof->make_axiom(lits); } +#ifdef LOCALIZATION_KLUDGE + else if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST + && get_locality_rec(prem(proof,1)) == INT_MAX){ + std::vector lits; + ast con = conc(proof); + get_Z3_lits(con, lits); + iproof->make_axiom(lits); + } +#endif else { unsigned nprems = num_prems(proof); for(unsigned i = 0; i < nprems; i++){ @@ -1271,6 +1280,84 @@ public: return make(Plus,args); } + + ast replace_summands_with_fresh_vars(const ast &t, hash_map &map){ + if(op(t) == Plus){ + int nargs = num_args(t); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = replace_summands_with_fresh_vars(arg(t,i),map); + return make(Plus,args); + } + if(op(t) == Times) + return make(Times,arg(t,0),replace_summands_with_fresh_vars(arg(t,1),map)); + if(map.find(t) == map.end()) + map[t] = mk_fresh_constant("@s",get_type(t)); + return map[t]; + } + + ast painfully_normalize_ineq(const ast &ineq, hash_map &map){ + ast res = normalize_inequality(ineq); + ast lhs = arg(res,0); + lhs = replace_summands_with_fresh_vars(lhs,map); + res = make(op(res),SortSum(lhs),arg(res,1)); + return res; + } + + Iproof::node painfully_reconstruct_farkas(const std::vector &prems, const std::vector &pfs, const ast &con){ + int nprems = prems.size(); + std::vector pcons(nprems),npcons(nprems); + hash_map pcon_to_pf, npcon_to_pcon, pain_map; + for(int i = 0; i < nprems; i++){ + pcons[i] = conc(prems[i]); + npcons[i] = painfully_normalize_ineq(pcons[i],pain_map); + pcon_to_pf[npcons[i]] = pfs[i]; + npcon_to_pcon[npcons[i]] = pcons[i]; + } + // ast leq = make(Leq,arg(con,0),arg(con,1)); + ast ncon = painfully_normalize_ineq(mk_not(con),pain_map); + pcons.push_back(mk_not(con)); + npcons.push_back(ncon); + // ast assumps = make(And,pcons); + ast new_proof; + if(is_sat(npcons,new_proof)) + throw "Proof error!"; + pfrule dk = pr(new_proof); + int nnp = num_prems(new_proof); + std::vector my_prems; + std::vector farkas_coeffs, my_pcons; + + if(dk == PR_TH_LEMMA + && get_theory_lemma_theory(new_proof) == ArithTheory + && get_theory_lemma_kind(new_proof) == FarkasKind) + get_farkas_coeffs(new_proof,farkas_coeffs); + else if(dk == PR_UNIT_RESOLUTION && nnp == 2){ + for(int i = 0; i < nprems; i++) + farkas_coeffs.push_back(make_int(rational(1))); + } + else + throw "cannot reconstruct farkas proof"; + + for(int i = 0; i < nnp; i++){ + ast p = conc(prem(new_proof,i)); + p = really_normalize_ineq(p); + if(pcon_to_pf.find(p) != pcon_to_pf.end()){ + my_prems.push_back(pcon_to_pf[p]); + my_pcons.push_back(npcon_to_pcon[p]); + } + else if(p == ncon){ + my_prems.push_back(iproof->make_hypothesis(mk_not(con))); + my_pcons.push_back(mk_not(con)); + } + else + throw "cannot reconstruct farkas proof"; + } + Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs); + return res; + } + + + ast really_normalize_ineq(const ast &ineq){ ast res = normalize_inequality(ineq); res = make(op(res),SortSum(arg(res,0)),arg(res,1)); @@ -1309,7 +1396,7 @@ public: farkas_coeffs.push_back(make_int(rational(1))); } else - throw "cannot reconstruct farkas proof"; + return painfully_reconstruct_farkas(prems,pfs,con); for(int i = 0; i < nnp; i++){ ast p = conc(prem(new_proof,i)); @@ -1452,9 +1539,11 @@ public: lits.push_back(from_ast(con)); // pattern match some idioms - if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST && pr(prem(proof,1)) == PR_REWRITE ) { - res = iproof->make_axiom(lits); - return res; + if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST){ + if(get_locality_rec(prem(proof,1)) == INT_MAX) { + res = iproof->make_axiom(lits); + return res; + } } if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){ Iproof::node clause = translate_main(prem(proof,0),true); @@ -1465,12 +1554,20 @@ public: if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or) std::cout << "foo!\n"; +#if 0 if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){ Iproof::node clause = translate_main(prem(proof,0),true); res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast. return res; } + if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,0)) == PR_COMMUTATIVITY){ + Iproof::node clause = translate_main(prem(proof,1),true); + res = make(commute,clause,conc(prem(proof,1))); // HACK -- we depend on Iproof::node being same as ast. + return res; + } +#endif + if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){ try { res = CombineEqPropagate(proof); @@ -1627,9 +1724,10 @@ public: break; case ArrayTheory: {// nothing fancy for this ast store_array; - if(!get_store_array(con,store_array)) - throw unsupported(); - res = iproof->make_axiom(lits,ast_scope(store_array)); + if(get_store_array(con,store_array)) + res = iproof->make_axiom(lits,ast_scope(store_array)); + else + res = iproof->make_axiom(lits); // for array extensionality axiom break; } default: @@ -1653,6 +1751,12 @@ public: res = args[0]; break; } + case PR_COMMUTATIVITY: { + ast comm_equiv = make(op(con),arg(con,0),arg(con,0)); + ast pf = iproof->make_reflexivity(comm_equiv); + res = make(commute,pf,comm_equiv); + break; + } default: assert(0 && "translate_main: unsupported proof rule"); throw unsupported(); diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp old mode 100644 new mode 100755