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 46451d4640e22d5f86ed34a0172de72acdb30bcd..c94f473a93a131e0fdb364a1c0fae99ddba4075d 100644 (file)
--- 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 74cc9cde835c7e32098b36d3c8c7e70ea0ea342f..307a4d7d9544de9bf569b29f81ea6d37ec0296f6 100644 (file)
--- 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 740c2e5e675b6f008d0a3fb864a3e0925cb53afd..372f8eb04245f7c5b7ce5e99001951211184ddfb 100644 (file)
--- 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 f668aa8560c67cd327f1cdf03c451908a1923d60..f4a10aabb1b72c1df9ef07f8f7eb116e0dc813eb 100644 (file)
--- 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 96e318e5f8dd0232ac3a653c5de4bf7b8c1644f1..481ed3f39b67091834c7e09a1a0261bda2e2e5f5 100644 (file)
--- 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 cb5929320afbe8766278f737d2c71eddc4951b64..2fa8d472da36593a871b5b8a30c8a3ebdd2f7a8f 100644 (file)
--- 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 b2094d466dec9f83f6ded1c1250c737f7cb1ed68..ac09646230655bc5e2c63797bf860c3b84454416 100644 (file)
--- 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 dab33af3ee30132dd2e49d87663a964a772e302e..aba0a5ac5a7792107cdbe6bae9a4536db2ccf4a1 100644 (file)
--- 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 a065ef91687e25525ddd038e0f654b2e60c5ece7..6a887bdb0778dc966baadd4fa7c50c6d75a4d712 100644 (file)
--- 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"
 
 //-------------------------------------------------------------------------------------------------