disable syrup on windows (need to make it work on unix though...)

Author: QuentinJanuel

src/solver/glucose/mod.rs

@@ -25,19 +25,28 @@ use super::config::Config;
 /// The Glucose solver
 pub struct Glucose {
     preprocessing: bool,
+    syrup: bool,
 }
 
 impl Glucose {
     pub fn new() -> Self {
         Glucose {
             preprocessing: false,
+            syrup: false,
         }
     }
     pub fn enable_preprocessing(&mut self) {
         self.preprocessing = true;
     }
 }
 
+#[cfg(not(target_os = "windows"))]
+impl Glucose {
+    pub fn enable_syrup(&mut self) {
+        self.syrup = true;
+    }
+}
+
 impl Solver for Glucose {
     fn solve_with_config(
         &self,
@@ -49,7 +58,7 @@ impl Solver for Glucose {
         unsafe {
             let ptr = bindings::glucose_new(
                 self.preprocessing as i32,
-                true as i32,
+                self.syrup as i32,
             );
             let mut m_vars: HashMap<Var, i32> = HashMap::new();
             for clause in cnf.get_clauses() {

src/tests/mod.rs

@@ -15,32 +15,40 @@ fn test_solver<S: Solver>(solver: S) {
     ];
     let models = solver.get_all_models(&mut cnf.clone());
     assert_eq!(models.len(), 2);
-    // let cnf = cnf![
-    //     1;
-    //     -1
-    // ];
-    // assert!(solver.solve(&cnf).is_none());
+    let cnf = cnf![
+        1;
+        -1
+    ];
+    assert!(solver.solve(&cnf).is_none());
 }
 
 #[test]
 fn test_solvers() {
-    // test_solver(DPLL::new());
-    // test_solver(Minisat::new());
-    // test_solver(Manysat::new());
-    // test_solver(portfolio![
-    //     DPLL::new(),
-    //     Minisat::new(),
-    //     Manysat::new(),
-    // ]);
-    // test_solver(portfolio![Manysat::new()]);
+    test_solver(DPLL::new());
+    test_solver(Minisat::new());
+    test_solver(Manysat::new());
+    test_solver(portfolio![
+        DPLL::new(),
+        Minisat::new(),
+        Manysat::new(),
+    ]);
+    test_solver(portfolio![Manysat::new()]);
     test_solver(Glucose::new());
-    // test_solver({
-    //     let mut s = Glucose::new();
-    //     s.enable_preprocessing();
-    //     s
-    // });
-    // test_solver(portfolio![
-    //     Glucose::new(),
-    //     DPLL::new(),
-    // ]);
+    test_solver({
+        let mut s = Glucose::new();
+        s.enable_preprocessing();
+        s
+    });
+    {
+        #[cfg(not(target_os = "windows"))]
+        test_solver({
+            let mut s = Glucose::new();
+            s.enable_syrup();
+            s
+        });
+    }
+    test_solver(portfolio![
+        Glucose::new(),
+        DPLL::new(),
+    ]);
 }