1 files changed, 28 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/libwriter.h b/proofs/lfsc_checker/libwriter.h
new file mode 100644
index 000000000..093cf541b
--- /dev/null
+++ b/proofs/lfsc_checker/libwriter.h
@@ -0,0 +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