Use more types of constraints in fuzzer (#212)

* test more constraints in Fuzzer

* fix normalize_extension_supports

Author: semiexp

cspuz_core/src/integration/tests/fuzz.rs

@@ -1,5 +1,6 @@
 use super::IntegrationTester;
 use crate::arithmetic::CmpOp;
+use crate::csp::Stmt;
 use crate::integration::*;
 
 struct Fuzzer {
@@ -69,13 +70,13 @@ impl Fuzzer {
             }
         }
 
-        let mut exprs = vec![];
+        let mut stmt_descs = vec![];
         for _ in 0..num_exprs {
-            let complexity = self.next_u32(max_complexity);
-
-            let expr = self.random_bool_expr(&bool_vars, &int_vars, complexity);
-            exprs.push(expr.clone());
-            tester.add_expr(expr);
+            let stmt = self.random_stmt(&bool_vars, &int_vars, max_complexity);
+            let mut buf = vec![];
+            let _ = stmt.pretty_print(&mut buf);
+            stmt_descs.push(String::from_utf8(buf).unwrap_or_default());
+            tester.add_constraint(stmt);
         }
 
         if !tester.check_internal(true) {
@@ -85,18 +86,124 @@ impl Fuzzer {
             for desc in &int_var_descs {
                 eprintln!("- {}", desc);
             }
-            eprintln!("Expressions:");
-            for expr in exprs {
-                eprint!("- ");
-                let mut out_buf = vec![];
-                let _ = expr.pretty_print(&mut out_buf);
-                eprint!("{}", String::from_utf8(out_buf).unwrap());
-                eprintln!();
+            eprintln!("Statements:");
+            for desc in &stmt_descs {
+                eprintln!("- {}", desc);
             }
             panic!();
         }
     }
 
+    fn random_stmt(
+        &mut self,
+        bool_vars: &[BoolVar],
+        int_vars: &[IntVar],
+        max_complexity: u32,
+    ) -> Stmt {
+        // Weights: 0,1 = AllDifferent, 2 = ActiveVerticesConnected,
+        // 3 (feature-gated) = ExtensionSupports, rest = BoolExpr
+        #[cfg(feature = "csp-extra-constraints")]
+        let mode = self.next_u32(11);
+        #[cfg(not(feature = "csp-extra-constraints"))]
+        let mode = self.next_u32(10);
+
+        match mode {
+            0 | 1 => self.random_alldifferent_stmt(bool_vars, int_vars, max_complexity),
+            2 => self.random_active_vertices_connected_stmt(bool_vars, int_vars, max_complexity),
+            #[cfg(feature = "csp-extra-constraints")]
+            3 => self.random_extension_supports_stmt(bool_vars, int_vars),
+            _ => {
+                let complexity = self.next_u32(max_complexity);
+                Stmt::Expr(self.random_bool_expr(bool_vars, int_vars, complexity))
+            }
+        }
+    }
+
+    fn random_alldifferent_stmt(
+        &mut self,
+        bool_vars: &[BoolVar],
+        int_vars: &[IntVar],
+        max_complexity: u32,
+    ) -> Stmt {
+        if int_vars.is_empty() {
+            let complexity = self.next_u32(max_complexity);
+            return Stmt::Expr(self.random_bool_expr(bool_vars, int_vars, complexity));
+        }
+        // 2 to 5 expressions
+        let n = (self.next_u32(4) as usize + 2).min(5);
+        let exprs: Vec<IntExpr> = (0..n)
+            .map(|_| {
+                let c = self.next_u32(max_complexity / 2 + 1);
+                self.random_int_expr(bool_vars, int_vars, c)
+            })
+            .collect();
+        Stmt::AllDifferent(exprs)
+    }
+
+    fn random_active_vertices_connected_stmt(
+        &mut self,
+        bool_vars: &[BoolVar],
+        int_vars: &[IntVar],
+        max_complexity: u32,
+    ) -> Stmt {
+        if bool_vars.is_empty() {
+            let complexity = self.next_u32(max_complexity);
+            return Stmt::Expr(self.random_bool_expr(bool_vars, int_vars, complexity));
+        }
+        // 2 to 6 vertices
+        let n = (self.next_u32(5) as usize + 2).min(bool_vars.len()).max(2);
+        let vertex_exprs: Vec<BoolExpr> = (0..n)
+            .map(|_| {
+                let c = self.next_u32(max_complexity / 2 + 1);
+                self.random_bool_expr(bool_vars, int_vars, c)
+            })
+            .collect();
+        let mut edges = vec![];
+        for i in 0..n {
+            for j in (i + 1)..n {
+                if self.next_u32(3) != 0 {
+                    edges.push((i, j));
+                }
+            }
+        }
+        Stmt::ActiveVerticesConnected(vertex_exprs, edges)
+    }
+
+    #[cfg(feature = "csp-extra-constraints")]
+    fn random_extension_supports_stmt(
+        &mut self,
+        _bool_vars: &[BoolVar],
+        int_vars: &[IntVar],
+    ) -> Stmt {
+        if int_vars.is_empty() {
+            return Stmt::Expr(BoolExpr::Const(true));
+        }
+        // 1 to 3 variables in the scope
+        let n = (self.next_u32(3) as usize + 1).min(int_vars.len());
+        let exprs: Vec<IntExpr> = (0..n)
+            .map(|_| {
+                let idx = self.next_u32(int_vars.len() as u32) as usize;
+                int_vars[idx].expr()
+            })
+            .collect();
+        // 1 to 6 support tuples; values in -3..=3 to match int var domains
+        let n_tuples = self.next_u32(6) as usize + 1;
+        let mut supports = vec![];
+        for _ in 0..n_tuples {
+            let tuple: Vec<Option<i32>> = (0..n)
+                .map(|_| {
+                    if self.next_u32(5) == 0 {
+                        None // wildcard
+                    } else {
+                        Some(self.next_i32(-3, 4))
+                    }
+                })
+                .collect();
+            supports.push(tuple);
+        }
+        Stmt::ExtensionSupports(exprs, supports)
+    }
+
     fn random_bool_expr(
         &mut self,
         bool_vars: &[BoolVar],
@@ -173,7 +280,11 @@ impl Fuzzer {
             }
         }
 
+        #[cfg(feature = "csp-extra-constraints")]
+        let mode = self.next_u32(5);
+        #[cfg(not(feature = "csp-extra-constraints"))]
         let mode = self.next_u32(4);
+
         match mode {
             0 => {
                 let cond_complexity = self.next_u32(complexity);
@@ -210,6 +321,16 @@ impl Fuzzer {
 
                 IntExpr::Linear(vec![(t1, scale1), (t2, scale2)])
             }
+            #[cfg(feature = "csp-extra-constraints")]
+            4 => {
+                let left_complexity = self.next_u32(complexity);
+                let right_complexity = complexity - left_complexity - 1;
+
+                let lhs = Box::new(self.random_int_expr(bool_vars, int_vars, left_complexity));
+                let rhs = Box::new(self.random_int_expr(bool_vars, int_vars, right_complexity));
+
+                IntExpr::Mul(lhs, rhs)
+            }
             _ => unreachable!(),
         }
     }

cspuz_core/src/normalizer.rs

@@ -1054,6 +1054,12 @@ fn normalize_extension_supports(
         }
     }
 
+    if supports_idx.is_empty() {
+        // No support tuple is compatible with the variable domains: constraint is UNSAT
+        env.norm.add_constraint(Constraint::new());
+        return;
+    }
+
     for n_prefix in 0..vars.len() {
         let mut left = 0;
         while left < supports_idx.len() {
@@ -1532,6 +1538,23 @@ mod tests {
         }
     }
 
+    #[cfg(feature = "csp-extra-constraints")]
+    #[test]
+    fn test_normalization_extension_supports_3() {
+        for use_native in [false, true] {
+            let mut tester = NormalizerTester::new();
+            tester.config.use_native_extension_supports = use_native;
+
+            let a = tester.new_int_var(Domain::range(0, 3));
+            let b = tester.new_int_var(Domain::range(0, 3));
+            tester.add_constraint(Stmt::ExtensionSupports(
+                vec![a.expr(), b.expr()],
+                vec![vec![Some(4), Some(-1)]],
+            ));
+            tester.check();
+        }
+    }
+
     #[cfg(feature = "csp-extra-constraints")]
     #[test]
     fn test_normalization_circuit_1() {