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/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"
 

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, Constraint, 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 += 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));
 

crates/huub/src/model.rs

@@ -1,30 +1,27 @@
-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;
 
 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<ValueFn = Sol>,
 	>(
 		&self,
-	) -> (Solver<Sat>, VariableMap) {
+	) -> Result<(Solver<Sat>, 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<I: IntoIterator<Item = pindakaas::Lit>>(&mut self, cl: I) -> pindakaas::Result {
+	fn add_clause<I: IntoIterator<Item = RawLit>>(&mut self, cl: I) -> pindakaas::Result {
 		self.cnf.add_clause(cl)
 	}
+
+	type CondDB = Model;
+	fn with_conditions(&mut self, conditions: Vec<RawLit>) -> ConditionalDatabase<Self::CondDB> {
+		ConditionalDatabase::new(self, conditions)
+	}
 }
 
 #[derive(Debug, PartialEq, Eq, Hash)]
 pub enum Constraint {
-	Clause(Vec<BoolExpr>),
+	SimpleBool(BoolExpr),
 	AllDifferent(Vec<IntExpr>),
 	IntLinLessEq(Vec<IntVal>, Vec<IntExpr>, IntVal),
 	IntLinEq(Vec<IntVal>, Vec<IntExpr>, IntVal),
@@ -109,28 +110,16 @@ impl Constraint {
 		&self,
 		slv: &mut Solver<Sat>,
 		map: &mut VariableMap,
-	) {
-		struct Satisfied;
+	) -> Result<(), ReformulationError> {
 		match self {
-			Constraint::Clause(v) => {
-				let lits: Result<Vec<RawLit>, 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(())
 			}
 		}
 	}