1 files changed, 27 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/scccode.h b/proofs/lfsc_checker/scccode.h
new file mode 100644
index 000000000..6f5efc8b5
--- /dev/null
+++ b/proofs/lfsc_checker/scccode.h
@@ -0,0 +1,27 @@
+#ifndef SCC_CODE_H
+#define SCC_CODE_H
+
+#include "check.h"
+
+void init_compiled_scc();
+
+Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );
+
+inline Expr* f_litvar( Expr* l );
+
+inline Expr* f_litpol( Expr* l );
+
+inline Expr* f_notb( Expr* b );
+
+inline Expr* f_iffb( Expr* b1, Expr* b2 );
+
+inline Expr* f_clear_mark( Expr* v );
+
+inline Expr* f_append( Expr* c1, Expr* c2 );
+
+inline Expr* f_simplify_clause_h( Expr* pol, Expr* c );
+
+inline Expr* f_simplify_clause( Expr* c );
+
+#endif
+