Classes
class	Invariant
class	InvariantPart
class	SafeInvariant
class	UnsafeInvariant
Functions
def	ensure_conjunction_sat
def	ensure_cover
def	ensure_inequality
def	find_unique_variables
def	get_literals
def	instantiate_factored_mapping
def	invert_list

Function Documentation

def invariants.ensure_conjunction_sat	(	system,
		parts
	)

Modifies the constraint system such that it is only solvable if the
   conjunction of all parts is satisfiable. 

   Each part must be an iterator, generator, or an iterable over
   literals.

Definition at line 58 of file invariants.py.

def invariants.ensure_cover	(	system,
		literal,
		invariant,
		inv_vars
	)

Modifies the constraint system such that it is only solvable if the
   invariant covers the literal

Definition at line 90 of file invariants.py.

def invariants.ensure_inequality	(	system,
		literal1,
		literal2
	)

Modifies the constraint system such that it is only solvable if the
   literal instantiations are not equal (ignoring whether one is negated and
   the other is not)

Definition at line 97 of file invariants.py.

def invariants.find_unique_variables	(	action,
		invariant
	)

Definition at line 31 of file invariants.py.

def invariants.get_literals ( condition )

Definition at line 49 of file invariants.py.

def invariants.instantiate_factored_mapping ( pairs )

Definition at line 25 of file invariants.py.

def invariants.invert_list ( alist )

Definition at line 18 of file invariants.py.

Classes

Functions

Function Documentation