Clingo Solver Integration
So for we have shown how to define predicates and fact bases, and perform queries over fact bases. However, we have not discussed in detail how these objects are integrated and interact with the Clingo ASP solver.
As detailed in Raw Clingo Symbols, at its most basic level a Clingo
Symbol object can be extracted from a Clorm
Predicate object using the
and conversely a
Symbol object can be passed as the
parameter in the
Symbol objects from
Predicates is sufficient to use
Clorm with the Clingo solver it is still not a particularly clean interface and
can result in unnecessary boilerplate code. To avoid this the
module fully integrates Clorm objects into the Clingo API. It does this by
providing wrapper classes around the key Clingo classes:
Controlis the heart of the interface to the reasoner and determines when and how the reasoner is called. The
Control.solve()function starts the solving process. Depending on the parameters it can operate in different modes; for example it can use a callback that is called with
Modelojects and can also return a
Modelis the class that contains the facts (and other meta-data) associated with an ASP model. This class should not be instantiated explicitly and is instead passed within the
SolveHandleprovides a mechanism to iterate over the models. Similarly to the
Modelclass it should not be instantiated explicitly and is instead returned from the
Control is the main object for interacting with the ASP grounder and solver
and provides a rich set of features. It allows an ASP program that is stored in
a file to be loaded. It can then be grounded and solved and the generated models
returned. It also allows for incremental solving, where a ground program can be
extended and solved repeatedly, as well as both synchronous and asynchronous
solving modes. These featuers are documented in the Clingo Control API so we
only highlight the changes that Clorm introduces.
Clorm adds some new member functions as well as overloading some existing functions:
__init__(). Clorm adds an optional
unifierparameter for specifying a default list of
Predicatesub-classes (or a single
SymbolPredicateUnifierobject). This parameter is passed to any generated
Modelobjects and is used during the unification process of converting raw symbols to Clorm facts. A second parameter
control_is introduced. This parameter is mutually exclusive with the standard parameters for
control_parameter allows an existing
clingo.Controlobject to be passed to the wrapper and is a mechanism to allow Clorm to be used even when Python is embedded within Clingo. See the example
embedded_quickstart.lpfor more details, but the basics are that a Control object is passed to the embedded
mainfunction which is then wrapped in
unifier. A property to get and set the unifier even after the
clorm.clingo.Controlobject has been instantiated.
ctrl = clorm.clingo.Control(control_=ctrl_)
add_facts(facts). A new function that adds facts to an ASP program. The input can be any collection of facts (such as a
clorm.FactBase). A fact can be either a
clingo.Symbolobject. Note however that a
clorm.FactBasecan only contain
clorm.Predicateinstances. Warning: because the initial facts in an ASP program will affect the grounding, new facts should only be added to the program before grounding.
from clorm.clingo import Control
ctrl = Control()
solve(). This function provides a rich set of options for calling the solver and returning the results. These parameters are documented in the Clingo API. Clorm modifies this interface in three ways:
assumptionsparameter. This parameter restricts the returned models to only those satisfying the given assumptions. This parameter must consist of a list of argument-boolean pairs. As well as
clingo.Symbolobjects the argument element is extended to allow
clorm.Predicateinstances or a collection of clingo symbols or clorm predicates. This makes it flexible so that, for example, a
FactBaseobject can be specified as being either True or False in the model.
on_modelcallback parameter. Clorm modifies this interface so that a
clorm.clingo.Modelis pass to the callback function.
If the parameter
yield_=Trueis specified then the return value of the function is a
clorm.clingo.SolveHandleobject. This object iterates over
assign_external(external,truth). This function assigns a truth value to an external atom. This function has been overloaded so that the
externalparameter can also take a
clorm.Predicateinstance or a collection of external atoms (e.g., a
FactBase), where the same truth value is assigned to all atoms in the collection.
release_external(external). This function releases an external atom so that it is permanently false. The function is overloaded so that the
externalparameter can also take a
clorm.Predicateinstance or a collection of extenal atoms.
The Clingo Model object
encapsulates an ASP model and the associated meta-data. It is passed to the
Clingo.solve(on_model=on_model) callback. Clorm wraps the
Model class to
provide a mechanism to extract Clorm facts from the model. The additional and
modified functions are:
facts(self, unifier=None, atoms=False, terms=False, shown=False, raise_on_empty=True). returns a fact base object constructed from unifying against the raw Clingo symbols within the model.
unifierparameter takes a list of
Predicatesub-classes or a single
SymbolPredicateUnifierwhich defines the predicates to unify against. If no
unifierparameter is provided then a
unifiermust have been passed to the
raise_on_emptyparameter specifies that a
ValueErrorwill be raised if the returned fact base is empty. This can happen for two reasons: there were no selected elements in the model or there were elements from the model but none of them was able to unify with the fact base. This parameter is potentially useful for debugging purposes. While returning an empty fact base can be legimate outcomes for some applications, however in many cases this would indicate a problem; either in the ASP program or in the declaration of the predicates to unify against.
Apart from the
raise_on_emptyparameters the remaining parameters are the same as for the
clingo.Model.contains()to allow for a clorm facts as well as a clingo symbols.
The Clingo SolveHandle object provides
a mechanism for iterating over the models when the
yield_=True option is
specified in the
Control.solve() function call. The various iterator functions
are modified by Clorm, but its operations should be transparent to the user.
Clorm provides monkey patching
Control class so that Clorm can be integrated into an existing code
base with minimal effort.
from clorm import monkey; monkey.patch()
from clingo import Control
In general monkey patching should be avoided where possible.