diff --git a/src/duality/duality.h b/src/duality/duality.h old mode 100644 new mode 100755 diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp old mode 100644 new mode 100755 diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp old mode 100644 new mode 100755 index 91532960b..6d39a4fe2 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -44,12 +44,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... @@ -1933,11 +1938,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 @@ -1977,7 +1986,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; @@ -2001,9 +2012,11 @@ namespace Duality { was_sat = true; 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 994d10e06..329fcb305 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -684,10 +684,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 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 8b78a7135..2d79e8151 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -677,8 +677,11 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){ - if(pf == pl) + if(pf == pl){ + if(sym(ineq) == normal) + return my_implies(Bproves,ineq); return my_implies(Bproves,simplify_ineq(ineq)); + } if(op(pf) == Uninterpreted && sym(pf) == sum){ if(arg(pf,2) == pl){ ast Aproves = mk_true(); @@ -829,6 +832,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(); } @@ -1443,6 +1448,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); @@ -2240,10 +2289,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 @@ -2427,7 +2485,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 abddb4bda..bba7b4d0d 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -181,6 +181,13 @@ public: get_Z3_lits(con, lits); iproof->make_axiom(lits); } + 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); + } else { unsigned nprems = num_prems(proof); for(unsigned i = 0; i < nprems; i++){ @@ -1264,6 +1271,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)); @@ -1302,7 +1387,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)); @@ -1445,9 +1530,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); @@ -1620,9 +1707,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: diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp old mode 100644 new mode 100755