added mbqi.id option, working on quantifiers in duality

src/duality/duality.h

@@ -79,9 +79,12 @@ namespace Duality {
 
       int CumulativeDecisions();
 
+      int CountOperators(const Term &t);
+
   private:
 
       void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
+      int CountOperatorsRec(hash_set<ast> &memo, const Term &t);
 
 };
 
@@ -280,7 +283,7 @@ namespace Duality {
       public:
 	std::list<Edge *> edges;
 	std::list<Node *> nodes;
-	std::list<Edge *> constraints;
+	std::list<std::pair<Edge *,Term> > constraints;
       };
       
       
@@ -556,6 +559,7 @@ namespace Duality {
 	  edge to their values in the current assignment. */
       void FixCurrentState(Edge *root);
     
+      void FixCurrentStateFull(Edge *edge);
 
       /** Declare a constant in the background theory. */
 
@@ -653,7 +657,11 @@ namespace Duality {
       Term ComputeUnderapprox(Node *root, int persist);
 
       /** Try to strengthen the annotation of a node by removing disjuncts. */
-      void Generalize(Node *node);
+      void Generalize(Node *root, Node *node);
+
+
+      /** Compute disjunctive interpolant for node by case splitting */
+      void InterpolateByCases(Node *root, Node *node);
 
       /** Push a scope. Assertions made after Push can be undone by Pop. */
       
@@ -687,6 +695,10 @@ namespace Duality {
       
       void Pop(int num_scopes);
       
+      /** Erase the proof by performing a Pop, Push and re-assertion of
+	  all the popped constraints */
+      void PopPush();
+
       /** Return true if the given edge is used in the proof of unsat.
 	  Can be called only after Solve or Check returns an unsat result. */
       
@@ -861,6 +873,11 @@ namespace Duality {
 
       Term UnderapproxFormula(const Term &f, hash_set<ast> &dont_cares);
 
+      void ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
+			    hash_set<ast> &done, hash_set<ast> &dont_cares);
+
+      Term UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares);
+
       Term ToRuleRec(Edge *e,  hash_map<ast,Term> &memo, const Term &t, std::vector<expr> &quants);
 
       hash_map<ast,Term> resolve_ite_memo;
@@ -896,6 +913,11 @@ namespace Duality {
       expr SimplifyOr(std::vector<expr> &lits);
 
       void SetAnnotation(Node *root, const expr &t);
+
+      void AddEdgeToSolver(Edge *edge);
+
+      void AddToProofCore(hash_set<ast> &core);
+
     };
     
     /** RPFP solver base class. */

src/duality/duality_rpfp.cpp

@@ -125,6 +125,32 @@ namespace Duality {
     }
   }
 
+  int Z3User::CountOperatorsRec(hash_set<ast> &memo, const Term &t){
+    if(memo.find(t) != memo.end())
+      return 0;
+    memo.insert(t);
+    if(t.is_app()){
+      decl_kind k = t.decl().get_decl_kind();
+      if(k == And || k == Or){
+	int count = 1;
+	int nargs = t.num_args();
+	for(int i = 0; i < nargs; i++)
+	  count += CountOperatorsRec(memo,t.arg(i));
+	return count;
+      }
+      return 0;
+    }
+    if(t.is_quantifier())
+      return CountOperatorsRec(memo,t.body())+1;
+    return 0;
+  }
+
+  int Z3User::CountOperators(const Term &t){
+    hash_set<ast> memo;
+    return CountOperatorsRec(memo,t);
+  }
+
+
   Z3User::Term Z3User::conjoin(const std::vector<Term> &args){
     return ctx.make(And,args);
   }
@@ -329,7 +355,15 @@ namespace Duality {
 	res = f(args.size(),&args[0]);
       }
     else if (t.is_quantifier())
-      res = CloneQuantifier(t,SubstRec(memo, t.body()));
+      {
+	std::vector<expr> pats;
+	t.get_patterns(pats);
+	for(unsigned i = 0; i < pats.size(); i++)
+	  pats[i] = SubstRec(memo,pats[i]);
+	Term body = SubstRec(memo,t.body());
+	res = clone_quantifier(t, body, pats);
+      }
+    // res = CloneQuantifier(t,SubstRec(memo, t.body()));
     else res = t;
     return res;
   }
@@ -552,7 +586,7 @@ namespace Duality {
   void RPFP::ConstrainEdgeLocalized(Edge *e, const Term &tl)
   {
     e->constraints.push_back(tl);
-    stack.back().constraints.push_back(e);
+    stack.back().constraints.push_back(std::pair<Edge *,Term>(e,tl));
     slvr.add(tl);
   }
 
@@ -1142,7 +1176,8 @@ namespace Duality {
 	  }
 	}
 	/* Unreachable! */
-	std::cerr << "error in RPFP::ImplicantRed";
+	// TODO: need to indicate this failure to caller
+	// std::cerr << "error in RPFP::ImplicantRed";
 	goto done;
       }
       else if(k == Not) {
@@ -1161,6 +1196,31 @@ namespace Duality {
     done[truth].insert(f);
   }
 
+  void RPFP::ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
+			      hash_set<ast> &done, hash_set<ast> &dont_cares){
+    if(done.find(f) != done.end())
+      return; /* already processed */
+    if(f.is_app()){
+      int nargs = f.num_args();
+      decl_kind k = f.decl().get_decl_kind();
+      if(k == Implies || k == Iff || k == And || k == Or || k == Not){
+	for(int i = 0; i < nargs; i++)
+	  ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares);
+	goto done;
+      }
+    }
+    {
+      if(dont_cares.find(f) == dont_cares.end()){
+	int b = SubtermTruth(memo,f);
+	if(b != 0 && b != 1) goto done;
+	expr bv = (b==1) ? f : !f;
+	lits.push_back(bv);
+      }
+    }
+  done:
+    done.insert(f);
+  }
+
   RPFP::Term RPFP::ResolveIte(hash_map<ast,int> &memo, const Term &t, std::vector<Term> &lits,
 			hash_set<ast> *done, hash_set<ast> &dont_cares){
     if(resolve_ite_memo.find(t) != resolve_ite_memo.end())
@@ -1223,6 +1283,16 @@ namespace Duality {
     return conjoin(lits);
   }
 
+  RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares){
+    /* first compute truth values of subterms */
+    hash_map<ast,int> memo;
+    hash_set<ast> done;
+    std::vector<Term> lits;
+    ImplicantFullRed(memo,f,lits,done,dont_cares);
+    /* return conjunction of literals */
+    return conjoin(lits);
+  }
+
   struct VariableProjector : Z3User {
   
     struct elim_cand {
@@ -1759,6 +1829,17 @@ namespace Duality {
     ConstrainEdgeLocalized(edge,eu);
   }
 
+  void RPFP::FixCurrentStateFull(Edge *edge){
+    hash_set<ast> dont_cares;
+    resolve_ite_memo.clear();
+    timer_start("UnderapproxFormula");
+    Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual;
+    for(unsigned i = 0; i < edge->constraints.size(); i++)
+      dual = dual && edge->constraints[i];
+    Term eu = UnderapproxFullFormula(dual,dont_cares);
+    timer_stop("UnderapproxFormula");
+    ConstrainEdgeLocalized(edge,eu);
+  }
 
 
   RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){
@@ -1803,6 +1884,7 @@ namespace Duality {
     res = CreateRelation(p->Annotation.IndParams,funder);
   }
 
+#if 0
   void RPFP::GreedyReduce(solver &s, std::vector<expr> &conjuncts){
     // verify
     s.push();
@@ -1829,6 +1911,36 @@ namespace Duality {
       }
     }
   }
+#endif
+
+  void RPFP::GreedyReduce(solver &s, std::vector<expr> &conjuncts){
+    std::vector<expr> lits(conjuncts.size());
+    for(unsigned i = 0; i < lits.size(); i++){
+      func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort());
+      lits[i] = pred();
+      s.add(ctx.make(Implies,lits[i],conjuncts[i]));
+    }
+    
+    // verify
+    check_result res = s.check(lits.size(),&lits[0]);
+    if(res != unsat)
+      throw "should be unsat";
+    
+    for(unsigned i = 0; i < conjuncts.size(); ){
+      std::swap(conjuncts[i],conjuncts.back());
+      std::swap(lits[i],lits.back());
+      check_result res = s.check(lits.size()-1,&lits[0]);
+      if(res != unsat){
+	std::swap(conjuncts[i],conjuncts.back());
+	std::swap(lits[i],lits.back());
+	i++;
+      }
+      else {
+	conjuncts.pop_back();
+	lits.pop_back();
+      }
+    }
+  }
 
   void RPFP::NegateLits(std::vector<expr> &lits){
     for(unsigned i = 0; i < lits.size(); i++){
@@ -1848,20 +1960,56 @@ namespace Duality {
     return ctx.make(Or,lits);
   }
 
-  void RPFP::Generalize(Node *node){
+    // set up edge constraint in aux solver
-    std::vector<expr> conjuncts;
+  void RPFP::AddEdgeToSolver(Edge *edge){
-    expr fmla = GetAnnotation(node);
-    CollectConjuncts(fmla,conjuncts,false);
-    // try to remove conjuncts one at a tme
-    aux_solver.push();
-    Edge *edge = node->Outgoing;
     if(!edge->dual.null())
       aux_solver.add(edge->dual);
     for(unsigned i = 0; i < edge->constraints.size(); i++){
       expr tl = edge->constraints[i];
       aux_solver.add(tl);
     }
-    GreedyReduce(aux_solver,conjuncts);
+  }
+
+  void RPFP::InterpolateByCases(Node *root, Node *node){
+    aux_solver.push();
+    AddEdgeToSolver(node->Outgoing);
+    node->Annotation.SetEmpty();
+    hash_set<ast> *core = new hash_set<ast>;
+    core->insert(node->Outgoing->dual);
+    while(1){
+      aux_solver.push();
+      aux_solver.add(!GetAnnotation(node));
+      if(aux_solver.check() == unsat){
+	aux_solver.pop(1);
+	break;
+      }
+      dualModel = aux_solver.get_model();
+      aux_solver.pop(1);
+      Push();
+      FixCurrentStateFull(node->Outgoing);
+      ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node));
+      check_result foo = Check(root);
+      if(foo != unsat)
+	throw "should be unsat";
+      AddToProofCore(*core);
+      Transformer old_annot = node->Annotation;
+      SolveSingleNode(root,node);
+      Pop(1);
+      node->Annotation.UnionWith(old_annot);
+    }
+    if(proof_core)
+      delete proof_core; // shouldn't happen
+    proof_core = core;
+    aux_solver.pop(1);
+  }
+
+  void RPFP::Generalize(Node *root, Node *node){
+    aux_solver.push();
+    AddEdgeToSolver(node->Outgoing);
+    expr fmla = GetAnnotation(node);
+    std::vector<expr> conjuncts;
+    CollectConjuncts(fmla,conjuncts,false);
+    GreedyReduce(aux_solver,conjuncts);     // try to remove conjuncts one at a tme
     aux_solver.pop(1);
     NegateLits(conjuncts);
     SetAnnotation(node,SimplifyOr(conjuncts));
@@ -1887,12 +2035,26 @@ namespace Duality {
 	  (*it)->dual = expr(ctx,NULL);
 	for(std::list<Node *>::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it)
 	  (*it)->dual = expr(ctx,NULL);
-	for(std::list<Edge *>::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it)
+	for(std::list<std::pair<Edge *,Term> >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it)
-	  (*it)->constraints.pop_back();
+	  (*it).first->constraints.pop_back();
 	stack.pop_back();
       }
   }
   
+  /** Erase the proof by performing a Pop, Push and re-assertion of
+      all the popped constraints */
+
+  void RPFP::PopPush(){
+    slvr.pop(1);
+    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);
+    for(std::list<Node *>::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it)
+      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);
+  }
   
   
   
@@ -2325,13 +2487,17 @@ namespace Duality {
     
   }
 
+  void RPFP::AddToProofCore(hash_set<ast> &core){
+    std::vector<expr> assumps;
+    slvr.get_proof().get_assumptions(assumps);
+    for(unsigned i = 0; i < assumps.size(); i++)
+      core.insert(assumps[i]);
+  }
+  
   void RPFP::ComputeProofCore(){
     if(!proof_core){
-      std::vector<expr> assumps;
-      slvr.get_proof().get_assumptions(assumps);
       proof_core = new hash_set<ast>;
-      for(unsigned i = 0; i < assumps.size(); i++)
+      AddToProofCore(*proof_core);
-	proof_core->insert(assumps[i]);
     }
   }
 

src/duality/duality_solver.cpp

@@ -1754,12 +1754,14 @@ namespace Duality {
 	      for(unsigned i = 0; i < expansions.size(); i++){
 		Node *node = expansions[i];
 		tree->SolveSingleNode(top,node);
-		tree->Generalize(node);
+		if(expansions.size() == 1 && NodeTooComplicated(node))
+		  SimplifyNode(node);
+		tree->Generalize(top,node);
 		if(RecordUpdate(node))
 		  update_count++;
 	      }
 	      if(update_count == 0)
-		std::cout << "backtracked without learning\n";
+		reporter->Message("backtracked without learning");
 	    }
 	    tree->ComputeProofCore(); // need to compute the proof core before popping solver
 	    while(1) {
@@ -1816,6 +1818,16 @@ namespace Duality {
 	}
       }
       
+      bool NodeTooComplicated(Node *node){
+	return tree->CountOperators(node->Annotation.Formula) > 5;
+      }
+
+      void SimplifyNode(Node *node){
+	// have to destroy the old proof to get a new interpolant
+	tree->PopPush();
+	tree->InterpolateByCases(top,node);
+      }
+
       bool LevelUsedInProof(unsigned level){
 	std::vector<Node *> &expansions = stack[level].expansions;
 	for(unsigned i = 0; i < expansions.size(); i++)

src/duality/duality_wrapper.cpp

@@ -34,8 +34,12 @@ namespace Duality {
     p.set_bool("proof", true); // this is currently useless
     p.set_bool("model", true); 
     p.set_bool("unsat_core", true); 
+    p.set_bool("mbqi",true);
+    p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
+    p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants
     scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
     m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
+    m_solver->updt_params(p); // why do we have to do this?
     canceled = false;
   }
 

src/duality/duality_wrapper.h

@@ -413,6 +413,7 @@ namespace Duality {
 
         expr operator()(unsigned n, expr const * args) const;
         expr operator()(const std::vector<expr> &args) const;
+        expr operator()() const;
         expr operator()(expr const & a) const;
         expr operator()(int a) const;
         expr operator()(expr const & a1, expr const & a2) const;
@@ -1184,6 +1185,9 @@ namespace Duality {
     inline expr func_decl::operator()(const std::vector<expr> &args) const {
       return operator()(args.size(),&args[0]);
     }
+    inline expr func_decl::operator()() const {
+      return operator()(0,0);
+    }
     inline expr func_decl::operator()(expr const & a) const {
       return operator()(1,&a);
     }

src/interp/iz3mgr.cpp

@@ -190,7 +190,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
 			     op == Forall, 
 			     names.size(), &types[0], &names[0], abs_body.get(),            
 			     0, 
-			     symbol(),
+			     symbol("itp"),
 			     symbol(),
 			     0, 0,
 			     0, 0
@@ -761,6 +761,19 @@ int iz3mgr::occurs_in(ast var, ast e){
 }
 
 
+bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){
+  if(op(x) == Plus){
+    int n = num_args(x);
+    for(int i = 0; i < n; i++){
+      if(arg(x,i) == v){
+	res = z3_simplify(make(Sub, y, make(Sub, x, v)));
+	return true;
+      }
+    }
+  }
+  return false;
+}
+
 // find a controlling equality for a given variable v in a term
 // a controlling equality is of the form v = t, which, being
 // false would force the formula to have the specifid truth value
@@ -774,6 +787,9 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, as
   if(!truth && op(e) == Equal){
     if(arg(e,0) == v) return(arg(e,1));
     if(arg(e,1) == v) return(arg(e,0));
+    ast res;
+    if(solve_arith(v,arg(e,0),arg(e,1),res)) return res;
+    if(solve_arith(v,arg(e,1),arg(e,0),res)) return res;
   }
   if((!truth && op(e) == And) || (truth && op(e) == Or)){
     int nargs = num_args(e);
@@ -836,6 +852,14 @@ iz3mgr::ast iz3mgr::subst(stl_ext::hash_map<ast,ast> &subst_memo,ast e){
   // 2) bound variable must be equal to some term -> substitute
 
 iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){
+  if((quantifier == Forall && op(e) == And)
+     || (quantifier == Exists && op(e) == Or)){
+    int n = num_args(e);
+    std::vector<ast> args(n);
+    for(int i = 0; i < n; i++)
+      args[i] = apply_quant(quantifier,var,arg(e,i));
+    return make(op(e),args);
+  }
   if(!occurs_in(var,e))return e;
   hash_set<ast> cont_eq_memo; 
   ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e);

src/interp/iz3mgr.h

@@ -692,13 +692,14 @@ class iz3mgr  {
 
  protected:
   ast_manager &m_manager;
+  int occurs_in(ast var, ast e);
 
  private:
   ast mki(family_id fid, decl_kind sk, int n, raw_ast **args);
   ast make(opr op, int n, raw_ast **args);
   ast make(symb sym, int n, raw_ast **args);
   int occurs_in1(stl_ext::hash_map<ast,bool> &occurs_in_memo, ast var, ast e);
-  int occurs_in(ast var, ast e);
+  bool solve_arith(const ast &v, const ast &x, const ast &y, ast &res);
   ast cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, ast v, ast e);
   ast subst(stl_ext::hash_map<ast,ast> &subst_memo, ast var, ast t, ast e);
 

src/interp/iz3proof_itp.cpp

@@ -138,7 +138,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
   
   symb normal;
 
+  /** Stand-ins for quantifiers */
 
+  symb sforall, sexists;
 
 
   ast get_placeholder(ast t){
@@ -231,6 +233,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast neg_pivot_lit = mk_not(atom);
     if(op(pivot) != Not)
       std::swap(premise1,premise2);
+    if(op(pivot) == Equal && op(arg(pivot,0)) == Select && op(arg(pivot,1)) == Select){
+      neg_pivot_lit = mk_not(neg_pivot_lit);
+      std::swap(premise1,premise2);
+    }      
     return resolve_arith_rec1(memo, neg_pivot_lit, premise1, premise2);
   }
   
@@ -355,7 +361,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	break;
       }
       default:
-	res = itp2;
+	{
+	  symb s = sym(itp2);
+	  if(s == sforall || s == sexists)
+	    res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1)));
+	  else
+	    res = itp2;
+	}
       }
     }
     return res;
@@ -385,7 +397,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	break;
       }
       default:
-	res = itp1;
+	{
+	  symb s = sym(itp1);
+	  if(s == sforall || s == sexists)
+	    res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2));
+	  else
+	    res = itp1;
+	}
       }
     }
     return res;
@@ -1897,6 +1915,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return itp;
   }
 
+  ast capture_localization(ast e){
+    // #define CAPTURE_LOCALIZATION
+#ifdef CAPTURE_LOCALIZATION
+    for(int i = localization_vars.size() - 1; i >= 0; i--){
+      LocVar &lv = localization_vars[i];
+      if(occurs_in(lv.var,e)){
+	symb q = (pv->in_range(lv.frame,rng)) ? sexists : sforall; 
+	e = make(q,make(Equal,lv.var,lv.term),e); // use Equal because it is polymorphic
+      }
+    }
+#endif
+    return e;
+  }
+
   /** Make an axiom node. The conclusion must be an instance of an axiom. */
   virtual node make_axiom(const std::vector<ast> &conclusion, prover::range frng){
     int nargs = conclusion.size();
@@ -1920,7 +1952,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
     
     for(unsigned i = 0; i < eqs.size(); i++)
       itp = make_mp(eqs[i],itp,pfs[i]);
-    return itp;
+    return capture_localization(itp);
   }
 
   virtual node make_axiom(const std::vector<ast> &conclusion){
@@ -2405,12 +2437,89 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return new_var;
   }
 
+  ast delete_quant(hash_map<ast,ast> &memo, const ast &v, const ast &e){
+    std::pair<ast,ast> foo(e,ast());
+    std::pair<hash_map<ast,ast>::iterator,bool> bar = memo.insert(foo);
+    ast &res = bar.first->second;
+    if(bar.second){
+      opr o = op(e);
+      switch(o){
+      case Or:
+      case And:
+      case Implies: {
+	unsigned nargs = num_args(e);
+	std::vector<ast> args; args.resize(nargs);
+	for(unsigned i = 0; i < nargs; i++)
+	  args[i] = delete_quant(memo, v, arg(e,i));
+	res = make(o,args);
+	break;
+      }
+      case Uninterpreted: {
+	symb s = sym(e);
+	ast w = arg(arg(e,0),0);
+	if(s == sforall || s == sexists){
+	  res = delete_quant(memo,v,arg(e,1));
+	  if(w != v)
+	    res = make(s,w,res);
+	  break;
+	}
+      }
+      default:
+	res = e;
+      }
+    }
+    return res;
+  }
+
+  ast insert_quants(hash_map<ast,ast> &memo, const ast &e){
+    std::pair<ast,ast> foo(e,ast());
+    std::pair<hash_map<ast,ast>::iterator,bool> bar = memo.insert(foo);
+    ast &res = bar.first->second;
+    if(bar.second){
+      opr o = op(e);
+      switch(o){
+      case Or:
+      case And:
+      case Implies: {
+	unsigned nargs = num_args(e);
+	std::vector<ast> args; args.resize(nargs);
+	for(unsigned i = 0; i < nargs; i++)
+	  args[i] = insert_quants(memo, arg(e,i));
+	res = make(o,args);
+	break;
+      }
+      case Uninterpreted: {
+	symb s = sym(e);
+	if(s == sforall || s == sexists){
+	  opr q = (s == sforall) ? Forall : Exists;
+	  ast v = arg(arg(e,0),0);
+	  hash_map<ast,ast> dmemo;
+	  ast body = delete_quant(dmemo,v,arg(e,1));
+	  body = insert_quants(memo,body);
+	  res = apply_quant(q,v,body);
+	  break;
+	}
+      }
+      default:
+	res = e;
+      }
+    }
+    return res;
+  }
+
   ast add_quants(ast e){
+#ifdef CAPTURE_LOCALIZATION
+    if(!localization_vars.empty()){
+      hash_map<ast,ast> memo;
+      e = insert_quants(memo,e);
+    }
+#else
     for(int i = localization_vars.size() - 1; i >= 0; i--){
       LocVar &lv = localization_vars[i];
       opr quantifier = (pv->in_range(lv.frame,rng)) ? Exists : Forall; 
       e = apply_quant(quantifier,lv.var,e);
     }
+#endif
     return e;
   }
 
@@ -2446,7 +2555,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast npP = make_mp(make(Iff,nPloc,nP),npPloc,neqpf);
     ast nrP = make_resolution(nP,conj2,npP);
     ast res = make_resolution(Ploc,rP,nrP);
-    return res;
+    return capture_localization(res);
   }
 
   ast get_contra_coeff(const ast &f){
@@ -2538,6 +2647,10 @@ public:
     m().inc_ref(normal_chain);
     normal = function("@normal",2,boolbooldom,bool_type());
     m().inc_ref(normal);
+    sforall = function("@sforall",2,boolbooldom,bool_type());
+    m().inc_ref(sforall);
+    sexists = function("@sexists",2,boolbooldom,bool_type());
+    m().inc_ref(sexists);
   }
 
   ~iz3proof_itp_impl(){

src/smt/params/qi_params.cpp

@@ -27,6 +27,7 @@ void qi_params::updt_params(params_ref const & _p) {
     m_mbqi_max_iterations = p.mbqi_max_iterations();
     m_mbqi_trace = p.mbqi_trace();
     m_mbqi_force_template = p.mbqi_force_template();
+    m_mbqi_id = p.mbqi_id();
     m_qi_profile = p.qi_profile();
     m_qi_profile_freq = p.qi_profile_freq();
     m_qi_max_instances = p.qi_max_instances();

src/smt/params/qi_params.h

@@ -51,6 +51,7 @@ struct qi_params {
     unsigned           m_mbqi_max_iterations;
     bool               m_mbqi_trace;
     unsigned           m_mbqi_force_template;
+    const char *       m_mbqi_id;
 
     qi_params(params_ref const & p = params_ref()):
         /*
@@ -97,7 +98,9 @@ struct qi_params {
         m_mbqi_max_cexs_incr(1),
         m_mbqi_max_iterations(1000),
         m_mbqi_trace(false),
-        m_mbqi_force_template(10) {
+	m_mbqi_force_template(10),
+        m_mbqi_id(0)  
+    {
         updt_params(p);
     }
 

src/smt/params/smt_params_helper.pyg

@@ -21,6 +21,7 @@ def_module_params(module_name='smt',
                           ('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'),
                           ('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'),
                           ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'),
+                          ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'),
                           ('qi.profile', BOOL, False, 'profile quantifier instantiation'),
                           ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'),
                           ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'),

src/smt/smt_model_checker.cpp

@@ -322,6 +322,7 @@ namespace smt {
 
         for (; it != end; ++it) {
             quantifier * q = *it;
+	    if(!m_qm->mbqi_enabled(q)) continue;
             if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
                 if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
                     verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";

src/smt/smt_quantifier.cpp

@@ -335,6 +335,10 @@ namespace smt {
         return m_imp->m_plugin->model_based();
     }
 
+    bool quantifier_manager::mbqi_enabled(quantifier *q) const {
+        return m_imp->m_plugin->mbqi_enabled(q);
+    }
+
     void quantifier_manager::adjust_model(proto_model * m) {
         m_imp->m_plugin->adjust_model(m);
     }
@@ -434,10 +438,24 @@ namespace smt {
 
         virtual bool model_based() const { return m_fparams->m_mbqi; }
 
+        virtual bool mbqi_enabled(quantifier *q) const { 
+	  if(!m_fparams->m_mbqi_id) return true;
+	  const symbol &s = q->get_qid();
+	  unsigned len = strlen(m_fparams->m_mbqi_id);
+	  if(s == symbol::null || s.is_numerical())
+	    return len == 0;
+	  return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;
+	}
+
+      /* Quantifier id's must begin with the prefix specified by
+	 parameter mbqi.id to be instantiated with MBQI.  The default
+	 value is the empty string, so all quantifiers are
+	 instantiated.
+       */
         virtual void add(quantifier * q) {
-            if (m_fparams->m_mbqi) {
+	  if (m_fparams->m_mbqi && mbqi_enabled(q)) {
-                m_model_finder->register_quantifier(q);
+	    m_model_finder->register_quantifier(q);
-            }
+	  }
         }
 
         virtual void del(quantifier * q) {

src/smt/smt_quantifier.h

@@ -75,6 +75,7 @@ namespace smt {
         };
 
         bool model_based() const;
+	bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
         void adjust_model(proto_model * m);
         check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
         
@@ -144,6 +145,11 @@ namespace smt {
          */
         virtual bool model_based() const = 0;
         
+        /**
+           \brief Is "model based" instantiate allowed to instantiate this quantifier?
+         */
+	virtual bool mbqi_enabled(quantifier *q) const {return true;}
+
         /**
            \brief Give a change to the plugin to adjust the interpretation of unintepreted functions.
            It can basically change the "else" of each uninterpreted function.