move SVA_to_LTL into separate header file

Introduce a header file for sva_to_ltl.cpp.

Author: kroening

src/ebmc/bdd_engine.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/sat/satcheck.h>
 #include <temporal-logic/ctl.h>
 #include <temporal-logic/ltl.h>
+#include <temporal-logic/sva_to_ltl.h>
 #include <temporal-logic/temporal_logic.h>
 #include <trans-netlist/aig_prop.h>
 #include <trans-netlist/instantiate_netlist.h>

src/ebmc/output_smv_word_level.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/bitvector_types.h>
 
 #include <smvlang/expr2smv.h>
+#include <temporal-logic/sva_to_ltl.h>
 
 #include "ebmc_error.h"
 #include "ebmc_properties.h"

src/temporal-logic/sva_to_ltl.cpp

@@ -6,6 +6,8 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include "sva_to_ltl.h"
+
 #include <util/arith_tools.h>
 
 #include <verilog/sva_expr.h>

src/temporal-logic/sva_to_ltl.h

@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: SVA to LTL
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEMPORAL_LOGIC_SVA_TO_LTL_H
+#define CPROVER_TEMPORAL_LOGIC_SVA_TO_LTL_H
+
+#include <util/expr.h>
+
+/// If possible, this maps an SVA expression to an equivalent LTL
+/// expression, or otherwise returns {}.
+std::optional<exprt> SVA_to_LTL(exprt);
+
+#endif

src/temporal-logic/temporal_logic.h

@@ -81,10 +81,6 @@ bool is_SVA_always_s_eventually_p(const exprt &);
 /// returns {} if not possible
 std::optional<exprt> LTL_to_CTL(exprt);
 
-/// If possible, this maps an SVA expression to an equivalent LTL
-/// expression, or otherwise returns {}.
-std::optional<exprt> SVA_to_LTL(exprt);
-
 /// Returns true iff the given expression is an SVA expression that
 /// we can convert into a Buechi automaton
 bool is_Buechi_SVA(const exprt &);

src/trans-netlist/instantiate_netlist.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ebmc/ebmc_error.h>
 #include <solvers/prop/literal_expr.h>
+#include <temporal-logic/sva_to_ltl.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 

src/trans-netlist/trans_to_netlist.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/prop/literal_expr.h>
 #include <temporal-logic/ctl.h>
 #include <temporal-logic/ltl.h>
+#include <temporal-logic/sva_to_ltl.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>