Internals

union_typeof(xs)

Equivalent to Union{map(typeof, xs)...}.

Examples

julia> PAndQ.union_typeof((⊤, ¬, ∧))
Union{PAndQ.Interface.Operator{:tautology}, PAndQ.Interface.Operator{:not}, PAndQ.Interface.Operator{:and}}

PicoSAT

This module provides an interface to libpicosat_jll.jl.

picosat_init()

Construct a new PicoSAT instance and return a pointer to it.

picosat_reset(pico_sat)

Destruct the pico_sat instance.

picosat_add(pico_sat, literal)

Append the literal to the pico_sat instance's current disjunctive clause.

picosat_variables(pico_sat)

Return the number of unique atoms in the pico_sat instance.

picosat_print(pico_sat, file)

Write the DIMACS format of the pico_sat instance's proposition to the given file.

picosat_sat(pico_sat, limit)

Search for a satisfiable assignment of the pico_sat instance's proposition and return 0, 10, or 20 if the status is unknown, satisfiable, or unsatisfiable, respectively.

picosat_deref(pico_sat, atom)

Return the assignment of the atom, where 1, -1, and 0 indicate true, false, and unknown, respectively.

This function must be called after verifying that the status of picosat_sat is satisfiable.

add_clause(pico_sat, clause)

Mutate the pico_sat instance's proposition to be the conjunction of itself and the disjunctive clause.

initialize(clauses)

Return a PicoSAT pointer with its proposition being a conjunction of the disjunctive clauses.

Solutions
Solutions(clauses)

A stateful iterator of valuations that satisfy the given proposition.

Calling finalize on this iterator will first check whether it has already been finalized. If not, it will call picosat_reset on its PicoSAT pointer and set the pointer equal to C_NULL.

eltype(::Type{Solutions})

The type of the elements generated by a Solutions iterator.

Examples

julia> eltype(PAndQ.PicoSAT.Solutions)
Base.Generator{Base.Iterators.Enumerate{Base.Iterators.Filter{Base.Fix2{typeof(!=), Int64}, Vector{Int32}}}, Base.Splat{typeof(*)}}

IteratorSize(::Type{Solutions})

Since counting the number of Solutions to a proposition is intractable, its IteratorSize is Base.SizeUnknown.

Examples

julia> Base.IteratorSize(PAndQ.PicoSAT.Solutions)
Base.SizeUnknown()

is_satisfiable(pico_sat)

Return whether the pico_sat instance's status is currently satisfiable.

isdone(solutions::Solutions, pico_sat = solutions.pico_sat)

Return a Boolean whether the pico_sat instance can yield any more solutions without advancing the Solutions iterator.

Finalize the iterator if it has not yet been finalized and is done.

iterate(solutions::Solutions, pico_sat = solutions.pico_sat)

If the status of pico_sat is_satisfiable, return a Tuple of the current solution and pico_sat. Otherwise, finalize the solutions and return nothing.

print_dimacs(io, clauses)

Print the DIMACS format of the conjunctive clauses.

The io can be an IO or file path String to write to.

Examples

julia> PAndQ.PicoSAT.print_dimacs(stdout, [[-1, -2], [1, 2]])
p cnf 2 2
-1 -2 0
1 2 0

julia> PAndQ.PicoSAT.print_dimacs(stdout, [[1, -2], [-1, 2]])
p cnf 2 2
1 -2 0
-1 2 0

InterfaceError{F <: Function, O <: Operator, N <: Union{Nothing, Int}} <: Exception
InterfaceError(::F, ::O, ::N)

An Exception indicating that the function of type F has not been implemented for the value of type T.

If N is Nothing, then the function does not accept any propositions. Otherwise, N is the number of propositions given.

showerror(::IO, ::InterfaceError)

Print a message indicating to implement a method of an interface.

@interface(f, xs...)

Define a fallback method that throws an InterfaceError.

NullaryOperator

The Union of Nullary Operators.

UnaryOperator

The Union of Unary Operators.

BinaryOperator

The Union of Binary Operators.

NaryOperator

The Union of Nary Operators.

AndOr

The Union of and and or.

Proposition

A proposition.

Supertype of Atom and Compound.

Atom <: Proposition

A proposition with no deeper propositional structure.

Subtype of Proposition. Supertype of Constant and Variable.

Compound <: Proposition

A proposition composed from connecting Atoms with one or more Operators.

Subtype of Proposition. Supertype of Tree, Clause, and Normal.

Constant <: Atom
Constant(value)

An atomic sentence.

Subtype of Atom.

Examples

julia> PAndQ.Constant(1)
$(1)

julia> PAndQ.Constant("Logic is fun")
$("Logic is fun")

Variable <: Atom

An atomic formula.

Subtype of Atom.

Examples

julia> PAndQ.Variable(:p)
p

julia> PAndQ.Variable(:q)
q

Tree{N} <: Compound
Tree(::Operator, ::Union{Atom, Tree}...)

A Proposition represented by an abstract syntax tree.

Subtype of Compound. See also Operator and Atom.

Examples

julia> PAndQ.Tree(⊤)
⊤

julia> @atomize PAndQ.Tree(¬, p)
¬p

julia> @atomize PAndQ.Tree(and, PAndQ.Tree(p), PAndQ.Tree(q))
p ∧ q

Clause{AO <: AndOr} <: Compound
Clause(::AO, ::Vector{<:Atom}, ::Set{Int})

A proposition represented as either a conjunction or disjunction of literals.

Subtype of Compound. See also AndOr and Atom.

Examples

julia> PAndQ.Clause(∧, PAndQ.Atom[], Set{Int}())
⊤

julia> @atomize PAndQ.Clause(∧, [p], Set(1))
p

julia> @atomize PAndQ.Clause(∨, [p, q], Set([1, -2]))
¬q ∨ p

Normal{AO <: AndOr} <: Compound
Normal(::AO, ::Vector{Atom}, ::Set{Set{Int}})

A Proposition represented in conjunctive or disjunctive normal form.

Subtype of Compound. See also AndOr and Clause.

Examples

julia> PAndQ.Normal(∧, PAndQ.Atom[], Set{Set{Int}}())
⊤

julia> @atomize PAndQ.Normal(∧, [p, q], Set(map(Set, ((1, 2), (-1, -2)))))
(¬p ∨ ¬q) ∧ (p ∨ q)

children(::Union{Tree, Clause, Normal})

Return an iterator over the child nodes of the given proposition.

See also Tree, Clause, and Normal.

Examples

julia> @atomize PAndQ.children(p)
()

julia> @atomize PAndQ.children(¬p)
(PAndQ.Variable(:p),)

julia> @atomize PAndQ.children(p ∧ q)
(identical(PAndQ.Variable(:p)), identical(PAndQ.Variable(:q)))

nodevalue(::Union{Tree, Clause, Normal})

Return the Operator of the proposition's root node.

See also Tree, Clause, and Normal.

Examples

julia> @atomize PAndQ.nodevalue(¬p)
¬

julia> @atomize PAndQ.nodevalue(p ∧ q)
∧

printnode(::IO, ::Union{Operator, Proposition}; kwargs...)

Print the representation of the proposition's root node.

See also Operator and Proposition.

Examples

julia> @atomize PAndQ.printnode(stdout, p)
p
julia> @atomize PAndQ.printnode(stdout, ¬p)
¬
julia> @atomize PAndQ.printnode(stdout, p ∧ q)
∧

NodeType(::Type{<:Atom})

See also Atom.

Examples

julia> PAndQ.NodeType(PAndQ.Atom)
AbstractTrees.HasNodeType()

nodetype(::Type{<:Atom})

See also Atom.

julia> PAndQ.nodetype(PAndQ.Atom)
PAndQ.Atom

deconstruct(p)

Return (nodevalue(p), children(p)).

See also nodevalue and children.

Examples

julia> @atomize PAndQ.deconstruct(p)
(PAndQ.Variable(:p), ())

julia> @atomize PAndQ.deconstruct(¬p)
(PAndQ.Interface.Operator{:not}(), (PAndQ.Variable(:p),))

julia> @atomize PAndQ.deconstruct(p ∧ q)
(PAndQ.Interface.Operator{:and}(), (identical(PAndQ.Variable(:p)), identical(PAndQ.Variable(:q))))

child(x)

Equivalent to only ∘ children.

See also children.

load_or_error(x)

Return an expression that when evaluated returns x if PAndQ is defined and throws an Exception otherwise.

atomize(x)

If x is a symbol, return an expression that instantiates it as a Variable if it is undefined in the caller's scope. If isexpr(x, :$), return an expression that instantiates it as a Constant. If x is a different expression, traverse it with recursive calls to atomize. Otherise, return x.

distribute(p)

Given a proposition in negation normal form, return that proposition in conjunction normal form.

flatten(p)

eval_pairs(f, pairs)

Define f(::typeof(left)) = right and f(::typeof(right)) = left for each pair left and right in pairs.

convert(::Type{<:Proposition}, p)

See also Proposition.

promote_rule