Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use polarity instead of negative for Lit's public API #54

Merged
merged 1 commit into from
May 17, 2019
Merged

Use polarity instead of negative for Lit's public API #54

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions manual/src/lib/formulas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion varisat-dimacs/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
));
}
}
Expand Down
24 changes: 12 additions & 12 deletions varisat-formula/src/lit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a nice ergonomic improvement, and a semver breaking change. The code like Lit::from_var(x, false) compiles before and after but means exactly opposite things.

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not semver breaking as I'm still on 0.x.y. Maybe I should add a more explicit warning that the API isn't stable yet. I will release a version 1.0 when I'm done tweaking the API.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

cargo disagrees with the semver spec about this:

This compatibility convention is different from SemVer in the way it treats versions before 1.0.0. While SemVer says there is no compatibility before 1.0.0, Cargo considers 0.x.y to be compatible with 0.x.z, where y ≥ z and x > 0.

So if you have a Cargo.toml that has varisat = "0.2" then you may get 0.2.0 or 0.2.1 as cargo consiters them semver compatible. Ether version will compile Lit::from_var(x, false) but do opposite things.

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I wasn't aware of that, I would have released this as 0.3.0 otherwise. Thanks for pointing out the details.

}

/// 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.
Expand All @@ -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),
}
}

Expand All @@ -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`.
Expand Down Expand Up @@ -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))
}
}
18 changes: 9 additions & 9 deletions varisat-formula/src/test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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() {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down
2 changes: 1 addition & 1 deletion varisat/src/cdcl.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
2 changes: 1 addition & 1 deletion varisat/src/decision.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
10 changes: 5 additions & 5 deletions varisat/src/prop.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
2 changes: 1 addition & 1 deletion varisat/src/solver.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
)
Expand Down