gistfile1.rs

pub trait Formula {
	type C: Clause;
	fn get_unit(&self) -> Option<&Self::C>;
	fn force_assignment(&mut self, lit: Literal, reason: &Self::C);
}

fn unit<F: Formula>(f: &mut F) -> bool {
	let unit_clause = match f.get_unit() {
		Some(x) => x,
		None    => return false
	};

	f.force_assignment(unit_clause.unit_lit().unwrap(), unit_clause);
	true
}