Module with general utilities and missing standard library features that could be useful in any Julia project

Retro-fitted super type of all bit vectors

Custom CUDA version of BitVector (lacking lots of functionality, just a container for now).

Literals are represented as 32-bit signed integers. Positive literals are positive integers identical to their variable. Negative literals are their negations. Integer 0 should not be used to represent literals.

Variables are represented as 32-bit unsigned integers

Find a type that can capture all column values

Are the given sets disjoint (no shared elements)?

Marginalize out dimensions dims from log-probability tensor

An array of 100% probabilities for the given element type

Returns an array of DataFrames where each DataFrame is randomly sampled from the original dataset data

Create mini-batches

Batch size of the dataset

Normalize the given log-likelihood as bits per pixel in data

Retrieve chunks of bit vector

Iterate over columns, excluding the sample weight column

Get the ith example

Get the ith feature values

Computer the per-example log-likelihood of a fully factorized ML model on Bool data

Retrieve the jth bit from a BitVector chunk

Get the weights from a weighted dataset.

Return a copy of Imputed values of X (potentially statistics from another DataFrame)

For example, to impute using same DataFrame:

impute(X; method=:median)

If you want to use another DataFrame to provide imputation statistics:

impute(test_x, train_x; method=:mean)

Supported methods are :median, :mean, :one, :zero

An array of undetermined values (fast) for the given element type

Is the dataset batched?

Is the dataset binary?

Is the data complete (no missing values)?

Is the data column complete (no missing values)?

Is the dataset consisting of floating point data?

Check whether data resides on the GPU

Is the argument not nothing?

Is the dataset weighted?

Convert a literal its variable, removing the sign of the literal

Normalize the given log-likelihood by the number of examples in data

make_missing_mcar(d::DataFrame; keep_prob::Float64=0.8)

Returns a copy of dataframe with making some features missing as MCAR, with keep_prob as probability of keeping each feature.

Compute the marginal prob of each feature in a binary dataset.

An array of 0% probabilities for the given element type

Function that does nothing

For binary complete data, how many UInt64 bit strings are needed to store one feature?

num_examples(df::DataFrame)

Number of examples in data

num_features(df::DataFrame)

Number of features in the data

Number of variables in the data structure

Order the arguments in a tuple in ascending order

Push element into random position in vectorv

Randomly draw samples from the dataset with replacement

Ensure that x resides on the same device as data

shuffle_examples(df::DataFrame)

Shuffle the examples in the data

Reuse a given array if it has the right type and size, otherwise make a new one

Turn binary data into floating point data close to 0 and 1.

Split a weighted dataset into unweighted dataset and its corresponding weights.

Replacement for BitSet.⊆ that does not allocate a new BitSet

Threshold a numeric dataset making it binary

Move data to the CPU

Move data to the GPU

An array of uniform probabilities

Convert a variable to the corresponding positive literal

Get the BitSet of variables in the data structure

Create a weighted copy of the data set

Canonical false Sdd node

The unique splain tructured logical false constant

The unique plain structured logical true constant

Canonical true Sdd node

Representation of the arguments of an Apply call

Apply cache for the result of conjunctions and disjunctions

A Binary Decision Diagram.

• index: the vertex variable (-1 if terminal vertex
• low: low child vertex of BDD (undef if terminal vertex)
• high: high child vertex of BDD (undef if terminal vertex)
• value: terminal boolean value
• id: unique identifier

A bit circuit is a low-level representation of a logical circuit structure.

They are a "flat" representation of a circuit, essentially a bit string, that can be processed by lower level code (e.g., GPU kernels)

The wiring of the circuit is captured by two matrices: nodes and elements.

• Nodes are either leafs or decision (disjunction) nodes in the circuit.
• Elements are conjunction nodes in the circuit.
• In addition, there is a vector of layers, where each layer is a list of node ids. Layer 1 is the leaf/input layer. Layer end is the circuit root.
• And there is a vector of parents, pointing to element id parents of decision nodes.

Nodes are represented as a 4xN matrix where

• nodes[1,:] is the first element id belonging to this decision
• nodes[2,:] is the last element id belonging to this decision
• nodes[3,:] is the first parent index belonging to this decision
• nodes[4,:] is the last parent index belonging to this decision

Elements belonging to node i are elements[:, nodes[1,i]:nodes[2,i]] Parents belonging to node i are parents[nodes[3,i]:nodes[4,i]]

Elements are represented by a 3xE matrix, where

• elements[1,:] is the decision node id (parents of the element),
• elements[2,:] is the prime node id (child of the element)
• elements[3,:] is the sub node id (child of the element)

construct a new BitCircuit accomodating the given number of features

A trait denoting constant leaf nodes of any type

Represents elements that are not yet compiled into conjunctions

A trait hierarchy denoting types of nodes GateType defines an orthogonal type hierarchy of node types, not circuit types, so we can dispatch on node type regardless of circuit type. See @ref{https://docs.julialang.org/en/v1/manual/methods/#Trait-based-dispatch-1}

Get the gate type trait of the given LogicCircuit

A logical gate that is an inner node

A logical gate that is a leaf node

A trait denoting literal leaf nodes of any type

Root of the logic circuit node hierarchy

Integer identifier for a circuit node

The BitCircuit ids associated with a node

A plain logical constant leaf node, representing true or false

A plain logical literal leaf node, representing the positive or negative literal of its variable

Root of the plain logic circuit node hierarchy

A plain logical inner node

A plain logical leaf node

A plain structured logical constant leaf node, representing true or false. These are the only structured nodes that don't have an associated vtree node (cf. SDD file format)

A plain structured logical literal leaf node, representing the positive or negative literal of its variable

Root of the plain structure logic circuit node hierarchy

A plain structured logical inner node

A plain structured logical leaf node

A plain structured logical conjunction node

A plain structured logical disjunction node

Root of the plain vtree node hierarchy

A plain logical conjunction node (And node)

A plain logical disjunction node (Or node)

Root of the trimmed Sdd circuit node hierarchy

A SDD logical constant leaf node, representing true or false. These are the only structured nodes that don't have an associated vtree node (cf. SDD file format)

A SDD logical inner node

A SDD logical leaf node

A SDD logical literal leaf node, representing the positive or negative literal of its variable

Root of the SDD manager node hierarchy

SDD manager inner vtree node for trimmed SDD nodes

SDD manager leaf vtree node for trimmed SDD nodes

A SDD logical conjunction node

A SDD logical disjunction node

Root of the structure logic circuit node hierarchy

Unique nodes cache for decision nodes

Root of the vtree node hiearchy

Represent an XY-partition that has not yet been compiled into a disjunction

A trait denoting conjuction nodes of any type

A trait denoting disjunction nodes of any type

Returns whether the two given boolean functions are not equivalent.

Returns whether the two given boolean functions are equivalent.

Returns a new reduced Bdd restricted to instantiation X.

Returns a xor of the given boolean functions.

deepcopy(n::LogicCircuit, depth::Int64)

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

hash(α::Bdd, h::UInt)::UInt

Returns a unique hash for the whole BDD.

merge(root::LogicCircuit, or1::LogicCircuit, or2::LogicCircuit)

Merge two circuits.

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.

Returns 0 if x is not a literal; else returns the literal's sign.

Returns the number of nodes in the BDD graph.

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

Return string representation of Bdd α.

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

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

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(files::Tuple{AbstractString,AbstractString}, circuit::StructLogicCircuit)

Saves circuit and vtree to file.

Exclusive logical disjunction (XOR)

Get the children of a given inner node

Compute the path length from vtree node n to leaf node for variable var

Find an inner vtree node that has left in its left subtree and right in its right subtree. Supports nothing as a catch-all for any node

Find the leaf in the vtree that represents the given variable

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.

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.

Compute the lowest common ancestor of two vtree nodes Warning: this method uses an incomplete varsubset check for descends_from and is only correct when v and w are part of the same larger vtree.

How many nodes are indexed by a given bit circuit?

(¬)(α::Bdd)::Bdd
(¬)(x::Integer)::Bdd
(¬)(x::Bool)::Bool

Negates this boolean function.

Logical negation

Material logical implication (reverse)

Material logical implication

Bidirectional logical implication

(∧)(α::Bdd, β::Bdd)::Bdd
(∧)(x::Integer, β::Bdd)::Bdd
(∧)(α::Bdd, x::Integer)::Bdd
(∧)(x::Integer, y::Integer)::Bdd
(∧)(x::Bool, y::Bool)::Bool

Returns a conjunction over the given boolean functions.

Logical conjunction

(∨)(α::Bdd, β::Bdd)::Bdd
(∨)(x::Integer, β::Bdd)::Bdd
(∨)(α::Bdd, x::Integer)::Bdd
(∨)(x::Integer, y::Integer)::Bdd
(∨)(x::Bool, y::Bool)::Bool

Returns a disjunction over the given boolean functions.

Logical disjunction

variables(root::LogicCircuit)::BitSet

Get a bitset of variables mentioned in the circuit root.

Computes all possible valuations of scope V and returns as a BitMatrix. Up to 64 variables.

and(α::Bdd, β::Bdd)::Bdd
and(x::Integer, β::Bdd)::Bdd
and(α::Bdd, x::Integer)::Bdd
and(x::Integer, y::Integer)::Bdd
and(Φ::Vararg{Bdd})::Bdd
and(Φ::AbstractVector{Bdd})::Bdd
and(Φ::Vararg{T})::Bdd where T <: Integer
and(Φ::AbstractVector{T})::Bdd where T <: Integer
and(Φ::Vararg{Union{T, Bdd}})::Bdd where T <: Integer

Returns a conjunction over the given boolean functions.

Get the list of And nodes in a given circuit

Returns a Bdd canonical representation of α ⊕ β, where ⊕ is some binary operator.

Recursively computes α ⊕ β. If the result was already computed as an intermediate result, return the cached result in T.

Constructs a BDD mapping to true if at least n literals in L are in the input; otherwise false.

Constructs a BDD mapping to true if at least n literals in L are in the input; otherwise false.

Constructs a BDD mapping to true if at most n literals in L are in the input; otherwise false.

Constructs a BDD mapping to true if at most n literals in L are in the input; otherwise false.

assign threads to examples and decision nodes so that everything is a power of 2

Returns a Bdd representing a single variable. If negative, negate variable.

Construct a mapping from constants to their canonical node representation

Construct a mapping from literals to their canonical node representation

Get the canonical compilation of the given XY Partition

Get the canonical compilation of the given compressed XY Partition

Clone the or node and redirect one of its parents to the new copy

Create new circuit nodes in the given context.

Compile a given variable, literal, or constant

Compress a given XY Partition (merge elements with identical subs)

Conjoin nodes into a single circuit

conjoin(root::LogicCircuit, lit::Lit; callback::Function)

Return the circuit conjoined with th given literal constrains callback is called after modifying conjunction node

function conjoin(s::Sdd, t::Sdd)::Sdd

Conjoins two SDDs.

Conjoin two SDDs

conjoin(s::SddLiteralNode, t::SddLiteralNode)::Sdd

Conjoin SDD Literal Nodes.

conjoin(arguments::Vector{<:PlainLogicCircuit})

Conjoins Plain LogicCircuits.

conjoin(arguments::Vector{<:PlainStructLogicCircuit})

Conjoins Structered LogicCircuits

Conjoin two SDDs when they respect the same vtree node

Conjoin two SDDs when one descends from the other

Conjoin two SDDs in separate parts of the vtree

Computes all possible valuations of scope V as conjunctions.

Get the logical constant in a given constant leaf node

Helper function to construct new SDD literal objects in SddMgrLeafNode constructor

Computes all possible valuations of scope V as both conjunctions and instantiation values.

Returns an approximation (does not account for some repeated nodes) of how many times each variable is mentioned in α.

Disjoin nodes into a single circuit

Eliminate a variable through disjunction. Equivalent to the expression (ϕ|x ∨ ϕ|¬x).

Decide whether one sentence logically entails another

Decide whether two sentences are logically equivalent

Constructs a BDD mapping to true if exactly n literals in L are in the input; otherwise false.

Constructs a BDD mapping to true if exactly n literals in L are in the input; otherwise false.

Construct a smoothed node from startvtr, when you get to endvtr insert the original node

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

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

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

Translates a cardinality constraint in normal pseudo-boolean constraint form into a BDD.

Since cardinality constraints correspond to having coefficients set to one, we ignore the C's.

Argument L corresponds to the vector of literals to be chosen from; b is how many literals in L are selected.

See Eén and Sörensson 2006.

Generate a fully factorized circuit over the given range of variables

Get the variable scope of the root of this vtree

Does the bitcircuit node have a single child?

Does the circuit have a contiguously indexed set of variables

implied_literals(root::LogicCircuit)::Union{BitSet, Nothing}

Compute at each node literals that are implied by the formula. nothing at a node means all literals are implied (i.e. the node's formula is false)

This algorithm is sound but not complete - all literals returned are correct, but some true implied literals may be missing.

infer_vtree(root::LogicCircuit)::Vtree

Infer circuits vtree if the circuit is struct-decomposable. Otherwise return nothing.

Initialize values from the data (data frames)

is_atom(α::Bdd)::Bool

Returns whether the given Bdd node is an atomic formula (i.e. a variable, ⊥, ⊤, or literal).

is_lit(α::Bdd)::Bool

Returns whether the given Bdd node represents a literal.

is_term(α::Bdd)::Bool

Returns whether this Bdd node is terminal.

is_var(α::Bdd)::Bool

Returns whether the given Bdd node represents a variable.

is_⊤(α::Bdd)::Bool

Returns whether the given Bdd node represents a ⊤.

is_⊥(α::Bdd)::Bool

Returns whether the given Bdd node represents a ⊥.

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

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

Is the circuit a conjunction of disjunctive clauses?

Is the node a constant gate?

isdecomposable(root::LogicCircuit)::Bool

Is the circuit decomposable?

isdeterministic(root::LogicCircuit)::Bool

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

Is the circuit a disjunction of conjunctive clauses?

Is the circuit syntactically equal to false?

Is the circuit a flat DNF or CNF structure?

Is the node an inner gate?

Is the node a leaf gate?

Is the node a literal gate?

Get the sign of the literal leaf node

issatisfiable(root::LogicCircuit)::Bool

Determine whether the logical circuit is satisfiable (has a satisfying assignment). Requires decomposability of the circuit.

issmooth(root::LogicCircuit)::Bool

Is the circuit smooth?

isstruct_decomposable(root::LogicCircuit)::Bool

Is the circuit structured-decomposable?

istautology(root::LogicCircuit)::Bool

Determine whether the logical circuit is a tautology (every assignment satisfies it; the sentence is valid). Requires decomposability and determinism of the circuit.

Is the circuit syntactically equal to true?

Is the node an And gate?

Is the node an Or gate?

Returns whether a variable x appears as a positive literal in α, given that α is a conjunction of literals.

Assumes ϕ is a full conjunction of literals. Returns ϕ as a zero-one vector and its scope.

Get the logical literal in a given literal leaf node

Get the list of literal nodes in a given circuit

Get a sequence of positive and negative literals

Loads a BDD from given file.

Supported file formats:

• CNF (.cnf);
• DNF (.dnf);
• BDD (.bdd).

To load as any of these file formats, simply set the filename with the desired extension.

Keyword arguments are passed down to the open function.

Loads a BDD from a file. Use load instead.

Loads a CNF as a BDD. Use load instead.

Loads a CNF as a BDD. Use load instead.

Make all variables in this circuit contiguously numbered. Return new circuit and the variable mapping.

Computes a mapping of the parents of each node.

Marginalize a variable through some binary operation.

Get the variable in the circuit with the largest index

Returns whether the formula (i.e. BDD) mentions a variable.

Get the manager of a Sdd node, which is its SddMgr vtree

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.

Compute the probability of each variable for a random satisfying assignment of the logical circuit

Get a sequence of negative literals

Negate an SDD

Runs a BFS on the mapping of parents, starting from either a ⊤ (true) or ⊥ (false) in order to find the corresponding CNF or DNF encoding.

Number of elements (conjunctions) in layer or bit circuit

or(α::Bdd, β::Bdd)::Bdd 
or(x::Integer, β::Bdd)::Bdd
or(α::Bdd, x::Integer)::Bdd
or(x::Integer, y::Integer)::Bdd
or(Φ::Vararg{Bdd})::Bdd
or(Φ::AbstractVector{Bdd})::Bdd
or(Φ::Vararg{T})::Bdd where T <: Integer
or(Φ::AbstractVector{T})::Bdd where T <: Integer
or(Φ::Vararg{Union{T, Bdd}})::Bdd where T <: Integer

Returns a disjunction over the given boolean functions.

Get the list of or nodes in a given circuit

Get a sequence of positive literals

Returns a Vector{Bdd} containing all nodes in α in post-order.

Get the prime, that is, the first conjunct

Pretty print a conjunction of literals BDD.

Pretty print BDD as a normal form (CNF or DNF).

Caution: may exponentially explode.

Alternatively, pretty prints using the given glyphs (default ∧, ∨ and ¬).

ϕ = (1 ∧ ¬2) ∨ (2 ∧ 3)
print_nf(α; out = false)

ϕ = (1 ∧ ¬2) ∨ (2 ∧ 3)
print_nf(α; out = false, which = "dnf", glyphs = ['+', '*', '-'])

Check equivalence using probabilistic equivalence checking. Note that this implentation may not have any formal guarantees as such.

prob_equiv_signature(circuit::LogicCircuit, k::Int)

Get a signature for each node using probabilistic equivalence checking. Note that this implentation may not have any formal guarantees as such.

Processes the mnist dataset using the MNIST object from MLDataSets package MLDS_MNIST = the MNIST from MLDataSets labeled = whether to return the lables

propagate_constants(root::LogicCircuit)

Remove all constant leafs from the circuit

Randomly picking egde and variable from candidates

Reduce a Bdd rooted at α inplace, removing duplicate nodes and redundant sub-trees. Returns canonical representation of α.

Replace node old with node new in circuit root

Does the circuit respect the given vtree? This function allows for constants in conjunctions, but only when a vtree node can be found where the left and right conjunct can be assigned to the left and right vtree.

Returns a new reduced Bdd restricted to instantiation X.

Returns a new Bdd restricted to instantiation X.

Returns a new Bdd restricted to instantiation X.

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.

Evaluate satisfaction of the circuit bottom-up for a given input

Evaluate the circuit bottom-up for a given input and return the value of all nodes

Compute the value and flow of each node

When values of nodes have already been computed, do a downward pass computing the flows at each node

Pass flows down the layers of a bit circuit on the GPU

Evaluate the layers of a bit circuit on the CPU (SIMD & multi-threaded)

CUDA kernel for passing flows down circuit

Evaluate the layers of a bit circuit on the GPU

Evaluate the layers of a bit circuit on the CPU (SIMD & multi-threaded)

CUDA kernel for circuit evaluation

Saves a BDD as a file.

Supported file formats:

• CNF (.cnf);
• DNF (.dnf);
• BDD (.bdd).

To save as any of these file formats, simply set the filename with the desired extension.

Keyword arguments are passed down to the open function.

Save as BDD. Use the save_bdd function instead.

Save as CNF. Use the save function instead.

Save as DNF. Use the save function instead.

Returns all variables in this formula as a Vector{Int}.

Returns all variables in this formula as a Set{Int}.

Obtain an SDD manager that can support compiling the given circuit

Count the number of decision nodes in the SDD

Count the number of decision and leaf nodes in the SDD

Count the number of elements in the decision nodes of the SDD

shallowhash(α::Bdd, h::UInt = UInt64(0))

Returns a shallow hash for the given node (not BDD as a whole).

Performs Shannon's Decomposition on the Bdd α, given a set of variables to isolate. Any decomposition that results in a ⊥ is discarded.

Performs Shannon's Decomposition on the Bdd α, given a variable to isolate.

Performs Shannon's Decomposition on the Bdd α, given a set of variables to isolate.

Get the other child of a parent element

smooth(root::LogicCircuit)

Create an equivalent smooth circuit from the given circuit.

Smooth an sdd to a StructLogicCircuit

smooth(root::StructLogicCircuit)::StructLogicCircuit

Create an equivalent smooth circuit from the given circuit.

smooth_node(node::LogicCircuit, missing_scope, lit_nodes)

Return a smooth version of the node where the missing_scope variables are added to the scope, using literals from lit_nodes

smooth_node(node::StructLogicCircuit, parent_scope, scope, lit_nodes, vtree_leaves)

Return a smooth version of the node where the are added to the scope by filling the gap in vtrees, using literals from lit_nodes

split_candidates(circuit::LogicCircuit)::Tuple{Vector{Tuple{LogicCircuit, LogicCircuit}}, Dict{LogicCircuit, BitSet}}

Return the edges and variables which can be splited on

Split step

Standardize the circuit:

1. Children of or nodes are and nodes.
2. Children of and nodes are or nodes.
3. Each and node has exactly two children.

Note: for circuits with parameters this function will not keep the parameters equavalent.

Structure learning manager

Get the sub, that is, the second and last conjunct

Returns a new terminal node of given boolean value.

Returns 0 if x is not a literal; else returns an integer representation of x.

Returns α as an integer literal. Assumes α is a leaf node.

Get the formula of a given circuit as a string, expanding the formula into a tree

train, valid, test = twenty_datasets(name)

Load a given dataset from the density estimation datasets. Automatically downloads the files as julia Artifacts. See https://github.com/UCLA-StarAI/Density-Estimation-Datasets for a list of avaialble datasets.

Construct a unique decision gate for the given vtree

Compute all possible valuations of scope V.

Get the variable in a vtree leaf

Get the logical variable in a given literal leaf node

Are the variables in n contained in the variables in m?

Are the variables in n contained in the left branch of m?

Are the variables in n contained in the right branch of m?

Get the vtree corresponding to the argument

Get the vtree corresponding to the argument, or nothing if the node has no vtree

zoo_cnf(name)

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

zoo_dnf(name)

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

zoo_jlc(name)

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

zoo_nnf(name)

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

zoo_sdd(name)

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

zoo_vtree(name)

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

Get the list of conjunction nodes in a given circuit

Get the list of disjunction nodes in a given circuit

TikzGraphs.plot(lc::LogicCircuit; simplify=false)

Plots a LogicCircuit using TikzGraphs. Needt o have LaTeX installed.

TikzGraphs.plot(vtree::Vtree)

Plots a vtree using TikzGraphs. Need to have LaTeX installed.