Add basic modelling and reformulation of propositional logic

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<SolverView> = 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<SolverView>) = 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,15 +126,15 @@ 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))
 						.collect::<Vec<_>>()
 						.join(",")
 				)
 			} else {
-				println!("{ident} = {}", value(var_map[ident]).unwrap())
+				println!("{ident} = {};", value(var_map[ident]).unwrap())
 			}
 		}
 		println!("----------");

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,18 +22,18 @@ type Conjunction<L = RawLit> = Vec<L>;
 
 #[cfg(test)]
 mod tests {
-	use crate::{Constraint, Model, SolveResult, Solver, Variable};
+	use crate::{BoolExpr, Model, SolveResult, Solver, Variable};
 
 	#[test]
 	fn it_works() {
 		let mut prb = Model::default();
 		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));