Ctrl+K

Run

Run#

Draco can run programs in the Clingo solver. draco.run exposes the low-level functions to run a program in the solver and get back the satisfying models with the answer sets.

Draco uses these methods in the high-level APIs for checking specifications. If you use this API, make sure to read the documentation of the Clingo Python API. It covers how to work with answer sets and symbols.

Available functions#

class draco.run.Model(answer_set, cost, number)#

Class for a model.

Attributes:
answer_set:

The answer set of this model. An answer set is a list of Clingo Symbols.

cost:

The cost of this answer set.

number:

The sequence number of this answer.

class draco.run.Observer#
minimize(priority, literals)#

Observe minimize directives (or weak constraints) passed to the solver.

Parameters#

priority

The priority of the directive.

literals

List of weighted literals whose sum to minimize (pairs of literal and weight).

draco.run.is_satisfiable(program)#

Checks whether the program is satisfiable.

Parameters:

program (Union[str, Iterable[str]]) – Program as a string or iterable of strings that will be concatenated.

Return type:

bool

Returns:

Whether the program is satisfiable.

draco.run.run_clingo(program, models=0, topK=False, arguments=[])#

Run the solver and yield the models.

Parameters:

  • program (Union[str, Iterable[str]]) – Program as a string or iterable of strings that will be concatenated.

  • models (int) – Number of models to generate, defaults to 0 (meaning all models).

  • topK – Whether to return the top K models. If false (default), the program will not optimize the output models.

  • arguments (list[str]) – Arguments to the clingo grounder and solver. Only gringo options (without –text) and clasp’s search options are supported. For example, you can use [“-c foo=5”] to override the occurrences of constant “foo” in your input program. Refer to the potassco guide for the options.

Yield:

The models.

Return type:

Generator[Model, None, None]

Usage Example#

from draco import run_clingo

for model in run_clingo("a. b :- a."):
    print(model)

    print(model.answer_set[0])
    print(model.answer_set[1])

a.
b.
a
b
Contents