working on incremental stratified inlining in duality

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

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(!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){
+    virtual void LearnFrom(Counterexample &old_cex){
-      cex = old_solver->GetCounterexample();
+      cex = old_cex;
     }
 
     /** Return the counterexample */
@@ -778,8 +784,14 @@ namespace Duality {
       std::vector<Node *> nchs(chs.size());
       for(unsigned i = 0; i < chs.size(); i++){
 	Node *child = chs[i];
-	if(TopoSort[child] < TopoSort[node->map])
+	if(TopoSort[child] < TopoSort[node->map]){
-	  nchs[i] = LeafMap[child];
+	  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<Node *, Node*> cex_map;
       

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<context,expr_ref_vector>(m_rule_fmls));
         m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_background));
     }
 

src/muz_qe/duality_dl_interface.cpp

@@ -79,13 +79,12 @@ namespace Duality {
 dl_interface::dl_interface(datalog::context& dl_ctx) :  m_ctx(dl_ctx)
 
 {
-  _d = alloc(duality_data,dl_ctx.get_manager());
+  _d = 0;
-  _d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx);
-  _d->rpfp = alloc(RPFP,_d->ls);
 }
 
 
 dl_interface::~dl_interface() {
+  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