core.expressions package#

Submodules#

core.expressions.BooleanExpression module#

class core.expressions.BooleanExpression.AND(expressions: Set[BooleanExpression])[source]#

Bases: BooleanExpression

eval(instance: Dict[str, bool]) bool[source]#
fix(atom: str, positive: bool) BooleanExpression[source]#
get_input_variables() Set[str][source]#
negate() BooleanExpression[source]#
simplify() BooleanExpression[source]#

TODO: Flatten a conjunction of conjunctions e.g. (A & B) & (C & D) & (E & F) = A & B & C & D & E & F :return:

substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
to_z3() Bool[source]#
class core.expressions.BooleanExpression.BooleanExpression[source]#

Bases: ABC

copy()[source]#
abstract eval(instance: Dict[str, bool]) bool[source]#
abstract fix(atom: str, positive: bool) BooleanExpression[source]#
abstract get_input_variables() Set[str][source]#
abstract negate() BooleanExpression[source]#
static read(formula: str) BooleanExpression[source]#
abstract simplify() BooleanExpression[source]#
abstract substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
abstract to_z3() Bool[source]#
class core.expressions.BooleanExpression.FALSE[source]#

Bases: LITERAL

eval(instance: Dict[str, bool]) bool[source]#
fix(atom: str, positive: bool) LITERAL[source]#
get_input_variables() Set[str][source]#
negate() BooleanExpression[source]#
simplify() BooleanExpression[source]#
substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
to_z3() Bool[source]#
class core.expressions.BooleanExpression.IF(condition: BooleanExpression, true_expression: BooleanExpression, false_expression: BooleanExpression)[source]#

Bases: BooleanExpression

eval(instance: Dict[str, bool]) bool[source]#
fix(atom: str, positive: bool) BooleanExpression[source]#
get_input_variables() Set[str][source]#
negate() BooleanExpression[source]#
simplify() BooleanExpression[source]#
substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
to_z3() Bool[source]#
class core.expressions.BooleanExpression.LITERAL(name: str, positive: bool = True)[source]#

Bases: BooleanExpression

eval(instance: Dict[str, bool]) bool[source]#
fix(atom: str, positive: bool) LITERAL[source]#
get_input_variables() Set[str][source]#
negate()[source]#
simplify() BooleanExpression[source]#
substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
to_z3() Bool[source]#
class core.expressions.BooleanExpression.NOT(expression: BooleanExpression)[source]#

Bases: BooleanExpression

eval(instance: Dict[str, bool]) bool[source]#
fix(atom: str, positive: bool) BooleanExpression[source]#
get_input_variables() Set[str][source]#
negate() BooleanExpression[source]#
simplify() BooleanExpression[source]#
substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
to_z3() Bool[source]#
class core.expressions.BooleanExpression.OR(expressions: Set[BooleanExpression])[source]#

Bases: BooleanExpression

eval(instance: Dict[str, bool]) bool[source]#
fix(atom: str, positive: bool) BooleanExpression[source]#
get_input_variables() Set[str][source]#
negate() BooleanExpression[source]#
simplify() BooleanExpression[source]#
substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
to_z3() Bool[source]#
class core.expressions.BooleanExpression.TRUE[source]#

Bases: LITERAL

eval(instance: Dict[str, bool]) bool[source]#
fix(literal: LITERAL, positive: bool) LITERAL[source]#
get_input_variables() Set[str][source]#
negate() BooleanExpression[source]#
simplify() BooleanExpression[source]#
substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
to_z3() Bool[source]#
class core.expressions.BooleanExpression.XOR(expressions: Set[BooleanExpression])[source]#

Bases: BooleanExpression

eval(instance: Dict[str, bool]) bool[source]#
fix(atom: str, positive: bool) BooleanExpression[source]#
get_input_variables() Set[str][source]#
negate() BooleanExpression[source]#
simplify() BooleanExpression[source]#

To simplify a XOR operations over a set of sub-expressions, we do the following after [1]: Let E = [e_0, e_1, …, e_n] be an ordered list of the sub-expressions e_i. While the length of the list is greater than two, we apply the XOR operation over the list in a recursive manner. We group the first n elements ([e_0, …, e_(n-1)]) as one factor, and exclude e_n. Then, we apply the XOR over these two factors [e_0, …, e_(n-1)] and e_n. We recursively apply this to the list until we arrive at the base case. [1] https://math.stackexchange.com/questions/2480640/boolean-expression-of-3-input-xor-gate :return:

substitute(original: LITERAL, replacement: BooleanExpression) BooleanExpression[source]#
to_z3() Bool[source]#

Module contents#