Crate gatesim

The base library of the Gate Project. It provides basic types of circuits and basic methods to operate on that circuits. The library doesn’t provide complex simulation routines. This library is really base of the Gate Project.

The basic type of circuit Circuit is constructed from gates of following types:

• ‘and’ - AND gate that returns true if two inputs are true, otherwise returns false.
• ‘nor’ - NOR (negation of OR) gate that returns true if two inputs are false, otherwise returns false.
• ‘nimpl’ - NIMPL (negation of implication) gate that returns true if first input is true and second is false, otherwise it returns false.
• ‘xor’ - XOR gate that return true if inputs are different.

The type of circuit is parametrized by type of wire index. It can be unsigned integer for example u32.

The circuit defined by input length (number), gates and outputs that are defined by wire and negation. If wire index is index of circuit input or index of gate output. The input of circuit starts from 0. The output of gate starts from input length number. The circuit can be constructed from gates satisfied following constraints:

• All inputs for all gates and output wires are correct types (input is less than current gate output wire index).
• All inputs are used by some gates or circuit outputs.
• All gate outputs are used some gates or circuit outputs.

Additional type of circuit ClauseCircuit is constructed from clauses. The clause is gate that uses any number of inputs. The clause contains literals (input wire that can be negated or not). The are two clause types:

• ‘and’ clause that returns true if all literals are true. If clause has no inputs then returns true.
• ‘xor’ clause that returns true if number of literals of true value is odd. If clause has no inputs then returns false.

Similary, the clause circuit defined by input length (number), clauses and outputs that are defined by wire and negation. If wire index is index of circuit input or gate output. The input of circuit starts from 0. The output of gate starts from input length number. The circuit can be constructed from gates satisfied following constraints:

• All inputs for all clauses and output wires are correct types (input is less than current clause output wire index).
• All inputs are used by some clauses or circuit outputs.
• All clauses outputs are used some clauses or circuit outputs.

Derived QuantCircuit from Circuit provides additional information about quantifiers. These quantifiers can be used to evaluate or solve quantified formula defined by circuit. There are two types of quantifiers:

• ‘all’ - formula is satisified if circuit returns true for all combinations of inputs.
• ‘exists’ - formula is satisified if circuit returns true for some combinations of inputs.

Number of quantifiers must match to input length. Any sequence of quantifiers for inputs determine single quantifier for some input length. Number of output must be 1.

For describe: [all,all,exists,exists,all,all] - formula is true if for all combinations of input0, input1 can be found some combination of input2,input3 all combinations input4, input5 circuit returns true.

Similary, QuantClauseCircuit is derive from ClauseCircuit. It provides information about quantifiers. These same constraints applied like in QuantCircuits.

Structs

Circuit

The main circuit structure that describe Gate circuit.

Clause

Clause is special gate that accepts any number of inputs.

ClauseCircuit

The circuit structure that describe circuit constructed from clauses.

FmtLiner

Helper for formatting longer circuits.

Gate

The gate of circuit. It describes gate of circuit with all inputs.

QuantCircuit

Derive of Circuit with quantifier list.

QuantClauseCircuit

Derive of ClauseCircuit with quantifier list.

Enums

CircuitParseError

Parse error for Circuit.

ClauseCircuitParseError

Clause circuit parse error type.

ClauseKind

Kind of clauses.

ClauseParseError

Clause parse error type.

GateFunc

Gate function (type).

GateParseError

Parse error for Gate.

Quant

Quantifier type.