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