optimizing solver performance in duality

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<Term> &lits);
+
+      virtual ~RPFP_caching(){}
+
   protected:
       hash_map<ast,expr> AssumptionLits;
       hash_map<Node *, Node *> NodeCloneMap;
       hash_map<Edge *, Edge *> EdgeCloneMap;
+      std::vector<expr> alit_stack;
+      std::vector<unsigned> alit_stack_sizes;
       
       void GetAssumptionLits(const expr &fmla, std::vector<expr> &lits, hash_map<ast,expr> *opt_map = 0);
 
       void GreedyReduceCache(std::vector<expr> &assumps, std::vector<expr> &core);
 
       void FilterCore(std::vector<expr> &core, std::vector<expr> &full_core);
+      void ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector<expr> &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);
 
     };
 

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<expr> 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,6 +788,95 @@ 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<expr> 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<expr> alits;
+    hash_map<ast,expr> map;
+    GetAssumptionLits(assumptions->getTerm(),alits,&map);
+    std::vector<expr> &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<expr> &lits, hash_map<ast,expr> *opt_map){
@@ -817,6 +903,10 @@ namespace Duality {
     ConstrainEdgeLocalized(parent,GetAnnotation(child));
   } 
 
+  void RPFP_caching::ConstrainParentCache(Edge *parent, Node *child, std::vector<Term> &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<Edge *,Term>(e,tl));
-    slvr.add(tl);
+    slvr_add(tl);
   }
 
+  void RPFP_caching::ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector<expr> &lits)
+  {
+    e->constraints.push_back(tl);
+    stack.back().constraints.push_back(std::pair<Edge *,Term>(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<expr> 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<expr> 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<expr> cnsts;
@@ -1093,7 +1189,7 @@ namespace Duality {
 		ls->write_interpolation_problem("temp.smt",cnsts,std::vector<expr>());
 	      }
 	    }
-            // 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<expr> 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]);
+    check_result res = slvr_check(assumps.size(),&assumps[0]);
-    dualModel = slvr.get_model();
+    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_pop(1);
-    slvr.push();
+    slvr_push();
     stack_entry &back = stack.back();
     for(std::list<Edge *>::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it)
-      slvr.add((*it)->dual);
+      slvr_add((*it)->dual);
     for(std::list<Node *>::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it)
-      slvr.add((*it)->dual);
+      slvr_add((*it)->dual);
     for(std::list<std::pair<Edge *,Term> >::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<expr> 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;
   }

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,17 +119,29 @@ 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(){
 #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
     }
 
@@ -133,6 +149,11 @@ namespace Duality {
     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<Node *> &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) || 
+	    if(checker->Empty(node) || 
-	       eq(checker->Eval(lb,NodeMarker(inst)),ctx.bool_val(true))){
+	       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){
+      void InitializeApproximatedInstance(RPFP::Node *to){
-	Node *to = tree->CloneNode(from);
+	to->Annotation = to->map->Annotation;
-	to->Annotation = from->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);
+	Edge *ne = p->Outgoing;
-	std::vector<RPFP::Node *> &cs = edge->Children;
+	if(ne) {
-	std::vector<RPFP::Node *> children(cs.size());
+	  reporter->Message("Recycling edge...");
-	for(unsigned i = 0; i < cs.size(); i++)
+	  std::vector<RPFP::Node *> &cs = ne->Children;
-	  children[i] = CreateApproximatedInstance(cs[i]);
+	  for(unsigned i = 0; i < cs.size(); i++)
-	Edge *ne = tree->CreateEdge(p, p->map->Outgoing->F, children);
+	    InitializeApproximatedInstance(cs[i]);
-        ne->map = p->map->Outgoing->map;
+	  // ne->dual = expr();
+	}
+	else {
+	  Edge *edge = duality->GetNodeOutgoing(p->map,last_decs);
+	  std::vector<RPFP::Node *> &cs = edge->Children;
+	  std::vector<RPFP::Node *> 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<RPFP::Node *> 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<RPFP::Node *> 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<Node *> &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<Node *> &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 {

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){ 

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 push() { scoped_proof_mode spm(m(),m_mode); m_solver->push(); }
-        void pop(unsigned n = 1) { m_solver->pop(n); }
+        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<Z3_ast> _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());
 	}
 

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<family_id>;