External Theory Support

This module defines a well-specified C interface that must be implemented by external theory plugins. More...

Classes
struct	clingo_theory_value
	A struct to hold values assigned by a theory. More...
struct	clingo_theory
	A theory object to extend solving. More...

Typedefs
typedef int	clingo_theory_value_type_t
	Corresponding type to clingo_theory_value_type.
typedef struct clingo_theory_value	clingo_theory_value_t
	A struct to hold values assigned by a theory.
typedef bool(*	clingo_theory_ast_callback_t) (clingo_ast_t *ast, void *data)
	A callback to rewrite asts.
typedef struct clingo_theory	clingo_theory_t
	A theory object to extend solving.

Enumerations
enum	clingo_theory_value_type_e { clingo_theory_value_type_int = 0 , clingo_theory_value_type_double = 1 , clingo_theory_value_type_symbol = 2 }
	The available value types. More...

Detailed Description

This module defines a well-specified C interface that must be implemented by external theory plugins.

The interface is designed to allow efficient interoperation between the core solver and external theory implementations. It facilitates integration across language barriers (for example, bridging C++ and Python) and across modular boundaries within the system.

Among its responsibilities, the theory interface includes: Providing essential theory callbacks (e.g., rewriting ASTs, model handling, preparing theory data, and statistics collection). Defining the lifecycle of a theory object, including optional cleanup via a destroy callback.

For an example, refer to theory.c.

Enumeration Type Documentation

clingo_theory_value_type_e

enum clingo_theory_value_type_e

The available value types.

Enumerator
clingo_theory_value_type_int	An integer value.
clingo_theory_value_type_double	A double value.
clingo_theory_value_type_symbol	A symbol value.