Skip to content

Commit

Permalink
Fix more tests by handling missing cases
Browse files Browse the repository at this point in the history
  • Loading branch information
@hbierlee
hbierlee committed May 16, 2024
1 parent fb17fb2 commit ac57ced
Show file tree
Hide file tree
Showing 7 changed files with 269 additions and 91 deletions.
23 changes: 21 additions & 2 deletions crates/pindakaas/src/helpers.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ use std::{
use itertools::Itertools;

use crate::{
linear::PosCoeff, trace::emit_clause, CheckError, Checker, ClauseDatabase, Coeff, Encoder,
LinExp, Lit, Result, Unsatisfiable, Valuation, Var,
int::LitOrConst, linear::PosCoeff, trace::emit_clause, CheckError, Checker, ClauseDatabase,
Coeff, Encoder, LinExp, Lit, Result, Unsatisfiable, Valuation, Var,
};

#[allow(unused_macros)]
Expand Down Expand Up @@ -154,6 +154,25 @@ pub(crate) fn add_clauses_for<DB: ClauseDatabase>(
Ok(())
}

pub(crate) fn emit_filtered_clause<DB: ClauseDatabase, I: IntoIterator<Item = LitOrConst>>(
db: &mut DB,
lits: I,
) -> Result {
if let Ok(clause) = lits
.into_iter()
.filter_map(|lit| match lit {
LitOrConst::Lit(lit) => Some(Ok(lit)),
LitOrConst::Const(true) => Some(Err(())), // clause satisfied
LitOrConst::Const(false) => None, // literal falsified
})
.collect::<std::result::Result<Vec<_>, ()>>()
{
emit_clause!(db, clause)
} else {
Ok(())
}
}

/// Negates CNF (flipping between empty clause and formula)
pub(crate) fn negate_cnf(clauses: Vec<Vec<Lit>>) -> Vec<Vec<Lit>> {
if clauses.is_empty() {
Expand Down
52 changes: 51 additions & 1 deletion crates/pindakaas/src/int/bin.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@ use itertools::Itertools;

use super::{required_lits, Dom, LitOrConst};
use crate::{
helpers::{add_clauses_for, as_binary, negate_cnf, pow2, unsigned_binary_range},
helpers::{
add_clauses_for, as_binary, emit_filtered_clause, negate_cnf, pow2, unsigned_binary_range,
},
int::{helpers::remove_red, model::PRINT_COUPLING},
linear::{lex_geq_const, lex_leq_const, PosCoeff},
trace::{emit_clause, new_var},
Expand Down Expand Up @@ -42,6 +44,54 @@ impl BinEnc {
}
}

/// Encode x:B <=/>= y:B
pub(crate) fn lex<DB: ClauseDatabase>(
&self,
db: &mut DB,
cmp: Comparator,
other: Self,
) -> crate::Result {
let n = std::cmp::max(self.bits(), other.bits()) as usize;

fn bit(x: &[LitOrConst], i: usize) -> LitOrConst {
*x.get(i).unwrap_or(&LitOrConst::Const(false))
}

let (x, y, c) = (
&self.xs(),
&other.xs(),
&(0..n)
.map(|_i| LitOrConst::Lit(new_var!(db, crate::trace::subscripted_name("c", _i))))
.chain(std::iter::once(LitOrConst::Const(true)))
.collect_vec(),
);

// higher i -> more significant
for i in 0..n {
// c = all more significant bits are equal AND current one is
// if up to i is equal, all preceding must be equal
emit_filtered_clause(db, [!bit(c, i), bit(c, i + 1)])?;
// if up to i is equal, x<->y
emit_filtered_clause(db, [!bit(c, i), !bit(x, i), bit(y, i)])?;
emit_filtered_clause(db, [!bit(c, i), !bit(y, i), bit(x, i)])?;

// if not up to i is equal, either preceding bit was not equal, or x!=y
emit_filtered_clause(db, [bit(c, i), !bit(c, i + 1), bit(x, i), bit(y, i)])?;
emit_filtered_clause(db, [bit(c, i), !bit(c, i + 1), !bit(x, i), !bit(y, i)])?;

// if preceding bits are equal, then x<=y (or x>=y)
match cmp {
Comparator::LessEq => {
emit_filtered_clause(db, [!bit(c, i + 1), !bit(x, i), bit(y, i)])
}
Comparator::GreaterEq => {
emit_filtered_clause(db, [!bit(c, i + 1), bit(x, i), !bit(y, i)])
}
Comparator::Equal => unreachable!(),
}?;
}
Ok(())
}
/// Returns conjunction for x>=k, given x>=b
pub(crate) fn geqs(&self, k: Coeff, a: Coeff) -> Vec<Vec<Lit>> {
let (range_lb, range_ub) = self.range();
Expand Down
25 changes: 24 additions & 1 deletion crates/pindakaas/src/int/con.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ pub(crate) enum LinCase {
Couple(Term, Term),
Fixed(Lin),
Unary(Term, Comparator, Coeff),
Binary(Term, Comparator, Term), // just for binary ineqs
Scm(Term, IntVarRef),
Rca(Term, Term, Term),
Order,
Expand All @@ -57,6 +58,11 @@ impl TryFrom<&Lin> for LinCase {
{
LinCase::Unary((*t).clone().encode_bin(None, cmp, None)?, cmp, con.k)
}
(
[(x, Some(IntVarEnc::Bin(_))), (y, Some(IntVarEnc::Bin(_)))],
Comparator::LessEq | Comparator::GreaterEq,
0,
) => LinCase::Binary((*x).clone(), con.cmp, (*y).clone()),
// VIEW COUPLING
// TODO this makes single literal comparisons views if possible
// ([(t, Some(IntVarEnc::Ord(_))), (y, Some(IntVarEnc::Bin(None)))], _)
Expand All @@ -83,7 +89,14 @@ impl TryFrom<&Lin> for LinCase {
{
LinCase::Couple((*t).clone(), (*y).clone())
}

// ([(x, Some(IntVarEnc::Bin(_)))], Comparator::Equal, k) => {
// LinCase::Rca((*x).clone(), Term::from(0), Term::from(k))
// }
(
[(x, Some(IntVarEnc::Bin(_))), (y, Some(IntVarEnc::Bin(_)))],
Comparator::Equal,
k,
) => LinCase::Rca((*x).clone(), (*y).clone(), Term::from(-k)),
(
[(x, Some(IntVarEnc::Bin(_))), (y, Some(IntVarEnc::Bin(_))), (z, Some(IntVarEnc::Bin(_)))],
Comparator::Equal,
Expand Down Expand Up @@ -344,6 +357,16 @@ impl Lin {
let x_enc = x.clone().borrow_mut().encode_bin(db)?;
x_enc.encode_unary_constraint(db, &cmp, k, &dom, false)
}
LinCase::Binary(t_x, cmp, t_y) => {
println!("self = {}", self);

t_x.x.borrow_mut().encode_bin(db)?;
t_y.x.borrow_mut().encode_bin(db)?;

let x_enc = t_x.x.borrow_mut().encode_bin(db)?;
let y_enc = (t_y * -1).x.borrow_mut().encode_bin(db)?;
x_enc.lex(db, cmp, y_enc)
}
LinCase::Couple(t_x, t_y) => {
t_x.x.borrow_mut().encode_ord(db)?;
if !t_x.x.borrow().add_consistency {
Expand Down
75 changes: 60 additions & 15 deletions crates/pindakaas/src/int/decompose.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,14 @@ pub trait Decompose {
pub struct EqualizeTernsDecomposer {}

impl Decompose for EqualizeTernsDecomposer {
fn decompose(&self, model: Model) -> Result<Model, Unsatisfiable> {
const REMOVE_GAPS: bool = true;

fn decompose(&self, mut model: Model) -> Result<Model, Unsatisfiable> {
let cons = model.cons.iter().cloned().collect_vec();
Ok(Model {
cons: cons
.into_iter()
.map(|con| {
if REMOVE_GAPS && con.exp.terms.len() >= 2 && con.cmp.is_ineq() {
.with_position()
.flat_map(|(pos, con)| {
if con.exp.terms.len() >= 2 && con.cmp.is_ineq() {
if con
.exp
.terms
Expand All @@ -40,15 +39,51 @@ impl Decompose for EqualizeTernsDecomposer {
Comparator::GreaterEq => (std::cmp::max(-last.ub(), lb), ub),
Comparator::Equal => unreachable!(),
};
let dom = Dom::from_bounds(lb, ub);
if matches!(pos, Position::First | Position::Middle) {
last.x.borrow_mut().dom = dom;

last.x.borrow_mut().dom = Dom::from_bounds(lb, ub);
vec![Lin {
exp: LinExp {
terms: firsts.iter().chain([last]).cloned().collect(),
},
cmp: Comparator::Equal,
..con
}]
} else if con.exp.terms.len() >= 3 {
// x+y<=z == x+y=z' /\ z' <= z
let y = model
.new_aux_var(
dom,
true,
Some(IntVarEnc::Bin(None)),
Some(String::from("last")),
)
.unwrap();

Lin {
exp: LinExp {
terms: firsts.iter().chain([last]).cloned().collect(),
},
cmp: Comparator::Equal,
..con
vec![
Lin {
exp: LinExp {
terms: firsts
.iter()
.chain([&Term::new(-1, y.clone())])
.cloned()
.collect(),
},
cmp: Comparator::Equal,
k: 0,
lbl: Some(String::from("last")),
},
Lin {
exp: LinExp {
terms: vec![Term::from(y), last.clone()],
},
cmp: con.cmp,
..con
},
]
} else {
vec![con]
}
} else {
unreachable!()
Expand All @@ -67,12 +102,22 @@ impl Decompose for EqualizeTernsDecomposer {
) {
con.exp.terms[0].x.borrow_mut().dom =
con.exp.terms[1].x.borrow().dom.clone();
con
vec![con]
} else {
con
vec![con]
}
// } else if con.exp.terms.len() == 2 && con.cmp == Comparator::Equal && false {
// let z = con.exp.terms[0]
// .clone()
// .add(con.exp.terms[1].clone(), &mut model)
// .unwrap();
// vec![Lin {
// exp: LinExp { terms: vec![z] },
// cmp: con.cmp,
// ..con
// }]
} else {
con
vec![con]
}
})
.collect(),
Expand Down
Loading

0 comments on commit ac57ced

Please sign in to comment.