Merge /home/mcmillan/projects/z3_interp into interp

scripts/mk_util.py

@@ -1496,6 +1496,7 @@ def mk_config():
             if test_foci2(CXX,FOCI2LIB):
                 LDFLAGS  = '%s %s' % (LDFLAGS,FOCI2LIB)
                 SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB)
+                CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS
             else:
                 print "FAILED\n"
                 FOCI2 = False

src/duality/duality_rpfp.cpp

@@ -1636,7 +1636,8 @@ namespace Duality {
     dont_cares.insert(b);
     resolve_ite_memo.clear();
     timer_start("UnderapproxFormula");
-    Term eu = UnderapproxFormula(root->Outgoing->dual,dont_cares);
+    Term dual = root->Outgoing->dual.null() ? ctx.bool_val(true) : root->Outgoing->dual;
+    Term eu = UnderapproxFormula(dual,dont_cares);
     timer_stop("UnderapproxFormula");
     /* combine with children */
     chu.push_back(eu);
@@ -1944,6 +1945,8 @@ namespace Duality {
 
     for(unsigned i = 0; i < clauses.size(); i++){
       Term &clause = clauses[i];
+      if(clause.is_app() && clause.decl().get_decl_kind() == Uninterpreted)
+	clause = implies(ctx.bool_val(true),clause);
       if(!canonical_clause(clause))
 	clause = implies((!clause).simplify(),ctx.bool_val(false));
       Term head = clause.arg(1);

src/duality/duality_solver.cpp

@@ -916,7 +916,7 @@ namespace Duality {
 	return true;
       }
 #ifdef UNDERAPPROX_NODES
-      if(0 && last_decisions > 5000){
+      if(UseUnderapprox && last_decisions > 500){
 	std::cout << "making an underapprox\n";
 	ExpandNodeFromCoverFail(node);
       }
@@ -1642,7 +1642,7 @@ namespace Duality {
       std::set<Node *> old_choices;
 
       void ExpansionChoices(std::set<Node *> &best, bool high_priority){
-	if(!underapprox || constrained){
+	if(!underapprox || constrained || high_priority){
 	  ExpansionChoicesFull(best, high_priority);
 	  return;
 	}

src/duality/duality_wrapper.h

@@ -515,39 +515,39 @@ namespace Duality {
         }
 
         friend expr operator+(expr const & a, expr const & b) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_ADD,a,b));
+	  return a.ctx().make(Plus,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_ADD,a,b));
         }
 
         friend expr operator*(expr const & a, expr const & b) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_MUL,a,b));
+	  return a.ctx().make(Times,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_MUL,a,b));
 	}
 
         friend expr operator/(expr const & a, expr const & b) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_DIV,a,b));
+	  return a.ctx().make(Div,a,b); //  expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_DIV,a,b));
         }
 	
         friend expr operator-(expr const & a) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_UMINUS,a));
+	  return a.ctx().make(Uminus,a); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_UMINUS,a));
         }
 
         friend expr operator-(expr const & a, expr const & b) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_SUB,a,b));
+	  return a.ctx().make(Sub,a,b); // expr(a.ctx(),a.m().mk_app(a.ctx().m_arith_fid,OP_SUB,a,b));
         }
 
         friend expr operator<=(expr const & a, expr const & b) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LE,a,b));
+	  return a.ctx().make(Leq,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LE,a,b));
 	}
 
         friend expr operator>=(expr const & a, expr const & b) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GE,a,b));
+	  return a.ctx().make(Geq,a,b); //expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GE,a,b));
         }
 	
         friend expr operator<(expr const & a, expr const & b) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LT,a,b));
+	  return a.ctx().make(Lt,a,b); expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LT,a,b));
         }
         
         friend expr operator>(expr const & a, expr const & b) {
-	  return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GT,a,b));
+	  return a.ctx().make(Gt,a,b); expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GT,a,b));
 	}
 
         expr simplify() const;

src/interp/iz3foci.cpp

@@ -308,7 +308,11 @@ public:
   int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
     assert((int)cnsts.size() == frames);
     std::string lia("lia");
+#ifdef _FOCI2
     foci = foci2::create(lia);
+#else
+    foci = 0;
+#endif
     if(!foci){
       std::cerr << "iZ3: cannot find foci lia solver.\n";
       assert(0);

src/interp/iz3mgr.cpp

@@ -26,6 +26,7 @@ Revision History:
 #include <ostream>
 
 #include "expr_abstract.h"
+#include "params.h"
 
 
 #ifndef WIN32
@@ -145,19 +146,19 @@ iz3mgr::ast iz3mgr::make(symb sym){
   return make(sym,0,0);
 }
 
-iz3mgr::ast iz3mgr::make(symb sym, ast &arg0){
+iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0){
   raw_ast *a = arg0.raw();
   return make(sym,1,&a);
 }
 
-iz3mgr::ast iz3mgr::make(symb sym, ast &arg0, ast &arg1){
+iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0, const ast &arg1){
   raw_ast *args[2];
   args[0] = arg0.raw();
   args[1] = arg1.raw();
   return make(sym,2,args);
 }
 
-iz3mgr::ast iz3mgr::make(symb sym, ast &arg0, ast &arg1, ast &arg2){
+iz3mgr::ast iz3mgr::make(symb sym, const ast &arg0, const ast &arg1, const ast &arg2){
   raw_ast *args[3];
   args[0] = arg0.raw();
   args[1] = arg1.raw();
@@ -199,7 +200,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
 
 // FIXME replace this with existing Z3 functionality
 
-iz3mgr::ast iz3mgr::clone(ast &t, const std::vector<ast> &_args){
+iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector<ast> &_args){
   if(_args.size() == 0)
     return t;
 
@@ -242,6 +243,10 @@ void iz3mgr::show(ast t){
   std::cout  << mk_pp(t.raw(), m()) << std::endl;
 }
 
+void iz3mgr::show_symb(symb s){
+  std::cout  << mk_pp(s, m()) << std::endl;
+}
+
 void iz3mgr::print_expr(std::ostream &s, const ast &e){
   s << mk_pp(e.raw(), m());
 }
@@ -431,3 +436,203 @@ void iz3mgr::print_sat_problem(std::ostream &out, const ast &t){
   pp.set_simplify_implies(false);
   pp.display_smt2(out, to_expr(t.raw()));
 }
+
+iz3mgr::ast iz3mgr::z3_simplify(const ast &e){
+    ::expr * a = to_expr(e.raw());
+    params_ref p; 
+    th_rewriter m_rw(m(), p);
+    expr_ref    result(m());
+    m_rw(a, result);
+    return cook(result);
+}
+
+
+#if 0
+static rational lcm(const rational &x, const rational &y){
+  int a = x.numerator();
+  int b = y.numerator();
+  return rational(a * b / gcd(a, b));
+}
+#endif
+
+static rational extract_lcd(std::vector<rational> &res){
+  if(res.size() == 0) return rational(1); // shouldn't happen
+  rational lcd = denominator(res[0]);
+  for(unsigned i = 1; i < res.size(); i++)
+    lcd = lcm(lcd,denominator(res[i]));
+  for(unsigned i = 0; i < res.size(); i++)
+    res[i] *= lcd;
+  return lcd;
+}
+
+void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs){
+  std::vector<rational> rats;
+  get_farkas_coeffs(proof,rats);
+  coeffs.resize(rats.size());
+  for(unsigned i = 0; i < rats.size(); i++){
+    sort *is = m().mk_sort(m_arith_fid, INT_SORT);
+    ast coeff = cook(m_arith_util.mk_numeral(rats[i],is));
+    coeffs[i] = coeff;
+  }
+}
+
+void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
+  symb s = sym(proof);
+  int numps = s->get_num_parameters();
+  rats.resize(numps-2);
+  for(int i = 2; i < numps; i++){
+    rational r;
+    bool ok = s->get_parameter(i).is_rational(r);
+    if(!ok)
+      throw "Bad Farkas coefficient";
+    {
+      ast con = conc(prem(proof,i-2));
+      ast temp = make_real(r); // for debugging
+      opr o = is_not(con) ? op(arg(con,0)) : op(con);
+      if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt))
+	r = -r;
+    }
+    rats[i-2] = r;
+  }
+  if(rats.size() != 0 && rats[0].is_neg()){
+    for(unsigned i = 0; i < rats.size(); i++){
+      assert(rats[i].is_neg());
+      rats[i] = -rats[i];
+    }
+  }
+  extract_lcd(rats);
+}
+
+void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& coeffs){
+  std::vector<rational> rats;
+  get_assign_bounds_coeffs(proof,rats);
+  coeffs.resize(rats.size());
+  for(unsigned i = 0; i < rats.size(); i++){
+    coeffs[i] = make_int(rats[i]);
+  }
+}
+
+void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& rats){
+  symb s = sym(proof);
+  int numps = s->get_num_parameters();
+  rats.resize(numps-1);
+  rats[0] = rational(1);
+  for(int i = 2; i < numps; i++){
+    rational r;
+    bool ok = s->get_parameter(i).is_rational(r);
+    if(!ok)
+      throw "Bad Farkas coefficient";
+    {
+      ast con = arg(conc(proof),i-1);
+      ast temp = make_real(r); // for debugging
+      opr o = is_not(con) ? op(arg(con,0)) : op(con);
+      if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt))
+	r = -r;
+      r = -r;
+    }
+    rats[i-1] = r;
+  }
+  extract_lcd(rats);
+}
+
+  /** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */
+
+void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q){
+  ast Qrhs;
+  bool strict = op(P) == Lt;
+  if(is_not(Q)){
+    ast nQ = arg(Q,0);
+    switch(op(nQ)){
+    case Gt:
+      Qrhs = make(Sub,arg(nQ,1),arg(nQ,0));
+      break;
+    case Lt: 
+      Qrhs = make(Sub,arg(nQ,0),arg(nQ,1));
+      break;
+    case Geq:
+      Qrhs = make(Sub,arg(nQ,1),arg(nQ,0));
+      strict = true;
+      break;
+    case Leq: 
+      Qrhs = make(Sub,arg(nQ,0),arg(nQ,1));
+      strict = true;
+      break;
+    default:
+      throw "not an inequality";
+    }
+  }
+  else {
+    switch(op(Q)){
+    case Leq:
+      Qrhs = make(Sub,arg(Q,1),arg(Q,0));
+      break;
+    case Geq: 
+      Qrhs = make(Sub,arg(Q,0),arg(Q,1));
+      break;
+    case Lt:
+      Qrhs = make(Sub,arg(Q,1),arg(Q,0));
+      strict = true;
+      break;
+    case Gt: 
+      Qrhs = make(Sub,arg(Q,0),arg(Q,1));
+      strict = true;
+      break;
+    default:
+      throw "not an inequality";
+    }
+  }
+  Qrhs = make(Times,c,Qrhs);
+  if(strict)
+    P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
+  else
+    P = make(Leq,arg(P,0),make(Plus,arg(P,1),Qrhs));
+}
+
+iz3mgr::ast iz3mgr::sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs){
+  ast zero = make_int("0");
+  ast thing = make(Leq,zero,zero);
+  for(unsigned i = 0; i < ineqs.size(); i++){
+    linear_comb(thing,coeffs[i],ineqs[i]);
+  }
+  thing = simplify_ineq(thing);
+  return thing;
+}
+
+void iz3mgr::mk_idiv(const ast& t, const rational &d, ast &whole, ast &frac){
+  opr o = op(t);
+  if(o == Plus){
+    int nargs = num_args(t);
+    for(int i = 0; i < nargs; i++)
+      mk_idiv(arg(t,i),d,whole,frac);
+    return;
+  }
+  else if(o == Times){
+    rational coeff;
+    if(is_numeral(arg(t,0),coeff)){
+      if(gcd(coeff,d) == d){
+	whole = make(Plus,whole,make(Times,make_int(coeff/d),arg(t,1)));
+	return;
+      }
+    }
+  }
+  frac = make(Plus,frac,t);
+}
+
+iz3mgr::ast iz3mgr::mk_idiv(const ast& q, const rational &d){
+  ast t = z3_simplify(q);
+  if(d == rational(1))
+    return t;
+  else {
+    ast whole = make_int("0");
+    ast frac = whole;
+    mk_idiv(t,d,whole,frac);
+    return z3_simplify(make(Plus,whole,make(Idiv,z3_simplify(frac),make_int(d))));
+  }
+}
+
+iz3mgr::ast iz3mgr::mk_idiv(const ast& t, const ast &d){
+  rational r;
+  if(is_numeral(d,r))
+    return mk_idiv(t,r);
+  return make(Idiv,t,d);
+}

src/interp/iz3mgr.h

@@ -224,11 +224,11 @@ class iz3mgr  {
   ast make(opr op, const ast &arg0, const ast &arg1, const ast &arg2);
   ast make(symb sym, const std::vector<ast> &args);
   ast make(symb sym);
-  ast make(symb sym, ast &arg0);
-  ast make(symb sym, ast &arg0, ast &arg1);
-  ast make(symb sym, ast &arg0, ast &arg1, ast &arg2);
+  ast make(symb sym, const ast &arg0);
+  ast make(symb sym, const ast &arg0, const ast &arg1);
+  ast make(symb sym, const ast &arg0, const ast &arg1, const ast &arg2);
   ast make_quant(opr op, const std::vector<ast> &bvs, ast &body);
-  ast clone(ast &t, const std::vector<ast> &args);
+  ast clone(const ast &t, const std::vector<ast> &args);
 
   ast_manager &m() {return m_manager;}
 
@@ -276,6 +276,12 @@ class iz3mgr  {
     return ast();
   }
   
+  void get_args(const ast &t, std::vector<ast> &res){
+    res.resize(num_args(t));
+    for(unsigned i = 0; i < res.size(); i++)
+      res[i] = arg(t,i);
+  }
+
   symb sym(ast t){
     return to_app(t.raw())->get_decl();
   }
@@ -306,6 +312,19 @@ class iz3mgr  {
     return "NaN";
   }
 
+  bool is_numeral(const ast& t, rational &r){
+    expr* e = to_expr(t.raw());
+    assert(e);
+    return m_arith_util.is_numeral(e, r);
+  }
+
+  rational get_coeff(const ast& t){
+    rational res;
+    if(op(t) == Times && is_numeral(arg(t,0),res))
+      return res;
+    return rational(1);
+  }
+
   int get_quantifier_num_bound(const ast &t) {
     return to_quantifier(t.raw())->get_num_decls();
   }
@@ -337,6 +356,54 @@ class iz3mgr  {
     return to_func_decl(s)->get_range();
   }
 
+  int get_num_parameters(const symb &s){
+    return to_func_decl(s)->get_num_parameters();
+  }
+
+  ast get_ast_parameter(const symb &s, int idx){
+    return cook(to_func_decl(s)->get_parameters()[idx].get_ast());
+  }
+
+  enum lemma_theory {ArithTheory,UnknownTheory};
+
+  lemma_theory get_theory_lemma_theory(const ast &proof){
+    symb s = sym(proof);
+    ::symbol p0;
+    bool ok = s->get_parameter(0).is_symbol(p0);
+    if(!ok) return UnknownTheory;
+    std::string foo(p0.bare_str());
+    if(foo == "arith")
+      return ArithTheory;
+    return UnknownTheory;
+  }
+
+  enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,UnknownKind};
+
+  lemma_kind get_theory_lemma_kind(const ast &proof){
+    symb s = sym(proof);
+    ::symbol p0;
+    bool ok = s->get_parameter(1).is_symbol(p0);
+    if(!ok) return UnknownKind;
+    std::string foo(p0.bare_str());
+    if(foo == "farkas")
+      return FarkasKind;
+    if(foo == "triangle-eq")
+      return is_not(arg(conc(proof),0)) ? Eq2LeqKind : Leq2EqKind;
+    if(foo == "gcd-test")
+      return GCDTestKind;
+    if(foo == "assign-bounds")
+      return AssignBoundsKind;
+    return UnknownKind;
+  }
+
+  void get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs);
+
+  void get_farkas_coeffs(const ast &proof, std::vector<rational>& rats);
+
+  void get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& rats);
+
+  void get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& rats);
+
   bool is_true(ast t){
     return op(t) == True;
   }
@@ -357,6 +424,10 @@ class iz3mgr  {
     return op(t) == Not;
   }
   
+  /** Simplify an expression using z3 simplifier */
+
+  ast z3_simplify(const ast& e);
+
   // Some constructors that simplify things
 
   ast mk_not(ast x){
@@ -389,6 +460,41 @@ class iz3mgr  {
     return make(Or,x,y);
   }
 
+  ast mk_implies(ast x, ast y){
+    opr ox = op(x);
+    opr oy = op(y);
+    if(ox == True) return y;
+    if(oy == False) return mk_not(x);
+    if(ox == False) return mk_true();
+    if(oy == True) return y;
+    if(x == y) return mk_true();
+    return make(Implies,x,y);
+  }
+
+  ast mk_or(const std::vector<ast> &x){
+    ast res = mk_false();
+    for(unsigned i = 0; i < x.size(); i++)
+      res = mk_or(res,x[i]);
+    return res;
+  }
+
+  ast mk_and(const std::vector<ast> &x){
+    std::vector<ast> conjs;
+    for(unsigned i = 0; i < x.size(); i++){
+      const ast &e = x[i];
+      opr o = op(e);
+      if(o == False)
+	return mk_false();
+      if(o != True)
+	conjs.push_back(e);
+    }
+    if(conjs.size() == 0)
+      return mk_true();
+    if(conjs.size() == 1)
+      return conjs[0];
+    return make(And,conjs);
+  }
+
   ast mk_equal(ast x, ast y){
     if(x == y) return make(True);
     opr ox = op(x);
@@ -419,11 +525,74 @@ class iz3mgr  {
     return cook(m_arith_util.mk_numeral(rational(s.c_str()),r));
   }
 
+  ast make_int(const rational &s) {
+    sort *r = m().mk_sort(m_arith_fid, INT_SORT);
+    return cook(m_arith_util.mk_numeral(s,r));
+  }
+
+  ast make_real(const std::string &s) {
+    sort *r = m().mk_sort(m_arith_fid, REAL_SORT);
+    return cook(m_arith_util.mk_numeral(rational(s.c_str()),r));
+  }
+
+  ast make_real(const rational &s) {
+    sort *r = m().mk_sort(m_arith_fid, REAL_SORT);
+    return cook(m_arith_util.mk_numeral(s,r));
+  }
 
   ast mk_false() { return make(False); }
 
   ast mk_true() { return make(True); }
 
+  ast mk_fresh_constant(char const * prefix, type s){
+    return cook(m().mk_fresh_const(prefix, s));
+  }
+
+  type bool_type() {
+    ::sort *s = m().mk_sort(m_basic_fid, BOOL_SORT); 
+    return s;
+  }
+
+  type int_type()  {
+    ::sort *s = m().mk_sort(m_arith_fid, INT_SORT); 
+    return s;
+  }
+
+  type real_type()  {
+    ::sort *s = m().mk_sort(m_arith_fid, REAL_SORT); 
+    return s;
+  }
+
+  type array_type(type d, type r) {
+    parameter params[2]  = { parameter(d), parameter(to_sort(r)) };
+    ::sort * s =  m().mk_sort(m_array_fid, ARRAY_SORT, 2, params);
+    return s;
+  }
+
+  symb function(const std::string &str_name, unsigned arity, type *domain, type range) {
+    ::symbol name = ::symbol(str_name.c_str());
+    std::vector< ::sort *> sv(arity);
+    for(unsigned i = 0; i < arity; i++)
+      sv[i] = domain[i];
+    ::func_decl* d = m().mk_func_decl(name,arity,&sv[0],range);
+    return d;
+  }
+  
+  void linear_comb(ast &P, const ast &c, const ast &Q);
+
+  ast sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs);
+
+  ast simplify_ineq(const ast &ineq){
+    ast res = make(op(ineq),arg(ineq,0),z3_simplify(arg(ineq,1)));
+    return res;
+  }
+
+  void mk_idiv(const ast& t, const rational &d, ast &whole, ast &frac);
+
+  ast mk_idiv(const ast& t, const rational &d);
+
+  ast mk_idiv(const ast& t, const ast &d);
+  
   /** methods for destructing proof terms */
 
   pfrule pr(const z3pf &t);
@@ -437,6 +606,8 @@ class iz3mgr  {
   /** For debugging */
   void show(ast);
 
+  void show_symb(symb s);
+
   /** Constructor */
 
   void print_lit(ast lit);

src/interp/iz3proof_itp.h

@@ -0,0 +1,130 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    iz3proof.h
+
+Abstract:
+
+   This class defines a simple interpolating proof system.
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+#ifndef IZ3PROOF_ITP_H
+#define IZ3PROOF_ITP_H
+
+#include <set>
+
+#include "iz3base.h"
+#include "iz3secondary.h"
+
+// #define CHECK_PROOFS
+
+/** This class defines a simple proof system.
+
+    As opposed to iz3proof, this class directly computes interpolants,
+    so the proof representation is just the interpolant itself.
+    
+ */
+
+class iz3proof_itp : public iz3mgr {
+ public:
+
+  /** Enumeration of proof rules. */
+  enum rule {Resolution,Assumption,Hypothesis,Theory,Axiom,Contra,Lemma,Reflexivity,Symmetry,Transitivity,Congruence,EqContra};
+
+  /** Interface to prover. */
+  typedef iz3base prover;
+
+  /** Ast type. */
+  typedef prover::ast ast;
+
+  /** The type of proof nodes (just interpolants). */
+  typedef ast node;
+
+  /** Object thrown in case of a proof error. */
+  struct proof_error {};
+
+
+  /** Make a resolution node with given pivot literal and premises.
+      The conclusion of premise1 should contain the negation of the
+      pivot literal, while the conclusion of premise2 should containe the
+      pivot literal.
+   */
+  virtual node make_resolution(ast pivot, const std::vector<ast> &conc, node premise1, node premise2) = 0;
+
+  /** Make an assumption node. The given clause is assumed in the given frame. */
+  virtual node make_assumption(int frame, const std::vector<ast> &assumption) = 0;
+
+  /** Make a hypothesis node. If phi is the hypothesis, this is
+      effectively phi |- phi. */
+  virtual node make_hypothesis(const ast &hypothesis) = 0;
+
+  /** Make an axiom node. The conclusion must be an instance of an axiom. */
+  virtual node make_axiom(const std::vector<ast> &conclusion) = 0;
+
+  /** Make a Contra node. This rule takes a derivation of the form
+     Gamma |- False and produces |- \/~Gamma. */
+
+  virtual node make_contra(node prem, const std::vector<ast> &conclusion) = 0;
+
+  /** Make a Reflexivity node. This rule produces |- x = x */
+  
+  virtual node make_reflexivity(ast con) = 0;
+  
+  /** Make a Symmetry node. This takes a derivation of |- x = y and
+      produces | y = x */
+
+  virtual node make_symmetry(ast con, const ast &premcon, node prem) = 0;
+
+  /** Make a transitivity node. This takes derivations of |- x = y
+      and |- y = z produces | x = z */
+
+  virtual node make_transitivity(const ast &x, const ast &y, const ast &z, node prem1, node prem2) = 0;
+  
+  /** Make a congruence node. This takes a derivation of |- x_i = y_i
+      and produces |- f(...x_i,...) = f(...,y_i,...) */
+  
+  virtual node make_congruence(const ast &xi_eq_yi, const ast &con, const ast &prem1) = 0;
+
+  /** Make a modus-ponens node. This takes derivations of |- x
+      and |- x = y and produces |- y */
+  
+  virtual node make_mp(const ast &x_eq_y, const ast &prem1, const ast &prem2) = 0;
+
+  /** Make a farkas proof node. */
+
+  virtual node make_farkas(ast con, const std::vector<node> &prems, const std::vector<ast> &prem_cons, const std::vector<ast> &coeffs) = 0;
+
+  /* Make an axiom instance of the form |- x<=y, y<= x -> x =y */
+  virtual node make_leq2eq(ast x, ast y, const ast &xleqy, const ast &yleqx) = 0;
+
+  /* Make an axiom instance of the form |- x = y -> x <= y */
+  virtual node make_eq2leq(ast x, ast y, const ast &xeqy) = 0;
+
+  /* Make an inference of the form t <= c |- t/d <= floor(c/d) where t
+     is an affine term divisble by d and c is an integer constant */
+  virtual node make_cut_rule(const ast &tleqc, const ast &d, const ast &con, const ast &prem) = 0;
+
+  /** Create proof object to construct an interpolant. */
+  static iz3proof_itp *create(prover *p, const prover::range &r, bool _weak);
+
+ protected:
+  iz3proof_itp(iz3mgr &m)
+    : iz3mgr(m)
+  {
+  }
+
+ public:
+  virtual ~iz3proof_itp(){
+  }
+};
+
+#endif

src/interp/iz3translate.h

@@ -34,6 +34,10 @@ public:
   virtual ast quantify(ast e, const range &rng){return e;}
   virtual ~iz3translation(){}
 
+  /** This is thrown when the proof cannot be translated. */
+  struct unsupported {
+  };
+
   static iz3translation *create(iz3mgr &mgr,
 				iz3secondary *secondary,
 				const std::vector<ast> &frames,
@@ -49,7 +53,11 @@ public:
 };
 
 //#define IZ3_TRANSLATE_DIRECT2
+#ifndef _FOCI2
 #define IZ3_TRANSLATE_DIRECT
+#else
+#define IZ3_TRANSLATE_FULL
+#endif
 
 #endif