Struct FormulaFactory

pub struct FormulaFactory {
    pub config: FormulaFactoryConfig,
    /* private fields */
}

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

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

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])	f1 | f2 | f3

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:

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:

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

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.

Fields

config: FormulaFactoryConfig

Configuration

Implementations

impl FormulaFactory

pub fn new() -> Self

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.

Examples

Basic usage:

use logicng::formulas::FormulaFactory;

let f = FormulaFactory::new();

pub fn with_id(id: &str) -> Self

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.

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 parse(&self, input: &str) -> Result<EncodedFormula, Box<Error<Rule>>>

Parses a given string to a formula using a Pseudo-Boolean parser.

Examples

Basic usage:

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);

pub fn verum(&self) -> EncodedFormula

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:

let f = FormulaFactory::new();

let verum = f.verum();
assert_eq!(verum.formula_type(), FormulaType::True);

pub fn falsum(&self) -> EncodedFormula

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:

let f = FormulaFactory::new();

let falsum = f.falsum();
assert_eq!(falsum.formula_type(), FormulaType::False);

pub fn constant(&self, value: bool) -> EncodedFormula

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:

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 var(&self, name: &str) -> Variable

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.

Examples

Basic usage:

let f = FormulaFactory::new();

let var = f.var("MyVar");

assert_eq!(var.name(&f).into_owned(), "MyVar");

pub fn variable(&self, name: &str) -> EncodedFormula

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.

Examples

Basic usage:

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 parsed_variable(&self, name: &str) -> EncodedFormula

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.

Examples

Basic usage:

let f = FormulaFactory::new();

let _ = f.parsed_variable("MyVar"); //Normal variable
let _ = f.parsed_variable("@RESERVED_00_CNF_00"); //Auxiliary variable

pub fn lit(&self, name: &str, phase: bool) -> Literal

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.

Examples

Basic usage:

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 literal(&self, name: &str, phase: bool) -> EncodedFormula

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.

Examples

Basic usage:

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 and(&self, operands: &[EncodedFormula]) -> EncodedFormula

Creates a new conjunction from a vector of formulas.

Examples

Basic usage:

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 or(&self, operands: &[EncodedFormula]) -> EncodedFormula

Creates a new disjunction from a vector of formulas.

Examples

Basic usage:

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 clause(&self, operands: &[Literal]) -> EncodedFormula

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.

Examples

Basic usage:

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 implication( &self, left: EncodedFormula, right: EncodedFormula, ) -> EncodedFormula

Creates a new implication, where left implies right.

Examples

Basic usage:

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 equivalence( &self, left: EncodedFormula, right: EncodedFormula, ) -> EncodedFormula

Creates a new equivalence between left and right.

Examples

Basic usage:

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 not(&self, op: EncodedFormula) -> EncodedFormula

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:

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 negate(&self, formula: EncodedFormula) -> EncodedFormula

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.

Examples

Basic usage:

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 cc<V: Into<Box<[Variable]>>>( &self, comparator: CType, rhs: u64, variables: V, ) -> EncodedFormula

Creates a new cardinality constraints.

Examples

Basic usage:

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");

pub fn exo<V: Into<Box<[Variable]>>>(&self, variables: V) -> EncodedFormula

Creates a new exactly-one cardinality constraint.

Given n variables (v_1, v_2, ... , v_n), the exo-constraint looks as follows:

v_1 + v_2 + ... + v_n = 1

This is equivalent to cc(EQ, 1, variables).

Examples

Basic usage:

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 amo<V: Into<Box<[Variable]>>>(&self, variables: V) -> EncodedFormula

Creates a new at-most-one cardinality constraint.

Given n variables (v_1, v_2, ... , v_n), the amo-constraint looks as follows:

v_1 + v_2 + ... + v_n <= 1

This is equivalent to cc(LE, 1, variables).

Examples

Basic usage:

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 pbc<L, C>( &self, comparator: CType, rhs: i64, literals: L, coefficients: C, ) -> EncodedFormula

where L: Into<Box<[Literal]>>, C: Into<Box<[i64]>>,

Creates a new pseudo-boolean constraint.

Examples

Basic usage:

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 cnf_of(&self, formula: EncodedFormula) -> EncodedFormula

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.

Examples

Basic usage:

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)");

pub fn nnf_of(&self, formula: EncodedFormula) -> EncodedFormula

Returns the NNF form of formula.

Examples

Basic usage:

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");

pub fn evaluate(&self, formula: EncodedFormula, assignment: &Assignment) -> bool

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.

Examples

Basic usage:

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 restrict( &self, formula: EncodedFormula, assignment: &Assignment, ) -> EncodedFormula

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.

Examples

Basic usage:

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 substitute( &self, formula: EncodedFormula, substitution: &Substitution, ) -> EncodedFormula

Substitutes variables of the given formulas with specified formulas.

Examples

Basic usage:

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_var( &self, formula: EncodedFormula, variable: Variable, substitute: EncodedFormula, ) -> EncodedFormula

Substitutes single variable of the given formulas with specified formulas.

Examples

Basic usage:

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 shrink_to_fit(&self)

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:

let f = FormulaFactory::new();
//...
f.shrink_to_fit();
//...

pub fn number_of_cached_nodes(&self) -> usize

Returns the number of nodes that are currently cached in this FormulaFactory.

Examples

Basic usage:

let f = FormulaFactory::new();
//...
println!("{}", f.number_of_cached_nodes());

pub fn id(&self) -> String

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.

Examples

Basic usage:

let f = FormulaFactory::with_id("MyFactory");
assert_eq!(f.id(), "MyFactory");

pub fn print_stats(&self) -> String

Returns the statistics for this formula factory.

Examples

Basic usage:

let f = FormulaFactory::new();
//...
println!("{}", f.print_stats());

Trait Implementations

impl Default for FormulaFactory

fn default() -> Self

Returns the “default value” for a type.