Conjunction.
Conjunction.
A cardinality constraint of the form
A cardinality constraint of the form
sum(lits) relop k
. sum(lits) relop k }}}
A classic PB constraint f the form
A classic PB constraint f the form
sum(weights(lit)*lit) relop k
. sum(weights(lit)*lit) relop k }}}
A clause.
A clause.
Abstract trait for optimization criteria.
Abstract trait for optimization criteria.
Abstract type for logical gates used when constructing a CNF formula.
Abstract type for logical gates used when constructing a CNF formula.
Equivalence.
Equivalence.
Implication.
Implication.
If-then-else.
If-then-else.
A linear criterion to be maximized.
A linear criterion to be maximized.
A linear criterion to be minimized.
A linear criterion to be minimized.
Negation.
Negation.
Disjunction.
Disjunction.
Abstract type for relational operators used in cardinality constraints.
Abstract type for relational operators used in cardinality constraints.
Equivalence.
Equivalence.
Represents an input gate of the circuit.
Represents an input gate of the circuit.
Adds a cardinality constraint
Adds a cardinality constraint
sum(lits) >= k
.
sum(lits) >= k }}}
optionally add a masking literal that allows to switch the clause on and off
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Adds a cardinality constraint
Adds a cardinality constraint
sum(lits) <= k
.
sum(lits) <= k }}}
optionally add a masking literal that allows to switch the clause on and off
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Adds a cardinality constraint with specified relop and constant to the solver.
Adds a cardinality constraint with specified relop and constant to the solver.
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the constraint on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Method to use to effectively add a cardinality constraint to the underlying Solver implementation.
Method to use to effectively add a cardinality constraint to the underlying Solver implementation.
Adds a collection of literals as a clause to the solver.
Adds a collection of literals as a clause to the solver.
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Method to use to effectively add a clause to the underlying Solver implementation.
Method to use to effectively add a clause to the underlying Solver implementation.
Adds a list of literals as a clause to the solver.
Adds a list of literals as a clause to the solver.
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Adds an optimization criterion to the formula.
Adds an optimization criterion to the formula.
Adds a cardinality constraint
Adds a cardinality constraint
sum(lits) <= k
.
sum(lits) <= k }}}
optionally add a masking literal that allows to switch the clause on and off
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Add a header comment in the formula.
Add a header comment in the formula.
Asserts that a certain literal must be true.
Asserts that a certain literal must be true.
Asserts that a collection of literals are all equal, implemented using a loop of implications.
Asserts that a collection of literals are all equal, implemented using a loop of implications.
l1 = l2 = ... = ln := l1 -> l2 & ... & ln -> l1
list of literals of size >= 2
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the assertion on and off
The optional switching literal
An itetator on the gate variables of the formula.
an iterator on the cardinality constraints currently in the solver.
an iterator on the clauses currently in the solver.
An iterator on criteria of the formula.
Declares a literal as an output of the circuit.
Declares a literal as an output of the circuit.
Declares a literal as an output of the circuit.
Declares a literal as an output of the circuit.
Encodes the equation
Encodes the equation
x = And(a1, ... ,an)
as clauses:
( x, ~a1, ... , ~an) ( ~x, a1 ) ... ( ~x, an )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Iff(p, q)
as clauses:
( ~x, ~p, q ) ( ~x, p, ~q ) ( x, ~p, ~q ) ( x, p, q )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Implies(p, q)
as clauses:
(~x, ~p, q ) ( x, p ) ( x, ~q )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Ite(s, t, f)
as clauses:
( x, ~s, ~t ) ( ~x, ~s, t ) ( x, s, ~f ) ( ~x, s, f ) ( x, ~t, ~f ) ( ~x, f, t )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Not(p)
as clauses:
(~x, ~p) (x, p)
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Or(a1, ... , an)
as clauses:
( ~x, a1, ... , an) ( x, ~a1) ... ( x, ~an)
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Encodes the equation
Encodes the equation
x = Xor(p, q)
as clauses:
( ~x, p, q ) ( ~x, ~p, ~q ) ( x, p, ~q ) ( x, ~p, q )
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the gate clauses on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a switching literal, None otherwise.
Freeze the variable underlying the literal.
Freeze the variable underlying the literal.
Reserve
Reserve
howmany
variables to express the problem, reserving dimacs variables identifiers in [1, howmany]. Next fresh variables identifiers will start at
howmany+1
howmany }}} Next fresh variables identifiers will start at
howmany+1
number of variables to create
The total variables used in the solver.
Creates a fresh variable in the solver.
Creates a fresh variable in the solver.
the number of variables created in the solver so far, equal to the fresh variable identifier.
Method to implement to effectively create a fresh var in the underlying representation.
Method to implement to effectively create a fresh var in the underlying representation.
Method to implement to effectively create a fresh var in the underlying representation.
Method to implement to effectively create a fresh var in the underlying representation.
A gate Map indexed by literals.
An itetator on gate literal definitions.
Iterator over all header comments, in insertion order.
An itetator on the gate variables of the formula.
True iff the literal is not a gate.
True iff the variable is frozen.
True iff the variable is frozen.
True iff the literal or its complement is defined as a gate.
True iff the literal was previously declared as a circuit input.
True iff the literal was previously declared as a circuit input.
Returns a switching literal: if switch is Some( s ), returns this Some( s ), else if switchable is true, returns a Some( newSwitch ) else returns None.
Returns a switching literal: if switch is Some( s ), returns this Some( s ), else if switchable is true, returns a Some( newSwitch ) else returns None.
the number of gates of the formula.
the number of clauses of the formula.
the number of criteria of the formula.
The number of gates of the formula.
the number of gates of the formula.
the number of gates of the formula.
the number of cardinality constraints of the formula.
An iterator on the gate variables of the formula.
Created by rdelmas on 21/06/16.