# Public APIs

This page lists documentation for the most commonly used public APIs of `LogicCircuits.jl`

. Visit the internals section for a auto generated documentation for more public API and internal APIs.

## Circuit IO

`Base.read`

— Function`Base.read(io::IO, ::Type{PlainLogicCircuit}, ::FnfFormat)`

Read CNF/DNF from file.

`Base.read(file::AbstractString, ::Type{C}) where C <: LogicCircuit`

Reads circuit from file; uses extension to detect format type, for example ".sdd" for SDDs.

`Base.write`

— Function`write(file::AbstractString, vtree::PlainVtree)`

Saves a vtree in the given file path based on file format. Supported formats:

- ".vtree" for Vtree files
- ".dot" for dot files

`Base.write(io::IO, fnf::LogicCircuit, ::FnfFormat)`

Write CNF/DNF to file.

`Base.write(file::AbstractString, circuit::LogicCircuit)`

Writes circuit to file; uses file name extention to detect file format.

`Base.write(files::Tuple{AbstractString,AbstractString}, circuit::StructLogicCircuit)`

Saves circuit and vtree to file.

## Circuit Zoo IO

`LogicCircuits.zoo_cnf`

— Function`zoo_cnf(name)`

Loads CNF file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

`LogicCircuits.zoo_dnf`

— Function`zoo_dnf(name)`

Loads DNF file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

`LogicCircuits.zoo_sdd`

— Function`zoo_sdd(name)`

Loads SDD file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

`LogicCircuits.zoo_nnf`

— Function`zoo_nnf(name)`

Loads NNF file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

`LogicCircuits.zoo_jlc`

— Function`zoo_jlc(name)`

Loads JLC file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

`LogicCircuits.zoo_vtree`

— Function`zoo_vtree(name)`

Loads Vtree file with given name from model zoo. See https://github.com/UCLA-StarAI/Circuit-Model-Zoo.

## Circuit Properties

`LogicCircuits.issmooth`

— Function`issmooth(root::LogicCircuit)::Bool`

Is the circuit smooth?

`LogicCircuits.isdecomposable`

— Function`isdecomposable(root::LogicCircuit)::Bool`

Is the circuit decomposable?

`LogicCircuits.isdeterministic`

— Function`isdeterministic(root::LogicCircuit)::Bool`

Is the circuit determinstic? Note: this function is generally intractable for large circuits.

`LogicCircuits.iscanonical`

— Function`iscanonical(circuit::LogicCircuit, k::Int; verbose = false)`

Does the given circuit have canonical Or gates, as determined by a probabilistic equivalence check?

## Circuit Queries

`LogicCircuits.sat_prob`

— Function`sat_prob(root::LogicCircuit; varprob::Function)::Rational{BigInt}`

Get the probability that a random world satisties the circuit. Probability of each variable is given by `varprob`

Function which defauls to 1/2 for every variable.

`LogicCircuits.model_count`

— Function`model_count(root::LogicCircuit, num_vars_in_scope::Int = num_variables(root))::BigInt`

Get the model count of the circuit. The `num_vars_in_scope`

is set to number of variables in the circuit, but sometimes need to set different values, for example, if not every variable is mentioned in the circuit.

## Circuit Operations

`DirectedAcyclicGraphs.foldup`

— Function```
foldup(node::LogicCircuit,
f_con::Function,
f_lit::Function,
f_a::Function,
f_o::Function)::T where {T}
```

Compute a function bottom-up on the circuit. `f_con`

is called on constant gates, `f_lit`

is called on literal gates, `f_a`

is called on conjunctions, and `f_o`

is called on disjunctions. Values of type `T`

are passed up the circuit and given to `f_a`

and `f_o`

through a callback from the children.

`DirectedAcyclicGraphs.foldup_aggregate`

— Function```
foldup_aggregate(node::LogicCircuit,
f_con::Function,
f_lit::Function,
f_a::Function,
f_o::Function,
::Type{T})::T where T
```

Compute a function bottom-up on the circuit. `f_con`

is called on constant gates, `f_lit`

is called on literal gates, `f_a`

is called on conjunctions, and `f_o`

is called on disjunctions. Values of type `T`

are passed up the circuit and given to `f_a`

and `f_o`

in an aggregate vector from the children.

## Circuit Transformations

`LogicCircuits.smooth`

— Function`smooth(root::StructLogicCircuit)::StructLogicCircuit`

Create an equivalent smooth circuit from the given circuit.

`smooth(root::LogicCircuit)`

Create an equivalent smooth circuit from the given circuit.

Smooth an sdd to a StructLogicCircuit

Missing docstring for `conjoin`

. Check Documenter's build log for details.

`LogicCircuits.forget`

— Function`forget(root::LogicCircuit, is_forgotten::Function)`

Forget variables from the circuit. Warning: this may or may not destroy the determinism property.

```
forget(α::Bdd, x::Integer)::Bdd = eliminate(α, x)
forget(α::Bdd, X::Union{Set, BitSet, AbstractVector{T}}) where T <: Integer
```

Returns the resulting BDD after applying the `forget`

operation. Equivalent to $\phi|_x \vee \phi|_{\neg x}$.

`Base.deepcopy`

— Function`deepcopy(n::LogicCircuit, depth::Int64)`

Recursively create a copy circuit rooted at `n`

to a certain depth `depth`

`Base.split`

— Function`split(root::LogicCircuit, (or, and)::Tuple{LogicCircuit, LogicCircuit}, var::Var; depth=0, sanity_check=true)`

Return the circuit after spliting on edge `edge`

and variable `var`

`LogicCircuits.clone`

— FunctionClone the `or`

node and redirect one of its parents to the new copy

`LogicCircuits.propagate_constants`

— Function`propagate_constants(root::LogicCircuit)`

Remove all constant leafs from the circuit

## Compilation

## GPU Related

`LogicCircuits.Utils.isgpu`

— FunctionCheck whether data resides on the GPU

`LogicCircuits.Utils.to_gpu`

— FunctionMove data to the GPU

`LogicCircuits.Utils.to_cpu`

— FunctionMove data to the CPU