pygplib package

Submodules

pygplib.absexpr module

Base class of logical formula as well as index generator

class pygplib.absexpr.AbsExpr(tag: str, left: AbsExpr = None, right: AbsExpr = None, aux: tuple = ())

Bases: object

Abstract class of logical formulas.

Each formula is a graph made up of objects of the same formula class. Each such object represents either an atom or a logical operator with operands. Instance methods are operations related to a single object such as getters of object fields, while class methods are operations for the whole formula. Each formula class is supposed to have dedicated constructor, and it is not supposed to create a new object by invoking an ordinary constructor directly like AbsExpr().

_unique_table

dict. to find an object from its string representation.

_ATOM_TAGS

tuple of strings, representing types of atom.

_BINOP_TAGS

tuple of strings, representing types of binary operator.

_UNOP_TAGS

tuple of strings, representing types of uniary operator.

_EXPR_TAGS

tuple of available tags in this class.

_COMMA

string to represent comma.

_LPAREN

string to represent left parentheses.

_RPAREN

string to represent right parentheses.

Note

The current implementation, for the sake of simplicity, does not provide the functionality of deleting unnecessary objects.

compute_cnf_step(igen: IndexGen, assoc: dict, cnf: list) → None

Performs CNF compuation for this object.

compute_nnf_step(negated: bool, s: list[list], t: list[list]) → None

Performs NNF compuation for this object.

gen_key() → str

Converts object into string.

The returned string consists of the top-most operator and its operands only, which is mainly used as identifiers (as keys for _unique_table) to decide whether formulas are syntatically identical.

classmethod get_comma_tag() → str

Gets tag of comma.

classmethod get_lparen_tag() → str

Gets tag of left parenthesis.

get_operand(i: int) → AbsExpr

Gets an operand of the top-most operator of the formula.

For binary operation, the left operand and the right operand are returned when i = 1 and 2, respectively. For quanfier and unary operation, the unique operand is returned when i = 1.

classmethod get_rparen_tag() → str

Gets tag of right parenthesis.

get_tag() → str

Gets the tag of the top-most operator of the formula.

is_atom() → bool

Is it an atomic formula ?

is_atom_term() → bool

Is it an atomic formula ?

is_binop() → bool

Is the top-most operator a binary operation ?

is_binop_term() → bool

Is the top-most operator a binary operation ?

is_unop() → bool

Is the top-most operator a unary operation ?

is_unop_term() → bool

Is the top-most operator a unary operation ?

make_node_str_step() → str

Makes string of this object for DOT print.

make_str_in_step() → str

Makes string of this object in infix order.

make_str_post_step() → str

Makes string of this object in postfix order.

make_str_pre_step() → str

Makes string of this object in prefix order.

partitioning_order = False

changes order of applying binary operations (see binop_batch())

reduce_formula_step(assoc: dict, st: BaseRelSt) → None

Performs reduce compuation for this object.

class pygplib.absexpr.IndexGen(init_index: int = 1)

Bases: object

Generates indices.

Parameters:

init_index – initial index

_init

initial index

_next

next index

clear(init_index: int = 1) → None

Clears index with init_index.

get_count() → int

Gets the number of indices issued so far.

get_next() → int

Gets the next index.

pygplib.absfo module

Class of first-order logic of graphs with True, False, and no other atom

class pygplib.absfo.AbsFo(tag: str, left: AbsExpr = None, right: AbsExpr = None, aux: tuple = ())

Bases: AbsProp

First-order logic of graphs with true and false and no other atoms.

Node           |  self._aux[0]  | self._aux[1]
---------------|----------------|--------------
True  constant |  -             | -
False constant |  -             | -
Quantifier     | index of       | -
               | bound variable |

Note

In the current implementation, syntactically identical subexpressions are shared. We have to keep it in mind that this might become source of bugs. For instance, consider (? [x] : x) & x. In this formula, the second occurrence of x is a bound variable, and third occurrence is a free variable. In the current implementation, despite different semantics, these variables are shared, that is, they are represented as a single object in the representation of the formula. We do this for the sake of simplicity, but this might become source of bugs. When we apply some operation to such a formula, we sometimes have to consider difference in semantics.

_FORALL

string, representing universal quantifier.

_EXISTS

string, representing existential quantifier.

_ATOM_TAGS

tuple of strings, representing types of atom.

_BINOP_TAGS

tuple of strings, representing types of binary operator.

_UNOP_TAGS

tuple of strings, representing types of uniary operator.

_QF_TAGS

tuple of strings, representing types of quantifier.

_EXPR_TAGS

tuple of available tags in this class.

compute_nnf_step(negated: bool, s: list[list], t: list[list]) → None

Performs NNF computation for this object.

classmethod exists(left: AbsExpr, bvar: int) → AbsExpr

Gets the formula obtained by applying existential quantifier.

Parameters:

• left – formula to be quantified

• bvar – index of variable to be bounded.

classmethod forall(left: AbsExpr, bvar: int) → AbsExpr

Gets the formula obtained by applying universal quantifier.

Parameters:

• left – formula to be quantified

• bvar – index of variable to be bounded.

get_bound_var() → int

Gets the index of bound variable.

classmethod get_exists_tag() → str

“Gets tag of exists.

classmethod get_forall_tag() → str

Gets tag of forall.

get_free_vars_and_consts_post_step(bound_vars: list, free_vars: list) → None

Performs computation in postfix order for this object.

get_free_vars_and_consts_pre_step(bound_vars: list, free_vars: list) → None

Performs computation in prefix order for this object.

is_exists() → bool

Is the top-most operator the existential quantifier ?

is_exists_term() → bool

Is the top-most operator the existential quantifier ?

is_forall() → bool

Is the top-most operator the universal quantifier ?

is_forall_term() → bool

Is the top-most operator the universal quantifier ?

is_qf() → bool

Is the top-most operator universal or existential quantifier ?

is_qf_term() → bool

Is the top-most operator universal or existential quantifier ?

make_node_str_step() → str

Makes string of this object for DOT print.

make_str_in_step() → str

Makes string in infix order for this object.

make_str_post_step() → str

Makes string in postfix order for this object.

make_str_pre_step() → str

Makes string in prefix order for this object.

classmethod qf(tag: str, left: AbsExpr, bvar: int) → AbsExpr

Gets the formula obtained by applying the tag-specified quantifier.

Parameters:

• tag – tag of quantifier

• left – formula to be quantified

• bvar – index of variable to be bounded.

reduce_formula_step(assoc: dict, st: BaseRelSt) → None

Performs reduce compuation for this object.

substitute_step(y: int, x: int, assoc: dict) → None

Performs substitution for this object.

pygplib.absneg module

Class of abstract logical formula with true/false constants and negation

class pygplib.absneg.AbsNeg(tag: str, left: AbsExpr = None, right: AbsExpr = None, aux: tuple = ())

Bases: AbsExpr

Class of abstract expressions with true and false and negation only.

Node           |  self._aux[0]  | self._aux[1]
---------------|----------------|--------------
True  constant |  -             | -
False constant |  -             | -

_NEG

string, representing logical negation.

_TRUE_CONST

string, representing true.

_FALSE_CONST

string, representing false.

_ATOM_TAGS

tuple of strings, representing types of atom.

_BINOP_TAGS

tuple of strings, representing types of binary operator.

_UNOP_TAGS

tuple of strings, representing types of uniary operator.

_EXPR_TAGS

tuple of available tags in this class.

compute_cnf_step(igen: IndexGen, assoc: dict, cnf: list) → None

Performs CNF computation for this object.

compute_nnf_step(negated: bool, s: list[list], t: list[list]) → None

Perform NNF computation for this object.

classmethod false_const() → AbsExpr

Gets the false atom, the atom that always evaluates to false.

classmethod get_false_const_tag() → str

Gets tag of false constant.

classmethod get_neg_tag() → str

Gets tag of negation.

classmethod get_true_const_tag() → str

Gets tag of true constant.

is_const_atom() → bool

Is it either the true constant atom or the false constant atom ?

is_false_atom() → bool

Is it the false constant atom ?

is_neg() → bool

Is the top-most operator the logical negation ?

is_neg_term() → bool

Is the top-most operator the logical negation ?

is_true_atom() → bool

Is it the true constant atom ?

make_node_str_step() → str

Makes string of this object for DOT print.

make_str_in_step() → str

Makes string in infix order for this object.

make_str_post_step() → str

Makes string in postfix order for this object.

make_str_pre_step() → str

Makes string in prefix order for this object.

classmethod neg(left: AbsExpr) → AbsExpr

Gets the formula obtained by applying negation to the operand.

Parameters:

left – the formula to be negated

reduce_formula_step(assoc: dict, st: BaseRelSt) → None

Performs reduce computation for this object.

classmethod true_const() → AbsExpr

Gets the true atom, the atom that always evaluates to true.

pygplib.absprop module

Class of propositional logic with true and false and no variable

class pygplib.absprop.AbsProp(tag: str, left: AbsExpr = None, right: AbsExpr = None, aux: tuple = ())

Bases: AbsNeg

Expression of Propositional Logic with true and false and no variable

Node           |  self._aux[0]  | self._aux[1]
---------------|----------------|--------------
True  constant |  -             | -
False constant |  -             | -

_LAND

string, representing logical conjunction.

_LOR

string, representing logical disjunction.

_IMPLIES

string, representing logical implication.

_IFF

string, representing logical equivalence.

_ATOM_TAGS

tuple of strings, representing types of atom.

_BINOP_TAGS

tuple of strings, representing types of binary operator.

_UNOP_TAGS

tuple of strings, representing types of uniary operator.

_EXPR_TAGS

tuple of available tags in this class.

classmethod binop(tag: str, left: AbsExpr, right: AbsExpr) → AbsExpr

Gets the formula obtained applying the tag-specified operation.

Parameters:

• tag – tag of binary operation

• left – left operand

• right – right operand

classmethod binop_batch(tag: str, expr_li: list) → AbsExpr

Gets the formula obtained from a list of formulas by applying operations.

If partitioning_order is set True, operations are recusively applied by partitioning operands into the left and the right halves. Otherwise, operations are iteratively applied in a left-associative way.

Parameters:

• tag – tag of AND or OR operation

• expr_li – list of operands

classmethod bitwise_binop(tag: str, left_li: list, right_li: list) → AbsExpr

Performs binary operation in bitwise manner.

compute_cnf_step(igen: IndexGen, assoc: dict, cnf: list) → None

Performs CNF computation for this object.

compute_nnf_step(negated: bool, s: list[list], t: list[list]) → None

Performs NNF computation for this object.

classmethod get_iff_tag() → str

Gets tag of logical equivalence.

classmethod get_implies_tag() → str

Gets tag of logical implication.

classmethod get_land_tag() → str

Gets tag of logical AND.

classmethod get_lor_tag() → str

Gets tag of logical OR.

classmethod iff(left: AbsExpr, right: AbsExpr) → AbsExpr

Gets the formula obtained by applying equivalence to operands.

Parameters:

• left – left operand

• right – right operand

classmethod implies(left: AbsExpr, right: AbsExpr) → AbsExpr

Gets the formula obtained by applying implication to operands.

Parameters:

• left – left operand

• right – right operand

is_iff() → bool

Is the top-most operator logical equivalence ?

is_iff_term() → bool

Is the top-most operator logical equivalence ?

is_implies() → bool

Is the top-most operator logical implication ?

is_implies_term() → bool

Is the top-most operator logical implication ?

is_land() → bool

Is the top-most operator logical conjunction ?

is_land_term() → bool

Is the top-most operator logical conjunction ?

is_lor() → bool

Is the top-most operator logical disjunction ?

is_lor_term() → bool

Is the top-most operator logical disjunction ?

classmethod land(left: AbsExpr, right: AbsExpr) → AbsExpr

Gets the formula obtained by applying conjunction to operands.

Parameters:

• left – left operand

• right – right operand

classmethod lor(left: AbsExpr, right: AbsExpr) → AbsExpr

Gets the formula obtained by applying disjunction to operands.

Parameters:

• left – left operand

• right – right operand

make_node_str_step() → str

Makes string of this object for DOT print.

make_str_in_step() → str

Makes string in infix order for this object.

make_str_post_step() → str

Makes string in postfix order for this object.

make_str_pre_step() → str

Makes string in prefix order for this object.

reduce_formula_step(assoc: dict, st: BaseRelSt) → None

Performs reduce computation for this object.

pygplib.be module

Class of Boolean encoding of variables

class pygplib.be.Be(length: int)

Bases: object

Class of Boolean encoding of variables

A variable is encoded to a sequence of Boolean variables of fixed-length.

code_length

length of boolean encoding of a variable

exists_boolean_var(i: int, pos: int) → bool

Answers whether there is a Boolean var k, given symbol index and pos.

Parameters:

• i – variable or constant symbol index

• pos – code position ranging from 0 to the code length minus 1.

Returns:

returns True if for some k, k == get_boolean_var(i, pos).

Return type:

bool

exists_symbol(k: int) → bool

Answers whether there exists symbol index, given Boolean var. index.

Parameters:

k – Boolean variable index

Returns:

returns True if for some i, k == get_boolean_var(i, j).

Return type:

bool

get_boolean_var(i: int, pos: int) → int

Returns a Boolean encoding of a variable at a given position.

Parameters:

• i – index of variable symbol

• pos – code position ranging from 0 to the code length minus 1.

Returns:

index of Boolean variable

get_boolean_var_list(i: int) → list[int]

Returns a Boolean encoding of a variable.

Parameters:

i – index of variable symbol

Returns:

list of Boolean variables

get_code_pos(k: int) → int

Returns code position, given Boolean variable index.

Parameters:

k – Boolean variable index

Returns:

code position ranging from 0 to the code length minus 1.

Return type:

int

get_symbol_index(k: int) → int

Returns symbol index, given Boolean variable index.

Parameters:

k – Boolean variable index

Returns:

variable or constant symbol index

Return type:

int

get_variable_position_pair(k: int) → tuple[int, int]

Decode a Boolean variable to a variable and a position.

Parameters:

k – index of Boolean variable

Returns:

index of a variable symbol and a position

is_decodable_boolean_var(k: int) → bool

Is it a decodable Boolean variable?

Parameters:

k – index of Boolean variable

Returns:

returns True if for some i, k == get_boolean_var(i, j).

Return type:

bool

Note

auxiliary propositional variables are not decodable.

pygplib.cnf module

CNF Converter Class

class pygplib.cnf.Cnf(li: Iterable, st: BaseRelSt = None, check_cnf: bool = False)

Bases: object

CNF Converter Class

base

number of decodable variables

cnf

CNF, where variables are renumbered so that all indices from 1 to nvar appear at least once and all indices from 1 to base are decodable.

decode_assignment(assign: Iterable) → tuple[int]

Decodes assignment.

Parameters:

assign – assignment of external CNF variables

Returns:

assignment of DECODATABLE internal CNF variables.

Return type:

tuple

get_clause(pos: int) → tuple[int]

Gets clause of given position.

Parameters:

pos – position ranging from 0 to the number of clauses minus 1.

get_ncls() → int

Gets the number of clauses in CNF.

get_nvar() → int

Gets the number of variables in CNF.

nvar

maximum variable index

write(stream=None, format: str = 'dimacs') → None

Write CNF in DIMACS CNF format.

Parameters:

• stream – stream (stdout if not specified) to which CNF is written.

• format – file format of cnf

pygplib.ecc module

class pygplib.ecc.Ecc(vertex_list, edge_list)

Bases: object

Class for computing an edge clique cover.

The algorithm for computing an edge clique cover is based on heuristic algorithms by Conte et al. Please see : https://doi.org/10.1016/j.ic.2019.104464

compute_ecc(variant: str = 'rr') → list[list[int]]

Computes an edge clique cover of a given graph.

compute_separating_ecc(variant: str = 'rr') → list[list[int]]

Computes a separating edge clique cover of a given graph.

pygplib.fog module

Class of first-order logic of graphs

class pygplib.fog.Fog(tag: str, left: AbsExpr = None, right: AbsExpr = None, aux: tuple = ())

Bases: AbsFo

Expression of First-order logic of graphs

Node           |  self._aux[0]  | self._aux[1]
---------------|----------------|--------------
True  constant |  -             | -
False constant |  -             | -
Quantifier     | index of       | -
               | bound variable |
Relation       | 1st argument   | 2nd argument

Note

In the current implementation, syntactically identical subexpressions are shared. We have to keep it in mind that this might become source of bugs. For instance, consider (? [x] : x) & x. In this formula, the second occurrence of x is a bound variable, and third occurrence is a free variable. In the current implementation, despite different semantics, these variables are shared, that is, they are represented as a single object in the representation of the formula. We do this for the sake of simplicity, but this might become source of bugs. When we apply some operation to such a formula, we sometimes have to consider difference in semantics.

_EDG

string, representing adjacency relation of vertices.

_EQ

string, representing equality relation of vertices.

_LT

string, representing less-than relation of vertices.

_ATOM_TAGS

tuple of strings, representing types of atom.

_BINOP_TAGS

tuple of strings, representing types of binary operator.

_UNOP_TAGS

tuple of strings, representing types of uniary operator.

_QF_TAGS

tuple of strings, representing types of quantifier.

_EXPR_TAGS

tuple of available tags in this class.

classmethod atom(tag: str, *args) → AbsExpr

Gets the tag-specified atomic formula.

Args: args: tuple of indices of (variable or constant) symbols (or 0 for true or false)

staticmethod cmp_atom_args(x, y) → int

compute_nnf_step(negated: bool, s: list[list], t: list[list]) → None

Performs NNF computation for this object.

classmethod edg(x: int, y: int) → AbsExpr

Gets the atomic formula of the form edg(x,y).

Parameters:

• x – index of (variable or constant) symbol

• y – index of (variable or constant) symbol

classmethod eq(x: int, y: int) → AbsExpr

Gets the atomic formula of the form x=y.

Parameters:

• x – index of (variable or constant) symbol

• y – index of (variable or constant) symbol

get_atom_arg(i: int) → int

Gets the i-th argument of the atomic formula.

Parameters:

i – argument index (1 or 2)

Returns:

term given as argument of the atom.

get_atom_value(i: int) → int

Gets the term, specified by position, of the atomic formula.

Parameters:

i – position of term (1 or 2)

classmethod get_edg_tag() → str

Gets tag of edg.

classmethod get_eq_tag() → str

Gets tag of eq.

get_free_vars_and_consts_pre_step(bound_vars: list, free_vars: list) → None

Performs computation for this object.

classmethod get_lt_tag() → str

Gets tag of lt.

is_edg_atom() → bool

Is it an atom of the form edg(x,y) ?

is_eq_atom() → bool

Is it an atom of the form x=y ?

is_lt_atom() → bool

Is it an atom of the form x<y ?

classmethod lt(x: int, y: int) → AbsExpr

Gets the atomic formula of the form lt(x,y).

Parameters:

• x – index of (variable or constant) symbol

• y – index of (variable or constant) symbol

make_node_str_step() → str

Makes string of this object for DOT print.

make_str_in_step() → str

Makes string in infix order for this object.

make_str_post_step() → str

Makes string in postfix order for this object.

make_str_pre_step() → str

Makes string in prefix order for this object.

perform_boolean_encoding_step(assoc: dict, st: BaseRelSt) → None

Performs Boolean encoding for this object.

classmethod read(formula_str: str) → AbsExpr

Constructs formula from string.

The format of first-order formulas is defined here in Backus–Naur form. The following notation is useful shorthand.

• e1 | e2 | e3 | … means a choice of e1, e2, e3, etc.

• ( e )* means zero or more occurences of e.

• [“a”-“z”] matches any lowercase alphabet letter.

• [“A”-“Z”] matches any uppercase alphabet letter.

• [“0”-“9”] matches any digit from “0” to “9”.

• <word> means a non-terminal symbol.

The name of a variable symbol is defined as follows:

<var_symb>::= <alpha_lower> (<alpha_lower> | <digit> | "_")*
<alpha_lower>::= ["a"-"z"]
<digit>::= ["0"-"9"]

The name of a constant symbol is defined as follows:

<con_symb>::= <alpha_upper> (<alpha_upper> | <digit> | "_")*
<alpha_upper>::= ["A"-"Z"]
<digit>::= ["0"-"9"]

An atomic formula is defined as follows:

<atom>::= <edg_atom> | <eq_atom> | <con_atom> | <lt_atom>
<edg_atom>::= "edg" "(" <term> "," <term> ")"
<eq_atom>::=  <term> "=" <term>
<con_atom>::= "T" | "F"
<lt_atom>::=  <term> "<" <term>
<term>::= <var_symb> | <con_symb>

A formula is defined as follows:

<expr>::= <atom> | "(" <unop> <expr> ")"
                | "(" <expr> <binop> <expr> ")"
                | "(" <qf> "[" <var> "]" ":" <expr> ")"
<unop>::= "~"
<binop>::= "&" | "|" | "->" | "<->"
<qf>::= "!" | "?"

Parenthesis can be omitted as long as the interpretation is uniquely determined. Here, the precedence of logical operators is determined as follows:

"!"="?" > "~" > "&" > "|" > "->" > "<->"

Operators of the same precedence are associated in such a way that binary operations are left-associative, unary operation and quantifiers are right-associative.

Note

~ ! [x] : T means ~ (! [x] : T), but ! [x] : ~ T cannot be parsed because the parser attempts to interprete it as (! [x] : ~) T due to precedence, unless I misunderstand.

Parameters:

formula_str – string representation of formula

reduce_formula_step(assoc: dict, st: BaseRelSt) → None

Performs reduce computation for this object.

substitute_step(y: int, x: int, assoc: dict) → None

Performs substitution for this object.

pygplib.grst module

Graph relational structure class

class pygplib.grst.GrSt(vertex_list: list, edge_list: list, encoding: str = 'edge', prefix: str = 'V', ecc=None, msg: str = '')

Bases: SymRelSt

Manages graph structure for interpreting formulas (and index-mapping).

_EDGE_ENC

edge-encoding

_CLIQUE_ENC

clique-encoding

_DIRECT_ENC

direct-encoding

_LOG_ENC

log-encoding

_ENCODING

tuple of available encodings

Example of Usage is as follows.

W1---W2
|   /
|  /
| /
W3---W5

import pygplib import GrSt, Fog, NameMgr
vertex_list = [3,1,2,5]
edge_list   = [(2,1),(1,3),(3,2),(3,5)]
st = GrSt(vertex_list, edge_list, prefix = "W")
i = st.vertex_to_object(vertex_list[0])
assert NameMgr.lookup_name(i) == f"W{vertex_list[0]}"

adjacent(x: int, y: int) → bool

Determines if constants (meaning vertices) are adjacent.

Parameters:

• x – constant symbol index (meaning vertex)

• y – constant symbol index (meaning vertex)

Returns:

True if adjacent, and False otherwise.

be_F() → Prop

Encodes false constant object of Fog class to Prop object.

be_T() → Prop

Encodes true constant object of Fog class to Prop object.

be_edg(x: int, y: int) → Prop

Encodes predicate of adjacency relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

be_eq(x: int, y: int) → Prop

Encodes predicate of equality relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

be_lt(x: int, y: int) → Prop

Encodes predicate of less-than relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

compute_auxiliary_constraint(f: Fog) → Prop

Auxiliary constraint encoder

Parameters:

f – a first-order formula object of Fog class

Returns:

formula object of Prop class

compute_domain_constraint(x: int) → Prop

Domain constraint encoder

Parameters:

x – index of a first-order variable symbol

Returns:

formula object of Prop class

encode_F() → Prop

Encodes false constant object of Fog class to Prop object.

encode_T() → Prop

Encodes true constant object of Fog class to Prop object.

encode_edg(x: int, y: int) → Prop

Encodes predicate of adjacency relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

encode_eq(x: int, y: int) → Prop

Encodes predicate of equality relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

equal(x: int, y: int) → bool

Determines if constants (meaning vertices) are equal with each other.

Parameters:

• x – constant symbol index (meaning vertex)

• y – constant symbol index (meaning vertex)

Returns:

True if equal, and False otherwise.

lt(x: int, y: int) → bool

Determines if x is less than y in an internal order of vertices.

Parameters:

• x – constant symbol index (meaning vertex)

• y – constant symbol index (meaning vertex)

Returns:

True if x is less than y, and False otherwise.

object_to_vertex(obj: int) → int

Converts object (constant symbol index) to vertex.

Parameters:

obj – domain object (constant symbol index)

Returns:

index of vertex.

sorted(li: list) → None

Sorts list of constants (i.e. vertices) in an increasing order.

Parameters:

li – list of constant indices

Returns:

Sorted list

vertex_to_object(x: int) → int

vertex_to_object(x: tuple) → tuple

Converts vertex to object (constant symbol index).

Alias of vertex_to_object_int() and vertex_to_object_tuple()

vertex_to_object_int(vertex: int) → int

Converts vertex to object (constant symbol index).

Parameters:

vertex – a domain object (a constant symbol index)

Returns:

a domain object (a constant symbol index)

vertex_to_object_tuple(tup: tuple[int]) → tuple[int]

Converts vertex to object (constant symbol index).

Parameters:

tup – tuple of (tuples of) vertices

Returns:

tuple of (tuples of) domain objects (constant symbol indices)

pygplib.name module

Name manager class

class pygplib.name.NameMgr

Bases: object

Manages names of individual variables and constant symbols.

The name of a variable symbol must begin with a lowercase letter, while the name of a constant symbol must begin with a uppercase letter.

The name manager also manages names of propositional variables.

Note

Names are added as soon as formulas are parsed, propositional variables are produced by perform_boolean_encoding(). Also names can be added manually through lookup_index(), but in such a case, it is not checked whether it has a correct format. Actually, the name manager examines only the leading character, and it does not care of the second and later characters. See fo.py for the format of first-order formulas, and prop.py for that of propositional formulas.

_dict

dict to find index from name.

_inv_list

list to find name from index.

classmethod clear() → None

Clears all names added so far.

classmethod get_aux_index() → int

Gets the index of a new auxiliary variable to introduce.

The leading character of variable name is “_” to avoid collision.

classmethod has_index(name: str) → bool

Does the name have index ?

Parameters:

name – arbitrary string

classmethod has_name(index: int) → bool

Does the index have name ?

Parameters:

index – arbitrary integer

classmethod is_constant(index: int) → bool

Is it a name for some constant ?

Raises:

ValueError – if the index does not have any name.

Parameters:

index – index of (variable or constant) symbol

classmethod is_variable(index: int) → bool

Is it a name for some variable ?

Raises:

ValueError – if the index does not have any name.

Parameters:

index – index of (variable or constant) symbol

classmethod lookup_index(name: str) → int

Look-up index from name.

Note

If not exists, a new index will be assigned. The method fails if names of auxiliary variables introduced by get_aux_index are given. If the leading character is “_” and the name is already registered, then this means that it is the index of an auxiliary variable.

Parameters:

name – name of (variable or constant) symbol

Raises:

ValueError – if the leading character is not alphabetic.

classmethod lookup_name(index: int) → str

Look-up name from index.

Raises:

IndexError – if not exists.

Parameters:

index – index of (variable or constant) symbol

pygplib.op module

Operations for traversing, manipulating, and converting formulas

pygplib.op.compute_cnf(data: Props) → tuple[int, int, tuple[tuple[int, ...], ...]]

Computes Conjunction Normal Form for Props using Tsentin transformation.

Iterable[Prop] is considered as the conjunction of all Prop formulas. The transformation is done so as to retain one-to-one correspondence betweeen satisfying assignments of the original formula and those of CNF.

Note

Variable indices of CNF are divided into twos: Those less than or equal to the maximum index of variables occuring in input formula represent variables occurring in input formula. The other indices represent auxiliary variables introduced in encoding. There might be missing indices in CNF because not all indices consecutively starting from 1 occur in input formula.

Returns:

a tuple containing, respectively,

• the maximum index of variables occurring in input formula,

• the number of auxiliary variables introduced during CNF-encoding,

• a tuple of clauses, each clause is a tuple of variable indices.

Return type:

(int,int,tuple)

pygplib.op.compute_nnf(f: AbsExpr) → AbsExpr

Computes negation normal form (NNF).

The iff and implies operators, if any, will be excluded in the output formula.

Parameters:

f – formula to be converted.

pygplib.op.compute_size(f: AbsExpr) → int

Computes the total number of operators and atoms.

pygplib.op.eliminate_qf(expr: AbsFo, st: BaseRelSt) → AbsFo

Performs quantifier elimination.

Parameters:

expr – formula to which elimination is performed.

Note

The behaviour of this method changes depending on structures.

Raises:

Exception – if no relational structure is set (i.e. None).

for ... in pygplib.op.generate_subformulas(f: AbsExpr, skip_shared: bool = False)

Yeilds all subformulas with left subformula first.

It generates all occurrences of syntactically identical subformulas by default. If skip_shared is set True, it generate all different subformulas.

Note

This method is not supposed to be given formulas including quantifiers. Theoretically speaking, generating all subformulas of a quantified formula (say ?[x]: f) means generating not only subformulas of f (and ?[x]: f itself) but also those of f[t/x] for any term t free for x in f. This method generates subformulas of the former case but it does not generate those of the latter case. If you really want to give quantified formulas, we recommend not to set skip_shared True. To see this, let us consider what happens when (? [x] : x) & x is given and skip_shared is mistakenly set True. Since the second and the third occurrences of x are shared in the graphical representation of this formula, the third occurence of x is skipped. However, there are situations in which the third one should be treated separately from the second one. For instance, let us consider computing all free variables from the above formula. If the third occurrence of x is skipped, no free variable will be mistakenly output.

Parameters:

• f – formula to be traversed

• skip_shared – indicates whether shared formulas are skipped.

Yields:

(i, subexpr) – when subexpr appears in prefix order (for i=0), in infix order (for i=1), and in postfix order (for i=2).

pygplib.op.generator(f: AbsExpr, skip_shared: bool = False)

Yeilds all subformulas with left subformula first.

If skip_shared is set True, shared subformulas are skipped, that is, if there are multiple occurrences of a synactically identical subformula, the second or later occurences of each such subformula are ignored.

Note

It would be safe to call with skip_shared False for first-order formulas. Consider, for instance, (? [x] : x) & x. Since the second and the third occurrences of x are shared, the third occurence of x is skipped if skip_shared is enabled. However, there are cases for which the third one should be treated separately from the second one. For instance, consider computing all free variables from the above formula. If the third occurrence of x is skipped, no free variable will be mistakenly output.

Parameters:

• f – formula to be traversed

• skip_shared – indicates whether shared formulas are skipped.

Yields:

(i, subexpr) – when subexpr appears in prefix order (for i=0), in infix order (for i=1), and in postfix order (for i=2).

pygplib.op.get_free_vars(expr: AbsFo) → tuple

Gets all free variables from the formula.

pygplib.op.get_free_vars_and_consts(expr: AbsFo) → tuple

Gets all free variables and constant symbols.

pygplib.op.get_prop_vars(f: Prop) → tuple

Gets all variables from Prop formula.

pygplib.op.perform_boolean_encoding(f: AbsFo, st: BaseRelSt) → Prop

Converts a first-order formula into an equiv. propositional formula.

Parameters:

f – first-order formula

Returns:

propositional formula

Return type:

Prop

Note

The behaviour of this method changes depending on structures.

Raises:

Exception – if no relational structure is set (i.e. None).

pygplib.op.print_formula(f: AbsExpr, stream=None, graph_name='output', fmt='str') → None

Prints formula to stream (stdout if not given).

Parameters:

• f – formula

• stream – stream (stdout if None)

• graph_name – name of graph in DOT format

• format – human-readble format “str” or DOT format “dot”

pygplib.op.propnize(f: AbsFo, st: BaseRelSt) → Prop

Converts a first-order formula into an equiv. propositional formula.

Parameters:

f – first-order formula

Returns:

propositional formula

Return type:

Prop

Note

The behaviour of this method changes depending on structures.

Raises:

Exception – if no relational structure is set (i.e. None).

pygplib.op.reduce(f: AbsExpr, st: BaseRelSt = None) → AbsExpr

Reduces it into as simple formula as possible, retaining equivalence.

Quantifiers are not eliminated except for constant operands. Relational structure is not mandatory. If relational structure is set, it reduces constant symbols as much as possible.

Parameters:

f – formula to be reduced

Note

The behaviour of this method changes depending on structures.

pygplib.op.reduce_formula(f: AbsExpr, st: BaseRelSt = None) → AbsExpr

Reduces it into as simple formula as possible, retaining equivalence.

Quantifiers are not eliminated except for constant operands. Relational structure is not mandatory. If relational structure is set, it reduces constant symbols as much as possible.

Parameters:

f – formula to be reduced

Note

The behaviour of this method changes depending on structures.

pygplib.op.substitute(expr: AbsFo, y: int, x: int) → AbsFo

Substitutes y for all free occurences of x.

Parameters:

• expr – formula

• y – index of (variable or constant) symbol

• x – index of (variable or constant) symbol

pygplib.op.to_str(f: AbsExpr) → str

Converts formula into string.

The same formula can be constructed, by read(), from the string produced by this method.

pygplib.prop module

Class of propositional logic

class pygplib.prop.Prop(tag: str, left: AbsExpr = None, right: AbsExpr = None, aux: tuple = ())

Bases: AbsProp

Expression of Propositional Logic

Node             |  self._aux[0]  | self._aux[1]
-----------------|----------------|--------------
True  constant   |  -             | -
False constant   |  -             | -
Boolean Variable | variable index | -

_VAR

string, representing Boolean variable.

_ATOM_TAGS

tuple of strings, representing types of atom.

_BINOP_TAGS

tuple of strings, representing types of binary operator.

_UNOP_TAGS

tuple of strings, representing types of uniary operator.

_EXPR_TAGS

tuple of available tags in this class.

compute_cnf_step(igen: IndexGen, assoc: dict, cnf: list) → None

Peforms CNF computation for this object.

compute_nnf_step(negated: bool, s: list[list], t: list[list]) → None

Performs NNF computation for this object.

get_atom_value(i: int) → int

Gets the index of the Boolean variable.

get_var_index()

Gets the index of the Boolean variable.

classmethod get_var_tag()

Gets tag of var.

is_var_atom()

Is the formula a Boolean variable ?

make_node_str_step() → str

Makes string of this object for DOT print.

make_str_in_step() → str

Makes string in infix order for this object.

make_str_post_step() → str

Makes string in postfix order for this object.

make_str_pre_step() → str

Makes string in prefix order for this object.

classmethod read(formula_str: str) → AbsExpr

Constructs formula from string.

The format of propositional formulas is defined here in Backus–Naur form. The following notation is useful shorthand.

• e1 | e2 | e3 | … means a choice of e1, e2, e3, etc.

• ( e )* means zero or more occurences of e.

• ( e )+ means one or more occurences of e.

• [“a”-“z”] matches any lowercase alphabet letter.

• [“A”-“Z”] matches any uppercase alphabet letter.

• [“0”-“9”] matches any digit from “0” to “9”.

• <word> means a non-terminal symbol.

The name of a variable symbol is defined as follows:

<var_symb>::= <alpha_lower> (<alpha_lower> | <digit> | "_")*
<alpha_lower>::= ["a"-"z"]
<digit>::= ["0"-"9"]
<decimal_literal>::= ["1"-"9"](["0"-"9"])*

A formula is defined as follows:

<expr>::= <var_symb> | "T" | "F" | "(" <unop> <expr> ")" |             "(" <expr> <binop> <exr> ")"
<unop>::= "~"
<binop>::= "&" | "|" | "->" | "<->"

Parenthesis can be omitted as long as the interpretation is uniquely determined. Here, the precedence of logical operators is determined as follows:

"~" > "&" > "|" > "->" > "<->"

Operators of the same precedence are associated in such a way that binary operations are left-associative, unary operation is right-associative.

reduce_formula_step(assoc: dict, st: BaseRelSt) → None

Performs reduce computation for this object.

classmethod var(index: int)

Gets the formula of the index-speficied Boolean variable.

pygplib.symrelst module

Class of Symmetric Relational Structure over a single domain of discourse

class pygplib.symrelst.SymRelSt(objects: tuple[int], relation: tuple[tuple[int]], msg: str = '')

Bases: BaseRelSt

Class of symmetric relational structure.

All relations are considered to be symmetric. Variables run over a single domain of discourse. There is no function symbol.

Module contents

class pygplib.BaseRelSt(objects: tuple[int], codes: tuple[tuple[int]], length: int, msg: str = '')

Bases: Be

Base class of relational structure.

This class assumes the followings: There is no function symbol. A first-order variable runs over a single domain of discourse. A first-order variable is encoded with a sequence of Boolean variables of fixed-length. Each object in domain has unique code, represented by a tuple of integers.

decode_assignment(assign: tuple[int]) → dict[int, int]

Decodes truth assignment of Boolean variables.

Parameters:

assign – truth assignment of Boolean variables

Returns:

assignment of first-order variables to objects

Return type:

dict

Note

element index ranges from 0 to number of codes minus 1

domain

tuple of objects (constant symbol indices)

get_code(obj: int) → tuple

Returns the code of an object (a constant symbol index).

Parameters:

obj – constant symbol index

class pygplib.Cnf(li: Iterable, st: BaseRelSt = None, check_cnf: bool = False)

Bases: object

CNF Converter Class

base

number of decodable variables

cnf

CNF, where variables are renumbered so that all indices from 1 to nvar appear at least once and all indices from 1 to base are decodable.

decode_assignment(assign: Iterable) → tuple[int]

Decodes assignment.

Parameters:

assign – assignment of external CNF variables

Returns:

assignment of DECODATABLE internal CNF variables.

Return type:

tuple

get_clause(pos: int) → tuple[int]

Gets clause of given position.

Parameters:

pos – position ranging from 0 to the number of clauses minus 1.

get_ncls() → int

Gets the number of clauses in CNF.

get_nvar() → int

Gets the number of variables in CNF.

nvar

maximum variable index

write(stream=None, format: str = 'dimacs') → None

Write CNF in DIMACS CNF format.

Parameters:

• stream – stream (stdout if not specified) to which CNF is written.

• format – file format of cnf

class pygplib.Fog(tag: str, left: AbsExpr = None, right: AbsExpr = None, aux: tuple = ())

Bases: AbsFo

Expression of First-order logic of graphs

Node           |  self._aux[0]  | self._aux[1]
---------------|----------------|--------------
True  constant |  -             | -
False constant |  -             | -
Quantifier     | index of       | -
               | bound variable |
Relation       | 1st argument   | 2nd argument

Note

In the current implementation, syntactically identical subexpressions are shared. We have to keep it in mind that this might become source of bugs. For instance, consider (? [x] : x) & x. In this formula, the second occurrence of x is a bound variable, and third occurrence is a free variable. In the current implementation, despite different semantics, these variables are shared, that is, they are represented as a single object in the representation of the formula. We do this for the sake of simplicity, but this might become source of bugs. When we apply some operation to such a formula, we sometimes have to consider difference in semantics.

_EDG

string, representing adjacency relation of vertices.

_EQ

string, representing equality relation of vertices.

_LT

string, representing less-than relation of vertices.

_ATOM_TAGS

tuple of strings, representing types of atom.

_BINOP_TAGS

tuple of strings, representing types of binary operator.

_UNOP_TAGS

tuple of strings, representing types of uniary operator.

_QF_TAGS

tuple of strings, representing types of quantifier.

_EXPR_TAGS

tuple of available tags in this class.

classmethod atom(tag: str, *args) → AbsExpr

Gets the tag-specified atomic formula.

Args: args: tuple of indices of (variable or constant) symbols (or 0 for true or false)

staticmethod cmp_atom_args(x, y) → int

compute_nnf_step(negated: bool, s: list[list], t: list[list]) → None

Performs NNF computation for this object.

classmethod edg(x: int, y: int) → AbsExpr

Gets the atomic formula of the form edg(x,y).

Parameters:

• x – index of (variable or constant) symbol

• y – index of (variable or constant) symbol

classmethod eq(x: int, y: int) → AbsExpr

Gets the atomic formula of the form x=y.

Parameters:

• x – index of (variable or constant) symbol

• y – index of (variable or constant) symbol

get_atom_arg(i: int) → int

Gets the i-th argument of the atomic formula.

Parameters:

i – argument index (1 or 2)

Returns:

term given as argument of the atom.

get_atom_value(i: int) → int

Gets the term, specified by position, of the atomic formula.

Parameters:

i – position of term (1 or 2)

classmethod get_edg_tag() → str

Gets tag of edg.

classmethod get_eq_tag() → str

Gets tag of eq.

get_free_vars_and_consts_pre_step(bound_vars: list, free_vars: list) → None

Performs computation for this object.

classmethod get_lt_tag() → str

Gets tag of lt.

is_edg_atom() → bool

Is it an atom of the form edg(x,y) ?

is_eq_atom() → bool

Is it an atom of the form x=y ?

is_lt_atom() → bool

Is it an atom of the form x<y ?

classmethod lt(x: int, y: int) → AbsExpr

Gets the atomic formula of the form lt(x,y).

Parameters:

• x – index of (variable or constant) symbol

• y – index of (variable or constant) symbol

make_node_str_step() → str

Makes string of this object for DOT print.

make_str_in_step() → str

Makes string in infix order for this object.

make_str_post_step() → str

Makes string in postfix order for this object.

make_str_pre_step() → str

Makes string in prefix order for this object.

perform_boolean_encoding_step(assoc: dict, st: BaseRelSt) → None

Performs Boolean encoding for this object.

classmethod read(formula_str: str) → AbsExpr

Constructs formula from string.

The format of first-order formulas is defined here in Backus–Naur form. The following notation is useful shorthand.

• e1 | e2 | e3 | … means a choice of e1, e2, e3, etc.

• ( e )* means zero or more occurences of e.

• [“a”-“z”] matches any lowercase alphabet letter.

• [“A”-“Z”] matches any uppercase alphabet letter.

• [“0”-“9”] matches any digit from “0” to “9”.

• <word> means a non-terminal symbol.

The name of a variable symbol is defined as follows:

<var_symb>::= <alpha_lower> (<alpha_lower> | <digit> | "_")*
<alpha_lower>::= ["a"-"z"]
<digit>::= ["0"-"9"]

The name of a constant symbol is defined as follows:

<con_symb>::= <alpha_upper> (<alpha_upper> | <digit> | "_")*
<alpha_upper>::= ["A"-"Z"]
<digit>::= ["0"-"9"]

An atomic formula is defined as follows:

<atom>::= <edg_atom> | <eq_atom> | <con_atom> | <lt_atom>
<edg_atom>::= "edg" "(" <term> "," <term> ")"
<eq_atom>::=  <term> "=" <term>
<con_atom>::= "T" | "F"
<lt_atom>::=  <term> "<" <term>
<term>::= <var_symb> | <con_symb>

A formula is defined as follows:

<expr>::= <atom> | "(" <unop> <expr> ")"
                | "(" <expr> <binop> <expr> ")"
                | "(" <qf> "[" <var> "]" ":" <expr> ")"
<unop>::= "~"
<binop>::= "&" | "|" | "->" | "<->"
<qf>::= "!" | "?"

Parenthesis can be omitted as long as the interpretation is uniquely determined. Here, the precedence of logical operators is determined as follows:

"!"="?" > "~" > "&" > "|" > "->" > "<->"

Operators of the same precedence are associated in such a way that binary operations are left-associative, unary operation and quantifiers are right-associative.

Note

~ ! [x] : T means ~ (! [x] : T), but ! [x] : ~ T cannot be parsed because the parser attempts to interprete it as (! [x] : ~) T due to precedence, unless I misunderstand.

Parameters:

formula_str – string representation of formula

reduce_formula_step(assoc: dict, st: BaseRelSt) → None

Performs reduce computation for this object.

substitute_step(y: int, x: int, assoc: dict) → None

Performs substitution for this object.

class pygplib.GrSt(vertex_list: list, edge_list: list, encoding: str = 'edge', prefix: str = 'V', ecc=None, msg: str = '')

Bases: SymRelSt

Manages graph structure for interpreting formulas (and index-mapping).

_EDGE_ENC

edge-encoding

_CLIQUE_ENC

clique-encoding

_DIRECT_ENC

direct-encoding

_LOG_ENC

log-encoding

_ENCODING

tuple of available encodings

Example of Usage is as follows.

W1---W2
|   /
|  /
| /
W3---W5

import pygplib import GrSt, Fog, NameMgr
vertex_list = [3,1,2,5]
edge_list   = [(2,1),(1,3),(3,2),(3,5)]
st = GrSt(vertex_list, edge_list, prefix = "W")
i = st.vertex_to_object(vertex_list[0])
assert NameMgr.lookup_name(i) == f"W{vertex_list[0]}"

adjacent(x: int, y: int) → bool

Determines if constants (meaning vertices) are adjacent.

Parameters:

• x – constant symbol index (meaning vertex)

• y – constant symbol index (meaning vertex)

Returns:

True if adjacent, and False otherwise.

be_F() → Prop

Encodes false constant object of Fog class to Prop object.

be_T() → Prop

Encodes true constant object of Fog class to Prop object.

be_edg(x: int, y: int) → Prop

Encodes predicate of adjacency relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

be_eq(x: int, y: int) → Prop

Encodes predicate of equality relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

be_lt(x: int, y: int) → Prop

Encodes predicate of less-than relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

compute_auxiliary_constraint(f: Fog) → Prop

Auxiliary constraint encoder

Parameters:

f – a first-order formula object of Fog class

Returns:

formula object of Prop class

compute_domain_constraint(x: int) → Prop

Domain constraint encoder

Parameters:

x – index of a first-order variable symbol

Returns:

formula object of Prop class

encode_F() → Prop

Encodes false constant object of Fog class to Prop object.

encode_T() → Prop

Encodes true constant object of Fog class to Prop object.

encode_edg(x: int, y: int) → Prop

Encodes predicate of adjacency relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

encode_eq(x: int, y: int) → Prop

Encodes predicate of equality relation, given two symbols.

Parameters:

• x – symbol index (constant symbol or variable symbol)

• y – symbol index (constant symbol or variable symbol)

Returns:

formula object of Prop class

equal(x: int, y: int) → bool

Determines if constants (meaning vertices) are equal with each other.

Parameters:

• x – constant symbol index (meaning vertex)

• y – constant symbol index (meaning vertex)

Returns:

True if equal, and False otherwise.

lt(x: int, y: int) → bool

Determines if x is less than y in an internal order of vertices.

Parameters:

• x – constant symbol index (meaning vertex)

• y – constant symbol index (meaning vertex)

Returns:

True if x is less than y, and False otherwise.

object_to_vertex(obj: int) → int

Converts object (constant symbol index) to vertex.

Parameters:

obj – domain object (constant symbol index)

Returns:

index of vertex.

sorted(li: list) → None

Sorts list of constants (i.e. vertices) in an increasing order.

Parameters:

li – list of constant indices

Returns:

Sorted list

vertex_to_object(x: int) → int

vertex_to_object(x: tuple) → tuple

Converts vertex to object (constant symbol index).

Alias of vertex_to_object_int() and vertex_to_object_tuple()

vertex_to_object_int(vertex: int) → int

Converts vertex to object (constant symbol index).

Parameters:

vertex – a domain object (a constant symbol index)

Returns:

a domain object (a constant symbol index)

vertex_to_object_tuple(tup: tuple[int]) → tuple[int]

Converts vertex to object (constant symbol index).

Parameters:

tup – tuple of (tuples of) vertices

Returns:

tuple of (tuples of) domain objects (constant symbol indices)

class pygplib.IndexGen(init_index: int = 1)

Bases: object

Generates indices.

Parameters:

init_index – initial index

_init

initial index

_next

next index

clear(init_index: int = 1) → None

Clears index with init_index.

get_count() → int

Gets the number of indices issued so far.

get_next() → int

Gets the next index.

class pygplib.NameMgr

Bases: object

Manages names of individual variables and constant symbols.

The name of a variable symbol must begin with a lowercase letter, while the name of a constant symbol must begin with a uppercase letter.

The name manager also manages names of propositional variables.

Note

Names are added as soon as formulas are parsed, propositional variables are produced by perform_boolean_encoding(). Also names can be added manually through lookup_index(), but in such a case, it is not checked whether it has a correct format. Actually, the name manager examines only the leading character, and it does not care of the second and later characters. See fo.py for the format of first-order formulas, and prop.py for that of propositional formulas.

_dict

dict to find index from name.

_inv_list

list to find name from index.

classmethod clear() → None

Clears all names added so far.

classmethod get_aux_index() → int

Gets the index of a new auxiliary variable to introduce.

The leading character of variable name is “_” to avoid collision.

classmethod has_index(name: str) → bool

Does the name have index ?

Parameters:

name – arbitrary string

classmethod has_name(index: int) → bool

Does the index have name ?

Parameters:

index – arbitrary integer

classmethod is_constant(index: int) → bool

Is it a name for some constant ?

Raises:

ValueError – if the index does not have any name.

Parameters:

index – index of (variable or constant) symbol

classmethod is_variable(index: int) → bool

Is it a name for some variable ?

Raises:

ValueError – if the index does not have any name.

Parameters:

index – index of (variable or constant) symbol

classmethod lookup_index(name: str) → int

Look-up index from name.

Note

If not exists, a new index will be assigned. The method fails if names of auxiliary variables introduced by get_aux_index are given. If the leading character is “_” and the name is already registered, then this means that it is the index of an auxiliary variable.

Parameters:

name – name of (variable or constant) symbol

Raises:

ValueError – if the leading character is not alphabetic.

classmethod lookup_name(index: int) → str

Look-up name from index.

Raises:

IndexError – if not exists.

Parameters:

index – index of (variable or constant) symbol

class pygplib.Prop(tag: str, left: AbsExpr = None, right: AbsExpr = None, aux: tuple = ())

Bases: AbsProp

Expression of Propositional Logic

Node             |  self._aux[0]  | self._aux[1]
-----------------|----------------|--------------
True  constant   |  -             | -
False constant   |  -             | -
Boolean Variable | variable index | -

_VAR

string, representing Boolean variable.

_ATOM_TAGS

tuple of strings, representing types of atom.

_BINOP_TAGS

tuple of strings, representing types of binary operator.

_UNOP_TAGS

tuple of strings, representing types of uniary operator.

_EXPR_TAGS

tuple of available tags in this class.

compute_cnf_step(igen: IndexGen, assoc: dict, cnf: list) → None

Peforms CNF computation for this object.

compute_nnf_step(negated: bool, s: list[list], t: list[list]) → None

Performs NNF computation for this object.

get_atom_value(i: int) → int

Gets the index of the Boolean variable.

get_var_index()

Gets the index of the Boolean variable.

classmethod get_var_tag()

Gets tag of var.

is_var_atom()

Is the formula a Boolean variable ?

make_node_str_step() → str

Makes string of this object for DOT print.

make_str_in_step() → str

Makes string in infix order for this object.

make_str_post_step() → str

Makes string in postfix order for this object.

make_str_pre_step() → str

Makes string in prefix order for this object.

classmethod read(formula_str: str) → AbsExpr

Constructs formula from string.

The format of propositional formulas is defined here in Backus–Naur form. The following notation is useful shorthand.

• e1 | e2 | e3 | … means a choice of e1, e2, e3, etc.

• ( e )* means zero or more occurences of e.

• ( e )+ means one or more occurences of e.

• [“a”-“z”] matches any lowercase alphabet letter.

• [“A”-“Z”] matches any uppercase alphabet letter.

• [“0”-“9”] matches any digit from “0” to “9”.

• <word> means a non-terminal symbol.

The name of a variable symbol is defined as follows:

<var_symb>::= <alpha_lower> (<alpha_lower> | <digit> | "_")*
<alpha_lower>::= ["a"-"z"]
<digit>::= ["0"-"9"]
<decimal_literal>::= ["1"-"9"](["0"-"9"])*

A formula is defined as follows:

<expr>::= <var_symb> | "T" | "F" | "(" <unop> <expr> ")" |             "(" <expr> <binop> <exr> ")"
<unop>::= "~"
<binop>::= "&" | "|" | "->" | "<->"

Parenthesis can be omitted as long as the interpretation is uniquely determined. Here, the precedence of logical operators is determined as follows:

"~" > "&" > "|" > "->" > "<->"

Operators of the same precedence are associated in such a way that binary operations are left-associative, unary operation is right-associative.

reduce_formula_step(assoc: dict, st: BaseRelSt) → None

Performs reduce computation for this object.

classmethod var(index: int)

Gets the formula of the index-speficied Boolean variable.

class pygplib.SymRelSt(objects: tuple[int], relation: tuple[tuple[int]], msg: str = '')

Bases: BaseRelSt

Class of symmetric relational structure.

All relations are considered to be symmetric. Variables run over a single domain of discourse. There is no function symbol.