diff options
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 15 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 7 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 6 |
3 files changed, 15 insertions, 13 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index ca7228ee8..5a37da27c 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -18,19 +18,20 @@ 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 <math.h> -#include "mtl/Sort.h" -#include "core/Solver.h" #include <vector> #include <iostream> -#include "util/output.h" -#include "util/utility.h" -#include "util/exception.h" -#include "theory/bv/options.h" -#include "smt/options.h" +#include "base/exception.h" +#include "base/output.h" +#include "mtl/Sort.h" +#include "options/bv_options.h" +#include "options/smt_options.h" #include "theory/interrupted.h" +#include "util/utility.h" namespace CVC4 { namespace BVMinisat { diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index e7e489985..c5b185c95 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -18,11 +18,12 @@ 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 "simp/SimpSolver.h" + +#include "mtl/Sort.h" +#include "options/bv_options.h" +#include "options/smt_options.h" #include "utils/System.h" -#include "theory/bv/options.h" -#include "smt/options.h" namespace CVC4 { namespace BVMinisat { diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 707f62e34..bef8e0a70 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -21,10 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_SimpSolver_h #define BVMinisat_SimpSolver_h -#include "prop/bvminisat/mtl/Queue.h" -#include "prop/bvminisat/core/Solver.h" -#include "util/statistics_registry.h" #include "context/context.h" +#include "expr/statistics_registry.h" +#include "prop/bvminisat/core/Solver.h" +#include "prop/bvminisat/mtl/Queue.h" namespace CVC4 { namespace BVMinisat { |