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 printsat
if theory namedT
has a model expanding structure namedS
.- Parameters
theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.
- Returns
sat
,unsat
orunknown
- Return type
str
-
model_expand
(*theories, max=10, timeout=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 namedT
expanding structure namedS
.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 argument to see them.
More models may be available. Change the max and timeout 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 (int, optional) – timeout in 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)[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 namedS
consistent with the theory namedT
.- 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.
- Yields
str
- Return type
Iterator[str]
-
decision_table
(*theories, goal_string='', timeout=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 (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)[source] Execute the
main()
procedure block in the IDP program- Parameters
self (idp_engine.Parse.IDP) –
- Return type
None