use crate::common::error::Error;
use crate::traits::SolidStruct;
use std::ops::{Add, Mul, Sub};
pub struct Boolean<S: SolidStruct> {
pub(crate) solids: Vec<S>,
pub(crate) clauses: Vec<i64>, }
impl<S: SolidStruct> Boolean<S> {
pub(crate) fn from_parts(solids: Vec<S>, clauses: Vec<i64>) -> Self {
Boolean { solids, clauses }
}
pub fn solids(&self) -> &[S] {
&self.solids
}
pub fn clauses(&self) -> &[i64] {
&self.clauses
}
pub fn build(self) -> Result<S, Error> {
let mut v = self.build_vec()?;
match v.len() {
1 => Ok(v.pop().unwrap()),
n => Err(Error::OneFailed(n)),
}
}
pub fn build_vec(self) -> Result<Vec<S>, Error> {
if self.solids.is_empty() || self.clauses.is_empty() {
return Err(Error::OneFailed(0));
}
S::boolean_build(&self)
}
pub(crate) fn dnf_union(mut a: Self, b: Self) -> Self {
let shift = a.solids.len() as i64;
a.solids.extend(b.solids);
for lit in b.clauses {
if lit == 0 {
a.clauses.push(0);
} else if lit > 0 {
a.clauses.push(lit + shift);
} else {
a.clauses.push(lit - shift);
}
}
a
}
pub(crate) fn dnf_intersect(a: Self, b: Self) -> Self {
let a_clauses: Vec<Vec<i64>> = a.clauses.split(|&l| l == 0).filter(|c| !c.is_empty()).map(|c| c.to_vec()).collect();
let shift = a.solids.len() as i64;
let b_clauses: Vec<Vec<i64>> = b.clauses.split(|&l| l == 0).filter(|c| !c.is_empty()).map(|c| c.iter().map(|&l| if l > 0 { l + shift } else { l - shift }).collect()).collect();
let mut solids = a.solids;
solids.extend(b.solids);
let mut clauses = Vec::with_capacity(a_clauses.len() * b_clauses.len() * 4);
for ca in &a_clauses {
for cb in &b_clauses {
clauses.extend_from_slice(ca);
clauses.extend_from_slice(cb);
clauses.push(0);
}
}
Boolean { solids, clauses }
}
pub(crate) fn dnf_subtract(a: Self, b: Self) -> Self {
let b_clauses: Vec<Vec<i64>> = b.clauses.split(|&l| l == 0).filter(|c| !c.is_empty()).map(|c| c.to_vec()).collect();
if b_clauses.is_empty() {
return a; }
let mut accum: Vec<Vec<i64>> = vec![Vec::new()];
for clause in &b_clauses {
let mut next = Vec::with_capacity(accum.len() * clause.len());
for partial in &accum {
for &lit in clause {
let mut combined = partial.clone();
combined.push(-lit);
next.push(combined);
}
}
accum = next;
}
let mut neg_b_clauses = Vec::new();
for cl in accum {
neg_b_clauses.extend(cl);
neg_b_clauses.push(0);
}
let neg_b = Boolean { solids: b.solids, clauses: neg_b_clauses };
Self::dnf_intersect(a, neg_b)
}
}
impl<S: SolidStruct> Clone for Boolean<S> {
fn clone(&self) -> Self {
S::boolean(self.solids.iter(), self.clauses.iter().copied())
}
}
impl<S: SolidStruct> TryFrom<Boolean<S>> for Vec<S> {
type Error = Error;
fn try_from(b: Boolean<S>) -> Result<Self, Error> {
b.build_vec()
}
}
impl<S: SolidStruct> From<S> for Boolean<S> {
fn from(s: S) -> Self {
S::boolean(std::iter::once(&s), [1i64, 0])
}
}
impl<'a, S: SolidStruct> From<&'a S> for Boolean<S> {
fn from(s: &'a S) -> Self {
S::boolean(std::iter::once(s), [1i64, 0])
}
}
macro_rules! boolean_lhs_ops {
(& $rhs:ty) => {
impl<'a, S: SolidStruct> Add<&'a $rhs> for Boolean<S> {
type Output = Boolean<S>;
fn add(self, rhs: &'a $rhs) -> Boolean<S> {
Boolean::dnf_union(self, rhs.into())
}
}
impl<'a, S: SolidStruct> Sub<&'a $rhs> for Boolean<S> {
type Output = Boolean<S>;
fn sub(self, rhs: &'a $rhs) -> Boolean<S> {
Boolean::dnf_subtract(self, rhs.into())
}
}
impl<'a, S: SolidStruct> Mul<&'a $rhs> for Boolean<S> {
type Output = Boolean<S>;
fn mul(self, rhs: &'a $rhs) -> Boolean<S> {
Boolean::dnf_intersect(self, rhs.into())
}
}
};
($rhs:ty) => {
impl<S: SolidStruct> Add<$rhs> for Boolean<S> {
type Output = Boolean<S>;
fn add(self, rhs: $rhs) -> Boolean<S> {
Boolean::dnf_union(self, rhs.into())
}
}
impl<S: SolidStruct> Sub<$rhs> for Boolean<S> {
type Output = Boolean<S>;
fn sub(self, rhs: $rhs) -> Boolean<S> {
Boolean::dnf_subtract(self, rhs.into())
}
}
impl<S: SolidStruct> Mul<$rhs> for Boolean<S> {
type Output = Boolean<S>;
fn mul(self, rhs: $rhs) -> Boolean<S> {
Boolean::dnf_intersect(self, rhs.into())
}
}
};
}
boolean_lhs_ops!(Boolean<S>);
boolean_lhs_ops!(S);
boolean_lhs_ops!(&S);
impl<S: SolidStruct> Default for Boolean<S> {
fn default() -> Self {
Boolean { solids: Vec::new(), clauses: Vec::new() }
}
}