idp_engine.Run

The following Python functions can be used to perform computations using FO-dot knowledge bases:

model_check(*theories)[source]

Returns a string stating whether the combination of theories is satisfiable.

For example, print(model_check(T, S)) will print sat if theory named T has a model expanding structure named S.

Parameters

theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.

Returns

sat, unsat or unknown

Return type

str

model_expand(*theories, max=10, timeout_seconds=10, complete=False, extended=False, sort=False)[source]

Returns a (possibly empty) list of models of the combination of theories, followed by a string message.

For example, print(model_expand(T, S)) will return (up to) 10 string representations of models of theory named T expanding structure named S.

The string message can be one of the following:

  • No models.

  • More models may be available.  Change the max argument to see them.

  • More models may be available.  Change the timeout_seconds argument to see them.

  • More models may be available.  Change the max and timeout_seconds arguments to see them.

Parameters

  • theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.

  • max (int, optional) – max number of models. Defaults to 10.

  • timeout_seconds (int, optional) – timeout_seconds seconds. Defaults to 10.

  • complete (bool, optional) – True to obtain complete structures. Defaults to False.

  • extended (bool, optional) – use True when the truth value of inequalities and quantified formula is of interest (e.g. for the Interactive Consultant). Defaults to False.

  • sort (bool, optional) – True if the models should be in alphabetical order. Defaults to False.

Yields

str

Return type

Iterator[str]

model_propagate(*theories, sort=False, complete=False)[source]

Returns a list of assignments that are true in any model of the combination of theories.

Terms and symbols starting with ‘_’ are ignored.

For example, print(model_propagate(T, S)) will return the assignments that are true in any expansion of the structure named S consistent with the theory named T.

Parameters

  • theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.

  • sort (bool, optional) – True if the assignments should be in alphabetical order. Defaults to False.

  • complete (bool, optional) – True when requiring a propagation including negated function value assignments. Defaults to False.

Yields

str

Return type

Iterator[str]

maximize(*theories, term)[source]

Returns a model that maximizes term.

Parameters

  • theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.

  • term (str) – a string representing a term

Yields

str

Return type

idp_engine.Theory.Theory

minimize(*theories, term)[source]

Returns a model that minimizes term.

Parameters

  • theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.

  • term (str) – a string representing a term

Yields

str

Return type

idp_engine.Theory.Theory

decision_table(*theories, goal_string='', timeout_seconds=20, max_rows=50, first_hit=True, verify=False)[source]

Experimental. Returns a decision table for goal_string, given the combination of theories.

Parameters

  • theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.

  • goal_string (str, optional) – the last column of the table. Must be a predicate application defined in the theory, e.g. eligible().

  • timeout_seconds (int, optional) – maximum duration in seconds. Defaults to 20.

  • max_rows (int, optional) – maximum number of rows. Defaults to 50.

  • first_hit (bool, optional) – requested hit-policy. Defaults to True.

  • verify (bool, optional) – request verification of table completeness. Defaults to False

Yields

a textual representation of each rule

Return type

Iterator[str]

determine_relevance(*theories)[source]

Generates a list of questions that are relevant, or that can appear in a justification of a goal_symbol.

The questions are preceded with `` ? `` when their answer is unknown.

When an irrelevant value is changed in a model M of the theories, the resulting M’ structure is still a model. Relevant questions are those that are not irrelevant.

If goal_symbol has an enumeration in the theory (e.g., goal_symbol := {`tax_amount}.), relevance is computed relative to those goals.

Definitions in the theory are ignored, unless they influence axioms in the theory or goals in goal_symbol.

Yields

relevant questions

Parameters

theories (Union[idp_engine.Parse.TheoryBlock, idp_engine.Parse.Structure, idp_engine.Theory.Theory]) –

Return type

Iterator[str]

pretty_print(x='')[source]

Prints its argument on stdout, in a readable form.

Parameters

x (Any, optional) – the result of an API call. Defaults to “”.

Return type

None

duration(msg='')[source]

Returns the processing time since the last call to duration(), or since the begining of execution

Parameters

msg (str) –

Return type

str

execute(self, capture_print=False)[source]

Execute the main() procedure block in the IDP program

Parameters
Return type

Optional[str]