move decision_procedure.h to src/solvers

Daniel Kroening · Daniel Kroening · commit 627afcf88a82 · 2019-04-14T13:17:46.000+01:00
The new API has no dependency on or connection with anything in prop.
diff --git a/jbmc/src/jbmc/bmc.h b/jbmc/src/jbmc/bmc.h
@@ -30,7 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/safety_checker.h>
 #include <goto-symex/memory_model.h>
 
-#include <solvers/prop/decision_procedure.h>
+#include <solvers/decision_procedure.h>
 
 class cbmc_solverst;
 
diff --git a/jbmc/src/jbmc/module_dependencies.txt b/jbmc/src/jbmc/module_dependencies.txt
@@ -9,6 +9,7 @@ jbmc
 langapi # should go away
 linking
 pointer-analysis
+solvers
 solvers/refinement
 solvers/prop
 solvers/sat
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -13,7 +13,7 @@ Author: Matt Lewis
 
 #include <util/fixedbv.h>
 
-#include <solvers/prop/decision_procedure.h>
+#include <solvers/decision_procedure.h>
 
 #include <goto-symex/slice.h>
 
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -79,6 +79,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(PICOSAT_SRC) \
       $(SQUOLEM2_SRC) \
       $(CADICAL_SRC) \
+      decision_procedure.cpp \
       flattening/arrays.cpp \
       flattening/boolbv.cpp \
       flattening/boolbv_abs.cpp \
@@ -144,7 +145,6 @@ SRC = $(BOOLEFORCE_SRC) \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \
-      prop/decision_procedure.cpp \
       prop/literal.cpp \
       prop/prop_minimize.cpp \
       prop/prop.cpp \
diff --git a/src/solvers/decision_procedure.cpp b/src/solvers/decision_procedure.cpp
diff --git a/src/solvers/decision_procedure.h b/src/solvers/decision_procedure.h
@@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Decision Procedure Interface
 
-#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
-#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
+#ifndef CPROVER_SOLVERS_DECISION_PROCEDURE_H
+#define CPROVER_SOLVERS_DECISION_PROCEDURE_H
 
 #include <iosfwd>
 #include <string>
@@ -75,4 +75,4 @@ operator<<(decision_proceduret &dest, const exprt &src)
   return dest;
 }
 
-#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
+#endif // CPROVER_SOLVERS_DECISION_PROCEDURE_H
diff --git a/src/solvers/lowering/functions.h b/src/solvers/lowering/functions.h
@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/mathematical_expr.h>
 
-#include <solvers/prop/decision_procedure.h>
+#include <solvers/decision_procedure.h>
 
 class functionst
 {
diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h
@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <list>
 
-#include "decision_procedure.h"
+#include <solvers/decision_procedure.h>
 
 #include <util/expr.h>
 
diff --git a/src/solvers/prop/module_dependencies.txt b/src/solvers/prop/module_dependencies.txt
@@ -1,3 +1,4 @@
+solvers
 solvers/prop
 solvers/bdd
 util
diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h
@@ -10,7 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H
 #define CPROVER_SOLVERS_PROP_PROP_CONV_H
 
-#include "decision_procedure.h"
+#include <solvers/decision_procedure.h>
+
 #include "literal.h"
 
 class tvt;
diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h
@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 #include <util/std_expr.h>
 
-#include "decision_procedure.h"
 #include "literal.h"
 #include "literal_expr.h"
 #include "prop.h"

Original file line number	Diff line number	Diff line change
`@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]`
`17`	`17`
`18`	`18`	`#include <util/mathematical_expr.h>`
`19`	`19`
`20`		`-#include <solvers/prop/decision_procedure.h>`
	`20`	`+#include <solvers/decision_procedure.h>`
`21`	`21`
`22`	`22`	`class functionst`
`23`	`23`	`{`
-Original file line number
+Diff line change
@@ @@ -1,3 +1,4 @@ @@
 +solvers
 solvers/prop
 solvers/bdd
 util