cnfgen/
boolvar.rs

1// boolexpr.rs - boolean expression structures.
2
3#![cfg_attr(docsrs, feature(doc_cfg))]
4//! The module to generate CNF clauses from boolean expressions better than 'boolexpr'.
5//!
6//! This is new module to handle expressions better than boolexpr. It allows to use
7//! references and other types. To write some formula `call16`, `call32` or `callsys` should be
8//! used to call routine that generates formula by using this module.
9//!
10//! Simple example:
11//!
12//! ```
13//! use cnfgen::boolvar::*;
14//! use cnfgen::writer::{CNFError, CNFWriter};
15//! use std::io;
16//! fn simple_expr_generator() -> Result<(), CNFError> {
17//!     // call routine to generate formula.
18//!     let expr = call32(|| {
19//!         // define variables.
20//!         let x1 = BoolVar32::var();
21//!         let x2 = BoolVar32::var();
22//!         let x3 = BoolVar32::var();
23//!         let x4 = BoolVar32::var();
24//!         // define final expression: x1 => ((x2 xor x3) == (x3 and x4)).
25//!         x1.imp((x2 ^ &x3).bequal(&x3 & x4))
26//!     });
27//!     // write CNF to stdout.
28//!     expr.write(&mut CNFWriter::new(io::stdout()))
29//! }
30//! ```
31
32use std::cell::RefCell;
33use std::collections::HashMap;
34use std::fmt::Debug;
35use std::io::Write;
36use std::ops::{BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Neg, Not};
37use std::rc::Rc;
38
39use crate::boolexpr::BoolExprNode;
40pub use crate::boolexpr::{BoolEqual, BoolImpl};
41pub use crate::boolexpr_creator::{ExprCreator, ExprCreator32, ExprCreatorSys};
42use crate::writer::{CNFError, CNFWriter, Literal, QuantSet, Quantifier, VarLit};
43
44#[derive(thiserror::Error, Debug)]
45pub enum BoolVarError {
46    /// If no value in BoolVar
47    #[error("No value")]
48    NoValue,
49    /// If no literal in BoolVar
50    #[error("No literal")]
51    NoLiteral,
52}
53
54thread_local! {
55    pub(crate) static EXPR_CREATOR_16: RefCell<Option<Rc<RefCell<ExprCreator<i16>>>>> =
56        RefCell::new(None);
57    pub(crate) static EXPR_CREATOR_32: RefCell<Option<Rc<RefCell<ExprCreator32>>>> =
58        RefCell::new(None);
59    pub(crate) static EXPR_CREATOR_SYS: RefCell<Option<Rc<RefCell<ExprCreatorSys>>>> =
60        RefCell::new(None);
61}
62
63/// Get current ExprCreator. Panic if it not set.
64pub fn get_expr_creator_16() -> Rc<RefCell<ExprCreator<i16>>> {
65    EXPR_CREATOR_16.with_borrow(|ec| ec.as_ref().unwrap().clone())
66}
67
68/// Get current ExprCreator. Panic if it not set.
69pub fn get_expr_creator_32() -> Rc<RefCell<ExprCreator32>> {
70    EXPR_CREATOR_32.with_borrow(|ec| ec.as_ref().unwrap().clone())
71}
72
73/// Get current ExprCreator. Panic if it not set.
74pub fn get_expr_creator_sys() -> Rc<RefCell<ExprCreatorSys>> {
75    EXPR_CREATOR_SYS.with_borrow(|ec| ec.as_ref().unwrap().clone())
76}
77
78/// Call routine of that operates on expressions with new ExprCreator16 (where T type is i16).
79/// Before call install new ExprCreator and after call uninstall ExprCreator.
80pub fn call16<F, R>(mut f: F) -> R
81where
82    F: FnMut() -> R,
83{
84    // install new ExprCreator
85    EXPR_CREATOR_16.with_borrow(|ec| assert!(!ec.is_some()));
86    EXPR_CREATOR_16.set(Some(ExprCreator::<i16>::new()));
87    let r = f();
88    // drop
89    let _ = EXPR_CREATOR_16.replace(None);
90    r
91}
92
93/// Call routine of that operates on expressions with new ExprCreator32 (where T type is i32).
94/// Before call install new ExprCreator and after call uninstall ExprCreator.
95pub fn call32<F, R>(mut f: F) -> R
96where
97    F: FnMut() -> R,
98{
99    // install new ExprCreator
100    EXPR_CREATOR_32.with_borrow(|ec| assert!(!ec.is_some()));
101    EXPR_CREATOR_32.set(Some(ExprCreator32::new()));
102    let r = f();
103    // drop
104    let _ = EXPR_CREATOR_32.replace(None);
105    r
106}
107
108/// Call routine of that operates on expressions with new ExprCreatorSys (where T type is isize).
109/// Before call install new ExprCreator and after call uninstall ExprCreator.
110pub fn callsys<F, R>(mut f: F) -> R
111where
112    F: FnMut() -> R,
113{
114    // install new ExprCreator
115    EXPR_CREATOR_SYS.with_borrow(|ec| assert!(!ec.is_some()));
116    EXPR_CREATOR_SYS.set(Some(ExprCreatorSys::new()));
117    let r = f();
118    // drop
119    let _ = EXPR_CREATOR_SYS.replace(None);
120    r
121}
122
123/// Main structure to that provides easier to use interface than same BoolExprNode.
124/// Usage is simplier and allow to use references.
125#[derive(Clone, Debug, PartialEq, Eq)]
126pub struct BoolVar<T: VarLit>(BoolExprNode<T>);
127
128impl<T: VarLit> From<BoolVar<T>> for BoolExprNode<T> {
129    fn from(t: BoolVar<T>) -> Self {
130        t.0
131    }
132}
133
134impl<T: VarLit> From<BoolExprNode<T>> for BoolVar<T> {
135    fn from(t: BoolExprNode<T>) -> Self {
136        Self(t)
137    }
138}
139
140macro_rules! from_bool_impl {
141    ($t:ident, $creator:ident) => {
142        impl From<bool> for BoolVar<$t> {
143            fn from(v: bool) -> Self {
144                $creator.with_borrow(|ec| {
145                    BoolVar(BoolExprNode::single_value(ec.clone().unwrap().clone(), v))
146                })
147            }
148        }
149    };
150}
151from_bool_impl!(i16, EXPR_CREATOR_16);
152from_bool_impl!(i32, EXPR_CREATOR_32);
153from_bool_impl!(isize, EXPR_CREATOR_SYS);
154
155macro_rules! from_literal_impl {
156    ($t:ident, $creator:ident) => {
157        impl From<Literal<$t>> for BoolVar<$t> {
158            fn from(v: Literal<$t>) -> Self {
159                $creator
160                    .with_borrow(|ec| BoolVar(BoolExprNode::single(ec.clone().unwrap().clone(), v)))
161            }
162        }
163    };
164}
165from_literal_impl!(i16, EXPR_CREATOR_16);
166from_literal_impl!(i32, EXPR_CREATOR_32);
167from_literal_impl!(isize, EXPR_CREATOR_SYS);
168
169macro_rules! default_impl {
170    ($t:ident, $creator:ident) => {
171        impl Default for BoolVar<$t> {
172            fn default() -> Self {
173                Self::from(false)
174            }
175        }
176    };
177}
178default_impl!(i16, EXPR_CREATOR_16);
179default_impl!(i32, EXPR_CREATOR_32);
180default_impl!(isize, EXPR_CREATOR_SYS);
181
182impl<T> TryFrom<BoolVar<T>> for bool
183where
184    T: VarLit + Neg<Output = T> + Debug,
185    isize: TryFrom<T>,
186    <T as TryInto<usize>>::Error: Debug,
187    <T as TryFrom<usize>>::Error: Debug,
188    <isize as TryFrom<T>>::Error: Debug,
189{
190    type Error = BoolVarError;
191    fn try_from(value: BoolVar<T>) -> Result<Self, Self::Error> {
192        value.0.value().ok_or(BoolVarError::NoValue)
193    }
194}
195
196impl<T> TryFrom<BoolVar<T>> for Literal<T>
197where
198    T: VarLit + Neg<Output = T> + Debug,
199    isize: TryFrom<T>,
200    <T as TryInto<usize>>::Error: Debug,
201    <T as TryFrom<usize>>::Error: Debug,
202    <isize as TryFrom<T>>::Error: Debug,
203{
204    type Error = BoolVarError;
205    fn try_from(value: BoolVar<T>) -> Result<Self, Self::Error> {
206        value
207            .0
208            .varlit()
209            .map(|t| Literal::VarLit(t))
210            .ok_or(BoolVarError::NoLiteral)
211    }
212}
213
214macro_rules! var_impl {
215    ($t:ident, $creator:ident) => {
216        impl BoolVar<$t> {
217            pub fn var() -> Self {
218                $creator.with_borrow(|ec| BoolVar(BoolExprNode::variable(ec.clone().unwrap())))
219            }
220        }
221    };
222}
223var_impl!(i16, EXPR_CREATOR_16);
224var_impl!(i32, EXPR_CREATOR_32);
225var_impl!(isize, EXPR_CREATOR_SYS);
226
227impl<T> BoolVar<T>
228where
229    T: VarLit + Neg<Output = T> + Debug,
230    isize: TryFrom<T>,
231    <T as TryInto<usize>>::Error: Debug,
232    <T as TryFrom<usize>>::Error: Debug,
233    <isize as TryFrom<T>>::Error: Debug,
234{
235    pub fn value(&self) -> Option<bool> {
236        self.0.value()
237    }
238    pub fn varlit(&self) -> Option<T> {
239        self.0.varlit()
240    }
241
242    /// Writes expression to CNF.
243    pub fn write<W: Write>(&self, cnf: &mut CNFWriter<W>) -> Result<(), CNFError> {
244        self.0.write(cnf)
245    }
246
247    /// Writes quantified expression to QCNF.
248    pub fn write_quant<W, QL, Q>(&self, quants: QL, cnf: &mut CNFWriter<W>) -> Result<(), CNFError>
249    where
250        W: Write,
251        QL: IntoIterator<Item = (Quantifier, Q)>,
252        Q: QuantSet<T>,
253    {
254        self.0.write_quant(quants, cnf)
255    }
256}
257
258impl<T> Not for BoolVar<T>
259where
260    T: VarLit + Neg<Output = T> + Debug,
261    isize: TryFrom<T>,
262    <T as TryInto<usize>>::Error: Debug,
263    <T as TryFrom<usize>>::Error: Debug,
264    <isize as TryFrom<T>>::Error: Debug,
265{
266    type Output = Self;
267
268    fn not(self) -> Self::Output {
269        BoolVar(!self.0)
270    }
271}
272
273impl<T> Not for &BoolVar<T>
274where
275    T: VarLit + Neg<Output = T> + Debug,
276    isize: TryFrom<T>,
277    <T as TryInto<usize>>::Error: Debug,
278    <T as TryFrom<usize>>::Error: Debug,
279    <isize as TryFrom<T>>::Error: Debug,
280{
281    type Output = <BoolVar<T> as Not>::Output;
282
283    fn not(self) -> Self::Output {
284        BoolVar(!self.0.clone())
285    }
286}
287
288macro_rules! new_op_from_impl {
289    ($t:ident, $v:ident, $t2:ident) => {
290        impl<T> $t<$t2<T>> for BoolVar<T>
291        where
292            T: VarLit + Neg<Output = T> + Debug,
293            isize: TryFrom<T>,
294            <T as TryInto<usize>>::Error: Debug,
295            <T as TryFrom<usize>>::Error: Debug,
296            <isize as TryFrom<T>>::Error: Debug,
297        {
298            type Output = BoolVar<T>;
299            fn $v(self, rhs: $t2<T>) -> Self::Output {
300                Self(self.0.$v(rhs))
301            }
302        }
303        impl<T> $t<&$t2<T>> for BoolVar<T>
304        where
305            T: VarLit + Neg<Output = T> + Debug,
306            isize: TryFrom<T>,
307            <T as TryInto<usize>>::Error: Debug,
308            <T as TryFrom<usize>>::Error: Debug,
309            <isize as TryFrom<T>>::Error: Debug,
310        {
311            type Output = BoolVar<T>;
312            fn $v(self, rhs: &$t2<T>) -> Self::Output {
313                Self(self.0.$v(rhs.clone()))
314            }
315        }
316        impl<T> $t<$t2<T>> for &BoolVar<T>
317        where
318            T: VarLit + Neg<Output = T> + Debug,
319            isize: TryFrom<T>,
320            <T as TryInto<usize>>::Error: Debug,
321            <T as TryFrom<usize>>::Error: Debug,
322            <isize as TryFrom<T>>::Error: Debug,
323        {
324            type Output = BoolVar<T>;
325            fn $v(self, rhs: $t2<T>) -> Self::Output {
326                BoolVar::<T>(self.0.clone().$v(rhs))
327            }
328        }
329        impl<T> $t<&$t2<T>> for &BoolVar<T>
330        where
331            T: VarLit + Neg<Output = T> + Debug,
332            isize: TryFrom<T>,
333            <T as TryInto<usize>>::Error: Debug,
334            <T as TryFrom<usize>>::Error: Debug,
335            <isize as TryFrom<T>>::Error: Debug,
336        {
337            type Output = BoolVar<T>;
338            fn $v(self, rhs: &$t2<T>) -> Self::Output {
339                BoolVar::<T>(self.0.clone().$v(rhs.clone()))
340            }
341        }
342
343        impl<T> $t<BoolVar<T>> for $t2<T>
344        where
345            T: VarLit + Neg<Output = T> + Debug,
346            isize: TryFrom<T>,
347            <T as TryInto<usize>>::Error: Debug,
348            <T as TryFrom<usize>>::Error: Debug,
349            <isize as TryFrom<T>>::Error: Debug,
350        {
351            type Output = BoolVar<T>;
352            fn $v(self, rhs: BoolVar<T>) -> Self::Output {
353                BoolVar::<T>(self.$v(rhs.0))
354            }
355        }
356        impl<T> $t<&BoolVar<T>> for $t2<T>
357        where
358            T: VarLit + Neg<Output = T> + Debug,
359            isize: TryFrom<T>,
360            <T as TryInto<usize>>::Error: Debug,
361            <T as TryFrom<usize>>::Error: Debug,
362            <isize as TryFrom<T>>::Error: Debug,
363        {
364            type Output = BoolVar<T>;
365            fn $v(self, rhs: &BoolVar<T>) -> Self::Output {
366                BoolVar::<T>(self.$v(rhs.0.clone()))
367            }
368        }
369        impl<T> $t<BoolVar<T>> for &$t2<T>
370        where
371            T: VarLit + Neg<Output = T> + Debug,
372            isize: TryFrom<T>,
373            <T as TryInto<usize>>::Error: Debug,
374            <T as TryFrom<usize>>::Error: Debug,
375            <isize as TryFrom<T>>::Error: Debug,
376        {
377            type Output = BoolVar<T>;
378            fn $v(self, rhs: BoolVar<T>) -> Self::Output {
379                BoolVar::<T>(self.clone().$v(rhs.0))
380            }
381        }
382        impl<T> $t<&BoolVar<T>> for &$t2<T>
383        where
384            T: VarLit + Neg<Output = T> + Debug,
385            isize: TryFrom<T>,
386            <T as TryInto<usize>>::Error: Debug,
387            <T as TryFrom<usize>>::Error: Debug,
388            <isize as TryFrom<T>>::Error: Debug,
389        {
390            type Output = BoolVar<T>;
391            fn $v(self, rhs: &BoolVar<T>) -> Self::Output {
392                BoolVar::<T>(self.clone().$v(rhs.0.clone()))
393            }
394        }
395    };
396}
397
398macro_rules! new_op_impl {
399    ($t:ident, $v:ident) => {
400        impl<T> $t<BoolVar<T>> for BoolVar<T>
401        where
402            T: VarLit + Neg<Output = T> + Debug,
403            isize: TryFrom<T>,
404            <T as TryInto<usize>>::Error: Debug,
405            <T as TryFrom<usize>>::Error: Debug,
406            <isize as TryFrom<T>>::Error: Debug,
407        {
408            type Output = BoolVar<T>;
409            fn $v(self, rhs: BoolVar<T>) -> Self::Output {
410                Self(self.0.$v(rhs.0))
411            }
412        }
413        impl<T> $t<&BoolVar<T>> for BoolVar<T>
414        where
415            T: VarLit + Neg<Output = T> + Debug,
416            isize: TryFrom<T>,
417            <T as TryInto<usize>>::Error: Debug,
418            <T as TryFrom<usize>>::Error: Debug,
419            <isize as TryFrom<T>>::Error: Debug,
420        {
421            type Output = BoolVar<T>;
422            fn $v(self, rhs: &Self) -> Self::Output {
423                Self(self.0.$v(rhs.0.clone()))
424            }
425        }
426        impl<T> $t<BoolVar<T>> for &BoolVar<T>
427        where
428            T: VarLit + Neg<Output = T> + Debug,
429            isize: TryFrom<T>,
430            <T as TryInto<usize>>::Error: Debug,
431            <T as TryFrom<usize>>::Error: Debug,
432            <isize as TryFrom<T>>::Error: Debug,
433        {
434            type Output = BoolVar<T>;
435            fn $v(self, rhs: BoolVar<T>) -> Self::Output {
436                BoolVar::<T>(self.0.clone().$v(rhs.0))
437            }
438        }
439        impl<T> $t for &BoolVar<T>
440        where
441            T: VarLit + Neg<Output = T> + Debug,
442            isize: TryFrom<T>,
443            <T as TryInto<usize>>::Error: Debug,
444            <T as TryFrom<usize>>::Error: Debug,
445            <isize as TryFrom<T>>::Error: Debug,
446        {
447            type Output = BoolVar<T>;
448            fn $v(self, rhs: Self) -> Self::Output {
449                BoolVar::<T>(self.0.clone().$v(rhs.0.clone()))
450            }
451        }
452
453        // for BoolExprNodes
454        new_op_from_impl!($t, $v, BoolExprNode);
455        new_op_from_impl!($t, $v, Literal);
456
457        // for booleans
458        impl<T> $t<bool> for BoolVar<T>
459        where
460            T: VarLit + Neg<Output = T> + Debug,
461            isize: TryFrom<T>,
462            <T as TryInto<usize>>::Error: Debug,
463            <T as TryFrom<usize>>::Error: Debug,
464            <isize as TryFrom<T>>::Error: Debug,
465        {
466            type Output = BoolVar<T>;
467            fn $v(self, rhs: bool) -> Self::Output {
468                Self(self.0.$v(rhs))
469            }
470        }
471        impl<T> $t<&bool> for BoolVar<T>
472        where
473            T: VarLit + Neg<Output = T> + Debug,
474            isize: TryFrom<T>,
475            <T as TryInto<usize>>::Error: Debug,
476            <T as TryFrom<usize>>::Error: Debug,
477            <isize as TryFrom<T>>::Error: Debug,
478        {
479            type Output = BoolVar<T>;
480            fn $v(self, rhs: &bool) -> Self::Output {
481                Self(self.0.$v(*rhs))
482            }
483        }
484        impl<T> $t<bool> for &BoolVar<T>
485        where
486            T: VarLit + Neg<Output = T> + Debug,
487            isize: TryFrom<T>,
488            <T as TryInto<usize>>::Error: Debug,
489            <T as TryFrom<usize>>::Error: Debug,
490            <isize as TryFrom<T>>::Error: Debug,
491        {
492            type Output = BoolVar<T>;
493            fn $v(self, rhs: bool) -> Self::Output {
494                BoolVar::<T>(self.0.clone().$v(rhs))
495            }
496        }
497        impl<T> $t<&bool> for &BoolVar<T>
498        where
499            T: VarLit + Neg<Output = T> + Debug,
500            isize: TryFrom<T>,
501            <T as TryInto<usize>>::Error: Debug,
502            <T as TryFrom<usize>>::Error: Debug,
503            <isize as TryFrom<T>>::Error: Debug,
504        {
505            type Output = BoolVar<T>;
506            fn $v(self, rhs: &bool) -> Self::Output {
507                BoolVar::<T>(self.0.clone().$v(*rhs))
508            }
509        }
510
511        impl<T> $t<BoolVar<T>> for bool
512        where
513            T: VarLit + Neg<Output = T> + Debug,
514            isize: TryFrom<T>,
515            <T as TryInto<usize>>::Error: Debug,
516            <T as TryFrom<usize>>::Error: Debug,
517            <isize as TryFrom<T>>::Error: Debug,
518        {
519            type Output = BoolVar<T>;
520            fn $v(self, rhs: BoolVar<T>) -> Self::Output {
521                BoolVar::<T>(self.$v(rhs.0))
522            }
523        }
524        impl<T> $t<&BoolVar<T>> for bool
525        where
526            T: VarLit + Neg<Output = T> + Debug,
527            isize: TryFrom<T>,
528            <T as TryInto<usize>>::Error: Debug,
529            <T as TryFrom<usize>>::Error: Debug,
530            <isize as TryFrom<T>>::Error: Debug,
531        {
532            type Output = BoolVar<T>;
533            fn $v(self, rhs: &BoolVar<T>) -> Self::Output {
534                BoolVar::<T>(self.$v(rhs.0.clone()))
535            }
536        }
537        impl<T> $t<BoolVar<T>> for &bool
538        where
539            T: VarLit + Neg<Output = T> + Debug,
540            isize: TryFrom<T>,
541            <T as TryInto<usize>>::Error: Debug,
542            <T as TryFrom<usize>>::Error: Debug,
543            <isize as TryFrom<T>>::Error: Debug,
544        {
545            type Output = BoolVar<T>;
546            fn $v(self, rhs: BoolVar<T>) -> Self::Output {
547                BoolVar::<T>((*self).$v(rhs.0))
548            }
549        }
550        impl<T> $t<&BoolVar<T>> for &bool
551        where
552            T: VarLit + Neg<Output = T> + Debug,
553            isize: TryFrom<T>,
554            <T as TryInto<usize>>::Error: Debug,
555            <T as TryFrom<usize>>::Error: Debug,
556            <isize as TryFrom<T>>::Error: Debug,
557        {
558            type Output = BoolVar<T>;
559            fn $v(self, rhs: &BoolVar<T>) -> Self::Output {
560                BoolVar::<T>((*self).$v(rhs.0.clone()))
561            }
562        }
563    };
564}
565
566new_op_impl!(BitAnd, bitand);
567new_op_impl!(BitOr, bitor);
568new_op_impl!(BitXor, bitxor);
569new_op_impl!(BoolEqual, bequal);
570new_op_impl!(BoolImpl, imp);
571
572macro_rules! new_opassign_impl {
573    ($t:ident, $v:ident) => {
574        impl<T> $t for BoolVar<T>
575        where
576            T: VarLit + Neg<Output = T> + Debug,
577            isize: TryFrom<T>,
578            <T as TryInto<usize>>::Error: Debug,
579            <T as TryFrom<usize>>::Error: Debug,
580            <isize as TryFrom<T>>::Error: Debug,
581        {
582            fn $v(&mut self, rhs: BoolVar<T>) {
583                self.0.$v(rhs.0)
584            }
585        }
586        impl<T> $t<&BoolVar<T>> for BoolVar<T>
587        where
588            T: VarLit + Neg<Output = T> + Debug,
589            isize: TryFrom<T>,
590            <T as TryInto<usize>>::Error: Debug,
591            <T as TryFrom<usize>>::Error: Debug,
592            <isize as TryFrom<T>>::Error: Debug,
593        {
594            fn $v(&mut self, rhs: &BoolVar<T>) {
595                self.0.$v(rhs.0.clone())
596            }
597        }
598        impl<T> $t<BoolExprNode<T>> for BoolVar<T>
599        where
600            T: VarLit + Neg<Output = T> + Debug,
601            isize: TryFrom<T>,
602            <T as TryInto<usize>>::Error: Debug,
603            <T as TryFrom<usize>>::Error: Debug,
604            <isize as TryFrom<T>>::Error: Debug,
605        {
606            fn $v(&mut self, rhs: BoolExprNode<T>) {
607                self.0.$v(rhs)
608            }
609        }
610        impl<T> $t<&BoolExprNode<T>> for BoolVar<T>
611        where
612            T: VarLit + Neg<Output = T> + Debug,
613            isize: TryFrom<T>,
614            <T as TryInto<usize>>::Error: Debug,
615            <T as TryFrom<usize>>::Error: Debug,
616            <isize as TryFrom<T>>::Error: Debug,
617        {
618            fn $v(&mut self, rhs: &BoolExprNode<T>) {
619                self.0.$v(rhs.clone())
620            }
621        }
622        impl<T> $t<Literal<T>> for BoolVar<T>
623        where
624            T: VarLit + Neg<Output = T> + Debug,
625            isize: TryFrom<T>,
626            <T as TryInto<usize>>::Error: Debug,
627            <T as TryFrom<usize>>::Error: Debug,
628            <isize as TryFrom<T>>::Error: Debug,
629        {
630            fn $v(&mut self, rhs: Literal<T>) {
631                self.0.$v(rhs)
632            }
633        }
634        impl<T> $t<&Literal<T>> for BoolVar<T>
635        where
636            T: VarLit + Neg<Output = T> + Debug,
637            isize: TryFrom<T>,
638            <T as TryInto<usize>>::Error: Debug,
639            <T as TryFrom<usize>>::Error: Debug,
640            <isize as TryFrom<T>>::Error: Debug,
641        {
642            fn $v(&mut self, rhs: &Literal<T>) {
643                self.0.$v(rhs.clone())
644            }
645        }
646        impl<T> $t<bool> for BoolVar<T>
647        where
648            T: VarLit + Neg<Output = T> + Debug,
649            isize: TryFrom<T>,
650            <T as TryInto<usize>>::Error: Debug,
651            <T as TryFrom<usize>>::Error: Debug,
652            <isize as TryFrom<T>>::Error: Debug,
653        {
654            fn $v(&mut self, rhs: bool) {
655                self.0.$v(rhs)
656            }
657        }
658        impl<T> $t<&bool> for BoolVar<T>
659        where
660            T: VarLit + Neg<Output = T> + Debug,
661            isize: TryFrom<T>,
662            <T as TryInto<usize>>::Error: Debug,
663            <T as TryFrom<usize>>::Error: Debug,
664            <isize as TryFrom<T>>::Error: Debug,
665        {
666            fn $v(&mut self, rhs: &bool) {
667                self.0.$v(*rhs)
668            }
669        }
670    };
671}
672
673new_opassign_impl!(BitAndAssign, bitand_assign);
674new_opassign_impl!(BitOrAssign, bitor_assign);
675new_opassign_impl!(BitXorAssign, bitxor_assign);
676
677pub use crate::boolexpr::{bool_ite, full_adder, half_adder};
678
679pub fn bool_ite_r<T, I0, I1, I2>(c: &I0, t: &I1, e: &I2) -> BoolVar<T>
680where
681    T: VarLit + Neg<Output = T> + Debug,
682    isize: TryFrom<T>,
683    <T as TryInto<usize>>::Error: Debug,
684    <T as TryFrom<usize>>::Error: Debug,
685    <isize as TryFrom<T>>::Error: Debug,
686    I0: Into<BoolVar<T>> + Clone,
687    I1: Into<BoolVar<T>> + Clone,
688    I2: Into<BoolVar<T>> + Clone,
689{
690    let c: BoolVar<T> = (c.clone()).into();
691    let t: BoolVar<T> = (t.clone()).into();
692    let e: BoolVar<T> = (e.clone()).into();
693    bool_ite(c, t, e)
694}
695
696/// Returns result of the If-Then-Else (ITE) - bitwise version. Optimized version.
697pub fn bool_opt_ite<T>(c: BoolVar<T>, t: BoolVar<T>, e: BoolVar<T>) -> BoolVar<T>
698where
699    T: VarLit + Neg<Output = T> + Debug,
700    isize: TryFrom<T>,
701    <T as TryInto<usize>>::Error: Debug,
702    <T as TryFrom<usize>>::Error: Debug,
703    <isize as TryFrom<T>>::Error: Debug,
704{
705    BoolVar(crate::boolexpr::bool_opt_ite(c.0, t.0, e.0))
706}
707
708pub fn bool_opt_ite_r<T, I0, I1, I2>(c: &I0, t: &I1, e: &I2) -> BoolVar<T>
709where
710    T: VarLit + Neg<Output = T> + Debug,
711    isize: TryFrom<T>,
712    <T as TryInto<usize>>::Error: Debug,
713    <T as TryFrom<usize>>::Error: Debug,
714    <isize as TryFrom<T>>::Error: Debug,
715    I0: Into<BoolVar<T>> + Clone,
716    I1: Into<BoolVar<T>> + Clone,
717    I2: Into<BoolVar<T>> + Clone,
718{
719    let c: BoolVar<T> = (c.clone()).into();
720    let t: BoolVar<T> = (t.clone()).into();
721    let e: BoolVar<T> = (e.clone()).into();
722    bool_opt_ite(c, t, e)
723}
724
725pub fn opt_full_adder_r<T, I0, I1, I2>(a: &I0, b: &I1, c: &I2) -> (BoolVar<T>, BoolVar<T>)
726where
727    T: VarLit + Neg<Output = T> + Debug,
728    isize: TryFrom<T>,
729    <T as TryInto<usize>>::Error: Debug,
730    <T as TryFrom<usize>>::Error: Debug,
731    <isize as TryFrom<T>>::Error: Debug,
732    I0: Into<BoolVar<T>> + Clone,
733    I1: Into<BoolVar<T>> + Clone,
734    I2: Into<BoolVar<T>> + Clone,
735{
736    let a: BoolVar<T> = (a.clone()).into();
737    let b: BoolVar<T> = (b.clone()).into();
738    let c: BoolVar<T> = (c.clone()).into();
739    opt_full_adder(a, b, c)
740}
741
742pub fn opt_full_adder<T, I0, I1, I2>(a: I0, b: I1, c: I2) -> (BoolVar<T>, BoolVar<T>)
743where
744    T: VarLit + Neg<Output = T> + Debug,
745    isize: TryFrom<T>,
746    <T as TryInto<usize>>::Error: Debug,
747    <T as TryFrom<usize>>::Error: Debug,
748    <isize as TryFrom<T>>::Error: Debug,
749    I0: Into<BoolVar<T>>,
750    I1: Into<BoolVar<T>>,
751    I2: Into<BoolVar<T>>,
752{
753    let a: BoolVar<T> = a.into();
754    let b: BoolVar<T> = b.into();
755    let c: BoolVar<T> = c.into();
756    if a.value().is_some() {
757        full_adder(b, c, a)
758    } else if b.value().is_some() {
759        full_adder(a, c, b)
760    } else {
761        full_adder(a, b, c)
762    }
763}
764
765pub type BoolVar16 = BoolVar<i16>;
766pub type BoolVar32 = BoolVar<i32>;
767pub type BoolVarSys = BoolVar<isize>;
cnfgen/boolvar.rs

cnfgen/
boolvar.rs
