Merge branch 'interp' of https://git01.codeplex.com/z3 into interp

src/interp/iz3base.cpp

@@ -193,13 +193,14 @@ iz3base::ast iz3base::simplify(ast n){
   return res;
 }
 
-void iz3base::initialize(const std::vector<ast> &_parts, const std::vector<int> &_parents, const std::vector<ast> &theory){
+void iz3base::initialize(const std::vector<ast> &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory){
   cnsts = _parts;
+  theory = _theory;
   for(unsigned i = 0; i < cnsts.size(); i++)
     add_frame_range(i, cnsts[i]);
-  for(unsigned i = 0; i < theory.size(); i++){
-    add_frame_range(SHRT_MIN, theory[i]);
-    add_frame_range(SHRT_MAX, theory[i]);
+  for(unsigned i = 0; i < _theory.size(); i++){
+    add_frame_range(SHRT_MIN, _theory[i]);
+    add_frame_range(SHRT_MAX, _theory[i]);
   }
 }
 

src/interp/iz3base.h

@@ -65,6 +65,15 @@ class iz3base : public iz3mgr, public scopes {
     weak = false;
   }
 
+ iz3base(const iz3mgr& other,
+	 const std::vector<ast> &_cnsts,
+	 const std::vector<int> &_parents,
+	 const std::vector<ast> &_theory)
+   : iz3mgr(other), scopes(_parents)  {
+    initialize(_cnsts,_parents,_theory);
+    weak = false;
+  }
+
   /* Set our options */
   void set_option(const std::string &name, const std::string &value){
     if(name == "weak" && value == "1") weak = true;
@@ -87,6 +96,12 @@ class iz3base : public iz3mgr, public scopes {
     throw "no interpolator";
   }
 
+  ast get_proof_check_assump(range &rng){
+    std::vector<ast> cs(theory);
+    cs.push_back(cnsts[rng.hi]);
+    return make(And,cs);
+  }
+  
  private:
 
   struct ranges {
@@ -106,6 +121,7 @@ class iz3base : public iz3mgr, public scopes {
   void initialize(const std::vector<ast> &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory);
 
   std::vector<ast> cnsts;
+  std::vector<ast> theory;
 
   bool is_literal(ast n);
   void gather_conjuncts_rec(ast n, std::vector<ast> &conjuncts, stl_ext::hash_set<ast> &memo);

src/interp/iz3interp.cpp

@@ -0,0 +1,256 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+   iz3interp.cpp
+
+Abstract:
+
+   Interpolation based on proof translation.
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+/* Copyright 2011 Microsoft Research. */
+#include <assert.h>
+#include <algorithm>
+#include <stdio.h>
+#include <fstream>
+#include <sstream>
+#include <set>
+#include <iostream>
+
+#include "iz3profiling.h"
+#include "iz3translate.h"
+#include "iz3foci.h"
+#include "iz3proof.h"
+#include "iz3hash.h"
+#include "iz3interp.h"
+
+
+#ifndef WIN32
+using namespace stl_ext;
+#endif
+
+
+
+#if 1
+
+struct frame_reducer : public iz3mgr {
+  
+  int frames;
+  hash_map<ast,int> frame_map;
+  std::vector<int> assertions_map;
+  std::vector<int> orig_parents_copy;
+  std::vector<bool> used_frames;
+
+
+  frame_reducer(const iz3mgr &other)
+    : iz3mgr(other) {}
+
+  void get_proof_assumptions_rec(z3pf proof, hash_set<ast> &memo, std::vector<bool> &used_frames){
+    if(memo.count(proof))return;
+    memo.insert(proof);
+    pfrule dk = pr(proof);
+    if(dk == PR_ASSERTED){
+      ast con = conc(proof);
+      if(frame_map.find(con) != frame_map.end()){  // false for theory facts
+        int frame = frame_map[con];
+        used_frames[frame] = true;
+      }
+    }
+    else {
+      unsigned nprems = num_prems(proof);
+      for(unsigned i = 0; i < nprems; i++){
+	z3pf arg = prem(proof,i);
+	get_proof_assumptions_rec(arg,memo,used_frames);
+      }
+    }
+  }
+  
+  void get_frames(const std::vector<ast> &z3_preds, 
+		  const std::vector<int> &orig_parents,
+		  std::vector<ast> &assertions,
+		  std::vector<int> &parents,
+		  z3pf proof){
+    frames = z3_preds.size();
+    orig_parents_copy = orig_parents;
+    for(unsigned i = 0; i < z3_preds.size(); i++)
+      frame_map[z3_preds[i]] = i;
+    used_frames.resize(frames);
+    hash_set<ast> memo;
+    get_proof_assumptions_rec(proof,memo,used_frames);
+    std::vector<int> assertions_back_map(frames);
+
+    for(unsigned i = 0; i < z3_preds.size(); i++)
+      if(used_frames[i] || i == z3_preds.size() - 1){
+	assertions.push_back(z3_preds[i]);
+	assertions_map.push_back(i);
+        assertions_back_map[i] = assertions.size() - 1;
+      }
+    
+    if(orig_parents.size()){
+      parents.resize(assertions.size());
+      for(unsigned i = 0; i < assertions.size(); i++){
+	int p = orig_parents[assertions_map[i]];
+	while(p != SHRT_MAX && !used_frames[p])
+	  p = orig_parents[p];
+	parents[i] = p == SHRT_MAX ? p : assertions_back_map[p];
+      }
+    }
+
+    // std::cout << "used frames = " << frames << "\n";
+  }
+
+  void fix_interpolants(std::vector<ast> &interpolants){
+    std::vector<ast> unfixed = interpolants;
+    interpolants.resize(frames - 1);
+    for(int i = 0; i < frames - 1; i++)
+      interpolants[i] = mk_true();
+    for(unsigned i = 0; i < unfixed.size(); i++)
+      interpolants[assertions_map[i]] = unfixed[i];
+    for(int i = 0; i < frames-2; i++){
+      int p = orig_parents_copy.size() == 0 ? i+1 : orig_parents_copy[i];
+      if(p < frames - 1 && !used_frames[p])
+        interpolants[p] = interpolants[i];
+    }
+  }
+};
+
+#else
+struct frame_reducer {
+  
+
+
+  frame_reducer(context _ctx){
+  }
+
+  void get_frames(const std::vector<ast> &z3_preds, 
+		  const std::vector<int> &orig_parents,
+		  std::vector<ast> &assertions,
+		  std::vector<int> &parents,
+		  ast proof){
+    assertions = z3_preds;
+    parents = orig_parents;
+  }
+
+  void fix_interpolants(std::vector<ast> &interpolants){
+  }
+};
+
+#endif  
+
+
+#if 0
+static lbool test_secondary(context ctx,
+			 int num, 
+			 ast *cnsts,
+			 ast *interps,
+			 int *parents = 0
+			 ){
+      iz3secondary *sp = iz3foci::create(ctx,num,parents);
+      std::vector<ast> frames(num), interpolants(num-1);
+      std::copy(cnsts,cnsts+num,frames.begin());
+      int res = sp->interpolate(frames,interpolants);
+      if(res == 0)
+        std::copy(interpolants.begin(),interpolants.end(),interps);
+      return res ? L_TRUE : L_FALSE;
+}                         
+#endif
+    
+
+class iz3interp : public iz3mgr {
+public:
+  void proof_to_interpolant(z3pf proof,
+			    const std::vector<ast> &cnsts,
+			    const std::vector<int> &parents,
+			    std::vector<ast> &interps,
+			    const std::vector<ast> &theory,
+			    interpolation_options_struct *options = 0
+			    ){
+    
+    profiling::timer_start("Interpolation prep");
+
+    // get rid of frames not used in proof
+
+    std::vector<ast> cnsts_vec;
+    std::vector<int> parents_vec;
+    frame_reducer fr(*this);
+    fr.get_frames(cnsts,parents,cnsts_vec,parents_vec,proof);
+
+    int num = cnsts_vec.size();
+    std::vector<ast> interps_vec(num-1);
+    
+    // create a secondary prover
+    iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]);
+	  
+    // create a translator
+    iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory);
+    
+    // set the translation options, if needed
+    if(options)
+      for(hash_map<std::string,std::string>::iterator it = options->map.begin(), en = options->map.end(); it != en; ++it)
+	tr->set_option(it->first, it->second);
+    
+    // create a proof object to hold the translation
+    iz3proof pf(tr);
+    
+    profiling::timer_stop("Interpolation prep");
+
+    // translate into an interpolatable proof
+    profiling::timer_start("Proof translation");
+    tr->translate(proof,pf);
+    profiling::timer_stop("Proof translation");
+    
+    // translate the proof into interpolants
+    profiling::timer_start("Proof interpolation");
+    for(int i = 0; i < num-1; i++){
+      interps_vec[i] = pf.interpolate(tr->range_downward(i),tr->weak_mode());
+      interps_vec[i] = tr->quantify(interps_vec[i],tr->range_downward(i)); 
+    }
+    profiling::timer_stop("Proof interpolation");
+       
+    // put back in the removed frames
+    fr.fix_interpolants(interps_vec);
+
+    interps = interps_vec;
+    delete tr;
+    delete sp;
+  }
+
+  iz3interp(scoped_ptr<ast_manager> &_m_manager)
+    : iz3mgr(_m_manager) {}
+};
+
+void iz3interpolate(scoped_ptr<ast_manager> &_m_manager,
+		    ast *proof,
+		    const ptr_vector<ast> &cnsts,
+		    const ::vector<int> &parents,
+		    ptr_vector<ast> &interps,
+		    const ptr_vector<ast> theory,
+		    interpolation_options_struct * options)
+{
+  std::vector<ast_r> _cnsts(cnsts.size());
+  std::vector<int> _parents(parents.size());
+  std::vector<ast_r> _interps;
+  std::vector<ast_r> _theory(theory.size());
+  for(unsigned i = 0; i < cnsts.size(); i++)
+    _cnsts[i] = cnsts[i];
+  for(unsigned i = 0; i < parents.size(); i++)
+    _parents[i] = parents[i];
+  for(unsigned i = 0; i < theory.size(); i++)
+    _theory[i] = theory[i];
+  ast_r _proof(proof);
+  iz3interp itp(_m_manager);
+  itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options);
+  interps.resize(_interps.size());
+  for(unsigned i = 0; i < interps.size(); i++)
+    _interps[i] = interps[i];
+}
+

src/interp/iz3interp.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+   iz3interp.h
+
+Abstract:
+
+   Interpolation based on proof translation.
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+#ifndef IZ3_INTERP_H
+#define IZ3_INTERP_H
+
+#include "iz3hash.h"
+
+struct interpolation_options_struct {
+  stl_ext::hash_map<std::string,std::string> map;
+};
+
+
+typedef interpolation_options_struct *interpolation_options;
+
+void iz3interpolate(scoped_ptr<ast_manager> &_m_manager,
+		    ast *proof,
+		    const ptr_vector<ast> &cnsts,
+		    const ::vector<int> &parents,
+		    ptr_vector<ast> &interps,
+		    const ptr_vector<ast> theory,
+		    interpolation_options_struct * options = 0);
+
+#endif

src/interp/iz3mgr.cpp

@@ -65,7 +65,7 @@ iz3mgr::ast iz3mgr::make(opr op, ast &arg0){
   return make(op,1,&a);
 }
 
-iz3mgr::ast iz3mgr::make(opr op, ast &arg0, ast &arg1){
+iz3mgr::ast iz3mgr::make(opr op, const ast &arg0, const ast &arg1){
   raw_ast *args[2];
   args[0] = arg0.raw();
   args[1] = arg1.raw();
@@ -367,3 +367,10 @@ iz3mgr::opr iz3mgr::op(ast &t){
     }
     return Other;
 }
+
+
+iz3mgr::pfrule iz3mgr::pr(const ast &t){
+  func_decl *d = to_app(t.raw())->get_decl();
+  assert(m_basic_fid == d->get_family_id());
+  return d->get_decl_kind();
+}

src/interp/iz3mgr.h

@@ -63,9 +63,20 @@ class ast_r {
   bool eq(const ast_r &other) const {
     return _ast == other._ast;
   }
+  bool lt(const ast_r &other) const {
+    return _ast < other._ast;
+  }
   friend bool operator==(const ast_r &x, const ast_r&y){
     return x.eq(y);
   }
+  friend bool operator!=(const ast_r &x, const ast_r&y){
+    return !x.eq(y);
+  }
+  friend bool operator<(const ast_r &x, const ast_r&y){
+    return x.lt(y);
+  }
+  size_t hash() const {return (size_t)_ast;}
+  bool null() const {return !_ast;}
 };
 
 
@@ -101,6 +112,8 @@ class iz3mgr  {
   // typedef decl_kind opr;
   typedef func_decl *symb;
   typedef sort *type;
+  typedef ast_r z3pf;
+  typedef decl_kind pfrule;
 
   enum opr {
     True,
@@ -163,7 +176,7 @@ class iz3mgr  {
   ast make(opr op, const std::vector<ast> &args);
   ast make(opr op);
   ast make(opr op, ast &arg0);
-  ast make(opr op, ast &arg0, ast &arg1);
+  ast make(opr op, const ast &arg0, const ast &arg1);
   ast make(opr op, ast &arg0, ast &arg1, ast &arg2);
   ast make(symb sym, const std::vector<ast> &args);
   ast make(symb sym);
@@ -354,6 +367,16 @@ class iz3mgr  {
 
   ast mk_true() { return make(True); }
 
+  /** methods for destructing proof terms */
+
+  pfrule pr(const z3pf &t);
+
+  int num_prems(const z3pf &t){return to_app(t.raw())->get_num_args()-1;}
+  
+  z3pf prem(const z3pf &t, int n){return arg(t,n);}
+
+  z3pf conc(const z3pf &t){return arg(t,num_prems(t));}
+  
   /** For debugging */
   void show(ast);
 

src/interp/iz3scopes.cpp

@@ -31,7 +31,7 @@ int scopes::tree_lca(int n1, int n2){
   if(n1 == SHRT_MAX || n2 == SHRT_MAX) return SHRT_MAX;
   while(n1 != n2){
     if(n1 == SHRT_MAX || n2 == SHRT_MAX) return SHRT_MAX;
-    assert(n1 >= 0 && n2 >= 0 && n1 < parents.size() && n2 < parents.size());
+    assert(n1 >= 0 && n2 >= 0 && n1 < (int)parents.size() && n2 < (int)parents.size());
     if(n1 < n2) n1 = parents[n1];
     else n2 = parents[n2];
   }

src/interp/iz3translate.h

@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+   iz3translate.h
+
+Abstract:
+
+   Interface for proof translations from Z3 proofs to interpolatable
+   proofs.
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+
+#ifndef IZ3TRANSLATION_H
+#define IZ3TRANSLATION_H
+
+#include "iz3proof.h"
+#include "iz3secondary.h"
+
+// This is a interface class for translation from Z3 proof terms to
+// an interpolatable proof
+
+class iz3translation : public iz3base {
+public:
+  virtual iz3proof::node translate(ast, iz3proof &) = 0;
+  virtual ast quantify(ast e, const range &rng){return e;}
+  virtual ~iz3translation(){}
+
+  static iz3translation *create(iz3mgr &mgr,
+				iz3secondary *secondary,
+				const std::vector<ast> &frames,
+				const std::vector<int> &parents,
+                                const std::vector<ast> &theory);
+
+ protected:
+ iz3translation(iz3mgr &mgr,
+	 const std::vector<ast> &_cnsts,
+	 const std::vector<int> &_parents,
+	 const std::vector<ast> &_theory)
+   : iz3base(mgr,_cnsts,_parents,_theory)  {}
+};
+
+//#define IZ3_TRANSLATE_DIRECT2
+#define IZ3_TRANSLATE_DIRECT
+
+#endif
+
+
+