From 1fff02b2509210f7d3f05517835393199c1e05bb Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 6 May 2024 21:29:05 +1000 Subject: [PATCH] Add basic modelling and reformulation of propositional logic --- crates/fzn-huub/src/main.rs | 26 ++- crates/huub/Cargo.toml | 5 +- crates/huub/src/lib.rs | 13 +- crates/huub/src/model.rs | 57 ++--- crates/huub/src/model/bool.rs | 305 +++++++++++++++++++++++++- crates/huub/src/model/flatzinc.rs | 134 ++++++++++- crates/huub/src/model/reformulate.rs | 16 ++ crates/huub/src/solver/view.rs | 23 +- share/minizinc/huub/redefinitions.mzn | 3 + 9 files changed, 518 insertions(+), 64 deletions(-) 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/Cargo.toml b/crates/huub/Cargo.toml index e6d3cbe8..68fc18b2 100644 --- a/crates/huub/Cargo.toml +++ b/crates/huub/Cargo.toml @@ -14,9 +14,12 @@ delegate = "0.12" flatzinc-serde = "0.2" index_vec = "0.1.3" itertools = "0.12.1" -pindakaas = { git = "https://github.com/pindakaashq/pindakaas.git", features = [ +pindakaas = { path = "/Users/dekker1/Code/github.com/pindakaas/crates/pindakaas", features = [ "ipasir-up", ] } +# pindakaas = { git = "https://github.com/pindakaashq/pindakaas.git", features = [ +# "ipasir-up", +# ] } thiserror = "1.0.59" tracing = "0.1.40" diff --git a/crates/huub/src/lib.rs b/crates/huub/src/lib.rs index 19ec63fc..1c482b6b 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, Constraint, 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 += Constraint::SimpleBool(BoolExpr::Or(vec![(!a).into(), (!b).into()])); + prb += Constraint::SimpleBool(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..b1f5ab14 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)) } } @@ -88,14 +84,19 @@ impl ClauseDatabase for Model { 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 +110,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 +138,7 @@ impl Constraint { }) .collect(); slv.add_propagator(LinearLE::new(coeffs, vars, *c)); + Ok(()) } Constraint::IntLinEq(coeffs, vars, c) => { let vars: Vec<_> = vars @@ -162,7 +152,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..f07edb9e 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,157 @@ 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).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).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) { + BoolView(BoolViewInner::Const(true)) => return b.constrain(slv, map), + BoolView(BoolViewInner::Const(false)) => return Ok(()), + BoolView(BoolViewInner::Lit(l)) => l, + }; + + match b.to_arg(ReifContext::Pos, slv, map).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).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).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).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, @@ -39,6 +184,131 @@ impl BoolExpr { 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::Or(es) => { + let mut lits = Vec::with_capacity(es.len()); + for e in es { + match e.to_arg(ctx, slv, map).0 { + BoolViewInner::Const(false) => {} + BoolViewInner::Const(true) => return BoolView(BoolViewInner::Const(true)), + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let r = slv.oracle.new_var().into(); + slv.oracle + .encode( + &Formula::Equiv(vec![Formula::Atom(r), Formula::Or(lits)]), + &TseitinEncoder, + ) + .unwrap(); + BoolView(BoolViewInner::Lit(r)) + } + BoolExpr::And(es) => { + let mut lits = Vec::with_capacity(es.len()); + for e in es { + match e.to_arg(ctx, slv, map).0 { + BoolViewInner::Const(true) => {} + BoolViewInner::Const(false) => return BoolView(BoolViewInner::Const(true)), + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let r = slv.oracle.new_var().into(); + slv.oracle + .encode( + &Formula::Equiv(vec![Formula::Atom(r), Formula::And(lits)]), + &TseitinEncoder, + ) + .unwrap(); + BoolView(BoolViewInner::Lit(r)) + } + BoolExpr::Implies(a, b) => { + let a = match a.to_arg(ctx, slv, map) { + BoolView(BoolViewInner::Const(true)) => return b.to_arg(ctx, slv, map), + BoolView(BoolViewInner::Const(false)) => { + return BoolView(BoolViewInner::Const(true)) + } + BoolView(BoolViewInner::Lit(l)) => l, + }; + + match b.to_arg(ctx, slv, map).0 { + BoolViewInner::Const(true) => BoolView(BoolViewInner::Const(true)), + BoolViewInner::Const(false) => BoolView(BoolViewInner::Lit(!a)), + BoolViewInner::Lit(b) => { + let r = slv.oracle.new_var().into(); + slv.oracle + .encode( + &Formula::Equiv(vec![ + Formula::Atom(r), + Formula::Implies( + Box::new(Formula::Atom(a)), + Box::new(Formula::Atom(b)), + ), + ]), + &TseitinEncoder, + ) + .unwrap(); + BoolView(BoolViewInner::Lit(r)) + } + } + } + BoolExpr::Equiv(es) => { + let mut lits = Vec::with_capacity(es.len()); + let mut res = None; + for e in es { + match e.to_arg(ctx, slv, map).0 { + BoolViewInner::Const(b) => match res { + None => res = Some(b), + Some(b2) if b != b2 => { + return BoolView(BoolViewInner::Const(false)); + } + Some(_) => {} + }, + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let r = 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(r), f]), &TseitinEncoder) + .unwrap(); + BoolView(BoolViewInner::Lit(r)) + } + BoolExpr::Xor(es) => { + let mut lits = Vec::with_capacity(es.len()); + let mut count = 0; + for e in es { + match e.to_arg(ctx, slv, map).0 { + BoolViewInner::Const(true) => count += 1, + BoolViewInner::Const(false) => {} + BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), + } + } + let r = 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(r), formula]), + &TseitinEncoder, + ) + .unwrap(); + BoolView(BoolViewInner::Lit(r)) + } + BoolExpr::IfThenElse { cond, then, els } => match cond.to_arg(ctx, slv, map).0 { + BoolViewInner::Const(true) => then.to_arg(ctx, slv, map), + BoolViewInner::Const(false) => then.to_arg(ctx, slv, map), + BoolViewInner::Lit(_) => BoolExpr::And(vec![ + BoolExpr::Or(vec![!*cond.clone(), *then.clone()]), + BoolExpr::Or(vec![*cond.clone(), *els.clone()]), + ]) + .to_arg(ctx, slv, map), + }, } } @@ -55,6 +325,18 @@ impl BoolExpr { 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::Or(_) + | BoolExpr::And(_) + | BoolExpr::Implies(_, _) + | BoolExpr::IfThenElse { + cond: _, + then: _, + els: _, + } => (!self).to_arg(ctx, slv, map), + _ => { + let r = self.to_arg(ctx, slv, map); + !r + } } } } @@ -66,6 +348,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 +364,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..771735bc 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 += Constraint::SimpleBool(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 += Constraint::SimpleBool(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 += Constraint::SimpleBool(BoolExpr::Or(lits)); } else { return Err(FlatZincError::InvalidNumArgs { name: "bool_clause", @@ -44,6 +73,78 @@ 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 += Constraint::SimpleBool(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 += Constraint::SimpleBool(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 += Constraint::SimpleBool(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 += Constraint::SimpleBool(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 +237,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 +311,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 +378,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..df732d5f 100644 --- a/crates/huub/src/model/reformulate.rs +++ b/crates/huub/src/model/reformulate.rs @@ -1,10 +1,13 @@ use std::collections::HashMap; +use thiserror::Error; use crate::{ model::Variable, solver::view::{BoolView, BoolViewInner, SolverView}, }; +use super::bool::{BoolVar, Literal}; + /// A reformulation mapping helper that automatically maps variables to /// themselves unless otherwise specified #[derive(Default, Clone, Debug, PartialEq, Eq)] @@ -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,9 @@ pub(crate) enum ReifContext { #[allow(dead_code)] 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);