| | |
- object
-
- ConfigProxy
- Control
- Domain
- DomainElement
- DomainIter
- Fun
- InfType
- Model
- SolveControl
- SolveFuture
- SolveIter
- SolveResult
- SupType
class ConfigProxy(object) |
| |
Proxy object that allows for changing the configuration of the
underlying solver.
Options are organized hierarchically. To change and inspect an option use:
proxy.group.subgroup.option = "value"
value = proxy.group.subgroup.option
There are also arrays of option groups that can be accessed using integer
indices:
proxy.group.subgroup[0].option = "value1"
proxy.group.subgroup[1].option = "value2"
To list the subgroups of an option group, use the keys() method. Array option
groups, like solver, have have a non-negative length and can be iterated.
Furthermore, there are meta options having key "configuration". Assigning a
meta option sets a number of related options. To get further information about
an option or option group <opt>, use property __desc_<opt> to retrieve a
description.
Example:
#script (python)
import gringo
def main(prg):
prg.conf.solve.models = 0
prg.ground([("base", [])])
prg.solve()
#end.
{a; c}.
Expected Answer Sets:
{ {}, {a}, {c}, {a,c} }
|
| |
Methods defined here:
- __delattr__(...)
- x.__delattr__('name') <==> del x.name
- __getattribute__(...)
- x.__getattribute__('name') <==> x.name
- __getitem__(...)
- x.__getitem__(y) <==> x[y]
- __len__(...)
- x.__len__() <==> len(x)
- __setattr__(...)
- x.__setattr__('name', value) <==> x.name = value
- keys(...)
- keys(self) -> [string]
Returns the list of sub-option groups or options of this proxy. Returns None if
the proxy is not an option group.
|
class Control(object) |
| |
Control(args) -> Control object
Control object for the grounding/solving process.
Arguments:
args -- optional arguments to the grounder and solver (default: []).
Note that only gringo options (without --text) and clasp's search options are
supported. Furthermore, a Control object is blocked while a search call is
active; you must not call any member function during search.
|
| |
Methods defined here:
- __init__(...)
- x.__init__(...) initializes x; see help(type(x)) for signature
- add(...)
- add(self, name, params, program) -> None
Extend the logic program with the given non-ground logic program in string form.
Arguments:
name -- name of program block to add
params -- parameters of program block
program -- non-ground program as string
Example:
#script (python)
import gringo
def main(prg):
prg.add("p", ["t"], "q(t).")
prg.ground([("p", [2])])
prg.solve()
#end.
Expected Answer Set:
q(2)
- assign_external(...)
- assign_external(self, external, truth) -> None
Assign a truth value to an external atom (represented as a term). It is
possible to assign a Boolean or None. A Boolean fixes the external to the
respective truth value; and None leaves its truth value open.
The truth value of an external atom can be changed before each solve call. An
atom is treated as external if it has been declared using an #external
directive, and has not been forgotten by calling Control.release_external or
defined in a logic program with some rule. If the given atom is not external,
then the function has no effect.
Arguments:
external -- term representing the external atom
truth -- Boolean or None indicating the truth value
See Control.release_external for an example.
- cleanup_domains(...)
- cleanup_domains(self) -> None
This functions cleans up the domains used for grounding. This is done by first
simplifying the current program representation (falsifying released external
atoms). Afterwards, the top-level implications are used to either remove atoms
from domains or mark them as facts.
Note that any atoms falsified are completely removed from the logic program.
Hence, a definition for such an atom in a successive step introduces a fresh atom.
- get_const(...)
- get_const(self, name) -> Fun, integer, string, or tuple object
Returns the term for a constant definition of form: #const name = term.
- ground(...)
- ground(self, parts, context) -> None
Grounds the given list programs specified by tuples of names and arguments.
Keyword Arguments:
parts -- list of tuples of program names and program arguments to ground
context -- an context object whose methods are called during grounding using
the @-syntax (if ommitted methods from the main module are used)
Note that parts of a logic program without an explicit #program specification
are by default put into a program called base without arguments.
Example:
#script (python)
import gringo
def main(prg):
parts = []
parts.append(("p", [1]))
parts.append(("p", [2]))
prg.ground(parts)
prg.solve()
#end.
#program p(t).
q(t).
Expected Answer Set:
q(1) q(2)
- load(...)
- load(self, path) -> None
Extend the logic program with a (non-ground) logic program in a file.
Arguments:
path -- path to program
- release_external(...)
- release_external(self, term) -> None
Release an external represented by the given term.
This function causes the corresponding atom to become permanently false if
there is no definition for the atom in the program. In all other cases this
function has no effect.
Example:
#script (python)
from gringo import Fun
def main(prg):
prg.ground([("base", [])])
prg.assign_external(Fun("b"), True)
prg.solve()
prg.release_external(Fun("b"))
prg.solve()
#end.
a.
#external b.
Expected Answer Sets:
a b
a
- solve(...)
- solve(self, assumptions, on_model) -> SolveResult
Starts a search process and returns a SolveResult.
Keyword Arguments:
assumptions -- a list of (atom, boolean) tuples that serve as assumptions for
the solve call, e.g. - solving under assumptions [(Fun("a"),
True)] only admits answer sets that contain atom a
on_model -- optional callback for intercepting models
a Model object is passed to the callback
Note that in gringo or in clingo with lparse or text output enabled this
functions just grounds and returns SolveResult.UNKNOWN. Furthermore, you might
want to start clingo using the --outf=3 option to disable all output from
clingo.
This function releases the GIL but it is not thread-safe.
Take a look at Control.solve_async for an example on how to use the model
callback.
- solve_async(...)
- solve_async(self, assumptions, on_model, on_finish) -> SolveFuture
Start a search process in the background and return a SolveFuture object.
Keyword Arguments:
assumptions -- a list of (atom, boolean) tuples that serve as assumptions for
the solve call, e.g. - solving under assumptions [(Fun("a"),
True)] only admits answer sets that contain atom a
on_model -- optional callback for intercepting models
a Model object is passed to the callback
on_finish -- optional callback once search has finished
a SolveResult and a Boolean indicating whether the solve call
has been canceled is passed to the callback
Note that this function is only available in clingo with thread support
enabled. Both the on_model and the on_finish callbacks are called from another
thread. To ensure that the methods can be called, make sure to not use any
functions that block the GIL indefinitely. Furthermore, you might want to start
clingo using the --outf=3 option to disable all output from clingo.
Example:
#script (python)
import gringo
def on_model(model):
print model
def on_finish(res, canceled):
print res, canceled
def main(prg):
prg.ground([("base", [])])
f = prg.solve_async(None, on_model, on_finish)
f.wait()
#end.
q.
Expected Output:
q
SAT False
- solve_iter(...)
- solve_iter(self, assumptions) -> SolveIter
Returns a SolveIter object, which can be used to iterate over models.
Keyword Arguments:
assumptions -- a list of (atom, boolean) tuples that serve as assumptions for
the solve call, e.g. - solving under assumptions [(Fun("a"),
True)] only admits answer sets that contain atom a
Example:
#script (python)
import gringo
def main(prg):
prg.add("p", "{a;b;c}.")
prg.ground([("p", [])])
with prg.solve_iter() as it:
for m in it: print m
#end.
Data descriptors defined here:
- conf
- ConfigProxy to change the configuration.
- domains
- Domain object to inspect the domains.
- stats
- A dictionary containing solve statistics of the last solve call.
Contains the statistics of the last Control.solve, Control.solve_async, or
Control.solve_iter call. The statistics correspond to the --stats output of
clingo. The detail of the statistics depends on what level is requested on the
command line. Furthermore, you might want to start clingo using the --outf=3
option to disable all output from clingo.
Note that this (read-only) property is only available in clingo.
Example:
import json
json.dumps(prg.stats, sort_keys=True, indent=4, separators=(',', ': '))
- use_enum_assumption
- Boolean determining how learnt information from enumeration modes is treated.
If the enumeration assumption is enabled, then all information learnt from
clasp's various enumeration modes is removed after a solve call. This includes
enumeration of cautious or brave consequences, enumeration of answer sets with
or without projection, or finding optimal models; as well as clauses/nogoods
added with Model.add_clause()/Model.add_nogood().
Note that initially the enumeration assumption is enabled.
Data and other attributes defined here:
- __new__ = <built-in method __new__ of type object>
- T.__new__(S, ...) -> a new object with type S, a subtype of T
|
class Domain(object) |
| |
This class provides read-only acces to the domains of the grounder.
Example:
p(1).
{ p(3) }.
#external p(1..3).
q(X) :- p(X).
#script (python)
import gringo
def main(prg):
prg.ground([("base", [])])
print "universe:", len(prg.domains)
for x in prg.domains:
print x.atom, x.is_fact, x.is_external
print "p(2) is in domain:", prg.domains[gringo.Fun("p", [3])] is not None
print "p(4) is in domain:", prg.domains[gringo.Fun("p", [6])] is not None
print "domain of p/1:"
for x in prg.domains.by_signature(("p", 1)):
print x.atom, x.is_fact, x.is_external
print "signatures:", prg.domains.signatures()
#end.
Expected Output:
universe: 6
p(1) True False
p(3) False False
p(2) False True
q(1) True False
q(3) False False
q(2) False False
p(2) is in domain: True
p(4) is in domain: False
domain of p/1:
p(1) True False
p(3) False False
p(2) False True
signatures: [('p', 1), ('q', 1)]
|
| |
Methods defined here:
- __getitem__(...)
- x.__getitem__(y) <==> x[y]
- __iter__(...)
- x.__iter__() <==> iter(x)
- __len__(...)
- x.__len__() <==> len(x)
- by_signature(...)
- by_signature(self, name, arity) -> DomainIter
Returns an iterator over the domain elements with the given signature.
Arguments:
name -- the name of the signature
arity -- the arity of the signature
- signatures(...)
- signatures(self) -> list((str, int))
Returns the list of predicate signatures occurring in the program.
|
class DomainElement(object) |
| |
Captures a domain element and provides properties to inspect its state.
|
| |
Data descriptors defined here:
- atom
- atom -> Fun
Returns the representation of the domain element in form of a term (Fun
object).
- is_external
- is_external -> bool
Returns wheather the domain element is external.
- is_fact
- is_fact -> bool
Returns wheather the domain element is a is_fact.
|
class Fun(object) |
| |
Fun(name, args) -> Fun object
Represents a gringo function term.
This also includes symbolic terms, which have to be created by either omitting
the arguments or passing an empty sequence.
Arguments:
name -- string representing the name of the function symbol
(must follow gringo's identifier syntax)
args -- optional sequence of terms representing the arguments of the function
symbol (Default: [])
Fun objects are ordered like in gringo and their string representation
corresponds to their gringo representation.
|
| |
Methods defined here:
- __eq__(...)
- x.__eq__(y) <==> x==y
- __ge__(...)
- x.__ge__(y) <==> x>=y
- __gt__(...)
- x.__gt__(y) <==> x>y
- __hash__(...)
- x.__hash__() <==> hash(x)
- __init__(...)
- x.__init__(...) initializes x; see help(type(x)) for signature
- __le__(...)
- x.__le__(y) <==> x<=y
- __lt__(...)
- x.__lt__(y) <==> x<y
- __ne__(...)
- x.__ne__(y) <==> x!=y
- __repr__(...)
- x.__repr__() <==> repr(x)
- __str__(...)
- x.__str__() <==> str(x)
- args(...)
- args(self) -> list object
Return the arguments of the Fun object.
- name(...)
- name(self) -> string object
Return the name of the Fun object.
Data and other attributes defined here:
- __new__ = <built-in method __new__ of type object>
- T.__new__(S, ...) -> a new object with type S, a subtype of T
|
class Model(object) |
| |
Provides access to a model during a solve call.
Note that model objects cannot be constructed from python. Instead they are
passed as argument to a model callback (see Control.solve and
Control.solve_async). Furthermore, the lifetime of a model object is limited
to the scope of the callback. They must not be stored for later use in other
places like - e.g., the main function.
|
| |
Methods defined here:
- __repr__(...)
- x.__repr__() <==> repr(x)
- __str__(...)
- x.__str__() <==> str(x)
- atoms(...)
- atoms(self, atomset=SHOWN) -> list of terms
Return the list of atoms, terms, or CSP assignments in the model.
Argument atomset is a bitset to select what kind of atoms or terms are returned:
Model.ATOMS -- selects all atoms in the model (independent of #show statements)
Model.TERMS -- selects all terms displayed with #show statements in the model
Model.SHOWN -- selects all atoms and terms as outputted by clingo's default
output format
Model.CSP -- selects all csp assignments (independent of #show statements)
Model.COMP -- return the complement of the answer set w.r.t. to the Herbrand
base accumulated so far (does not affect csp assignments)
The string representation of a model object is similar to the output of models
by clingo using the default output.
Note that atoms are represented using Fun objects, and that CSP assignments are
represented using function symbols with name "$" where the first argument is
the name of the CSP variable and the second its value.
- contains(...)
- contains(self, a) -> Boolean
Returns true if atom a is contained in the model.
Atom a must be represented using a Fun term.
- optimization(...)
- optimization(self) -> [int]
Returns the list of optimization values of the model. This corresponds to
clasp's optimization output.
Data descriptors defined here:
- context
- SolveControl object that allows for controlling the running search.
Data and other attributes defined here:
- ATOMS = 4
- COMP = 16
- CSP = 1
- SHOWN = 2
- TERMS = 8
|
class SolveControl(object) |
| |
Object that allows for controlling a running search.
Note that SolveControl objects cannot be constructed from python. Instead
they are available as properties of Model objects.
|
| |
Methods defined here:
- add_clause(...)
- add_clause(self, lits) -> None
Adds a clause to the solver during the search.
Arguments:
lits -- A list of literals represented as pairs of atoms and Booleans
representing the clause.
Note that this function can only be called in the model callback (or while
iterating when using a SolveIter).
- add_nogood(...)
- add_nogood(self, lits) -> None
Equivalent to add_clause with the literals inverted.
Arguments:
lits -- A list of pairs of Booleans and atoms representing the nogood.
|
class SolveFuture(object) |
| |
Handle for asynchronous solve calls.
SolveFuture objects cannot be created from python. Instead they are returned by
Control.solve_async, which performs a search in the background. A SolveFuture
object can be used to wait for such a background search or cancel it.
Functions in this object release the GIL. They are not thread-safe though.
See Control.solve_async for an example.
|
| |
Methods defined here:
- cancel(...)
- cancel(self) -> None
Interrupts the running search.
Note that unlike other functions of this class, this function can safely be
called from other threads.
- get(...)
- get(self) -> SolveResult object
Get the result of an solve_async call. If the search is not completed yet, the
function blocks until the result is ready.
- wait(...)
- wait(self, timeout) -> None or Boolean
Wait for solve_async call to finish. If a timeout is given, the function waits
at most timeout seconds and returns a Boolean indicating whether the search has
finished. Otherwise, the function blocks until the search is finished and
returns nothing.
Arguments:
timeout -- optional timeout in seconds
(permits floating point values)
|
class SolveIter(object) |
| |
Object to conveniently iterate over all models.
During solving the GIL is released. The functions in this object are not
thread-safe though.
|
| |
Methods defined here:
- __enter__(...)
- __exit__(self) -> SolveIter
Returns self.
- __exit__(...)
- __exit__(self, type, value, traceback) -> Boolean
Follows python __exit__ conventions. Does not suppress exceptions.
Stops the current search. It is necessary to call this method after each search.
- __iter__(...)
- x.__iter__() <==> iter(x)
- get(...)
- get(self) -> SolveResult
Returns the result of the search. Note that this might start a search for the
next model and then returns a result accordingly. The function might be called
after iteration to check if the search has been canceled.
- next(...)
- x.next() -> the next value, or raise StopIteration
|
|