Edit on GitHub

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.

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

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

source
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
source
Base.write(io::IO, fnf::LogicCircuit, ::FnfFormat)

Write CNF/DNF to file.

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

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

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

Saves circuit and vtree to file.

source

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.

source
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.

source
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.

source
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.

source
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.

source
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.

source

Circuit Properties

LogicCircuits.isdeterministic — Function
isdeterministic(root::LogicCircuit)::Bool

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

source
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?

source

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.

source
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.

source

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.

source
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.

source

Circuit Transformations

LogicCircuits.smooth — Function
smooth(root::StructLogicCircuit)::StructLogicCircuit

Create an equivalent smooth circuit from the given circuit.

source
smooth(root::LogicCircuit)

Create an equivalent smooth circuit from the given circuit.

source

Smooth an sdd to a StructLogicCircuit

source
Missing docstring.

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.

source
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}$.

source
Base.deepcopy — Function
deepcopy(n::LogicCircuit, depth::Int64)

Recursively create a copy circuit rooted at n to a certain depth depth

source
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

source

Compilation