From 5186ca79710fe935d1f7ed27c4a34e913ab547e8 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 12 Dec 2013 18:24:54 -0500 Subject: First attempt at incorporating LFSC proof checker into CVC4. --- proofs/lfsc_checker/libwriter.h | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 proofs/lfsc_checker/libwriter.h (limited to 'proofs/lfsc_checker/libwriter.h') 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 + +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 -- cgit v1.2.3