diff --git a/src/duality/duality.h b/src/duality/duality.h index fe86ed2ec..a37896af1 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -118,6 +118,8 @@ protected: expr FinishAndOr(const std::vector &args, bool is_and); expr PullCommonFactors(std::vector &args, bool is_and); Term IneqToEqRec(hash_map &memo, const Term &t); + Term CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall); + Term PushQuantifier(const expr &t, const expr &body, bool is_forall); }; diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 25c5f9c7d..3cbeafa77 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -548,24 +548,50 @@ 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); + Z3User::Term Z3User::PushQuantifier(const expr &t, const expr &body, bool is_forall){ + if(t.get_quantifier_num_bound() == 1){ + std::vector fmlas,free,not_free; + CollectConjuncts(body,fmlas, !is_forall); + for(unsigned i = 0; i < fmlas.size(); i++){ + const expr &fmla = fmlas[i]; + if(fmla.has_free(0)) + free.push_back(fmla); + else + not_free.push_back(fmla); + } + decl_kind op = is_forall ? Or : And; + if(free.empty()) + return SimplifyAndOr(not_free,op == And); + expr q = clone_quantifier(is_forall ? Forall : Exists,t, SimplifyAndOr(free, op == And)); + if(!not_free.empty()) + q = ctx.make(op,q,SimplifyAndOr(not_free, op == And)); + return q; } - 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(is_forall ? Forall : Exists,t,body); + } + + Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall){ + if(body.is_app()){ + if(body.decl().get_decl_kind() == (is_forall ? And : Or)){ // quantifier distributes + int nargs = body.num_args(); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = CloneQuantAndSimp(t, body.arg(i), is_forall); + return SimplifyAndOr(args, body.decl().get_decl_kind() == And); + } + else if(body.decl().get_decl_kind() == is_forall ? And : Or){ // quantifier distributes + return PushQuantifier(t,body,is_forall); // may distribute partially + } + else if(body.decl().get_decl_kind() == Not){ + return CloneQuantAndSimp(t,body.arg(0),!is_forall); + } } return clone_quantifier(t,body); } + Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){ + return CloneQuantAndSimp(t,body,t.is_quantifier_forall()); + } Z3User::Term Z3User::SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val){ std::pair foo(t,expr(ctx)); @@ -659,7 +685,7 @@ namespace Duality { else if (t.is_quantifier()) { Term body = RemoveRedundancyRec(memo,smemo,t.body()); - res = clone_quantifier(t, body); + res = CloneQuantAndSimp(t, body); } else res = t; return res; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 2a699a995..d5c9a9575 100755 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -374,6 +374,12 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, &_patterns[0], to_expr(b.raw()))); } + expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){ + quantifier *thing = to_quantifier(q.raw()); + bool is_forall = dk == Forall; + return q.ctx().cook(q.m().update_quantifier(thing, is_forall, to_expr(b.raw()))); + } + void expr::get_patterns(std::vector &pats) const { quantifier *thing = to_quantifier(raw()); unsigned num_patterns = thing->get_num_patterns(); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 0861ab791..a85b3981d 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -466,6 +466,11 @@ namespace Duality { bool is_label (bool &pos,std::vector &names) const ; bool is_ground() const {return to_app(raw())->is_ground();} bool has_quantifiers() const {return to_app(raw())->has_quantifiers();} + bool has_free(int idx) const { + used_vars proc; + proc.process(to_expr(raw())); + return proc.contains(idx); + } // operator Z3_app() const { assert(is_app()); return reinterpret_cast(m_ast); } func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());} @@ -573,6 +578,8 @@ namespace Duality { friend expr clone_quantifier(const expr &q, const expr &b, const std::vector &patterns); + friend expr clone_quantifier(decl_kind, const expr &, const expr &); + friend std::ostream & operator<<(std::ostream & out, expr const & m){ m.ctx().print_expr(out,m); return out; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 2a4c4bd85..c880d60aa 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -814,6 +814,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equa = sep_cond(arg(pf,0),cond); if(is_equivrel_chain(equa)){ ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove + if(!rewrites_from_to(equa,lhs,rhs)){ + lhs = arg(arg(neg_equality,0),0); // the equality proved is ambiguous, sadly + rhs = arg(arg(neg_equality,0),1); + } LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs); if(lhst != LitMixed && rhst != LitMixed) return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond); @@ -1671,9 +1675,20 @@ class iz3proof_itp_impl : public iz3proof_itp { return head; } - // split a rewrite chain into head and tail at last non-mixed term + bool has_mixed_summands(const ast &e){ + if(op(e) == Plus){ + int nargs = num_args(e); + for(int i = 0; i < nargs; i++) + if(has_mixed_summands(arg(e,i))) + return true; + return false; + } + return get_term_type(e) == LitMixed; + } + + // split a rewrite chain into head and tail at last sum with no mixed sumands ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){ - if(is_true(chain) || get_term_type(rhs) != LitMixed){ + if(is_true(chain) || !has_mixed_summands(rhs)){ mid = rhs; tail = mk_true(); return chain; @@ -1686,11 +1701,11 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; } - // split a rewrite chain into head and tail at first non-mixed term + // split a rewrite chain into head and tail at first sum with no mixed sumands 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){ + if(!has_mixed_summands(lhs)){ tail = mk_true(); return chain; } @@ -1790,10 +1805,21 @@ class iz3proof_itp_impl : public iz3proof_itp { } + bool rewrites_from_to(const ast &chain, const ast &lhs, const ast &rhs){ + if(is_true(chain)) + return lhs == rhs; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast mid = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last)); + return rewrites_from_to(rest,lhs,mid); + } + + struct bad_ineq_inference {}; + ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){ if(is_true(chain)){ if(lhs != rhs) - throw "bad ineq inference"; + throw bad_ineq_inference(); return make(Leq,make_int(rational(0)),make_int(rational(0))); } ast last = chain_last(chain);