idp_solver.Run

Classes to execute the main block of an IDP program

idp_solver.Run.model_check(theories, structures=None)[source]

output: “sat”, “unsat” or “unknown”

idp_solver.Run.model_expand(theories, structures=None, max=10, complete=False, extended=False)[source]

output: a list of Assignments, ending with a string

idp_solver.Run.model_propagate(theories, structures=None)[source]

output: a list of Assignment

idp_solver.Run.decision_table(theories, structures=None, goal_string='', timeout=20, max_rows=50, first_hit=True, verify=False)[source]

returns a decision table for goal_string, given theories and structures.

Parameters
  • goal_string (str, optional) – the last column of the table.

  • 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

str – a textual representation of each rule

idp_solver.Run.execute(self)[source]

Execute the IDP program