From 418f148ecf4e8c405ddd844f665f077018af1c9e Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 4 Jun 2013 18:22:54 -0700 Subject: [PATCH] working on incremental stratified inlining in duality --- src/duality/duality.h | 2 +- src/duality/duality_solver.cpp | 32 +++++++++++++++++++++-------- src/muz_qe/dl_context.cpp | 1 + src/muz_qe/duality_dl_interface.cpp | 29 +++++++++++++++++++++----- 4 files changed, 50 insertions(+), 14 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 343eeeb72..f514e045f 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -803,7 +803,7 @@ namespace Duality { is chiefly useful for abstraction refinement, when we want to solve a series of similar problems. */ - virtual void LearnFrom(Solver *old_solver) = 0; + virtual void LearnFrom(Counterexample &old_cex) = 0; virtual ~Solver(){} diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 40aa352c2..e53ead302 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -160,6 +160,9 @@ namespace Duality { Heuristic(RPFP *_rpfp){ rpfp = _rpfp; } + + virtual ~Heuristic(){} + virtual void Update(RPFP::Node *node){ scores[node].updates++; } @@ -247,6 +250,7 @@ namespace Duality { heuristic = !cex.tree ? (Heuristic *)(new LocalHeuristic(rpfp)) : (Heuristic *)(new ReplayHeuristic(rpfp,cex)); #endif + cex.tree = 0; // heuristic now owns it unwinding = new RPFP(rpfp->ls); unwinding->HornClauses = rpfp->HornClauses; indset = new Covering(this); @@ -254,8 +258,10 @@ namespace Duality { CreateEdgesByChildMap(); CreateLeaves(); #ifndef TOP_DOWN - if(FeasibleEdges)NullaryCandidates(); - else InstantiateAllEdges(); + if(!StratifiedInlining){ + if(FeasibleEdges)NullaryCandidates(); + else InstantiateAllEdges(); + } #else for(unsigned i = 0; i < leaves.size(); i++) if(!SatisfyUpperBound(leaves[i])) @@ -289,8 +295,8 @@ namespace Duality { } #endif - virtual void LearnFrom(Solver *old_solver){ - cex = old_solver->GetCounterexample(); + virtual void LearnFrom(Counterexample &old_cex){ + cex = old_cex; } /** Return the counterexample */ @@ -778,8 +784,14 @@ namespace Duality { std::vector nchs(chs.size()); for(unsigned i = 0; i < chs.size(); i++){ Node *child = chs[i]; - if(TopoSort[child] < TopoSort[node->map]) - nchs[i] = LeafMap[child]; + if(TopoSort[child] < TopoSort[node->map]){ + Node *leaf = LeafMap[child]; + nchs[i] = leaf; + if(unexpanded.find(leaf) != unexpanded.end()){ + unexpanded.erase(leaf); + insts_of_node[child].push_back(leaf); + } + } else { if(StratifiedLeafMap.find(child) == StratifiedLeafMap.end()){ RPFP::Node *nchild = CreateNodeInstance(child,StratifiedLeafCount--); @@ -1450,7 +1462,7 @@ namespace Duality { #ifdef EFFORT_BOUNDED_STRAT start_decs = tree->CumulativeDecisions(); #endif - // while(ExpandSomeNodes(true)); // do high-priority expansions + while(ExpandSomeNodes(true)); // do high-priority expansions while (true) { #ifndef WITH_CHILDREN @@ -1999,13 +2011,17 @@ namespace Duality { class ReplayHeuristic : public Heuristic { - Counterexample &old_cex; + Counterexample old_cex; public: ReplayHeuristic(RPFP *_rpfp, Counterexample &_old_cex) : Heuristic(_rpfp), old_cex(_old_cex) { } + ~ReplayHeuristic(){ + delete old_cex.tree; + } + // Maps nodes of derivation tree into old cex hash_map cex_map; diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index ef8168607..c171b66e4 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -198,6 +198,7 @@ namespace datalog { void context::push() { m_trail.push_scope(); m_trail.push(restore_rules(m_rule_set)); + m_trail.push(restore_vec_size_trail(m_rule_fmls)); m_trail.push(restore_vec_size_trail(m_background)); } diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp index eb455ffe7..e53d79409 100644 --- a/src/muz_qe/duality_dl_interface.cpp +++ b/src/muz_qe/duality_dl_interface.cpp @@ -79,14 +79,13 @@ namespace Duality { dl_interface::dl_interface(datalog::context& dl_ctx) : m_ctx(dl_ctx) { - _d = alloc(duality_data,dl_ctx.get_manager()); - _d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx); - _d->rpfp = alloc(RPFP,_d->ls); + _d = 0; } dl_interface::~dl_interface() { - dealloc(_d); + if(_d) + dealloc(_d); } @@ -120,10 +119,22 @@ void dl_interface::check_reset() { lbool dl_interface::query(::expr * query) { - // TODO: you can only call this once! // we restore the initial state in the datalog context m_ctx.ensure_opened(); + // if there is old data, get the cex and dispose (later) + Solver::Counterexample old_cex; + duality_data *old_data = _d; + if(old_data) + old_cex = old_data->cex; + + // make a new problem and solver + _d = alloc(duality_data,m_ctx.get_manager()); + _d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx); + _d->rpfp = alloc(RPFP,_d->ls); + + + expr_ref_vector rules(m_ctx.get_manager()); svector< ::symbol> names; // m_ctx.get_rules_as_formulas(rules, names); @@ -173,6 +184,8 @@ lbool dl_interface::query(::expr * query) { Solver *rs = Solver::Create("duality", _d->rpfp); + rs->LearnFrom(old_cex); // new solver gets hints from old cex + // set its options IF_VERBOSE(1, rs->SetOption("report","1");); rs->SetOption("full_expand",m_ctx.get_params().full_expand() ? "1" : "0"); @@ -193,6 +206,12 @@ lbool dl_interface::query(::expr * query) { _d->status = ans ? StatusModel : StatusRefutation; _d->cex = rs->GetCounterexample(); + if(old_data){ + old_data->cex.tree = 0; // we own it now + dealloc(old_data); + } + + dealloc(rs); // true means the RPFP problem is SAT, so the query is UNSAT