3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

duality fixes

This commit is contained in:
Ken McMillan 2014-02-17 12:15:11 -08:00
parent cb3dc63e68
commit 928d419138
4 changed files with 51 additions and 24 deletions

View file

@ -1184,7 +1184,13 @@ namespace Duality {
hash_map<Edge *, Edge *> EdgeCloneMap;
std::vector<expr> alit_stack;
std::vector<unsigned> alit_stack_sizes;
hash_map<Edge *, uptr<LogicSolver> > edge_solvers;
// to let us use one solver per edge
struct edge_solver {
hash_map<ast,expr> AssumptionLits;
uptr<solver> slvr;
};
hash_map<Edge *, edge_solver > 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);
}
};

View file

@ -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<expr> &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<expr> dummy;
@ -2883,13 +2895,14 @@ namespace Duality {
timer_stop("Generalize");
}
RPFP::LogicSolver *RPFP_caching::SolverForEdge(Edge *edge, bool models){
uptr<LogicSolver> &p = edge_solvers[edge];
RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models){
edge_solver &es = edge_solvers[edge];
uptr<solver> &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<label_struct > 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<int> 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<int,hash_map<ast,Term> > 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]);
}

View file

@ -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

View file

@ -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<ast> 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++){