From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 13 Sep 2018 22:17:39 +0000 (-0700)
Subject: Fix #include for minisat headers in bvminisat. (#2463)
X-Git-Tag: cvc5-1.0.0~4651
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb7f6bf4eb7a84ce0e9c2f6578ce76ecab88d020;p=cvc5.git

Fix #include for minisat headers in bvminisat. (#2463)
---

diff --git a/src/prop/bvminisat/core/Dimacs.h b/src/prop/bvminisat/core/Dimacs.h
index 46451d464..c94f473a9 100644
--- a/src/prop/bvminisat/core/Dimacs.h
+++ b/src/prop/bvminisat/core/Dimacs.h
@@ -23,8 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <stdio.h>
 
-#include "utils/ParseUtils.h"
-#include "core/SolverTypes.h"
+#include "prop/bvminisat/core/SolverTypes.h"
+#include "prop/bvminisat/utils/ParseUtils.h"
 
 namespace CVC4 {
 namespace BVMinisat {
diff --git a/src/prop/bvminisat/core/Main.cc b/src/prop/bvminisat/core/Main.cc
index 74cc9cde8..307a4d7d9 100644
--- a/src/prop/bvminisat/core/Main.cc
+++ b/src/prop/bvminisat/core/Main.cc
@@ -23,12 +23,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <signal.h>
 #include <zlib.h>
 
-#include "utils/System.h"
-#include "utils/ParseUtils.h"
-#include "utils/Options.h"
-#include "core/Dimacs.h"
-#include "core/Solver.h"
-
+#include "prop/bvminisat/core/Dimacs.h"
+#include "prop/bvminisat/core/Solver.h"
+#include "prop/bvminisat/utils/Options.h"
+#include "prop/bvminisat/utils/ParseUtils.h"
+#include "prop/bvminisat/utils/System.h"
 
 namespace CVC4 {
 namespace BVMinisat {
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 740c2e5e6..372f8eb04 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -18,7 +18,7 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "core/Solver.h"
+#include "prop/bvminisat/core/Solver.h"
 
 #include <math.h>
 
@@ -27,7 +27,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "base/exception.h"
 #include "base/output.h"
-#include "mtl/Sort.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "proof/bitvector_proof.h"
@@ -35,6 +34,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
 #include "proof/sat_proof_implementation.h"
+#include "prop/bvminisat/mtl/Sort.h"
 #include "theory/interrupted.h"
 #include "util/utility.h"
 
diff --git a/src/prop/bvminisat/mtl/Sort.h b/src/prop/bvminisat/mtl/Sort.h
index f668aa856..f4a10aabb 100644
--- a/src/prop/bvminisat/mtl/Sort.h
+++ b/src/prop/bvminisat/mtl/Sort.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BVMinisat_Sort_h
 #define BVMinisat_Sort_h
 
-#include "mtl/Vec.h"
+#include "prop/bvminisat/mtl/Vec.h"
 
 //=================================================================================================
 // Some sorting algorithms for vec's
diff --git a/src/prop/bvminisat/simp/Main.cc b/src/prop/bvminisat/simp/Main.cc
index 96e318e5f..481ed3f39 100644
--- a/src/prop/bvminisat/simp/Main.cc
+++ b/src/prop/bvminisat/simp/Main.cc
@@ -24,12 +24,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <zlib.h>
 #include <sys/resource.h>
 
-#include "utils/System.h"
-#include "utils/ParseUtils.h"
-#include "utils/Options.h"
-#include "core/Dimacs.h"
-#include "simp/SimpSolver.h"
-
+#include "prop/bvminisat/core/Dimacs.h"
+#include "prop/bvminisat/simp/SimpSolver.h"
+#include "prop/bvminisat/utils/Options.h"
+#include "prop/bvminisat/utils/ParseUtils.h"
+#include "prop/bvminisat/utils/System.h"
 
 //=================================================================================================
 
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index cb5929320..2fa8d472d 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -18,14 +18,14 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "simp/SimpSolver.h"
+#include "prop/bvminisat/simp/SimpSolver.h"
 
-#include "mtl/Sort.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "proof/clause_id.h"
 #include "proof/proof.h"
-#include "utils/System.h"
+#include "prop/bvminisat/mtl/Sort.h"
+#include "prop/bvminisat/utils/System.h"
 
 namespace CVC4 {
 namespace BVMinisat {
diff --git a/src/prop/bvminisat/utils/Options.cc b/src/prop/bvminisat/utils/Options.cc
index b2094d466..ac0964623 100644
--- a/src/prop/bvminisat/utils/Options.cc
+++ b/src/prop/bvminisat/utils/Options.cc
@@ -17,9 +17,9 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "mtl/Sort.h"
-#include "utils/Options.h"
-#include "utils/ParseUtils.h"
+#include "prop/bvminisat/utils/Options.h"
+#include "prop/bvminisat/mtl/Sort.h"
+#include "prop/bvminisat/utils/ParseUtils.h"
 
 namespace CVC4 {
 namespace BVMinisat {
diff --git a/src/prop/bvminisat/utils/System.cc b/src/prop/bvminisat/utils/System.cc
index dab33af3e..aba0a5ac5 100644
--- a/src/prop/bvminisat/utils/System.cc
+++ b/src/prop/bvminisat/utils/System.cc
@@ -18,7 +18,7 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "utils/System.h"
+#include "prop/bvminisat/utils/System.h"
 
 #if defined(__linux__)
 
diff --git a/src/prop/bvminisat/utils/System.h b/src/prop/bvminisat/utils/System.h
index a065ef916..6a887bdb0 100644
--- a/src/prop/bvminisat/utils/System.h
+++ b/src/prop/bvminisat/utils/System.h
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <fpu_control.h>
 #endif
 
-#include "mtl/IntTypes.h"
+#include "prop/bvminisat/mtl/IntTypes.h"
 
 //-------------------------------------------------------------------------------------------------