fix #1330. Interpolation transformation needs to handle TRANSITIVITY_STAR

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/interp/iz3mgr.h

@@ -57,12 +57,12 @@ typedef ast raw_ast;
 
 /** Wrapper around an ast pointer */
 class ast_i {
- protected:
+protected:
     raw_ast *_ast;
- public:
+public:
     raw_ast * const &raw() const {return _ast;}
     ast_i(raw_ast *a){_ast = a;}
-  
+    
     ast_i(){_ast = 0;}
     bool eq(const ast_i &other) const {
         return _ast == other._ast;
@@ -86,19 +86,19 @@ class ast_i {
 /** Reference counting verison of above */
 class ast_r : public ast_i {
     ast_manager *_m;
- public:
- ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
+public:
+    ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
         _m = m;
         m->inc_ref(a);
     }
-  
+    
     ast_r() {_m = 0;}
-
- ast_r(const ast_r &other) : ast_i(other) {
+    
+    ast_r(const ast_r &other) : ast_i(other) {
         _m = other._m;
         if (_m) _m->inc_ref(_ast);
     }
-
+    
     ast_r &operator=(const ast_r &other) {
         if(_ast)
             _m->dec_ref(_ast);
@@ -107,12 +107,12 @@ class ast_r : public ast_i {
         if (_m) _m->inc_ref(_ast);
         return *this;
     }
-
-    ~ast_r(){
+    
+    ~ast_r() {
         if(_ast)
             _m->dec_ref(_ast);
     }
-  
+    
     ast_manager *mgr() const {return _m;}
 
 };

src/interp/iz3translate.cpp

@@ -29,6 +29,7 @@
 #include "interp/iz3profiling.h"
 #include "interp/iz3interp.h"
 #include "interp/iz3proof_itp.h"
+#include "ast/ast_pp.h"
 
 #include <assert.h>
 #include <algorithm>
@@ -1851,6 +1852,21 @@ public:
                 }
                 break;
             }
+            case PR_TRANSITIVITY_STAR: {
+                // assume the premises are x = y, y = z, z = u, u = v, ..
+                
+                ast x = arg(conc(prem(proof,0)),0);
+                ast y = arg(conc(prem(proof,0)),1);
+                ast z = arg(conc(prem(proof,1)),1);
+                res = iproof->make_transitivity(x,y,z,args[0],args[1]);
+
+                for (unsigned i = 2; i < nprems; ++i) {
+                    y = z;
+                    z = arg(conc(prem(proof,i)),1);
+                    res = iproof->make_transitivity(x,y,z,res,args[i]);
+                }
+                break;
+            }
             case PR_QUANT_INTRO:
             case PR_MONOTONICITY:
                 {
@@ -2029,6 +2045,7 @@ public:
                 break;
             }
             default:
+                IF_VERBOSE(0, verbose_stream() << "Unsupported proof rule: " << expr_ref((expr*)proof.raw(), *proof.mgr()) << "\n";);
                 //                pfgoto(proof);                
                 // SASSERT(0 && "translate_main: unsupported proof rule");
                 throw unsupported();

src/interp/iz3translate.h

@@ -36,7 +36,7 @@ class iz3translation : public iz3base {
 
     /** This is thrown when the proof cannot be translated. */
     struct unsupported: public iz3_exception {
-        unsupported(): iz3_exception("unsupported") {}
+    unsupported(): iz3_exception("unsupported") { }
     };
 
     static iz3translation *create(iz3mgr &mgr,