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

(mostly whitespace differences).

1 files changed, 238 insertions, 238 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;
+  }
+}