1 // {{{ MIT License 2 3 // Copyright 2017 Roland Kaminski 4 5 // Permission is hereby granted, free of charge, to any person obtaining a copy 6 // of this software and associated documentation files (the "Software"), to 7 // deal in the Software without restriction, including without limitation the 8 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or 9 // sell copies of the Software, and to permit persons to whom the Software is 10 // furnished to do so, subject to the following conditions: 11 12 // The above copyright notice and this permission notice shall be included in 13 // all copies or substantial portions of the Software. 14 15 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 16 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 17 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 18 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 19 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 20 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 21 // IN THE SOFTWARE. 22 23 // }}} 24 25 //! @file clingo.h 26 //! Single header containing the whole clingo API. 27 //! 28 //! @author Roland Kaminski 29 30 //! @mainpage Clingo C API 31 //! This API provides functions to ground and solve logic programs. 32 //! 33 //! The documentation is structured into different modules. 34 //! To get an overview, checkout the [Modules](modules.html) page. 35 //! To get started, take a look at the documentation of the @ref Control module. 36 //! 37 //! The source code of clingo is available on [github.com/potassco/clingo](https://github.com/potassco/clingo). 38 //! 39 //! For information about the syntax and semantics of the clingo language, 40 //! take a look the [Potassco Guide](https://github.com/potassco/guide/releases/). 41 //! 42 //! @note Each module comes with an example highlighting key functionality. 43 //! The example should be studied along with the module documentation. 44 45 #ifndef CLINGO_H 46 #define CLINGO_H 47 48 #ifdef __cplusplus 49 extern "C" { 50 #endif 51 52 #include <stddef.h> 53 #include <stdint.h> 54 #include <stdbool.h> 55 56 #if defined _WIN32 || defined __CYGWIN__ 57 # define CLINGO_WIN 58 #endif 59 #ifdef CLINGO_NO_VISIBILITY 60 # define CLINGO_VISIBILITY_DEFAULT 61 # define CLINGO_VISIBILITY_PRIVATE 62 #else 63 # ifdef CLINGO_WIN 64 # ifdef CLINGO_BUILD_LIBRARY 65 # define CLINGO_VISIBILITY_DEFAULT __declspec (dllexport) 66 # else 67 # define CLINGO_VISIBILITY_DEFAULT __declspec (dllimport) 68 # endif 69 # define CLINGO_VISIBILITY_PRIVATE 70 # else 71 # if __GNUC__ >= 4 72 # define CLINGO_VISIBILITY_DEFAULT __attribute__ ((visibility ("default"))) 73 # define CLINGO_VISIBILITY_PRIVATE __attribute__ ((visibility ("hidden"))) 74 # else 75 # define CLINGO_VISIBILITY_DEFAULT 76 # define CLINGO_VISIBILITY_PRIVATE 77 # endif 78 # endif 79 #endif 80 81 #if defined __GNUC__ 82 #define CLINGO_DEPRECATED __attribute__((deprecated)) 83 #elif defined _MSC_VER 84 #define CLINGO_DEPRECATED __declspec(deprecated) 85 #else 86 #define CLINGO_DEPRECATED 87 #endif 88 89 // {{{1 basic types and error/warning handling 90 91 //! @example version.c 92 //! The example shows how to get version information. 93 //! 94 //! ## Output ## 95 //! 96 //! ~~~~~~~~~~~~ 97 //! $ ./version 98 //! Hello, this is clingo version... 99 //! ~~~~~~~~~~~~ 100 //! 101 //! ## Code ## 102 103 //! @defgroup BasicTypes Basic Data Types and Functions 104 //! Data types and functions used throughout all modules and version information. 105 //! 106 //! For an example, see @ref version.c. 107 108 //! @addtogroup BasicTypes 109 //! @{ 110 111 //! Major version number. 112 #define CLINGO_VERSION_MAJOR 5 113 //! Minor version number. 114 #define CLINGO_VERSION_MINOR 5 115 //! Revision number. 116 #define CLINGO_VERSION_REVISION 1 117 //! String representation of version. 118 #define CLINGO_VERSION "5.5.1" 119 120 //! Signed integer type used for aspif and solver literals. 121 typedef int32_t clingo_literal_t; 122 //! Unsigned integer type used for aspif atoms. 123 typedef uint32_t clingo_atom_t; 124 //! Unsigned integer type used in various places. 125 typedef uint32_t clingo_id_t; 126 //! Signed integer type for weights in sum aggregates and minimize constraints. 127 typedef int32_t clingo_weight_t; 128 //! A Literal with an associated weight. 129 typedef struct clingo_weighted_literal { 130 clingo_literal_t literal; 131 clingo_weight_t weight; 132 } clingo_weighted_literal_t; 133 134 135 //! Enumeration of error codes. 136 //! 137 //! @note Errors can only be recovered from if explicitly mentioned; most 138 //! functions do not provide strong exception guarantees. This means that in 139 //! case of errors associated objects cannot be used further. If such an 140 //! object has a free function, this function can and should still be called. 141 enum clingo_error_e { 142 clingo_error_success = 0, //!< successful API calls 143 clingo_error_runtime = 1, //!< errors only detectable at runtime like invalid input 144 clingo_error_logic = 2, //!< wrong usage of the clingo API 145 clingo_error_bad_alloc = 3, //!< memory could not be allocated 146 clingo_error_unknown = 4 //!< errors unrelated to clingo 147 }; 148 //! Corresponding type to ::clingo_error_e. 149 typedef int clingo_error_t; 150 //! Convert error code into string. 151 CLINGO_VISIBILITY_DEFAULT char const *clingo_error_string(clingo_error_t code); 152 //! Get the last error code set by a clingo API call. 153 //! @note Each thread has its own local error code. 154 //! @return error code 155 CLINGO_VISIBILITY_DEFAULT clingo_error_t clingo_error_code(); 156 //! Get the last error message set if an API call fails. 157 //! @note Each thread has its own local error message. 158 //! @return error message or NULL 159 CLINGO_VISIBILITY_DEFAULT char const *clingo_error_message(); 160 //! Set a custom error code and message in the active thread. 161 //! @param[in] code the error code 162 //! @param[in] message the error message 163 CLINGO_VISIBILITY_DEFAULT void clingo_set_error(clingo_error_t code, char const *message); 164 165 //! Enumeration of warning codes. 166 enum clingo_warning_e { 167 clingo_warning_operation_undefined = 0, //!< undefined arithmetic operation or weight of aggregate 168 clingo_warning_runtime_error = 1, //!< to report multiple errors; a corresponding runtime error is raised later 169 clingo_warning_atom_undefined = 2, //!< undefined atom in program 170 clingo_warning_file_included = 3, //!< same file included multiple times 171 clingo_warning_variable_unbounded = 4, //!< CSP variable with unbounded domain 172 clingo_warning_global_variable = 5, //!< global variable in tuple of aggregate element 173 clingo_warning_other = 6, //!< other kinds of warnings 174 }; 175 //! Corresponding type to ::clingo_warning_e. 176 typedef int clingo_warning_t; 177 //! Convert warning code into string. 178 CLINGO_VISIBILITY_DEFAULT char const *clingo_warning_string(clingo_warning_t code); 179 //! Callback to intercept warning messages. 180 //! 181 //! @param[in] code associated warning code 182 //! @param[in] message warning message 183 //! @param[in] data user data for callback 184 //! 185 //! @see clingo_control_new() 186 //! @see clingo_parse_term() 187 //! @see clingo_parse_program() 188 typedef void (*clingo_logger_t)(clingo_warning_t code, char const *message, void *data); 189 190 //! Obtain the clingo version. 191 //! 192 //! @param[out] major major version number 193 //! @param[out] minor minor version number 194 //! @param[out] revision revision number 195 CLINGO_VISIBILITY_DEFAULT void clingo_version(int *major, int *minor, int *revision); 196 197 //! Represents three-valued truth values. 198 enum clingo_truth_value_e { 199 clingo_truth_value_free = 0, //!< no truth value 200 clingo_truth_value_true = 1, //!< true 201 clingo_truth_value_false = 2 //!< false 202 }; 203 //! Corresponding type to ::clingo_truth_value_e. 204 typedef int clingo_truth_value_t; 205 206 //! Represents a source code location marking its beginnig and end. 207 //! 208 //! @note Not all locations refer to physical files. 209 //! By convention, such locations use a name put in angular brackets as filename. 210 //! The string members of a location object are internalized and valid for the duration of the process. 211 typedef struct clingo_location { 212 char const *begin_file; //!< the file where the location begins 213 char const *end_file; //!< the file where the location ends 214 size_t begin_line; //!< the line where the location begins 215 size_t end_line; //!< the line where the location ends 216 size_t begin_column; //!< the column where the location begins 217 size_t end_column; //!< the column where the location ends 218 } clingo_location_t; 219 220 //! @} 221 222 // {{{1 signature and symbols 223 224 //! @example symbol.c 225 //! The example shows how to create and inspect symbols. 226 //! 227 //! ## Output ## 228 //! 229 //! ~~~~~~~~~~~~ 230 //! $ ./symbol 0 231 //! the hash of 42 is 281474976710698 232 //! the hash of x is 562949963481760 233 //! the hash of x(42,x) is 1407374893613792 234 //! 42 is equal to 42 235 //! 42 is not equal to x 236 //! 42 is less than x 237 //! ~~~~~~~~~~~~ 238 //! 239 //! ## Code ## 240 241 //! @defgroup Symbols Symbols 242 //! Working with (evaluated) ground terms and related functions. 243 //! 244 //! @note All functions in this module are thread-safe. 245 //! 246 //! For an example, see @ref symbol.c. 247 248 //! @addtogroup Symbols 249 //! @{ 250 251 //! Represents a predicate signature. 252 //! 253 //! Signatures have a name and an arity, and can be positive or negative (to 254 //! represent classical negation). 255 typedef uint64_t clingo_signature_t; 256 257 //! @name Signature Functions 258 //! @{ 259 260 //! Create a new signature. 261 //! 262 //! @param[in] name name of the signature 263 //! @param[in] arity arity of the signature 264 //! @param[in] positive false if the signature has a classical negation sign 265 //! @param[out] signature the resulting signature 266 //! @return whether the call was successful; might set one of the following error codes: 267 //! - ::clingo_error_bad_alloc 268 CLINGO_VISIBILITY_DEFAULT bool clingo_signature_create(char const *name, uint32_t arity, bool positive, clingo_signature_t *signature); 269 //! Get the name of a signature. 270 //! 271 //! @note 272 //! The string is internalized and valid for the duration of the process. 273 //! 274 //! @param[in] signature the target signature 275 //! @return the name of the signature 276 CLINGO_VISIBILITY_DEFAULT char const *clingo_signature_name(clingo_signature_t signature); 277 //! Get the arity of a signature. 278 //! 279 //! @param[in] signature the target signature 280 //! @return the arity of the signature 281 CLINGO_VISIBILITY_DEFAULT uint32_t clingo_signature_arity(clingo_signature_t signature); 282 //! Whether the signature is positive (is not classically negated). 283 //! 284 //! @param[in] signature the target signature 285 //! @return whether the signature has no sign 286 CLINGO_VISIBILITY_DEFAULT bool clingo_signature_is_positive(clingo_signature_t signature); 287 //! Whether the signature is negative (is classically negated). 288 //! 289 //! @param[in] signature the target signature 290 //! @return whether the signature has a sign 291 CLINGO_VISIBILITY_DEFAULT bool clingo_signature_is_negative(clingo_signature_t signature); 292 //! Check if two signatures are equal. 293 //! 294 //! @param[in] a first signature 295 //! @param[in] b second signature 296 //! @return whether a == b 297 CLINGO_VISIBILITY_DEFAULT bool clingo_signature_is_equal_to(clingo_signature_t a, clingo_signature_t b); 298 //! Check if a signature is less than another signature. 299 //! 300 //! Signatures are compared first by sign (unsigned < signed), then by arity, 301 //! then by name. 302 //! 303 //! @param[in] a first signature 304 //! @param[in] b second signature 305 //! @return whether a < b 306 CLINGO_VISIBILITY_DEFAULT bool clingo_signature_is_less_than(clingo_signature_t a, clingo_signature_t b); 307 //! Calculate a hash code of a signature. 308 //! 309 //! @param[in] signature the target signature 310 //! @return the hash code of the signature 311 CLINGO_VISIBILITY_DEFAULT size_t clingo_signature_hash(clingo_signature_t signature); 312 313 //! @} 314 315 //! Enumeration of available symbol types. 316 enum clingo_symbol_type_e { 317 clingo_symbol_type_infimum = 0, //!< the <tt>\#inf</tt> symbol 318 clingo_symbol_type_number = 1, //!< a numeric symbol, e.g., `1` 319 clingo_symbol_type_string = 4, //!< a string symbol, e.g., `"a"` 320 clingo_symbol_type_function = 5, //!< a numeric symbol, e.g., `c`, `(1, "a")`, or `f(1,"a")` 321 clingo_symbol_type_supremum = 7 //!< the <tt>\#sup</tt> symbol 322 }; 323 //! Corresponding type to ::clingo_symbol_type. 324 typedef int clingo_symbol_type_t; 325 326 //! Represents a symbol. 327 //! 328 //! This includes numbers, strings, functions (including constants when 329 //! arguments are empty and tuples when the name is empty), <tt>\#inf</tt> and <tt>\#sup</tt>. 330 typedef uint64_t clingo_symbol_t; 331 332 //! @name Symbol Construction Functions 333 //! @{ 334 335 //! Construct a symbol representing a number. 336 //! 337 //! @param[in] number the number 338 //! @param[out] symbol the resulting symbol 339 CLINGO_VISIBILITY_DEFAULT void clingo_symbol_create_number(int number, clingo_symbol_t *symbol); 340 //! Construct a symbol representing \#sup. 341 //! 342 //! @param[out] symbol the resulting symbol 343 CLINGO_VISIBILITY_DEFAULT void clingo_symbol_create_supremum(clingo_symbol_t *symbol); 344 //! Construct a symbol representing <tt>\#inf</tt>. 345 //! 346 //! @param[out] symbol the resulting symbol 347 CLINGO_VISIBILITY_DEFAULT void clingo_symbol_create_infimum(clingo_symbol_t *symbol); 348 //! Construct a symbol representing a string. 349 //! 350 //! @param[in] string the string 351 //! @param[out] symbol the resulting symbol 352 //! @return whether the call was successful; might set one of the following error codes: 353 //! - ::clingo_error_bad_alloc 354 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_create_string(char const *string, clingo_symbol_t *symbol); 355 //! Construct a symbol representing an id. 356 //! 357 //! @note This is just a shortcut for clingo_symbol_create_function() with 358 //! empty arguments. 359 //! 360 //! @param[in] name the name 361 //! @param[in] positive whether the symbol has a classical negation sign 362 //! @param[out] symbol the resulting symbol 363 //! @return whether the call was successful; might set one of the following error codes: 364 //! - ::clingo_error_bad_alloc 365 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_create_id(char const *name, bool positive, clingo_symbol_t *symbol); 366 //! Construct a symbol representing a function or tuple. 367 //! 368 //! @note To create tuples, the empty string has to be used as name. 369 //! 370 //! @param[in] name the name of the function 371 //! @param[in] arguments the arguments of the function 372 //! @param[in] arguments_size the number of arguments 373 //! @param[in] positive whether the symbol has a classical negation sign 374 //! @param[out] symbol the resulting symbol 375 //! @return whether the call was successful; might set one of the following error codes: 376 //! - ::clingo_error_bad_alloc 377 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_create_function(char const *name, clingo_symbol_t const *arguments, size_t arguments_size, bool positive, clingo_symbol_t *symbol); 378 379 //! @} 380 381 //! @name Symbol Inspection Functions 382 //! @{ 383 384 //! Get the number of a symbol. 385 //! 386 //! @param[in] symbol the target symbol 387 //! @param[out] number the resulting number 388 //! @return whether the call was successful; might set one of the following error codes: 389 //! - ::clingo_error_runtime if symbol is not of type ::clingo_symbol_type_number 390 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_number(clingo_symbol_t symbol, int *number); 391 //! Get the name of a symbol. 392 //! 393 //! @note 394 //! The string is internalized and valid for the duration of the process. 395 //! 396 //! @param[in] symbol the target symbol 397 //! @param[out] name the resulting name 398 //! @return whether the call was successful; might set one of the following error codes: 399 //! - ::clingo_error_runtime if symbol is not of type ::clingo_symbol_type_function 400 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_name(clingo_symbol_t symbol, char const **name); 401 //! Get the string of a symbol. 402 //! 403 //! @note 404 //! The string is internalized and valid for the duration of the process. 405 //! 406 //! @param[in] symbol the target symbol 407 //! @param[out] string the resulting string 408 //! @return whether the call was successful; might set one of the following error codes: 409 //! - ::clingo_error_runtime if symbol is not of type ::clingo_symbol_type_string 410 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_string(clingo_symbol_t symbol, char const **string); 411 //! Check if a function is positive (does not have a sign). 412 //! 413 //! @param[in] symbol the target symbol 414 //! @param[out] positive the result 415 //! @return whether the call was successful; might set one of the following error codes: 416 //! - ::clingo_error_runtime if symbol is not of type ::clingo_symbol_type_function 417 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_is_positive(clingo_symbol_t symbol, bool *positive); 418 //! Check if a function is negative (has a sign). 419 //! 420 //! @param[in] symbol the target symbol 421 //! @param[out] negative the result 422 //! @return whether the call was successful; might set one of the following error codes: 423 //! - ::clingo_error_runtime if symbol is not of type ::clingo_symbol_type_function 424 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_is_negative(clingo_symbol_t symbol, bool *negative); 425 //! Get the arguments of a symbol. 426 //! 427 //! @param[in] symbol the target symbol 428 //! @param[out] arguments the resulting arguments 429 //! @param[out] arguments_size the number of arguments 430 //! @return whether the call was successful; might set one of the following error codes: 431 //! - ::clingo_error_runtime if symbol is not of type ::clingo_symbol_type_function 432 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_arguments(clingo_symbol_t symbol, clingo_symbol_t const **arguments, size_t *arguments_size); 433 //! Get the type of a symbol. 434 //! 435 //! @param[in] symbol the target symbol 436 //! @return the type of the symbol 437 CLINGO_VISIBILITY_DEFAULT clingo_symbol_type_t clingo_symbol_type(clingo_symbol_t symbol); 438 //! Get the size of the string representation of a symbol (including the terminating 0). 439 //! 440 //! @param[in] symbol the target symbol 441 //! @param[out] size the resulting size 442 //! @return whether the call was successful; might set one of the following error codes: 443 //! - ::clingo_error_bad_alloc 444 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_to_string_size(clingo_symbol_t symbol, size_t *size); 445 //! Get the string representation of a symbol. 446 //! 447 //! @param[in] symbol the target symbol 448 //! @param[out] string the resulting string 449 //! @param[in] size the size of the string 450 //! @return whether the call was successful; might set one of the following error codes: 451 //! - ::clingo_error_bad_alloc 452 //! 453 //! @see clingo_symbol_to_string_size() 454 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_to_string(clingo_symbol_t symbol, char *string, size_t size); 455 456 //! @} 457 458 //! @name Symbol Comparison Functions 459 //! @{ 460 461 //! Check if two symbols are equal. 462 //! 463 //! @param[in] a first symbol 464 //! @param[in] b second symbol 465 //! @return whether a == b 466 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_is_equal_to(clingo_symbol_t a, clingo_symbol_t b); 467 //! Check if a symbol is less than another symbol. 468 //! 469 //! Symbols are first compared by type. If the types are equal, the values are 470 //! compared (where strings are compared using strcmp). Functions are first 471 //! compared by signature and then lexicographically by arguments. 472 //! 473 //! @param[in] a first symbol 474 //! @param[in] b second symbol 475 //! @return whether a < b 476 CLINGO_VISIBILITY_DEFAULT bool clingo_symbol_is_less_than(clingo_symbol_t a, clingo_symbol_t b); 477 //! Calculate a hash code of a symbol. 478 //! 479 //! @param[in] symbol the target symbol 480 //! @return the hash code of the symbol 481 CLINGO_VISIBILITY_DEFAULT size_t clingo_symbol_hash(clingo_symbol_t symbol); 482 483 //! @} 484 485 //! Internalize a string. 486 //! 487 //! This functions takes a string as input and returns an equal unique string 488 //! that is (at the moment) not freed until the program is closed. 489 //! 490 //! @param[in] string the string to internalize 491 //! @param[out] result the internalized string 492 //! @return whether the call was successful; might set one of the following error codes: 493 //! - ::clingo_error_bad_alloc 494 CLINGO_VISIBILITY_DEFAULT bool clingo_add_string(char const *string, char const **result); 495 //! Parse a term in string form. 496 //! 497 //! The result of this function is a symbol. The input term can contain 498 //! unevaluated functions, which are evaluated during parsing. 499 //! 500 //! @param[in] string the string to parse 501 //! @param[in] logger optional logger to report warnings during parsing 502 //! @param[in] logger_data user data for the logger 503 //! @param[in] message_limit maximum number of times to call the logger 504 //! @param[out] symbol the resulting symbol 505 //! @return whether the call was successful; might set one of the following error codes: 506 //! - ::clingo_error_bad_alloc 507 //! - ::clingo_error_runtime if parsing fails 508 CLINGO_VISIBILITY_DEFAULT bool clingo_parse_term(char const *string, clingo_logger_t logger, void *logger_data, unsigned message_limit, clingo_symbol_t *symbol); 509 510 //! @} 511 512 // {{{1 symbolic atoms 513 514 //! @example symbolic-atoms.c 515 //! The example shows how to iterate over symbolic atoms. 516 //! 517 //! ## Output ## 518 //! 519 //! ~~~~~~~~~~~~ 520 //! ./symbolic-atoms 0 521 //! Symbolic atoms: 522 //! b 523 //! c, external 524 //! a, fact 525 //! ~~~~~~~~~~~~ 526 //! 527 //! ## Code ## 528 529 //! @defgroup SymbolicAtoms Symbolic Atom Inspection 530 //! Inspection of atoms occurring in ground logic programs. 531 //! 532 //! For an example, see @ref symbolic-atoms.c. 533 //! @ingroup Control 534 535 //! @addtogroup SymbolicAtoms 536 //! @{ 537 538 //! Object to inspect symbolic atoms in a program---the relevant Herbrand base 539 //! gringo uses to instantiate programs. 540 //! 541 //! @see clingo_control_symbolic_atoms() 542 typedef struct clingo_symbolic_atoms clingo_symbolic_atoms_t; 543 //! Object to iterate over symbolic atoms. 544 //! 545 //! Such an iterator either points to a symbolic atom within a sequence of 546 //! symbolic atoms or to the end of the sequence. 547 //! 548 //! @note Iterators are valid as long as the underlying sequence is not modified. 549 //! Operations that can change this sequence are ::clingo_control_ground(), 550 //! ::clingo_control_cleanup(), and functions that modify the underlying 551 //! non-ground program. 552 typedef uint64_t clingo_symbolic_atom_iterator_t; 553 //! Get the number of different atoms occurring in a logic program. 554 //! 555 //! @param[in] atoms the target 556 //! @param[out] size the number of atoms 557 //! @return whether the call was successful 558 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_size(clingo_symbolic_atoms_t const *atoms, size_t *size); 559 //! Get a forward iterator to the beginning of the sequence of all symbolic 560 //! atoms optionally restricted to a given signature. 561 //! 562 //! @param[in] atoms the target 563 //! @param[in] signature optional signature 564 //! @param[out] iterator the resulting iterator 565 //! @return whether the call was successful 566 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_begin(clingo_symbolic_atoms_t const *atoms, clingo_signature_t const *signature, clingo_symbolic_atom_iterator_t *iterator); 567 //! Iterator pointing to the end of the sequence of symbolic atoms. 568 //! 569 //! @param[in] atoms the target 570 //! @param[out] iterator the resulting iterator 571 //! @return whether the call was successful 572 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_end(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t *iterator); 573 //! Find a symbolic atom given its symbolic representation. 574 //! 575 //! @param[in] atoms the target 576 //! @param[in] symbol the symbol to lookup 577 //! @param[out] iterator iterator pointing to the symbolic atom or to the end 578 //! of the sequence if no corresponding atom is found 579 //! @return whether the call was successful 580 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_find(clingo_symbolic_atoms_t const *atoms, clingo_symbol_t symbol, clingo_symbolic_atom_iterator_t *iterator); 581 //! Check if two iterators point to the same element (or end of the sequence). 582 //! 583 //! @param[in] atoms the target 584 //! @param[in] a the first iterator 585 //! @param[in] b the second iterator 586 //! @param[out] equal whether the two iterators are equal 587 //! @return whether the call was successful 588 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_iterator_is_equal_to(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t a, clingo_symbolic_atom_iterator_t b, bool *equal); 589 //! Get the symbolic representation of an atom. 590 //! 591 //! @param[in] atoms the target 592 //! @param[in] iterator iterator to the atom 593 //! @param[out] symbol the resulting symbol 594 //! @return whether the call was successful 595 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_symbol(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t iterator, clingo_symbol_t *symbol); 596 //! Check whether an atom is a fact. 597 //! 598 //! @note This does not determine if an atom is a cautious consequence. The 599 //! grounding or solving component's simplifications can only detect this in 600 //! some cases. 601 //! 602 //! @param[in] atoms the target 603 //! @param[in] iterator iterator to the atom 604 //! @param[out] fact whether the atom is a fact 605 //! @return whether the call was successful 606 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_is_fact(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t iterator, bool *fact); 607 //! Check whether an atom is external. 608 //! 609 //! An atom is external if it has been defined using an external directive and 610 //! has not been released or defined by a rule. 611 //! 612 //! @param[in] atoms the target 613 //! @param[in] iterator iterator to the atom 614 //! @param[out] external whether the atom is a external 615 //! @return whether the call was successful 616 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_is_external(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t iterator, bool *external); 617 //! Returns the (numeric) aspif literal corresponding to the given symbolic atom. 618 //! 619 //! Such a literal can be mapped to a solver literal (see the \ref Propagator 620 //! module) or be used in rules in aspif format (see the \ref ProgramBuilder 621 //! module). 622 //! 623 //! @param[in] atoms the target 624 //! @param[in] iterator iterator to the atom 625 //! @param[out] literal the associated literal 626 //! @return whether the call was successful 627 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_literal(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t iterator, clingo_literal_t *literal); 628 //! Get the number of different predicate signatures used in the program. 629 //! 630 //! @param[in] atoms the target 631 //! @param[out] size the number of signatures 632 //! @return whether the call was successful 633 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_signatures_size(clingo_symbolic_atoms_t const *atoms, size_t *size); 634 //! Get the predicate signatures occurring in a logic program. 635 //! 636 //! @param[in] atoms the target 637 //! @param[out] signatures the resulting signatures 638 //! @param[in] size the number of signatures 639 //! @return whether the call was successful; might set one of the following error codes: 640 //! - ::clingo_error_bad_alloc 641 //! - ::clingo_error_runtime if the size is too small 642 //! 643 //! @see clingo_symbolic_atoms_signatures_size() 644 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_signatures(clingo_symbolic_atoms_t const *atoms, clingo_signature_t *signatures, size_t size); 645 //! Get an iterator to the next element in the sequence of symbolic atoms. 646 //! 647 //! @param[in] atoms the target 648 //! @param[in] iterator the current iterator 649 //! @param[out] next the succeeding iterator 650 //! @return whether the call was successful 651 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_next(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t iterator, clingo_symbolic_atom_iterator_t *next); 652 //! Check whether the given iterator points to some element with the sequence 653 //! of symbolic atoms or to the end of the sequence. 654 //! 655 //! @param[in] atoms the target 656 //! @param[in] iterator the iterator 657 //! @param[out] valid whether the iterator points to some element within the 658 //! sequence 659 //! @return whether the call was successful 660 CLINGO_VISIBILITY_DEFAULT bool clingo_symbolic_atoms_is_valid(clingo_symbolic_atoms_t const *atoms, clingo_symbolic_atom_iterator_t iterator, bool *valid); 661 662 //! Callback function to inject symbols. 663 //! 664 //! @param symbols array of symbols 665 //! @param symbols_size size of the symbol array 666 //! @param data user data of the callback 667 //! @return whether the call was successful; might set one of the following error codes: 668 //! - ::clingo_error_bad_alloc 669 //! @see ::clingo_ground_callback_t 670 typedef bool (*clingo_symbol_callback_t) (clingo_symbol_t const *symbols, size_t symbols_size, void *data); 671 //! @} 672 673 // {{{1 theory atoms 674 675 //! @example theory-atoms.c 676 //! The example shows how to inspect and use theory atoms. 677 //! 678 //! @verbatim@endverbatim 679 //! 680 //! This is a very simple example that uses the @link ProgramBuilder backend@endlink to let theory atoms affect answer sets. 681 //! In general, the backend can be used to implement a custom theory by translating it to a logic program. 682 //! On the other hand, a @link Propagator propagator@endlink can be used to implement a custom theory without adding any constraints in advance. 683 //! Or both approaches can be combined. 684 //! 685 //! ## Output ## 686 //! 687 //! ~~~~~~~~~~~~ 688 //! ./theory-atoms 0 689 //! number of grounded theory atoms: 2 690 //! theory atom b/1 has a guard: true 691 //! Model: y 692 //! Model: x y 693 //! ~~~~~~~~~~~~ 694 //! 695 //! ## Code ## 696 697 //! @defgroup TheoryAtoms Theory Atom Inspection 698 //! Inspection of theory atoms occurring in ground logic programs. 699 //! @ingroup Control 700 //! 701 //! During grounding, theory atoms get consecutive numbers starting with zero. 702 //! The total number of theory atoms can be obtained using clingo_theory_atoms_size(). 703 //! 704 //! @attention 705 //! All structural information about theory atoms, elements, and terms is reset after @link clingo_control_solve() solving@endlink. 706 //! If afterward fresh theory atoms are @link clingo_control_ground() grounded@endlink, previously used ids are reused. 707 //! 708 //! For an example, see @ref theory-atoms.c. 709 710 //! @addtogroup TheoryAtoms 711 //! @{ 712 713 //! Enumeration of theory term types. 714 enum clingo_theory_term_type_e { 715 clingo_theory_term_type_tuple = 0, //!< a tuple term, e.g., `(1,2,3)` 716 clingo_theory_term_type_list = 1, //!< a list term, e.g., `[1,2,3]` 717 clingo_theory_term_type_set = 2, //!< a set term, e.g., `{1,2,3}` 718 clingo_theory_term_type_function = 3, //!< a function term, e.g., `f(1,2,3)` 719 clingo_theory_term_type_number = 4, //!< a number term, e.g., `42` 720 clingo_theory_term_type_symbol = 5 //!< a symbol term, e.g., `c` 721 }; 722 //! Corresponding type to ::clingo_theory_term_type_e. 723 typedef int clingo_theory_term_type_t; 724 725 //! Container that stores theory atoms, elements, and terms (see @ref clingo_control_theory_atoms()). 726 typedef struct clingo_theory_atoms clingo_theory_atoms_t; 727 728 //! @name Theory Term Inspection 729 //! @{ 730 731 //! Get the type of the given theory term. 732 //! 733 //! @param[in] atoms container where the term is stored 734 //! @param[in] term id of the term 735 //! @param[out] type the resulting type 736 //! @return whether the call was successful 737 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_type(clingo_theory_atoms_t const *atoms, clingo_id_t term, clingo_theory_term_type_t *type); 738 //! Get the number of the given numeric theory term. 739 //! 740 //! @pre The term must be of type ::clingo_theory_term_type_number. 741 //! @param[in] atoms container where the term is stored 742 //! @param[in] term id of the term 743 //! @param[out] number the resulting number 744 //! @return whether the call was successful 745 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_number(clingo_theory_atoms_t const *atoms, clingo_id_t term, int *number); 746 //! Get the name of the given constant or function theory term. 747 //! 748 //! @note 749 //! The lifetime of the string is tied to the current solve step. 750 //! 751 //! @pre The term must be of type ::clingo_theory_term_type_function or ::clingo_theory_term_type_symbol. 752 //! @param[in] atoms container where the term is stored 753 //! @param[in] term id of the term 754 //! @param[out] name the resulting name 755 //! @return whether the call was successful 756 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_name(clingo_theory_atoms_t const *atoms, clingo_id_t term, char const **name); 757 //! Get the arguments of the given function theory term. 758 //! 759 //! @pre The term must be of type ::clingo_theory_term_type_function. 760 //! @param[in] atoms container where the term is stored 761 //! @param[in] term id of the term 762 //! @param[out] arguments the resulting arguments in form of an array of term ids 763 //! @param[out] size the number of arguments 764 //! @return whether the call was successful 765 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_arguments(clingo_theory_atoms_t const *atoms, clingo_id_t term, clingo_id_t const **arguments, size_t *size); 766 //! Get the size of the string representation of the given theory term (including the terminating 0). 767 //! 768 //! @param[in] atoms container where the term is stored 769 //! @param[in] term id of the term 770 //! @param[out] size the resulting size 771 //! @return whether the call was successful; might set one of the following error codes: 772 //! - ::clingo_error_bad_alloc 773 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_to_string_size(clingo_theory_atoms_t const *atoms, clingo_id_t term, size_t *size); 774 //! Get the string representation of the given theory term. 775 //! 776 //! @param[in] atoms container where the term is stored 777 //! @param[in] term id of the term 778 //! @param[out] string the resulting string 779 //! @param[in] size the size of the string 780 //! @return whether the call was successful; might set one of the following error codes: 781 //! - ::clingo_error_runtime if the size is too small 782 //! - ::clingo_error_bad_alloc 783 //! 784 //! @see clingo_theory_atoms_term_to_string_size() 785 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_term_to_string(clingo_theory_atoms_t const *atoms, clingo_id_t term, char *string, size_t size); 786 //! @} 787 788 //! @name Theory Element Inspection 789 //! @{ 790 791 //! Get the tuple (array of theory terms) of the given theory element. 792 //! 793 //! @param[in] atoms container where the element is stored 794 //! @param[in] element id of the element 795 //! @param[out] tuple the resulting array of term ids 796 //! @param[out] size the number of term ids 797 //! @return whether the call was successful 798 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_tuple(clingo_theory_atoms_t const *atoms, clingo_id_t element, clingo_id_t const **tuple, size_t *size); 799 //! Get the condition (array of aspif literals) of the given theory element. 800 //! 801 //! @param[in] atoms container where the element is stored 802 //! @param[in] element id of the element 803 //! @param[out] condition the resulting array of aspif literals 804 //! @param[out] size the number of term literals 805 //! @return whether the call was successful 806 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_condition(clingo_theory_atoms_t const *atoms, clingo_id_t element, clingo_literal_t const **condition, size_t *size); 807 //! Get the id of the condition of the given theory element. 808 //! 809 //! @note 810 //! This id can be mapped to a solver literal using clingo_propagate_init_solver_literal(). 811 //! This id is not (necessarily) an aspif literal; 812 //! to get aspif literals use clingo_theory_atoms_element_condition(). 813 //! 814 //! @param[in] atoms container where the element is stored 815 //! @param[in] element id of the element 816 //! @param[out] condition the resulting condition id 817 //! @return whether the call was successful 818 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_condition_id(clingo_theory_atoms_t const *atoms, clingo_id_t element, clingo_literal_t *condition); 819 //! Get the size of the string representation of the given theory element (including the terminating 0). 820 //! 821 //! @param[in] atoms container where the element is stored 822 //! @param[in] element id of the element 823 //! @param[out] size the resulting size 824 //! @return whether the call was successful; might set one of the following error codes: 825 //! - ::clingo_error_bad_alloc 826 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_to_string_size(clingo_theory_atoms_t const *atoms, clingo_id_t element, size_t *size); 827 //! Get the string representation of the given theory element. 828 //! 829 //! @param[in] atoms container where the element is stored 830 //! @param[in] element id of the element 831 //! @param[out] string the resulting string 832 //! @param[in] size the size of the string 833 //! @return whether the call was successful; might set one of the following error codes: 834 //! - ::clingo_error_runtime if the size is too small 835 //! - ::clingo_error_bad_alloc 836 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_element_to_string(clingo_theory_atoms_t const *atoms, clingo_id_t element, char *string, size_t size); 837 //! @} 838 839 //! @name Theory Atom Inspection 840 //! @{ 841 842 //! Get the total number of theory atoms. 843 //! 844 //! @param[in] atoms the target 845 //! @param[out] size the resulting number 846 //! @return whether the call was successful 847 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_size(clingo_theory_atoms_t const *atoms, size_t *size); 848 //! Get the theory term associated with the theory atom. 849 //! 850 //! @param[in] atoms container where the atom is stored 851 //! @param[in] atom id of the atom 852 //! @param[out] term the resulting term id 853 //! @return whether the call was successful 854 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_term(clingo_theory_atoms_t const *atoms, clingo_id_t atom, clingo_id_t *term); 855 //! Get the theory elements associated with the theory atom. 856 //! 857 //! @param[in] atoms container where the atom is stored 858 //! @param[in] atom id of the atom 859 //! @param[out] elements the resulting array of elements 860 //! @param[out] size the number of elements 861 //! @return whether the call was successful 862 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_elements(clingo_theory_atoms_t const *atoms, clingo_id_t atom, clingo_id_t const **elements, size_t *size); 863 //! Whether the theory atom has a guard. 864 //! 865 //! @param[in] atoms container where the atom is stored 866 //! @param[in] atom id of the atom 867 //! @param[out] has_guard whether the theory atom has a guard 868 //! @return whether the call was successful 869 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_has_guard(clingo_theory_atoms_t const *atoms, clingo_id_t atom, bool *has_guard); 870 //! Get the guard consisting of a theory operator and a theory term of the given theory atom. 871 //! 872 //! @note 873 //! The lifetime of the string is tied to the current solve step. 874 //! 875 //! @param[in] atoms container where the atom is stored 876 //! @param[in] atom id of the atom 877 //! @param[out] connective the resulting theory operator 878 //! @param[out] term the resulting term 879 //! @return whether the call was successful 880 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_guard(clingo_theory_atoms_t const *atoms, clingo_id_t atom, char const **connective, clingo_id_t *term); 881 //! Get the aspif literal associated with the given theory atom. 882 //! 883 //! @param[in] atoms container where the atom is stored 884 //! @param[in] atom id of the atom 885 //! @param[out] literal the resulting literal 886 //! @return whether the call was successful 887 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_literal(clingo_theory_atoms_t const *atoms, clingo_id_t atom, clingo_literal_t *literal); 888 //! Get the size of the string representation of the given theory atom (including the terminating 0). 889 //! 890 //! @param[in] atoms container where the atom is stored 891 //! @param[in] atom id of the element 892 //! @param[out] size the resulting size 893 //! @return whether the call was successful; might set one of the following error codes: 894 //! - ::clingo_error_bad_alloc 895 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_to_string_size(clingo_theory_atoms_t const *atoms, clingo_id_t atom, size_t *size); 896 //! Get the string representation of the given theory atom. 897 //! 898 //! @param[in] atoms container where the atom is stored 899 //! @param[in] atom id of the element 900 //! @param[out] string the resulting string 901 //! @param[in] size the size of the string 902 //! @return whether the call was successful; might set one of the following error codes: 903 //! - ::clingo_error_runtime if the size is too small 904 //! - ::clingo_error_bad_alloc 905 CLINGO_VISIBILITY_DEFAULT bool clingo_theory_atoms_atom_to_string(clingo_theory_atoms_t const *atoms, clingo_id_t atom, char *string, size_t size); 906 //! @} 907 908 //! @} 909 910 // {{{1 propagator 911 912 //! @example propagator.c 913 //! The example shows how to write a simple propagator for the pigeon hole problem. For 914 //! a detailed description of what is implemented here and some background, take a look at the following paper: 915 //! 916 //! https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/iclp/GebserKKOSW16x 917 //! 918 //! ## Output ## 919 //! 920 //! The output is empty because the pigeon hole problem is unsatisfiable. 921 //! 922 //! ## Code ## 923 924 //! @defgroup Propagator Theory Propagation 925 //! Extend the search with propagators for arbitrary theories. 926 //! 927 //! For an example, see @ref propagator.c. 928 //! @ingroup Control 929 930 //! @addtogroup Propagator 931 //! @{ 932 933 //! Represents a (partial) assignment of a particular solver. 934 //! 935 //! An assignment assigns truth values to a set of literals. 936 //! A literal is assigned to either @link clingo_assignment_truth_value() true or false, or is unassigned@endlink. 937 //! Furthermore, each assigned literal is associated with a @link clingo_assignment_level() decision level@endlink. 938 //! There is exactly one @link clingo_assignment_decision() decision literal@endlink for each decision level greater than zero. 939 //! Assignments to all other literals on the same level are consequences implied by the current and possibly previous decisions. 940 //! Assignments on level zero are immediate consequences of the current program. 941 //! Decision levels are consecutive numbers starting with zero up to and including the @link clingo_assignment_decision_level() current decision level@endlink. 942 typedef struct clingo_assignment clingo_assignment_t; 943 944 //! @name Assignment Functions 945 //! @{ 946 947 //! Get the current decision level. 948 //! 949 //! @param[in] assignment the target assignment 950 //! @return the decision level 951 CLINGO_VISIBILITY_DEFAULT uint32_t clingo_assignment_decision_level(clingo_assignment_t const *assignment); 952 //! Get the current root level. 953 //! 954 //! Decisions levels smaller or equal to the root level are not backtracked during solving. 955 //! 956 //! @param[in] assignment the target assignment 957 //! @return the decision level 958 CLINGO_VISIBILITY_DEFAULT uint32_t clingo_assignment_root_level(clingo_assignment_t const *assignment); 959 //! Check if the given assignment is conflicting. 960 //! 961 //! @param[in] assignment the target assignment 962 //! @return whether the assignment is conflicting 963 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_conflict(clingo_assignment_t const *assignment); 964 //! Check if the given literal is part of a (partial) assignment. 965 //! 966 //! @param[in] assignment the target assignment 967 //! @param[in] literal the literal 968 //! @return whether the literal is valid 969 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_has_literal(clingo_assignment_t const *assignment, clingo_literal_t literal); 970 //! Determine the decision level of a given literal. 971 //! 972 //! @param[in] assignment the target assignment 973 //! @param[in] literal the literal 974 //! @param[out] level the resulting level 975 //! @return whether the call was successful 976 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_level(clingo_assignment_t const *assignment, clingo_literal_t literal, uint32_t *level); 977 //! Determine the decision literal given a decision level. 978 //! 979 //! @param[in] assignment the target assignment 980 //! @param[in] level the level 981 //! @param[out] literal the resulting literal 982 //! @return whether the call was successful 983 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_decision(clingo_assignment_t const *assignment, uint32_t level, clingo_literal_t *literal); 984 //! Check if a literal has a fixed truth value. 985 //! 986 //! @param[in] assignment the target assignment 987 //! @param[in] literal the literal 988 //! @param[out] is_fixed whether the literal is fixed 989 //! @return whether the call was successful 990 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_fixed(clingo_assignment_t const *assignment, clingo_literal_t literal, bool *is_fixed); 991 //! Check if a literal is true. 992 //! 993 //! @param[in] assignment the target assignment 994 //! @param[in] literal the literal 995 //! @param[out] is_true whether the literal is true 996 //! @return whether the call was successful 997 //! @see clingo_assignment_truth_value() 998 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_true(clingo_assignment_t const *assignment, clingo_literal_t literal, bool *is_true); 999 //! Check if a literal has a fixed truth value. 1000 //! 1001 //! @param[in] assignment the target assignment 1002 //! @param[in] literal the literal 1003 //! @param[out] is_false whether the literal is false 1004 //! @return whether the call was successful 1005 //! @see clingo_assignment_truth_value() 1006 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_false(clingo_assignment_t const *assignment, clingo_literal_t literal, bool *is_false); 1007 //! Determine the truth value of a given literal. 1008 //! 1009 //! @param[in] assignment the target assignment 1010 //! @param[in] literal the literal 1011 //! @param[out] value the resulting truth value 1012 //! @return whether the call was successful 1013 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_truth_value(clingo_assignment_t const *assignment, clingo_literal_t literal, clingo_truth_value_t *value); 1014 //! The number of (positive) literals in the assignment. 1015 //! 1016 //! @param[in] assignment the target 1017 //! @return the number of literals 1018 CLINGO_VISIBILITY_DEFAULT size_t clingo_assignment_size(clingo_assignment_t const *assignment); 1019 //! The (positive) literal at the given offset in the assignment. 1020 //! 1021 //! @param[in] assignment the target 1022 //! @param[in] offset the offset of the literal 1023 //! @param[out] literal the literal 1024 //! @return whether the call was successful 1025 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_at(clingo_assignment_t const *assignment, size_t offset, clingo_literal_t *literal); 1026 //! Check if the assignment is total, i.e. there are no free literal. 1027 //! 1028 //! @param[in] assignment the target 1029 //! @return wheather the assignment is total 1030 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_is_total(clingo_assignment_t const *assignment); 1031 //! Returns the number of literals in the trail, i.e., the number of assigned literals. 1032 //! 1033 //! @param[in] assignment the target 1034 //! @param[out] size the number of literals in the trail 1035 //! @return whether the call was successful 1036 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_size(clingo_assignment_t const *assignment, uint32_t *size); 1037 //! Returns the offset of the decision literal with the given decision level in 1038 //! the trail. 1039 //! 1040 //! @note Literals in the trail are ordered by decision levels, where the first 1041 //! literal with a larger level than the previous literals is a decision; the 1042 //! following literals with same level are implied by this decision literal. 1043 //! Each decision level up to and including the current decision level has a 1044 //! valid offset in the trail. 1045 //! 1046 //! @param[in] assignment the target 1047 //! @param[in] level the decision level 1048 //! @param[out] offset the offset of the decision literal 1049 //! @return whether the call was successful 1050 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_begin(clingo_assignment_t const *assignment, uint32_t level, uint32_t *offset); 1051 //! Returns the offset following the last literal with the given decision level. 1052 //! 1053 //! @note This function is the counter part to clingo_assignment_trail_begin(). 1054 //! 1055 //! @param[in] assignment the target 1056 //! @param[in] level the decision level 1057 //! @param[out] offset the offset 1058 //! @return whether the call was successful 1059 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_end(clingo_assignment_t const *assignment, uint32_t level, uint32_t *offset); 1060 //! Returns the literal at the given position in the trail. 1061 //! 1062 //! @param[in] assignment the target 1063 //! @param[in] offset the offset of the literal 1064 //! @param[out] literal the literal 1065 //! @return whether the call was successful 1066 CLINGO_VISIBILITY_DEFAULT bool clingo_assignment_trail_at(clingo_assignment_t const *assignment, uint32_t offset, clingo_literal_t *literal); 1067 1068 //! @} 1069 1070 //! Supported check modes for propagators. 1071 //! 1072 //! Note that total checks are subject to the lock when a model is found. 1073 //! This means that information from previously found models can be used to discard assignments in check calls. 1074 enum clingo_propagator_check_mode_e { 1075 clingo_propagator_check_mode_none = 0, //!< do not call @ref ::clingo_propagator::check() at all 1076 clingo_propagator_check_mode_total = 1, //!< call @ref ::clingo_propagator::check() on total assignments 1077 clingo_propagator_check_mode_fixpoint = 2, //!< call @ref ::clingo_propagator::check() on propagation fixpoints 1078 clingo_propagator_check_mode_both = 3, //!< call @ref ::clingo_propagator::check() on propagation fixpoints and total assignments 1079 }; 1080 //! Corresponding type to ::clingo_propagator_check_mode_e. 1081 typedef int clingo_propagator_check_mode_t; 1082 1083 //! Enumeration of weight_constraint_types. 1084 enum clingo_weight_constraint_type_e { 1085 clingo_weight_constraint_type_implication_left = -1, //!< the weight constraint implies the literal 1086 clingo_weight_constraint_type_implication_right = 1, //!< the literal implies the weight constraint 1087 clingo_weight_constraint_type_equivalence = 0, //!< the weight constraint is equivalent to the literal 1088 }; 1089 //! Corresponding type to ::clingo_weight_constraint_type_e. 1090 typedef int clingo_weight_constraint_type_t; 1091 1092 //! Object to initialize a user-defined propagator before each solving step. 1093 //! 1094 //! Each @link SymbolicAtoms symbolic@endlink or @link TheoryAtoms theory atom@endlink is uniquely associated with an aspif atom in form of a positive integer (@ref ::clingo_literal_t). 1095 //! Aspif literals additionally are signed to represent default negation. 1096 //! Furthermore, there are non-zero integer solver literals (also represented using @ref ::clingo_literal_t). 1097 //! There is a surjective mapping from program atoms to solver literals. 1098 //! 1099 //! All methods called during propagation use solver literals whereas clingo_symbolic_atoms_literal() and clingo_theory_atoms_atom_literal() return program literals. 1100 //! The function clingo_propagate_init_solver_literal() can be used to map program literals or @link clingo_theory_atoms_element_condition_id() condition ids@endlink to solver literals. 1101 typedef struct clingo_propagate_init clingo_propagate_init_t; 1102 1103 //! @name Initialization Functions 1104 //! @{ 1105 1106 //! Map the given program literal or condition id to its solver literal. 1107 //! 1108 //! @param[in] init the target 1109 //! @param[in] aspif_literal the aspif literal to map 1110 //! @param[out] solver_literal the resulting solver literal 1111 //! @return whether the call was successful 1112 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_solver_literal(clingo_propagate_init_t const *init, clingo_literal_t aspif_literal, clingo_literal_t *solver_literal); 1113 //! Add a watch for the solver literal in the given phase. 1114 //! 1115 //! @param[in] init the target 1116 //! @param[in] solver_literal the solver literal 1117 //! @return whether the call was successful 1118 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_watch(clingo_propagate_init_t *init, clingo_literal_t solver_literal); 1119 //! Add a watch for the solver literal in the given phase to the given solver thread. 1120 //! 1121 //! @param[in] init the target 1122 //! @param[in] solver_literal the solver literal 1123 //! @param[in] thread_id the id of the solver thread 1124 //! @return whether the call was successful 1125 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_watch_to_thread(clingo_propagate_init_t *init, clingo_literal_t solver_literal, clingo_id_t thread_id); 1126 //! Remove the watch for the solver literal in the given phase. 1127 //! 1128 //! @param[in] init the target 1129 //! @param[in] solver_literal the solver literal 1130 //! @return whether the call was successful 1131 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_remove_watch(clingo_propagate_init_t *init, clingo_literal_t solver_literal); 1132 //! Remove the watch for the solver literal in the given phase from the given solver thread. 1133 //! 1134 //! @param[in] init the target 1135 //! @param[in] solver_literal the solver literal 1136 //! @param[in] thread_id the id of the solver thread 1137 //! @return whether the call was successful 1138 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_remove_watch_from_thread(clingo_propagate_init_t *init, clingo_literal_t solver_literal, uint32_t thread_id); 1139 //! Freeze the given solver literal. 1140 //! 1141 //! Any solver literal that is not frozen is subject to simplification and might be removed in a preprocessing step after propagator initialization. 1142 //! A propagator should freeze all literals over which it might add clauses during propagation. 1143 //! Note that any watched literal is automatically frozen and that it does not matter which phase of the literal is frozen. 1144 //! 1145 //! @param[in] init the target 1146 //! @param[in] solver_literal the solver literal 1147 //! @return whether the call was successful 1148 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_freeze_literal(clingo_propagate_init_t *init, clingo_literal_t solver_literal); 1149 //! Get an object to inspect the symbolic atoms. 1150 //! 1151 //! @param[in] init the target 1152 //! @param[out] atoms the resulting object 1153 //! @return whether the call was successful 1154 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_symbolic_atoms(clingo_propagate_init_t const *init, clingo_symbolic_atoms_t const **atoms); 1155 //! Get an object to inspect the theory atoms. 1156 //! 1157 //! @param[in] init the target 1158 //! @param[out] atoms the resulting object 1159 //! @return whether the call was successful 1160 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_theory_atoms(clingo_propagate_init_t const *init, clingo_theory_atoms_t const **atoms); 1161 //! Get the number of threads used in subsequent solving. 1162 //! 1163 //! @param[in] init the target 1164 //! @return the number of threads 1165 //! @see clingo_propagate_control_thread_id() 1166 CLINGO_VISIBILITY_DEFAULT int clingo_propagate_init_number_of_threads(clingo_propagate_init_t const *init); 1167 //! Configure when to call the check method of the propagator. 1168 //! 1169 //! @param[in] init the target 1170 //! @param[in] mode bitmask when to call the propagator 1171 //! @see @ref ::clingo_propagator::check() 1172 CLINGO_VISIBILITY_DEFAULT void clingo_propagate_init_set_check_mode(clingo_propagate_init_t *init, clingo_propagator_check_mode_t mode); 1173 //! Get the current check mode of the propagator. 1174 //! 1175 //! @param[in] init the target 1176 //! @return bitmask when to call the propagator 1177 //! @see clingo_propagate_init_set_check_mode() 1178 CLINGO_VISIBILITY_DEFAULT clingo_propagator_check_mode_t clingo_propagate_init_get_check_mode(clingo_propagate_init_t const *init); 1179 //! Get the top level assignment solver. 1180 //! 1181 //! @param[in] init the target 1182 //! @return the assignment 1183 CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const *clingo_propagate_init_assignment(clingo_propagate_init_t const *init); 1184 //! Add a literal to the solver. 1185 //! 1186 //! To be able to use the variable in clauses during propagation or add watches to it, it has to be frozen. 1187 //! Otherwise, it might be removed during preprocessing. 1188 //! 1189 //! @attention If varibales were added, subsequent calls to functions adding constraints or ::clingo_propagate_init_propagate() are expensive. 1190 //! It is best to add varables in batches. 1191 //! 1192 //! @param[in] init the target 1193 //! @param[in] freeze whether to freeze the literal 1194 //! @param[out] result the added literal 1195 //! @return whether the call was successful; might set one of the following error codes: 1196 //! - ::clingo_error_bad_alloc 1197 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_literal(clingo_propagate_init_t *init, bool freeze, clingo_literal_t *result); 1198 //! Add the given clause to the solver. 1199 //! 1200 //! @attention No further calls on the init object or functions on the assignment should be called when the result of this method is false. 1201 //! 1202 //! @param[in] init the target 1203 //! @param[in] clause the clause to add 1204 //! @param[in] size the size of the clause 1205 //! @param[out] result result indicating whether the problem became unsatisfiable 1206 //! @return whether the call was successful; might set one of the following error codes: 1207 //! - ::clingo_error_bad_alloc 1208 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_clause(clingo_propagate_init_t *init, clingo_literal_t const *clause, size_t size, bool *result); 1209 //! Add the given weight constraint to the solver. 1210 //! 1211 //! This function adds a constraint of form `literal <=> { lit=weight | (lit, weight) in literals } >= bound` to the solver. 1212 //! Depending on the type the `<=>` connective can be either a left implication, right implication, or equivalence. 1213 //! 1214 //! @attention No further calls on the init object or functions on the assignment should be called when the result of this method is false. 1215 //! 1216 //! @param[in] init the target 1217 //! @param[in] literal the literal of the constraint 1218 //! @param[in] literals the weighted literals 1219 //! @param[in] size the number of weighted literals 1220 //! @param[in] bound the bound of the constraint 1221 //! @param[in] type the type of the weight constraint 1222 //! @param[in] compare_equal if true compare equal instead of less than equal 1223 //! @param[out] result result indicating whether the problem became unsatisfiable 1224 //! @return whether the call was successful; might set one of the following error codes: 1225 //! - ::clingo_error_bad_alloc 1226 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_weight_constraint(clingo_propagate_init_t *init, clingo_literal_t literal, clingo_weighted_literal_t const *literals, size_t size, clingo_weight_t bound, clingo_weight_constraint_type_t type, bool compare_equal, bool *result); 1227 //! Add the given literal to minimize to the solver. 1228 //! 1229 //! This corresponds to a weak constraint of form `:~ literal. [weight@priority]`. 1230 //! 1231 //! @param[in] init the target 1232 //! @param[in] literal the literal to minimize 1233 //! @param[in] weight the weight of the literal 1234 //! @param[in] priority the priority of the literal 1235 //! @return whether the call was successful; might set one of the following error codes: 1236 //! - ::clingo_error_bad_alloc 1237 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_add_minimize(clingo_propagate_init_t *init, clingo_literal_t literal, clingo_weight_t weight, clingo_weight_t priority); 1238 //! Propagates consequences of the underlying problem excluding registered propagators. 1239 //! 1240 //! @note The function has no effect if SAT-preprocessing is enabled. 1241 //! @attention No further calls on the init object or functions on the assignment should be called when the result of this method is false. 1242 //! 1243 //! @param[in] init the target 1244 //! @param[out] result result indicating whether the problem became unsatisfiable 1245 //! @return whether the call was successful; might set one of the following error codes: 1246 //! - ::clingo_error_bad_alloc 1247 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_init_propagate(clingo_propagate_init_t *init, bool *result); 1248 1249 //! @} 1250 1251 //! Enumeration of clause types determining the lifetime of a clause. 1252 //! 1253 //! Clauses in the solver are either cleaned up based on a configurable deletion policy or at the end of a solving step. 1254 //! The values of this enumeration determine if a clause is subject to one of the above deletion strategies. 1255 enum clingo_clause_type_e { 1256 clingo_clause_type_learnt = 0, //!< clause is subject to the solvers deletion policy 1257 clingo_clause_type_static = 1, //!< clause is not subject to the solvers deletion policy 1258 clingo_clause_type_volatile = 2, //!< like ::clingo_clause_type_learnt but the clause is deleted after a solving step 1259 clingo_clause_type_volatile_static = 3 //!< like ::clingo_clause_type_static but the clause is deleted after a solving step 1260 }; 1261 //! Corresponding type to ::clingo_clause_type_e. 1262 typedef int clingo_clause_type_t; 1263 1264 //! This object can be used to add clauses and propagate literals while solving. 1265 typedef struct clingo_propagate_control clingo_propagate_control_t; 1266 1267 //! @name Propagation Functions 1268 //! @{ 1269 1270 //! Get the id of the underlying solver thread. 1271 //! 1272 //! Thread ids are consecutive numbers starting with zero. 1273 //! 1274 //! @param[in] control the target 1275 //! @return the thread id 1276 CLINGO_VISIBILITY_DEFAULT clingo_id_t clingo_propagate_control_thread_id(clingo_propagate_control_t const *control); 1277 //! Get the assignment associated with the underlying solver. 1278 //! 1279 //! @param[in] control the target 1280 //! @return the assignment 1281 CLINGO_VISIBILITY_DEFAULT clingo_assignment_t const *clingo_propagate_control_assignment(clingo_propagate_control_t const *control); 1282 //! Adds a new volatile literal to the underlying solver thread. 1283 //! 1284 //! @attention The literal is only valid within the current solving step and solver thread. 1285 //! All volatile literals and clauses involving a volatile literal are deleted after the current search. 1286 //! 1287 //! @param[in] control the target 1288 //! @param[out] result the (positive) solver literal 1289 //! @return whether the call was successful; might set one of the following error codes: 1290 //! - ::clingo_error_bad_alloc 1291 //! - ::clingo_error_logic if the assignment is conflicting 1292 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_literal(clingo_propagate_control_t *control, clingo_literal_t *result); 1293 //! Add a watch for the solver literal in the given phase. 1294 //! 1295 //! @note Unlike @ref clingo_propagate_init_add_watch() this does not add a watch to all solver threads but just the current one. 1296 //! 1297 //! @param[in] control the target 1298 //! @param[in] literal the literal to watch 1299 //! @return whether the call was successful; might set one of the following error codes: 1300 //! - ::clingo_error_bad_alloc 1301 //! - ::clingo_error_logic if the literal is invalid 1302 //! @see clingo_propagate_control_remove_watch() 1303 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_watch(clingo_propagate_control_t *control, clingo_literal_t literal); 1304 //! Check whether a literal is watched in the current solver thread. 1305 //! 1306 //! @param[in] control the target 1307 //! @param[in] literal the literal to check 1308 //! 1309 //! @return whether the literal is watched 1310 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_has_watch(clingo_propagate_control_t const *control, clingo_literal_t literal); 1311 //! Removes the watch (if any) for the given solver literal. 1312 //! 1313 //! @note Similar to @ref clingo_propagate_init_add_watch() this just removes the watch in the current solver thread. 1314 //! 1315 //! @param[in] control the target 1316 //! @param[in] literal the literal to remove 1317 CLINGO_VISIBILITY_DEFAULT void clingo_propagate_control_remove_watch(clingo_propagate_control_t *control, clingo_literal_t literal); 1318 //! Add the given clause to the solver. 1319 //! 1320 //! This method sets its result to false if the current propagation must be stopped for the solver to backtrack. 1321 //! 1322 //! @attention No further calls on the control object or functions on the assignment should be called when the result of this method is false. 1323 //! 1324 //! @param[in] control the target 1325 //! @param[in] clause the clause to add 1326 //! @param[in] size the size of the clause 1327 //! @param[in] type the clause type determining its lifetime 1328 //! @param[out] result result indicating whether propagation has to be stopped 1329 //! @return whether the call was successful; might set one of the following error codes: 1330 //! - ::clingo_error_bad_alloc 1331 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_add_clause(clingo_propagate_control_t *control, clingo_literal_t const *clause, size_t size, clingo_clause_type_t type, bool *result); 1332 //! Propagate implied literals (resulting from added clauses). 1333 //! 1334 //! This method sets its result to false if the current propagation must be stopped for the solver to backtrack. 1335 //! 1336 //! @attention No further calls on the control object or functions on the assignment should be called when the result of this method is false. 1337 //! 1338 //! @param[in] control the target 1339 //! @param[out] result result indicating whether propagation has to be stopped 1340 //! @return whether the call was successful; might set one of the following error codes: 1341 //! - ::clingo_error_bad_alloc 1342 CLINGO_VISIBILITY_DEFAULT bool clingo_propagate_control_propagate(clingo_propagate_control_t *control, bool *result); 1343 1344 //! @} 1345 1346 //! Typedef for @ref ::clingo_propagator::init(). 1347 typedef bool (*clingo_propagator_init_callback_t) (clingo_propagate_init_t *, void *); 1348 1349 //! Typedef for @ref ::clingo_propagator::propagate(). 1350 typedef bool (*clingo_propagator_propagate_callback_t) (clingo_propagate_control_t *, clingo_literal_t const *, size_t, void *); 1351 1352 //! Typedef for @ref ::clingo_propagator::undo(). 1353 typedef void (*clingo_propagator_undo_callback_t) (clingo_propagate_control_t const *, clingo_literal_t const *, size_t, void *); 1354 1355 //! Typedef for @ref ::clingo_propagator::check(). 1356 typedef bool (*clingo_propagator_check_callback_t) (clingo_propagate_control_t *, void *); 1357 1358 //! An instance of this struct has to be registered with a solver to implement a custom propagator. 1359 //! 1360 //! Not all callbacks have to be implemented and can be set to NULL if not needed. 1361 //! @see Propagator 1362 typedef struct clingo_propagator { 1363 //! This function is called once before each solving step. 1364 //! It is used to map relevant program literals to solver literals, add watches for solver literals, and initialize the data structures used during propagation. 1365 //! 1366 //! @note This is the last point to access symbolic and theory atoms. 1367 //! Once the search has started, they are no longer accessible. 1368 //! 1369 //! @param[in] init initizialization object 1370 //! @param[in] data user data for the callback 1371 //! @return whether the call was successful 1372 //! @see ::clingo_propagator_init_callback_t 1373 bool (*init) (clingo_propagate_init_t *init, void *data); 1374 //! Can be used to propagate solver literals given a @link clingo_assignment_t partial assignment@endlink. 1375 //! 1376 //! Called during propagation with a non-empty array of @link clingo_propagate_init_add_watch() watched solver literals@endlink 1377 //! that have been assigned to true since the last call to either propagate, undo, (or the start of the search) - the change set. 1378 //! Only watched solver literals are contained in the change set. 1379 //! Each literal in the change set is true w.r.t. the current @link clingo_assignment_t assignment@endlink. 1380 //! @ref clingo_propagate_control_add_clause() can be used to add clauses. 1381 //! If a clause is unit resulting, it can be propagated using @ref clingo_propagate_control_propagate(). 1382 //! If the result of either of the two methods is false, the propagate function must return immediately. 1383 //! 1384 //! The following snippet shows how to use the methods to add clauses and propagate consequences within the callback. 1385 //! The important point is to return true (true to indicate there was no error) if the result of either of the methods is false. 1386 //! ~~~~~~~~~~~~~~~{.c} 1387 //! bool result; 1388 //! clingo_literal_t clause[] = { ... }; 1389 //! 1390 //! // add a clause 1391 //! if (!clingo_propagate_control_add_clause(control, clause, clingo_clause_type_learnt, &result) { return false; } 1392 //! if (!result) { return true; } 1393 //! // propagate its consequences 1394 //! if (!clingo_propagate_control_propagate(control, &result) { return false; } 1395 //! if (!result) { return true; } 1396 //! 1397 //! // add further clauses and propagate them 1398 //! ... 1399 //! 1400 //! return true; 1401 //! ~~~~~~~~~~~~~~~ 1402 //! 1403 //! @note 1404 //! This function can be called from different solving threads. 1405 //! Each thread has its own assignment and id, which can be obtained using @ref clingo_propagate_control_thread_id(). 1406 //! 1407 //! @param[in] control control object for the target solver 1408 //! @param[in] changes the change set 1409 //! @param[in] size the size of the change set 1410 //! @param[in] data user data for the callback 1411 //! @return whether the call was successful 1412 //! @see ::clingo_propagator_propagate_callback_t 1413 bool (*propagate) (clingo_propagate_control_t *control, clingo_literal_t const *changes, size_t size, void *data); 1414 //! Called whenever a solver undoes assignments to watched solver literals. 1415 //! 1416 //! This callback is meant to update assignment dependent state in the propagator. 1417 //! 1418 //! @note No clauses must be propagated in this callback and no errors should be set. 1419 //! 1420 //! @param[in] control control object for the target solver 1421 //! @param[in] changes the change set 1422 //! @param[in] size the size of the change set 1423 //! @param[in] data user data for the callback 1424 //! @return whether the call was successful 1425 //! @see ::clingo_propagator_undo_callback_t 1426 void (*undo) (clingo_propagate_control_t const *control, clingo_literal_t const *changes, size_t size, void *data); 1427 //! This function is similar to @ref clingo_propagate_control_propagate() but is called without a change set on propagation fixpoints. 1428 //! 1429 //! When exactly this function is called, can be configured using the @ref clingo_propagate_init_set_check_mode() function. 1430 //! 1431 //! @note This function is called even if no watches have been added. 1432 //! 1433 //! @param[in] control control object for the target solver 1434 //! @param[in] data user data for the callback 1435 //! @return whether the call was successful 1436 //! @see ::clingo_propagator_check_callback_t 1437 bool (*check) (clingo_propagate_control_t *control, void *data); 1438 //! This function allows a propagator to implement domain-specific heuristics. 1439 //! 1440 //! It is called whenever propagation reaches a fixed point and 1441 //! should return a free solver literal that is to be assigned true. 1442 //! In case multiple propagators are registered, 1443 //! this function can return 0 to let a propagator registered later make a decision. 1444 //! If all propagators return 0, then the fallback literal is 1445 //! 1446 //! @param[in] thread_id the solver's thread id 1447 //! @param[in] assignment the assignment of the solver 1448 //! @param[in] fallback the literal choosen by the solver's heuristic 1449 //! @param[out] decision the literal to make true 1450 //! @return whether the call was successful 1451 bool (*decide) (clingo_id_t thread_id, clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data, clingo_literal_t *decision); 1452 } clingo_propagator_t; 1453 1454 //! @} 1455 1456 // {{{1 backend 1457 1458 //! @example backend.c 1459 //! The example shows how to used the backend to extend a grounded program. 1460 //! 1461 //! ## Output ## 1462 //! 1463 //! ~~~~~~~~~~~~ 1464 //! ./backend 0 1465 //! Model: a b 1466 //! Model: a b c 1467 //! Model: 1468 //! Model: a 1469 //! Model: b 1470 //! ~~~~~~~~~~~~ 1471 //! 1472 //! ## Code ## 1473 1474 //! @defgroup ProgramBuilder Program Building 1475 //! Add non-ground program representations (ASTs) to logic programs or extend the ground (aspif) program. 1476 //! @ingroup Control 1477 //! 1478 //! For an example about ground logic programs, see @ref backend.c. 1479 //! For an example about non-ground logic programs, see @ref ast.c and the @ref AST module. 1480 1481 //! @addtogroup ProgramBuilder 1482 //! @{ 1483 1484 //! Enumeration of different heuristic modifiers. 1485 //! @ingroup ProgramInspection 1486 enum clingo_heuristic_type_e { 1487 clingo_heuristic_type_level = 0, //!< set the level of an atom 1488 clingo_heuristic_type_sign = 1, //!< configure which sign to chose for an atom 1489 clingo_heuristic_type_factor = 2, //!< modify VSIDS factor of an atom 1490 clingo_heuristic_type_init = 3, //!< modify the initial VSIDS score of an atom 1491 clingo_heuristic_type_true = 4, //!< set the level of an atom and choose a positive sign 1492 clingo_heuristic_type_false = 5 //!< set the level of an atom and choose a negative sign 1493 }; 1494 //! Corresponding type to ::clingo_heuristic_type_e. 1495 //! @ingroup ProgramInspection 1496 typedef int clingo_heuristic_type_t; 1497 1498 //! Enumeration of different external statements. 1499 //! @ingroup ProgramInspection 1500 enum clingo_external_type_e { 1501 clingo_external_type_free = 0, //!< allow an external to be assigned freely 1502 clingo_external_type_true = 1, //!< assign an external to true 1503 clingo_external_type_false = 2, //!< assign an external to false 1504 clingo_external_type_release = 3, //!< no longer treat an atom as external 1505 }; 1506 //! Corresponding type to ::clingo_external_type_e. 1507 //! @ingroup ProgramInspection 1508 typedef int clingo_external_type_t; 1509 1510 //! Handle to the backend to add directives in aspif format. 1511 typedef struct clingo_backend clingo_backend_t; 1512 1513 //! Prepare the backend for usage. 1514 //! 1515 //! @param[in] backend the target backend 1516 //! @return whether the call was successful; might set one of the following error codes: 1517 //! - ::clingo_error_bad_alloc 1518 //! - ::clingo_error_runtime 1519 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_begin(clingo_backend_t *backend); 1520 //! Finalize the backend after using it. 1521 //! 1522 //! @param[in] backend the target backend 1523 //! @return whether the call was successful; might set one of the following error codes: 1524 //! - ::clingo_error_bad_alloc 1525 //! - ::clingo_error_runtime 1526 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_end(clingo_backend_t *backend); 1527 //! Add a rule to the program. 1528 //! 1529 //! @param[in] backend the target backend 1530 //! @param[in] choice determines if the head is a choice or a disjunction 1531 //! @param[in] head the head atoms 1532 //! @param[in] head_size the number of atoms in the head 1533 //! @param[in] body the body literals 1534 //! @param[in] body_size the number of literals in the body 1535 //! @return whether the call was successful; might set one of the following error codes: 1536 //! - ::clingo_error_bad_alloc 1537 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_rule(clingo_backend_t *backend, bool choice, clingo_atom_t const *head, size_t head_size, clingo_literal_t const *body, size_t body_size); 1538 //! Add a weight rule to the program. 1539 //! 1540 //! @attention All weights and the lower bound must be positive. 1541 //! @param[in] backend the target backend 1542 //! @param[in] choice determines if the head is a choice or a disjunction 1543 //! @param[in] head the head atoms 1544 //! @param[in] head_size the number of atoms in the head 1545 //! @param[in] lower_bound the lower bound of the weight rule 1546 //! @param[in] body the weighted body literals 1547 //! @param[in] body_size the number of weighted literals in the body 1548 //! @return whether the call was successful; might set one of the following error codes: 1549 //! - ::clingo_error_bad_alloc 1550 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_weight_rule(clingo_backend_t *backend, bool choice, clingo_atom_t const *head, size_t head_size, clingo_weight_t lower_bound, clingo_weighted_literal_t const *body, size_t body_size); 1551 //! Add a minimize constraint (or weak constraint) to the program. 1552 //! 1553 //! @param[in] backend the target backend 1554 //! @param[in] priority the priority of the constraint 1555 //! @param[in] literals the weighted literals whose sum to minimize 1556 //! @param[in] size the number of weighted literals 1557 //! @return whether the call was successful; might set one of the following error codes: 1558 //! - ::clingo_error_bad_alloc 1559 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_minimize(clingo_backend_t *backend, clingo_weight_t priority, clingo_weighted_literal_t const* literals, size_t size); 1560 //! Add a projection directive. 1561 //! 1562 //! @param[in] backend the target backend 1563 //! @param[in] atoms the atoms to project on 1564 //! @param[in] size the number of atoms 1565 //! @return whether the call was successful; might set one of the following error codes: 1566 //! - ::clingo_error_bad_alloc 1567 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_project(clingo_backend_t *backend, clingo_atom_t const *atoms, size_t size); 1568 //! Add an external statement. 1569 //! 1570 //! @param[in] backend the target backend 1571 //! @param[in] atom the external atom 1572 //! @param[in] type the type of the external statement 1573 //! @return whether the call was successful; might set one of the following error codes: 1574 //! - ::clingo_error_bad_alloc 1575 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_external(clingo_backend_t *backend, clingo_atom_t atom, clingo_external_type_t type); 1576 //! Add an assumption directive. 1577 //! 1578 //! @param[in] backend the target backend 1579 //! @param[in] literals the literals to assume (positive literals are true and negative literals false for the next solve call) 1580 //! @param[in] size the number of atoms 1581 //! @return whether the call was successful; might set one of the following error codes: 1582 //! - ::clingo_error_bad_alloc 1583 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_assume(clingo_backend_t *backend, clingo_literal_t const *literals, size_t size); 1584 //! Add an heuristic directive. 1585 //! 1586 //! @param[in] backend the target backend 1587 //! @param[in] atom the target atom 1588 //! @param[in] type the type of the heuristic modification 1589 //! @param[in] bias the heuristic bias 1590 //! @param[in] priority the heuristic priority 1591 //! @param[in] condition the condition under which to apply the heuristic modification 1592 //! @param[in] size the number of atoms in the condition 1593 //! @return whether the call was successful; might set one of the following error codes: 1594 //! - ::clingo_error_bad_alloc 1595 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_heuristic(clingo_backend_t *backend, clingo_atom_t atom, clingo_heuristic_type_t type, int bias, unsigned priority, clingo_literal_t const *condition, size_t size); 1596 //! Add an edge directive. 1597 //! 1598 //! @param[in] backend the target backend 1599 //! @param[in] node_u the start vertex of the edge 1600 //! @param[in] node_v the end vertex of the edge 1601 //! @param[in] condition the condition under which the edge is part of the graph 1602 //! @param[in] size the number of atoms in the condition 1603 //! @return whether the call was successful; might set one of the following error codes: 1604 //! - ::clingo_error_bad_alloc 1605 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_acyc_edge(clingo_backend_t *backend, int node_u, int node_v, clingo_literal_t const *condition, size_t size); 1606 //! Get a fresh atom to be used in aspif directives. 1607 //! 1608 //! @param[in] backend the target backend 1609 //! @param[in] symbol optional symbol to associate the atom with 1610 //! @param[out] atom the resulting atom 1611 //! @return whether the call was successful 1612 CLINGO_VISIBILITY_DEFAULT bool clingo_backend_add_atom(clingo_backend_t *backend, clingo_symbol_t *symbol, clingo_atom_t *atom); 1613 1614 //! @} 1615 1616 // {{{1 configuration 1617 1618 //! @example configuration.c 1619 //! The example shows how to configure the solver. 1620 //! 1621 //! @note It is also possible to loop over all configuration entries. 1622 //! This can be done in a similar fashion as in the @ref statistics.c example. 1623 //! But note that, unlike with statistics entries, a configuration entry can have more than one type. 1624 //! 1625 //! ## Output ## 1626 //! 1627 //! ~~~~~~~~ 1628 //! ./configuration 1629 //! Model: a 1630 //! Model: b 1631 //! ~~~~~~~~ 1632 //! 1633 //! ## Code ## 1634 1635 //! @defgroup Configuration Solver Configuration 1636 //! Configuration of search and enumeration algorithms. 1637 //! 1638 //! Entries in a configuration are organized hierarchically. 1639 //! Subentries are either accessed by name for map entries or by offset for array entries. 1640 //! Value entries have a string value that can be inspected or modified. 1641 //! 1642 //! For an example, see @ref configuration.c. 1643 //! @ingroup Control 1644 1645 //! @addtogroup Configuration 1646 //! @{ 1647 1648 //! Enumeration for entries of the configuration. 1649 enum clingo_configuration_type_e { 1650 clingo_configuration_type_value = 1, //!< the entry is a (string) value 1651 clingo_configuration_type_array = 2, //!< the entry is an array 1652 clingo_configuration_type_map = 4 //!< the entry is a map 1653 }; 1654 //! Bitset for values of type ::clingo_configuration_type_e. 1655 typedef unsigned clingo_configuration_type_bitset_t; 1656 1657 //! Handle for to the solver configuration. 1658 typedef struct clingo_configuration clingo_configuration_t; 1659 1660 //! Get the root key of the configuration. 1661 //! 1662 //! @param[in] configuration the target configuration 1663 //! @param[out] key the root key 1664 //! @return whether the call was successful 1665 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_root(clingo_configuration_t const *configuration, clingo_id_t *key); 1666 //! Get the type of a key. 1667 //! 1668 //! @note The type is bitset, an entry can have multiple (but at least one) type. 1669 //! 1670 //! @param[in] configuration the target configuration 1671 //! @param[in] key the key 1672 //! @param[out] type the resulting type 1673 //! @return whether the call was successful 1674 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_type(clingo_configuration_t const *configuration, clingo_id_t key, clingo_configuration_type_bitset_t *type); 1675 //! Get the description of an entry. 1676 //! 1677 //! @param[in] configuration the target configuration 1678 //! @param[in] key the key 1679 //! @param[out] description the description 1680 //! @return whether the call was successful 1681 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_description(clingo_configuration_t const *configuration, clingo_id_t key, char const **description); 1682 1683 //! @name Functions to access arrays 1684 //! @{ 1685 1686 //! Get the size of an array entry. 1687 //! 1688 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_array. 1689 //! @param[in] configuration the target configuration 1690 //! @param[in] key the key 1691 //! @param[out] size the resulting size 1692 //! @return whether the call was successful 1693 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_array_size(clingo_configuration_t const *configuration, clingo_id_t key, size_t *size); 1694 //! Get the subkey at the given offset of an array entry. 1695 //! 1696 //! @note Some array entries, like fore example the solver configuration, can be accessed past there actual size to add subentries. 1697 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_array. 1698 //! @param[in] configuration the target configuration 1699 //! @param[in] key the key 1700 //! @param[in] offset the offset in the array 1701 //! @param[out] subkey the resulting subkey 1702 //! @return whether the call was successful 1703 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_array_at(clingo_configuration_t const *configuration, clingo_id_t key, size_t offset, clingo_id_t *subkey); 1704 //! @} 1705 1706 //! @name Functions to access maps 1707 //! @{ 1708 1709 //! Get the number of subkeys of a map entry. 1710 //! 1711 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_map. 1712 //! @param[in] configuration the target configuration 1713 //! @param[in] key the key 1714 //! @param[out] size the resulting number 1715 //! @return whether the call was successful 1716 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_size(clingo_configuration_t const *configuration, clingo_id_t key, size_t* size); 1717 //! Query whether the map has a key. 1718 //! 1719 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_map. 1720 //! @note Multiple levels can be looked up by concatenating keys with a period. 1721 //! @param[in] configuration the target configuration 1722 //! @param[in] key the key 1723 //! @param[in] name the name to lookup the subkey 1724 //! @param[out] result whether the key is in the map 1725 //! @return whether the call was successful 1726 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_has_subkey(clingo_configuration_t const *configuration, clingo_id_t key, char const *name, bool *result); 1727 //! Get the name associated with the offset-th subkey. 1728 //! 1729 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_map. 1730 //! @param[in] configuration the target configuration 1731 //! @param[in] key the key 1732 //! @param[in] offset the offset of the name 1733 //! @param[out] name the resulting name 1734 //! @return whether the call was successful 1735 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_subkey_name(clingo_configuration_t const *configuration, clingo_id_t key, size_t offset, char const **name); 1736 //! Lookup a subkey under the given name. 1737 //! 1738 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_map. 1739 //! @note Multiple levels can be looked up by concatenating keys with a period. 1740 //! @param[in] configuration the target configuration 1741 //! @param[in] key the key 1742 //! @param[in] name the name to lookup the subkey 1743 //! @param[out] subkey the resulting subkey 1744 //! @return whether the call was successful 1745 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_map_at(clingo_configuration_t const *configuration, clingo_id_t key, char const *name, clingo_id_t* subkey); 1746 //! @} 1747 1748 //! @name Functions to access values 1749 //! @{ 1750 1751 //! Check whether a entry has a value. 1752 //! 1753 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_value. 1754 //! @param[in] configuration the target configuration 1755 //! @param[in] key the key 1756 //! @param[out] assigned whether the entry has a value 1757 //! @return whether the call was successful 1758 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_value_is_assigned(clingo_configuration_t const *configuration, clingo_id_t key, bool *assigned); 1759 //! Get the size of the string value of the given entry. 1760 //! 1761 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_value. 1762 //! @param[in] configuration the target configuration 1763 //! @param[in] key the key 1764 //! @param[out] size the resulting size 1765 //! @return whether the call was successful 1766 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_value_get_size(clingo_configuration_t const *configuration, clingo_id_t key, size_t *size); 1767 //! Get the string value of the given entry. 1768 //! 1769 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_value. 1770 //! @pre The given size must be larger or equal to size of the value. 1771 //! @param[in] configuration the target configuration 1772 //! @param[in] key the key 1773 //! @param[out] value the resulting string value 1774 //! @param[in] size the size of the given char array 1775 //! @return whether the call was successful 1776 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_value_get(clingo_configuration_t const *configuration, clingo_id_t key, char *value, size_t size); 1777 //! Set the value of an entry. 1778 //! 1779 //! @pre The @link clingo_configuration_type() type@endlink of the entry must be @ref ::clingo_configuration_type_value. 1780 //! @param[in] configuration the target configuration 1781 //! @param[in] key the key 1782 //! @param[in] value the value to set 1783 //! @return whether the call was successful 1784 CLINGO_VISIBILITY_DEFAULT bool clingo_configuration_value_set(clingo_configuration_t *configuration, clingo_id_t key, char const *value); 1785 //! @} 1786 1787 //! @} 1788 1789 // {{{1 statistics 1790 1791 //! @example statistics.c 1792 //! The example shows how to inspect statistics. 1793 //! 1794 //! ## Output ## 1795 //! 1796 //! ~~~~~~~~ 1797 //! ./statistics 0 1798 //! Model: a 1799 //! Model: b 1800 //! problem: 1801 //! lp: 1802 //! atoms: 1803 //! 2 1804 //! atoms_aux: 1805 //! 0 1806 //! ... 1807 //! solving: 1808 //! ... 1809 //! summary: 1810 //! ... 1811 //! accu: 1812 //! times: 1813 //! ... 1814 //! models: 1815 //! ... 1816 //! solving: 1817 //! ... 1818 //! ~~~~~~~~ 1819 //! 1820 //! ## Code ## 1821 1822 //! @defgroup Statistics Statistics 1823 //! Inspect search and problem statistics. 1824 //! 1825 //! @ingroup Control 1826 //! For an example, see @ref statistics.c. 1827 1828 //! @addtogroup Statistics 1829 //! @{ 1830 1831 //! Enumeration for entries of the statistics. 1832 enum clingo_statistics_type_e { 1833 clingo_statistics_type_empty = 0, //!< the entry is invalid (has neither of the types below) 1834 clingo_statistics_type_value = 1, //!< the entry is a (double) value 1835 clingo_statistics_type_array = 2, //!< the entry is an array 1836 clingo_statistics_type_map = 3 //!< the entry is a map 1837 }; 1838 //! Corresponding type to ::clingo_statistics_type. 1839 typedef int clingo_statistics_type_t; 1840 1841 //! Handle for the solver statistics. 1842 typedef struct clingo_statistic clingo_statistics_t; 1843 1844 //! Get the root key of the statistics. 1845 //! 1846 //! @param[in] statistics the target statistics 1847 //! @param[out] key the root key 1848 //! @return whether the call was successful 1849 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_root(clingo_statistics_t const *statistics, uint64_t *key); 1850 //! Get the type of a key. 1851 //! 1852 //! @param[in] statistics the target statistics 1853 //! @param[in] key the key 1854 //! @param[out] type the resulting type 1855 //! @return whether the call was successful 1856 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_type(clingo_statistics_t const *statistics, uint64_t key, clingo_statistics_type_t *type); 1857 1858 //! @name Functions to access arrays 1859 //! @{ 1860 1861 //! Get the size of an array entry. 1862 //! 1863 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_array. 1864 //! @param[in] statistics the target statistics 1865 //! @param[in] key the key 1866 //! @param[out] size the resulting size 1867 //! @return whether the call was successful 1868 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_array_size(clingo_statistics_t const *statistics, uint64_t key, size_t *size); 1869 //! Get the subkey at the given offset of an array entry. 1870 //! 1871 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_array. 1872 //! @param[in] statistics the target statistics 1873 //! @param[in] key the key 1874 //! @param[in] offset the offset in the array 1875 //! @param[out] subkey the resulting subkey 1876 //! @return whether the call was successful 1877 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_array_at(clingo_statistics_t const *statistics, uint64_t key, size_t offset, uint64_t *subkey); 1878 //! Create the subkey at the end of an array entry. 1879 //! 1880 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_array. 1881 //! @param[in] statistics the target statistics 1882 //! @param[in] key the key 1883 //! @param[in] type the type of the new subkey 1884 //! @param[out] subkey the resulting subkey 1885 //! @return whether the call was successful 1886 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_array_push(clingo_statistics_t *statistics, uint64_t key, clingo_statistics_type_t type, uint64_t *subkey); 1887 //! @} 1888 1889 //! @name Functions to access maps 1890 //! @{ 1891 1892 //! Get the number of subkeys of a map entry. 1893 //! 1894 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_map. 1895 //! @param[in] statistics the target statistics 1896 //! @param[in] key the key 1897 //! @param[out] size the resulting number 1898 //! @return whether the call was successful 1899 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_map_size(clingo_statistics_t const *statistics, uint64_t key, size_t *size); 1900 //! Test if the given map contains a specific subkey. 1901 //! 1902 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_map. 1903 //! @param[in] statistics the target statistics 1904 //! @param[in] key the key 1905 //! @param[in] name name of the subkey 1906 //! @param[out] result true if the map has a subkey with the given name 1907 //! @return whether the call was successful 1908 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_map_has_subkey(clingo_statistics_t const *statistics, uint64_t key, char const *name, bool* result); 1909 //! Get the name associated with the offset-th subkey. 1910 //! 1911 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_map. 1912 //! @param[in] statistics the target statistics 1913 //! @param[in] key the key 1914 //! @param[in] offset the offset of the name 1915 //! @param[out] name the resulting name 1916 //! @return whether the call was successful 1917 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_map_subkey_name(clingo_statistics_t const *statistics, uint64_t key, size_t offset, char const **name); 1918 //! Lookup a subkey under the given name. 1919 //! 1920 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_map. 1921 //! @note Multiple levels can be looked up by concatenating keys with a period. 1922 //! @param[in] statistics the target statistics 1923 //! @param[in] key the key 1924 //! @param[in] name the name to lookup the subkey 1925 //! @param[out] subkey the resulting subkey 1926 //! @return whether the call was successful 1927 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_map_at(clingo_statistics_t const *statistics, uint64_t key, char const *name, uint64_t *subkey); 1928 //! Add a subkey with the given name. 1929 //! 1930 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_map. 1931 //! @param[in] statistics the target statistics 1932 //! @param[in] key the key 1933 //! @param[in] name the name of the new subkey 1934 //! @param[in] type the type of the new subkey 1935 //! @param[out] subkey the index of the resulting subkey 1936 //! @return whether the call was successful 1937 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_map_add_subkey(clingo_statistics_t *statistics, uint64_t key, char const *name, clingo_statistics_type_t type, uint64_t *subkey); 1938 //! @} 1939 1940 //! @name Functions to inspect and change values 1941 //! @{ 1942 1943 //! Get the value of the given entry. 1944 //! 1945 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_value. 1946 //! @param[in] statistics the target statistics 1947 //! @param[in] key the key 1948 //! @param[out] value the resulting value 1949 //! @return whether the call was successful 1950 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_value_get(clingo_statistics_t const *statistics, uint64_t key, double *value); 1951 //! Set the value of the given entry. 1952 //! 1953 //! @pre The @link clingo_statistics_type() type@endlink of the entry must be @ref ::clingo_statistics_type_value. 1954 //! @param[in] statistics the target statistics 1955 //! @param[in] key the key 1956 //! @param[out] value the new value 1957 //! @return whether the call was successful 1958 CLINGO_VISIBILITY_DEFAULT bool clingo_statistics_value_set(clingo_statistics_t *statistics, uint64_t key, double value); 1959 //! @} 1960 1961 //! @} 1962 1963 // {{{1 model and solve control 1964 1965 //! @example model.c 1966 //! The example shows how to inspect a model. 1967 //! 1968 //! ## Output ## 1969 //! 1970 //! ~~~~~~~~~~~~ 1971 //! $ ./model 0 1972 //! Stable model: 1973 //! shown: c 1974 //! atoms: b 1975 //! terms: c 1976 //! ~atoms: a 1977 //! Stable model: 1978 //! shown: a 1979 //! atoms: a 1980 //! terms: 1981 //! ~atoms: b 1982 //! ~~~~~~~~~~~~ 1983 //! 1984 //! ## Code ## 1985 1986 //! @defgroup Model Model Inspection 1987 //! Inspection of models and a high-level interface to add constraints during solving. 1988 //! 1989 //! For an example, see @ref model.c. 1990 //! @ingroup Control 1991 1992 //! @addtogroup Model 1993 //! @{ 1994 1995 //! Object to add clauses during search. 1996 typedef struct clingo_solve_control clingo_solve_control_t; 1997 1998 //! Object representing a model. 1999 typedef struct clingo_model clingo_model_t; 2000 2001 //! Enumeration for the different model types. 2002 enum clingo_model_type_e { 2003 clingo_model_type_stable_model = 0, //!< The model represents a stable model. 2004 clingo_model_type_brave_consequences = 1, //!< The model represents a set of brave consequences. 2005 clingo_model_type_cautious_consequences = 2 //!< The model represents a set of cautious consequences. 2006 }; 2007 //! Corresponding type to ::clingo_model_type_e. 2008 typedef int clingo_model_type_t; 2009 2010 //! Enumeration of bit flags to select symbols in models. 2011 enum clingo_show_type_e { 2012 clingo_show_type_csp = 1, //!< Select CSP assignments. 2013 clingo_show_type_shown = 2, //!< Select shown atoms and terms. 2014 clingo_show_type_atoms = 4, //!< Select all atoms. 2015 clingo_show_type_terms = 8, //!< Select all terms. 2016 clingo_show_type_theory = 16, //!< Select symbols added by theory. 2017 clingo_show_type_all = 31, //!< Select everything. 2018 clingo_show_type_complement = 32 //!< Select false instead of true atoms (::clingo_show_type_atoms) or terms (::clingo_show_type_terms). 2019 }; 2020 //! Corresponding type to ::clingo_show_type_e. 2021 typedef unsigned clingo_show_type_bitset_t; 2022 2023 //! @name Functions for Inspecting Models 2024 //! @{ 2025 2026 //! Get the type of the model. 2027 //! 2028 //! @param[in] model the target 2029 //! @param[out] type the type of the model 2030 //! @return whether the call was successful 2031 CLINGO_VISIBILITY_DEFAULT bool clingo_model_type(clingo_model_t const *model, clingo_model_type_t *type); 2032 //! Get the running number of the model. 2033 //! 2034 //! @param[in] model the target 2035 //! @param[out] number the number of the model 2036 //! @return whether the call was successful 2037 CLINGO_VISIBILITY_DEFAULT bool clingo_model_number(clingo_model_t const *model, uint64_t *number); 2038 //! Get the number of symbols of the selected types in the model. 2039 //! 2040 //! @param[in] model the target 2041 //! @param[in] show which symbols to select 2042 //! @param[out] size the number symbols 2043 //! @return whether the call was successful; might set one of the following error codes: 2044 //! - ::clingo_error_bad_alloc 2045 CLINGO_VISIBILITY_DEFAULT bool clingo_model_symbols_size(clingo_model_t const *model, clingo_show_type_bitset_t show, size_t *size); 2046 //! Get the symbols of the selected types in the model. 2047 //! 2048 //! @note CSP assignments are represented using functions with name "$" 2049 //! where the first argument is the name of the CSP variable and the second one its 2050 //! value. 2051 //! 2052 //! @param[in] model the target 2053 //! @param[in] show which symbols to select 2054 //! @param[out] symbols the resulting symbols 2055 //! @param[in] size the number of selected symbols 2056 //! @return whether the call was successful; might set one of the following error codes: 2057 //! - ::clingo_error_bad_alloc 2058 //! - ::clingo_error_runtime if the size is too small 2059 //! 2060 //! @see clingo_model_symbols_size() 2061 CLINGO_VISIBILITY_DEFAULT bool clingo_model_symbols(clingo_model_t const *model, clingo_show_type_bitset_t show, clingo_symbol_t *symbols, size_t size); 2062 //! Constant time lookup to test whether an atom is in a model. 2063 //! 2064 //! @param[in] model the target 2065 //! @param[in] atom the atom to lookup 2066 //! @param[out] contained whether the atom is contained 2067 //! @return whether the call was successful 2068 CLINGO_VISIBILITY_DEFAULT bool clingo_model_contains(clingo_model_t const *model, clingo_symbol_t atom, bool *contained); 2069 //! Check if a program literal is true in a model. 2070 //! 2071 //! @param[in] model the target 2072 //! @param[in] literal the literal to lookup 2073 //! @param[out] result whether the literal is true 2074 //! @return whether the call was successful 2075 CLINGO_VISIBILITY_DEFAULT bool clingo_model_is_true(clingo_model_t const *model, clingo_literal_t literal, bool *result); 2076 //! Get the number of cost values of a model. 2077 //! 2078 //! @param[in] model the target 2079 //! @param[out] size the number of costs 2080 //! @return whether the call was successful 2081 CLINGO_VISIBILITY_DEFAULT bool clingo_model_cost_size(clingo_model_t const *model, size_t *size); 2082 //! Get the cost vector of a model. 2083 //! 2084 //! @param[in] model the target 2085 //! @param[out] costs the resulting costs 2086 //! @param[in] size the number of costs 2087 //! @return whether the call was successful; might set one of the following error codes: 2088 //! - ::clingo_error_bad_alloc 2089 //! - ::clingo_error_runtime if the size is too small 2090 //! 2091 //! @see clingo_model_cost_size() 2092 //! @see clingo_model_optimality_proven() 2093 CLINGO_VISIBILITY_DEFAULT bool clingo_model_cost(clingo_model_t const *model, int64_t *costs, size_t size); 2094 //! Whether the optimality of a model has been proven. 2095 //! 2096 //! @param[in] model the target 2097 //! @param[out] proven whether the optimality has been proven 2098 //! @return whether the call was successful 2099 //! 2100 //! @see clingo_model_cost() 2101 CLINGO_VISIBILITY_DEFAULT bool clingo_model_optimality_proven(clingo_model_t const *model, bool *proven); 2102 //! Get the id of the solver thread that found the model. 2103 //! 2104 //! @param[in] model the target 2105 //! @param[out] id the resulting thread id 2106 //! @return whether the call was successful 2107 CLINGO_VISIBILITY_DEFAULT bool clingo_model_thread_id(clingo_model_t const *model, clingo_id_t *id); 2108 //! Add symbols to the model. 2109 //! 2110 //! These symbols will appear in clingo's output, which means that this 2111 //! function is only meaningful if there is an underlying clingo application. 2112 //! Only models passed to the ::clingo_solve_event_callback_t are extendable. 2113 //! 2114 //! @param[in] model the target 2115 //! @param[in] symbols the symbols to add 2116 //! @param[in] size the number of symbols to add 2117 //! @return whether the call was successful 2118 CLINGO_VISIBILITY_DEFAULT bool clingo_model_extend(clingo_model_t *model, clingo_symbol_t const *symbols, size_t size); 2119 //! @} 2120 2121 //! @name Functions for Adding Clauses 2122 //! @{ 2123 2124 //! Get the associated solve control object of a model. 2125 //! 2126 //! This object allows for adding clauses during model enumeration. 2127 //! @param[in] model the target 2128 //! @param[out] control the resulting solve control object 2129 //! @return whether the call was successful 2130 CLINGO_VISIBILITY_DEFAULT bool clingo_model_context(clingo_model_t const *model, clingo_solve_control_t **control); 2131 //! Get an object to inspect the symbolic atoms. 2132 //! 2133 //! @param[in] control the target 2134 //! @param[out] atoms the resulting object 2135 //! @return whether the call was successful 2136 CLINGO_VISIBILITY_DEFAULT bool clingo_solve_control_symbolic_atoms(clingo_solve_control_t const *control, clingo_symbolic_atoms_t const **atoms); 2137 //! Add a clause that applies to the current solving step during model 2138 //! enumeration. 2139 //! 2140 //! @note The @ref Propagator module provides a more sophisticated 2141 //! interface to add clauses - even on partial assignments. 2142 //! 2143 //! @param[in] control the target 2144 //! @param[in] clause array of literals representing the clause 2145 //! @param[in] size the size of the literal array 2146 //! @return whether the call was successful; might set one of the following error codes: 2147 //! - ::clingo_error_bad_alloc 2148 //! - ::clingo_error_runtime if adding the clause fails 2149 CLINGO_VISIBILITY_DEFAULT bool clingo_solve_control_add_clause(clingo_solve_control_t *control, clingo_literal_t const *clause, size_t size); 2150 //! @} 2151 2152 //! @} 2153 2154 // {{{1 solve result 2155 2156 // NOTE: documented in Control Module 2157 enum clingo_solve_result_e { 2158 clingo_solve_result_satisfiable = 1, 2159 clingo_solve_result_unsatisfiable = 2, 2160 clingo_solve_result_exhausted = 4, 2161 clingo_solve_result_interrupted = 8 2162 }; 2163 typedef unsigned clingo_solve_result_bitset_t; 2164 2165 // {{{1 solve handle 2166 2167 //! @example solve-async.c 2168 //! The example shows how to solve in the background. 2169 //! 2170 //! ## Output (approximately) ## 2171 //! 2172 //! ~~~~~~~~~~~~ 2173 //! ./solve-async 0 2174 //! pi = 3. 2175 //! 1415926535 8979323846 2643383279 5028841971 6939937510 5820974944 2176 //! 5923078164 0628620899 8628034825 3421170679 8214808651 3282306647 2177 //! 0938446095 5058223172 5359408128 4811174502 8410270193 8521105559 2178 //! 6446229489 5493038196 4428810975 6659334461 2847564823 3786783165 2179 //! 2712019091 4564856692 3460348610 4543266482 1339360726 0249141273 2180 //! 7245870066 0631558817 4881520920 9628292540 9171536436 7892590360 2181 //! 0113305305 4882046652 1384146951 9415116094 3305727036 5759591953 2182 //! 0921861173 8193261179 3105118548 0744623799 6274956735 1885752724 2183 //! 8912279381 8301194912 ... 2184 //! ~~~~~~~~~~~~ 2185 //! 2186 //! ## Code ## 2187 2188 //! @defgroup SolveHandle Solving 2189 //! Interact with a running search. 2190 //! 2191 //! A ::clingo_solve_handle_t objects can be used for both synchronous and asynchronous search, 2192 //! as well as iteratively receiving models and solve results. 2193 //! 2194 //! For an example showing how to solve asynchronously, see @ref solve-async.c. 2195 //! @ingroup Control 2196 2197 //! @addtogroup SolveHandle 2198 //! @{ 2199 2200 //! Enumeration of solve modes. 2201 enum clingo_solve_mode_e { 2202 clingo_solve_mode_async = 1, //!< Enable non-blocking search. 2203 clingo_solve_mode_yield = 2, //!< Yield models in calls to clingo_solve_handle_model. 2204 }; 2205 //! Corresponding type to ::clingo_solve_mode_e. 2206 typedef unsigned clingo_solve_mode_bitset_t; 2207 2208 //! Enumeration of solve events. 2209 enum clingo_solve_event_type_e { 2210 clingo_solve_event_type_model = 0, //!< Issued if a model is found. 2211 clingo_solve_event_type_unsat = 1, //!< Issued if an optimization problem is found unsatisfiable. 2212 clingo_solve_event_type_statistics = 2, //!< Issued when the statistics can be updated. 2213 clingo_solve_event_type_finish = 3, //!< Issued if the search has completed. 2214 }; 2215 //! Corresponding type to ::clingo_solve_event_type_e. 2216 typedef unsigned clingo_solve_event_type_t; 2217 2218 //! Callback function called during search to notify when the search is finished or a model is ready. 2219 //! 2220 //! If a (non-recoverable) clingo API function fails in this callback, it must return false. 2221 //! In case of errors not related to clingo, set error code ::clingo_error_unknown and return false to stop solving with an error. 2222 //! 2223 //! The event is either a pointer to a model, a pointer to an int64_t* and a size_t, a pointer to two statistics objects (per step and accumulated statistics), or a solve result. 2224 //! @attention If the search is finished, the model is NULL. 2225 //! 2226 //! @param[in] event the current event. 2227 //! @param[in] data user data of the callback 2228 //! @param[out] goon can be set to false to stop solving 2229 //! @return whether the call was successful 2230 //! 2231 //! @see clingo_control_solve() 2232 typedef bool (*clingo_solve_event_callback_t) (clingo_solve_event_type_t type, void *event, void *data, bool *goon); 2233 2234 //! Search handle to a solve call. 2235 //! 2236 //! @see clingo_control_solve() 2237 typedef struct clingo_solve_handle clingo_solve_handle_t; 2238 2239 //! Get the next solve result. 2240 //! 2241 //! Blocks until the result is ready. 2242 //! When yielding partial solve results can be obtained, i.e., 2243 //! when a model is ready, the result will be satisfiable but neither the search exhausted nor the optimality proven. 2244 //! 2245 //! @param[in] handle the target 2246 //! @param[out] result the solve result 2247 //! @return whether the call was successful; might set one of the following error codes: 2248 //! - ::clingo_error_bad_alloc 2249 //! - ::clingo_error_runtime if solving fails 2250 CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_get(clingo_solve_handle_t *handle, clingo_solve_result_bitset_t *result); 2251 //! Wait for the specified amount of time to check if the next result is ready. 2252 //! 2253 //! If the time is set to zero, this function can be used to poll if the search is still active. 2254 //! If the time is negative, the function blocks until the search is finished. 2255 //! 2256 //! @param[in] handle the target 2257 //! @param[in] timeout the maximum time to wait 2258 //! @param[out] result whether the search has finished 2259 CLINGO_VISIBILITY_DEFAULT void clingo_solve_handle_wait(clingo_solve_handle_t *handle, double timeout, bool *result); 2260 //! Get the next model (or zero if there are no more models). 2261 //! 2262 //! @param[in] handle the target 2263 //! @param[out] model the model (it is NULL if there are no more models) 2264 //! @return whether the call was successful; might set one of the following error codes: 2265 //! - ::clingo_error_bad_alloc 2266 //! - ::clingo_error_runtime if solving fails 2267 CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_model(clingo_solve_handle_t *handle, clingo_model_t const **model); 2268 //! When a problem is unsatisfiable, get a subset of the assumptions that made the problem unsatisfiable. 2269 //! 2270 //! If the program is not unsatisfiable, core is set to NULL and size to zero. 2271 //! 2272 //! @param[in] handle the target 2273 //! @param[out] core pointer where to store the core 2274 //! @param[out] size size of the given array 2275 //! @return whether the call was successful; might set one of the following error codes: 2276 //! - ::clingo_error_bad_alloc 2277 CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_core(clingo_solve_handle_t *handle, clingo_literal_t const **core, size_t *size); 2278 //! Discards the last model and starts the search for the next one. 2279 //! 2280 //! If the search has been started asynchronously, this function continues the search in the background. 2281 //! 2282 //! @note This function does not block. 2283 //! 2284 //! @param[in] handle the target 2285 //! @return whether the call was successful; might set one of the following error codes: 2286 //! - ::clingo_error_bad_alloc 2287 //! - ::clingo_error_runtime if solving fails 2288 CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_resume(clingo_solve_handle_t *handle); 2289 //! Stop the running search and block until done. 2290 //! 2291 //! @param[in] handle the target 2292 //! @return whether the call was successful; might set one of the following error codes: 2293 //! - ::clingo_error_bad_alloc 2294 //! - ::clingo_error_runtime if solving fails 2295 CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_cancel(clingo_solve_handle_t *handle); 2296 //! Stops the running search and releases the handle. 2297 //! 2298 //! Blocks until the search is stopped (as if an implicit cancel was called before the handle is released). 2299 //! 2300 //! @param[in] handle the target 2301 //! @return whether the call was successful; might set one of the following error codes: 2302 //! - ::clingo_error_bad_alloc 2303 //! - ::clingo_error_runtime if solving fails 2304 CLINGO_VISIBILITY_DEFAULT bool clingo_solve_handle_close(clingo_solve_handle_t *handle); 2305 2306 //! @} 2307 // {{{1 ast 2308 2309 //! @example ast.c 2310 //! The example shows how to rewrite a non-ground logic program. 2311 //! 2312 //! ## Output ## 2313 //! 2314 //! ~~~~~~~~ 2315 //! ./ast 0 2316 //! Solving with enable = false... 2317 //! Model: 2318 //! Solving with enable = true... 2319 //! Model: enable a 2320 //! Model: enable b 2321 //! Solving with enable = false... 2322 //! Model: 2323 //! ~~~~~~~~ 2324 //! 2325 //! ## Code ## 2326 2327 //! @defgroup AST Abstract Syntax Trees 2328 //! Functions and data structures to work with program ASTs. 2329 2330 //! @addtogroup AST 2331 //! @{ 2332 2333 //! Enumeration of theory sequence types. 2334 enum clingo_ast_theory_sequence_type_e { 2335 clingo_ast_theory_sequence_type_tuple, //!< Theory tuples "(t1,...,tn)". 2336 clingo_ast_theory_sequence_type_list, //!< Theory lists "[t1,...,tn]". 2337 clingo_ast_theory_sequence_type_set //!< Theory sets "{t1,...,tn}". 2338 }; 2339 //! Corresponding type to ::clingo_ast_theory_sequence_type_e. 2340 typedef int clingo_ast_theory_sequence_type_t; 2341 2342 //! Enumeration of comparison relations. 2343 enum clingo_ast_comparison_operator_e { 2344 clingo_ast_comparison_operator_greater_than = 0, //!< Operator ">". 2345 clingo_ast_comparison_operator_less_than = 1, //!< Operator "<". 2346 clingo_ast_comparison_operator_less_equal = 2, //!< Operator "<=". 2347 clingo_ast_comparison_operator_greater_equal = 3, //!< Operator ">=". 2348 clingo_ast_comparison_operator_not_equal = 4, //!< Operator "!=". 2349 clingo_ast_comparison_operator_equal = 5 //!< Operator "==". 2350 }; 2351 //! Corresponding type to ::clingo_ast_comparison_operator_e. 2352 typedef int clingo_ast_comparison_operator_t; 2353 2354 //! Enumeration of signs. 2355 enum clingo_ast_sign_e { 2356 clingo_ast_sign_no_sign = 0, //!< For positive literals. 2357 clingo_ast_sign_negation = 1, //!< For negative literals (prefix "not"). 2358 clingo_ast_sign_double_negation = 2 //!< For double negated literals (prefix "not not"). 2359 }; 2360 //! Corresponding type to ::clingo_ast_sign_t. 2361 typedef int clingo_ast_sign_t; 2362 2363 //! Enumeration of unary operators. 2364 enum clingo_ast_unary_operator_e { 2365 clingo_ast_unary_operator_minus = 0, //!< Operator "-". 2366 clingo_ast_unary_operator_negation = 1, //!< Operator "~". 2367 clingo_ast_unary_operator_absolute = 2 //!< Operator "|.|". 2368 }; 2369 //! Corresponding type to ::clingo_ast_unary_operator_e. 2370 typedef int clingo_ast_unary_operator_t; 2371 2372 //! Enumeration of binary operators. 2373 enum clingo_ast_binary_operator_e { 2374 clingo_ast_binary_operator_xor = 0, //!< Operator "^". 2375 clingo_ast_binary_operator_or = 1, //!< Operator "?". 2376 clingo_ast_binary_operator_and = 2, //!< Operator "&". 2377 clingo_ast_binary_operator_plus = 3, //!< Operator "+". 2378 clingo_ast_binary_operator_minus = 4, //!< Operator "-". 2379 clingo_ast_binary_operator_multiplication = 5, //!< Operator "*". 2380 clingo_ast_binary_operator_division = 6, //!< Operator "/". 2381 clingo_ast_binary_operator_modulo = 7, //!< Operator "\". 2382 clingo_ast_binary_operator_power = 8 //!< Operator "**". 2383 }; 2384 //! Corresponding type to ::clingo_ast_binary_operator_e. 2385 typedef int clingo_ast_binary_operator_t; 2386 2387 //! Enumeration of aggregate functions. 2388 enum clingo_ast_aggregate_function_e { 2389 clingo_ast_aggregate_function_count = 0, //!< Operator "^". 2390 clingo_ast_aggregate_function_sum = 1, //!< Operator "?". 2391 clingo_ast_aggregate_function_sump = 2, //!< Operator "&". 2392 clingo_ast_aggregate_function_min = 3, //!< Operator "+". 2393 clingo_ast_aggregate_function_max = 4 //!< Operator "-". 2394 }; 2395 //! Corresponding type to ::clingo_ast_aggregate_function_e. 2396 typedef int clingo_ast_aggregate_function_t; 2397 2398 //! Enumeration of theory operators. 2399 enum clingo_ast_theory_operator_type_e { 2400 clingo_ast_theory_operator_type_unary = 0, //!< An unary theory operator. 2401 clingo_ast_theory_operator_type_binary_left = 1, //!< A left associative binary operator. 2402 clingo_ast_theory_operator_type_binary_right = 2 //!< A right associative binary operator. 2403 }; 2404 //! Corresponding type to ::clingo_ast_theory_operator_type_e. 2405 typedef int clingo_ast_theory_operator_type_t; 2406 2407 //! Enumeration of the theory atom types. 2408 enum clingo_ast_theory_atom_definition_type_e { 2409 clingo_ast_theory_atom_definition_type_head = 0, //!< For theory atoms that can appear in the head. 2410 clingo_ast_theory_atom_definition_type_body = 1, //!< For theory atoms that can appear in the body. 2411 clingo_ast_theory_atom_definition_type_any = 2, //!< For theory atoms that can appear in both head and body. 2412 clingo_ast_theory_atom_definition_type_directive = 3 //!< For theory atoms that must not have a body. 2413 }; 2414 //! Corresponding type to ::clingo_ast_theory_atom_definition_type_e. 2415 typedef int clingo_ast_theory_atom_definition_type_t; 2416 2417 //! Enumeration of AST types. 2418 enum clingo_ast_type_e { 2419 // terms 2420 clingo_ast_type_id, 2421 clingo_ast_type_variable, 2422 clingo_ast_type_symbolic_term, 2423 clingo_ast_type_unary_operation, 2424 clingo_ast_type_binary_operation, 2425 clingo_ast_type_interval, 2426 clingo_ast_type_function, 2427 clingo_ast_type_pool, 2428 // csp terms 2429 clingo_ast_type_csp_product, 2430 clingo_ast_type_csp_sum, 2431 clingo_ast_type_csp_guard, 2432 // simple atoms 2433 clingo_ast_type_boolean_constant, 2434 clingo_ast_type_symbolic_atom, 2435 clingo_ast_type_comparison, 2436 clingo_ast_type_csp_literal, 2437 // aggregates 2438 clingo_ast_type_aggregate_guard, 2439 clingo_ast_type_conditional_literal, 2440 clingo_ast_type_aggregate, 2441 clingo_ast_type_body_aggregate_element, 2442 clingo_ast_type_body_aggregate, 2443 clingo_ast_type_head_aggregate_element, 2444 clingo_ast_type_head_aggregate, 2445 clingo_ast_type_disjunction, 2446 clingo_ast_type_disjoint_element, 2447 clingo_ast_type_disjoint, 2448 // theory atoms 2449 clingo_ast_type_theory_sequence, 2450 clingo_ast_type_theory_function, 2451 clingo_ast_type_theory_unparsed_term_element, 2452 clingo_ast_type_theory_unparsed_term, 2453 clingo_ast_type_theory_guard, 2454 clingo_ast_type_theory_atom_element, 2455 clingo_ast_type_theory_atom, 2456 // literals 2457 clingo_ast_type_literal, 2458 // theory definition 2459 clingo_ast_type_theory_operator_definition, 2460 clingo_ast_type_theory_term_definition, 2461 clingo_ast_type_theory_guard_definition, 2462 clingo_ast_type_theory_atom_definition, 2463 // statements 2464 clingo_ast_type_rule, 2465 clingo_ast_type_definition, 2466 clingo_ast_type_show_signature, 2467 clingo_ast_type_show_term, 2468 clingo_ast_type_minimize, 2469 clingo_ast_type_script, 2470 clingo_ast_type_program, 2471 clingo_ast_type_external, 2472 clingo_ast_type_edge, 2473 clingo_ast_type_heuristic, 2474 clingo_ast_type_project_atom, 2475 clingo_ast_type_project_signature, 2476 clingo_ast_type_defined, 2477 clingo_ast_type_theory_definition 2478 }; 2479 //! Corresponding type to ::clingo_ast_type_e. 2480 typedef int clingo_ast_type_t; 2481 2482 //! Enumeration of attributes types used by the AST. 2483 enum clingo_ast_attribute_type_e { 2484 clingo_ast_attribute_type_number = 0, //!< For an attribute of type "int". 2485 clingo_ast_attribute_type_symbol = 1, //!< For an attribute of type "clingo_ast_symbol_t". 2486 clingo_ast_attribute_type_location = 2, //!< For an attribute of type "clingo_location_t". 2487 clingo_ast_attribute_type_string = 3, //!< For an attribute of type "char const *". 2488 clingo_ast_attribute_type_ast = 4, //!< For an attribute of type "clingo_ast_t *". 2489 clingo_ast_attribute_type_optional_ast = 5, //!< For an attribute of type "clingo_ast_t *" that can be NULL. 2490 clingo_ast_attribute_type_string_array = 6, //!< For an attribute of type "char const **". 2491 clingo_ast_attribute_type_ast_array = 7, //!< For an attribute of type "clingo_ast_t **". 2492 }; 2493 //! Corresponding type to ::clingo_ast_attribute_type. 2494 typedef int clingo_ast_attribute_type_t; 2495 2496 //! Enumeration of attributes used by the AST. 2497 enum clingo_ast_attribute_e { 2498 clingo_ast_attribute_argument, 2499 clingo_ast_attribute_arguments, 2500 clingo_ast_attribute_arity, 2501 clingo_ast_attribute_atom, 2502 clingo_ast_attribute_atoms, 2503 clingo_ast_attribute_atom_type, 2504 clingo_ast_attribute_bias, 2505 clingo_ast_attribute_body, 2506 clingo_ast_attribute_code, 2507 clingo_ast_attribute_coefficient, 2508 clingo_ast_attribute_comparison, 2509 clingo_ast_attribute_condition, 2510 clingo_ast_attribute_csp, 2511 clingo_ast_attribute_elements, 2512 clingo_ast_attribute_external, 2513 clingo_ast_attribute_external_type, 2514 clingo_ast_attribute_function, 2515 clingo_ast_attribute_guard, 2516 clingo_ast_attribute_guards, 2517 clingo_ast_attribute_head, 2518 clingo_ast_attribute_is_default, 2519 clingo_ast_attribute_left, 2520 clingo_ast_attribute_left_guard, 2521 clingo_ast_attribute_literal, 2522 clingo_ast_attribute_location, 2523 clingo_ast_attribute_modifier, 2524 clingo_ast_attribute_name, 2525 clingo_ast_attribute_node_u, 2526 clingo_ast_attribute_node_v, 2527 clingo_ast_attribute_operator_name, 2528 clingo_ast_attribute_operator_type, 2529 clingo_ast_attribute_operators, 2530 clingo_ast_attribute_parameters, 2531 clingo_ast_attribute_positive, 2532 clingo_ast_attribute_priority, 2533 clingo_ast_attribute_right, 2534 clingo_ast_attribute_right_guard, 2535 clingo_ast_attribute_sequence_type, 2536 clingo_ast_attribute_sign, 2537 clingo_ast_attribute_symbol, 2538 clingo_ast_attribute_term, 2539 clingo_ast_attribute_terms, 2540 clingo_ast_attribute_value, 2541 clingo_ast_attribute_variable, 2542 clingo_ast_attribute_weight, 2543 }; 2544 //! Corresponding type to ::clingo_ast_attribute_e. 2545 typedef int clingo_ast_attribute_t; 2546 2547 //! Struct to map attributes to their string representation. 2548 typedef struct clingo_ast_attribute_names { 2549 char const * const * names; 2550 size_t size; 2551 } clingo_ast_attribute_names_t; 2552 2553 //! A map from attributes to their string representation. 2554 CLINGO_VISIBILITY_DEFAULT extern clingo_ast_attribute_names_t g_clingo_ast_attribute_names; 2555 2556 //! Struct to define an argument that consists of a name and a type. 2557 typedef struct clingo_ast_argument { 2558 clingo_ast_attribute_t attribute; 2559 clingo_ast_attribute_type_t type; 2560 } clingo_ast_argument_t; 2561 2562 //! A lists of required attributes to construct an AST. 2563 typedef struct clingo_ast_constructor { 2564 char const *name; 2565 clingo_ast_argument_t const *arguments; 2566 size_t size; 2567 } clingo_ast_constructor_t; 2568 2569 //! Struct to map AST types to lists of required attributes to construct ASTs. 2570 typedef struct clingo_ast_constructors { 2571 clingo_ast_constructor_t const *constructors; 2572 size_t size; 2573 } clingo_ast_constructors_t; 2574 2575 //! A map from AST types to their constructors. 2576 //! 2577 //! @note The idea of this variable is to provide enough information to auto-generate code for language bindings. 2578 CLINGO_VISIBILITY_DEFAULT extern clingo_ast_constructors_t g_clingo_ast_constructors; 2579 2580 //! This struct provides a view to nodes in the AST. 2581 typedef struct clingo_ast clingo_ast_t; 2582 2583 //! @name Functions to construct ASTs 2584 //! @{ 2585 2586 //! Construct an AST of the given type. 2587 //! 2588 //! @note The arguments corresponding to the given type can be inspected using "g_clingo_ast_constructors.constructors[type]". 2589 //! 2590 //! @param[in] type the type of AST to construct 2591 //! @param[out] ast the resulting AST 2592 //! @return whether the call was successful; might set one of the following error codes: 2593 //! - ::clingo_error_bad_alloc 2594 //! - ::clingo_error_runtime if one of the arguments is incompatible with the type 2595 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_build(clingo_ast_type_t type, clingo_ast_t **ast, ...); 2596 2597 //! @} 2598 2599 //! @name Functions to manage life time of ASTs 2600 //! @{ 2601 2602 //! Increment the reference count of an AST node. 2603 //! 2604 //! @note All functions that return AST nodes already increment the reference count. 2605 //! The reference count of callback arguments is not incremented. 2606 //! 2607 //! @param[in] ast the target AST 2608 CLINGO_VISIBILITY_DEFAULT void clingo_ast_acquire(clingo_ast_t *ast); 2609 //! Decrement the reference count of an AST node. 2610 //! 2611 //! @note The node is deleted if the reference count reaches zero. 2612 //! 2613 //! @param[in] ast the target AST 2614 CLINGO_VISIBILITY_DEFAULT void clingo_ast_release(clingo_ast_t *ast); 2615 2616 //! @} 2617 2618 //! @name Functions to copy ASTs 2619 //! @{ 2620 2621 //! Create a shallow copy of an AST node. 2622 //! 2623 //! @param[in] ast the AST to copy 2624 //! @param[out] copy the resulting AST 2625 //! @return whether the call was successful; might set one of the following error codes: 2626 //! - ::clingo_error_bad_alloc 2627 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_copy(clingo_ast_t *ast, clingo_ast_t **copy); 2628 //! Create a deep copy of an AST node. 2629 //! 2630 //! @param[in] ast the AST to copy 2631 //! @param[out] copy the resulting AST 2632 //! @return whether the call was successful; might set one of the following error codes: 2633 //! - ::clingo_error_bad_alloc 2634 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_deep_copy(clingo_ast_t *ast, clingo_ast_t **copy); 2635 2636 //! @} 2637 2638 //! @name Functions to compare ASTs 2639 //! @{ 2640 2641 //! Less than compare two AST nodes. 2642 //! 2643 //! @param[in] a the left-hand-side AST 2644 //! @param[in] b the right-hand-side AST 2645 //! @return the result of the comparison 2646 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_less_than(clingo_ast_t *a, clingo_ast_t *b); 2647 //! Equality compare two AST nodes. 2648 //! 2649 //! @param[in] a the left-hand-side AST 2650 //! @param[in] b the right-hand-side AST 2651 //! @return the result of the comparison 2652 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_equal(clingo_ast_t *a, clingo_ast_t *b); 2653 //! Compute a hash for an AST node. 2654 //! 2655 //! @param[in] ast the target AST 2656 //! @return the resulting hash code 2657 CLINGO_VISIBILITY_DEFAULT size_t clingo_ast_hash(clingo_ast_t *ast); 2658 2659 //! @} 2660 2661 //! @name Functions to get convert ASTs to strings 2662 //! @{ 2663 2664 //! Get the size of the string representation of an AST node. 2665 //! 2666 //! @param[in] ast the target AST 2667 //! @param[out] size the size of the string representation 2668 //! @return whether the call was successful; might set one of the following error codes: 2669 //! - ::clingo_error_runtime 2670 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_to_string_size(clingo_ast_t *ast, size_t *size); 2671 //! Get the string representation of an AST node. 2672 //! 2673 //! @param[in] ast the target AST 2674 //! @param[out] string the string representation 2675 //! @param[out] size the size of the string representation 2676 //! @return whether the call was successful; might set one of the following error codes: 2677 //! - ::clingo_error_runtime 2678 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_to_string(clingo_ast_t *ast, char *string, size_t size); 2679 2680 //! @} 2681 2682 //! @name Functions to inspect ASTs 2683 //! @{ 2684 2685 //! Get the type of an AST node. 2686 //! 2687 //! @param[in] ast the target AST 2688 //! @param[out] type the resulting type 2689 //! @return whether the call was successful; might set one of the following error codes: 2690 //! - ::clingo_error_runtime 2691 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_get_type(clingo_ast_t *ast, clingo_ast_type_t *type); 2692 //! Check if an AST has the given attribute. 2693 //! 2694 //! @param[in] ast the target AST 2695 //! @param[in] attribute the attribute to check 2696 //! @param[out] has_attribute the result 2697 //! @return whether the call was successful; might set one of the following error codes: 2698 //! - ::clingo_error_runtime 2699 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_has_attribute(clingo_ast_t *ast, clingo_ast_attribute_t attribute, bool *has_attribute); 2700 //! Get the type of the given AST. 2701 //! 2702 //! @param[in] ast the target AST 2703 //! @param[in] attribute the target attribute 2704 //! @param[out] type the resulting type 2705 //! @return whether the call was successful; might set one of the following error codes: 2706 //! - ::clingo_error_runtime 2707 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_type(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_ast_attribute_type_t *type); 2708 2709 //! @} 2710 2711 //! @name Functions to get/set numeric attributes of ASTs 2712 //! @{ 2713 2714 //! Get the value of an attribute of type "clingo_ast_attribute_type_number". 2715 //! 2716 //! @param[in] ast the target AST 2717 //! @param[in] attribute the target attribute 2718 //! @param[out] value the resulting value 2719 //! @return whether the call was successful; might set one of the following error codes: 2720 //! - ::clingo_error_runtime 2721 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_get_number(clingo_ast_t *ast, clingo_ast_attribute_t attribute, int *value); 2722 //! Set the value of an attribute of type "clingo_ast_attribute_type_number". 2723 //! 2724 //! @param[in] ast the target AST 2725 //! @param[in] attribute the target attribute 2726 //! @param[in] value the value 2727 //! @return whether the call was successful; might set one of the following error codes: 2728 //! - ::clingo_error_runtime 2729 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_set_number(clingo_ast_t *ast, clingo_ast_attribute_t attribute, int value); 2730 2731 //! @} 2732 2733 //! @name Functions to get/set symbolic attributes of ASTs 2734 //! @{ 2735 2736 //! Get the value of an attribute of type "clingo_ast_attribute_type_symbol". 2737 //! 2738 //! @param[in] ast the target AST 2739 //! @param[in] attribute the target attribute 2740 //! @param[out] value the resulting value 2741 //! @return whether the call was successful; might set one of the following error codes: 2742 //! - ::clingo_error_runtime 2743 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_get_symbol(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_symbol_t *value); 2744 //! Set the value of an attribute of type "clingo_ast_attribute_type_symbol". 2745 //! 2746 //! @param[in] ast the target AST 2747 //! @param[in] attribute the target attribute 2748 //! @param[in] value the value 2749 //! @return whether the call was successful; might set one of the following error codes: 2750 //! - ::clingo_error_runtime 2751 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_set_symbol(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_symbol_t value); 2752 2753 //! @} 2754 2755 //! @name Functions to get/set location attributes of ASTs 2756 //! @{ 2757 2758 //! Get the value of an attribute of type "clingo_ast_attribute_type_location". 2759 //! 2760 //! @param[in] ast the target AST 2761 //! @param[in] attribute the target attribute 2762 //! @param[out] value the resulting value 2763 //! @return whether the call was successful; might set one of the following error codes: 2764 //! - ::clingo_error_runtime 2765 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_get_location(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_location_t *value); 2766 //! Set the value of an attribute of type "clingo_ast_attribute_type_location". 2767 //! 2768 //! @param[in] ast the target AST 2769 //! @param[in] attribute the target attribute 2770 //! @param[in] value the value 2771 //! @return whether the call was successful; might set one of the following error codes: 2772 //! - ::clingo_error_runtime 2773 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_set_location(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_location_t const *value); 2774 2775 //! @} 2776 2777 //! @name Functions to get/set string attributes of ASTs 2778 //! @{ 2779 2780 //! Get the value of an attribute of type "clingo_ast_attribute_type_string". 2781 //! 2782 //! @param[in] ast the target AST 2783 //! @param[in] attribute the target attribute 2784 //! @param[out] value the resulting value 2785 //! @return whether the call was successful; might set one of the following error codes: 2786 //! - ::clingo_error_runtime 2787 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_get_string(clingo_ast_t *ast, clingo_ast_attribute_t attribute, char const **value); 2788 //! Set the value of an attribute of type "clingo_ast_attribute_type_string". 2789 //! 2790 //! @param[in] ast the target AST 2791 //! @param[in] attribute the target attribute 2792 //! @param[in] value the value 2793 //! @return whether the call was successful; might set one of the following error codes: 2794 //! - ::clingo_error_runtime 2795 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_set_string(clingo_ast_t *ast, clingo_ast_attribute_t attribute, char const *value); 2796 2797 //! @} 2798 2799 //! @name Functions to get/set AST attributes of ASTs 2800 //! @{ 2801 2802 //! Get the value of an attribute of type "clingo_ast_attribute_type_ast". 2803 //! 2804 //! @param[in] ast the target AST 2805 //! @param[in] attribute the target attribute 2806 //! @param[out] value the resulting value 2807 //! @return whether the call was successful; might set one of the following error codes: 2808 //! - ::clingo_error_runtime 2809 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_get_ast(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_ast_t **value); 2810 //! Set the value of an attribute of type "clingo_ast_attribute_type_ast". 2811 //! 2812 //! @param[in] ast the target AST 2813 //! @param[in] attribute the target attribute 2814 //! @param[in] value the value 2815 //! @return whether the call was successful; might set one of the following error codes: 2816 //! - ::clingo_error_runtime 2817 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_set_ast(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_ast_t *value); 2818 2819 //! @} 2820 2821 //! @name Functions to get/set optional AST attributes of ASTs 2822 //! @{ 2823 2824 //! Get the value of an attribute of type "clingo_ast_attribute_type_optional_ast". 2825 //! 2826 //! @note The value might be "NULL". 2827 //! 2828 //! @param[in] ast the target AST 2829 //! @param[in] attribute the target attribute 2830 //! @param[out] value the resulting value 2831 //! @return whether the call was successful; might set one of the following error codes: 2832 //! - ::clingo_error_runtime 2833 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_get_optional_ast(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_ast_t **value); 2834 //! Set the value of an attribute of type "clingo_ast_attribute_type_optional_ast". 2835 //! 2836 //! @note The value might be "NULL". 2837 //! 2838 //! @param[in] ast the target AST 2839 //! @param[in] attribute the target attribute 2840 //! @param[in] value the value 2841 //! @return whether the call was successful; might set one of the following error codes: 2842 //! - ::clingo_error_runtime 2843 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_set_optional_ast(clingo_ast_t *ast, clingo_ast_attribute_t attribute, clingo_ast_t *value); 2844 2845 //! @} 2846 2847 //! @name Functions to get/set string array attributes of ASTs 2848 //! @{ 2849 2850 //! Get the value of an attribute of type "clingo_ast_attribute_type_string_array" at the given index. 2851 //! 2852 //! @param[in] ast the target AST 2853 //! @param[in] attribute the target attribute 2854 //! @param[in] index the target index 2855 //! @param[out] value the resulting value 2856 //! @return whether the call was successful; might set one of the following error codes: 2857 //! - ::clingo_error_runtime 2858 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_get_string_at(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t index, char const **value); 2859 //! Set the value of an attribute of type "clingo_ast_attribute_type_string_array" at the given index. 2860 //! 2861 //! @param[in] ast the target AST 2862 //! @param[in] attribute the target attribute 2863 //! @param[in] index the target index 2864 //! @param[in] value the value 2865 //! @return whether the call was successful; might set one of the following error codes: 2866 //! - ::clingo_error_runtime 2867 //! - ::clingo_error_bad_alloc 2868 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_set_string_at(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t index, char const *value); 2869 //! Remove an element from an attribute of type "clingo_ast_attribute_type_string_array" at the given index. 2870 //! 2871 //! @param[in] ast the target AST 2872 //! @param[in] attribute the target attribute 2873 //! @param[in] index the target index 2874 //! @return whether the call was successful; might set one of the following error codes: 2875 //! - ::clingo_error_runtime 2876 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_delete_string_at(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t index); 2877 //! Get the size of an attribute of type "clingo_ast_attribute_type_string_array". 2878 //! 2879 //! @param[in] ast the target AST 2880 //! @param[in] attribute the target attribute 2881 //! @param[out] size the resulting size 2882 //! @return whether the call was successful; might set one of the following error codes: 2883 //! - ::clingo_error_runtime 2884 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_size_string_array(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t *size); 2885 //! Insert a value into an attribute of type "clingo_ast_attribute_type_string_array" at the given index. 2886 //! 2887 //! @param[in] ast the target AST 2888 //! @param[in] attribute the target attribute 2889 //! @param[in] index the target index 2890 //! @param[in] value the value 2891 //! @return whether the call was successful; might set one of the following error codes: 2892 //! - ::clingo_error_runtime 2893 //! - ::clingo_error_bad_alloc 2894 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_insert_string_at(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t index, char const *value); 2895 2896 //! @} 2897 2898 //! @name Functions to get/set AST array attributes of ASTs 2899 //! @{ 2900 2901 //! Get the value of an attribute of type "clingo_ast_attribute_type_ast_array" at the given index. 2902 //! 2903 //! @param[in] ast the target AST 2904 //! @param[in] attribute the target attribute 2905 //! @param[in] index the target index 2906 //! @param[out] value the resulting value 2907 //! @return whether the call was successful; might set one of the following error codes: 2908 //! - ::clingo_error_runtime 2909 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_get_ast_at(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t index, clingo_ast_t **value); 2910 //! Set the value of an attribute of type "clingo_ast_attribute_type_ast_array" at the given index. 2911 //! 2912 //! @param[in] ast the target AST 2913 //! @param[in] attribute the target attribute 2914 //! @param[in] index the target index 2915 //! @param[in] value the value 2916 //! @return whether the call was successful; might set one of the following error codes: 2917 //! - ::clingo_error_runtime 2918 //! - ::clingo_error_bad_alloc 2919 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_set_ast_at(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t index, clingo_ast_t *value); 2920 //! Remove an element from an attribute of type "clingo_ast_attribute_type_ast_array" at the given index. 2921 //! 2922 //! @param[in] ast the target AST 2923 //! @param[in] attribute the target attribute 2924 //! @param[in] index the target index 2925 //! @return whether the call was successful; might set one of the following error codes: 2926 //! - ::clingo_error_runtime 2927 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_delete_ast_at(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t index); 2928 //! Get the size of an attribute of type "clingo_ast_attribute_type_ast_array". 2929 //! 2930 //! @param[in] ast the target AST 2931 //! @param[in] attribute the target attribute 2932 //! @param[out] size the resulting size 2933 //! @return whether the call was successful; might set one of the following error codes: 2934 //! - ::clingo_error_runtime 2935 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_size_ast_array(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t *size); 2936 //! Insert a value into an attribute of type "clingo_ast_attribute_type_ast_array" at the given index. 2937 //! 2938 //! @param[in] ast the target AST 2939 //! @param[in] attribute the target attribute 2940 //! @param[in] index the target index 2941 //! @param[in] value the value 2942 //! @return whether the call was successful; might set one of the following error codes: 2943 //! - ::clingo_error_runtime 2944 //! - ::clingo_error_bad_alloc 2945 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_attribute_insert_ast_at(clingo_ast_t *ast, clingo_ast_attribute_t attribute, size_t index, clingo_ast_t *value); 2946 2947 //! @} 2948 2949 //! @name Functions to construct ASTs from strings 2950 //! @{ 2951 2952 //! Callback function to intercept AST nodes. 2953 //! 2954 //! @param[in] ast the AST 2955 //! @param[in] data a user data pointer 2956 //! @return whether the call was successful 2957 typedef bool (*clingo_ast_callback_t) (clingo_ast_t *ast, void *data); 2958 //! Parse the given program and return an abstract syntax tree for each statement via a callback. 2959 //! 2960 //! @param[in] program the program in gringo syntax 2961 //! @param[in] callback the callback reporting statements 2962 //! @param[in] callback_data user data for the callback 2963 //! @param[in] logger callback to report messages during parsing 2964 //! @param[in] logger_data user data for the logger 2965 //! @param[in] message_limit the maximum number of times the logger is called 2966 //! @return whether the call was successful; might set one of the following error codes: 2967 //! - ::clingo_error_runtime if parsing fails 2968 //! - ::clingo_error_bad_alloc 2969 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_parse_string(char const *program, clingo_ast_callback_t callback, void *callback_data, clingo_logger_t logger, void *logger_data, unsigned message_limit); 2970 //! Parse the programs in the given list of files and return an abstract syntax tree for each statement via a callback. 2971 //! 2972 //! The function follows clingo's handling of files on the command line. 2973 //! Filename "-" is treated as "STDIN" and if an empty list is given, then the parser will read from "STDIN". 2974 //! 2975 //! @param[in] files the beginning of the file name array 2976 //! @param[in] size the number of file names 2977 //! @param[in] callback the callback reporting statements 2978 //! @param[in] callback_data user data for the callback 2979 //! @param[in] logger callback to report messages during parsing 2980 //! @param[in] logger_data user data for the logger 2981 //! @param[in] message_limit the maximum number of times the logger is called 2982 //! @return whether the call was successful; might set one of the following error codes: 2983 //! - ::clingo_error_runtime if parsing fails 2984 //! - ::clingo_error_bad_alloc 2985 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_parse_files(char const * const *files, size_t size, clingo_ast_callback_t callback, void *callback_data, clingo_logger_t logger, void *logger_data, unsigned message_limit); 2986 2987 //! @} 2988 2989 //! Object to build non-ground programs. 2990 typedef struct clingo_program_builder clingo_program_builder_t; 2991 2992 //! @name Functions to add ASTs to logic programs 2993 //! @{ 2994 2995 //! Begin building a program. 2996 //! 2997 //! @param[in] builder the target program builder 2998 //! @return whether the call was successful 2999 CLINGO_VISIBILITY_DEFAULT bool clingo_program_builder_begin(clingo_program_builder_t *builder); 3000 //! End building a program. 3001 //! 3002 //! @param[in] builder the target program builder 3003 //! @return whether the call was successful 3004 CLINGO_VISIBILITY_DEFAULT bool clingo_program_builder_end(clingo_program_builder_t *builder); 3005 //! Adds a statement to the program. 3006 //! 3007 //! @attention @ref clingo_program_builder_begin() must be called before adding statements and @ref clingo_program_builder_end() must be called after all statements have been added. 3008 //! @param[in] builder the target program builder 3009 //! @param[in] ast the AST node to add 3010 //! @return whether the call was successful; might set one of the following error codes: 3011 //! - ::clingo_error_runtime for statements of invalid form or AST nodes that do not represent statements 3012 //! - ::clingo_error_bad_alloc 3013 CLINGO_VISIBILITY_DEFAULT bool clingo_program_builder_add(clingo_program_builder_t *builder, clingo_ast_t *ast); 3014 3015 //! @} 3016 3017 //! @name Functions to unpool ASts 3018 //! @{ 3019 3020 //! Enum to configure unpooling. 3021 enum clingo_ast_unpool_type_e { 3022 clingo_ast_unpool_type_condition = 1, //!< To only unpool conditions of conditional literals. 3023 clingo_ast_unpool_type_other = 2, //!< To unpool everything except conditions of conditional literals. 3024 clingo_ast_unpool_type_all = 3, //!< To unpool everything. 3025 }; 3026 //! Corresponding type to ::clingo_ast_unpool_type_e. 3027 typedef int clingo_ast_unpool_type_bitset_t; 3028 3029 //! Unpool the given AST. 3030 //! 3031 //! @param[in] ast the target AST 3032 //! @param[in] unpool_type what to unpool 3033 //! @param[in] callback the callback to report ASTs 3034 //! @param[in] callback_data user data for the callback 3035 //! @return whether the call was successful; might set one of the following error codes: 3036 //! - ::clingo_error_bad_alloc 3037 CLINGO_VISIBILITY_DEFAULT bool clingo_ast_unpool(clingo_ast_t *ast, clingo_ast_unpool_type_bitset_t unpool_type, clingo_ast_callback_t callback, void *callback_data); 3038 3039 //! @} 3040 3041 //! @} 3042 3043 // {{{1 ground program observer 3044 3045 //! @defgroup ProgramInspection Program Inspection 3046 //! Functions and data structures to inspect programs. 3047 //! @ingroup Control 3048 3049 //! @addtogroup ProgramInspection 3050 //! @{ 3051 3052 //! An instance of this struct has to be registered with a solver to observe ground directives as they are passed to the solver. 3053 //! 3054 //! @note This interface is closely modeled after the aspif format. 3055 //! For more information please refer to the specification of the aspif format. 3056 //! 3057 //! Not all callbacks have to be implemented and can be set to NULL if not needed. 3058 //! If one of the callbacks in the struct fails, grounding is stopped. 3059 //! If a non-recoverable clingo API call fails, a callback must return false. 3060 //! Otherwise ::clingo_error_unknown should be set and false returned. 3061 //! 3062 //! @see clingo_control_register_observer() 3063 typedef struct clingo_ground_program_observer { 3064 //! Called once in the beginning. 3065 //! 3066 //! If the incremental flag is true, there can be multiple calls to @ref clingo_control_solve(). 3067 //! 3068 //! @param[in] incremental whether the program is incremental 3069 //! @param[in] data user data for the callback 3070 //! @return whether the call was successful 3071 bool (*init_program)(bool incremental, void *data); 3072 //! Marks the beginning of a block of directives passed to the solver. 3073 //! 3074 //! @see @ref end_step 3075 //! 3076 //! @param[in] data user data for the callback 3077 //! @return whether the call was successful 3078 bool (*begin_step)(void *data); 3079 //! Marks the end of a block of directives passed to the solver. 3080 //! 3081 //! This function is called before solving starts. 3082 //! 3083 //! @see @ref begin_step 3084 //! 3085 //! @param[in] data user data for the callback 3086 //! @return whether the call was successful 3087 bool (*end_step)(void *data); 3088 3089 //! Observe rules passed to the solver. 3090 //! 3091 //! @param[in] choice determines if the head is a choice or a disjunction 3092 //! @param[in] head the head atoms 3093 //! @param[in] head_size the number of atoms in the head 3094 //! @param[in] body the body literals 3095 //! @param[in] body_size the number of literals in the body 3096 //! @param[in] data user data for the callback 3097 //! @return whether the call was successful 3098 bool (*rule)(bool choice, clingo_atom_t const *head, size_t head_size, clingo_literal_t const *body, size_t body_size, void *data); 3099 //! Observe weight rules passed to the solver. 3100 //! 3101 //! @param[in] choice determines if the head is a choice or a disjunction 3102 //! @param[in] head the head atoms 3103 //! @param[in] head_size the number of atoms in the head 3104 //! @param[in] lower_bound the lower bound of the weight rule 3105 //! @param[in] body the weighted body literals 3106 //! @param[in] body_size the number of weighted literals in the body 3107 //! @param[in] data user data for the callback 3108 //! @return whether the call was successful 3109 bool (*weight_rule)(bool choice, clingo_atom_t const *head, size_t head_size, clingo_weight_t lower_bound, clingo_weighted_literal_t const *body, size_t body_size, void *data); 3110 //! Observe minimize constraints (or weak constraints) passed to the solver. 3111 //! 3112 //! @param[in] priority the priority of the constraint 3113 //! @param[in] literals the weighted literals whose sum to minimize 3114 //! @param[in] size the number of weighted literals 3115 //! @param[in] data user data for the callback 3116 //! @return whether the call was successful 3117 bool (*minimize)(clingo_weight_t priority, clingo_weighted_literal_t const* literals, size_t size, void *data); 3118 //! Observe projection directives passed to the solver. 3119 //! 3120 //! @param[in] atoms the atoms to project on 3121 //! @param[in] size the number of atoms 3122 //! @param[in] data user data for the callback 3123 //! @return whether the call was successful 3124 bool (*project)(clingo_atom_t const *atoms, size_t size, void *data); 3125 //! Observe shown atoms passed to the solver. 3126 //! \note Facts do not have an associated aspif atom. 3127 //! The value of the atom is set to zero. 3128 //! 3129 //! @param[in] symbol the symbolic representation of the atom 3130 //! @param[in] atom the aspif atom (0 for facts) 3131 //! @param[in] data user data for the callback 3132 //! @return whether the call was successful 3133 bool (*output_atom)(clingo_symbol_t symbol, clingo_atom_t atom, void *data); 3134 //! Observe shown terms passed to the solver. 3135 //! 3136 //! @param[in] symbol the symbolic representation of the term 3137 //! @param[in] condition the literals of the condition 3138 //! @param[in] size the size of the condition 3139 //! @param[in] data user data for the callback 3140 //! @return whether the call was successful 3141 bool (*output_term)(clingo_symbol_t symbol, clingo_literal_t const *condition, size_t size, void *data); 3142 //! Observe shown csp variables passed to the solver. 3143 //! 3144 //! @param[in] symbol the symbolic representation of the variable 3145 //! @param[in] value the value of the variable 3146 //! @param[in] condition the literals of the condition 3147 //! @param[in] size the size of the condition 3148 //! @param[in] data user data for the callback 3149 //! @return whether the call was successful 3150 bool (*output_csp)(clingo_symbol_t symbol, int value, clingo_literal_t const *condition, size_t size, void *data); 3151 //! Observe external statements passed to the solver. 3152 //! 3153 //! @param[in] atom the external atom 3154 //! @param[in] type the type of the external statement 3155 //! @param[in] data user data for the callback 3156 //! @return whether the call was successful 3157 bool (*external)(clingo_atom_t atom, clingo_external_type_t type, void *data); 3158 //! Observe assumption directives passed to the solver. 3159 //! 3160 //! @param[in] literals the literals to assume (positive literals are true and negative literals false for the next solve call) 3161 //! @param[in] size the number of atoms 3162 //! @param[in] data user data for the callback 3163 //! @return whether the call was successful 3164 bool (*assume)(clingo_literal_t const *literals, size_t size, void *data); 3165 //! Observe heuristic directives passed to the solver. 3166 //! 3167 //! @param[in] atom the target atom 3168 //! @param[in] type the type of the heuristic modification 3169 //! @param[in] bias the heuristic bias 3170 //! @param[in] priority the heuristic priority 3171 //! @param[in] condition the condition under which to apply the heuristic modification 3172 //! @param[in] size the number of atoms in the condition 3173 //! @param[in] data user data for the callback 3174 //! @return whether the call was successful 3175 bool (*heuristic)(clingo_atom_t atom, clingo_heuristic_type_t type, int bias, unsigned priority, clingo_literal_t const *condition, size_t size, void *data); 3176 //! Observe edge directives passed to the solver. 3177 //! 3178 //! @param[in] node_u the start vertex of the edge 3179 //! @param[in] node_v the end vertex of the edge 3180 //! @param[in] condition the condition under which the edge is part of the graph 3181 //! @param[in] size the number of atoms in the condition 3182 //! @param[in] data user data for the callback 3183 //! @return whether the call was successful 3184 bool (*acyc_edge)(int node_u, int node_v, clingo_literal_t const *condition, size_t size, void *data); 3185 3186 //! Observe numeric theory terms. 3187 //! 3188 //! @param[in] term_id the id of the term 3189 //! @param[in] number the value of the term 3190 //! @param[in] data user data for the callback 3191 //! @return whether the call was successful 3192 bool (*theory_term_number)(clingo_id_t term_id, int number, void *data); 3193 //! Observe string theory terms. 3194 //! 3195 //! @param[in] term_id the id of the term 3196 //! @param[in] name the value of the term 3197 //! @param[in] data user data for the callback 3198 //! @return whether the call was successful 3199 bool (*theory_term_string)(clingo_id_t term_id, char const *name, void *data); 3200 //! Observe compound theory terms. 3201 //! 3202 //! The name_id_or_type gives the type of the compound term: 3203 //! - if it is -1, then it is a tuple 3204 //! - if it is -2, then it is a set 3205 //! - if it is -3, then it is a list 3206 //! - otherwise, it is a function and name_id_or_type refers to the id of the name (in form of a string term) 3207 //! 3208 //! @param[in] term_id the id of the term 3209 //! @param[in] name_id_or_type the name or type of the term 3210 //! @param[in] arguments the arguments of the term 3211 //! @param[in] size the number of arguments 3212 //! @param[in] data user data for the callback 3213 //! @return whether the call was successful 3214 bool (*theory_term_compound)(clingo_id_t term_id, int name_id_or_type, clingo_id_t const *arguments, size_t size, void *data); 3215 //! Observe theory elements. 3216 //! 3217 //! @param element_id the id of the element 3218 //! @param terms the term tuple of the element 3219 //! @param terms_size the number of terms in the tuple 3220 //! @param condition the condition of the elemnt 3221 //! @param condition_size the number of literals in the condition 3222 //! @param[in] data user data for the callback 3223 //! @return whether the call was successful 3224 bool (*theory_element)(clingo_id_t element_id, clingo_id_t const *terms, size_t terms_size, clingo_literal_t const *condition, size_t condition_size, void *data); 3225 //! Observe theory atoms without guard. 3226 //! 3227 //! @param[in] atom_id_or_zero the id of the atom or zero for directives 3228 //! @param[in] term_id the term associated with the atom 3229 //! @param[in] elements the elements of the atom 3230 //! @param[in] size the number of elements 3231 //! @param[in] data user data for the callback 3232 //! @return whether the call was successful 3233 bool (*theory_atom)(clingo_id_t atom_id_or_zero, clingo_id_t term_id, clingo_id_t const *elements, size_t size, void *data); 3234 //! Observe theory atoms with guard. 3235 //! 3236 //! @param[in] atom_id_or_zero the id of the atom or zero for directives 3237 //! @param[in] term_id the term associated with the atom 3238 //! @param[in] elements the elements of the atom 3239 //! @param[in] size the number of elements 3240 //! @param[in] operator_id the id of the operator (a string term) 3241 //! @param[in] right_hand_side_id the id of the term on the right hand side of the atom 3242 //! @param[in] data user data for the callback 3243 //! @return whether the call was successful 3244 bool (*theory_atom_with_guard)(clingo_id_t atom_id_or_zero, clingo_id_t term_id, clingo_id_t const *elements, size_t size, clingo_id_t operator_id, clingo_id_t right_hand_side_id, void *data); 3245 } clingo_ground_program_observer_t; 3246 3247 //! @} 3248 3249 // {{{1 control 3250 3251 //! @example control.c 3252 //! The example shows how to ground and solve a simple logic program, and print 3253 //! its answer sets. 3254 //! 3255 //! ## Output ## 3256 //! 3257 //! ~~~~~~~~~~~~ 3258 //! ./control 0 3259 //! Model: a 3260 //! Model: b 3261 //! ~~~~~~~~~~~~ 3262 //! 3263 //! ## Code ## 3264 3265 //! @defgroup Control Grounding and Solving 3266 //! Functions to control the grounding and solving process. 3267 //! 3268 //! For an example, see @ref control.c. 3269 3270 //! @addtogroup Control 3271 //! @{ 3272 3273 //! @enum clingo_solve_result_e 3274 //! Enumeration of bit masks for solve call results. 3275 //! 3276 //! @note Neither ::clingo_solve_result_satisfiable nor 3277 //! ::clingo_solve_result_exhausted is set if the search is interrupted and no 3278 //! model was found. 3279 //! 3280 //! @var clingo_solve_result::clingo_solve_result_satisfiable 3281 //! The last solve call found a solution. 3282 //! @var clingo_solve_result::clingo_solve_result_unsatisfiable 3283 //! The last solve call did not find a solution. 3284 //! @var clingo_solve_result::clingo_solve_result_exhausted 3285 //! The last solve call completely exhausted the search space. 3286 //! @var clingo_solve_result::clingo_solve_result_interrupted 3287 //! The last solve call was interrupted. 3288 //! 3289 //! @see clingo_control_interrupt() 3290 3291 //! @typedef clingo_solve_result_bitset_t 3292 //! Corresponding type to ::clingo_solve_result_e. 3293 3294 //! Struct used to specify the program parts that have to be grounded. 3295 //! 3296 //! Programs may be structured into parts, which can be grounded independently with ::clingo_control_ground. 3297 //! Program parts are mainly interesting for incremental grounding and multi-shot solving. 3298 //! For single-shot solving, program parts are not needed. 3299 //! 3300 //! @note Parts of a logic program without an explicit <tt>\#program</tt> 3301 //! specification are by default put into a program called `base` without 3302 //! arguments. 3303 //! 3304 //! @see clingo_control_ground() 3305 typedef struct clingo_part { 3306 char const *name; //!< name of the program part 3307 clingo_symbol_t const *params; //!< array of parameters 3308 size_t size; //!< number of parameters 3309 } clingo_part_t; 3310 3311 //! Callback function to implement external functions. 3312 //! 3313 //! If an external function of form <tt>\@name(parameters)</tt> occurs in a logic program, 3314 //! then this function is called with its location, name, parameters, and a callback to inject symbols as arguments. 3315 //! The callback can be called multiple times; all symbols passed are injected. 3316 //! 3317 //! If a (non-recoverable) clingo API function fails in this callback, for example, the symbol callback, the callback must return false. 3318 //! In case of errors not related to clingo, this function can set error ::clingo_error_unknown and return false to stop grounding with an error. 3319 //! 3320 //! @param[in] location location from which the external function was called 3321 //! @param[in] name name of the called external function 3322 //! @param[in] arguments arguments of the called external function 3323 //! @param[in] arguments_size number of arguments 3324 //! @param[in] data user data of the callback 3325 //! @param[in] symbol_callback function to inject symbols 3326 //! @param[in] symbol_callback_data user data for the symbol callback 3327 //! (must be passed untouched) 3328 //! @return whether the call was successful 3329 //! @see clingo_control_ground() 3330 //! 3331 //! The following example implements the external function <tt>\@f()</tt> returning 42. 3332 //! ~~~~~~~~~~~~~~~{.c} 3333 //! bool 3334 //! ground_callback(clingo_location_t const *location, 3335 //! char const *name, 3336 //! clingo_symbol_t const *arguments, 3337 //! size_t arguments_size, 3338 //! void *data, 3339 //! clingo_symbol_callback_t symbol_callback, 3340 //! void *symbol_callback_data) { 3341 //! if (strcmp(name, "f") == 0 && arguments_size == 0) { 3342 //! clingo_symbol_t sym; 3343 //! clingo_symbol_create_number(42, &sym); 3344 //! return symbol_callback(&sym, 1, symbol_callback_data); 3345 //! } 3346 //! clingo_set_error(clingo_error_runtime, "function not found"); 3347 //! return false; 3348 //! } 3349 //! ~~~~~~~~~~~~~~~ 3350 typedef bool (*clingo_ground_callback_t) (clingo_location_t const *location, char const *name, clingo_symbol_t const *arguments, size_t arguments_size, void *data, clingo_symbol_callback_t symbol_callback, void *symbol_callback_data); 3351 3352 //! Control object holding grounding and solving state. 3353 typedef struct clingo_control clingo_control_t; 3354 3355 //! Create a new control object. 3356 //! 3357 //! A control object has to be freed using clingo_control_free(). 3358 //! 3359 //! @note Only gringo options (without <code>\-\-output</code>) and clasp's options are supported as arguments, 3360 //! except basic options such as <code>\-\-help</code>. 3361 //! Furthermore, a control object is blocked while a search call is active; 3362 //! you must not call any member function during search. 3363 //! 3364 //! If the logger is NULL, messages are printed to stderr. 3365 //! 3366 //! @param[in] arguments C string array of command line arguments 3367 //! @param[in] arguments_size size of the arguments array 3368 //! @param[in] logger callback functions for warnings and info messages 3369 //! @param[in] logger_data user data for the logger callback 3370 //! @param[in] message_limit maximum number of times the logger callback is called 3371 //! @param[out] control resulting control object 3372 //! @return whether the call was successful; might set one of the following error codes: 3373 //! - ::clingo_error_bad_alloc 3374 //! - ::clingo_error_runtime if argument parsing fails 3375 CLINGO_VISIBILITY_DEFAULT bool clingo_control_new(char const *const * arguments, size_t arguments_size, clingo_logger_t logger, void *logger_data, unsigned message_limit, clingo_control_t **control); 3376 3377 //! Free a control object created with clingo_control_new(). 3378 //! @param[in] control the target 3379 CLINGO_VISIBILITY_DEFAULT void clingo_control_free(clingo_control_t *control); 3380 3381 //! @name Grounding Functions 3382 //! @{ 3383 3384 //! Extend the logic program with a program in a file. 3385 //! 3386 //! @param[in] control the target 3387 //! @param[in] file path to the file 3388 //! @return whether the call was successful; might set one of the following error codes: 3389 //! - ::clingo_error_bad_alloc 3390 //! - ::clingo_error_runtime if parsing or checking fails 3391 CLINGO_VISIBILITY_DEFAULT bool clingo_control_load(clingo_control_t *control, char const *file); 3392 3393 //! Extend the logic program with the given non-ground logic program in string form. 3394 //! 3395 //! This function puts the given program into a block of form: <tt>\#program name(parameters).</tt> 3396 //! 3397 //! After extending the logic program, the corresponding program parts are typically grounded with ::clingo_control_ground. 3398 //! 3399 //! @param[in] control the target 3400 //! @param[in] name name of the program block 3401 //! @param[in] parameters string array of parameters of the program block 3402 //! @param[in] parameters_size number of parameters 3403 //! @param[in] program string representation of the program 3404 //! @return whether the call was successful; might set one of the following error codes: 3405 //! - ::clingo_error_bad_alloc 3406 //! - ::clingo_error_runtime if parsing fails 3407 CLINGO_VISIBILITY_DEFAULT bool clingo_control_add(clingo_control_t *control, char const *name, char const * const * parameters, size_t parameters_size, char const *program); 3408 3409 //! Ground the selected @link ::clingo_part parts @endlink of the current (non-ground) logic program. 3410 //! 3411 //! After grounding, logic programs can be solved with ::clingo_control_solve(). 3412 //! 3413 //! @note Parts of a logic program without an explicit <tt>\#program</tt> 3414 //! specification are by default put into a program called `base` without 3415 //! arguments. 3416 //! 3417 //! @param[in] control the target 3418 //! @param[in] parts array of parts to ground 3419 //! @param[in] parts_size size of the parts array 3420 //! @param[in] ground_callback callback to implement external functions 3421 //! @param[in] ground_callback_data user data for ground_callback 3422 //! @return whether the call was successful; might set one of the following error codes: 3423 //! - ::clingo_error_bad_alloc 3424 //! - error code of ground callback 3425 //! 3426 //! @see clingo_part 3427 CLINGO_VISIBILITY_DEFAULT bool clingo_control_ground(clingo_control_t *control, clingo_part_t const *parts, size_t parts_size, clingo_ground_callback_t ground_callback, void *ground_callback_data); 3428 3429 //! @} 3430 3431 //! @name Solving Functions 3432 //! @{ 3433 3434 //! Solve the currently @link ::clingo_control_ground grounded @endlink logic program enumerating its models. 3435 //! 3436 //! See the @ref SolveHandle module for more information. 3437 //! 3438 //! @param[in] control the target 3439 //! @param[in] mode configures the search mode 3440 //! @param[in] assumptions array of assumptions to solve under 3441 //! @param[in] assumptions_size number of assumptions 3442 //! @param[in] notify the event handler to register 3443 //! @param[in] data the user data for the event handler 3444 //! @param[out] handle handle to the current search to enumerate models 3445 //! @return whether the call was successful; might set one of the following error codes: 3446 //! - ::clingo_error_bad_alloc 3447 //! - ::clingo_error_runtime if solving could not be started 3448 CLINGO_VISIBILITY_DEFAULT bool clingo_control_solve(clingo_control_t *control, clingo_solve_mode_bitset_t mode, clingo_literal_t const *assumptions, size_t assumptions_size, clingo_solve_event_callback_t notify, void *data, clingo_solve_handle_t **handle); 3449 //! Clean up the domains of the grounding component using the solving 3450 //! component's top level assignment. 3451 //! 3452 //! This function removes atoms from domains that are false and marks atoms as 3453 //! facts that are true. With multi-shot solving, this can result in smaller 3454 //! groundings because less rules have to be instantiated and more 3455 //! simplifications can be applied. 3456 //! 3457 //! @note It is typically not necessary to call this function manually because 3458 //! automatic cleanups at the right time are enabled by default. 3459 // 3460 //! @param[in] control the target 3461 //! @return whether the call was successful; might set one of the following error codes: 3462 //! - ::clingo_error_bad_alloc 3463 //! 3464 //! @see clingo_control_get_enable_cleanup() 3465 //! @see clingo_control_set_enable_cleanup() 3466 CLINGO_VISIBILITY_DEFAULT bool clingo_control_cleanup(clingo_control_t *control); 3467 //! Assign a truth value to an external atom. 3468 //! 3469 //! If a negative literal is passed, the corresponding atom is assigned the 3470 //! inverted truth value. 3471 //! 3472 //! If the atom does not exist or is not external, this is a noop. 3473 //! 3474 //! @param[in] control the target 3475 //! @param[in] literal literal to assign 3476 //! @param[in] value the truth value 3477 //! @return whether the call was successful; might set one of the following error codes: 3478 //! - ::clingo_error_bad_alloc 3479 CLINGO_VISIBILITY_DEFAULT bool clingo_control_assign_external(clingo_control_t *control, clingo_literal_t literal, clingo_truth_value_t value); 3480 //! Release an external atom. 3481 //! 3482 //! If a negative literal is passed, the corresponding atom is released. 3483 //! 3484 //! After this call, an external atom is no longer external and subject to 3485 //! program simplifications. If the atom does not exist or is not external, 3486 //! this is a noop. 3487 //! 3488 //! @param[in] control the target 3489 //! @param[in] literal literal to release 3490 //! @return whether the call was successful; might set one of the following error codes: 3491 //! - ::clingo_error_bad_alloc 3492 CLINGO_VISIBILITY_DEFAULT bool clingo_control_release_external(clingo_control_t *control, clingo_literal_t literal); 3493 //! Register a custom propagator with the control object. 3494 //! 3495 //! If the sequential flag is set to true, the propagator is called 3496 //! sequentially when solving with multiple threads. 3497 //! 3498 //! See the @ref Propagator module for more information. 3499 //! 3500 //! @param[in] control the target 3501 //! @param[in] propagator the propagator 3502 //! @param[in] data user data passed to the propagator functions 3503 //! @param[in] sequential whether the propagator should be called sequentially 3504 //! @return whether the call was successful; might set one of the following error codes: 3505 //! - ::clingo_error_bad_alloc 3506 CLINGO_VISIBILITY_DEFAULT bool clingo_control_register_propagator(clingo_control_t *control, clingo_propagator_t const *propagator, void *data, bool sequential); 3507 //! Check if the solver has determined that the internal program representation is conflicting. 3508 //! 3509 //! If this function returns true, solve calls will return immediately with an unsatisfiable solve result. 3510 //! Note that conflicts first have to be detected, e.g. - 3511 //! initial unit propagation results in an empty clause, 3512 //! or later if an empty clause is resolved during solving. 3513 //! Hence, the function might return false even if the problem is unsatisfiable. 3514 //! 3515 //! @param[in] control the target 3516 //! @return whether the program representation is conflicting 3517 CLINGO_VISIBILITY_DEFAULT bool clingo_control_is_conflicting(clingo_control_t const *control); 3518 3519 //! Get a statistics object to inspect solver statistics. 3520 //! 3521 //! Statistics are updated after a solve call. 3522 //! 3523 //! See the @ref Statistics module for more information. 3524 //! 3525 //! @attention 3526 //! The level of detail of the statistics depends on the stats option 3527 //! (which can be set using @ref Configuration module or passed as an option when @link clingo_control_new creating the control object@endlink). 3528 //! The default level zero only provides basic statistics, 3529 //! level one provides extended and accumulated statistics, 3530 //! and level two provides per-thread statistics. 3531 //! Furthermore, the statistics object is best accessed right after solving. 3532 //! Otherwise, not all of its entries have valid values. 3533 //! 3534 //! @param[in] control the target 3535 //! @param[out] statistics the statistics object 3536 //! @return whether the call was successful; might set one of the following error codes: 3537 //! - ::clingo_error_bad_alloc 3538 CLINGO_VISIBILITY_DEFAULT bool clingo_control_statistics(clingo_control_t const *control, clingo_statistics_t const **statistics); 3539 //! Interrupt the active solve call (or the following solve call right at the beginning). 3540 //! 3541 //! @param[in] control the target 3542 CLINGO_VISIBILITY_DEFAULT void clingo_control_interrupt(clingo_control_t *control); 3543 //! Get low-level access to clasp. 3544 //! 3545 //! @attention 3546 //! This function is intended for experimental use only and not part of the stable API. 3547 //! 3548 //! This function may return a <code>nullptr</code>. 3549 //! Otherwise, the returned pointer can be casted to a ClaspFacade pointer. 3550 //! 3551 //! @param[in] control the target 3552 //! @param[out] clasp pointer to the ClaspFacade object (may be <code>nullptr</code>) 3553 //! @return whether the call was successful 3554 CLINGO_VISIBILITY_DEFAULT bool clingo_control_clasp_facade(clingo_control_t *control, void **clasp); 3555 3556 //! @} 3557 3558 //! @name Configuration Functions 3559 //! @{ 3560 3561 //! Get a configuration object to change the solver configuration. 3562 //! 3563 //! See the @ref Configuration module for more information. 3564 //! 3565 //! @param[in] control the target 3566 //! @param[out] configuration the configuration object 3567 //! @return whether the call was successful 3568 CLINGO_VISIBILITY_DEFAULT bool clingo_control_configuration(clingo_control_t *control, clingo_configuration_t **configuration); 3569 3570 //! Configure how learnt constraints are handled during enumeration. 3571 //! 3572 //! If the enumeration assumption is enabled, then all information learnt from 3573 //! the solver's various enumeration modes is removed after a solve call. This 3574 //! includes enumeration of cautious or brave consequences, enumeration of 3575 //! answer sets with or without projection, or finding optimal models, as well 3576 //! as clauses added with clingo_solve_control_add_clause(). 3577 //! 3578 //! @attention For practical purposes, this option is only interesting for single-shot solving 3579 //! or before the last solve call to squeeze out a tiny bit of performance. 3580 //! Initially, the enumeration assumption is enabled. 3581 //! 3582 //! @param[in] control the target 3583 //! @param[in] enable whether to enable the assumption 3584 //! @return whether the call was successful 3585 CLINGO_VISIBILITY_DEFAULT bool clingo_control_set_enable_enumeration_assumption(clingo_control_t *control, bool enable); 3586 //! Check whether the enumeration assumption is enabled. 3587 //! 3588 //! See ::clingo_control_set_enable_enumeration_assumption(). 3589 //! @param[in] control the target 3590 //! @return whether using the enumeration assumption is enabled 3591 CLINGO_VISIBILITY_DEFAULT bool clingo_control_get_enable_enumeration_assumption(clingo_control_t *control); 3592 3593 //! Enable automatic cleanup after solving. 3594 //! 3595 //! @note Cleanup is enabled by default. 3596 //! 3597 //! @param[in] control the target 3598 //! @param[in] enable whether to enable cleanups 3599 //! @return whether the call was successful 3600 //! 3601 //! @see clingo_control_cleanup() 3602 //! @see clingo_control_get_enable_cleanup() 3603 CLINGO_VISIBILITY_DEFAULT bool clingo_control_set_enable_cleanup(clingo_control_t *control, bool enable); 3604 //! Check whether automatic cleanup is enabled. 3605 //! 3606 //! See ::clingo_control_set_enable_cleanup(). 3607 //! 3608 //! @param[in] control the target 3609 //! 3610 //! @see clingo_control_cleanup() 3611 //! @see clingo_control_set_enable_cleanup() 3612 CLINGO_VISIBILITY_DEFAULT bool clingo_control_get_enable_cleanup(clingo_control_t *control); 3613 3614 //! @} 3615 3616 //! @name Program Inspection Functions 3617 //! @{ 3618 3619 //! Return the symbol for a constant definition of form: <tt>\#const name = symbol</tt>. 3620 //! 3621 //! @param[in] control the target 3622 //! @param[in] name the name of the constant 3623 //! @param[out] symbol the resulting symbol 3624 //! @return whether the call was successful 3625 CLINGO_VISIBILITY_DEFAULT bool clingo_control_get_const(clingo_control_t const *control, char const *name, clingo_symbol_t *symbol); 3626 //! Check if there is a constant definition for the given constant. 3627 //! 3628 //! @param[in] control the target 3629 //! @param[in] name the name of the constant 3630 //! @param[out] exists whether a matching constant definition exists 3631 //! @return whether the call was successful; might set one of the following error codes: 3632 //! - ::clingo_error_runtime if constant definition does not exist 3633 //! 3634 //! @see clingo_control_get_const() 3635 CLINGO_VISIBILITY_DEFAULT bool clingo_control_has_const(clingo_control_t const *control, char const *name, bool *exists); 3636 //! Get an object to inspect symbolic atoms (the relevant Herbrand base) used 3637 //! for grounding. 3638 //! 3639 //! See the @ref SymbolicAtoms module for more information. 3640 //! 3641 //! @param[in] control the target 3642 //! @param[out] atoms the symbolic atoms object 3643 //! @return whether the call was successful 3644 CLINGO_VISIBILITY_DEFAULT bool clingo_control_symbolic_atoms(clingo_control_t const *control, clingo_symbolic_atoms_t const **atoms); 3645 //! Get an object to inspect theory atoms that occur in the grounding. 3646 //! 3647 //! See the @ref TheoryAtoms module for more information. 3648 //! 3649 //! @param[in] control the target 3650 //! @param[out] atoms the theory atoms object 3651 //! @return whether the call was successful 3652 CLINGO_VISIBILITY_DEFAULT bool clingo_control_theory_atoms(clingo_control_t const *control, clingo_theory_atoms_t const **atoms); 3653 //! Register a program observer with the control object. 3654 //! 3655 //! @param[in] control the target 3656 //! @param[in] observer the observer to register 3657 //! @param[in] replace just pass the grounding to the observer but not the solver 3658 //! @param[in] data user data passed to the observer functions 3659 //! @return whether the call was successful 3660 CLINGO_VISIBILITY_DEFAULT bool clingo_control_register_observer(clingo_control_t *control, clingo_ground_program_observer_t const *observer, bool replace, void *data); 3661 //! @} 3662 3663 //! @name Program Modification Functions 3664 //! @{ 3665 3666 //! Get an object to add ground directives to the program. 3667 //! 3668 //! See the @ref ProgramBuilder module for more information. 3669 //! 3670 //! @param[in] control the target 3671 //! @param[out] backend the backend object 3672 //! @return whether the call was successful; might set one of the following error codes: 3673 //! - ::clingo_error_bad_alloc 3674 CLINGO_VISIBILITY_DEFAULT bool clingo_control_backend(clingo_control_t *control, clingo_backend_t **backend); 3675 //! Get an object to add non-ground directives to the program. 3676 //! 3677 //! See the @ref ProgramBuilder module for more information. 3678 //! 3679 //! @param[in] control the target 3680 //! @param[out] builder the program builder object 3681 //! @return whether the call was successful 3682 CLINGO_VISIBILITY_DEFAULT bool clingo_control_program_builder(clingo_control_t *control, clingo_program_builder_t **builder); 3683 //! @} 3684 3685 //! @} 3686 3687 // {{{1 extending clingo 3688 3689 //! @example application.c 3690 //! The example shows how to extend the clingo application. 3691 //! 3692 //! It behaves like a normal normal clingo but adds one option to override the default program part to ground. 3693 //! ## Example calls ## 3694 //! 3695 //! ~~~~~~~~~~~~ 3696 //! $ cat example.lp 3697 //! b. 3698 //! #program test. 3699 //! t. 3700 //! 3701 //! $ ./application --program test example.lp 3702 //! example version 1.0.0 3703 //! Reading from example.lp 3704 //! Solving... 3705 //! Answer: 1 3706 //! t 3707 //! SATISFIABLE 3708 //! 3709 //! Models : 1+ 3710 //! Calls : 1 3711 //! Time : 0.004s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) 3712 //! CPU Time : 0.004s 3713 //! ~~~~~~~~~~~~ 3714 //! 3715 //! ## Code ## 3716 3717 //! @defgroup ExtendingClingo Extending Clingo 3718 //! Functions to customize clingo's main function. 3719 //! 3720 //! This module allows for customizing the clingo application. 3721 //! For example, this can be used to register custom propagators and command line options with clingo. 3722 //! 3723 //! Warning: This part of the API is not yet finalized and might change in the future. 3724 3725 //! @addtogroup ExtendingClingo 3726 //! @{ 3727 3728 //! Object to add command-line options. 3729 typedef struct clingo_options clingo_options_t; 3730 3731 //! Callback to customize clingo main function. 3732 //! 3733 //! @param[in] control corresponding control object 3734 //! @param[in] files files passed via command line arguments 3735 //! @param[in] size number of files 3736 //! @param[in] data user data for the callback 3737 //! 3738 //! @return whether the call was successful 3739 typedef bool (*clingo_main_function_t) (clingo_control_t *control, char const *const * files, size_t size, void *data); 3740 3741 //! Callback to print a model in default format. 3742 //! 3743 //! @param[in] data user data for the callback 3744 //! 3745 //! @return whether the call was successful 3746 typedef bool (*clingo_default_model_printer_t) (void *data); 3747 3748 //! Callback to customize model printing. 3749 //! 3750 //! @param[in] model the model 3751 //! @param[in] printer the default model printer 3752 //! @param[in] printer_data user data for the printer 3753 //! @param[in] data user data for the callback 3754 //! 3755 //! @return whether the call was successful 3756 typedef bool (*clingo_model_printer_t) (clingo_model_t const *model, clingo_default_model_printer_t printer, void *printer_data, void *data); 3757 3758 //! This struct contains a set of functions to customize the clingo application. 3759 typedef struct clingo_application { 3760 char const *(*program_name) (void *data); //!< callback to obtain program name 3761 char const *(*version) (void *data); //!< callback to obtain version information 3762 unsigned (*message_limit) (void *data); //!< callback to obtain message limit 3763 clingo_main_function_t main; //!< callback to override clingo's main function 3764 clingo_logger_t logger; //!< callback to override default logger 3765 clingo_model_printer_t printer; //!< callback to override default model printing 3766 bool (*register_options)(clingo_options_t *options, void *data); //!< callback to register options 3767 bool (*validate_options)(void *data); //!< callback validate options 3768 } clingo_application_t; 3769 3770 //! Add an option that is processed with a custom parser. 3771 //! 3772 //! Note that the parser also has to take care of storing the semantic value of 3773 //! the option somewhere. 3774 //! 3775 //! Parameter option specifies the name(s) of the option. 3776 //! For example, "ping,p" adds the short option "-p" and its long form "--ping". 3777 //! It is also possible to associate an option with a help level by adding ",@l" to the option specification. 3778 //! Options with a level greater than zero are only shown if the argument to help is greater or equal to l. 3779 //! 3780 //! @param[in] options object to register the option with 3781 //! @param[in] group options are grouped into sections as given by this string 3782 //! @param[in] option specifies the command line option 3783 //! @param[in] description the description of the option 3784 //! @param[in] parse callback to parse the value of the option 3785 //! @param[in] data user data for the callback 3786 //! @param[in] multi whether the option can appear multiple times on the command-line 3787 //! @param[in] argument optional string to change the value name in the generated help output 3788 //! @return whether the call was successful 3789 CLINGO_VISIBILITY_DEFAULT bool clingo_options_add(clingo_options_t *options, char const *group, char const *option, char const *description, bool (*parse) (char const *value, void *data), void *data, bool multi, char const *argument); 3790 //! Add an option that is a simple flag. 3791 //! 3792 //! This function is similar to @ref clingo_options_add() but simpler because it only supports flags, which do not have values. 3793 //! If a flag is passed via the command-line the parameter target is set to true. 3794 //! 3795 //! @param[in] options object to register the option with 3796 //! @param[in] group options are grouped into sections as given by this string 3797 //! @param[in] option specifies the command line option 3798 //! @param[in] description the description of the option 3799 //! @param[in] target boolean set to true if the flag is given on the command-line 3800 //! @return whether the call was successful 3801 CLINGO_VISIBILITY_DEFAULT bool clingo_options_add_flag(clingo_options_t *options, char const *group, char const *option, char const *description, bool *target); 3802 3803 //! Run clingo with a customized main function (similar to python and lua embedding). 3804 //! 3805 //! @param[in] application struct with callbacks to override default clingo functionality 3806 //! @param[in] arguments command line arguments 3807 //! @param[in] size number of arguments 3808 //! @param[in] data user data to pass to callbacks in application 3809 //! @return exit code to return from main function 3810 CLINGO_VISIBILITY_DEFAULT int clingo_main(clingo_application_t *application, char const *const * arguments, size_t size, void *data); 3811 3812 //! Custom scripting language to run functions during grounding. 3813 typedef struct clingo_script { 3814 //! Evaluate the given source code. 3815 //! @param[in] location the location in the logic program of the source code 3816 //! @param[in] code the code to evaluate 3817 //! @param[in] data user data as given when registering the script 3818 //! @return whether the function call was successful 3819 bool (*execute) (clingo_location_t const *location, char const *code, void *data); 3820 //! Call the function with the given name and arguments. 3821 //! @param[in] location the location in the logic program of the function call 3822 //! @param[in] name the name of the function 3823 //! @param[in] arguments the arguments to the function 3824 //! @param[in] arguments_size the number of arguments 3825 //! @param[in] symbol_callback callback to return a pool of symbols 3826 //! @param[in] symbol_callback_data user data for the symbol callback 3827 //! @param[in] data user data as given when registering the script 3828 //! @return whether the function call was successful 3829 bool (*call) (clingo_location_t const *location, char const *name, clingo_symbol_t const *arguments, size_t arguments_size, clingo_symbol_callback_t symbol_callback, void *symbol_callback_data, void *data); 3830 //! Check if the given function is callable. 3831 //! @param[in] name the name of the function 3832 //! @param[out] result whether the function is callable 3833 //! @param[in] data user data as given when registering the script 3834 //! @return whether the function call was successful 3835 bool (*callable) (char const * name, bool *result, void *data); 3836 //! Run the main function. 3837 //! @param[in] control the control object to pass to the main function 3838 //! @param[in] data user data as given when registering the script 3839 //! @return whether the function call was successful 3840 bool (*main) (clingo_control_t *control, void *data); 3841 //! This function is called once when the script is deleted. 3842 //! @param[in] data user data as given when registering the script 3843 void (*free) (void *data); 3844 char const *version; 3845 } clingo_script_t; 3846 3847 //! Add a custom scripting language to clingo. 3848 //! 3849 //! @param[in] name the name of the scripting language 3850 //! @param[in] script struct with functions implementing the language 3851 //! @param[in] data user data to pass to callbacks in the script 3852 //! @return whether the call was successful 3853 CLINGO_VISIBILITY_DEFAULT bool clingo_register_script(char const *name, clingo_script_t const *script, void *data); 3854 //! Get the version of the registered scripting language. 3855 //! 3856 //! @param[in] name the name of the scripting language 3857 //! @return the version 3858 CLINGO_VISIBILITY_DEFAULT char const *clingo_script_version(char const *name); 3859 3860 //! @} 3861 3862 // }}}1 3863 3864 #ifdef __cplusplus 3865 } 3866 #endif 3867 3868 #endif 3869