logicng 0.1.0-alpha.3

//! The formula factory for LogicNG.
//!
//! New formulas can only be generated by a formula factory.  It is implemented
//! s.t. it is guaranteed that equivalent formulas (in terms of associativity
//! and commutativity) are hold exactly once in memory.


use std::collections::{HashMap, HashSet};
use std::str::FromStr;
use std::sync::atomic::{AtomicUsize, Ordering};
use std::sync::OnceLock;

use pest::error::Error;
use regex::Regex;

use CType::{EQ, LE, LT};

use crate::datastructures::Assignment;
use crate::formulas::formula_cache::formula_factory_caches::FormulaFactoryCaches;
use crate::formulas::formula_cache::simple_cache::SimpleCache;
use crate::formulas::CType::{GE, GT};
use crate::formulas::Literal::Pos;
use crate::formulas::{AuxVarType, CType, CardinalityConstraint, EncodedFormula, FormulaFactoryConfig, Literal, PbConstraint, Variable};
use crate::operations::transformations::{self, CnfEncoder, Substitution};
use crate::parser::pseudo_boolean_parser::{parse, Rule};

use super::formula_cache::equivalence_cache::EquivalenceCache;
use super::formula_cache::formula_encoding::{Encoding, FormulaEncoding, SmallFormulaEncoding};
use super::formula_cache::implication_cache::ImplicationCache;
use super::formula_cache::nary_formula_cache::NaryFormulaCache;
use super::formula_cache::not_cache::NotCache;
use super::{Formula, FormulaType, LitType, VarType};

const FF_ID_LENGTH: i32 = 4;

pub(super) const AUX_PREFIX: &str = "@RESERVED_";
pub(super) const AUX_REGEX: &str = "^@RESERVED_(?P<FF_ID>[0-9A-Z]*)_(?P<AUX_TYPE>(CNF)|(CC)|(PB))_(?P<INDEX>[0-9]+)$";

static AUX_REGEX_LOCK: OnceLock<Regex> = OnceLock::new(); // TODO replace with LazyLock once available

type FilterResult = (Vec<SmallFormulaEncoding>, HashSet<SmallFormulaEncoding>, Vec<FormulaEncoding>, HashSet<FormulaEncoding>);

/// The formula factory is the central concept of LogicNG and is always required
/// when working with LogicNG.  A formula factory is an object consisting of two
/// major components:
///
/// A *factory*, which creates formulas, and a *container*, which stores created
/// formulas.
///
/// The *container function* is 'smart': A formula factory guarantees that
/// syntactically equivalent formulas are created only once.  This mechanism
/// also extends to variants of the formula in terms of associativity and
/// commutativity. Therefore, if the user creates formulas for
///
/// ```
/// # use logicng::formulas::{FormulaFactory, ToFormula};
/// # let f = FormulaFactory::new();
///
/// let f1 = "A & B".to_formula(&f);
/// let f2 = "B & A".to_formula(&f);
/// let f3 = "(B & A)".to_formula(&f);
///
/// assert_eq!(f1, f2);
/// assert_eq!(f1, f3);
/// assert_eq!(f2, f3);
/// ```
///
/// all of them are represented by only one formula in memory.  This approach is
/// only possible, because formulas in LogicNG are immutable data structures. So
/// once created, a formula can never be altered again.
///
/// In order to use the fact that formula factories avoid unnecessary formula
/// creations, it is generally recommended to use only *one* formula factory for
/// a certain task.
///
/// # Invariants and Simplifications
///
/// Formulas in LogicNG cannot be constructed directly but must be created by an
/// instance of a `FormulaFactory`. This factory ensures the following six
/// invariants:
///
/// 1. A constant (`true` or `false`) cannot be an operand to any other formula,
///    i.e. constants are automatically removed.
/// 2. The operand of a conjunction may not be another conjunction; the same
///    applies to disjunctions. These cases are merged in one big
///    conjunction/disjunction.
/// 3. The operand of a negation may only be a binary operator, an n-ary
///    operator or a pseudo-Boolean constraint. For other operands the
///    respective simplifications are performed.
/// 4. An n-ary operator has unique operands.  Duplicate operands in a
///    disjunction or conjunction are filtered.
/// 5. Every positive literal is guaranteed to be an instance of class
///    `Variable`.
/// 6. Inverse operands of an n-ary operator are simplified, this means `f1 &
///    ~f1` is parsed to `$false`, and `f1 | ~f1` is parsed to `$true`.
///
/// Furthermore, some further simplifications are performed when parsing or
/// creating formulas, such as `A <=> A` is equivalent to `$true`, or `A <=> ~A`
/// is equivalent to `$false`.
///
/// While being rather easy to realize, these restrictions simplify reasoning
/// about the structure of a formula and thus significantly reduce the number of
/// corner cases algorithms have to face.
///
/// Together with the smart container function presented in the last section,
/// the example can be extended.  Not only are formulas `A & B`, `B & A`, or `(B
/// & A)` represented by only one formula object in memory, but also variants
/// like
///
/// ```
/// # use logicng::formulas::{FormulaFactory, ToFormula};
/// # let f = FormulaFactory::new();
///
/// let f1 = "A & A & B".to_formula(&f);
/// let f2 = "B & A & $true".to_formula(&f);
/// let f3 = "(B & A) & B & ($false | A) & ($true | C)".to_formula(&f);
///
/// assert_eq!(f1, f2);
/// assert_eq!(f1, f3);
/// assert_eq!(f2, f3);
/// ```
///
/// # Formulas in `LogicNG Rust`
///
/// Formulas in `LogicNG Rust` are a bit unintuitive. Especially if you are used
/// to `LogicNG Java`. There are two relevant types for formulas:
/// [`EncodedFormula`] and [`Formula`].
///
/// Unexpectedly, `EncodedFormula` is the more important data type, this holds
/// all the information necessary to identify the formula in the
/// `FormulaFactory`. So in general a `FormulaFactory` will only accept and
/// return `EncodedFormulas`.
///
/// `Formula`, on the other hand, is a helper type, which is designed to allow
/// you to extract information from a `EncodedFormula`. You can use
/// [`EncodedFormula::unpack`] to get a `Formula`, on which you can then apply
/// pattern matching to extract type and the operands of the formula. A
/// `Formula` can have a shared reference to objects in the `FormulaFactory`.
/// The current design of `LogicNG Rust`, however, requires for most functions
/// an exclusive reference of the `FormulaFactory`. So the borrow
/// checker will not allow to call such functions as long as a `Formula`
/// exists. So you should drop a `Formula` as soon as possible.
///
/// # Creating formulas with a `FormulaFactory`
///
/// There are two ways to create formulas using a `FormulaFactory`:
///
/// Firstly, one can parse a formula from a string: E.g. `f.parse("A & B");` or
/// `"A & B".to_formula(f)`. (`to_formula()` panics if the string is not a valid
/// formula, but `f.parse()` returns a result and, therefore, an error if
/// parsing fails.)
///
/// Secondly, one can create a formula of a certain type with the methods for
/// formula creation in the `FormulaFactory`. An overview about how to create
/// those formulas is here:
///
/// | Object      | Factory Method           | Syntax                              |
/// |-------------|--------------------------|-------------------------------------|
/// | True        | `f.verum()`              | `$true`                             |
/// | False       | `f.falsum()`             | `$false`                            |
/// | Variable    | `f.variable("A")`        | `A`                                 |
/// | Literal     | `f.literal("A", false)`  | `~A`                                |
/// | Negation    | `f.not(f1)`              | `~f1`                               |
/// | Implication | `f.implication(f1, f2)`  | `f1 => f2`                          |
/// | Equivalence | `f.equivalence(f1, f2)`  | `f1 <=> f2`                         |
/// | Conjunction | `f.and(vec![f1, f2, f3])`| `f1 & f2 & f3`                      |
/// | Disjunction | `f.or(vec![f1, f2, f3])` | <code>f1 &vert; f2 &vert; f3</code> |
///
/// The order of operands in the resulting formula does not follow an overall
/// ordering but depends on the formulas created first. If a formula `B & A` was
/// created, the order of the operands will be always `B, A`. Thus, when
/// creating another formula `A & B` it will result in `B & A`. If another
/// formula `A & B & C` is created, the operands occur in the order `A, B, C`,
/// since `A & B & C` was the first created formula.
///
/// It is also possible to write Pseudo-Boolean constraints, especially
/// cardinality constraints like e.g. `A + B + C <= 1`:
///
/// ```
/// # use logicng::formulas::{FormulaFactory, CType};
/// # let f = FormulaFactory::new();
/// let vars = vec![f.var("A"), f.var("B"), f.var("C")];
/// f.cc(CType::LE, 1, vars);
/// ```
///
/// which means from variables `A`, `B`, `C` can be at most one variable
/// assigned to true. An example for a Pseudo-Boolean constraint is
/// `A + 2* ~B - 3*C = 2`:
///
/// ```
/// # use logicng::formulas::{FormulaFactory, CType};
/// # let f = FormulaFactory::new();
/// let lits = vec![f.lit("A", true), f.lit("B", false), f.lit("C", true)];
/// let coeffs = vec![1, 2, -3];
/// f.pbc(CType::EQ, 2, lits, coeffs);
/// ```
///
/// Beside the mentioned factory methods there are many convenience methods to
/// create formulas. Examples are:
///
/// - `constant(value: bool)` which creates a `$true` or `$false` constant
///   depending on the given Boolean value
/// - `clause(literals: &[Literal])` creating a clause for the given literals
///
/// ```
/// # use logicng::formulas::FormulaFactory;
/// # let f = FormulaFactory::new();
/// f.constant(true); //$true
/// f.constant(false); //$false
///
/// let lits = &[f.lit("A", true), f.lit("B", false), f.lit("C", true)];
/// f.clause(lits);
/// ```
///
/// # Thread Safety
///
/// A formula factory has many internal data structures which are not thread
/// safe. Therefore, a formula factory does not implement `Sync`. Different
/// threads accessing the same formula factory at the same time could lead to
/// concurrency exceptions, undefined behaviour, and incorrect computations. In
/// a multi-threaded application, each thread should have its own formula
/// factory on which it operates.
pub struct FormulaFactory {
    pub(crate) id: String,
    /// Configuration
    pub config: FormulaFactoryConfig,
    pub(crate) variables: SimpleCache<String>,
    pub(crate) ands: NaryFormulaCache,
    pub(crate) ors: NaryFormulaCache,
    pub(crate) nots: NotCache,
    pub(crate) impls: ImplicationCache,
    pub(crate) equivs: EquivalenceCache,
    // TODO: Memory-efficient encodings for CCs and PBCs (Variables/Literals and optionally the CType should be encoded)
    pub(crate) ccs: SimpleCache<CardinalityConstraint>,
    pub(crate) pbcs: SimpleCache<PbConstraint>,
    cnf_counter: AtomicUsize,
    cc_counter: AtomicUsize,
    pb_counter: AtomicUsize,
    pub(crate) caches: FormulaFactoryCaches,
}

impl Default for FormulaFactory {
    fn default() -> Self {
        Self::new()
    }
}

impl FormulaFactory {
    /// Creates a new `FormulaFactory`.
    ///
    /// It will generate a random ID to identify the `FormulaFactory`. If you
    /// need to specify a custom ID, you can use [`with_id`].
    ///
    /// [`with_id`]: FormulaFactory::with_id
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// use logicng::formulas::FormulaFactory;
    ///
    /// let f = FormulaFactory::new();
    /// ```
    pub fn new() -> Self {
        Self::with_id(&generate_random_id())
    }

    /// Creates a new `FormulaFactory` with the specified `id`.
    ///
    /// The ID is used to identify the `FormulaFactory`. If you don't need to
    /// specify a ID, we suggest to use [`new`], which will create a random ID.
    ///
    /// [`new`]: FormulaFactory::new
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// use logicng::formulas::FormulaFactory;
    ///
    /// let my_id = "MyOwnFactory";
    /// let f = FormulaFactory::with_id(my_id);
    /// assert_eq!(f.id(), my_id);
    /// ```
    pub fn with_id(id: &str) -> Self {
        Self {
            id: id.into(),
            config: FormulaFactoryConfig::new(),
            variables: SimpleCache::new(),
            ands: NaryFormulaCache::new(FormulaType::And),
            ors: NaryFormulaCache::new(FormulaType::Or),
            nots: NotCache::new(),
            impls: ImplicationCache::new(),
            equivs: EquivalenceCache::new(),
            ccs: SimpleCache::new(),
            pbcs: SimpleCache::new(),
            cnf_counter: AtomicUsize::new(0),
            cc_counter: AtomicUsize::new(0),
            pb_counter: AtomicUsize::new(0),
            caches: FormulaFactoryCaches::new(),
        }
    }

    /// Parses a given string to a formula using a Pseudo-Boolean parser.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::{FormulaFactory, EncodedFormula, CType};
    /// # use std::error::Error;
    /// # fn main() -> Result<(), Box<dyn Error>> {
    /// let f = FormulaFactory::new();
    ///
    /// let input1 = "~a";
    /// let input2 = "a & b";
    /// let input3 = "a + b = 1";
    ///
    /// let parsed1 = f.parse(input1)?;
    /// let parsed2 = f.parse(input2)?;
    /// let parsed3 = f.parse(input3)?;
    ///
    /// let expected1 = f.literal("a", false);
    ///
    /// let b = f.var("b");
    /// let a = f.var("a");
    /// let expected2 = f.and(&[EncodedFormula::from(a), EncodedFormula::from(b)]);
    /// let expected3 = f.cc(CType::EQ, 1, vec![a, b]);
    ///
    /// assert_eq!(parsed1, expected1);
    /// assert_eq!(parsed2, expected2);
    /// assert_eq!(parsed3, expected3);
    /// # Ok(())
    /// # }
    /// ```
    pub fn parse(&self, input: &str) -> Result<EncodedFormula, Box<Error<Rule>>> {
        parse(self, input)
    }

    /// Returns the constant `True`.
    ///
    /// This function is equivalent to [`EncodedFormula::constant(true)`], which
    /// you can call without a reference to a `FormulaFactory`. This also means
    /// that a constant is independent of a factory.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use logicng::formulas::FormulaType;
    /// let f = FormulaFactory::new();
    ///
    /// let verum = f.verum();
    /// assert_eq!(verum.formula_type(), FormulaType::True);
    /// ```
    #[allow(clippy::unused_self)]
    pub fn verum(&self) -> EncodedFormula {
        EncodedFormula::from(FormulaEncoding::encode_type(FormulaType::True))
    }

    /// Returns the constant `False`.
    ///
    /// This function is equivalent to [`EncodedFormula::constant(false)`],
    /// which you can call without a reference to a `FormulaFactory`. This also
    /// means that a constant is independent of a factory.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use logicng::formulas::FormulaType;
    /// let f = FormulaFactory::new();
    ///
    /// let falsum = f.falsum();
    /// assert_eq!(falsum.formula_type(), FormulaType::False);
    /// ```
    #[allow(clippy::unused_self)]
    pub fn falsum(&self) -> EncodedFormula {
        EncodedFormula::from(FormulaEncoding::encode_type(FormulaType::False))
    }

    /// Returns the constant `True` or `False` based on `value`.
    ///
    /// This function is equivalent to [`EncodedFormula::constant`], which you
    /// can call without a reference to a `FormulaFactory`. This also means that
    /// a constant is independent of a factory.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::{FormulaFactory, FormulaType, EncodedFormula};
    /// let f = FormulaFactory::new();
    ///
    /// assert_eq!(f.constant(true).formula_type(), FormulaType::True);
    /// assert_eq!(f.constant(false).formula_type(), FormulaType::False);
    /// assert_eq!(f.constant(true), EncodedFormula::constant(true));
    /// assert_eq!(f.constant(false), EncodedFormula::constant(false));
    /// ```
    pub fn constant(&self, value: bool) -> EncodedFormula {
        if value {
            self.verum()
        } else {
            self.falsum()
        }
    }

    /// Creates a new [`Variable`] instance with the given name and registers it
    /// in this `FormulaFactory`. If a variable with that name already exists,
    /// no new variable will be added.
    ///
    /// `Variable` is an explicit datatype for handling variables. If a
    /// functions only needs variables, it will probably ask for this explicit
    /// datatype. In many contexts, however, a function not only wants
    /// variables, but formulas in general. For these applications you might
    /// want to use [`variable`], which immediately returns a variable as an
    /// [`EncodedFormula`].
    ///
    /// A `Variable` makes only sense in the context of the `FormulaFactory`
    /// it was created in. Using it in the context of another `FormulaFactory`
    /// results in undefined behavior.
    ///
    /// [`variable`]: FormulaFactory::variable
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// let f = FormulaFactory::new();
    ///
    /// let var = f.var("MyVar");
    ///
    /// assert_eq!(var.name(&f).into_owned(), "MyVar");
    /// ```
    pub fn var(&self, name: &str) -> Variable {
        Variable::try_from(self.variable(name)).unwrap()
    }

    /// Creates a new variable with the given name and returns the variable as an
    /// [`EncodedFormula`]. If a variable with that name already exists, no new
    /// variable will be added.
    ///
    /// If you are interested in a new variable as the explicit datatype
    /// [`Variable`], you can instead use [`var`], which will do exactly the
    /// same, but not converting the type to a [`EncodedFormula`] in the end.
    ///
    /// A variable encoded as an [`EncodedFormula`] makes only sense in the
    /// context of the `FormulaFactory` it was created in. Using it in the
    /// context of another `FormulaFactory` results in undefined behavior.
    ///
    /// [`var`]: FormulaFactory::var
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::{FormulaFactory, EncodedFormula};
    /// let f = FormulaFactory::new();
    ///
    /// let formula = f.variable("MyVar");
    ///
    /// assert_eq!(formula.to_string(&f), "MyVar");
    /// assert_eq!(formula, EncodedFormula::from(f.var("MyVar")));
    /// ```
    pub fn variable(&self, name: &str) -> EncodedFormula {
        EncodedFormula::from(self.variables.get_or_insert(name.into(), FormulaType::Lit(LitType::Pos(VarType::FF))))
    }

    /// Creates a new variable with the given name and returns the variable as a
    /// [`EncodedFormula`]. In identifies auxiliary variables of _LogicNG_ and adds
    /// them as such. In all other cases it behaves the same as [`variable`],
    /// which you should use, if you don't import variables exported by
    /// _LogicNG_.
    ///
    /// [`variable`]: FormulaFactory::variable
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// let f = FormulaFactory::new();
    ///
    /// let _ = f.parsed_variable("MyVar"); //Normal variable
    /// let _ = f.parsed_variable("@RESERVED_00_CNF_00"); //Auxiliary variable
    /// ```
    pub fn parsed_variable(&self, name: &str) -> EncodedFormula {
        let aux_regex = AUX_REGEX_LOCK.get_or_init(|| Regex::new(AUX_REGEX).unwrap());
        aux_regex.captures(name).map_or_else(
            || self.variable(name),
            |captures| {
                if captures["FF_ID"] == self.id {
                    let aux_type = AuxVarType::from_str(&captures["AUX_TYPE"]).unwrap();
                    let index = captures["INDEX"].parse::<u64>().unwrap();
                    Pos(Variable::Aux(aux_type, index)).into()
                } else {
                    self.variable(name)
                }
            },
        )
    }

    /// Creates a new [`Literal`] instance with the given name and phase. If no
    /// variable with the corresponding name exists yet, it will be added to the
    /// `FormulaFactory`.
    ///
    /// `Literal` is a explicit datatype for handling literals. If a functions
    /// only needs literals, it will probably ask for this explicit datatype. In
    /// many contexts, however, a function not only wants literals, but formulas
    /// in general. For these applications you might want to use [`literal`],
    /// which immediately returns a literal as a [`EncodedFormula`].
    ///
    /// A `Literal` is always based on a [`Variable`]. If you only need a
    /// variable, you should instead use [`var`] or [`variable`]. Or you can use
    /// [`Literal::new`] to create a new literal with an existing variable.
    ///
    /// A `Literal` makes only sense in the context of the `FormulaFactory` it
    /// was created in. Using it in the context of another `FormulaFactory`
    /// results in undefined behavior.
    ///
    /// [`var`]: FormulaFactory::var
    /// [`variable`]: FormulaFactory::variable
    /// [`literal`]: FormulaFactory::literal
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// let f = FormulaFactory::new();
    ///
    /// let lit = f.lit("A", false);
    ///
    /// assert_eq!(lit.name(&f).into_owned(), "A");
    /// assert_eq!(lit.to_string(&f), "~A");
    /// ```
    pub fn lit(&self, name: &str, phase: bool) -> Literal {
        Literal::new(self.var(name), phase)
    }

    /// Creates a new literal with the given name and phase and returns it as a
    /// [`EncodedFormula`]. If no variable with the corresponding name exists
    /// yet, it will be added to the `FormulaFactory`.
    ///
    /// If you are interested in a new literal as the explicit datatype
    /// [`Literal`], you can instead use [`lit`], which will do exactly the
    /// same, but not converting the type in the end.
    ///
    /// A `Literal` depends on a [`Variable`]. If you only need a variable, you
    /// should instead use [`var`] or [`variable`]. Or you can use
    /// [`Literal::new`] to create a new literal with an existing variable.
    ///
    /// A `Literal` makes only sense in the context of the `FormulaFactory` it
    /// was created in. Using it in the context of another `FormulaFactory`
    /// results in undefined behavior.
    ///
    /// [`var`]: FormulaFactory::var
    /// [`variable`]: FormulaFactory::variable
    /// [`lit`]: FormulaFactory::lit
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::{FormulaFactory, EncodedFormula};
    /// let f = FormulaFactory::new();
    ///
    /// let formula1 = f.literal("MyLiteral", true);
    /// let formula2 = f.literal("MyLiteral", false);
    ///
    /// assert_eq!(formula1.to_string(&f), "MyLiteral");
    /// assert_eq!(formula2.to_string(&f), "~MyLiteral");
    /// assert_eq!(formula2, EncodedFormula::from(f.lit("MyLiteral", false)));
    /// ```
    pub fn literal(&self, name: &str, phase: bool) -> EncodedFormula {
        EncodedFormula::from(self.lit(name, phase))
    }

    /// Creates a new conjunction from a vector of formulas.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.variable("a");
    /// let b = f.literal("b", false);
    /// let c = f.literal("c", false);
    ///
    /// let conjunction = f.and(&[a, b, c]);
    ///
    /// assert_eq!(conjunction, "a & ~b & ~c".to_formula(&f));
    /// ```
    pub fn and(&self, operands: &[EncodedFormula]) -> EncodedFormula {
        match self.filter(operands, FormulaType::And) {
            None => self.falsum(),
            Some((new_ops32, new_set32, new_ops64, new_set64)) => {
                if new_ops32.is_empty() && new_ops64.is_empty() {
                    self.verum()
                } else if new_ops32.len() == 1 && new_ops64.is_empty() {
                    new_ops32[0].to_formula()
                } else if new_ops32.is_empty() && new_ops64.len() == 1 {
                    new_ops64[0].to_formula()
                } else {
                    EncodedFormula::from(self.ands.get_or_insert(new_ops32, new_set32, new_ops64, new_set64))
                }
            }
        }
    }

    /// Creates a new disjunction from a vector of formulas.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.variable("a");
    /// let b = f.literal("b", false);
    /// let c = f.literal("c", false);
    ///
    /// let disjunction = f.or(&[a, b, c]);
    ///
    /// assert_eq!(disjunction, "a | ~b | ~c".to_formula(&f));
    /// ```
    pub fn or(&self, operands: &[EncodedFormula]) -> EncodedFormula {
        match self.filter(operands, FormulaType::Or) {
            None => self.verum(),
            Some((new_ops32, new_set32, new_ops64, new_set64)) => {
                if new_ops32.is_empty() && new_ops64.is_empty() {
                    self.falsum()
                } else if new_ops32.len() == 1 && new_ops64.is_empty() {
                    new_ops32[0].to_formula()
                } else if new_ops32.is_empty() && new_ops64.len() == 1 {
                    new_ops64[0].to_formula()
                } else {
                    EncodedFormula::from(self.ors.get_or_insert(new_ops32, new_set32, new_ops64, new_set64))
                }
            }
        }
    }

    /// Creates a new _CNF_ clause from a slice of literals.
    ///
    /// If you want to create a clause out of literals in an [`EncodedFormula`]
    /// representation, you should instead use [`or`].
    ///
    /// [`or`]: FormulaFactory::or
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.lit("a", true);
    /// let b = f.lit("b", false);
    /// let c = f.lit("c", false);
    ///
    /// let clause = f.clause(&[a, b, c]);
    ///
    /// assert_eq!(clause, "a | ~b | ~c".to_formula(&f));
    /// ```
    pub fn clause(&self, operands: &[Literal]) -> EncodedFormula {
        self.or(&operands.iter().map(|&lit| lit.into()).collect::<Box<[_]>>())
    }

    /// Creates a new implication, where `left` implies `right`.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let left = f.literal("a", true);
    /// let right = f.literal("b", false);
    ///
    /// let implication = f.implication(left, right);
    ///
    /// assert_eq!(implication, "a => ~b".to_formula(&f));
    /// ```
    pub fn implication(&self, left: EncodedFormula, right: EncodedFormula) -> EncodedFormula {
        if left.is_verum() {
            right
        } else if left.is_falsum() || right.is_verum() {
            self.verum()
        } else if right.is_falsum() {
            self.not(left)
        } else if left == right {
            self.verum()
        } else {
            EncodedFormula::from(self.impls.get_or_insert((left, right)))
        }
    }

    /// Creates a new equivalence between `left` and `right`.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let left = f.literal("a", true);
    /// let right = f.literal("b", false);
    ///
    /// let equivalence = f.equivalence(left, right);
    ///
    /// assert_eq!(equivalence, "a <=> ~b".to_formula(&f));
    /// ```
    pub fn equivalence(&self, left: EncodedFormula, right: EncodedFormula) -> EncodedFormula {
        if left.is_verum() {
            right
        } else if left.is_falsum() {
            self.not(right)
        } else if right.is_verum() {
            left
        } else if right.is_falsum() {
            self.not(left)
        } else if left == right {
            self.verum()
        } else if left == self.negate(right) {
            self.falsum()
        } else {
            EncodedFormula::from(self.equivs.get_or_insert((left, right)))
        }
    }

    /// Creates the negation of the given formula.
    ///
    /// For simple formulas, such as _constants_, _literals_, `not` can
    /// trivially apply the negation on the formula. Other, more complex,
    /// formulas will be wrapped into a `Not`-node. On the other hand, if the
    /// current formula, is already a `Not`-node, the node gets unwrapped,
    /// avoiding nesting of multiple `Not`-nodes.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let literal = f.literal("a", true);
    /// let formula = "b + c < 1".to_formula(&f);
    ///
    /// let not1 = f.not(literal);
    /// let not2 = f.not(not1);
    ///
    /// let not3 = f.not(formula);
    /// let not4 = f.not(not3);
    ///
    /// assert_eq!(not1.to_string(&f), "~a");
    /// assert_eq!(not2.to_string(&f), "a");
    /// assert_eq!(not3.to_string(&f), "~(b + c < 1)");
    /// assert_eq!(not4.to_string(&f), "b + c < 1");
    /// ```
    pub fn not(&self, op: EncodedFormula) -> EncodedFormula {
        match op.formula_type() {
            FormulaType::False | FormulaType::True | FormulaType::Lit(_) | FormulaType::Not => self.negate(op),
            _ => EncodedFormula::from(self.nots.get_or_insert(op)),
        }
    }

    /// Applies a negation on the given formula.
    ///
    /// This function is different to [`not`] in the way, that it directly
    /// applies the negation for Pseudo-Boolean constraints. [`not`] does that only in
    /// trivial cases (_constants_, _literals_) and wraps all complex formulas
    /// into a `Not`-node.
    ///
    /// [`not`]: FormulaFactory::not
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let literal = f.literal("a", true);
    /// let formula = "b + c < 1".to_formula(&f);
    ///
    /// let not1 = f.negate(literal);
    /// let not2 = f.negate(formula);
    ///
    /// assert_eq!(not1.to_string(&f), "~a");
    /// assert_eq!(not2.to_string(&f), "b + c >= 1");
    /// ```
    pub fn negate(&self, formula: EncodedFormula) -> EncodedFormula {
        match formula.unpack(self) {
            Formula::Pbc(pbc) => pbc.clone().negate(self),
            Formula::Cc(cc) => cc.clone().negate(self),
            Formula::Equiv(_) | Formula::Impl(_) | Formula::Or(_) | Formula::And(_) => self.not(formula),
            Formula::Not(op) => op,
            Formula::Lit(lit) => lit.negate().into(),
            Formula::True => self.falsum(),
            Formula::False => self.verum(),
        }
    }

    /// Creates a new cardinality constraints.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use logicng::formulas::CType::{EQ, LT};
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.var("a");
    /// let b = f.var("b");
    /// let c = f.var("c");
    ///
    /// let cc1 = f.cc(EQ, 2, vec![a, b, c]);
    /// let cc2 = f.cc(LT, 1, vec![a, c]);
    ///
    /// assert_eq!(cc1.to_string(&f), "a + b + c = 2");
    /// assert_eq!(cc2.to_string(&f), "a + c < 1");
    /// ```
    #[allow(clippy::cast_possible_wrap)]
    pub fn cc<V: Into<Box<[Variable]>>>(&self, comparator: CType, rhs: u64, variables: V) -> EncodedFormula {
        assert!(is_cc(comparator, rhs as i64), "Given values do not represent a cardinality constraint.");
        self.construct_cc_unsafe(comparator, rhs as i64, variables.into())
    }

    /// Creates a new _exactly-one_ cardinality constraint.
    ///
    /// Given _n_ variables `(v_1, v_2, ... , v_n)`, the `exo`-constraint looks as follows:
    /// ```text
    /// v_1 + v_2 + ... + v_n = 1
    /// ```
    /// This is equivalent to [`cc(EQ, 1, variables)`].
    ///
    /// [`cc(EQ, 1, variables)`]: FormulaFactory::cc
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use logicng::formulas::CType::EQ;
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.var("a");
    /// let b = f.var("b");
    ///
    /// let exo = f.exo(vec![a, b]);
    ///
    /// assert_eq!(exo.to_string(&f), "a + b = 1");
    /// assert_eq!(exo, f.cc(EQ, 1, vec![a, b]));
    /// ```
    pub fn exo<V: Into<Box<[Variable]>>>(&self, variables: V) -> EncodedFormula {
        self.cc(EQ, 1, variables)
    }

    /// Creates a new _at-most-one_ cardinality constraint.
    ///
    /// Given _n_ variables `(v_1, v_2, ... , v_n)`, the `amo`-constraint looks as follows:
    /// ```text
    /// v_1 + v_2 + ... + v_n <= 1
    /// ```
    /// This is equivalent to [`cc(LE, 1, variables)`].
    ///
    /// [`cc(LE, 1, variables)`]: FormulaFactory::cc
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use logicng::formulas::CType::LE;
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.var("a");
    /// let b = f.var("b");
    ///
    /// let amo = f.amo(vec![a, b]);
    ///
    /// assert_eq!(amo.to_string(&f), "a + b <= 1");
    /// assert_eq!(amo, f.cc(LE, 1, vec![a, b]));
    /// ```
    pub fn amo<V: Into<Box<[Variable]>>>(&self, variables: V) -> EncodedFormula {
        self.cc(LE, 1, variables)
    }

    /// Creates a new pseudo-boolean constraint.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use logicng::formulas::CType::{EQ, LT};
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.lit("a", true);
    /// let b = f.lit("b", true);
    /// let c = f.lit("c", false);
    ///
    /// let pbc1 = f.pbc(EQ, 2, vec![a, b, c], vec![2, -1, 1]);
    /// let pbc2 = f.pbc(LT, 1, vec![a, c], vec![3, -4]);
    ///
    /// assert_eq!(pbc1.to_string(&f), "2*a + -1*b + ~c = 2");
    /// assert_eq!(pbc2.to_string(&f), "3*a + -4*~c < 1");
    /// ```
    pub fn pbc<L, C>(&self, comparator: CType, rhs: i64, literals: L, coefficients: C) -> EncodedFormula
    where
        L: Into<Box<[Literal]>>,
        C: Into<Box<[i64]>>, {
        let l = literals.into();
        let c = coefficients.into();
        assert_eq!(l.len(), c.len(), "The number of literals and coefficients in a pseudo-boolean constraint must be the same.");
        if l.is_empty() {
            self.constant(evaluate_trivial_pb_constraint(comparator, rhs))
        } else if is_lit_cc(comparator, rhs, &l, &c) {
            self.construct_cc_unsafe(comparator, rhs, l.iter().map(|&lit| lit.variable()).collect())
        } else {
            EncodedFormula::from(self.pbcs.get_or_insert(PbConstraint::new(l, c, comparator, rhs), FormulaType::Pbc))
        }
    }

    /// Returns the _CNF_ form of `formula`.
    ///
    /// You can specify the algorithm for the _CNF_ transformation by
    /// overwriting [`self.config.cnf_config`]. Be aware that some algorithm (e.
    /// g. the default configuration) for the CNF transformation may result in a
    /// CNF containing additional auxiliary variables. Also, the result may not
    /// be a semantically equivalent CNF but an equisatisfiable CNF.
    ///
    /// If the introduction of auxiliary variables is unwanted, you can choose
    /// one of the algorithms [`CnfAlgorithm::Factorization`] and
    /// [`CnfAlgorithm::Bdd`]. Both algorithms provide CNF conversions without
    /// the introduction of auxiliary variables and the result is a semantically
    /// equivalent CNF.
    ///
    /// Since CNF is the input for the SAT or MaxSAT solvers, it has a special
    /// treatment here.  For other conversions, use the according formula
    /// functions.
    ///
    /// [`CnfAlgorithm::Bdd`]: crate::operations::transformations::CnfAlgorithm::Bdd
    /// [`CnfAlgorithm::Factorization`]: crate::operations::transformations::CnfAlgorithm::Factorization
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let formula1 = "(a & b) | c".to_formula(&f);
    /// let cnf = f.cnf_of(formula1);
    ///
    /// assert_eq!(cnf.to_string(&f), "(a | c) & (b | c)");
    /// ```
    #[must_use]
    pub fn cnf_of(&self, formula: EncodedFormula) -> EncodedFormula {
        CnfEncoder::stateless(self.config.cnf_config.clone()).transform(formula, self)
    }

    /// Returns the _NNF_ form of `formula`.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let formula1 = "a => b".to_formula(&f);
    /// let nnf = f.nnf_of(formula1);
    ///
    /// assert_eq!(nnf.to_string(&f), "~a | b");
    /// ```
    #[must_use]
    pub fn nnf_of(&self, formula: EncodedFormula) -> EncodedFormula {
        transformations::nnf(formula, self)
    }

    /// Evaluates the given formula based on `assignment`.
    ///
    /// Any literal not covered by `assignment` evaluates to `false` if it is
    /// positive, or to `true` if it is negative. In other words, it will be
    /// evaluated in such a way, that it is not satisfied. This behavior ensures
    /// that the formula evaluates to a `true/false` value. Unlike
    /// [`restrict`], which only applies the literals of given assignment.
    /// However, this might not be enough to fully evaluate a formula.
    ///
    /// [`restrict`]: FormulaFactory::restrict
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use logicng::datastructures::Assignment;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.var("a");
    /// let b = f.var("b");
    /// let formula = "a & b".to_formula(&f);
    ///
    /// let assignment1 = Assignment::from_variables(&[a, b], &[]);
    /// let assignment2 = Assignment::from_variables(&[a], &[b]);
    ///
    /// assert!(f.evaluate(formula, &assignment1));
    /// assert!(!f.evaluate(formula, &assignment2));
    /// ```
    pub fn evaluate(&self, formula: EncodedFormula, assignment: &Assignment) -> bool {
        let res = match formula.unpack(self) {
            Formula::Pbc(pbc) => pbc.evaluate(assignment),
            Formula::Cc(cc) => cc.evaluate(assignment),
            Formula::Equiv((left, right)) => self.evaluate(left, assignment) == self.evaluate(right, assignment),
            Formula::Impl((left, right)) => !self.evaluate(left, assignment) || self.evaluate(right, assignment),
            Formula::Or(mut ops) => ops.any(|op| self.evaluate(op, assignment)),
            Formula::And(mut ops) => ops.all(|op| self.evaluate(op, assignment)),
            Formula::Not(op) => !self.evaluate(op, assignment),
            Formula::Lit(lit) => assignment.evaluate_lit(lit),
            Formula::True => true,
            Formula::False => false,
        };
        res
    }

    /// Restricts this formula with the give assignment.
    ///
    /// If you want to fully evaluate a formula, consider to use `evaluate`.
    /// `evaluate` ensures that a formula evaluates to a `true/false` value by
    /// assuming that literals not in the assignment are unsatisfiable.
    ///
    /// If you want to restrict the formula only by one literal, you want to use
    /// `restrict_lit`.
    ///
    /// [`evaluate`]: FormulaFactory::evaluate
    /// [`restrict_lit`]: FormulaFactory::restrict_lit
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// # use logicng::datastructures::Assignment;
    /// # use crate::logicng::formulas::ToFormula;
    /// let f = FormulaFactory::new();
    ///
    /// let a = f.var("a");
    /// let b = f.var("b");
    /// let formula = "a & b".to_formula(&f);
    ///
    /// let assignment1 = Assignment::from_variables(&[a], &[]);
    /// let assignment2 = Assignment::from_variables(&[], &[a]);
    ///
    /// let restricted1 = f.restrict(formula, &assignment1);
    /// let restricted2 = f.restrict(formula, &assignment2);
    ///
    /// assert_eq!(restricted1.to_string(&f), "b");
    /// assert_eq!(restricted2.to_string(&f), "$false");
    /// ```
    pub fn restrict(&self, formula: EncodedFormula, assignment: &Assignment) -> EncodedFormula {
        transformations::restrict(formula, assignment, self)
    }

    /// Substitutes variables of the given formulas with specified formulas.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::{FormulaFactory, ToFormula};
    /// # use std::collections::HashMap;
    ///
    /// let f = FormulaFactory::new();
    ///
    /// let formula = "a & b".to_formula(&f);
    ///
    /// let mut substitutions = HashMap::new();
    /// substitutions.insert(f.var("a"), "c => d".to_formula(&f));
    ///
    /// let substituted = f.substitute(formula, &substitutions);
    ///
    /// assert_eq!(substituted.to_string(&f), "(c => d) & b");
    /// ```
    pub fn substitute(&self, formula: EncodedFormula, substitution: &Substitution) -> EncodedFormula {
        transformations::substitute(formula, substitution, self)
    }

    /// Substitutes single variable of the given formulas with specified formulas.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::{FormulaFactory, ToFormula};
    /// # use std::collections::HashMap;
    ///
    /// let f = FormulaFactory::new();
    ///
    /// let formula = "a & b".to_formula(&f);
    /// let variable = f.var("a");
    /// let substitute = "c => d".to_formula(&f);
    ///
    /// let substituted = f.substitute_var(formula, variable, substitute);
    ///
    /// assert_eq!(substituted.to_string(&f), "(c => d) & b");
    /// ```
    pub fn substitute_var(&self, formula: EncodedFormula, variable: Variable, substitute: EncodedFormula) -> EncodedFormula {
        let mut substitution = HashMap::new();
        substitution.insert(variable, substitute);
        self.substitute(formula, &substitution)
    }


    /// Shrinks the `FormulaFactory` as much as possible.
    ///
    /// A `FormulaFactory` makes use of data structures that might allocate more
    /// memory than they are currently needing. This increases the speed of some
    /// operations, but also results in additional memory usage. With
    /// `shrink_to_fit` those data structures try to get rid of as much excess
    /// memory as reasonable possible. This also means, that this function will
    /// not delete any formulas or variables.
    ///
    /// Caution: This function might move a lot of data.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// let f = FormulaFactory::new();
    /// //...
    /// f.shrink_to_fit();
    /// //...
    /// ```
    pub fn shrink_to_fit(&self) {
        self.variables.shrink_to_fix();
        self.ands.shrink_to_fit();
        self.ors.shrink_to_fit();
        self.nots.shrink_to_fit();
        self.impls.shrink_to_fit();
        self.equivs.shrink_to_fit();
    }

    /// Returns the number of nodes that are currently cached in this `FormulaFactory`.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// let f = FormulaFactory::new();
    /// //...
    /// println!("{}", f.number_of_cached_nodes());
    /// ```
    pub fn number_of_cached_nodes(&self) -> usize {
        self.variables.len() + self.ands.len() + self.ors.len() + self.nots.len() + self.impls.len() + self.equivs.len()
    }

    /// Returns the ID of this `FormulaFactory`.
    ///
    /// If you used [`with_id`] to create this factory, the returned ID is the
    /// same as the ID passed to the constructor. If you did not specify an ID
    /// for this factory, a random ID was generated.
    ///
    /// [`with_id`]: FormulaFactory::with_id
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// let f = FormulaFactory::with_id("MyFactory");
    /// assert_eq!(f.id(), "MyFactory");
    /// ```
    pub fn id(&self) -> String {
        self.id.clone()
    }

    /// Returns the statistics for this formula factory.
    ///
    /// # Examples
    ///
    /// Basic usage:
    ///
    /// ```
    /// # use logicng::formulas::FormulaFactory;
    /// let f = FormulaFactory::new();
    /// //...
    /// println!("{}", f.print_stats());
    /// ```
    pub fn print_stats(&self) -> String {
        format!(
            "FormulaFactory Stats\n\
                    num_variables: {},\n\
                    num_ands: {},\n\
                    num_ors: {},\n\
                    num_nots: {},\n\
                    num_impls: {},\n\
                    num_equivs: {},\n\
                    cnf_counter: {},\n\
                    cc_counter: {}\
        ",
            self.variables.len(),
            self.ands.len(),
            self.ors.len(),
            self.nots.len(),
            self.impls.len(),
            self.equivs.len(),
            self.cnf_counter.load(Ordering::SeqCst),
            self.cc_counter.load(Ordering::SeqCst)
        )
    }

    pub(crate) fn new_cnf_variable(&self) -> Variable {
        let n = self.cnf_counter.fetch_add(1, Ordering::SeqCst);
        Variable::Aux(AuxVarType::CNF, n as u64)
    }

    pub(crate) fn new_cc_variable(&self) -> Variable {
        let n = self.cc_counter.fetch_add(1, Ordering::SeqCst);
        Variable::Aux(AuxVarType::CC, n as u64)
    }

    pub(crate) fn new_pb_variable(&self) -> Variable {
        let n = self.pb_counter.fetch_add(1, Ordering::SeqCst);
        Variable::Aux(AuxVarType::PB, n as u64)
    }

    pub(crate) fn var_name(&self, index: FormulaEncoding) -> &str {
        &self.variables[index]
    }

    #[allow(clippy::cast_sign_loss)]
    fn construct_cc_unsafe(&self, comparator: CType, rhs: i64, variables: Box<[Variable]>) -> EncodedFormula {
        if variables.is_empty() {
            self.constant(evaluate_trivial_pb_constraint(comparator, rhs))
        } else {
            let (comp, r): (CType, u64) = if rhs >= 0 {
                (comparator, rhs as u64)
            } else {
                assert_eq!(comparator, GT);
                (GE, 0)
            };
            let cc = self.ccs.get_or_insert(CardinalityConstraint::new(variables, comp, r), FormulaType::Cc);
            EncodedFormula::from(cc)
        }
    }

    fn filter(&self, ops: &[EncodedFormula], op_type: FormulaType) -> Option<FilterResult> {
        let flattened_ops = self.flatten_ops(ops, op_type);
        let mut reduced32 = Vec::new();
        let mut reduced_set32 = HashSet::new();
        let mut reduced64 = Vec::new();
        let mut reduced_set64 = HashSet::new();
        for op in flattened_ops {
            if op.is_verum() {
                if op_type == FormulaType::Or {
                    return None;
                }
            } else if op.is_falsum() {
                if op_type == FormulaType::And {
                    return None;
                }
            } else if op.is_type(op_type) {
                for &sub_op in &*op.operands(self) {
                    let sub_encoded = sub_op.encoding;
                    if sub_encoded.is_large() {
                        if reduced_set64.insert(sub_encoded) {
                            reduced64.push(sub_encoded);
                        }
                    } else if reduced_set32.insert(sub_encoded.as_32()) {
                        reduced32.push(sub_encoded.as_32());
                    }
                }
            } else if self.contains_complement(&reduced_set32, &reduced_set64, op) {
                return None;
            } else {
                let op_encoded = op.encoding;
                if op_encoded.is_large() {
                    if reduced_set64.insert(op_encoded) {
                        reduced64.push(op_encoded);
                    }
                } else if reduced_set32.insert(op_encoded.as_32()) {
                    reduced32.push(op_encoded.as_32());
                }
            };
        }
        Some((reduced32, reduced_set32, reduced64, reduced_set64))
    }

    fn flatten_ops(&self, ops: &[EncodedFormula], op_type: FormulaType) -> Vec<EncodedFormula> {
        let mut nops = Vec::with_capacity(ops.len());
        for &op in ops {
            if op.is_type(op_type) {
                nops.extend(self.flatten_ops(&op.operands(self), op_type));
            } else {
                nops.push(op);
            }
        }
        nops
    }

    fn contains_complement(
        &self,
        set32: &HashSet<SmallFormulaEncoding>,
        set64: &HashSet<FormulaEncoding>,
        formula: EncodedFormula,
    ) -> bool {
        use Formula::{False, Lit, Not, True};

        match formula.unpack(self) {
            True => {
                let enc = &FormulaEncoding::encode_type(FormulaType::False);
                set32.contains(&enc.as_32()) || set64.contains(enc)
            }
            False => {
                let enc = &FormulaEncoding::encode_type(FormulaType::True);
                set32.contains(&enc.as_32()) || set64.contains(enc)
            }
            Lit(lit) => {
                let enc = &EncodedFormula::from(lit.negate()).encoding;
                set32.contains(&enc.as_32()) || set64.contains(enc)
            }
            Not(op) => set32.contains(&op.encoding.as_32()) || set64.contains(&op.encoding),
            _ => self.nots.lookup(formula).map(|not| set32.contains(&not.as_32()) || set64.contains(&not)) == Some(true),
        }
    }
}

const fn evaluate_trivial_pb_constraint(comparator: CType, rhs: i64) -> bool {
    match comparator {
        EQ => rhs == 0,
        GT => rhs < 0,
        GE => rhs <= 0,
        LT => rhs > 0,
        LE => rhs >= 0,
    }
}

fn is_lit_cc(comparator: CType, rhs: i64, literals: &[Literal], coefficients: &[i64]) -> bool {
    literals.iter().all(Literal::phase) && coefficients.iter().all(|&c| c == 1) && is_cc(comparator, rhs)
}

fn is_cc(comparator: CType, rhs: i64) -> bool {
    comparator == LE && rhs >= 0
        || comparator == LT && rhs >= 1
        || comparator == GE && rhs >= 0
        || comparator == GT && rhs >= -1
        || comparator == EQ && rhs >= 0
}

fn generate_random_id() -> String {
    (0..FF_ID_LENGTH).map(|_| fastrand::alphanumeric().to_uppercase().to_string()).collect::<String>()
}