1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2017 SRI International. 4 * 5 * Yices is free software: you can redistribute it and/or modify 6 * it under the terms of the GNU General Public License as published by 7 * the Free Software Foundation, either version 3 of the License, or 8 * (at your option) any later version. 9 * 10 * Yices is distributed in the hope that it will be useful, 11 * but WITHOUT ANY WARRANTY; without even the implied warranty of 12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 * GNU General Public License for more details. 14 * 15 * You should have received a copy of the GNU General Public License 16 * along with Yices. If not, see <http://www.gnu.org/licenses/>. 17 */ 18 19 /* 20 * PUBLIC TYPES 21 * 22 * All types that are part of the API must be defined here. 23 */ 24 25 #ifndef __YICES_TYPES_H 26 #define __YICES_TYPES_H 27 28 #include <stdint.h> 29 30 31 /********************* 32 * TERMS AND TYPES * 33 ********************/ 34 35 /* 36 * Exported types 37 * - term = index in a term table 38 * - type = index in a type table 39 */ 40 typedef int32_t term_t; 41 typedef int32_t type_t; 42 43 /* 44 * Error values 45 */ 46 #define NULL_TERM (-1) 47 #define NULL_TYPE (-1) 48 49 50 51 /************************ 52 * CONTEXT AND MODELS * 53 ***********************/ 54 55 /* 56 * Context and models (opaque types) 57 */ 58 typedef struct context_s context_t; 59 typedef struct model_s model_t; 60 61 62 /* 63 * Context configuration (opaque type) 64 */ 65 typedef struct ctx_config_s ctx_config_t; 66 67 68 /* 69 * Search parameters (opaque type) 70 */ 71 typedef struct param_s param_t; 72 73 74 /* 75 * Context status code 76 */ 77 typedef enum smt_status { 78 STATUS_IDLE, 79 STATUS_SEARCHING, 80 STATUS_UNKNOWN, 81 STATUS_SAT, 82 STATUS_UNSAT, 83 STATUS_INTERRUPTED, 84 STATUS_ERROR 85 } smt_status_t; 86 87 88 89 90 91 /******************************** 92 * VECTORS OF TERMS OR TYPES * 93 *******************************/ 94 95 /* 96 * Some functions return a collection of terms or types 97 * via a vector. The vector is an array that gets resized 98 * by the library as needed. 99 * 100 * For each vector type, the API provide three functions: 101 * - yices_init_xxx_vector(xxx_vector_t *v) 102 * - yices_reset_xxx_vector(xxx_vector_t *v) 103 * - yices_delete_xxx_vector(xxx_vector_t *v) 104 * 105 * The first function must be called first to initialize a vector. 106 * The reset function can be used to empty vector v. It just resets 107 * v->size to zero. 108 * The delete function must be called to delete a vector that is no 109 * longer needed. This is required to avoid memory leaks. 110 */ 111 typedef struct term_vector_s { 112 uint32_t capacity; 113 uint32_t size; 114 term_t *data; 115 } term_vector_t; 116 117 typedef struct type_vector_s { 118 uint32_t capacity; 119 uint32_t size; 120 type_t *data; 121 } type_vector_t; 122 123 124 125 /*********************** 126 * TERM CONSTRUCTORS * 127 **********************/ 128 129 /* 130 * These codes are part of the term exploration API. 131 */ 132 typedef enum term_constructor { 133 YICES_CONSTRUCTOR_ERROR = -1, // to report an error 134 135 // atomic terms 136 YICES_BOOL_CONSTANT, // boolean constant 137 YICES_ARITH_CONSTANT, // rational constant 138 YICES_BV_CONSTANT, // bitvector constant 139 YICES_SCALAR_CONSTANT, // constant of uninterpreted/scalar 140 YICES_VARIABLE, // variable in quantifiers 141 YICES_UNINTERPRETED_TERM, // (i.e., global variables, can't be bound) 142 143 // composite terms 144 YICES_ITE_TERM, // if-then-else 145 YICES_APP_TERM, // application of an uninterpreted function 146 YICES_UPDATE_TERM, // function update 147 YICES_TUPLE_TERM, // tuple constructor 148 YICES_EQ_TERM, // equality 149 YICES_DISTINCT_TERM, // distinct t_1 ... t_n 150 YICES_FORALL_TERM, // quantifier 151 YICES_LAMBDA_TERM, // lambda 152 YICES_NOT_TERM, // (not t) 153 YICES_OR_TERM, // n-ary OR 154 YICES_XOR_TERM, // n-ary XOR 155 156 YICES_BV_ARRAY, // array of boolean terms 157 YICES_BV_DIV, // unsigned division 158 YICES_BV_REM, // unsigned remainder 159 YICES_BV_SDIV, // signed division 160 YICES_BV_SREM, // remainder in signed division (rounding to 0) 161 YICES_BV_SMOD, // remainder in signed division (rounding to -infinity) 162 YICES_BV_SHL, // shift left (padding with 0) 163 YICES_BV_LSHR, // logical shift right (padding with 0) 164 YICES_BV_ASHR, // arithmetic shift right (padding with sign bit) 165 YICES_BV_GE_ATOM, // unsigned comparison: (t1 >= t2) 166 YICES_BV_SGE_ATOM, // signed comparison (t1 >= t2) 167 YICES_ARITH_GE_ATOM, // atom (t1 >= t2) for arithmetic terms: t2 is always 0 168 YICES_ARITH_ROOT_ATOM, // atom (0 <= k <= root_count(p)) && (x r root(p, k)) for r in <, <=, ==, !=, >, >= 169 170 171 YICES_ABS, // absolute value 172 YICES_CEIL, // ceil 173 YICES_FLOOR, // floor 174 YICES_RDIV, // real division (as in x/y) 175 YICES_IDIV, // integer division 176 YICES_IMOD, // modulo 177 YICES_IS_INT_ATOM, // integrality test: (is-int t) 178 YICES_DIVIDES_ATOM, // divisibility test: (divides t1 t2) 179 180 // projections 181 YICES_SELECT_TERM, // tuple projection 182 YICES_BIT_TERM, // bit-select: extract the i-th bit of a bitvector 183 184 // sums 185 YICES_BV_SUM, // sum of pairs a * t where a is a bitvector constant (and t is a bitvector term) 186 YICES_ARITH_SUM, // sum of pairs a * t where a is a rational (and t is an arithmetic term) 187 188 // products 189 YICES_POWER_PRODUCT // power products: (t1^d1 * ... * t_n^d_n) 190 } term_constructor_t; 191 192 193 /********************** 194 * VALUES IN MODELS * 195 *********************/ 196 197 /* 198 * A model maps terms to constant objects that can be 199 * atomic values, tuples, or functions. These different 200 * objects form a DAG. The API provides functions to 201 * explore this DAG. Every node in this DAG is defined 202 * by a unique id and a tag that identifies the node type. 203 * 204 * Atomic nodes have one of the following tags: 205 * YVAL_UNKNOWN (special marker) 206 * YVAL_BOOL Boolean constant 207 * YVAL_RATIONAL Rational constant 208 * YVAL_ALGEBRAIC Algebraic number 209 * YVAL_BV Bitvector constant 210 * YVAL_SCALAR Constant of uninterpreted or scalar type 211 * 212 * Non-leaf nodes: 213 * YVAL_TUPLE Tuple 214 * YVAL_FUNCTION Function 215 * YVAL_MAPPING A pair [tuple -> value]. 216 * 217 * All functions are defined by a finite set of mappings 218 * and a default value. For example, if we have 219 * f(0, 0) = 0 220 * f(0, 1) = 1 221 * f(1, 0) = 1 222 * f(1, 1) = 2 223 * f(x, y) = 2 if x and y are different from 0 and 1 224 * 225 * Then f will be represented as follows: 226 * - default value = 2 227 * - mappings: 228 * [0, 0 -> 0] 229 * [0, 1 -> 1] 230 * [1, 0 -> 1] 231 * 232 * In the DAG, there is one node for f, one node for the default value, 233 * and three nodes for each of the three mappings. 234 */ 235 236 // Tags for the node descriptors 237 typedef enum yval_tag { 238 YVAL_UNKNOWN, 239 YVAL_BOOL, 240 YVAL_RATIONAL, 241 YVAL_ALGEBRAIC, 242 YVAL_BV, 243 YVAL_SCALAR, 244 YVAL_TUPLE, 245 YVAL_FUNCTION, 246 YVAL_MAPPING 247 } yval_tag_t; 248 249 // Node descriptor 250 typedef struct yval_s { 251 int32_t node_id; 252 yval_tag_t node_tag; 253 } yval_t; 254 255 // Vector of node descriptors 256 typedef struct yval_vector_s { 257 uint32_t capacity; 258 uint32_t size; 259 yval_t *data; 260 } yval_vector_t; 261 262 263 264 /************************* 265 * MODEL GENERALIZATION * 266 ************************/ 267 268 /* 269 * These codes define a generalization algorithm for functions 270 * yices_generalize_model 271 * and yices_generalize_model_array 272 * 273 * There are currently two algorithms: generalization by 274 * substitution and generalization by projection. 275 * The default is to select the algorithm based on variables 276 * to eliminate. 277 */ 278 typedef enum yices_gen_mode { 279 YICES_GEN_DEFAULT, 280 YICES_GEN_BY_SUBST, 281 YICES_GEN_BY_PROJ 282 } yices_gen_mode_t; 283 284 285 286 /***************** 287 * ERROR CODES * 288 ****************/ 289 290 /* 291 * Error reports 292 * - the API function return a default value if there's an error 293 * (e.g., term constructors return NULL_TERM, type constructors return NULL_TYPE). 294 * - details about the cause of the error are stored in an error_report structure 295 * defined below. 296 * - the error report contains an error code and extra information 297 * that depends on the error code. 298 */ 299 typedef enum error_code { 300 NO_ERROR = 0, 301 302 /* 303 * Errors in type or term construction 304 */ 305 INVALID_TYPE, 306 INVALID_TERM, 307 INVALID_CONSTANT_INDEX, 308 INVALID_VAR_INDEX, // Not used anymore 309 INVALID_TUPLE_INDEX, 310 INVALID_RATIONAL_FORMAT, 311 INVALID_FLOAT_FORMAT, 312 INVALID_BVBIN_FORMAT, 313 INVALID_BVHEX_FORMAT, 314 INVALID_BITSHIFT, 315 INVALID_BVEXTRACT, 316 INVALID_BITEXTRACT, // added 2014/02/17 317 TOO_MANY_ARGUMENTS, 318 TOO_MANY_VARS, 319 MAX_BVSIZE_EXCEEDED, 320 DEGREE_OVERFLOW, 321 DIVISION_BY_ZERO, 322 POS_INT_REQUIRED, 323 NONNEG_INT_REQUIRED, 324 SCALAR_OR_UTYPE_REQUIRED, 325 FUNCTION_REQUIRED, 326 TUPLE_REQUIRED, 327 VARIABLE_REQUIRED, 328 ARITHTERM_REQUIRED, 329 BITVECTOR_REQUIRED, 330 SCALAR_TERM_REQUIRED, 331 WRONG_NUMBER_OF_ARGUMENTS, 332 TYPE_MISMATCH, 333 INCOMPATIBLE_TYPES, 334 DUPLICATE_VARIABLE, 335 INCOMPATIBLE_BVSIZES, 336 EMPTY_BITVECTOR, 337 ARITHCONSTANT_REQUIRED, // added 2013/01/23 338 INVALID_MACRO, // added 2013/03/31 339 TOO_MANY_MACRO_PARAMS, // added 2013/03/31 340 TYPE_VAR_REQUIRED, // added 2013/03/31 341 DUPLICATE_TYPE_VAR, // added 2013/03/31 342 BVTYPE_REQUIRED, // added 2013/05/27 343 BAD_TERM_DECREF, // added 2013/10/03 344 BAD_TYPE_DECREF, // added 2013/10/03 345 INVALID_TYPE_OP, // added 2014/12/03 346 INVALID_TERM_OP, // added 2014/12/04 347 348 /* 349 * Parser errors 350 */ 351 INVALID_TOKEN = 100, 352 SYNTAX_ERROR, 353 UNDEFINED_TYPE_NAME, 354 UNDEFINED_TERM_NAME, 355 REDEFINED_TYPE_NAME, 356 REDEFINED_TERM_NAME, 357 DUPLICATE_NAME_IN_SCALAR, 358 DUPLICATE_VAR_NAME, 359 INTEGER_OVERFLOW, 360 INTEGER_REQUIRED, 361 RATIONAL_REQUIRED, 362 SYMBOL_REQUIRED, 363 TYPE_REQUIRED, 364 NON_CONSTANT_DIVISOR, 365 NEGATIVE_BVSIZE, 366 INVALID_BVCONSTANT, 367 TYPE_MISMATCH_IN_DEF, 368 ARITH_ERROR, 369 BVARITH_ERROR, 370 371 372 /* 373 * Errors in assertion processing. 374 * These codes mean that the context, as configured, 375 * cannot process the assertions. 376 */ 377 CTX_FREE_VAR_IN_FORMULA = 300, 378 CTX_LOGIC_NOT_SUPPORTED, 379 CTX_UF_NOT_SUPPORTED, 380 CTX_ARITH_NOT_SUPPORTED, 381 CTX_BV_NOT_SUPPORTED, 382 CTX_ARRAYS_NOT_SUPPORTED, 383 CTX_QUANTIFIERS_NOT_SUPPORTED, 384 CTX_LAMBDAS_NOT_SUPPORTED, 385 CTX_NONLINEAR_ARITH_NOT_SUPPORTED, 386 CTX_FORMULA_NOT_IDL, 387 CTX_FORMULA_NOT_RDL, 388 CTX_TOO_MANY_ARITH_VARS, 389 CTX_TOO_MANY_ARITH_ATOMS, 390 CTX_TOO_MANY_BV_VARS, 391 CTX_TOO_MANY_BV_ATOMS, 392 CTX_ARITH_SOLVER_EXCEPTION, 393 CTX_BV_SOLVER_EXCEPTION, 394 CTX_ARRAY_SOLVER_EXCEPTION, 395 CTX_SCALAR_NOT_SUPPORTED, // added 2015/03/26 396 CTX_TUPLE_NOT_SUPPORTED, // added 2015/03/26 397 CTX_UTYPE_NOT_SUPPORTED, // added 2015/03/26 398 399 400 /* 401 * Error codes for other operations 402 */ 403 CTX_INVALID_OPERATION = 400, 404 CTX_OPERATION_NOT_SUPPORTED, 405 406 /* 407 * Error codes for delegates 408 * 409 * Since 2.6.2. 410 */ 411 CTX_UNKNOWN_DELEGATE = 420, 412 CTX_DELEGATE_NOT_AVAILABLE, 413 414 /* 415 * Errors in context configurations and search parameter settings 416 */ 417 CTX_INVALID_CONFIG = 500, 418 CTX_UNKNOWN_PARAMETER, 419 CTX_INVALID_PARAMETER_VALUE, 420 CTX_UNKNOWN_LOGIC, 421 422 /* 423 * Error codes for model queries 424 */ 425 EVAL_UNKNOWN_TERM = 600, 426 EVAL_FREEVAR_IN_TERM, 427 EVAL_QUANTIFIER, 428 EVAL_LAMBDA, 429 EVAL_OVERFLOW, 430 EVAL_FAILED, 431 EVAL_CONVERSION_FAILED, 432 EVAL_NO_IMPLICANT, 433 EVAL_NOT_SUPPORTED, 434 435 /* 436 * Error codes for model construction 437 */ 438 MDL_UNINT_REQUIRED = 700, 439 MDL_CONSTANT_REQUIRED, 440 MDL_DUPLICATE_VAR, 441 MDL_FTYPE_NOT_ALLOWED, 442 MDL_CONSTRUCTION_FAILED, 443 444 /* 445 * Error codes in DAG/node queries 446 */ 447 YVAL_INVALID_OP = 800, 448 YVAL_OVERFLOW, 449 YVAL_NOT_SUPPORTED, 450 451 /* 452 * Error codes for model generalization 453 */ 454 MDL_GEN_TYPE_NOT_SUPPORTED = 900, 455 MDL_GEN_NONLINEAR, 456 MDL_GEN_FAILED, 457 458 /* 459 * MCSAT error codes 460 */ 461 MCSAT_ERROR_UNSUPPORTED_THEORY = 1000, 462 463 /* 464 * Input/output and system errors 465 */ 466 OUTPUT_ERROR = 9000, 467 468 /* 469 * Catch-all code for anything else. 470 * This is a symptom that a bug has been found. 471 */ 472 INTERNAL_EXCEPTION = 9999 473 } error_code_t; 474 475 476 477 /* 478 * Error report = a code + line and column + 1 or 2 terms + 1 or 2 types 479 * + an (erroneous) integer value. 480 * 481 * The yices API returns a negative number and set an error code on 482 * error. The fields other than the error code depend on the code. In 483 * addition, the parsing functions (yices_parse_type and 484 * yices_parse_term) set the line/column fields on error. 485 * 486 * error code meaningful fields 487 * 488 * NO_ERROR none 489 * 490 * INVALID_TYPE type1 491 * INVALID_TERM term1 492 * INVALID_CONSTANT_INDEX type1, badval 493 * INVALID_VAR_INDEX badval 494 * INVALID_TUPLE_INDEX type1, badval 495 * INVALID_RATIONAL_FORMAT none 496 * INVALID_FLOAT_FORMAT none 497 * INVALID_BVBIN_FORMAT none 498 * INVALID_BVHEX_FORMAT none 499 * INVALID_BITSHIFT badval 500 * INVALID_BVEXTRACT none 501 * INVALID_BITEXTRACT none 502 * TOO_MANY_ARGUMENTS badval 503 * TOO_MANY_VARS badval 504 * MAX_BVSIZE_EXCEEDED badval 505 * DEGREE_OVERFLOW badval 506 * DIVISION_BY_ZERO none 507 * POS_INT_REQUIRED badval 508 * NONNEG_INT_REQUIRED none 509 * SCALAR_OR_UTYPE_REQUIRED type1 510 * FUNCTION_REQUIRED term1 511 * TUPLE_REQUIRED term1 512 * VARIABLE_REQUIRED term1 513 * ARITHTERM_REQUIRED term1 514 * BITVECTOR_REQUIRED term1 515 * SCALAR_TERM_REQUIRED term1 516 * WRONG_NUMBER_OF_ARGUMENTS type1, badval 517 * TYPE_MISMATCH term1, type1 518 * INCOMPATIBLE_TYPES term1, type1, term2, type2 519 * DUPLICATE_VARIABLE term1 520 * INCOMPATIBLE_BVSIZES term1, type1, term2, type2 521 * EMPTY_BITVECTOR none 522 * ARITHCONSTANT_REQUIRED term1 523 * INVALID_MACRO badval 524 * TOO_MANY_MACRO_PARAMS badval 525 * TYPE_VAR_REQUIRED type1 526 * DUPLICATE_TYPE_VAR type1 527 * BVTYPE_REQUIRED type1 528 * BAD_TERM_DECREF term1 529 * BAD_TYPE_DECREF type1 530 * 531 * The following error codes are used only by the parsing functions. 532 * No field other than line/column is set. 533 * 534 * INVALID_TOKEN 535 * SYNTAX_ERROR 536 * UNDEFINED_TERM_NAME 537 * UNDEFINED_TYPE_NAME 538 * REDEFINED_TERM_NAME 539 * REDEFINED_TYPE_NAME 540 * DUPLICATE_NAME_IN_SCALAR 541 * DUPLICATE_VAR_NAME 542 * INTEGER_OVERFLOW 543 * INTEGER_REQUIRED 544 * RATIONAL_REQUIRED 545 * SYMBOL_REQUIRED 546 * TYPE_REQUIRED 547 * NON_CONSTANT_DIVISOR 548 * NEGATIVE_BVSIZE 549 * INVALID_BVCONSTANT 550 * TYPE_MISMATCH_IN_DEF 551 * ARITH_ERROR 552 * BVARITH_ERROR 553 * 554 * The following error codes are triggered by invalid operations 555 * on a context. For these errors, no fields of error_report (other 556 * than the code) is meaningful. 557 * 558 * CTX_FREE_VAR_IN_FORMULA 559 * CTX_LOGIC_NOT_SUPPORTED 560 * CTX_UF_NOT_SUPPORTED 561 * CTX_ARITH_NOT_SUPPORTED 562 * CTX_BV_NOT_SUPPORTED 563 * CTX_ARRAYS_NOT_SUPPORTED 564 * CTX_QUANTIFIERS_NOT_SUPPORTED 565 * CTX_LAMBDAS_NOT_SUPPORTED 566 * CTX_NONLINEAR_ARITH_NOT_SUPPORTED 567 * CTX_FORMULA_NOT_IDL 568 * CTX_FORMULA_NOT_RDL 569 * CTX_TOO_MANY_ARITH_VARS 570 * CTX_TOO_MANY_ARITH_ATOMS 571 * CTX_TOO_MANY_BV_VARS 572 * CTX_TOO_MANY_BV_ATOMS 573 * CTX_ARITH_SOLVER_EXCEPTION 574 * CTX_BV_SOLVER_EXCEPTION 575 * CTX_ARRAY_SOLVER_EXCEPTION 576 * CTX_SCALAR_NOT_SUPPORTED, 577 * CTX_TUPLE_NOT_SUPPORTED, 578 * CTX_UTYPE_NOT_SUPPORTED, 579 * 580 * CTX_INVALID_OPERATION 581 * CTX_OPERATION_NOT_SUPPORTED 582 * 583 * CTX_UNKNOWN_DELEGATE 584 * CTX_DELEGATE_NOT_AVAILABLE 585 * 586 * CTX_INVALID_CONFIG 587 * CTX_UNKNOWN_PARAMETER 588 * CTX_INVALID_PARAMETER_VALUE 589 * CTX_UNKNOWN_LOGIC 590 * 591 * 592 * Errors for functions that operate on a model (i.e., evaluate 593 * terms in a model). 594 * EVAL_UNKNOWN_TERM 595 * EVAL_FREEVAR_IN_TERM 596 * EVAL_QUANTIFIER 597 * EVAL_LAMBDA 598 * EVAL_OVERFLOW 599 * EVAL_FAILED 600 * EVAL_CONVERSION_FAILED 601 * EVAL_NO_IMPLICANT 602 * 603 * 604 * Other error codes. No field is meaningful in the error_report, 605 * except the error code: 606 * 607 * OUTPUT_ERROR 608 * INTERNAL_EXCEPTION 609 */ 610 typedef struct error_report_s { 611 error_code_t code; 612 uint32_t line; 613 uint32_t column; 614 term_t term1; 615 type_t type1; 616 term_t term2; 617 type_t type2; 618 int64_t badval; 619 } error_report_t; 620 621 #endif /* YICES_TYPES_H */ 622