Internals

union_typeof(xs)

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

Z3

This module provides an interface to z3_jll.jl.

Library

add_clause(context, solver, clause)

Solutions

IteratorSize(::Type{Solutions})

Examples

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

eltype(::Type{Solutions})

The type of the elements generated by a Solutions iterator.

Examples

julia> eltype(PAndQ.Z3.Solutions)
Vector{Bool} (alias for Array{Bool, 1})

isdone

iterate

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_adjust

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, n)

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)
Vector{Bool} (alias for Array{Bool, 1})

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()

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, n)

Print the DIMACS format of the conjunctive clauses.

Examples

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

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

InterfaceError{F <: Function, O <: Operator} <: Exception
InterfaceError(::F, ::O)

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

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.

Kind

AbstractSyntaxTree

A proposition represented by an abstract syntax tree.

See also Operator.

Examples

julia> PAndQ.AbstractSyntaxTree(⊤)
⊤

julia> @atomize PAndQ.AbstractSyntaxTree(¬, [p])
¬p

julia> @atomize PAndQ.AbstractSyntaxTree(and, [PAndQ.AbstractSyntaxTree(p), PAndQ.AbstractSyntaxTree(q)])
p ∧ q

children(::AbstractSyntaxTree)

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

See also AbstractSyntaxTree.

Examples

julia> @atomize PAndQ.children(¬p)
1-element Vector{PAndQ.AbstractSyntaxTree}:
 p

julia> @atomize PAndQ.children(p ∧ q)
2-element Vector{PAndQ.AbstractSyntaxTree}:
 p
 q

nodevalue(::AbstractSyntaxTree)

Return the Operator of the proposition's root node.

See also AbstractSyntaxTree.

Examples

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

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

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

Print the representation of the proposition's root node.

See also Operator and AbstractSyntaxTree.

Examples

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

::AbstractSyntaxTree == ::AbstractSyntaxTree

hash(::AbstractSyntaxTree, ::UInt)

deconstruct(p)

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

See also nodevalue and children.

Examples

julia> @atomize PAndQ.deconstruct(p)
(PAndQ.AbstractSyntaxTree(:p), PAndQ.AbstractSyntaxTree[])

julia> @atomize PAndQ.deconstruct(¬p)
(not, PAndQ.AbstractSyntaxTree[PAndQ.AbstractSyntaxTree(:p)])

julia> @atomize PAndQ.deconstruct(p ∧ q)
(and, PAndQ.AbstractSyntaxTree[PAndQ.AbstractSyntaxTree(:p), PAndQ.AbstractSyntaxTree(:q)])

child(x)

Equivalent to only ∘ children.

See also children.

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.

prune(p, atoms = AbstractSyntaxTree[], mapping = Dict{AbstractSyntaxTree, Int}())

reconstruct(clauses, atoms)

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

See also AbstractSyntaxTree.

promote_rule