From 9e88691c69ef4f9c7f1059c225a343c9a3e5861d Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 22 Dec 2013 18:33:40 -0800 Subject: [PATCH] optimizing solver performance in duality --- src/duality/duality.h | 45 +++++- src/duality/duality_rpfp.cpp | 169 +++++++++++++++++++---- src/duality/duality_solver.cpp | 128 +++++++++++++++-- src/duality/duality_wrapper.cpp | 1 + src/duality/duality_wrapper.h | 18 ++- src/muz/duality/duality_dl_interface.cpp | 1 - 6 files changed, 311 insertions(+), 51 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index b29a6a610..b88e5011f 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -350,7 +350,7 @@ protected: proof_core = 0; } - ~RPFP(); + virtual ~RPFP(); /** Symbolic representation of a relational transformer */ class Transformer @@ -962,6 +962,22 @@ protected: expr NegateLit(const expr &f); expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox); + + virtual void slvr_add(const expr &e); + + virtual void slvr_pop(int i); + + virtual void slvr_push(); + + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); + + virtual lbool ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); }; @@ -1085,16 +1101,43 @@ namespace Duality { /** Construct a caching RPFP using a LogicSolver */ RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {} + /** Constraint an edge by its child's annotation. Return + assumption lits. */ + void ConstrainParentCache(Edge *parent, Node *child, std::vector &lits); + + virtual ~RPFP_caching(){} + protected: hash_map AssumptionLits; hash_map NodeCloneMap; hash_map EdgeCloneMap; + std::vector alit_stack; + std::vector alit_stack_sizes; void GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map = 0); void GreedyReduceCache(std::vector &assumps, std::vector &core); void FilterCore(std::vector &core, std::vector &full_core); + void ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits); + + virtual void slvr_add(const expr &e); + + virtual void slvr_pop(int i); + + virtual void slvr_push(); + + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); + + virtual lbool ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); + + void GetTermTreeAssertionLiterals(TermTree *assumptions); }; diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index a95561f5d..04b4d075e 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -732,9 +732,6 @@ namespace Duality { e->dual = ReducedDualEdge(e); timer_stop("ReducedDualEdge"); timer_start("getting children"); - if(with_children) - for(unsigned i = 0; i < e->Children.size(); i++) - e->dual = e->dual && GetAnnotation(e->Children[i]); if(underapprox){ std::vector cus(e->Children.size()); for(unsigned i = 0; i < e->Children.size(); i++) @@ -753,9 +750,6 @@ namespace Duality { //Console.WriteLine("{0}", cnst); } return e->dual; - timer_start("solver add"); - slvr.add(e->dual); - timer_stop("solver add"); } /** For incremental solving, asserts the constraint associated @@ -781,8 +775,11 @@ namespace Duality { return; expr fmla = GetEdgeFormula(e, persist, with_children, underapprox); timer_start("solver add"); - slvr.add(e->dual); + slvr_add(e->dual); timer_stop("solver add"); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParent(e,e->Children[i]); } // caching verion of above @@ -791,8 +788,97 @@ namespace Duality { return; expr fmla = GetEdgeFormula(e, 0, with_children, false); GetAssumptionLits(fmla,lits); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParentCache(e,e->Children[i],lits); } + void RPFP::slvr_add(const expr &e){ + slvr.add(e); + } + + void RPFP_caching::slvr_add(const expr &e){ + GetAssumptionLits(e,alit_stack); + } + + void RPFP::slvr_pop(int i){ + slvr.pop(i); + } + + void RPFP::slvr_push(){ + slvr.push(); + } + + void RPFP_caching::slvr_pop(int i){ + for(int j = 0; j < i; j++){ + alit_stack.resize(alit_stack_sizes.back()); + alit_stack_sizes.pop_back(); + } + } + + void RPFP_caching::slvr_push(){ + alit_stack_sizes.push_back(alit_stack.size()); + } + + check_result RPFP::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ + return slvr.check(n, assumptions, core_size, core); + } + + check_result RPFP_caching::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ + slvr_push(); + if(n && assumptions) + std::copy(assumptions,assumptions+n,std::inserter(alit_stack,alit_stack.end())); + check_result res; + if(core_size && core){ + std::vector full_core(alit_stack.size()), core1(n); + std::copy(assumptions,assumptions+n,core1.begin()); + res = slvr.check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]); + full_core.resize(*core_size); + if(res == unsat){ + FilterCore(core1,full_core); + *core_size = core1.size(); + std::copy(core1.begin(),core1.end(),core); + } + } + else + res = slvr.check(alit_stack.size(), &alit_stack[0]); + slvr_pop(1); + return res; + } + + lbool RPFP::ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals, + bool weak){ + return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); + } + + lbool RPFP_caching::ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals, + bool weak){ + GetTermTreeAssertionLiterals(assumptions); + return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); + } + + void RPFP_caching::GetTermTreeAssertionLiterals(TermTree *assumptions){ + std::vector alits; + hash_map map; + GetAssumptionLits(assumptions->getTerm(),alits,&map); + std::vector &ts = assumptions->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + GetAssumptionLits(ts[i],alits,&map); + assumptions->setTerm(ctx.bool_val(true)); + ts = alits; + for(unsigned i = 0; i < alits.size(); i++) + ts.push_back(ctx.make(Implies,alits[i],map[alits[i]])); + for(unsigned i = 0; i < assumptions->getChildren().size(); i++) + GetTermTreeAssertionLiterals(assumptions->getChildren()[i]); + return; + } + void RPFP_caching::GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map){ std::vector conjs; CollectConjuncts(fmla,conjs); @@ -817,6 +903,10 @@ namespace Duality { ConstrainEdgeLocalized(parent,GetAnnotation(child)); } + void RPFP_caching::ConstrainParentCache(Edge *parent, Node *child, std::vector &lits){ + ConstrainEdgeLocalizedCache(parent,GetAnnotation(child),lits); + } + /** For incremental solving, asserts the negation of the upper bound associated * with a node. @@ -828,7 +918,7 @@ namespace Duality { { n->dual = GetUpperBound(n); stack.back().nodes.push_back(n); - slvr.add(n->dual); + slvr_add(n->dual); } } @@ -892,9 +982,15 @@ namespace Duality { { e->constraints.push_back(tl); stack.back().constraints.push_back(std::pair(e,tl)); - slvr.add(tl); + slvr_add(tl); } + void RPFP_caching::ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits) + { + e->constraints.push_back(tl); + stack.back().constraints.push_back(std::pair(e,tl)); + GetAssumptionLits(tl,lits); + } /** Declare a constant in the background theory. */ @@ -971,7 +1067,7 @@ namespace Duality { // if (dualLabels != null) dualLabels.Dispose(); timer_start("interpolate_tree"); - lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals,true); + lbool res = ls_interpolate_tree(tree, interpolant, dualModel,goals,true); timer_stop("interpolate_tree"); if (res == l_false) { @@ -1017,7 +1113,7 @@ namespace Duality { ClearProofCore(); timer_start("interpolate_tree"); - lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true); + lbool res = ls_interpolate_tree(tree, interpolant, dualModel,0,true); timer_stop("interpolate_tree"); if (res == l_false) { @@ -1068,22 +1164,22 @@ namespace Duality { // if (dualModel != null) dualModel.Dispose(); check_result res; if(!underapproxes.size()) - res = slvr.check(); + res = slvr_check(); else { std::vector us(underapproxes.size()); for(unsigned i = 0; i < underapproxes.size(); i++) us[i] = UnderapproxFlag(underapproxes[i]); - slvr.check(); // TODO: no idea why I need to do this + slvr_check(); // TODO: no idea why I need to do this if(underapprox_core){ std::vector unsat_core(us.size()); unsigned core_size = 0; - res = slvr.check(us.size(),&us[0],&core_size,&unsat_core[0]); + res = slvr_check(us.size(),&us[0],&core_size,&unsat_core[0]); underapprox_core->resize(core_size); for(unsigned i = 0; i < core_size; i++) (*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]); } else { - res = slvr.check(us.size(),&us[0]); + res = slvr_check(us.size(),&us[0]); bool dump = false; if(dump){ std::vector cnsts; @@ -1093,7 +1189,7 @@ namespace Duality { ls->write_interpolation_problem("temp.smt",cnsts,std::vector()); } } - // check_result temp = slvr.check(); + // check_result temp = slvr_check(); } dualModel = slvr.get_model(); timer_stop("Check"); @@ -1101,10 +1197,12 @@ namespace Duality { } check_result RPFP::CheckUpdateModel(Node *root, std::vector assumps){ - // check_result temp1 = slvr.check(); // no idea why I need to do this + // check_result temp1 = slvr_check(); // no idea why I need to do this ClearProofCore(); - check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]); - dualModel = slvr.get_model(); + check_result res = slvr_check(assumps.size(),&assumps[0]); + model mod = slvr.get_model(); + if(!mod.null()) + dualModel = mod;; return res; } @@ -1117,8 +1215,6 @@ namespace Duality { return dualModel.eval(tl); } - - /** Returns true if the given node is empty in the primal solution. For proecudure summaries, this means that the procedure is not called in the current counter-model. */ @@ -2609,14 +2705,14 @@ namespace Duality { void RPFP::Push() { stack.push_back(stack_entry()); - slvr.push(); + slvr_push(); } /** Pop a scope (see Push). Note, you cannot pop axioms. */ void RPFP::Pop(int num_scopes) { - slvr.pop(num_scopes); + slvr_pop(num_scopes); for (int i = 0; i < num_scopes; i++) { stack_entry &back = stack.back(); @@ -2634,15 +2730,15 @@ namespace Duality { all the popped constraints */ void RPFP::PopPush(){ - slvr.pop(1); - slvr.push(); + slvr_pop(1); + slvr_push(); stack_entry &back = stack.back(); for(std::list::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it) - slvr.add((*it)->dual); + slvr_add((*it)->dual); for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) - slvr.add((*it)->dual); + slvr_add((*it)->dual); for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) - slvr.add((*it).second); + slvr_add((*it).second); } @@ -3121,12 +3217,25 @@ namespace Duality { } } + bool RPFP::proof_core_contains(const expr &e){ + return proof_core->find(e) != proof_core->end(); + } + + bool RPFP_caching::proof_core_contains(const expr &e){ + std::vector foo; + GetAssumptionLits(e,foo); + for(unsigned i = 0; i < foo.size(); i++) + if(proof_core->find(foo[i]) != proof_core->end()) + return true; + return false; + } + bool RPFP::EdgeUsedInProof(Edge *edge){ ComputeProofCore(); - if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end()) + if(!edge->dual.null() && proof_core_contains(edge->dual)) return true; for(unsigned i = 0; i < edge->constraints.size(); i++) - if(proof_core->find(edge->constraints[i]) != proof_core->end()) + if(proof_core_contains(edge->constraints[i])) return true; return false; } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 7318b020d..1faf838b0 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -37,7 +37,7 @@ Revision History: #define MINIMIZE_CANDIDATES // #define MINIMIZE_CANDIDATES_HARDER #define BOUNDED -#define CHECK_CANDS_FROM_IND_SET +// #define CHECK_CANDS_FROM_IND_SET #define UNDERAPPROX_NODES #define NEW_EXPAND #define EARLY_EXPAND @@ -45,6 +45,10 @@ Revision History: // #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_NEW_GEN_CANDS namespace Duality { @@ -115,11 +119,19 @@ namespace Duality { Report = false; StratifiedInlining = false; RecursionBound = -1; + { + scoped_no_proof no_proofs_please(ctx.m()); #ifdef USE_RPFP_CLONE clone_ls = new RPFP::iZ3LogicSolver(ctx); clone_rpfp = new RPFP_caching(clone_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->Clone(rpfp); +#endif + } } ~Duality(){ @@ -127,12 +139,21 @@ namespace Duality { 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 + typedef RPFP::Node Node; typedef RPFP::Edge Edge; @@ -1102,7 +1123,8 @@ namespace Duality { void ExtractCandidateFromCex(Edge *edge, RPFP *checker, Node *root, Candidate &candidate){ candidate.edge = edge; for(unsigned j = 0; j < edge->Children.size(); j++){ - Edge *lb = root->Outgoing->Children[j]->Outgoing; + Node *node = root->Outgoing->Children[j]; + Edge *lb = node->Outgoing; std::vector &insts = insts_of_node[edge->Children[j]]; #ifndef MINIMIZE_CANDIDATES for(int k = insts.size()-1; k >= 0; k--) @@ -1112,8 +1134,8 @@ namespace Duality { { Node *inst = insts[k]; if(indset->Contains(inst)){ - if(checker->Empty(lb->Parent) || - eq(checker->Eval(lb,NodeMarker(inst)),ctx.bool_val(true))){ + if(checker->Empty(node) || + eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){ candidate.Children.push_back(inst); goto next_child; } @@ -1183,6 +1205,25 @@ namespace Duality { #endif + Node *CheckerForEdgeClone(Edge *edge, RPFP_caching *checker){ + Edge *gen_cands_edge = gen_cands_rpfp->GetEdgeClone(edge); + Node *root = gen_cands_edge->Parent; + root->Outgoing = gen_cands_edge; + GenNodeSolutionFromIndSet(edge->Parent, root->Bound); +#if 0 + if(root->Bound.IsFull()) + return = 0; +#endif + checker->AssertNode(root); + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = gen_cands_edge->Children[j]; + GenNodeSolutionWithMarkers(oc,nc->Annotation,true); + } + checker->AssertEdge(gen_cands_edge,1,true); + return root; + } + /** If the current proposed solution is not inductive, use the induction failure to generate candidates for extension. */ void GenCandidatesFromInductionFailure(bool full_scan = false){ @@ -1192,6 +1233,7 @@ namespace Duality { Edge *edge = edges[i]; if(!full_scan && updated_nodes.find(edge->Parent) == updated_nodes.end()) continue; +#ifndef USE_RPFP_CLONE slvr.push(); RPFP *checker = new RPFP(rpfp->ls); Node *root = CheckerForEdge(edge,checker); @@ -1203,6 +1245,17 @@ namespace Duality { } slvr.pop(1); delete checker; +#else + clone_rpfp->Push(); + Node *root = CheckerForEdgeClone(edge,clone_rpfp); + if(clone_rpfp->Check(root) != unsat){ + Candidate candidate; + ExtractCandidateFromCex(edge,clone_rpfp,root,candidate); + reporter->InductionFailure(edge,candidate.Children); + candidates.push_back(candidate); + } + clone_rpfp->Pop(1); +#endif } updated_nodes.clear(); timer_stop("GenCandIndFail"); @@ -1326,7 +1379,9 @@ namespace Duality { node. */ bool SatisfyUpperBound(Node *node){ if(node->Bound.IsFull()) return true; +#ifdef PROPAGATE_BEFORE_CHECK Propagate(); +#endif reporter->Bound(node); int start_decs = rpfp->CumulativeDecisions(); DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand); @@ -1544,7 +1599,13 @@ namespace Duality { constrained = _constrained; false_approx = true; timer_start("Derive"); +#ifndef USE_CACHING_RPFP tree = _tree ? _tree : new RPFP(rpfp->ls); +#else + RPFP::LogicSolver *cache_ls = new RPFP::iZ3LogicSolver(ctx); + cache_ls->slvr->push(); + tree = _tree ? _tree : new RPFP_caching(cache_ls); +#endif tree->HornClauses = rpfp->HornClauses; tree->Push(); // so we can clear out the solver later when finished top = CreateApproximatedInstance(root); @@ -1556,19 +1617,27 @@ namespace Duality { timer_start("Pop"); tree->Pop(1); timer_stop("Pop"); +#ifdef USE_CACHING_RPFP + cache_ls->slvr->pop(1); + delete cache_ls; +#endif timer_stop("Derive"); return res; } #define WITH_CHILDREN - Node *CreateApproximatedInstance(RPFP::Node *from){ - Node *to = tree->CloneNode(from); - to->Annotation = from->Annotation; + void InitializeApproximatedInstance(RPFP::Node *to){ + to->Annotation = to->map->Annotation; #ifndef WITH_CHILDREN tree->CreateLowerBoundEdge(to); #endif leaves.push_back(to); + } + + Node *CreateApproximatedInstance(RPFP::Node *from){ + Node *to = tree->CloneNode(from); + InitializeApproximatedInstance(to); return to; } @@ -1637,13 +1706,23 @@ namespace Duality { virtual void ExpandNode(RPFP::Node *p){ // tree->RemoveEdge(p->Outgoing); - Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); - std::vector &cs = edge->Children; - std::vector children(cs.size()); - for(unsigned i = 0; i < cs.size(); i++) - children[i] = CreateApproximatedInstance(cs[i]); - Edge *ne = tree->CreateEdge(p, p->map->Outgoing->F, children); - ne->map = p->map->Outgoing->map; + Edge *ne = p->Outgoing; + if(ne) { + reporter->Message("Recycling edge..."); + std::vector &cs = ne->Children; + for(unsigned i = 0; i < cs.size(); i++) + InitializeApproximatedInstance(cs[i]); + // ne->dual = expr(); + } + else { + Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); + std::vector &cs = edge->Children; + std::vector children(cs.size()); + for(unsigned i = 0; i < cs.size(); i++) + children[i] = CreateApproximatedInstance(cs[i]); + ne = tree->CreateEdge(p, p->map->Outgoing->F, children); + ne->map = p->map->Outgoing->map; + } #ifndef WITH_CHILDREN tree->AssertEdge(ne); // assert the edge in the solver #else @@ -1785,12 +1864,25 @@ namespace Duality { void RemoveExpansion(RPFP::Node *p){ Edge *edge = p->Outgoing; Node *parent = edge->Parent; +#ifndef KEEP_EXPANSIONS std::vector cs = edge->Children; tree->DeleteEdge(edge); for(unsigned i = 0; i < cs.size(); i++) tree->DeleteNode(cs[i]); +#endif leaves.push_back(parent); } + + // remove all the descendants of tree root (but not root itself) + void RemoveTree(RPFP *tree, RPFP::Node *root){ + Edge *edge = root->Outgoing; + std::vector cs = edge->Children; + tree->DeleteEdge(edge); + for(unsigned i = 0; i < cs.size(); i++){ + RemoveTree(tree,cs[i]); + tree->DeleteNode(cs[i]); + } + } }; class DerivationTreeSlow : public DerivationTree { @@ -1852,6 +1944,7 @@ namespace Duality { } } tree->ComputeProofCore(); // need to compute the proof core before popping solver + bool propagated = false; while(1) { std::vector &expansions = stack.back().expansions; bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop @@ -1881,16 +1974,21 @@ namespace Duality { if(!Propagate(node)) break; if(!RecordUpdate(node)) break; // shouldn't happen! RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list + propagated = true; continue; } + if(propagated) break; // propagation invalidates the proof core, so disable non-chron backtrack RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list std::vector &unused_ex = stack.back().expansions; for(unsigned i = 0; i < unused_ex.size(); i++) heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future } HandleUpdatedNodes(); - if(stack.size() == 1) + if(stack.size() == 1){ + if(top->Outgoing) + tree->DeleteEdge(top->Outgoing); // in case we kept the tree return false; + } was_sat = false; } else { diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 26bdf52d7..51f357653 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -44,6 +44,7 @@ namespace Duality { m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); m_solver->updt_params(p); // why do we have to do this? canceled = false; + m_mode = m().proof_mode(); } expr context::constant(const std::string &name, const sort &ty){ diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index fa4eca77b..76b28a426 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -50,6 +50,7 @@ Revision History: #include"scoped_ctrl_c.h" #include"cancel_eh.h" #include"scoped_timer.h" +#include"scoped_proof.h" namespace Duality { @@ -718,6 +719,7 @@ namespace Duality { m_model = s; return *this; } + bool null() const {return !m_model;} expr eval(expr const & n, bool model_completion=true) const { ::model * _m = m_model.get(); @@ -811,6 +813,7 @@ namespace Duality { ::solver *m_solver; model the_model; bool canceled; + proof_gen_mode m_mode; public: solver(context & c, bool extensional = false); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} @@ -824,6 +827,7 @@ namespace Duality { m_ctx = s.m_ctx; m_solver = s.m_solver; the_model = s.the_model; + m_mode = s.m_mode; return *this; } struct cancel_exception {}; @@ -832,11 +836,12 @@ namespace Duality { throw(cancel_exception()); } // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); } - void push() { m_solver->push(); } - void pop(unsigned n = 1) { m_solver->pop(n); } + void push() { scoped_proof_mode spm(m(),m_mode); m_solver->push(); } + void pop(unsigned n = 1) { scoped_proof_mode spm(m(),m_mode); m_solver->pop(n); } // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } - void add(expr const & e) { m_solver->assert_expr(e); } + void add(expr const & e) { scoped_proof_mode spm(m(),m_mode); m_solver->assert_expr(e); } check_result check() { + scoped_proof_mode spm(m(),m_mode); checkpoint(); lbool r = m_solver->check_sat(0,0); model_ref m; @@ -845,6 +850,7 @@ namespace Duality { return to_check_result(r); } check_result check_keep_model(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); model old_model(the_model); check_result res = check(n,assumptions,core_size,core); if(the_model == 0) @@ -852,6 +858,7 @@ namespace Duality { return res; } check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); checkpoint(); std::vector< ::expr *> _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -876,6 +883,7 @@ namespace Duality { } #if 0 check_result check(expr_vector assumptions) { + scoped_proof_mode spm(m(),m_mode); unsigned n = assumptions.size(); z3array _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -900,17 +908,19 @@ namespace Duality { int get_num_decisions(); void cancel(){ + scoped_proof_mode spm(m(),m_mode); canceled = true; if(m_solver) m_solver->cancel(); } - unsigned get_scope_level(){return m_solver->get_scope_level();} + unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} void show(); void show_assertion_ids(); proof get_proof(){ + scoped_proof_mode spm(m(),m_mode); return proof(ctx(),m_solver->get_proof()); } diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 1409212d4..397d50655 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -35,7 +35,6 @@ Revision History: #include "model_smt2_pp.h" #include "model_v2_pp.h" #include "fixedpoint_params.hpp" -#include "scoped_proof.h" // template class symbol_table;