A few more minor updates to match google repository with CVC4 repository

(mostly whitespace differences).

8 files changed, 1177 insertions, 1177 deletions

diff --git a/proofs/lfsc_checker/libwriter.cpp b/proofs/lfsc_checker/libwriter.cpp
index 49e9bbaad..016016c9d 100644
--- a/proofs/lfsc_checker/libwriter.cpp
+++ b/proofs/lfsc_checker/libwriter.cpp
@@ -1,238 +1,238 @@
-#include "libwriter.h"

-#include <sstream>

-#include <algorithm>

-#include <fstream>

-

-void libwriter::get_var_name( const std::string& n, std::string& nn ) {

-  nn = std::string( n.c_str() );

-  for( int i = 0; i <(int)n.length(); i++ ){

-    char c = n[i];

-    if (c <= 47)

-        c += 65;

-    else if (c >= 58 && c <= 64)

-        c += 97-58;

-    if ((c >= 91 && c <= 94) || c == 96)

-        c += 104-91;

-    else if (c >= 123)

-        c -= 4;

-    nn[i] = c;

-  }  

-}

-

-void libwriter::write_file()

-{

-  //std::cout << "write lib" << std::endl;

-  std::ostringstream os_enum;

-  std::ostringstream os_print;

-  std::ostringstream os_constructor_h;

-  std::ostringstream os_constructor_c;

-

-  for ( int a=0; a<(int)syms.size(); a++ ) {

-    //std::cout << "sym #" << (a+1) << ": ";

-    //std::cout << ((SymSExpr*)syms[a])->s.c_str() << std::endl;

-    //defs[a]->print( std::cout );

-    //std::cout << std::endl;

-    

-    if( defs[a]->getclass()==CEXPR ){

-      //calculate which arguments are required for input

-      std::vector< Expr* > args;

-      std::vector< bool > argsNeed;

-      std::vector< Expr* > argTypes;

-      CExpr* c = ((CExpr*)defs[a]);

-      while( c->getop()==PI ){

-        //std::cout << c->kids[0] << std::endl;

-        if( ((CExpr*)c->kids[1])->getop()!=RUN ){

-          args.push_back( c->kids[0] );

-          argsNeed.push_back( true );

-          argTypes.push_back( c->kids[1] );

-        }

-        for( int b=0; b<(int)args.size(); b++ ){

-          if( argsNeed[b] ){

-            if( ((CExpr*)c->kids[1])->getop()==RUN ){

-              if( ((CExpr*)c->kids[1])->kids[1]->free_in( args[b] ) ){

-                argsNeed[b] = false;

-              }

-            }else{

-              if( c->kids[1]->free_in( args[b] ) ){

-                argsNeed[b] = false;

-              }

-            }

-          }

-        }

-        c = (CExpr*)(c->kids[2]);

-      }

-

-      //record if this declares a judgement

-      if( ((CExpr*)defs[a])->getop()==PI && c->getop()==TYPE ){

-        //std::cout << "This is a judgement" << std::endl;

-        judgements.push_back( syms[a] );

-      //record if this declares a proof rule

-      }else if( c->getclass()==CEXPR && std::find( judgements.begin(), judgements.end(), c->kids[0] )!=judgements.end() ){

-        std::cout << "Handle rule: " << ((SymSExpr*)syms[a])->s.c_str() << std::endl;

-        //std::cout << "These are required to input:" << std::endl;

-        //for( int b=0; b<(int)args.size(); b++ ){

-        //  if( argsNeed[b] ){

-        //    std::cout << ((SymSExpr*)args[b])->s.c_str() << std::endl;

-        //  }

-        //}

-        os_enum << "    rule_" << ((SymSExpr*)syms[a])->s.c_str() << "," << std::endl;

-

-        os_print << "  case rule_" << ((SymSExpr*)syms[a])->s.c_str() << ": os << \"";

-        os_print << ((SymSExpr*)syms[a])->s.c_str() << "\";break;" << std::endl;

-

-        std::ostringstream os_args;

-        os_args << "(";

-        bool firstTime = true;

-        for( int b=0; b<(int)args.size(); b++ ){

-          if( argsNeed[b] ){

-            if( !firstTime )

-              os_args << ",";

-            std::string str;

-            get_var_name( ((SymSExpr*)args[b])->s, str );

-            os_args << " LFSCProof* " << str.c_str();

-            firstTime = false;

-          }

-        }

-        if( !firstTime ){

-          os_args << " ";

-        }

-        os_args << ")";

-

-        os_constructor_h << "  static LFSCProof* make_" << ((SymSExpr*)syms[a])->s.c_str();

-        os_constructor_h << os_args.str().c_str() << ";" << std::endl;

-

-        os_constructor_c << "LFSCProof* LFSCProof::make_" << ((SymSExpr*)syms[a])->s.c_str();

-        os_constructor_c << os_args.str().c_str() << "{" << std::endl;

-        os_constructor_c << "  LFSCProof **kids = new LFSCProof *[" << (int)args.size()+1 << "];" << std::endl;

-        for( int b=0; b<(int)args.size(); b++ ){

-          os_constructor_c << "  kids[" << b << "] = ";

-          if( argsNeed[b] ){

-            std::string str;

-            get_var_name( ((SymSExpr*)args[b])->s, str );

-            os_constructor_c << str.c_str();

-          }else{

-            os_constructor_c << "hole";

-          }

-          os_constructor_c << ";" << std::endl;

-        }

-        os_constructor_c << "  kids[" << (int)args.size() << "] = 0;" << std::endl;

-        os_constructor_c << "  return new LFSCProofC( rule_" << ((SymSExpr*)syms[a])->s.c_str() << ", kids );" << std::endl;

-        os_constructor_c << "}" << std::endl << std::endl;

-      }

-    }

-

-    //write the header

-    static std::string filename( "lfsc_proof" );

-    std::fstream fsh;

-    std::string fnameh( filename );

-    fnameh.append(".h");

-    fsh.open( fnameh.c_str(), std::ios::out );

-

-    fsh << "#ifndef LFSC_PROOF_LIB_H" << std::endl;

-    fsh << "#define LFSC_PROOF_LIB_H" << std::endl;

-    fsh << std::endl;

-    fsh << "#include <string>" << std::endl;

-    fsh << std::endl;

-    fsh << "class LFSCProof{" << std::endl;

-    fsh << "protected:" << std::endl;

-    fsh << "  enum{" << std::endl;

-    fsh << os_enum.str().c_str();

-    fsh << "  };" << std::endl;

-    fsh << "  static LFSCProof* hole;" << std::endl;

-    fsh << "  LFSCProof(){}" << std::endl;

-    fsh << "public:" << std::endl;

-    fsh << "  virtual ~LFSCProof(){}" << std::endl;

-    fsh << "  static void init();" << std::endl;

-    fsh << std::endl;

-    fsh << "  //functions to build LFSC proofs" << std::endl;

-    fsh << os_constructor_h.str().c_str();

-    fsh << std::endl;

-    fsh << "  virtual void set_child( int i, LFSCProof* e ) {}" << std::endl;

-    fsh << "  virtual void print( std::ostream& os ){}" << std::endl;

-    fsh << "};" << std::endl;

-    fsh << std::endl;

-    fsh << "class LFSCProofC : public LFSCProof{" << std::endl;

-    fsh << "  short id;" << std::endl;

-    fsh << "  LFSCProof **kids;" << std::endl;

-    fsh << "public:" << std::endl;

-    fsh << "  LFSCProofC( short d_id, LFSCProof **d_kids ) : id( d_id ), kids( d_kids ){}" << std::endl;

-    fsh << "  void set_child( int i, LFSCProof* e ) { kids[i] = e; }" << std::endl;

-    fsh << "  void print( std::ostream& os );" << std::endl;

-    fsh << "};" << std::endl;

-    fsh << std::endl;

-    fsh << "class LFSCProofSym : public LFSCProof{" << std::endl;

-    fsh << "private:" << std::endl;

-    fsh << "  std::string s;" << std::endl;

-    fsh << "  LFSCProofSym( std::string ss ) : s( ss ){}" << std::endl;

-    fsh << "public:" << std::endl;

-    fsh << "  static LFSCProofSym* make( std::string ss ) { return new LFSCProofSym( ss ); }" << std::endl;

-    fsh << "  static LFSCProofSym* make( const char* ss ) { return new LFSCProofSym( std::string( ss ) ); }" << std::endl;

-    fsh << "  ~LFSCProofSym(){}" << std::endl;

-    fsh << "  void print( std::ostream& os ) { os << s.c_str(); }" << std::endl;

-    fsh << "};" << std::endl;

-    fsh << std::endl;

-    fsh << "class LFSCProofLam : public LFSCProof{" << std::endl;

-    fsh << "  LFSCProofSym* var;" << std::endl;

-    fsh << "  LFSCProof* body;" << std::endl;

-    fsh << "  LFSCProof* typ;" << std::endl;

-    fsh << "  LFSCProofLam( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ ) : var( d_var ), body( d_body ), typ( d_typ ){}" << std::endl;

-    fsh << "public:" << std::endl;

-    fsh << "  static LFSCProof* make( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ = NULL ) {" << std::endl;

-    fsh << "    return new LFSCProofLam( d_var, d_body, d_typ );" << std::endl;

-    fsh << "  }" << std::endl;

-    fsh << "  ~LFSCProofLam(){}" << std::endl;

-    fsh << std::endl;

-    fsh << "  void print( std::ostream& os );" << std::endl;

-    fsh << "};" << std::endl;

-    fsh << std::endl;

-    fsh << "#endif" << std::endl;

-

-    //write the cpp

-    std::fstream fsc;

-    std::string fnamec( filename );

-    fnamec.append(".cpp");

-    fsc.open( fnamec.c_str(), std::ios::out );

-

-    fsc << "#include \"lfsc_proof.h\"" << std::endl;

-    fsc << std::endl;

-    fsc << "LFSCProof* LFSCProof::hole = NULL;" << std::endl;

-    fsc << std::endl;

-    fsc << "void LFSCProof::init(){" << std::endl;

-    fsc << "  hole = LFSCProofSym::make( \"_\" );" << std::endl;

-    fsc << "}" << std::endl;

-    fsc << std::endl;

-    fsc << "void LFSCProofC::print( std::ostream& os ){" << std::endl;

-    fsc << "  os << \"(\";" << std::endl;

-    fsc << "  switch( id ){" << std::endl;

-    fsc << os_print.str().c_str();

-    fsc << "  }" << std::endl;

-    fsc << "  int counter = 0;" << std::endl;

-    fsc << "  while( kids[counter] ){" << std::endl;

-    fsc << "    os << \" \";" << std::endl;

-    fsc << "    kids[counter]->print( os );" << std::endl;

-    fsc << "    counter++;" << std::endl;

-    fsc << "  }" << std::endl;

-    fsc << "  os << \")\";" << std::endl;

-    fsc << "}" << std::endl;

-    fsc << std::endl;

-    fsc << "void LFSCProofLam::print( std::ostream& os ){" << std::endl;

-    fsc << "  os << \"(\";" << std::endl;

-    fsc << "  if( typ ){" << std::endl;

-    fsc << "    os << \"% \";" << std::endl;

-    fsc << "  }else{" << std::endl;

-    fsc << "    os << \"\\\\ \";" << std::endl;

-    fsc << "  }" << std::endl;

-    fsc << "  var->print( os );" << std::endl;

-    fsc << "  if( typ ){" << std::endl;

-    fsc << "    os << \" \";" << std::endl;

-    fsc << "    typ->print( os );" << std::endl;

-    fsc << "  }" << std::endl;

-    fsc << "  os << std::endl;" << std::endl;

-    fsc << "  body->print( os );" << std::endl;

-    fsc << "  os << \")\";" << std::endl;

-    fsc << "}" << std::endl;

-    fsc << std::endl;

-    fsc << os_constructor_c.str().c_str();

-    fsc << std::endl;

-  }

-}

+#include "libwriter.h"
+#include <sstream>
+#include <algorithm>
+#include <fstream>
+
+void libwriter::get_var_name( const std::string& n, std::string& nn ) {
+  nn = std::string( n.c_str() );
+  for( int i = 0; i <(int)n.length(); i++ ){
+    char c = n[i];
+    if (c <= 47)
+        c += 65;
+    else if (c >= 58 && c <= 64)
+        c += 97-58;
+    if ((c >= 91 && c <= 94) || c == 96)
+        c += 104-91;
+    else if (c >= 123)
+        c -= 4;
+    nn[i] = c;
+  }  
+}
+
+void libwriter::write_file()
+{
+  //std::cout << "write lib" << std::endl;
+  std::ostringstream os_enum;
+  std::ostringstream os_print;
+  std::ostringstream os_constructor_h;
+  std::ostringstream os_constructor_c;
+
+  for ( int a=0; a<(int)syms.size(); a++ ) {
+    //std::cout << "sym #" << (a+1) << ": ";
+    //std::cout << ((SymSExpr*)syms[a])->s.c_str() << std::endl;
+    //defs[a]->print( std::cout );
+    //std::cout << std::endl;
+    
+    if( defs[a]->getclass()==CEXPR ){
+      //calculate which arguments are required for input
+      std::vector< Expr* > args;
+      std::vector< bool > argsNeed;
+      std::vector< Expr* > argTypes;
+      CExpr* c = ((CExpr*)defs[a]);
+      while( c->getop()==PI ){
+        //std::cout << c->kids[0] << std::endl;
+        if( ((CExpr*)c->kids[1])->getop()!=RUN ){
+          args.push_back( c->kids[0] );
+          argsNeed.push_back( true );
+          argTypes.push_back( c->kids[1] );
+        }
+        for( int b=0; b<(int)args.size(); b++ ){
+          if( argsNeed[b] ){
+            if( ((CExpr*)c->kids[1])->getop()==RUN ){
+              if( ((CExpr*)c->kids[1])->kids[1]->free_in( args[b] ) ){
+                argsNeed[b] = false;
+              }
+            }else{
+              if( c->kids[1]->free_in( args[b] ) ){
+                argsNeed[b] = false;
+              }
+            }
+          }
+        }
+        c = (CExpr*)(c->kids[2]);
+      }
+
+      //record if this declares a judgement
+      if( ((CExpr*)defs[a])->getop()==PI && c->getop()==TYPE ){
+        //std::cout << "This is a judgement" << std::endl;
+        judgements.push_back( syms[a] );
+      //record if this declares a proof rule
+      }else if( c->getclass()==CEXPR && std::find( judgements.begin(), judgements.end(), c->kids[0] )!=judgements.end() ){
+        std::cout << "Handle rule: " << ((SymSExpr*)syms[a])->s.c_str() << std::endl;
+        //std::cout << "These are required to input:" << std::endl;
+        //for( int b=0; b<(int)args.size(); b++ ){
+        //  if( argsNeed[b] ){
+        //    std::cout << ((SymSExpr*)args[b])->s.c_str() << std::endl;
+        //  }
+        //}
+        os_enum << "    rule_" << ((SymSExpr*)syms[a])->s.c_str() << "," << std::endl;
+
+        os_print << "  case rule_" << ((SymSExpr*)syms[a])->s.c_str() << ": os << \"";
+        os_print << ((SymSExpr*)syms[a])->s.c_str() << "\";break;" << std::endl;
+
+        std::ostringstream os_args;
+        os_args << "(";
+        bool firstTime = true;
+        for( int b=0; b<(int)args.size(); b++ ){
+          if( argsNeed[b] ){
+            if( !firstTime )
+              os_args << ",";
+            std::string str;
+            get_var_name( ((SymSExpr*)args[b])->s, str );
+            os_args << " LFSCProof* " << str.c_str();
+            firstTime = false;
+          }
+        }
+        if( !firstTime ){
+          os_args << " ";
+        }
+        os_args << ")";
+
+        os_constructor_h << "  static LFSCProof* make_" << ((SymSExpr*)syms[a])->s.c_str();
+        os_constructor_h << os_args.str().c_str() << ";" << std::endl;
+
+        os_constructor_c << "LFSCProof* LFSCProof::make_" << ((SymSExpr*)syms[a])->s.c_str();
+        os_constructor_c << os_args.str().c_str() << "{" << std::endl;
+        os_constructor_c << "  LFSCProof **kids = new LFSCProof *[" << (int)args.size()+1 << "];" << std::endl;
+        for( int b=0; b<(int)args.size(); b++ ){
+          os_constructor_c << "  kids[" << b << "] = ";
+          if( argsNeed[b] ){
+            std::string str;
+            get_var_name( ((SymSExpr*)args[b])->s, str );
+            os_constructor_c << str.c_str();
+          }else{
+            os_constructor_c << "hole";
+          }
+          os_constructor_c << ";" << std::endl;
+        }
+        os_constructor_c << "  kids[" << (int)args.size() << "] = 0;" << std::endl;
+        os_constructor_c << "  return new LFSCProofC( rule_" << ((SymSExpr*)syms[a])->s.c_str() << ", kids );" << std::endl;
+        os_constructor_c << "}" << std::endl << std::endl;
+      }
+    }
+
+    //write the header
+    static std::string filename( "lfsc_proof" );
+    std::fstream fsh;
+    std::string fnameh( filename );
+    fnameh.append(".h");
+    fsh.open( fnameh.c_str(), std::ios::out );
+
+    fsh << "#ifndef LFSC_PROOF_LIB_H" << std::endl;
+    fsh << "#define LFSC_PROOF_LIB_H" << std::endl;
+    fsh << std::endl;
+    fsh << "#include <string>" << std::endl;
+    fsh << std::endl;
+    fsh << "class LFSCProof{" << std::endl;
+    fsh << "protected:" << std::endl;
+    fsh << "  enum{" << std::endl;
+    fsh << os_enum.str().c_str();
+    fsh << "  };" << std::endl;
+    fsh << "  static LFSCProof* hole;" << std::endl;
+    fsh << "  LFSCProof(){}" << std::endl;
+    fsh << "public:" << std::endl;
+    fsh << "  virtual ~LFSCProof(){}" << std::endl;
+    fsh << "  static void init();" << std::endl;
+    fsh << std::endl;
+    fsh << "  //functions to build LFSC proofs" << std::endl;
+    fsh << os_constructor_h.str().c_str();
+    fsh << std::endl;
+    fsh << "  virtual void set_child( int i, LFSCProof* e ) {}" << std::endl;
+    fsh << "  virtual void print( std::ostream& os ){}" << std::endl;
+    fsh << "};" << std::endl;
+    fsh << std::endl;
+    fsh << "class LFSCProofC : public LFSCProof{" << std::endl;
+    fsh << "  short id;" << std::endl;
+    fsh << "  LFSCProof **kids;" << std::endl;
+    fsh << "public:" << std::endl;
+    fsh << "  LFSCProofC( short d_id, LFSCProof **d_kids ) : id( d_id ), kids( d_kids ){}" << std::endl;
+    fsh << "  void set_child( int i, LFSCProof* e ) { kids[i] = e; }" << std::endl;
+    fsh << "  void print( std::ostream& os );" << std::endl;
+    fsh << "};" << std::endl;
+    fsh << std::endl;
+    fsh << "class LFSCProofSym : public LFSCProof{" << std::endl;
+    fsh << "private:" << std::endl;
+    fsh << "  std::string s;" << std::endl;
+    fsh << "  LFSCProofSym( std::string ss ) : s( ss ){}" << std::endl;
+    fsh << "public:" << std::endl;
+    fsh << "  static LFSCProofSym* make( std::string ss ) { return new LFSCProofSym( ss ); }" << std::endl;
+    fsh << "  static LFSCProofSym* make( const char* ss ) { return new LFSCProofSym( std::string( ss ) ); }" << std::endl;
+    fsh << "  ~LFSCProofSym(){}" << std::endl;
+    fsh << "  void print( std::ostream& os ) { os << s.c_str(); }" << std::endl;
+    fsh << "};" << std::endl;
+    fsh << std::endl;
+    fsh << "class LFSCProofLam : public LFSCProof{" << std::endl;
+    fsh << "  LFSCProofSym* var;" << std::endl;
+    fsh << "  LFSCProof* body;" << std::endl;
+    fsh << "  LFSCProof* typ;" << std::endl;
+    fsh << "  LFSCProofLam( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ ) : var( d_var ), body( d_body ), typ( d_typ ){}" << std::endl;
+    fsh << "public:" << std::endl;
+    fsh << "  static LFSCProof* make( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ = NULL ) {" << std::endl;
+    fsh << "    return new LFSCProofLam( d_var, d_body, d_typ );" << std::endl;
+    fsh << "  }" << std::endl;
+    fsh << "  ~LFSCProofLam(){}" << std::endl;
+    fsh << std::endl;
+    fsh << "  void print( std::ostream& os );" << std::endl;
+    fsh << "};" << std::endl;
+    fsh << std::endl;
+    fsh << "#endif" << std::endl;
+
+    //write the cpp
+    std::fstream fsc;
+    std::string fnamec( filename );
+    fnamec.append(".cpp");
+    fsc.open( fnamec.c_str(), std::ios::out );
+
+    fsc << "#include \"lfsc_proof.h\"" << std::endl;
+    fsc << std::endl;
+    fsc << "LFSCProof* LFSCProof::hole = NULL;" << std::endl;
+    fsc << std::endl;
+    fsc << "void LFSCProof::init(){" << std::endl;
+    fsc << "  hole = LFSCProofSym::make( \"_\" );" << std::endl;
+    fsc << "}" << std::endl;
+    fsc << std::endl;
+    fsc << "void LFSCProofC::print( std::ostream& os ){" << std::endl;
+    fsc << "  os << \"(\";" << std::endl;
+    fsc << "  switch( id ){" << std::endl;
+    fsc << os_print.str().c_str();
+    fsc << "  }" << std::endl;
+    fsc << "  int counter = 0;" << std::endl;
+    fsc << "  while( kids[counter] ){" << std::endl;
+    fsc << "    os << \" \";" << std::endl;
+    fsc << "    kids[counter]->print( os );" << std::endl;
+    fsc << "    counter++;" << std::endl;
+    fsc << "  }" << std::endl;
+    fsc << "  os << \")\";" << std::endl;
+    fsc << "}" << std::endl;
+    fsc << std::endl;
+    fsc << "void LFSCProofLam::print( std::ostream& os ){" << std::endl;
+    fsc << "  os << \"(\";" << std::endl;
+    fsc << "  if( typ ){" << std::endl;
+    fsc << "    os << \"% \";" << std::endl;
+    fsc << "  }else{" << std::endl;
+    fsc << "    os << \"\\\\ \";" << std::endl;
+    fsc << "  }" << std::endl;
+    fsc << "  var->print( os );" << std::endl;
+    fsc << "  if( typ ){" << std::endl;
+    fsc << "    os << \" \";" << std::endl;
+    fsc << "    typ->print( os );" << std::endl;
+    fsc << "  }" << std::endl;
+    fsc << "  os << std::endl;" << std::endl;
+    fsc << "  body->print( os );" << std::endl;
+    fsc << "  os << \")\";" << std::endl;
+    fsc << "}" << std::endl;
+    fsc << std::endl;
+    fsc << os_constructor_c.str().c_str();
+    fsc << std::endl;
+  }
+}
diff --git a/proofs/lfsc_checker/libwriter.h b/proofs/lfsc_checker/libwriter.h
index 093cf541b..91db5e911 100644
--- a/proofs/lfsc_checker/libwriter.h
+++ b/proofs/lfsc_checker/libwriter.h
@@ -1,28 +1,28 @@
-#ifndef LIB_WRITER_H

-#define LIB_WRITER_H

-

-#include "expr.h"

-#include <map>

-

-class libwriter

-{

-private:

-  std::vector< Expr* > syms;

-  std::vector< Expr* > defs;

-

-  std::vector< Expr* > judgements;

-  //get the variable name

-  void get_var_name( const std::string& n, std::string& nn );

-public:

-  libwriter(){}

-  virtual ~libwriter(){}

-

-  void add_symbol( Expr* s, Expr* t ) { 

-    syms.push_back( s );

-    defs.push_back( t ); 

-  }

-

-  void write_file();

-};

-

-#endif

+#ifndef LIB_WRITER_H
+#define LIB_WRITER_H
+
+#include "expr.h"
+#include <map>
+
+class libwriter
+{
+private:
+  std::vector< Expr* > syms;
+  std::vector< Expr* > defs;
+
+  std::vector< Expr* > judgements;
+  //get the variable name
+  void get_var_name( const std::string& n, std::string& nn );
+public:
+  libwriter(){}
+  virtual ~libwriter(){}
+
+  void add_symbol( Expr* s, Expr* t ) { 
+    syms.push_back( s );
+    defs.push_back( t ); 
+  }
+
+  void write_file();
+};
+
+#endif
diff --git a/proofs/lfsc_checker/print_smt2.cpp b/proofs/lfsc_checker/print_smt2.cpp
index 34cb00cc4..40d9d1206 100644
--- a/proofs/lfsc_checker/print_smt2.cpp
+++ b/proofs/lfsc_checker/print_smt2.cpp
@@ -1,122 +1,122 @@
-#include "print_smt2.h"

-

-#ifdef PRINT_SMT2

-

-void print_smt2( Expr* p, std::ostream& s, short mode )

-{

-  switch( p->getclass() )

-  {

-  case CEXPR:

-    {

-      switch( p->getop() )

-      {

-      case APP:

-        {

+#include "print_smt2.h"
+
+#ifdef PRINT_SMT2
+
+void print_smt2( Expr* p, std::ostream& s, short mode )
+{
+  switch( p->getclass() )
+  {
+  case CEXPR:
+    {
+      switch( p->getop() )
+      {
+      case APP:
+        {
           std::vector<Expr *> args;
-          Expr *head = p->collect_args(args, false);

-          short newMode = get_mode( head );

-          if( is_smt2_poly_formula( head ) )

-          {

-            s << "(";

-            head->print( s );

-            s << " ";

-            print_smt2( args[1], s, newMode );

-            s << " ";

-            print_smt2( args[2], s, newMode );

-            s << ")";

-          }

-          else if( ( mode==2 || mode==3 ) && mode==newMode )

-          {

-            print_smt2( args[0], s, newMode );

-            s << " ";

-            print_smt2( args[1], s, newMode );

-          }

-          else if( newMode==1 )

-          {

-            if( mode!=1 || newMode!=mode ){

-              s << "(";

-            }

-            print_smt2( args[2], s, newMode );

-            s << " ";

-            print_smt2( args[3], s, 0 );

-            if( mode!=1 || newMode!=mode ){

-              s << ")";

-            }

-          }

-          else

-          {

-            s << "(";

-            switch( newMode )

-            {

-            case 4: s << "=>";break;

-            default: head->print( s );break;

-            }

-            s << " ";

-            for( int a=0; a<(int)args.size(); a++ ){

-              print_smt2( args[a], s, newMode );

-              if( a!=(int)args.size()-1 )

-                s << " ";

-            }

-            s << ")";

-          }

-        }

-        break;

-      default:

-        std::cout << "Unhandled op " << p->getop() << std::endl;

-        break;

-      }

-    }

-    break;

-  case HOLE_EXPR:

-    {

-      HoleExpr *e = (HoleExpr *)p;

-      if( e->val ){

-        print_smt2( e->val, s, mode );

-      }else{

-        s << "_";

-      }

-    }

-    break;

-  case SYMS_EXPR:

-  case SYM_EXPR:

-    if( ((SymExpr*)p)->val )

-      print_smt2( ((SymExpr*)p)->val, s, mode );

-    else

-      p->print( s );

-    break;

-  default:

-    std::cout << "Unhandled class " << p->getclass() << std::endl;

-    break;

-  }

-}

-

-bool is_smt2_poly_formula( Expr* e )

-{

-  if( e->getclass()==SYMS_EXPR )

-  {

-    SymSExpr* s = (SymSExpr*)e;

-    static std::string eq("=");

-    static std::string distinct("distinct");

-    return s->s==eq || s->s==distinct;

-  }else{

-    return false;

-  }

-}

-

-short get_mode( Expr* e )

-{

-  if( e->getclass()==SYMS_EXPR ){

-    SymSExpr* s = (SymSExpr*)e;

-    static std::string applys("apply");

-    if ( s->s==applys ) return 1;

-    static std::string ands("and");

-    if ( s->s==ands ) return 2;

-    static std::string ors("or");

-    if ( s->s==ors ) return 3;

-    static std::string impls("impl");

-    if ( s->s==impls ) return 4;

-  }

-  return 0;

-}

-

-#endif

+          Expr *head = p->collect_args(args, false);
+          short newMode = get_mode( head );
+          if( is_smt2_poly_formula( head ) )
+          {
+            s << "(";
+            head->print( s );
+            s << " ";
+            print_smt2( args[1], s, newMode );
+            s << " ";
+            print_smt2( args[2], s, newMode );
+            s << ")";
+          }
+          else if( ( mode==2 || mode==3 ) && mode==newMode )
+          {
+            print_smt2( args[0], s, newMode );
+            s << " ";
+            print_smt2( args[1], s, newMode );
+          }
+          else if( newMode==1 )
+          {
+            if( mode!=1 || newMode!=mode ){
+              s << "(";
+            }
+            print_smt2( args[2], s, newMode );
+            s << " ";
+            print_smt2( args[3], s, 0 );
+            if( mode!=1 || newMode!=mode ){
+              s << ")";
+            }
+          }
+          else
+          {
+            s << "(";
+            switch( newMode )
+            {
+            case 4: s << "=>";break;
+            default: head->print( s );break;
+            }
+            s << " ";
+            for( int a=0; a<(int)args.size(); a++ ){
+              print_smt2( args[a], s, newMode );
+              if( a!=(int)args.size()-1 )
+                s << " ";
+            }
+            s << ")";
+          }
+        }
+        break;
+      default:
+        std::cout << "Unhandled op " << p->getop() << std::endl;
+        break;
+      }
+    }
+    break;
+  case HOLE_EXPR:
+    {
+      HoleExpr *e = (HoleExpr *)p;
+      if( e->val ){
+        print_smt2( e->val, s, mode );
+      }else{
+        s << "_";
+      }
+    }
+    break;
+  case SYMS_EXPR:
+  case SYM_EXPR:
+    if( ((SymExpr*)p)->val )
+      print_smt2( ((SymExpr*)p)->val, s, mode );
+    else
+      p->print( s );
+    break;
+  default:
+    std::cout << "Unhandled class " << p->getclass() << std::endl;
+    break;
+  }
+}
+
+bool is_smt2_poly_formula( Expr* e )
+{
+  if( e->getclass()==SYMS_EXPR )
+  {
+    SymSExpr* s = (SymSExpr*)e;
+    static std::string eq("=");
+    static std::string distinct("distinct");
+    return s->s==eq || s->s==distinct;
+  }else{
+    return false;
+  }
+}
+
+short get_mode( Expr* e )
+{
+  if( e->getclass()==SYMS_EXPR ){
+    SymSExpr* s = (SymSExpr*)e;
+    static std::string applys("apply");
+    if ( s->s==applys ) return 1;
+    static std::string ands("and");
+    if ( s->s==ands ) return 2;
+    static std::string ors("or");
+    if ( s->s==ors ) return 3;
+    static std::string impls("impl");
+    if ( s->s==impls ) return 4;
+  }
+  return 0;
+}
+
+#endif
diff --git a/proofs/lfsc_checker/print_smt2.h b/proofs/lfsc_checker/print_smt2.h
index c70b1dfa4..9bee0e81c 100644
--- a/proofs/lfsc_checker/print_smt2.h
+++ b/proofs/lfsc_checker/print_smt2.h
@@ -1,17 +1,17 @@
-#ifndef PRINT_SMT2_H

-#define PRINT_SMT2_H

-

-#define PRINT_SMT2

-

-#include "expr.h"

-

-#ifdef PRINT_SMT2

-void print_smt2( Expr* p, std::ostream& s, short mode = 0 );

-

-bool is_smt2_poly_formula( Expr* p );

-short get_mode( Expr* p );

-

-#endif

-

-

-#endif

+#ifndef PRINT_SMT2_H
+#define PRINT_SMT2_H
+
+#define PRINT_SMT2
+
+#include "expr.h"
+
+#ifdef PRINT_SMT2
+void print_smt2( Expr* p, std::ostream& s, short mode = 0 );
+
+bool is_smt2_poly_formula( Expr* p );
+short get_mode( Expr* p );
+
+#endif
+
+
+#endif
diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp
index d11a96b19..5c1da2a3f 100644
--- a/proofs/lfsc_checker/sccwriter.cpp
+++ b/proofs/lfsc_checker/sccwriter.cpp
@@ -1,335 +1,335 @@
-#include "sccwriter.h"

-

-#include <fstream>

-#include <sstream>

-

-int sccwriter::exprCount = 0;

-int sccwriter::strCount = 0;

-int sccwriter::argsCount = 0;

-int sccwriter::rnumCount = 0;

-

-int sccwriter::get_prog_index( const std::string& str )

-{

-  for( int a=0; a<(int)progNames.size(); a++ ){

-    if( progNames[a]==str ){

-      return a;

-    }

-  }

-  return -1;

-}

-

-int sccwriter::get_prog_index_by_expr( Expr* e )

-{

-  for( int a=0; a<(int)progPtrs.size(); a++ ){

-    if( progPtrs[a]==e ){

-      return a;

-    }

-  }

-  return -1;

-}

-

-bool sccwriter::is_var( const std::string& str )

-{

-  for( int a=0; a<(int)vars.size(); a++ ){

-    if( vars[a]==str ){

-      return true;

-    }

-  }

-  return false;

-}

-

-void sccwriter::add_global_sym( const std::string& str )

-{

-  for( int a=0; a<(int)globalSyms.size(); a++ ){

-    if( globalSyms[a]==str ){

-      return;

-    }

-  }

-  globalSyms.push_back( str );

-}

-

-void sccwriter::indent( std::ostream& os, int ind )

-{

-   for( int a=0; a<ind; a++ )

-   {

-      os << "   ";

-   }

-}

-

-void sccwriter::write_function_header( std::ostream& os, int index, int opts )

-{

-  //write the function header

-  std::string fname;

-  get_function_name( progNames[index], fname );

-  os << "Expr* " << fname.c_str() << "( ";

-  CExpr* progvars = (CExpr*)get_prog( index )->kids[1];

-  int counter = 0;

-  //write each argument

-  while( progvars->kids[counter] )

-  {

-    if( counter!=0 )

-    {

-      os << ", ";

-    }

-    os << "Expr* ";

-    write_variable( ((SymSExpr*)progvars->kids[counter])->s, os );

-    //add to vars if options are set to do so

-    if( opts&opt_write_add_args )

-    {

-      vars.push_back( ((SymSExpr*)progvars->kids[counter])->s );

-    }

-    counter++;

-  }

-  os << " )";

-  if( opts&opt_write_call_debug )

-  {

-     os << "{" << std::endl;

-     indent( os, 1 );

-     os << "std::cout << \"Call function " << fname.c_str() << " with arguments \";" << std::endl;

-     counter = 0; 

-     while( progvars->kids[counter] )

-     {

-        if( counter!=0 )

-        {

-           indent( os, 1 );

-           os << "std::cout << \", \";" << std::endl;

-        }

-        indent( os, 1 );

-        write_variable( ((SymSExpr*)progvars->kids[counter])->s, os );

-        os << "->print( std::cout );" << std::endl;

-        counter++;

-     }

-     indent( os, 1 );

-     os << "std::cout << std::endl;" << std::endl;

-  }

-}

-

-void sccwriter::get_function_name( const std::string& pname, std::string& fname )

-{

-  fname = std::string( "f_" );

-  fname.append( pname );

-}

-

-void sccwriter::write_variable( const std::string& n, std::ostream& os )

-{

-  std::string nn;

-  get_var_name( n, nn );

-  os << nn.c_str();

-}

-

-void sccwriter::get_var_name( const std::string& n, std::string& nn ) {

-  nn = std::string( n.c_str() );

-  for( int i = 0; i <(int)n.length(); i++ ){

-    char c = n[i];

-    if (c <= 47)

-        c += 65;

-    else if (c >= 58 && c <= 64)

-        c += 97-58;

-    if ((c >= 91 && c <= 94) || c == 96)

-        c += 104-91;

-    else if (c >= 123)

-        c -= 4;

-    nn[i] = c;

-  }  

-}

-

-void sccwriter::write_file()

-{

-  static std::string filename( "scccode" );

-

-  //writer the h file

-  std::fstream fsh;

-  std::string fnameh( filename );

-  fnameh.append(".h");

-  fsh.open( fnameh.c_str(), std::ios::out );

-  //write the header in h

-  fsh << "#ifndef SCC_CODE_H" << std::endl;

-  fsh << "#define SCC_CODE_H" << std::endl << std::endl;

-  //include necessary files in h file

-  fsh << "#include \"check.h\"" << std::endl << std::endl;

-  //write the init function

-  fsh << "void init_compiled_scc();" << std::endl << std::endl;

-  //write the entry function

-  fsh << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );" << std::endl << std::endl;

-  //write the side condition code functions

-  for( int n=0; n<(int)progs.size(); n++ )

-  {

-    //write the header in the h file

-    fsh << "inline ";

-    write_function_header( fsh, n );

-    fsh << ";" << std::endl << std::endl;

-  }

-  fsh << "#endif" << std::endl << std::endl;

-  fsh.close();

-

-

-  //writer the cpp code

-  std::fstream fsc;

-  std::string fnamec( filename );

-  fnamec.append(".cpp");

-  fsc.open( fnamec.c_str(), std::ios::out );

-  //include the h file in the cpp

-  fsc << "#include \"scccode.h\"" << std::endl << std::endl;

-  std::ostringstream fsc_funcs;

-  //write the side condition code functions

-  for( currProgram=0; currProgram<(int)progs.size(); currProgram++ )

-  {

-    //reset naming counters

-    vars.clear();

-    exprCount = 0;

-    strCount = 0;

-    argsCount = 0;

-    rnumCount = 0;

-

-    //for debugging

-    std::cout << "program #" << currProgram << " " << progNames[currProgram].c_str() << std::endl;

-

-    //write the function header

-    write_function_header( fsc_funcs, currProgram, opt_write_add_args|options );

-    if( (options&opt_write_call_debug)==0 )

-    {

-       fsc_funcs << "{" << std::endl;

-    }

-    //write the code

-    //std::vector< std::string > cleanVec;

-    //write_code( get_prog( n )->kids[2], fsc, 1, "return ", cleanVec );

-    //debug_write_code( progs[n].second->kids[2], fsc, 1 );

-    std::string expr;

-    write_expr( get_prog( currProgram )->kids[2], fsc_funcs, 1, expr );

-    indent( fsc_funcs, 1 );

-    fsc_funcs << "return " << expr.c_str() << ";" << std::endl;

-    fsc_funcs << "}" << std::endl << std::endl;

-  }

-  //write the predefined symbols necessary - symbols and progs

-  for( int a=0; a<(int)globalSyms.size(); a++ )

-  {

-    fsc << "Expr* e_" << globalSyms[a].c_str() << ";" << std::endl;

-  }

-  for( int a=0; a<(int)progs.size(); a++ )

-  {

-    fsc << "Expr* e_" << progNames[a].c_str() << ";" << std::endl;

-  }

-  fsc << std::endl;

-  //write the init function - initialize symbols and progs

-  fsc << "void init_compiled_scc(){" << std::endl;

-  for( int a=0; a<(int)globalSyms.size(); a++ )

-  {

-    indent( fsc, 1 );

-    fsc << "e_" << globalSyms[a].c_str() << " = symbols->get(\"" << globalSyms[a].c_str() << "\").first;" << std::endl;

-  }

-  for( int a=0; a<(int)progs.size(); a++ )

-  {

-    indent( fsc, 1 );

-    fsc << "e_" << progNames[a].c_str() << " = progs[\"" << progNames[a].c_str() << "\"];" << std::endl;

-  }

-  fsc << "}" << std::endl << std::endl;

-  fsc << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){" << std::endl;

-  //for( int n=0; n<(int)progs.size(); n++ ){

-  //  indent( fsc, 1 );

-  //  fsc << "static std::string s_" << progNames[n].c_str() << " = std::string( \"" << progNames[n].c_str() << "\" );" << std::endl;

-  //}

-  for( int n=0; n<(int)progs.size(); n++ ){

-    indent( fsc, 1 );

-    if( n!=0 ){

-      fsc << "}else ";

-    }

-    //for each function, test to see if the string matches the name of the function

-    fsc << "if( p==e_" << progNames[n].c_str() << " ){" << std::endl;

-    indent( fsc, 2 );

-    std::string fname;

-    get_function_name( progNames[n], fname );

-    //map the function to the proper function

-    fsc << "return " << fname.c_str() << "( ";

-    //write the arguments to the function from args

-    CExpr* progvars = (CExpr*)get_prog( n )->kids[1];

-    int counter = 0;

-    bool firstTime = true;

-    while( progvars->kids[counter] )

-    {

-      if( !firstTime )

-      {

-        fsc << ", ";

-      }

-      fsc << "args[" << counter << "]";

-      firstTime = false;

-      counter++;

-    }

-    fsc << " );" << std::endl;

-  }

-  indent( fsc, 1 );

-  fsc << "}else{" << std::endl;

-  indent( fsc, 2 );

-  //return null in the case the function could not be found

-  fsc << "return NULL;" << std::endl;

-  indent( fsc, 1 );

-  fsc << "}" << std::endl;

-  fsc << "}" << std::endl << std::endl;

-  fsc << fsc_funcs.str().c_str();

-

-  fsc.close();

-}

-

-void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts )

-{

-  std::string retModString;

-  std::string incString;

-  if ( retModStr )

-  {

-    retModString = std::string( retModStr );

-    retModString.append( " = " );

-    incString = std::string( retModStr );

-    incString.append( "->inc();" );

-  }

-  switch( code->getclass() )

-  {

-  case INT_EXPR:

-    {

-      indent( os, ind );

-      os << retModString.c_str();

-      os << "new IntExpr( " << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl;

-      indent( os, ind );

-      os << incString.c_str() << std::endl;

-    }

-    break;

-  case RAT_EXPR:

-    {

-      mpz_t num, den;

-      mpz_init(num);

-      mpz_init(den);

-      mpq_get_num( num, ((RatExpr*)code)->n );

-      mpq_get_den( den, ((RatExpr*)code)->n );

-      indent( os, ind );

-      os << retModString.c_str();

-      os << "new RatExpr( " << mpz_get_si( num ) << ", " << mpz_get_si( den ) << " );" << std::endl;

-      indent( os, ind );

-      os << incString.c_str() << std::endl;

-    }

-    break;

-  case SYMS_EXPR:

-    {

-      //if it is a variable, simply write it to buffer

-      if( is_var( ((SymSExpr*)code)->s ) )

-      {

-        indent( os, ind );

-        os << retModString.c_str();

-        write_variable( ((SymSExpr*)code)->s.c_str(), os );

-        os << ";" << std::endl;  

-      }

-      else  //else must look at symbol lookup table

-      {

-        std::string var;

-        get_var_name( ((SymSExpr*)code)->s, var );

-        indent( os, ind );

-        os << retModString.c_str() << "e_" << var.c_str() << ";" << std::endl;

-        add_global_sym( var ); 

-      }

-      indent( os, ind );

-      os << incString.c_str() << std::endl;

-    }

-    break;

-  default:

-    switch( code->getop() )

-    {

+#include "sccwriter.h"
+
+#include <fstream>
+#include <sstream>
+
+int sccwriter::exprCount = 0;
+int sccwriter::strCount = 0;
+int sccwriter::argsCount = 0;
+int sccwriter::rnumCount = 0;
+
+int sccwriter::get_prog_index( const std::string& str )
+{
+  for( int a=0; a<(int)progNames.size(); a++ ){
+    if( progNames[a]==str ){
+      return a;
+    }
+  }
+  return -1;
+}
+
+int sccwriter::get_prog_index_by_expr( Expr* e )
+{
+  for( int a=0; a<(int)progPtrs.size(); a++ ){
+    if( progPtrs[a]==e ){
+      return a;
+    }
+  }
+  return -1;
+}
+
+bool sccwriter::is_var( const std::string& str )
+{
+  for( int a=0; a<(int)vars.size(); a++ ){
+    if( vars[a]==str ){
+      return true;
+    }
+  }
+  return false;
+}
+
+void sccwriter::add_global_sym( const std::string& str )
+{
+  for( int a=0; a<(int)globalSyms.size(); a++ ){
+    if( globalSyms[a]==str ){
+      return;
+    }
+  }
+  globalSyms.push_back( str );
+}
+
+void sccwriter::indent( std::ostream& os, int ind )
+{
+   for( int a=0; a<ind; a++ )
+   {
+      os << "   ";
+   }
+}
+
+void sccwriter::write_function_header( std::ostream& os, int index, int opts )
+{
+  //write the function header
+  std::string fname;
+  get_function_name( progNames[index], fname );
+  os << "Expr* " << fname.c_str() << "( ";
+  CExpr* progvars = (CExpr*)get_prog( index )->kids[1];
+  int counter = 0;
+  //write each argument
+  while( progvars->kids[counter] )
+  {
+    if( counter!=0 )
+    {
+      os << ", ";
+    }
+    os << "Expr* ";
+    write_variable( ((SymSExpr*)progvars->kids[counter])->s, os );
+    //add to vars if options are set to do so
+    if( opts&opt_write_add_args )
+    {
+      vars.push_back( ((SymSExpr*)progvars->kids[counter])->s );
+    }
+    counter++;
+  }
+  os << " )";
+  if( opts&opt_write_call_debug )
+  {
+     os << "{" << std::endl;
+     indent( os, 1 );
+     os << "std::cout << \"Call function " << fname.c_str() << " with arguments \";" << std::endl;
+     counter = 0; 
+     while( progvars->kids[counter] )
+     {
+        if( counter!=0 )
+        {
+           indent( os, 1 );
+           os << "std::cout << \", \";" << std::endl;
+        }
+        indent( os, 1 );
+        write_variable( ((SymSExpr*)progvars->kids[counter])->s, os );
+        os << "->print( std::cout );" << std::endl;
+        counter++;
+     }
+     indent( os, 1 );
+     os << "std::cout << std::endl;" << std::endl;
+  }
+}
+
+void sccwriter::get_function_name( const std::string& pname, std::string& fname )
+{
+  fname = std::string( "f_" );
+  fname.append( pname );
+}
+
+void sccwriter::write_variable( const std::string& n, std::ostream& os )
+{
+  std::string nn;
+  get_var_name( n, nn );
+  os << nn.c_str();
+}
+
+void sccwriter::get_var_name( const std::string& n, std::string& nn ) {
+  nn = std::string( n.c_str() );
+  for( int i = 0; i <(int)n.length(); i++ ){
+    char c = n[i];
+    if (c <= 47)
+        c += 65;
+    else if (c >= 58 && c <= 64)
+        c += 97-58;
+    if ((c >= 91 && c <= 94) || c == 96)
+        c += 104-91;
+    else if (c >= 123)
+        c -= 4;
+    nn[i] = c;
+  }  
+}
+
+void sccwriter::write_file()
+{
+  static std::string filename( "scccode" );
+
+  //writer the h file
+  std::fstream fsh;
+  std::string fnameh( filename );
+  fnameh.append(".h");
+  fsh.open( fnameh.c_str(), std::ios::out );
+  //write the header in h
+  fsh << "#ifndef SCC_CODE_H" << std::endl;
+  fsh << "#define SCC_CODE_H" << std::endl << std::endl;
+  //include necessary files in h file
+  fsh << "#include \"check.h\"" << std::endl << std::endl;
+  //write the init function
+  fsh << "void init_compiled_scc();" << std::endl << std::endl;
+  //write the entry function
+  fsh << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );" << std::endl << std::endl;
+  //write the side condition code functions
+  for( int n=0; n<(int)progs.size(); n++ )
+  {
+    //write the header in the h file
+    fsh << "inline ";
+    write_function_header( fsh, n );
+    fsh << ";" << std::endl << std::endl;
+  }
+  fsh << "#endif" << std::endl << std::endl;
+  fsh.close();
+
+
+  //writer the cpp code
+  std::fstream fsc;
+  std::string fnamec( filename );
+  fnamec.append(".cpp");
+  fsc.open( fnamec.c_str(), std::ios::out );
+  //include the h file in the cpp
+  fsc << "#include \"scccode.h\"" << std::endl << std::endl;
+  std::ostringstream fsc_funcs;
+  //write the side condition code functions
+  for( currProgram=0; currProgram<(int)progs.size(); currProgram++ )
+  {
+    //reset naming counters
+    vars.clear();
+    exprCount = 0;
+    strCount = 0;
+    argsCount = 0;
+    rnumCount = 0;
+
+    //for debugging
+    std::cout << "program #" << currProgram << " " << progNames[currProgram].c_str() << std::endl;
+
+    //write the function header
+    write_function_header( fsc_funcs, currProgram, opt_write_add_args|options );
+    if( (options&opt_write_call_debug)==0 )
+    {
+       fsc_funcs << "{" << std::endl;
+    }
+    //write the code
+    //std::vector< std::string > cleanVec;
+    //write_code( get_prog( n )->kids[2], fsc, 1, "return ", cleanVec );
+    //debug_write_code( progs[n].second->kids[2], fsc, 1 );
+    std::string expr;
+    write_expr( get_prog( currProgram )->kids[2], fsc_funcs, 1, expr );
+    indent( fsc_funcs, 1 );
+    fsc_funcs << "return " << expr.c_str() << ";" << std::endl;
+    fsc_funcs << "}" << std::endl << std::endl;
+  }
+  //write the predefined symbols necessary - symbols and progs
+  for( int a=0; a<(int)globalSyms.size(); a++ )
+  {
+    fsc << "Expr* e_" << globalSyms[a].c_str() << ";" << std::endl;
+  }
+  for( int a=0; a<(int)progs.size(); a++ )
+  {
+    fsc << "Expr* e_" << progNames[a].c_str() << ";" << std::endl;
+  }
+  fsc << std::endl;
+  //write the init function - initialize symbols and progs
+  fsc << "void init_compiled_scc(){" << std::endl;
+  for( int a=0; a<(int)globalSyms.size(); a++ )
+  {
+    indent( fsc, 1 );
+    fsc << "e_" << globalSyms[a].c_str() << " = symbols->get(\"" << globalSyms[a].c_str() << "\").first;" << std::endl;
+  }
+  for( int a=0; a<(int)progs.size(); a++ )
+  {
+    indent( fsc, 1 );
+    fsc << "e_" << progNames[a].c_str() << " = progs[\"" << progNames[a].c_str() << "\"];" << std::endl;
+  }
+  fsc << "}" << std::endl << std::endl;
+  fsc << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){" << std::endl;
+  //for( int n=0; n<(int)progs.size(); n++ ){
+  //  indent( fsc, 1 );
+  //  fsc << "static std::string s_" << progNames[n].c_str() << " = std::string( \"" << progNames[n].c_str() << "\" );" << std::endl;
+  //}
+  for( int n=0; n<(int)progs.size(); n++ ){
+    indent( fsc, 1 );
+    if( n!=0 ){
+      fsc << "}else ";
+    }
+    //for each function, test to see if the string matches the name of the function
+    fsc << "if( p==e_" << progNames[n].c_str() << " ){" << std::endl;
+    indent( fsc, 2 );
+    std::string fname;
+    get_function_name( progNames[n], fname );
+    //map the function to the proper function
+    fsc << "return " << fname.c_str() << "( ";
+    //write the arguments to the function from args
+    CExpr* progvars = (CExpr*)get_prog( n )->kids[1];
+    int counter = 0;
+    bool firstTime = true;
+    while( progvars->kids[counter] )
+    {
+      if( !firstTime )
+      {
+        fsc << ", ";
+      }
+      fsc << "args[" << counter << "]";
+      firstTime = false;
+      counter++;
+    }
+    fsc << " );" << std::endl;
+  }
+  indent( fsc, 1 );
+  fsc << "}else{" << std::endl;
+  indent( fsc, 2 );
+  //return null in the case the function could not be found
+  fsc << "return NULL;" << std::endl;
+  indent( fsc, 1 );
+  fsc << "}" << std::endl;
+  fsc << "}" << std::endl << std::endl;
+  fsc << fsc_funcs.str().c_str();
+
+  fsc.close();
+}
+
+void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts )
+{
+  std::string retModString;
+  std::string incString;
+  if ( retModStr )
+  {
+    retModString = std::string( retModStr );
+    retModString.append( " = " );
+    incString = std::string( retModStr );
+    incString.append( "->inc();" );
+  }
+  switch( code->getclass() )
+  {
+  case INT_EXPR:
+    {
+      indent( os, ind );
+      os << retModString.c_str();
+      os << "new IntExpr( " << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl;
+      indent( os, ind );
+      os << incString.c_str() << std::endl;
+    }
+    break;
+  case RAT_EXPR:
+    {
+      mpz_t num, den;
+      mpz_init(num);
+      mpz_init(den);
+      mpq_get_num( num, ((RatExpr*)code)->n );
+      mpq_get_den( den, ((RatExpr*)code)->n );
+      indent( os, ind );
+      os << retModString.c_str();
+      os << "new RatExpr( " << mpz_get_si( num ) << ", " << mpz_get_si( den ) << " );" << std::endl;
+      indent( os, ind );
+      os << incString.c_str() << std::endl;
+    }
+    break;
+  case SYMS_EXPR:
+    {
+      //if it is a variable, simply write it to buffer
+      if( is_var( ((SymSExpr*)code)->s ) )
+      {
+        indent( os, ind );
+        os << retModString.c_str();
+        write_variable( ((SymSExpr*)code)->s.c_str(), os );
+        os << ";" << std::endl;  
+      }
+      else  //else must look at symbol lookup table
+      {
+        std::string var;
+        get_var_name( ((SymSExpr*)code)->s, var );
+        indent( os, ind );
+        os << retModString.c_str() << "e_" << var.c_str() << ";" << std::endl;
+        add_global_sym( var ); 
+      }
+      indent( os, ind );
+      os << incString.c_str() << std::endl;
+    }
+    break;
+  default:
+    switch( code->getop() )
+    {
     case APP:
       {
         //collect the arguments
@@ -403,7 +403,7 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
           //os << expr.c_str() << "->dec();" << std::endl;
         }
       }
-      break;

+      break;
     case MATCH:
       {
         //calculate the value for the expression
@@ -565,13 +565,13 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         if( retModStr!=NULL ){
           indent( os, ind );
           os << retModString.c_str() << expr.c_str() << ";" << std::endl;
-          indent( os, ind );

+          indent( os, ind );
           os << incString.c_str() << std::endl;
         }
         write_dec( expr, os, ind );
       }
       break;
-    case IFMARKED:

+    case IFMARKED:
       {
         //calculate the value for the expression
         std::string expr;
@@ -585,10 +585,10 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         os << "}else{" << std::endl;
         write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr );
         indent( os, ind );
-        os << "}" << std::endl;

-        //clean up memory

-        write_dec( expr, os, ind );

-      }

+        os << "}" << std::endl;
+        //clean up memory
+        write_dec( expr, os, ind );
+      }
       break;
 #else
     case MARKVAR:
@@ -612,7 +612,7 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         if( retModStr!=NULL ){
           indent( os, ind );
           os << retModString.c_str() << expr.c_str() << ";" << std::endl;
-          indent( os, ind );

+          indent( os, ind );
           os << incString.c_str() << std::endl;
         }
         write_dec( expr, os, ind );
@@ -631,12 +631,12 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr );
         indent( os, ind );
         os << "}" << std::endl;
-        //clean up memory

+        //clean up memory
         write_dec( expr1, os, ind );
         write_dec( expr2, os, ind );
       }
       break;
-    case IFMARKED:

+    case IFMARKED:
       {
         //calculate the value for the expression
         std::string expr;
@@ -651,10 +651,10 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         os << "}else{" << std::endl;
         write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr );
         indent( os, ind );
-        os << "}" << std::endl;

-        //clean up memory

-        write_dec( expr, os, ind );

-      }

+        os << "}" << std::endl;
+        //clean up memory
+        write_dec( expr, os, ind );
+      }
       break;
 #endif
     case ADD:
@@ -709,8 +709,8 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         write_dec( expr2, os, ind );
       }
       break;
-    case NEG:

-      {

+    case NEG:
+      {
         //calculate the value for the first expression
         std::string expr1;
         write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 );
@@ -726,9 +726,9 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         indent( os, ind+1 );
         os << "mpz_neg( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl;
         indent( os, ind+1 );
-        os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl;

+        os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl;
         indent( os, ind );
-        os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl;

+        os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl;
         indent( os, ind+1 );
         os << "mpq_t " << ss.str().c_str() << ";" << std::endl;
         indent( os, ind+1 );
@@ -736,55 +736,55 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
         indent( os, ind+1 );
         os << "mpq_neg( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl;
         indent( os, ind+1 );
-        os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl;

+        os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl;
         indent( os, ind );
-        os << "}" << std::endl;

-        //clean up memory

-        write_dec( expr1, os, ind );

-      }

-      break;

-    case IFNEG:

-    case IFZERO:

-      {

+        os << "}" << std::endl;
+        //clean up memory
+        write_dec( expr1, os, ind );
+      }
+      break;
+    case IFNEG:
+    case IFZERO:
+      {
         std::string expr1;
-        write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 );

+        write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 );
         indent( os, ind );
-        os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl;

-        indent( os, ind+1 );

-        os << "if( mpz_sgn( ((IntExpr *)" << expr1.c_str() << "->followDefs())->n ) ";

-        if( code->getop()==IFNEG )

-          os << "<";

-        else

-          os << "==";

-        os << " 0 ){" << std::endl;

-        write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr );

-        indent( os, ind+1 );

-        os << "}else{" << std::endl;

-        write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr );

-        indent( os, ind+1 );

-        os << "}" << std::endl;

+        os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl;
+        indent( os, ind+1 );
+        os << "if( mpz_sgn( ((IntExpr *)" << expr1.c_str() << "->followDefs())->n ) ";
+        if( code->getop()==IFNEG )
+          os << "<";
+        else
+          os << "==";
+        os << " 0 ){" << std::endl;
+        write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr );
+        indent( os, ind+1 );
+        os << "}else{" << std::endl;
+        write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr );
+        indent( os, ind+1 );
+        os << "}" << std::endl;
         indent( os, ind );
-        os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl;

-        indent( os, ind+1 );

-        os << "if( mpq_sgn( ((RatExpr *)" << expr1.c_str() << "->followDefs())->n ) ";

-        if( code->getop()==IFNEG )

-          os << "<";

-        else

-          os << "==";

-        os << " 0 ){" << std::endl;

-        write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr );

-        indent( os, ind+1 );

-        os << "}else{" << std::endl;

-        write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr );

-        indent( os, ind+1 );

-        os << "}" << std::endl;

+        os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl;
+        indent( os, ind+1 );
+        os << "if( mpq_sgn( ((RatExpr *)" << expr1.c_str() << "->followDefs())->n ) ";
+        if( code->getop()==IFNEG )
+          os << "<";
+        else
+          os << "==";
+        os << " 0 ){" << std::endl;
+        write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr );
+        indent( os, ind+1 );
+        os << "}else{" << std::endl;
+        write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr );
+        indent( os, ind+1 );
+        os << "}" << std::endl;
         indent( os, ind );
-        os << "}" << std::endl;

-        //clean up memory

-        write_dec( expr1, os, ind );

-      }

-      break;

-    case RUN:/*?*/break;

+        os << "}" << std::endl;
+        //clean up memory
+        write_dec( expr1, os, ind );
+      }
+      break;
+    case RUN:/*?*/break;
     case PI:/*?*/break;
     case LAM:/*?*/break;
     case TYPE:/*?*/break;
@@ -793,16 +793,16 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r
     case MPZ:/*?*/break;
     case PROG:/*?*/break;
     case PROGVARS:/*?*/break;
-    case PAT:/*?*/break;

-    }

-    break;

-  }

-}

-

-void sccwriter::write_args( CExpr* code, std::ostream& os, int ind, int childCounter, 

-                            std::vector< std::string >& args, int opts )

-{

-  bool encounterCase = false;

+    case PAT:/*?*/break;
+    }
+    break;
+  }
+}
+
+void sccwriter::write_args( CExpr* code, std::ostream& os, int ind, int childCounter, 
+                            std::vector< std::string >& args, int opts )
+{
+  bool encounterCase = false;
   while( code->kids[childCounter] &&
          (!encounterCase || code->kids[childCounter]->getop()==CASE ) )
   {
@@ -819,68 +819,68 @@ void sccwriter::write_args( CExpr* code, std::ostream& os, int ind, int childCou
       args.push_back( expr );
     }
     childCounter++;
-  }

-}

-

-void sccwriter::write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts )

-{

-  if( code->getclass()==SYMS_EXPR && is_var( ((SymSExpr*)code)->s ) )

-  {

-    get_var_name( ((SymSExpr*)code)->s, expr );

-    indent( os, ind );

-    os << expr.c_str() << "->inc();" << std::endl;

-  }

-  else

-  {

+  }
+}
+
+void sccwriter::write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts )
+{
+  if( code->getclass()==SYMS_EXPR && is_var( ((SymSExpr*)code)->s ) )
+  {
+    get_var_name( ((SymSExpr*)code)->s, expr );
+    indent( os, ind );
+    os << expr.c_str() << "->inc();" << std::endl;
+  }
+  else
+  {
     std::ostringstream ss;
     ss << "e" << exprCount;
-    exprCount++;

-    //declare the expression

-    indent( os, ind );

-    if( code->getclass()==SYMS_EXPR && !is_var( ((SymSExpr*)code)->s ) )

-    {

-      os << "static ";

-    }

-    os << "Expr* " << ss.str().c_str() << ";" << std::endl;

-    //write the expression

+    exprCount++;
+    //declare the expression
+    indent( os, ind );
+    if( code->getclass()==SYMS_EXPR && !is_var( ((SymSExpr*)code)->s ) )
+    {
+      os << "static ";
+    }
+    os << "Expr* " << ss.str().c_str() << ";" << std::endl;
+    //write the expression
     std::ostringstream ss2;
     ss2 << ss.str().c_str();
-    write_code( code, os, ind, ss2.str().c_str(), opts );

-

-    //if is not a sym expression, then decrement the expression and return null

-    if( opts&opt_write_check_sym_expr )

+    write_code( code, os, ind, ss2.str().c_str(), opts );
+
+    //if is not a sym expression, then decrement the expression and return null
+    if( opts&opt_write_check_sym_expr )
     {
       indent( os, ind );
       os << "if (" << expr.c_str() << "->getclass() != SYM_EXPR) {" << std::endl;
       indent( os, ind+1 );
       os << "exit( 1 );" << std::endl;
       indent( os, ind );
-      os << "}" << std::endl;

-    }

-

-    expr = std::string( ss.str().c_str() );

-    vars.push_back( expr );

-  }

-  //increment the counter for memory management

-  //indent( os, ind );

-  //os << expr.c_str() << "->inc();" << std::endl;

-}

-

-void sccwriter::write_dec( const std::string& expr, std::ostream& os, int ind )

-{

-  bool wd = true;

-  if( wd )

-  {

-    indent( os, ind );

-    os << expr.c_str() << "->dec();" << std::endl;

-  }

-}

-

-void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind )

-{

-  indent( os, ind );

-  switch( code->getclass() )

-  {

+      os << "}" << std::endl;
+    }
+
+    expr = std::string( ss.str().c_str() );
+    vars.push_back( expr );
+  }
+  //increment the counter for memory management
+  //indent( os, ind );
+  //os << expr.c_str() << "->inc();" << std::endl;
+}
+
+void sccwriter::write_dec( const std::string& expr, std::ostream& os, int ind )
+{
+  bool wd = true;
+  if( wd )
+  {
+    indent( os, ind );
+    os << expr.c_str() << "->dec();" << std::endl;
+  }
+}
+
+void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind )
+{
+  indent( os, ind );
+  switch( code->getclass() )
+  {
   case INT_EXPR:
     os << "int_expr";
     break;
@@ -890,12 +890,12 @@ void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind )
   case SYM_EXPR:
     os << "sym_expr";
     break;
-  case SYMS_EXPR:

-    os << "syms_expr: " << ((SymSExpr*)code)->s.c_str();

-    break;

-  default:

-    switch( code->getop() )

-    {

+  case SYMS_EXPR:
+    os << "syms_expr: " << ((SymSExpr*)code)->s.c_str();
+    break;
+  default:
+    switch( code->getop() )
+    {
     case APP:
       os << "app";
       break;
@@ -920,9 +920,9 @@ void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind )
     case PROG:
       os << "prog";
       break;
-    case PROGVARS:

-      os << "progvars";

-      break;

+    case PROGVARS:
+      os << "progvars";
+      break;
     case MATCH:
       os << "match";
       break;
@@ -953,25 +953,25 @@ void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind )
     case MARKVAR:
       os << "markvar";
       break;
-    case IFMARKED:

-      os << "ifmarked";

-      break;

-    case COMPARE:

-      os << "compare";

-      break;

-    default:

-      os << "???";

-      break;

-    }

-  }

-  os << std::endl;

-  if( code->getop()!=0 )

-  {

-    CExpr* ce = (CExpr*)code;

-    int counter = 0;

-    while( ce->kids[counter] ){

-      debug_write_code( ce->kids[counter], os, ind+1 );

-      counter++;

-    }

-  }

-}

+    case IFMARKED:
+      os << "ifmarked";
+      break;
+    case COMPARE:
+      os << "compare";
+      break;
+    default:
+      os << "???";
+      break;
+    }
+  }
+  os << std::endl;
+  if( code->getop()!=0 )
+  {
+    CExpr* ce = (CExpr*)code;
+    int counter = 0;
+    while( ce->kids[counter] ){
+      debug_write_code( ce->kids[counter], os, ind+1 );
+      counter++;
+    }
+  }
+}
diff --git a/proofs/lfsc_checker/sccwriter.h b/proofs/lfsc_checker/sccwriter.h
index f8922934f..bd9732579 100644
--- a/proofs/lfsc_checker/sccwriter.h
+++ b/proofs/lfsc_checker/sccwriter.h
@@ -1,86 +1,86 @@
-#ifndef SCC_WRITER_H

-#define SCC_WRITER_H

-

-#include "expr.h"

-#include <vector>

-#include "check.h"

-

-enum

-{

-  opt_write_case_body = 0x00000001,

-  opt_write_check_sym_expr = 0x00000002,

-  opt_write_add_args = 0x000000004,

-  opt_write_no_inc = 0x00000008,

-

-  opt_write_call_debug = 0x00000010,

-  opt_write_nested_app = 0x00000020,

-};

-

-class sccwriter

-{

-private:

-  //options

-   int options;

-  //programs to write to file

-  symmap progs;

-  //list of indicies in progs

-  std::vector< Expr* > progPtrs;

-  std::vector< std::string > progNames;

-  int currProgram;

-  //current variables in the scope

-  std::vector< std::string > vars;

-  //global variables stored for lookups

-  std::vector< std::string > globalSyms;

-  //symbols that must be dec'ed

-  std::vector< std::string > decSyms;

-  //get program

-  CExpr* get_prog( int n ) { return (CExpr*)progs[ progNames[n] ]; }

-  //get index for string

-  int get_prog_index_by_expr( Expr* e );

-  int get_prog_index( const std::string& str );

-  //is variable in current scope

-  bool is_var( const std::string& str );

-  //add global sym

-  void add_global_sym( const std::string& str );

-  //expression count

-  static int exprCount;

-  //string count

-  static int strCount;

-  //args count

-  static int argsCount;

-  //num count

-  static int rnumCount;

-  //indent

-  static void indent( std::ostream& os, int ind );

-  //write function header

-  void write_function_header( std::ostream& os, int index, int opts = 0 );

-  void write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts = 0 );

-  //write all children starting at child counter to stream, store in Expr* e_...e_;

-  void write_args( CExpr* code, std::ostream& os, int ind, int childCounter, std::vector< std::string >& args, int opts = 0 );

-  //write expression - store result of code into e_ for some Expr* e_;

-  void write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts = 0 );

-  //write variable

-  void write_variable( const std::string& n, std::ostream& os );

-  //get function name

-  void get_function_name( const std::string& pname, std::string& fname );

-  //get the variable name

-  void get_var_name( const std::string& n, std::string& nn );

-  //write dec

-  void write_dec( const std::string& expr, std::ostream& os, int ind );

-public:

-  sccwriter( int opts = 0 ) : options( opts ){}

-  virtual ~sccwriter(){}

-

-  void add_scc( const std::string& pname, Expr* exp ) { 

-    //progs.push_back( std::pair< std::string, CExpr* >( pname, exp ) ); 

-    progs[pname] = exp;

-    progPtrs.push_back( exp );

-    progNames.push_back( pname );

-  }

-

-  void write_file();

-  //write code

-  static void debug_write_code( Expr* code, std::ostream& os, int ind );

-};

-

-#endif

+#ifndef SCC_WRITER_H
+#define SCC_WRITER_H
+
+#include "expr.h"
+#include <vector>
+#include "check.h"
+
+enum
+{
+  opt_write_case_body = 0x00000001,
+  opt_write_check_sym_expr = 0x00000002,
+  opt_write_add_args = 0x000000004,
+  opt_write_no_inc = 0x00000008,
+
+  opt_write_call_debug = 0x00000010,
+  opt_write_nested_app = 0x00000020,
+};
+
+class sccwriter
+{
+private:
+  //options
+   int options;
+  //programs to write to file
+  symmap progs;
+  //list of indicies in progs
+  std::vector< Expr* > progPtrs;
+  std::vector< std::string > progNames;
+  int currProgram;
+  //current variables in the scope
+  std::vector< std::string > vars;
+  //global variables stored for lookups
+  std::vector< std::string > globalSyms;
+  //symbols that must be dec'ed
+  std::vector< std::string > decSyms;
+  //get program
+  CExpr* get_prog( int n ) { return (CExpr*)progs[ progNames[n] ]; }
+  //get index for string
+  int get_prog_index_by_expr( Expr* e );
+  int get_prog_index( const std::string& str );
+  //is variable in current scope
+  bool is_var( const std::string& str );
+  //add global sym
+  void add_global_sym( const std::string& str );
+  //expression count
+  static int exprCount;
+  //string count
+  static int strCount;
+  //args count
+  static int argsCount;
+  //num count
+  static int rnumCount;
+  //indent
+  static void indent( std::ostream& os, int ind );
+  //write function header
+  void write_function_header( std::ostream& os, int index, int opts = 0 );
+  void write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts = 0 );
+  //write all children starting at child counter to stream, store in Expr* e_...e_;
+  void write_args( CExpr* code, std::ostream& os, int ind, int childCounter, std::vector< std::string >& args, int opts = 0 );
+  //write expression - store result of code into e_ for some Expr* e_;
+  void write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts = 0 );
+  //write variable
+  void write_variable( const std::string& n, std::ostream& os );
+  //get function name
+  void get_function_name( const std::string& pname, std::string& fname );
+  //get the variable name
+  void get_var_name( const std::string& n, std::string& nn );
+  //write dec
+  void write_dec( const std::string& expr, std::ostream& os, int ind );
+public:
+  sccwriter( int opts = 0 ) : options( opts ){}
+  virtual ~sccwriter(){}
+
+  void add_scc( const std::string& pname, Expr* exp ) { 
+    //progs.push_back( std::pair< std::string, CExpr* >( pname, exp ) ); 
+    progs[pname] = exp;
+    progPtrs.push_back( exp );
+    progNames.push_back( pname );
+  }
+
+  void write_file();
+  //write code
+  static void debug_write_code( Expr* code, std::ostream& os, int ind );
+};
+
+#endif
diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf
index 02cadaeab..ae585e455 100755
--- a/proofs/signatures/ex_bv.plf
+++ b/proofs/signatures/ex_bv.plf
@@ -1,57 +1,57 @@
-; a = b ^ a = 00000 ^ b = 11111 is UNSAT

-

-(check

-(% a var_bv

-(% b var_bv

-(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))

-(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))

-(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))

-(: (holds cln)

-

-(decl_bv_atom_var 5 a (\ ba1

-(decl_bv_atom_var 5 b (\ ba2

-(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3

-(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4

-

-(decl_atom (bblast a 4) (\ v1 (\ a1

-(decl_atom (bblast b 4) (\ v2 (\ a2

-

-; bitblasting terms

-(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1

-(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2

-(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3

-(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4

-

-; bitblasting formulas

-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1

-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2

-(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3

-

-; CNFication

-; a.4 V ~b.4

-(satlem _ _

-(asf _ _ _ a1 (\ l1

-(ast _ _ _ a2 (\ l2

-(clausify_false

-  (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1)   ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation

-))))) (\ C2

-

-; ~a.4

-(satlem _ _

-(ast _ _ _ a1 (\ l1

-(clausify_false

-  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))

-))) (\ C3

-

-; b.4 

-(satlem _ _

-(asf _ _ _ a2 (\ l2

-(clausify_false

-  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)

-))) (\ C6

-

-

-(satlem_simplify _ _ _ 

-(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))

-

+; a = b ^ a = 00000 ^ b = 11111 is UNSAT
+
+(check
+(% a var_bv
+(% b var_bv
+(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))
+(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))
+(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
+(: (holds cln)
+
+(decl_bv_atom_var 5 a (\ ba1
+(decl_bv_atom_var 5 b (\ ba2
+(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
+(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4
+
+(decl_atom (bblast a 4) (\ v1 (\ a1
+(decl_atom (bblast b 4) (\ v2 (\ a2
+
+; bitblasting terms
+(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1
+(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4
+
+; bitblasting formulas
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ bf2
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt2 bt4) (\ bf3
+
+; CNFication
+; a.4 V ~b.4
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(clausify_false
+  (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1)   ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation
+))))) (\ C2
+
+; ~a.4
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(clausify_false
+  (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))
+))) (\ C3
+
+; b.4 
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+  (contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)
+))) (\ C6
+
+
+(satlem_simplify _ _ _ 
+(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
+
 )))))))))))))))))))))))))))))))))))))))))))
\ No newline at end of file
diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf
index 3fb9d1356..0fb50f8cf 100755
--- a/proofs/signatures/th_bv.plf
+++ b/proofs/signatures/th_bv.plf
@@ -1,145 +1,145 @@
-; "bitvec" is a term of type "sort"

-(declare BitVec sort)

-

-; bit type

-(declare bit type)

-(declare b0 bit)

-(declare b1 bit)

-

-; bit vector type

-(declare bv type)

-(declare bvn bv)

-(declare bvc (! b bit (! v bv bv)))

-; a bv constant term

-(declare a_bv (! v bv (term BitVec)))

-

-; calculate the length of a bitvector

-(program bv_len ((v bv)) mpz 

-  (match v

-    (bvn 0)

-    ((bvc b v') (mp_add (bv_len v') 1))))

-

-; a bv variable

-(declare var_bv type)

-; a bv variable term

-(declare a_var_bv (! v var_bv (term BitVec)))

-

-

-; bit vector operators

-(define bvoper (! x (term BitVec) 

-               (! y (term BitVec) 

-                    (term BitVec))))

-(declare bvand bvoper)

-(declare bvadd bvoper)

-;....

-

-; all bit-vector terms are mapped with "bv_atom" to:

-;  - a simply-typed term of type "var_bv", which is necessary for bit-blasting

-;  - a integer size

-(declare bv_atom (! x (term BitVec) (! y var_bv (! n mpz type))))

-

-(declare decl_bv_atom_var (! n mpz    ; must be specified

-                          (! x var_bv

-                          (! p (! u (bv_atom (a_var_bv x) x n)

-                                 (holds cln))

-                             (holds cln)))))

-

-(declare decl_bv_atom_const (! n mpz

-                            (! v bv

-                            (! s (^ (bv_len v) n)

-                            (! p (! w var_bv

-                                 (! u (bv_atom (a_bv v) w n)

-                                   (holds cln)))

-			      (holds cln))))))

-

-

-; other terms here?

-

-

-; bit blasted terms

-(declare bblt type)

-(declare bbltn bblt)

-(declare bbltc (! f formula (! v bblt bblt)))

-

-; (bblast_term x y) means term x corresponds to bit level interpretation y

-(declare bblast_term (! x (term BitVec) (! y bblt formula)))

-

-; a predicate to represent the n^th bit of a bitvector term

-(declare bblast (! x var_bv (! n mpz formula)))

-

-

-; bit blast  constant

-(program bblast_const ((v bv) (n mpz)) bblt

-  (mp_ifneg n (match v (bvn bbltn) 

-                       (default (fail bblt)))

-              (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1)))))

-                       (default (fail bblt)))))

-              

-(declare bv_bbl_const (! n mpz

-                      (! v bv

-                      (! x var_bv

-                      (! f bblt

-                      (! u (bv_atom (a_bv v) x n)

-                      (! c (^ (bblast_const v (mp_add n (~ 1))) f)

-                         (th_holds (bblast_term (a_bv v) f)))))))))

-

-; bit blast  variable

-(program bblast_var ((x var_bv) (n mpz)) bblt

-  (mp_ifneg n bbltn 

-              (bbltc (bblast x n) (bblast_var x (mp_add n (~ 1))))))

-

-(declare bv_bbl_var (! n mpz

-                    (! x var_bv

-                    (! f bblt                    

-                    (! u (bv_atom (a_var_bv x) x n)

-                    (! c (^ (bblast_var x (mp_add n (~ 1))) f)

-                       (th_holds (bblast_term (a_var_bv x) f))))))))

-

-; bit blast  x = y

-;  for x,y of size n, it will return a conjuction (x.{n-1} = y.{n-1} ^ ( ... ^ (x.0 = y.0 ^ true)))

-(program bblast_eq ((x bblt) (y bblt)) formula

-  (match x 

-    (bbltn (match y (bbltn true) (default (fail formula))))

-    ((bbltc fx x') (match y 

-                      (bbltn (fail formula))

-                      ((bbltc fy y') (and (iff fx fy) (bblast_eq x' y')))))))

-

-(declare bv_bbl_eq (! x (term BitVec)

-                   (! y (term BitVec)

-                   (! fx bblt

-                   (! fy bblt

-                   (! f formula

-                   (! ux (th_holds (bblast_term x fx))

-                   (! uy (th_holds (bblast_term y fy))

-                   (! c (^ (bblast_eq fx fy) f)

-                      (th_holds (impl (= BitVec x y) f)))))))))))

-

-

-; rewrite rule :

-; x + y = y + x

-(declare bvadd_symm (! x (term BitVec)

-                    (! y (term BitVec)

-                    (! x' var_bv

-                    (! y' var_bv

-                    (! n mpz

-                    (! ux (bv_atom x x' n)

-                    (! uy (bv_atom y y' n)

-                       (th_holds (= BitVec (bvadd x y) (bvadd y x)))))))))))

-

-

-

-; necessary? 

-(program calc_bvand ((a bv) (b bv)) bv

-  (match a

-    (bvn (match b (bvn bvn) (default (fail bv))))

-    ((bvc ba a') (match b

-                      ((bvc bb b') (bvc (match ba (b0 b0) (b1 bb)) (calc_bvand a' b')))

-                      (default (fail bv))))))

-

-; rewrite rule (w constants) :

-; a & b = c    

-(declare bvand_const (! c bv

-		     (! a bv

-                     (! b bv

-                     (! u (^ (calc_bvand a b) c)

+; "bitvec" is a term of type "sort"
+(declare BitVec sort)
+
+; bit type
+(declare bit type)
+(declare b0 bit)
+(declare b1 bit)
+
+; bit vector type
+(declare bv type)
+(declare bvn bv)
+(declare bvc (! b bit (! v bv bv)))
+; a bv constant term
+(declare a_bv (! v bv (term BitVec)))
+
+; calculate the length of a bitvector
+(program bv_len ((v bv)) mpz 
+  (match v
+    (bvn 0)
+    ((bvc b v') (mp_add (bv_len v') 1))))
+
+; a bv variable
+(declare var_bv type)
+; a bv variable term
+(declare a_var_bv (! v var_bv (term BitVec)))
+
+
+; bit vector operators
+(define bvoper (! x (term BitVec) 
+               (! y (term BitVec) 
+                    (term BitVec))))
+(declare bvand bvoper)
+(declare bvadd bvoper)
+;....
+
+; all bit-vector terms are mapped with "bv_atom" to:
+;  - a simply-typed term of type "var_bv", which is necessary for bit-blasting
+;  - a integer size
+(declare bv_atom (! x (term BitVec) (! y var_bv (! n mpz type))))
+
+(declare decl_bv_atom_var (! n mpz    ; must be specified
+                          (! x var_bv
+                          (! p (! u (bv_atom (a_var_bv x) x n)
+                                 (holds cln))
+                             (holds cln)))))
+
+(declare decl_bv_atom_const (! n mpz
+                            (! v bv
+                            (! s (^ (bv_len v) n)
+                            (! p (! w var_bv
+                                 (! u (bv_atom (a_bv v) w n)
+                                   (holds cln)))
+			      (holds cln))))))
+
+
+; other terms here?
+
+
+; bit blasted terms
+(declare bblt type)
+(declare bbltn bblt)
+(declare bbltc (! f formula (! v bblt bblt)))
+
+; (bblast_term x y) means term x corresponds to bit level interpretation y
+(declare bblast_term (! x (term BitVec) (! y bblt formula)))
+
+; a predicate to represent the n^th bit of a bitvector term
+(declare bblast (! x var_bv (! n mpz formula)))
+
+
+; bit blast  constant
+(program bblast_const ((v bv) (n mpz)) bblt
+  (mp_ifneg n (match v (bvn bbltn) 
+                       (default (fail bblt)))
+              (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1)))))
+                       (default (fail bblt)))))
+              
+(declare bv_bbl_const (! n mpz
+                      (! v bv
+                      (! x var_bv
+                      (! f bblt
+                      (! u (bv_atom (a_bv v) x n)
+                      (! c (^ (bblast_const v (mp_add n (~ 1))) f)
+                         (th_holds (bblast_term (a_bv v) f)))))))))
+
+; bit blast  variable
+(program bblast_var ((x var_bv) (n mpz)) bblt
+  (mp_ifneg n bbltn 
+              (bbltc (bblast x n) (bblast_var x (mp_add n (~ 1))))))
+
+(declare bv_bbl_var (! n mpz
+                    (! x var_bv
+                    (! f bblt                    
+                    (! u (bv_atom (a_var_bv x) x n)
+                    (! c (^ (bblast_var x (mp_add n (~ 1))) f)
+                       (th_holds (bblast_term (a_var_bv x) f))))))))
+
+; bit blast  x = y
+;  for x,y of size n, it will return a conjuction (x.{n-1} = y.{n-1} ^ ( ... ^ (x.0 = y.0 ^ true)))
+(program bblast_eq ((x bblt) (y bblt)) formula
+  (match x 
+    (bbltn (match y (bbltn true) (default (fail formula))))
+    ((bbltc fx x') (match y 
+                      (bbltn (fail formula))
+                      ((bbltc fy y') (and (iff fx fy) (bblast_eq x' y')))))))
+
+(declare bv_bbl_eq (! x (term BitVec)
+                   (! y (term BitVec)
+                   (! fx bblt
+                   (! fy bblt
+                   (! f formula
+                   (! ux (th_holds (bblast_term x fx))
+                   (! uy (th_holds (bblast_term y fy))
+                   (! c (^ (bblast_eq fx fy) f)
+                      (th_holds (impl (= BitVec x y) f)))))))))))
+
+
+; rewrite rule :
+; x + y = y + x
+(declare bvadd_symm (! x (term BitVec)
+                    (! y (term BitVec)
+                    (! x' var_bv
+                    (! y' var_bv
+                    (! n mpz
+                    (! ux (bv_atom x x' n)
+                    (! uy (bv_atom y y' n)
+                       (th_holds (= BitVec (bvadd x y) (bvadd y x)))))))))))
+
+
+
+; necessary? 
+(program calc_bvand ((a bv) (b bv)) bv
+  (match a
+    (bvn (match b (bvn bvn) (default (fail bv))))
+    ((bvc ba a') (match b
+                      ((bvc bb b') (bvc (match ba (b0 b0) (b1 bb)) (calc_bvand a' b')))
+                      (default (fail bv))))))
+
+; rewrite rule (w constants) :
+; a & b = c    
+(declare bvand_const (! c bv
+		     (! a bv
+                     (! b bv
+                     (! u (^ (calc_bvand a b) c)
                         (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c))))))))                        
\ No newline at end of file