mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

duality fix

Browse source
This commit is contained in:
Ken McMillan 2014-02-19 13:57:27 -08:00
parent c9cf658e7c
commit 65c54b87d0
3 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/duality/duality.h
View file

@ -1242,17 +1242,17 @@ namespace Duality {
void GetTermTreeAssertionLiteralsRec(TermTree *assumptions); void GetTermTreeAssertionLiteralsRec(TermTree *assumptions);
edge_solver &SolverForEdge(Edge *edge, bool models); edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms);
public: public:
struct scoped_solver_for_edge { struct scoped_solver_for_edge {
solver *orig_slvr; solver *orig_slvr;
RPFP_caching *rpfp; RPFP_caching *rpfp;
edge_solver *es; edge_solver *es;
scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){ scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){
rpfp = _rpfp; rpfp = _rpfp;
orig_slvr = rpfp->ls->slvr; orig_slvr = rpfp->ls->slvr;
es = &(rpfp->SolverForEdge(edge,models)); es = &(rpfp->SolverForEdge(edge,models,axioms));
rpfp->ls->slvr = es->slvr.get(); rpfp->ls->slvr = es->slvr.get();
rpfp->AssumptionLits.swap(es->AssumptionLits); rpfp->AssumptionLits.swap(es->AssumptionLits);
} }

8
src/duality/duality_rpfp.cpp
View file

@ -2895,12 +2895,18 @@ namespace Duality {
timer_stop("Generalize"); timer_stop("Generalize");
} }
RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models){ RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models, bool axioms){
edge_solver &es = edge_solvers[edge]; edge_solver &es = edge_solvers[edge];
uptr<solver> &p = es.slvr; uptr<solver> &p = es.slvr;
if(!p.get()){ if(!p.get()){
scoped_no_proof no_proofs_please(ctx.m()); // no proofs scoped_no_proof no_proofs_please(ctx.m()); // no proofs
p.set(new solver(ctx,true,models)); // no models p.set(new solver(ctx,true,models)); // no models
if(axioms){
RPFP::LogicSolver *ls = edge->owner->ls;
const std::vector<expr> &axs = ls->get_axioms();
for(unsigned i = 0; i < axs.size(); i++)
p.get()->add(axs[i]);
}
} }
return es; return es;
} }

4
src/duality/duality_solver.cpp
View file

@ -1247,7 +1247,7 @@ namespace Duality {
slvr.pop(1); slvr.pop(1);
delete checker; delete checker;
#else #else
RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */); RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
gen_cands_rpfp->Push(); gen_cands_rpfp->Push();
Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp); Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
if(gen_cands_rpfp->Check(root) != unsat){ if(gen_cands_rpfp->Check(root) != unsat){
@ -2004,7 +2004,7 @@ namespace Duality {
} }
else { else {
was_sat = true; was_sat = true;
tree->Push(); tree->Push();
std::vector<Node *> &expansions = stack.back().expansions; std::vector<Node *> &expansions = stack.back().expansions;
#ifndef NO_DECISIONS #ifndef NO_DECISIONS
for(unsigned i = 0; i < expansions.size(); i++){ for(unsigned i = 0; i < expansions.size(); i++){