rolling-stones.core — rolling-stones 1.0.0

! clj

AND clj

(AND & literals)

and? clj

(and? x)

at-least clj

(at-least n literals)

at-most clj

(at-most n literals)

CNF clj protocol

encode-cnf clj

(encode-cnf this)

Returns variable and clauses

constraint? clj

(constraint? c)

encode-constraint clj

(encode-constraint constraint)

Returns (cons new-constraint new-clauses)

exactly clj

(exactly n literals)

formula->cnf clj

(formula->cnf wff)

formula? clj

(formula? x)

IFF clj

iff? clj

(iff? x)

IMP clj

imp? clj

(imp? x)

NAND clj

(NAND & literals)

negate clj

(negate x)

negative? clj

NOR clj

(NOR & literals)

NOT clj

not? clj

(not? r)

OR clj

(OR & literals)

or? clj

(or? x)

positive? clj

solutions clj

(solutions clauses)

(solutions clauses timeout)

(solutions clauses timeout timeout-atom)

Takes a formula in integer CNF form, i.e., vector of constraints and vectors of non-zero ints and optional timeout in millis and optional atom to set to true if timeout occurs. Returns lazy sequence of all solutions. Stats attached as metadata to each solution.

solutions-symbolic-cnf clj

(solutions-symbolic-cnf clauses)

(solutions-symbolic-cnf clauses timeout)

(solutions-symbolic-cnf clauses timeout timeout-atom)

Takes a formula in symbolic CNF form, i.e., vector of constraints and vectors of variables and ! of variables, where variables are represented by arbitrary Clojure data. Also takes optional timeout in millis and optional atom to set to true if timeout occurs. Returns lazy sequence of solutions. Stats attached as metadata to each solution.

solutions-symbolic-formula clj

(solutions-symbolic-formula wffs)

(solutions-symbolic-formula wffs timeout)

(solutions-symbolic-formula wffs timeout timeout-atom)

Takes a formula in symbolic form, i.e., vector of constraints and formulas, where formulas are built with formula constructors such as AND, OR, XOR, IFF, NAND, NOR, IMP, NOT, and formula variables are represented by arbitrary Clojure data. Also takes optional timeout in millis and optional atom to set to true if timeout occurs. Returns lazy sequence of all solutions. Stats attached as metadata.

solve clj

(solve clauses)

(solve clauses timeout)

(solve clauses timeout timeout-atom)

Takes a formula in integer CNF form, i.e., vector of constraints and vectors of non-zero ints and optional timeout in millis and optional atom to set to true if timeout occurs. Returns solution or nil if no solution exists. Stats attached as metadata.

solve-symbolic-cnf clj

(solve-symbolic-cnf clauses)

(solve-symbolic-cnf clauses timeout)

(solve-symbolic-cnf clauses timeout timeout-atom)

Takes a formula in symbolic CNF form, i.e., vector of constraints and vectors of variables and ! of variables, where variables are represented by arbitrary Clojure data. Also takes optional timeout in millis and optional atom to set to true if timeout occurs. Returns solution or nil if no solution exists. Stats attached as metadata.

solve-symbolic-formula clj

(solve-symbolic-formula wffs)

(solve-symbolic-formula wffs timeout)

(solve-symbolic-formula wffs timeout timeout-atom)

Takes a formula in symbolic form, i.e., vector of constraints and formulas, where formulas are built with formula constructors such as AND, OR, XOR, IFF, NAND, NOR, IMP, NOT, and formula variables are represented by arbitrary Clojure data. Also takes optional timeout in millis and optional atom to set to true if timeout occurs. Returns solution or nil if no solution exists. Stats attached as metadata.

temporary? clj

(temporary? var)

true-integer-variables clj

(true-integer-variables coll)

Returns a set of all the true variables from a collection of integer variables. Returns nil if passed nil.

true-symbolic-variables clj

(true-symbolic-variables coll)

Returns a set of all the true variables from a collection of symbolic variables. Returns nil if passed nil.

XOR clj

xor? clj

(xor? x)