working on quantifiers in interpolation

src/interp/iz3base.h

@@ -153,8 +153,10 @@ class iz3base : public iz3mgr, public scopes {
 
   int frames;                               // number of frames
 
+ protected:
   void add_frame_range(int frame, ast t);
 
+ private:
   void initialize(const std::vector<ast> &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory);
 
   void initialize(const std::vector<std::vector<ast> > &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory);

src/interp/iz3mgr.cpp

@@ -240,7 +240,9 @@ iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector<ast> &_args){
 
 
 void iz3mgr::show(ast t){
-  std::cout  << mk_pp(t.raw(), m()) << std::endl;
+  params_ref p;
+  p.set_bool("flat_assoc",false);
+  std::cout  << mk_pp(t.raw(), m(), p) << std::endl;
 }
 
 void iz3mgr::show_symb(symb s){
@@ -248,7 +250,9 @@ void iz3mgr::show_symb(symb s){
 }
 
 void iz3mgr::print_expr(std::ostream &s, const ast &e){
-  s << mk_pp(e.raw(), m());
+  params_ref p;
+  p.set_bool("flat_assoc",false);
+  s << mk_pp(e.raw(), m(), p);
 }
 
 

src/interp/iz3proof_itp.cpp

@@ -417,7 +417,16 @@ class iz3proof_itp_impl : public iz3proof_itp {
     std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
     ast &res = bar.first->second;
     if(bar.second){
-      if(sym(e) == rotate_sum && var == get_placeholder(arg(e,0))){
+      symb g = sym(e);
+      if(g == rotate_sum){
+	if(var == get_placeholder(arg(e,0))){
+	  res = e;
+	}
+	else 
+	  res = make(rotate_sum,arg(e,0),subst_term_and_simp_rec(var,t,arg(e,1)));
+	return res;
+      }
+      if(g == concat){
 	res = e;
 	return res;
       }
@@ -453,18 +462,26 @@ class iz3proof_itp_impl : public iz3proof_itp {
       int nargs = num_args(e);
       std::vector<ast> args(nargs);
       bool placeholder_arg = false;
+      symb g = sym(e);
+      if(g == concat){
+	res = e;
+	return res;
+      }
       for(int i = 0; i < nargs; i++){
-	args[i] = simplify_rec(arg(e,i));
+	if(i == 0 && g == rotate_sum)
+	  args[i] = arg(e,i);
+	else
+	  args[i] = simplify_rec(arg(e,i));
 	placeholder_arg |= is_placeholder(args[i]);
       }
       try {
 	opr f = op(e);
 	if(f == Equal && args[0] == args[1]) res = mk_true();
 	else if(f == And) res = my_and(args);
-	else if(f == Or) res = my_or(args);
+	else if(f == Or)
+	  res = my_or(args);
 	else if(f == Idiv) res = mk_idiv(args[0],args[1]);
 	else if(f == Uninterpreted && !placeholder_arg){
-	  symb g = sym(e);
 	  if(g == rotate_sum) res = simplify_rotate(args);
 	  else if(g == symm) res = simplify_symm(args);
 	  else if(g == modpon) res = simplify_modpon(args);
@@ -1945,38 +1962,45 @@ class iz3proof_itp_impl : public iz3proof_itp {
     hash_map<ast,ast>::iterator it = localization_map.find(e);
     if(it != localization_map.end()){
       pf = localization_pf_map[e];
-      return it->second;
+      e = it->second;
     }
 
-    // if is is non-local, we must first localize the arguments to
-    // the range of its function symbol
-    
-    int nargs = num_args(e);
-    if(nargs > 0 /*  && (!is_local(e) || flo <= hi || fhi >= lo) */){
-      prover::range frng = rng;
-      if(op(e) == Uninterpreted){
-	symb f = sym(e);
-	prover::range srng = pv->sym_range(f);
-	if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible
-	  frng = pv->range_glb(srng,rng);
-      }
-      std::vector<ast> largs(nargs);
-      std::vector<ast> eqs;
-      std::vector<ast> pfs;
-      for(int i = 0; i < nargs; i++){
-	ast argpf;
-	largs[i] = localize_term(arg(e,i),frng,argpf);
-	frng = pv->range_glb(frng,pv->ast_scope(largs[i]));
-	if(largs[i] != arg(e,i)){
-	  eqs.push_back(make_equiv(largs[i],arg(e,i)));
-	  pfs.push_back(argpf);
+    else {
+      // if it is non-local, we must first localize the arguments to
+      // the range of its function symbol
+      
+      int nargs = num_args(e);
+      if(nargs > 0 /*  && (!is_local(e) || flo <= hi || fhi >= lo) */){
+	prover::range frng = rng;
+	if(op(e) == Uninterpreted){
+	  symb f = sym(e);
+	  prover::range srng = pv->sym_range(f);
+	  if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible
+	    frng = pv->range_glb(srng,rng);
+	  else
+	    frng = srng; // this term will be localized
 	}
+	std::vector<ast> largs(nargs);
+	std::vector<ast> eqs;
+	std::vector<ast> pfs;
+	for(int i = 0; i < nargs; i++){
+	  ast argpf;
+	  largs[i] = localize_term(arg(e,i),frng,argpf);
+	  frng = pv->range_glb(frng,pv->ast_scope(largs[i]));
+	  if(largs[i] != arg(e,i)){
+	    eqs.push_back(make_equiv(largs[i],arg(e,i)));
+	    pfs.push_back(argpf);
+	  }
+	}
+	
+	e = clone(e,largs);
+	if(pfs.size())
+	  pf = make_congruence(eqs,make_equiv(e,orig_e),pfs);
+	// assert(is_local(e));
       }
-
-      e = clone(e,largs);
-      if(pfs.size())
-	pf = make_congruence(eqs,make_equiv(e,orig_e),pfs);
-      // assert(is_local(e));
+      
+      localization_pf_map[orig_e] = pf;
+      localization_map[orig_e] = e;
     }
 
     if(pv->ranges_intersect(pv->ast_scope(e),rng))
@@ -1986,7 +2010,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
     int frame = pv->range_near(pv->ast_scope(e),rng);
 
     ast new_var = fresh_localization_var(e,frame);
-    localization_map[e] = new_var;
+    localization_map[orig_e] = new_var;
     std::vector<ast> foo; foo.push_back(make_equiv(new_var,e));
     ast bar = make_assumption(frame,foo);
     pf = make_transitivity(new_var,e,orig_e,bar,pf);

src/interp/iz3translate.cpp

@@ -105,6 +105,42 @@ public:
   range rng; // the range of frames in the "A" part of the interpolant
 #endif
 
+  /* To handle skolemization, we have to scan the proof for skolem
+     symbols and assign each to a frame. THe assignment is heuristic.
+  */
+
+  void scan_skolems_rec(hash_set<ast> &memo, const ast &proof){
+    std::pair<hash_set<ast>::iterator,bool> bar = memo.insert(proof);
+    if(!bar.second)
+      return;
+    pfrule dk = pr(proof);
+    if(dk == PR_SKOLEMIZE){
+      ast quanted = arg(conc(proof),0);
+      if(op(quanted) == Not)
+	quanted = arg(quanted,0);
+      range r = ast_range(quanted);
+      if(range_is_empty(r))
+	r = ast_scope(quanted);
+      if(range_is_empty(r))
+	throw "can't skolemize";
+      int frame = range_max(r);
+      if(frame >= frames) frame = frames - 1;
+      add_frame_range(frame,arg(conc(proof),1));
+      r = ast_scope(arg(conc(proof),1));
+    }
+    else {
+      unsigned nprems = num_prems(proof);
+      for(unsigned i = 0; i < nprems; i++){
+	scan_skolems_rec(memo,prem(proof,i));
+      }
+    }
+  }
+
+  void scan_skolems(const ast &proof){
+    hash_set<ast> memo;
+    scan_skolems_rec(memo,proof);
+  }
+
   // determine locality of a proof term
   // return frame of derivation if local, or -1 if not
   // result INT_MAX means the proof term is a tautology
@@ -115,7 +151,8 @@ public:
     std::pair<AstToInt::iterator, bool> bar = locality.insert(foo);
     int &res = bar.first->second;
     if(!bar.second) return res;
-    if(pr(proof) == PR_ASSERTED){
+    pfrule dk = pr(proof);
+    if(dk == PR_ASSERTED){
       ast ass = conc(proof);
       res = frame_of_assertion(ass);
 #ifdef NEW_LOCALITY
@@ -125,6 +162,12 @@ public:
 	res = frames-1;
 #endif
     }
+    else if(dk == PR_QUANT_INST){
+      std::vector<ast> lits;
+      ast con = conc(proof);
+      get_Z3_lits(con, lits);
+      iproof->make_axiom(lits);
+    }
     else {
       unsigned nprems = num_prems(proof);
       for(unsigned i = 0; i < nprems; i++){
@@ -563,6 +606,33 @@ public:
       return 1;
   }
 
+  void symbols_out_of_scope_rec(hash_set<ast> &memo, hash_set<symb> &symb_memo, int frame, const ast &t){
+    if(memo.find(t) != memo.end())
+      return;
+    memo.insert(t);
+    if(op(t) == Uninterpreted){
+      symb s = sym(t);
+      range r = sym_range(s);
+      if(!in_range(frame,r) && symb_memo.find(s) == symb_memo.end()){
+	std::cout << string_of_symbol(s) << "\n";
+	symb_memo.insert(s);
+      }
+    }
+    int nargs = num_args(t);
+    for(int i = 0; i < nargs; i++)
+      symbols_out_of_scope_rec(memo,symb_memo,frame,arg(t,i));
+  }
+
+  void symbols_out_of_scope(int frame, const ast &t){
+    hash_set<ast> memo;
+    hash_set<symb> symb_memo;
+    symbols_out_of_scope_rec(memo,symb_memo,frame,t);
+  }
+
+  void conc_symbols_out_of_scope(int frame, const ast &t){
+    symbols_out_of_scope(frame,conc(t));
+  }
+
   std::vector<ast> lit_trace;
   hash_set<ast> marked_proofs;
 
@@ -634,18 +704,36 @@ public:
     return !(f == And || f == Or || f == Iff);
   }
 
+  hash_map<int,ast> asts_by_id;
+
   void print_lit(const ast &lit){
     ast abslit = is_not(lit) ? arg(lit,0) : lit;
     if(!is_literal_or_lit_iff(lit)){
       if(is_not(lit)) std::cout << "~";
-      std::cout << "[";
-      // print_expr(std::cout,abslit);
-      std::cout << "]";
+      int id = ast_id(abslit);
+      asts_by_id[id] = abslit;
+      std::cout << "[" << id << "]";
     }
     else
       print_expr(std::cout,lit);
   }
 
+  void expand(int id){
+    if(asts_by_id.find(id) == asts_by_id.end())
+      std::cout << "undefined\n";
+    else {
+      ast lit = asts_by_id[id];
+      std::string s = string_of_symbol(sym(lit));
+      std::cout << "(" << s;
+      unsigned nargs = num_args(lit);
+      for(unsigned i = 0; i < nargs; i++){
+	std::cout << " ";
+	print_lit(arg(lit,i));
+      }
+      std::cout << ")\n";;
+    }
+  }
+
   void show_lit(const ast &lit){
     print_lit(lit);
     std::cout << "\n";
@@ -682,6 +770,8 @@ public:
       print_lit(lits[i]);
       std::cout << " ";
     }
+    range r = ast_scope(con);
+    std::cout << " {" << r.lo << "," << r.hi << "}";
     std::cout << "\n";
   }
 
@@ -753,8 +843,12 @@ public:
     ast prem0 = prem(proof,0);
     Iproof::node itp = translate_main(prem0,true);
     std::vector<ast> clause;
-    get_Z3_lits(conc(prem0),clause);
+    ast conc0 = conc(prem0);
     int nprems = num_prems(proof);
+    if(nprems == 2 && conc0 == mk_not(conc(prem(proof,1))))
+      clause.push_back(conc0);
+    else
+      get_Z3_lits(conc0,clause);
     for(int position = 1; position < nprems; position++){
       ast ante =  prem(proof,position);
       ast pnode = conc(ante);
@@ -1500,6 +1594,10 @@ public:
 	res = iproof->make_axiom(lits);
 	break;
       }
+      case PR_DEF_AXIOM: { // this should only happen for formulas resulting from quantifier instantiation
+	res = iproof->make_axiom(lits);
+	break;
+      }
       default:
 	assert(0 && "translate_main: unsupported proof rule");
 	throw unsupported();
@@ -1518,6 +1616,7 @@ public:
 
   iz3proof::node translate(ast proof, iz3proof &dst){
     std::vector<ast> itps;
+    scan_skolems(proof);
     for(int i = 0; i < frames -1; i++){
 #ifdef NEW_LOCALITY
       rng = range_downward(i);
@@ -1609,6 +1708,17 @@ void iz3translation_full_pfprem(iz3translation_full *p, int i){
   p->pfprem(i);
 }
 
+void iz3translation_full_expand(iz3translation_full *p, int i){
+  p->expand(i);
+}
+
+void iz3translation_full_symbols_out_of_scope(iz3translation_full *p, int i, const iz3mgr::ast &t){
+  p->symbols_out_of_scope(i,t);
+}
+
+void iz3translation_full_conc_symbols_out_of_scope(iz3translation_full *p, int i, const iz3mgr::ast &t){
+  p->conc_symbols_out_of_scope(i,t);
+}
 
 struct stdio_fixer {
   stdio_fixer(){