From 928d419138ebb463d613b9f164078d52f359f9b9 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 17 Feb 2014 12:15:11 -0800 Subject: [PATCH] duality fixes --- src/duality/duality.h | 22 +++++++++++++----- src/duality/duality_rpfp.cpp | 41 +++++++++++++++++++++++++--------- src/duality/duality_solver.cpp | 10 ++------- src/interp/iz3translate.cpp | 2 ++ 4 files changed, 51 insertions(+), 24 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 8c469b9e4..aacc04f24 100755 --- 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); public: struct scoped_solver_for_edge { - LogicSolver *orig_ls; + solver *orig_slvr; RPFP_caching *rpfp; + edge_solver *es; scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){ rpfp = _rpfp; - orig_ls = rpfp->ls; - rpfp->ls = rpfp->SolverForEdge(edge,models); + orig_slvr = rpfp->ls->slvr; + es = &(rpfp->SolverForEdge(edge,models)); + 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 index 9813bce6a..173959567 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2741,8 +2741,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; @@ -2883,13 +2895,14 @@ 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){ + 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 } - return p.get(); + return es; } @@ -3356,6 +3369,8 @@ namespace Duality { } } + bool some_labels = false; + // create the edges for(unsigned i = 0; i < clauses.size(); i++){ @@ -3391,17 +3406,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 @@ -3663,7 +3684,7 @@ namespace Duality { for(unsigned j = 0; j < outs.size(); j++) for(unsigned k = 0; k < outs[j]->Children.size(); k++) chs.push_back(outs[j]->Children[k]); - Edge *fedge = CreateEdge(node,tr,chs); + CreateEdge(node,tr,chs); for(unsigned j = 0; j < outs.size(); j++) edges_to_delete.insert(outs[j]); } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 6d39a4fe2..e3a294550 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -127,13 +127,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 } @@ -142,20 +140,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 diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index bba7b4d0d..ef0c6f5ec 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -181,6 +181,7 @@ 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; @@ -188,6 +189,7 @@ public: get_Z3_lits(con, lits); iproof->make_axiom(lits); } +#endif else { unsigned nprems = num_prems(proof); for(unsigned i = 0; i < nprems; i++){