Module Reference#

bauhaus is a library for building logical theories on the fly with Python.

class bauhaus.Encoding[source]#

An Encoding object stores the propositions and constraints you create on the fly with @proposition and @constraint decorators and functions.

When you’re ready, you can compile your constraints into a logical theory in conjunctive or negation normal form to submit to a SAT solver.

If you’re interested in debugging your theory or learning about its origin story from each propositional object to the final theory, call the introspect() function on your encoding.

__init__()[source]#

Creates an Encoding object. This will store propositions and constraints that you can compile into a theory.

propositions#

Stores decorated classes/functions pointing to their associated instances.These are later used to build the theory’s constraints.

Type: defaultdict(weakref.WeakValueDictionary)

constraints#

A set of unique _ConstraintBuilder objects that hold relevant information to build an NNF constraint. They are added to the Encoding object whenever the constraint decorator is used or when it is called as a function.

Type: set

debug_constraints#

Maps ConstraintBuilder objects to their compiled constraints for debugging purposes.

Type: dictionary

add_constraint(constraint: NNF)[source]#

Add an NNF constraint to the encoding.

Parameters: cons (NNF) – Constraint to be added.

clear_constraints()[source]#: Clears the constraints of an Encoding object

clear_debug_constraints()[source]#: Clear debug_constraints attribute in Encoding

compile(CNF=True) → NNF[source]#

Convert constraints into a theory in conjunctive normal form, or if specified, the simpler negation-normal form.

Parameters: CNF (bool) – Default is True. Converts a theory to CNF.
Returns: theory – Conjunctive or Negation normal form of constraints.
Return type: NNF

disable_custom_constraints()[source]#: Disable the functionality for using custom_constraints

introspect(solution: Optional[dict] = None, var_level=False)[source]#

Observing the origin of a theory from each propositional object to the final constraint.

Details#

The mapping is structured like so,

Encoding.debug_constraints : dictionary

key -> ConstraintBuilder object

value -> Clause built in Encoding.compile()

Each ConstraintBuilder object has the attribute instance_constraints : defaultdict with,

key -> Object (from annotated class or method)

value -> List of constraint clauses created per object

This allows you to view the constraints created for annotated classes or methods and the per-instance object constraints, along with the final (succinct) constraint.

param solution: Optional; A solution to use to highlight output.
type solution: dictionary
param var_level: Defaults to False; If True, output coloring will be based on the variable instead of the literal.
type var_level: boolean

pprint(formula, solution: Optional[dict] = None, var_level=False)[source]#

Pretty print an NNF formula

Parameters

formula (NNF) – Formula to be displayed.
solution (dictionary) – Optional; A solution to use to highlight output.
var_level (boolean) – Defaults to False; If True, output coloring will be based on the variable instead of the literal.

purge_propositions()[source]#: Purges the propositional variables of an Encoding object

class bauhaus.constraint[source]#

Creates constraints on the fly when used as a decorator or as a function invocation.

The constraint class directs all function invokations of constraint methods to the classmethod _constraint_by_function.

@constraint.method calls are directed to classmethod _decorate.

In both cases, a _ConstraintBuilder object is created to store the given information.

Supports the following SAT constraints:

At least one
At most one
Exactly one
At most K
Implies all

Examples

Decorator for class or method:

@constraint.at_most_one(e)
@proposition
class A:

    @constraint.implies_all(e)
    def do_something(self):
        pass

Constraint creation by function call: constraint.add_at_least_one(e, *args)

add_at_least_one(*args)[source]#

At least one of the propositional variables are True

Constraint is added directly with this function.

Parameters: encoding (Encoding) – Given encoding.

Example

@constraint.add_at_least_one(encoding, [Obj, Class, Class.method])

add_at_most_k(k: int, *args)[source]#

At most K of the propositional variables are True

Constraint is added directly with this function.

Parameters

encoding (Encoding) – Given encoding.
k (int) – The number of variables that are true at one time. Must be less than the number of total variables for the constraint.

Example

@constraint.add_at_most_k(encoding, k, [Obj, Class, Class.method])

add_at_most_one(*args)[source]#

At most one of the propositional variables are True

Constraint is added directly with this function.

Parameters: encoding (Encoding) – Given encoding.

Example

@constraint.add_at_most_one(encoding, [Obj, Class, Class.method])

add_exactly_one(*args)[source]#

Exactly one of the propositional variables are True

Constraint is added directly with this function.

Parameters: encoding (Encoding) – Given encoding.

Example

@constraint.add_exactly_one(encoding, [Obj, Class, Class.method])

add_implies_all(left, right)[source]#

Left proposition(s) implies right proposition(s)

Constraint is added directly by calling this function.

Parameters

encoding (Encoding) – Given encoding.
left (list) – Propositional variables for the left side of an implication.
right (list) – Propositional variables for the right side of an implication.

Example

constraint.add_implies_all(encoding, left=[Obj, 'hello'], right=['goodbye'])

add_none_of(*args)[source]#

None of the propositional variables are True

Constraint is added directly with this function.

Parameters: encoding (Encoding) – Given encoding.

Example

@constraint.add_none_of(encoding, [Obj, Class, Class.method])

at_least_one(**kwargs)[source]#

At least one of the propositional variables are True.

Constraint is added with the @constraint decorator.

Parameters: encoding (Encoding) – Given encoding.

Example

@constraint.at_least_one(encoding)

at_most_k(k: int, **kwargs)[source]#

At most K of the propositional variables are True

Constraint is added with the @constraint decorator.

Parameters

encoding (Encoding) – Given encoding.
k (int) – The number of variables that are true at one time. Must be less than the number of total variables for the constraint.

Example

@constraint.at_most_k(encoding, k)

at_most_one(**kwargs)[source]#

At most one of the propositional variables are True.

Constraint is added with the @constraint decorator.

Parameters: encoding (Encoding) – Given encoding.

Example

@constraint.at_most_one(encoding)

exactly_one(**kwargs)[source]#

Exactly one of the propositional variables are True.

Constraint is added with the @constraint decorator.

Parameters: encoding (Encoding) – Given encoding.

Example

@constraint.exactly_one(encoding)

implies_all(left=None, right=None, **kwargs)[source]#

Left proposition(s) implies right proposition(s)

Constraint is added with the @constraint decorator.

Parameters

encoding (Encoding) – Given encoding.
left (list) – Propositional variables for the left side of an implication.
right (list) – Propositional variables for the right side of an implication.

Example

Above a class, each instance will be on the left side of an implication. You need to define a right side of the implication if you are decorating a class.:

@constraint.implies_all(encoding, right=[Obj])
@proposition(e)
class A(Object):
    pass

Above a method in a class, each instance will be on the left side of an implication. The return value(s) will be the right side of the implication. You can provide additional variables for either the left or right side.:

@proposition(e)
class A(object):

    def __init__(self, data):
        self.data = data

    @constraint.implies_all(encoding)
    def foo(self):
        return self.data

none_of(**kwargs)[source]#

None of the propositional variables are True.

Constraint is added with the @constraint decorator.

Parameters: encoding (Encoding) – Given encoding.

Example

@constraint.none_of(encoding)

bauhaus.print_theory(theory: Optional[dict], format: str = 'truth')[source]#

Prints a solved theory in a human readable format.

Propositions are printed according to their str or repr functions.

Parameters

theory (dict) – The theory to print.
format (str) –
The format to print the theory in. One of “truth”, “objects”, or “both”. Defaults to truth.

truth: group output by truth values. objects: group output by object types. both: group output primarily by truth values, and secondarily by object type.

bauhaus.proposition(encoding: Encoding)[source]#

Create a propositional variable from the decorated class or function.

Adds propositional variable to Encoding.

Return original object instance.

Parameters: encoding (Encoding) – Given encoding object.
Returns: The decorated function
Return type: function

Examples

Each instance of class A is added to propositions in the given Encoding object:

e = Encoding()
@proposition(e)
class A(object):
    pass
>> e.propositions = {'A': {id: object}}