Merge #54

54: Use `polarity` instead of `negative` for Lit's public API r=jix a=jix This resolves #53 Co-authored-by: Jannis Harder <[email protected]>
jix · May 17, 2019 · 37b8e38 · 37b8e38
2 parents 5fe037a + 8027f13
commit 37b8e38
Show file tree

Hide file tree

Showing 8 changed files with 34 additions and 34 deletions.
diff --git a/manual/src/lib/formulas.md b/manual/src/lib/formulas.md
@@ -41,13 +41,13 @@ assert_eq!(x.to_dimacs(), 1);
 assert!(Lit::from_dimacs(2).is_positive());
 assert!(Lit::from_dimacs(-3).is_negative());
 
-assert_eq!(Lit::positive(x), Lit::from_var(x, false));
-assert_eq!(Lit::negative(x), Lit::from_var(x, true));
+assert_eq!(Lit::positive(x), Lit::from_var(x, true));
+assert_eq!(Lit::negative(x), Lit::from_var(x, false));
 
 assert_eq!(Lit::negative(x), !Lit::positive(x));
 
-assert_eq!(Lit::from_index(6, false).code(), 12);
-assert_eq!(Lit::from_index(6, true).code(), 13);
+assert_eq!(Lit::from_index(6, true).code(), 12);
+assert_eq!(Lit::from_index(6, false).code(), 13);
 
 assert_eq!(Lit::from_code(13).var(), Var::from_dimacs(7));
 assert_eq!(Lit::from_code(13).index(), 6);

diff --git a/varisat-dimacs/src/lib.rs b/varisat-dimacs/src/lib.rs
@@ -311,7 +311,7 @@ impl DimacsParser {
             } else {
                 self.partial_clause.push(Lit::from_var(
                     Var::from_dimacs(self.partial_lit as isize),
-                    self.negate_next_lit,
+                    !self.negate_next_lit,
                 ));
             }
         }

diff --git a/varisat-formula/src/lit.rs b/varisat-formula/src/lit.rs
@@ -99,25 +99,25 @@ pub struct Lit {
 }
 
 impl Lit {
-    /// Creates a literal from a `Var` and a `bool` that is `true` when the literal is negative.
-    pub fn from_var(var: Var, negative: bool) -> Lit {
-        Lit::from_litidx(var.index, negative)
+    /// Creates a literal from a `Var` and a `bool` that is `true` when the literal is positive.
+    pub fn from_var(var: Var, polarity: bool) -> Lit {
+        Lit::from_litidx(var.index, polarity)
     }
 
     /// Create a positive literal from a `Var`.
     pub fn positive(var: Var) -> Lit {
-        Lit::from_var(var, false)
+        Lit::from_var(var, true)
     }
 
     /// Create a negative literal from a `Var`.
     pub fn negative(var: Var) -> Lit {
-        Lit::from_var(var, true)
+        Lit::from_var(var, false)
     }
 
     /// Create a literal from a variable index and a `bool` that is `true` when the literal is
-    /// negative.
-    pub fn from_index(index: usize, negative: bool) -> Lit {
-        Lit::from_var(Var::from_index(index), negative)
+    /// positive.
+    pub fn from_index(index: usize, polarity: bool) -> Lit {
+        Lit::from_var(Var::from_index(index), polarity)
     }
 
     /// Create a literal with the given encoding.
@@ -128,10 +128,10 @@ impl Lit {
         }
     }
 
-    fn from_litidx(index: LitIdx, negative: bool) -> Lit {
+    fn from_litidx(index: LitIdx, polarity: bool) -> Lit {
         debug_assert!(index <= Var::max_var().index);
         Lit {
-            code: (index << 1) | (negative as LitIdx),
+            code: (index << 1) | (!polarity as LitIdx),
         }
     }
 
@@ -140,7 +140,7 @@ impl Lit {
     /// The absolute value is used as 1-based index, the sign of
     /// the integer is used as sign of the literal.
     pub fn from_dimacs(number: isize) -> Lit {
-        Lit::from_var(Var::from_dimacs(number.abs()), number < 0)
+        Lit::from_var(Var::from_dimacs(number.abs()), number > 0)
     }
 
     /// 1-based Integer representation of the literal, opposite of `from_dimacs`.
@@ -226,6 +226,6 @@ pub mod strategy {
     }
 
     pub fn lit(index: impl Strategy<Value = usize>) -> impl Strategy<Value = Lit> {
-        (var(index), bool::ANY).prop_map(|(var, negative)| Lit::from_var(var, negative))
+        (var(index), bool::ANY).prop_map(|(var, polarity)| Lit::from_var(var, polarity))
     }
 }
diff --git a/varisat-formula/src/test.rs b/varisat-formula/src/test.rs
@@ -13,12 +13,12 @@ pub fn sgen_unsat_formula(
     blocks: impl Strategy<Value = usize>,
 ) -> impl Strategy<Value = CnfFormula> {
     blocks.prop_flat_map(|blocks| {
-        collection::vec(bool::ANY, blocks * 4 + 1).prop_perturb(|negate, mut rng| {
+        collection::vec(bool::ANY, blocks * 4 + 1).prop_perturb(|polarity, mut rng| {
             let mut clauses: Vec<Vec<Lit>> = vec![];
-            let mut lits = negate
+            let mut lits = polarity
                 .into_iter()
                 .enumerate()
-                .map(|(index, negate)| Lit::from_index(index, negate))
+                .map(|(index, polarity)| Lit::from_index(index, polarity))
                 .collect::<Vec<_>>();
 
             for &invert in [false, true].iter() {
@@ -66,12 +66,12 @@ pub fn sat_formula(
             let density = Bernoulli::new(density);
             let polarity_dist = Bernoulli::new(polarity_dist);
 
-            collection::vec(bool::ANY, vars).prop_perturb(move |negate, mut rng| {
+            collection::vec(bool::ANY, vars).prop_perturb(move |polarity, mut rng| {
                 let mut clauses: Vec<Vec<Lit>> = vec![];
-                let lits = negate
+                let lits = polarity
                     .into_iter()
                     .enumerate()
-                    .map(|(index, negate)| Lit::from_index(index, negate))
+                    .map(|(index, polarity)| Lit::from_index(index, polarity))
                     .collect::<Vec<_>>();
 
                 for _ in 0..clause_count {
@@ -102,12 +102,12 @@ pub fn conditional_pigeon_hole(
         let rows = columns + extra_rows;
         let vars = (columns + 1) * rows;
 
-        collection::vec(bool::ANY, vars).prop_perturb(move |negate, mut rng| {
+        collection::vec(bool::ANY, vars).prop_perturb(move |polarity, mut rng| {
             let mut clauses: Vec<Vec<Lit>> = vec![];
-            let lits = negate
+            let lits = polarity
                 .into_iter()
                 .enumerate()
-                .map(|(index, negate)| Lit::from_index(index, negate))
+                .map(|(index, polarity)| Lit::from_index(index, polarity))
                 .collect::<Vec<_>>();
 
             for i in 1..columns + 1 {

diff --git a/varisat/src/cdcl.rs b/varisat/src/cdcl.rs
@@ -49,7 +49,7 @@ pub fn conflict_step<'a>(
                         .iter()
                         .enumerate()
                         .flat_map(|(index, assignment)| {
-                            assignment.map(|polarity| Lit::from_index(index, !polarity))
+                            assignment.map(|polarity| Lit::from_index(index, polarity))
                         }),
                 );
                 proof::add_step(ctx.borrow(), &ProofStep::Model(&model));

diff --git a/varisat/src/decision.rs b/varisat/src/decision.rs
@@ -29,7 +29,7 @@ pub fn make_decision(
     {
         let decision = Lit::from_var(
             decision_var,
-            !ctx.part(AssignmentP).last_var_value(decision_var),
+            ctx.part(AssignmentP).last_var_value(decision_var),
         );
 
         ctx.part_mut(TrailP).new_decision_level();

diff --git a/varisat/src/prop.rs b/varisat/src/prop.rs
@@ -70,16 +70,16 @@ mod tests {
     ) -> impl Strategy<Value = (Vec<Lit>, CnfFormula)> {
         (vars, extra_vars, extra_clauses, density).prop_flat_map(
             |(vars, extra_vars, extra_clauses, density)| {
-                let negate = collection::vec(bool::ANY, vars + extra_vars);
+                let polarity = collection::vec(bool::ANY, vars + extra_vars);
 
                 let dist = Bernoulli::new(density);
 
-                let lits = negate
-                    .prop_map(|negate| {
-                        negate
+                let lits = polarity
+                    .prop_map(|polarity| {
+                        polarity
                             .into_iter()
                             .enumerate()
-                            .map(|(index, negate)| Lit::from_index(index, negate))
+                            .map(|(index, polarity)| Lit::from_index(index, polarity))
                             .collect::<Vec<_>>()
                     })
                     .prop_shuffle();

diff --git a/varisat/src/solver.rs b/varisat/src/solver.rs
@@ -170,7 +170,7 @@ impl<'a> Solver<'a> {
                     .iter()
                     .enumerate()
                     .flat_map(|(index, assignment)| {
-                        assignment.map(|polarity| Lit::from_index(index, !polarity))
+                        assignment.map(|polarity| Lit::from_index(index, polarity))
                     })
                     .collect(),
             )