diff --git a/Cargo.lock b/Cargo.lock index b80b5ae7..3e5bcd16 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -38,47 +38,48 @@ checksum = "5c6cb57a04249c6480766f7f7cef5467412af1490f8d1e243141daddada3264f" [[package]] name = "anstream" -version = "0.6.13" +version = "0.6.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d96bd03f33fe50a863e394ee9718a706f988b9079b20c3784fb726e7678b62fb" +checksum = "418c75fa768af9c03be99d17643f93f79bbba589895012a80e3452a19ddda15b" dependencies = [ "anstyle", "anstyle-parse", "anstyle-query", "anstyle-wincon", "colorchoice", + "is_terminal_polyfill", "utf8parse", ] [[package]] name = "anstyle" -version = "1.0.6" +version = "1.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8901269c6307e8d93993578286ac0edf7f195079ffff5ebdeea6a59ffb7e36bc" +checksum = "038dfcf04a5feb68e9c60b21c9625a54c2c0616e79b72b0fd87075a056ae1d1b" [[package]] name = "anstyle-parse" -version = "0.2.3" +version = "0.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c75ac65da39e5fe5ab759307499ddad880d724eed2f6ce5b5e8a26f4f387928c" +checksum = "c03a11a9034d92058ceb6ee011ce58af4a9bf61491aa7e1e59ecd24bd40d22d4" dependencies = [ "utf8parse", ] [[package]] name = "anstyle-query" -version = "1.0.2" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e28923312444cdd728e4738b3f9c9cac739500909bb3d3c94b43551b16517648" +checksum = "a64c907d4e79225ac72e2a354c9ce84d50ebb4586dee56c82b3ee73004f537f5" dependencies = [ "windows-sys 0.52.0", ] [[package]] name = "anstyle-wincon" -version = "3.0.2" +version = "3.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7" +checksum = "61a38449feb7068f52bb06c12759005cf459ee52bb4adc1d5a7c4322d716fb19" dependencies = [ "anstyle", "windows-sys 0.52.0", @@ -86,9 +87,9 @@ dependencies = [ [[package]] name = "autocfg" -version = "1.2.0" +version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1fdabc7756949593fe60f30ec81974b613357de856987752631dea1e3394c80" +checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" [[package]] name = "backtrace" @@ -161,9 +162,9 @@ checksum = "ade8366b8bd5ba243f0a58f036cc0ca8a2f069cff1a2351ef1cac6b083e16fc0" [[package]] name = "cc" -version = "1.0.95" +version = "1.0.97" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d32a725bc159af97c3e629873bb9f88fb8cf8a4867175f76dc987815ea07c83b" +checksum = "099a5357d84c4c61eb35fc8eafa9a79a902c2f76911e5747ced4e032edd8d9b4" dependencies = [ "jobserver", "libc", @@ -218,9 +219,9 @@ checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce" [[package]] name = "colorchoice" -version = "1.0.0" +version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" +checksum = "0b6a852b24ab71dffc585bcb46eaf7959d175cb865a7152e35b348d1b2960422" [[package]] name = "darling" @@ -428,6 +429,12 @@ version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7655c9839580ee829dfacba1d1278c2b7883e50a277ff7541299489d6bdfdc45" +[[package]] +name = "is_terminal_polyfill" +version = "1.70.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8478577c03552c21db0e2724ffb8986a5ce7af88107e6be5d2ee6e158c12800" + [[package]] name = "iset" version = "0.2.2" @@ -623,7 +630,7 @@ checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" [[package]] name = "pindakaas" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#03599e7302ee6d101edc73edfc54fabc2fa89c6b" +source = "git+https://github.com/pindakaashq/pindakaas.git#d5c43e12c5f46a64fbc7a041c8e57e356d97c665" dependencies = [ "cached", "iset", @@ -637,7 +644,7 @@ dependencies = [ [[package]] name = "pindakaas-build-macros" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#03599e7302ee6d101edc73edfc54fabc2fa89c6b" +source = "git+https://github.com/pindakaashq/pindakaas.git#d5c43e12c5f46a64fbc7a041c8e57e356d97c665" dependencies = [ "cc", "paste", @@ -646,7 +653,7 @@ dependencies = [ [[package]] name = "pindakaas-cadical" version = "1.9.5" -source = "git+https://github.com/pindakaashq/pindakaas.git#03599e7302ee6d101edc73edfc54fabc2fa89c6b" +source = "git+https://github.com/pindakaashq/pindakaas.git#d5c43e12c5f46a64fbc7a041c8e57e356d97c665" dependencies = [ "cc", "pindakaas-build-macros", @@ -655,7 +662,7 @@ dependencies = [ [[package]] name = "pindakaas-derive" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#03599e7302ee6d101edc73edfc54fabc2fa89c6b" +source = "git+https://github.com/pindakaashq/pindakaas.git#d5c43e12c5f46a64fbc7a041c8e57e356d97c665" dependencies = [ "darling 0.20.8", "quote", @@ -728,18 +735,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -version = "1.0.199" +version = "1.0.200" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c9f6e76df036c77cd94996771fb40db98187f096dd0b9af39c6c6e452ba966a" +checksum = "ddc6f9cc94d67c0e21aaf7eda3a010fd3af78ebf6e096aa6e2e13c79749cce4f" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.199" +version = "1.0.200" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "11bd257a6541e141e42ca6d24ae26f7714887b47e89aa739099104c7e4d3b7fc" +checksum = "856f046b9400cee3c8c94ed572ecdb752444c24528c035cd35882aad6f492bcb" dependencies = [ "proc-macro2", "quote", @@ -1159,18 +1166,18 @@ checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0" [[package]] name = "zerocopy" -version = "0.7.32" +version = "0.7.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "74d4d3961e53fa4c9a25a8637fc2bfaf2595b3d3ae34875568a5cf64787716be" +checksum = "087eca3c1eaf8c47b94d02790dd086cd594b912d2043d4de4bfdd466b3befb7c" dependencies = [ "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.7.32" +version = "0.7.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6" +checksum = "6f4b6c273f496d8fd4eaf18853e6b448760225dc030ff2c485a786859aea6393" dependencies = [ "proc-macro2", "quote", diff --git a/crates/fzn-huub/src/main.rs b/crates/fzn-huub/src/main.rs index 1ba05552..bc8513e4 100644 --- a/crates/fzn-huub/src/main.rs +++ b/crates/fzn-huub/src/main.rs @@ -14,7 +14,9 @@ use std::{ use ::tracing::Level; use clap::Parser; use flatzinc_serde::{FlatZinc, Literal}; -use huub::{SlvTermSignal, SolveResult, Solver, SolverView, Valuation}; +use huub::{ + FlatZincError, ReformulationError, SlvTermSignal, SolveResult, Solver, SolverView, Valuation, +}; use miette::{IntoDiagnostic, Result, WrapErr}; use tracing::{FmtLitFields, LitName}; use tracing_subscriber::fmt::time::uptime; @@ -67,10 +69,20 @@ fn main() -> Result<()> { })?; // Convert FlatZinc model to internal Solver representation - let (mut slv, var_map): (Solver, _) = Solver::from_fzn(&fzn) - .into_diagnostic() - .wrap_err("Error while processing FlatZinc")?; - let var_map: UstrMap = var_map.into_iter().collect(); + let res = Solver::from_fzn(&fzn); + // Resolve any errors that may have occurred during the conversion + let (mut slv, var_map): (Solver, UstrMap) = match res { + Err(FlatZincError::ReformulationError(ReformulationError::TrivialUnsatisfiable)) => { + println!("=====UNSATISFIABLE====="); + return Ok(()); + } + Err(err) => { + return Err(err) + .into_diagnostic() + .wrap_err("Error while processing FlatZinc") + } + Ok((slv, var_map)) => (slv, var_map.into_iter().collect()), + }; // Create reverse map for solver variables if required if args.verbose > 0 { @@ -114,7 +126,7 @@ fn main() -> Result<()> { for ident in &fzn.output { if let Some(arr) = fzn.arrays.get(ident) { println!( - "{ident} = [{}]", + "{ident} = [{}];", arr.contents .iter() .map(|lit| print_lit(value, &var_map, lit)) @@ -122,7 +134,7 @@ fn main() -> Result<()> { .join(",") ) } else { - println!("{ident} = {}", value(var_map[ident]).unwrap()) + println!("{ident} = {};", value(var_map[ident]).unwrap()) } } println!("----------"); diff --git a/crates/huub/src/lib.rs b/crates/huub/src/lib.rs index 19ec63fc..82a99d94 100644 --- a/crates/huub/src/lib.rs +++ b/crates/huub/src/lib.rs @@ -2,7 +2,10 @@ pub(crate) mod model; pub(crate) mod propagator; pub(crate) mod solver; -pub use model::{Constraint, Model, Variable}; +pub use model::{ + bool::BoolExpr, flatzinc::FlatZincError, int::IntExpr, reformulate::ReformulationError, + Constraint, Model, Variable, +}; pub use pindakaas::solver::{SlvTermSignal, SolveResult}; use pindakaas::Lit as RawLit; pub use solver::{ @@ -19,7 +22,7 @@ type Conjunction = Vec; #[cfg(test)] mod tests { - use crate::{Constraint, Model, SolveResult, Solver, Variable}; + use crate::{BoolExpr, Model, SolveResult, Solver, Variable}; #[test] fn it_works() { @@ -27,10 +30,10 @@ mod tests { let a = prb.new_bool_var(); let b = prb.new_bool_var(); - prb += Constraint::Clause(vec![(!a).into(), (!b).into()]); - prb += Constraint::Clause(vec![a.into(), b.into()]); + prb += BoolExpr::Or(vec![(!a).into(), (!b).into()]); + prb += BoolExpr::Or(vec![a.into(), b.into()]); - let (mut slv, map): (Solver, _) = prb.to_solver(); + let (mut slv, map): (Solver, _) = prb.to_solver().unwrap(); let a = map.get(&Variable::Bool(a)); let b = map.get(&Variable::Bool(b)); diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs index 5204af2c..77acaf38 100644 --- a/crates/huub/src/model.rs +++ b/crates/huub/src/model.rs @@ -1,7 +1,7 @@ -mod bool; -mod flatzinc; -mod int; -mod reformulate; +pub(crate) mod bool; +pub(crate) mod flatzinc; +pub(crate) mod int; +pub(crate) mod reformulate; use std::ops::AddAssign; @@ -9,22 +9,19 @@ use flatzinc_serde::RangeList; use itertools::Itertools; use pindakaas::{ solver::{PropagatorAccess, Solver as SolverTrait}, - ClauseDatabase, Cnf, Lit as RawLit, Valuation as SatValuation, Var as RawVar, + ClauseDatabase, Cnf, ConditionalDatabase, Lit as RawLit, Valuation as SatValuation, + Var as RawVar, }; use self::{ bool::{BoolExpr, BoolVar}, int::{IntExpr, IntVar}, - reformulate::VariableMap, + reformulate::{ReformulationError, VariableMap}, }; use crate::{ model::{int::IntVarDef, reformulate::ReifContext}, propagator::{all_different::AllDifferentValue, int_lin_le::LinearLE}, - solver::{ - engine::int_var::IntVar as SlvIntVar, - view::{BoolViewInner, SolverView}, - SatSolver, - }, + solver::{engine::int_var::IntVar as SlvIntVar, view::SolverView, SatSolver}, IntVal, Solver, }; @@ -46,13 +43,12 @@ impl Model { iv } - // TODO: Make generic on Solver again (need var range trait) pub fn to_solver< Sol: PropagatorAccess + SatValuation, Sat: SatSolver + SolverTrait, >( &self, - ) -> (Solver, VariableMap) { + ) -> Result<(Solver, VariableMap), ReformulationError> { let mut map = VariableMap::default(); // TODO: run SAT simplification @@ -70,10 +66,10 @@ impl Model { // Create constraint data structures within the solve for c in self.constraints.iter() { - c.to_solver(&mut slv, &mut map) + c.to_solver(&mut slv, &mut map)?; } - (slv, map) + Ok((slv, map)) } } @@ -82,20 +78,30 @@ impl AddAssign for Model { self.constraints.push(rhs) } } +impl AddAssign for Model { + fn add_assign(&mut self, rhs: BoolExpr) { + self.constraints.push(Constraint::SimpleBool(rhs)) + } +} impl ClauseDatabase for Model { fn new_var(&mut self) -> RawVar { self.cnf.new_var() } - fn add_clause>(&mut self, cl: I) -> pindakaas::Result { + fn add_clause>(&mut self, cl: I) -> pindakaas::Result { self.cnf.add_clause(cl) } + + type CondDB = Model; + fn with_conditions(&mut self, conditions: Vec) -> ConditionalDatabase { + ConditionalDatabase::new(self, conditions) + } } #[derive(Debug, PartialEq, Eq, Hash)] pub enum Constraint { - Clause(Vec), + SimpleBool(BoolExpr), AllDifferent(Vec), IntLinLessEq(Vec, Vec, IntVal), IntLinEq(Vec, Vec, IntVal), @@ -109,28 +115,16 @@ impl Constraint { &self, slv: &mut Solver, map: &mut VariableMap, - ) { - struct Satisfied; + ) -> Result<(), ReformulationError> { match self { - Constraint::Clause(v) => { - let lits: Result, Satisfied> = v - .iter() - .filter_map(|x| match x.to_arg(ReifContext::Pos, slv, map).0 { - BoolViewInner::Lit(l) => Some(Ok(l)), - BoolViewInner::Const(true) => Some(Err(Satisfied)), - BoolViewInner::Const(false) => None, - }) - .collect(); - if let Ok(lits) = lits { - let _ = slv.oracle.add_clause(lits); - } - } + Constraint::SimpleBool(exp) => exp.constrain(slv, map), Constraint::AllDifferent(v) => { let vars: Vec<_> = v .iter() .map(|v| v.to_arg(ReifContext::Mixed, slv, map)) .collect(); slv.add_propagator(AllDifferentValue::new(vars)); + Ok(()) } Constraint::IntLinLessEq(coeffs, vars, c) => { let vars: Vec<_> = vars @@ -149,6 +143,7 @@ impl Constraint { }) .collect(); slv.add_propagator(LinearLE::new(coeffs, vars, *c)); + Ok(()) } Constraint::IntLinEq(coeffs, vars, c) => { let vars: Vec<_> = vars @@ -162,7 +157,8 @@ impl Constraint { &coeffs.iter().map(|c| -c).collect_vec(), vars, -c, - )) + )); + Ok(()) } } } diff --git a/crates/huub/src/model/bool.rs b/crates/huub/src/model/bool.rs index 6b91a6ac..36bcda5f 100644 --- a/crates/huub/src/model/bool.rs +++ b/crates/huub/src/model/bool.rs @@ -6,10 +6,10 @@ use std::{ use pindakaas::{ solver::{PropagatorAccess, Solver as SolverTrait}, - Lit as RawLit, Valuation as SatValuation, Var as RawVar, + Formula, Lit as RawLit, TseitinEncoder, Valuation as SatValuation, Var as RawVar, }; -use super::reformulate::{ReifContext, VariableMap}; +use super::reformulate::{ReformulationError, ReifContext, VariableMap}; use crate::{ solver::{ view::{BoolView, BoolViewInner}, @@ -20,12 +20,162 @@ use crate::{ #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum BoolExpr { - Not(Box), - Lit(Literal), Val(bool), + Lit(Literal), + Not(Box), + Or(Vec), + And(Vec), + Implies(Box, Box), + Equiv(Vec), + Xor(Vec), + IfThenElse { + cond: Box, + then: Box, + els: Box, + }, } impl BoolExpr { + pub(crate) fn constrain< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( + &self, + slv: &mut Solver, + map: &mut VariableMap, + ) -> Result<(), ReformulationError> { + match self { + BoolExpr::Val(false) => Err(ReformulationError::TrivialUnsatisfiable), + BoolExpr::Val(true) => Ok(()), + BoolExpr::Lit(l) => { + let v = map.get_lit(l); + match v.0 { + BoolViewInner::Const(true) => Ok(()), + BoolViewInner::Const(false) => Err(ReformulationError::TrivialUnsatisfiable), + BoolViewInner::Lit(l) => slv + .oracle + .add_clause([l]) + .map_err(|_| ReformulationError::TrivialUnsatisfiable), + } + } + BoolExpr::Not(x) => (!*x.clone()).constrain(slv, map), + BoolExpr::Or(es) => { + let mut lits = Vec::with_capacity(es.len()); + for e in es { + match e.to_arg(ReifContext::Pos, slv, map, None)?.0 { + BoolViewInner::Const(false) => {} + BoolViewInner::Const(true) => return Ok(()), + BoolViewInner::Lit(l) => lits.push(l), + } + } + slv.oracle + .add_clause(lits) + .map_err(|_| ReformulationError::TrivialUnsatisfiable) + } + BoolExpr::And(es) => { + for e in es { + match e.to_arg(ReifContext::Pos, slv, map, None)?.0 { + BoolViewInner::Const(false) => { + return Err(ReformulationError::TrivialUnsatisfiable) + } + BoolViewInner::Const(true) => {} + BoolViewInner::Lit(l) => slv + .oracle + .add_clause([l]) + .map_err(|_| ReformulationError::TrivialUnsatisfiable)?, + } + } + Ok(()) + } + BoolExpr::Implies(a, b) => { + let a = match a.to_arg(ReifContext::Neg, slv, map, None)?.0 { + BoolViewInner::Const(true) => { + return b.constrain(slv, map); + } + BoolViewInner::Const(false) => { + return Ok(()); + } + BoolViewInner::Lit(l) => l, + }; + + // TODO: Conditional Compilation + match b.to_arg(ReifContext::Pos, slv, map, None)?.0 { + BoolViewInner::Const(true) => Ok(()), + BoolViewInner::Const(false) => slv + .oracle + .add_clause([!a]) + .map_err(|_| ReformulationError::TrivialUnsatisfiable), + BoolViewInner::Lit(b) => slv + .oracle + .add_clause([!a, b]) + .map_err(|_| ReformulationError::TrivialUnsatisfiable), + } + } + BoolExpr::Equiv(es) => { + let mut lits = Vec::with_capacity(es.len()); + let mut res = None; + for e in es { + match e.to_arg(ReifContext::Mixed, slv, map, None)?.0 { + BoolViewInner::Const(b) => match res { + None => res = Some(b), + Some(a) if b != a => { + return Err(ReformulationError::TrivialUnsatisfiable) + } + _ => {} + }, + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + match res { + Some(b) => { + for atom in lits { + let Formula::Atom(l) = atom else { + unreachable!() + }; + slv.oracle + .add_clause([if b { l } else { !l }]) + .map_err(|_| ReformulationError::TrivialUnsatisfiable)?; + } + Ok(()) + } + None => slv + .oracle + .encode(&Formula::Equiv(lits), &TseitinEncoder) + .map_err(|_| ReformulationError::TrivialUnsatisfiable), + } + } + BoolExpr::Xor(es) => { + let mut lits = Vec::with_capacity(es.len()); + let mut count = 0; + for e in es { + match e.to_arg(ReifContext::Mixed, slv, map, None)?.0 { + BoolViewInner::Const(true) => count += 1, + BoolViewInner::Const(false) => {} + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let mut formula = Formula::Xor(lits); + if count % 2 == 1 { + formula = !formula; + } + slv.oracle + .encode(&formula, &TseitinEncoder) + .map_err(|_| ReformulationError::TrivialUnsatisfiable) + } + BoolExpr::IfThenElse { cond, then, els } => { + match cond.to_arg(ReifContext::Mixed, slv, map, None)?.0 { + BoolViewInner::Const(true) => then.constrain(slv, map), + BoolViewInner::Const(false) => els.constrain(slv, map), + BoolViewInner::Lit(_) => BoolExpr::And(vec![ + BoolExpr::Or(vec![!*cond.clone(), *then.clone()]), + BoolExpr::Or(vec![*cond.clone(), *els.clone()]), + ]) + .constrain(slv, map), + } + } + } + } + pub(crate) fn to_arg< Sol: PropagatorAccess + SatValuation, Sat: SatSolver + SolverTrait, @@ -34,11 +184,163 @@ impl BoolExpr { ctx: ReifContext, slv: &mut Solver, map: &mut VariableMap, - ) -> BoolView { + name: Option, + ) -> Result { + let bind_lit = |oracle: &mut Sat, lit| { + Ok(BoolView(BoolViewInner::Lit(if let Some(name) = name { + oracle + .encode( + &Formula::Equiv(vec![Formula::Atom(name), Formula::Atom(lit)]), + &TseitinEncoder, + ) + .map_err(|_| ReformulationError::TrivialUnsatisfiable)?; + name + } else { + lit + }))) + }; + let bind_const = |oracle: &mut Sat, val| { + if let Some(name) = name { + oracle + .add_clause([if val { name } else { !name }]) + .map_err(|_| ReformulationError::TrivialUnsatisfiable)?; + } + Ok(BoolView(BoolViewInner::Const(val))) + }; match self { - BoolExpr::Not(b) => b.to_negated_arg(ctx, slv, map), - BoolExpr::Lit(l) => BoolView(BoolViewInner::Lit(l.0)), - BoolExpr::Val(v) => BoolView(BoolViewInner::Const(*v)), + BoolExpr::Not(b) => b.to_negated_arg(ctx, slv, map, name), + BoolExpr::Lit(l) => bind_lit(&mut slv.oracle, l.0), + BoolExpr::Val(v) => bind_const(&mut slv.oracle, *v), + BoolExpr::Or(es) => { + let mut lits = Vec::with_capacity(es.len()); + for e in es { + match e.to_arg(ReifContext::Pos, slv, map, None)?.0 { + BoolViewInner::Const(false) => {} + BoolViewInner::Const(true) => return bind_const(&mut slv.oracle, true), + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let r = name.unwrap_or_else(|| slv.oracle.new_var().into()); + slv.oracle + .encode( + &Formula::Equiv(vec![Formula::Atom(r), Formula::Or(lits)]), + &TseitinEncoder, + ) + .unwrap(); + Ok(BoolView(BoolViewInner::Lit(r))) + } + BoolExpr::And(es) => { + let mut lits = Vec::with_capacity(es.len()); + for e in es { + match e.to_arg(ReifContext::Pos, slv, map, None)?.0 { + BoolViewInner::Const(true) => {} + BoolViewInner::Const(false) => return bind_const(&mut slv.oracle, false), + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let name = name.unwrap_or_else(|| slv.oracle.new_var().into()); + slv.oracle + .encode( + &Formula::Equiv(vec![Formula::Atom(name), Formula::And(lits)]), + &TseitinEncoder, + ) + .unwrap(); + Ok(BoolView(BoolViewInner::Lit(name))) + } + BoolExpr::Implies(a, b) => { + let a = match a.to_arg(ReifContext::Neg, slv, map, None)?.0 { + BoolViewInner::Const(true) => return b.to_arg(ctx, slv, map, name), + BoolViewInner::Const(false) => return bind_const(&mut slv.oracle, true), + BoolViewInner::Lit(l) => l, + }; + + // TODO: Conditional encoding + match b.to_arg(ctx, slv, map, None)?.0 { + BoolViewInner::Const(true) => bind_const(&mut slv.oracle, true), + BoolViewInner::Const(false) => bind_lit(&mut slv.oracle, !a), + BoolViewInner::Lit(b) => { + let name = name.unwrap_or_else(|| slv.oracle.new_var().into()); + slv.oracle + .encode( + &Formula::Equiv(vec![ + Formula::Atom(name), + Formula::Implies( + Box::new(Formula::Atom(a)), + Box::new(Formula::Atom(b)), + ), + ]), + &TseitinEncoder, + ) + .unwrap(); + Ok(BoolView(BoolViewInner::Lit(name))) + } + } + } + BoolExpr::Equiv(es) => { + let mut lits = Vec::with_capacity(es.len()); + let mut res = None; + for e in es { + match e.to_arg(ReifContext::Mixed, slv, map, None)?.0 { + BoolViewInner::Const(b) => match res { + None => res = Some(b), + Some(b2) if b != b2 => { + return bind_const(&mut slv.oracle, false); + } + Some(_) => {} + }, + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let name = name.unwrap_or_else(|| slv.oracle.new_var().into()); + let f = match res { + Some(b) => { + Formula::And(lits.into_iter().map(|e| if b { e } else { !e }).collect()) + } + None => Formula::Equiv(lits), + }; + slv.oracle + .encode( + &Formula::Equiv(vec![Formula::Atom(name), f]), + &TseitinEncoder, + ) + .unwrap(); + Ok(BoolView(BoolViewInner::Lit(name))) + } + BoolExpr::Xor(es) => { + let mut lits = Vec::with_capacity(es.len()); + let mut count = 0; + for e in es { + match e.to_arg(ReifContext::Mixed, slv, map, None)?.0 { + BoolViewInner::Const(true) => count += 1, + BoolViewInner::Const(false) => {} + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let name = name.unwrap_or_else(|| slv.oracle.new_var().into()); + let mut formula = Formula::Xor(lits); + if count % 2 == 1 { + formula = !formula; + } + slv.oracle + .encode( + &Formula::Equiv(vec![Formula::Atom(name), formula]), + &TseitinEncoder, + ) + .unwrap(); + Ok(BoolView(BoolViewInner::Lit(name))) + } + BoolExpr::IfThenElse { cond, then, els } => { + match cond.to_arg(ReifContext::Mixed, slv, map, None)?.0 { + BoolViewInner::Const(true) => then.to_arg(ctx, slv, map, name), + BoolViewInner::Const(false) => then.to_arg(ctx, slv, map, name), + // TODO: Conditional encoding + BoolViewInner::Lit(_) => BoolExpr::And(vec![ + BoolExpr::Or(vec![!*cond.clone(), *then.clone()]), + BoolExpr::Or(vec![*cond.clone(), *els.clone()]), + ]) + .to_arg(ctx, slv, map, name), + } + } } } @@ -50,11 +352,24 @@ impl BoolExpr { ctx: ReifContext, slv: &mut Solver, map: &mut VariableMap, - ) -> BoolView { + name: Option, + ) -> Result { match self { - BoolExpr::Not(v) => v.to_arg(ctx, slv, map), - BoolExpr::Lit(v) => BoolView(BoolViewInner::Lit((!v).0)), - BoolExpr::Val(v) => BoolView(BoolViewInner::Const(!v)), + BoolExpr::Not(v) => v.to_arg(!ctx, slv, map, name), + BoolExpr::Lit(v) => Ok(BoolView(BoolViewInner::Lit((!v).0))), + BoolExpr::Val(v) => Ok(BoolView(BoolViewInner::Const(!v))), + BoolExpr::Or(_) + | BoolExpr::And(_) + | BoolExpr::Implies(_, _) + | BoolExpr::IfThenElse { + cond: _, + then: _, + els: _, + } => (!self).to_arg(ctx, slv, map, name), + _ => { + let r = self.to_arg(ReifContext::Mixed, slv, map, name)?; + Ok(!r) + } } } } @@ -66,6 +381,15 @@ impl Not for BoolExpr { BoolExpr::Lit(l) => BoolExpr::Lit(!l), BoolExpr::Val(v) => BoolExpr::Val(!v), BoolExpr::Not(e) => *e, + BoolExpr::Or(es) => BoolExpr::And(es.into_iter().map(|e| !e).collect()), + BoolExpr::And(es) => BoolExpr::Or(es.into_iter().map(|e| !e).collect()), + BoolExpr::Implies(a, b) => BoolExpr::And(vec![*a, !*b]), + BoolExpr::IfThenElse { cond, then, els } => BoolExpr::IfThenElse { + cond, + then: Box::new(!*then), + els: Box::new(!*els), + }, + _ => BoolExpr::Not(Box::new(self)), } } } @@ -73,11 +397,7 @@ impl Not for BoolExpr { impl Not for &BoolExpr { type Output = BoolExpr; fn not(self) -> Self::Output { - match self { - BoolExpr::Lit(l) => BoolExpr::Lit(!*l), - BoolExpr::Val(v) => BoolExpr::Val(!*v), - BoolExpr::Not(e) => (**e).clone(), - } + !self.clone() } } diff --git a/crates/huub/src/model/flatzinc.rs b/crates/huub/src/model/flatzinc.rs index 810a51dd..5c6e3af4 100644 --- a/crates/huub/src/model/flatzinc.rs +++ b/crates/huub/src/model/flatzinc.rs @@ -3,7 +3,7 @@ use std::{collections::BTreeMap, fmt::Debug, ops::Deref}; use flatzinc_serde::{Argument, Domain, FlatZinc, Literal, Type, Variable}; use thiserror::Error; -use super::bool::BoolExpr; +use super::{bool::BoolExpr, reformulate::ReformulationError}; use crate::{ model::{IntExpr, Variable as MVar}, Constraint, Model, Solver, SolverView, @@ -18,6 +18,39 @@ impl Model { for c in fzn.constraints.iter() { match c.id.deref() { + "array_bool_and" => { + if let [es, r] = c.args.as_slice() { + let es = arg_array(fzn, es)?; + let r = arg_bool(fzn, &mut prb, &mut map, r)?; + let es: Result, _> = es + .iter() + .map(|l| lit_bool(fzn, &mut prb, &mut map, l)) + .collect(); + prb += BoolExpr::Equiv(vec![r, BoolExpr::And(es?)]); + } else { + return Err(FlatZincError::InvalidNumArgs { + name: "array_bool_and", + found: c.args.len(), + expected: 2, + }); + } + } + "array_bool_xor" => { + if let [es] = c.args.as_slice() { + let es = arg_array(fzn, es)?; + let es: Result, _> = es + .iter() + .map(|l| lit_bool(fzn, &mut prb, &mut map, l)) + .collect(); + prb += BoolExpr::Xor(es?); + } else { + return Err(FlatZincError::InvalidNumArgs { + name: "array_bool_xor", + found: c.args.len(), + expected: 2, + }); + } + } "bool_clause" => { if let [pos, neg] = c.args.as_slice() { let pos = arg_array(fzn, pos)?; @@ -29,13 +62,9 @@ impl Model { } for l in neg { let e = lit_bool(fzn, &mut prb, &mut map, l)?; - lits.push(match e { - BoolExpr::Lit(l) => BoolExpr::Lit(!l), - BoolExpr::Val(v) => BoolExpr::Val(!v), - e => BoolExpr::Not(Box::new(e)), - }) + lits.push(!e) } - prb += Constraint::Clause(lits); + prb += BoolExpr::Or(lits); } else { return Err(FlatZincError::InvalidNumArgs { name: "bool_clause", @@ -44,6 +73,75 @@ impl Model { }); } } + "bool_clause_reif" => { + if let [pos, neg, r] = c.args.as_slice() { + let pos = arg_array(fzn, pos)?; + let neg = arg_array(fzn, neg)?; + let r = arg_bool(fzn, &mut prb, &mut map, r)?; + let mut lits = Vec::with_capacity(pos.len() + neg.len()); + for l in pos { + let e = lit_bool(fzn, &mut prb, &mut map, l)?; + lits.push(e); + } + for l in neg { + let e = lit_bool(fzn, &mut prb, &mut map, l)?; + lits.push(!e) + } + prb += BoolExpr::Equiv(vec![r, BoolExpr::Or(lits)]); + } else { + return Err(FlatZincError::InvalidNumArgs { + name: "bool_clause_reif", + found: c.args.len(), + expected: 3, + }); + } + } + "bool_eq_reif" => { + if let [a, b, r] = c.args.as_slice() { + let a = arg_bool(fzn, &mut prb, &mut map, a)?; + let b = arg_bool(fzn, &mut prb, &mut map, b)?; + let r = arg_bool(fzn, &mut prb, &mut map, r)?; + prb += BoolExpr::Equiv(vec![r, BoolExpr::Equiv(vec![a, b])]); + } else { + return Err(FlatZincError::InvalidNumArgs { + name: "bool_eq_reif", + found: c.args.len(), + expected: 3, + }); + } + } + "bool_not" => { + if let [a, b] = c.args.as_slice() { + let a = arg_bool(fzn, &mut prb, &mut map, a)?; + let b = arg_bool(fzn, &mut prb, &mut map, b)?; + // TODO: This should not need two variables + prb += BoolExpr::Equiv(vec![b, !a]); + } else { + return Err(FlatZincError::InvalidNumArgs { + name: "bool_not", + found: c.args.len(), + expected: 2, + }); + } + } + "bool_xor" => { + if (2..=3).contains(&c.args.len()) { + let a = arg_bool(fzn, &mut prb, &mut map, &c.args[0])?; + let b = arg_bool(fzn, &mut prb, &mut map, &c.args[1])?; + let mut f = BoolExpr::Xor(vec![a, b]); + if c.args.len() == 3 { + let r = arg_bool(fzn, &mut prb, &mut map, &c.args[2])?; + f = BoolExpr::Equiv(vec![r, f]); + } + prb += f; + } else { + return Err(FlatZincError::InvalidNumArgs { + name: "bool_xor", + found: c.args.len(), + expected: 2, + }); + } + } "huub_all_different_int" => { if let [args] = c.args.as_slice() { let args = arg_array(fzn, args)?; @@ -136,7 +234,7 @@ impl Solver { fzn: &FlatZinc, ) -> Result<(Self, BTreeMap), FlatZincError> { let (prb, map) = Model::from_fzn(fzn)?; - let (slv, remap) = prb.to_solver(); + let (slv, remap) = prb.to_solver()?; let map = map.into_iter().map(|(k, v)| (k, remap.get(&v))).collect(); Ok((slv, map)) } @@ -210,6 +308,21 @@ fn lit_bool + Clone + Debug>( } } +fn arg_bool + Clone + Debug>( + fzn: &FlatZinc, + prb: &mut Model, + map: &mut BTreeMap, + arg: &Argument, +) -> Result { + match arg { + Argument::Literal(l) => lit_bool(fzn, prb, map, l), + _ => Err(FlatZincError::InvalidArgumentType { + expected: "bool", + found: format!("{:?}", arg), + }), + } +} + fn lit_int + Clone + Debug>( fzn: &FlatZinc, prb: &mut Model, @@ -262,4 +375,6 @@ pub enum FlatZincError { expected: &'static str, found: String, }, + #[error("error reformulating generated model `{0}'")] + ReformulationError(#[from] ReformulationError), } diff --git a/crates/huub/src/model/reformulate.rs b/crates/huub/src/model/reformulate.rs index 4470e1d0..73cfd574 100644 --- a/crates/huub/src/model/reformulate.rs +++ b/crates/huub/src/model/reformulate.rs @@ -1,5 +1,8 @@ -use std::collections::HashMap; +use std::{collections::HashMap, ops::Not}; +use thiserror::Error; + +use super::bool::{BoolVar, Literal}; use crate::{ model::Variable, solver::view::{BoolView, BoolViewInner, SolverView}, @@ -21,6 +24,13 @@ impl VariableMap { }) } + pub fn get_lit(&self, lit: &Literal) -> BoolView { + let SolverView::Bool(v) = self.get(&Variable::Bool(BoolVar(lit.0.var()))) else { + unreachable!() + }; + v + } + pub fn insert(&mut self, index: Variable, elem: SolverView) { let _ = self.map.insert(index, elem); } @@ -34,3 +44,20 @@ pub(crate) enum ReifContext { #[allow(dead_code)] Mixed, } + +impl Not for ReifContext { + type Output = Self; + fn not(self) -> Self::Output { + match self { + ReifContext::Pos => ReifContext::Neg, + ReifContext::Neg => ReifContext::Pos, + ReifContext::Mixed => ReifContext::Mixed, + } + } +} + +#[derive(Error, Debug)] +pub enum ReformulationError { + #[error("The expression is trivially unsatisfiable")] + TrivialUnsatisfiable, +} diff --git a/crates/huub/src/solver/view.rs b/crates/huub/src/solver/view.rs index 75561e5f..fb127ecb 100644 --- a/crates/huub/src/solver/view.rs +++ b/crates/huub/src/solver/view.rs @@ -1,4 +1,4 @@ -use std::num::NonZeroI32; +use std::{num::NonZeroI32, ops::Not}; use pindakaas::{ solver::{PropagatorAccess, Solver as SolverTrait}, @@ -64,6 +64,27 @@ pub(crate) enum BoolViewInner { Const(bool), } +impl Not for BoolView { + type Output = Self; + + fn not(self) -> Self::Output { + match self.0 { + BoolViewInner::Lit(l) => BoolView(BoolViewInner::Lit(!l)), + BoolViewInner::Const(b) => BoolView(BoolViewInner::Const(!b)), + } + } +} +impl Not for &BoolView { + type Output = BoolView; + + fn not(self) -> Self::Output { + match self.0 { + BoolViewInner::Lit(l) => BoolView(BoolViewInner::Lit(!l)), + BoolViewInner::Const(b) => BoolView(BoolViewInner::Const(!b)), + } + } +} + #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] pub struct IntView(pub(crate) IntViewInner); diff --git a/share/minizinc/huub/redefinitions.mzn b/share/minizinc/huub/redefinitions.mzn index e69de29b..43210a1b 100644 --- a/share/minizinc/huub/redefinitions.mzn +++ b/share/minizinc/huub/redefinitions.mzn @@ -0,0 +1,3 @@ +predicate bool_lt(var bool: a, var bool: b) = not a /\ b; +predicate bool_lt_imp(var bool: a, var bool: b, var bool: r) = r -> (not a /\ b); +predicate bool_lt_reif(var bool: a, var bool: b, var bool: r) = r = (not a /\ b);