From ea8eb74744f04da7f517d8ef09485b57dc8d330b Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 11 Dec 2013 16:25:59 -0800 Subject: [PATCH] simplifying quantified interpolants in duality --- src/duality/duality.h | 21 ++- src/duality/duality_rpfp.cpp | 235 +++++++++++++++++++++++++++++++++- src/duality/duality_wrapper.h | 2 + 3 files changed, 254 insertions(+), 4 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index f1e848f0d..4539b4711 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -81,10 +81,23 @@ namespace Duality { int CountOperators(const Term &t); + Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); + + Term RemoveRedundancy(const Term &t); + + bool IsLiteral(const expr &lit, expr &atom, expr &val); + + expr Negate(const expr &f); + + expr SimplifyAndOr(const std::vector &args, bool is_and); + private: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); int CountOperatorsRec(hash_set &memo, const Term &t); + void RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo); + Term RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t); + Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val); }; @@ -570,7 +583,7 @@ namespace Duality { edge to their values in the current assignment. */ void FixCurrentState(Edge *root); - void FixCurrentStateFull(Edge *edge); + void FixCurrentStateFull(Edge *edge, const expr &extra); /** Declare a constant in the background theory. */ @@ -929,6 +942,12 @@ namespace Duality { void AddToProofCore(hash_set &core); + void GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under); + + Term StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits); + + expr NegateLit(const expr &f); + }; /** RPFP solver base class. */ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index f37545b48..5260dc7e9 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -368,6 +368,136 @@ namespace Duality { return res; } + bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ + if(!lit.is_app()) + return false; + decl_kind k = lit.decl().get_decl_kind(); + if(k == Not){ + if(IsLiteral(lit.arg(0),atom,val)){ + val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); + return true; + } + return false; + } + if(k == And || k == Or || k == Iff || k == Implies) + return false; + atom = lit; + val = ctx.bool_val(true); + return true; + } + + expr Z3User::Negate(const expr &f){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + return f.arg(0); + else if(eq(f,ctx.bool_val(true))) + return ctx.bool_val(false); + else if(eq(f,ctx.bool_val(false))) + return ctx.bool_val(true); + return !f; + } + + expr Z3User::SimplifyAndOr(const std::vector &args, bool is_and){ + std::vector sargs; + for(unsigned i = 0; i < args.size(); i++) + if(!eq(args[i],ctx.bool_val(is_and))){ + if(eq(args[i],ctx.bool_val(!is_and))) + return ctx.bool_val(!is_and); + sargs.push_back(args[i]); + } + if(sargs.size() == 0) + return ctx.bool_val(is_and); + if(sargs.size() == 1) + return sargs[0]; + return ctx.make(is_and ? And : Or,sargs); + } + + Z3User::Term Z3User::SubstAtomTriv(const expr &foo, const expr &atom, const expr &val){ + if(eq(foo,atom)) + return val; + else if(foo.is_app() && foo.decl().get_decl_kind() == Not && eq(foo.arg(0),atom)) + return Negate(val); + else + return foo; + } + + 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); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()){ + func_decl f = t.decl(); + decl_kind k = f.get_decl_kind(); + + // TODO: recur here, but how much? We don't want to be quadractic in formula size + + if(k == And || k == Or){ + int nargs = t.num_args(); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = SubstAtom(memo,t.arg(i),atom,val); + res = SimplifyAndOr(args,k == And); + return res; + } + } + res = SubstAtomTriv(t,atom,val); + return res; + } + + void Z3User::RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo){ + for(unsigned i = 0; i < args.size(); i++){ + const expr &lit = args[i]; + expr atom, val; + if(IsLiteral(lit,atom,val)){ + for(unsigned j = 0; j < args.size(); j++) + if(j != i){ + smemo.clear(); + args[j] = SubstAtom(smemo,args[j],atom,pol ? val : !val); + } + } + } + } + + + Z3User::Term Z3User::RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t) + { + 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(RemoveRedundancyRec(memo, smemo, t.arg(i))); + + decl_kind k = f.get_decl_kind(); + if(k == And) + RemoveRedundancyOp(true,args,smemo); + else if(k == Or) + RemoveRedundancyOp(false,args,smemo); + if(k == Equal && args[0].get_id() > args[1].get_id()) + std::swap(args[0],args[1]); + + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + { + Term body = RemoveRedundancyRec(memo,smemo,t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + Z3User::Term Z3User::RemoveRedundancy(const Term &t){ + hash_map memo; + hash_map smemo; + return RemoveRedundancyRec(memo,smemo,t); + } + Z3User::Term Z3User::SubstRecHide(hash_map &memo, const Term &t, int number) { std::pair foo(t,expr(ctx)); @@ -1829,18 +1959,100 @@ namespace Duality { ConstrainEdgeLocalized(edge,eu); } - void RPFP::FixCurrentStateFull(Edge *edge){ + 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; + memo[under].insert(f); + if(f.is_app()){ + if(!under && !f.has_quantifiers()) + return; + decl_kind k = f.decl().get_decl_kind(); + if(k == And || k == Or || k == Implies || k == Iff){ + int num_args = f.num_args(); + for(int i = 0; i < num_args; i++) + GetGroundLitsUnderQuants(memo,f.arg(i),res,under); + return; + } + } + else if (f.is_quantifier()){ + GetGroundLitsUnderQuants(memo,f.body(),res,1); + return; + } + if(under && f.is_ground()) + res.push_back(f); + } + + RPFP::Term RPFP::StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits){ + hash_set memo[2]; + std::vector lits; + GetGroundLitsUnderQuants(memo, f, lits, 0); + hash_set lits_hash; + for(unsigned i = 0; i < lits.size(); i++) + lits_hash.insert(lits[i]); + hash_map subst; + hash_map stt_memo; + std::vector conjuncts; + for(unsigned i = 0; i < lits.size(); i++){ + const expr &lit = lits[i]; + if(lits_hash.find(NegateLit(lit)) == lits_hash.end()){ + case_lits.push_back(lit); + bool tval = false; + expr atom = lit; + if(lit.is_app() && lit.decl().get_decl_kind() == Not){ + tval = true; + atom = lit.arg(0); + } + expr etval = ctx.bool_val(tval); + int b = SubtermTruth(stt_memo,atom); + if(b == (tval ? 1 : 0)) + subst[atom] = etval; + else { + if(b == 0 || b == 1){ + etval = ctx.bool_val(b ? true : false); + subst[atom] = etval; + conjuncts.push_back(b ? atom : !atom); + } + } + } + } + expr g = f; + if(!subst.empty()){ + g = SubstRec(subst,f); + if(conjuncts.size()) + g = g && ctx.make(And,conjuncts); + g = g.simplify(); + } +#if 0 + expr g_old = g; + g = RemoveRedundancy(g); + bool changed = !eq(g,g_old); + g = g.simplify(); + if(changed) { // a second pass can get some more simplification + g = RemoveRedundancy(g); + g = g.simplify(); + } +#else + g = RemoveRedundancy(g); + g = g.simplify(); +#endif + return g; + } RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){ if(t.is_array()){ @@ -1948,6 +2160,13 @@ namespace Duality { } } + expr RPFP::NegateLit(const expr &f){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + return f.arg(0); + else + return !f; + } + void RPFP::NegateLits(std::vector &lits){ for(unsigned i = 0; i < lits.size(); i++){ expr &f = lits[i]; @@ -1984,7 +2203,8 @@ namespace Duality { core->insert(node->Outgoing->dual); while(1){ aux_solver.push(); - aux_solver.add(!GetAnnotation(node)); + expr annot = !GetAnnotation(node); + aux_solver.add(annot); if(aux_solver.check() == unsat){ aux_solver.pop(1); break; @@ -1992,7 +2212,7 @@ namespace Duality { dualModel = aux_solver.get_model(); aux_solver.pop(1); Push(); - FixCurrentStateFull(node->Outgoing); + FixCurrentStateFull(node->Outgoing,annot); ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); check_result foo = Check(root); if(foo != unsat) @@ -2000,6 +2220,15 @@ namespace Duality { AddToProofCore(*core); Transformer old_annot = node->Annotation; SolveSingleNode(root,node); + + { + expr itp = GetAnnotation(node); + dualModel = aux_solver.get_model(); + std::vector case_lits; + itp = StrengthenFormulaByCaseSplitting(itp, case_lits); + SetAnnotation(node,itp); + } + if(node->Annotation.IsEmpty()){ std::cout << "bad in InterpolateByCase -- core:\n"; std::vector assumps; diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index f69bc642e..e0824d4be 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -457,6 +457,8 @@ namespace Duality { bool is_quantifier() const {return raw()->get_kind() == AST_QUANTIFIER;} bool is_var() const {return raw()->get_kind() == AST_VAR;} 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();} // 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());}