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 * CONTEXT 21 */ 22 23 #ifndef __CONTEXT_TYPES_H 24 #define __CONTEXT_TYPES_H 25 26 #include <stdint.h> 27 #include <stdbool.h> 28 #include <setjmp.h> 29 30 #include "api/smt_logic_codes.h" 31 #include "context/assumption_stack.h" 32 #include "context/common_conjuncts.h" 33 #include "context/divmod_table.h" 34 #include "context/internalization_table.h" 35 #include "context/pseudo_subst.h" 36 #include "context/shared_terms.h" 37 #include "io/tracer.h" 38 #include "solvers/cdcl/gates_manager.h" 39 #include "solvers/cdcl/smt_core.h" 40 #include "solvers/egraph/egraph.h" 41 #include "terms/bvpoly_buffers.h" 42 #include "terms/conditionals.h" 43 #include "terms/int_rational_hash_maps.h" 44 #include "terms/poly_buffer.h" 45 #include "terms/terms.h" 46 #include "utils/int_bv_sets.h" 47 #include "utils/int_hash_sets.h" 48 #include "utils/int_queues.h" 49 #include "utils/int_stack.h" 50 #include "utils/int_vectors.h" 51 #include "utils/mark_vectors.h" 52 #include "utils/pair_hash_map2.h" 53 54 #include "mcsat/solver.h" 55 56 /*********************** 57 * OPTIONAL FEATURES * 58 **********************/ 59 60 /* 61 * Bit mask for specifying which features are supported by a context. 62 * These are set when the context is created. 63 */ 64 #define MULTICHECKS_OPTION_MASK 0x1 65 #define PUSHPOP_OPTION_MASK 0x2 66 #define CLEANINT_OPTION_MASK 0x4 67 68 69 /* 70 * Possible modes: each mode defines which of the three above 71 * bits are set. 72 */ 73 typedef enum { 74 CTX_MODE_ONECHECK, 75 CTX_MODE_MULTICHECKS, 76 CTX_MODE_PUSHPOP, 77 CTX_MODE_INTERACTIVE, 78 } context_mode_t; 79 80 #define NUM_MODES (CTX_MODE_INTERACTIVE+1) 81 82 83 /* 84 * Possible solver classes. 85 */ 86 typedef enum { 87 CTX_SOLVER_TYPE_DPLLT, 88 CTX_SOLVER_TYPE_MCSAT, 89 } context_solver_type_t; 90 91 #define NUM_SOLVER_TYPES (CTX_SOLVER_TYPE_MCSAT+1) 92 93 /* 94 * More bit masks for enabling/disabling simplification 95 * - VARELIM eliminate variables (via substitution) 96 * - FLATTENOR rewrites (or ... (or ...) ...) into a single (or ....) 97 * - FLATTENDISEQ rewrite arithmetic disequality 98 * (not (p == 0)) into (or (not (p >= 0)) (not (-p >= 0))) 99 * FLATTENDISEQ requires FLATTENOR to be enabled 100 * - EQABSTRACT enables the abstraction-based equality learning heuristic 101 * - ARITHELIM enables variable elimination in arithmetic 102 * - KEEP_ITE: keep if-then-else terms in the egraph 103 * - BREAKSYM: enables symmetry breaking 104 * - PSEUDO_INVERSE: enables elimination of unconstrained terms using 105 * pseudo-inverse tricks 106 * - CONDITIONAL_DEF: attempt to detect and use assertions of the form 107 * (condition => (term = constant)) 108 * - FLATTEN_ITE: avoid intermediate variables when converting nested 109 * if-then-else terms 110 * - FACTOR_TOP_OR: extract common factors from top-level disjuncts 111 * 112 * BREAKSYM for QF_UF is based on the paper by Deharbe et al (CADE 2011) 113 * 114 * PSEUDO_INVERSE is based on Brummayer's thesis (Boolector stuff) 115 * - not implemented yet 116 * 117 * ITE_BOUNDS: for a special if-then-else term t (i.e., if-then-else 118 * term with constant leaves), compute the lower and upper bound on t 119 * and assert that t is between these two bounds. Example: for t = 120 * (ite c 0 1), assert (0 <= t <= 1), and similar for nested 121 * if-then-elses. 122 * 123 * Options passed to the simplex solver when it's created 124 * - EAGER_LEMMAS 125 * - ENABLE_ICHECK 126 * - EQPROP 127 * 128 * Options for testing and debugging 129 * - LAX_OPTION: try to keep going when the assertions contain unsupported 130 * constructs (e.g., quantifiers/bitvectors). 131 * - DUMP_OPTION 132 */ 133 #define VARELIM_OPTION_MASK 0x10 134 #define FLATTENOR_OPTION_MASK 0x20 135 #define FLATTENDISEQ_OPTION_MASK 0x40 136 #define EQABSTRACT_OPTION_MASK 0x80 137 #define ARITHELIM_OPTION_MASK 0x100 138 #define KEEP_ITE_OPTION_MASK 0x200 139 #define BVARITHELIM_OPTION_MASK 0x400 140 #define BREAKSYM_OPTION_MASK 0x800 141 #define PSEUDO_INVERSE_OPTION_MASK 0x1000 142 #define ITE_BOUNDS_OPTION_MASK 0x2000 143 #define CONDITIONAL_DEF_OPTION_MASK 0x4000 144 #define FLATTEN_ITE_OPTION_MASK 0x8000 145 #define FACTOR_OR_OPTION_MASK 0x10000 146 147 #define PREPROCESSING_OPTIONS_MASK \ 148 (VARELIM_OPTION_MASK|FLATTENOR_OPTION_MASK|FLATTENDISEQ_OPTION_MASK|\ 149 EQABSTRACT_OPTION_MASK|ARITHELIM_OPTION_MASK|KEEP_ITE_OPTION_MASK|\ 150 BVARITHELIM_OPTION_MASK|BREAKSYM_OPTION_MASK|PSEUDO_INVERSE_OPTION_MASK|\ 151 ITE_BOUNDS_OPTION_MASK|CONDITIONAL_DEF_OPTION_MASK|FLATTEN_ITE_OPTION_MASK|\ 152 FACTOR_OR_OPTION_MASK) 153 154 // SIMPLEX OPTIONS 155 #define SPLX_EGRLMAS_OPTION_MASK 0x1000000 156 #define SPLX_ICHECK_OPTION_MASK 0x2000000 157 #define SPLX_EQPROP_OPTION_MASK 0x4000000 158 159 // FOR TESTING 160 #define LAX_OPTION_MASK 0x40000000 161 #define DUMP_OPTION_MASK 0x80000000 162 163 164 165 /*************************************** 166 * ARCHITECTURES/SOLVER COMBINATIONS * 167 **************************************/ 168 169 /* 170 * An architecture is specified by one of the following codes 171 * - each architecture defines a set of solvers (and the supported theories) 172 * - the special "auto" codes can be used if mode is CTX_MODE_ONECHECK 173 */ 174 typedef enum { 175 CTX_ARCH_NOSOLVERS, // core only 176 CTX_ARCH_EG, // egraph 177 CTX_ARCH_SPLX, // simplex 178 CTX_ARCH_IFW, // integer floyd-warshall 179 CTX_ARCH_RFW, // real floyd-warshall 180 CTX_ARCH_BV, // bitvector solver 181 CTX_ARCH_EGFUN, // egraph+array/function theory 182 CTX_ARCH_EGSPLX, // egraph+simplex 183 CTX_ARCH_EGBV, // egraph+bitvector solver 184 CTX_ARCH_EGFUNSPLX, // egraph+fun+simplex 185 CTX_ARCH_EGFUNBV, // egraph+fun+bitvector 186 CTX_ARCH_EGSPLXBV, // egraph+simplex+bitvector 187 CTX_ARCH_EGFUNSPLXBV, // all solvers (should be the default) 188 189 CTX_ARCH_AUTO_IDL, // either simplex or integer floyd-warshall 190 CTX_ARCH_AUTO_RDL, // either simplex or real floyd-warshall 191 192 CTX_ARCH_MCSAT // mcsat solver 193 } context_arch_t; 194 195 196 #define NUM_ARCH (CTX_ARCH_MCSAT+1) 197 198 199 /* 200 * Supported theories (including arithmetic and function theory variants) 201 * - a 32bit theories word indicate what's supported 202 * - each bit selects a theory 203 * The theory word is derived from the architecture descriptor 204 */ 205 #define UF_MASK 0x1 206 #define BV_MASK 0x2 207 #define IDL_MASK 0x4 208 #define RDL_MASK 0x8 209 #define LIA_MASK 0x10 210 #define LRA_MASK 0x20 211 #define LIRA_MASK 0x40 212 #define NLIRA_MASK 0x80 // non-linear arithmetic 213 #define FUN_UPDT_MASK 0x100 214 #define FUN_EXT_MASK 0x200 215 #define QUANT_MASK 0x400 216 217 // arith means all variants of linear arithmetic are supported 218 #define ARITH_MASK (LIRA_MASK|LRA_MASK|LIA_MASK|RDL_MASK|IDL_MASK) 219 220 // nlarith_mask means non-linear arithmetic is supported too 221 #define NLARITH_MASK (NLIRA_MASK|ARITH_MASK) 222 223 // fun means both function theories are supported 224 #define FUN_MASK (FUN_UPDT_MASK|FUN_EXT_MASK) 225 226 // all theories, except non-linear arithmetic 227 #define ALLTH_MASK (UF_MASK|BV_MASK|ARITH_MASK|FUN_MASK) 228 229 230 231 232 /*********************************** 233 * PREPROCESSING/SIMPLIFICATION * 234 **********************************/ 235 236 /* 237 * Marks for detecting cycles in variable substitutions 238 * - white: term not visited 239 * - grey: term found but not fully explored yet 240 * - black: fully explored term 241 */ 242 enum { 243 WHITE = 0, 244 GREY = 1, 245 BLACK = 2, 246 }; 247 248 249 250 251 /************************** 252 * ARITHMETIC INTERFACE * 253 *************************/ 254 255 /* 256 * An arithmetic solver must implement the following internalization functions: 257 * 258 * Term constructors 259 * ----------------- 260 * A term in the arithmetic solver is identified by an integer index (arithmetic variable). 261 * 262 * 1) thvar_t create_var(void *solver, bool is_int) 263 * - this must return the index of a new arithmetic variable (no eterm attached) 264 * - if is_int is true, that variable must have integer type, otherwise, it must 265 * be a real. 266 * 267 * 2) thvar_t create_const(void *solver, rational_t *q) 268 * - this must create a theory variable equal to q and return it (no eterm attached) 269 * 270 * 3) thvar_t create_poly(void *solver, polynomial_t *p, thvar_t *map) 271 * - this must return a theory variable equal to p with variables renamed as 272 * defined by map 273 * - p is of the form a_0 t_0 + a_1 t1 ... + a_n t_n, 274 * where t_0 is either the special marker const_idx (= 0) or an arithmetic term 275 * and t_1 ... t_n are arithmetic terms 276 * - map is an array of n+1 theory variables: 277 * map[i] = the theory variable x_i mapped to t_i (with the convention that const_idx 278 * is always mapped to null_thvar) 279 * - the solver must return a theory variable y equal to a_0 x_0 + ... + a_n x_n 280 * 281 * 4) thvar_t create_pprod(void *solver, pprod_t *r, thvar_t *map) 282 * - must return a theory variable equal to r with variables defined by map 283 * - r if of the form t_0^d_0 x ... x t_n^d_n where t_0 ... t_n are arithmetic 284 * terms 285 * - map is an array of n+1 variables: map[i] = variable x_i mapped to t_i 286 * - the solver must return an arithmetic variable y equal to (x_0^d_0 x ... x x_n^d_n) 287 * 288 * 289 * Atom constructors 290 * ----------------- 291 * 292 * 5) literal_t create_eq_atom(void *solver, thvar_t x) 293 * - must create the atom (x == 0) and return the corresponding literal 294 * - x is an existing theory variable in solver 295 * 296 * 6) literal_t create_ge_atom(void *solver, thvar_t x) 297 * - must create the atom (x >= 0) and return the corresponding literal 298 * - x is an existing theory variable in solver 299 * 300 * 7) literal_t create_poly_eq_atom(void *solver, polynomial_t *p, thvar_t *map) 301 * - must create the atom (p == 0) and return the corresponding literal 302 * - p and map are as in create_poly 303 * 304 * 8) literal_t create_poly_ge_atom(void *solver, polynomial_t *p, thvar_t *map) 305 * - must create the atom (p >= 0) and return the corresponding literal 306 * - p and map are as in create_poly 307 * 308 * 9) literal_t create_vareq_atom(void *solver, thvar_t x, thvar_t y) 309 * - create the atom x == y where x and y are two existing variables in solver 310 * 311 * 312 * Assertion of top-level axioms 313 * ----------------------------- 314 * 315 * 10) void assert_eq_axiom(void *solver, thvar_t x, bool tt) 316 * - if tt assert (x == 0) otherwise assert (x != 0) 317 * 318 * 11) void assert_ge_axiom(void *solver, thvar_t x, bool tt) 319 * - if tt assert (x >= 0) otherwise assert (x < 0) 320 * 321 * 12) void assert_poly_eq_axiom(void *solver, polynomial_t *p, thvar_t *map, bool tt) 322 * - if tt assert (p == 0) otherwise assert (p != 0) 323 * - p and map are as in create_poly 324 * 325 * 13) void assert_poly_ge_axiom(void *solver, polynomial_t *p, thvar_t *map, bool tt) 326 * - if tt assert (p >= 0) otherwise assert (p < 0) 327 * - p and map are as in create_poly 328 * 329 * 14) void assert_vareq_axiom(void *solver, thvar_t x, thvar_t y, bool tt) 330 * - if tt assert x == y, otherwise assert x != y 331 * 332 * 15) void assert_cond_vareq_axiom(void *solver, literal_t c, thvar_t x, thvar_t y) 333 * - assert (c implies x == y) as an axiom 334 * - this is used to convert if-then-else equalities: 335 * (x == (ite c y1 y2)) is flattened to (c implies x = y1) and (not c implies x = y2) 336 * 337 * 15b) void assert_clause_vareq_axiom(void *solver, uint32_t n, literal_t *c, thvar_t x, thvar_t y) 338 * - assert (c[0] \/ ... \/ c[n-1] \/ x == y) 339 * 340 * Egraph connection 341 * ----------------- 342 * 343 * 16) void attach_eterm(void *solver, thvar_t v, eterm_t t) 344 * - attach egraph term t to theory variable v 345 * - this function may be omitted for standalone solvers (no egraph is used in that case) 346 * 347 * 17) eterm_t eterm_of_var(void *solver, thvar_t v) 348 * - must return the eterm t attached to v (if any) or null_eterm if v has no term attached 349 * - this function may be omitted for standalone solvers (no egraph) 350 * 351 * NOTE: these functions are also used by the egraph. They are required only if 352 * the context includes both the egraph and the arithmetic solver. 353 * 354 * 355 * Model construction 356 * ------------------ 357 * 358 * The following functions are used when the solver reaches SAT (or UNKNOWN). 359 * First, build_model is called. The solver must construct an assignment M from variables to 360 * rationals at that point. Then, the context can query for the value of a variable x in M. 361 * If the solver cannot assign a rational value to x, it can signal this when value_in_model 362 * is called. M must not be changed until the context calls free_model. 363 * 364 * 18) void build_model(void *solver) 365 * - build a model M: maps variable to rationals. 366 * (or do nothing if the solver does not support model construction). 367 * 368 * 19) bool value_in_model(void *solver, thvar_t x, rational_t *v) 369 * - must return true and copy the value of x in M into v if that value is available. 370 * - return false otherwise (e.g., if model construction is not supported by 371 * solver or x has an irrational value). 372 * 373 * 20) void free_model(void *solver) 374 * - notify solver that M is no longer needed. 375 * 376 * 377 * Queries about variables 378 * ----------------------- 379 * 380 * 21) bool arith_var_is_int(void *solver, thvar_t x): 381 * - return true if x is an integer variable, false otherwise. 382 * 383 * 384 * Exception mechanism 385 * ------------------- 386 * When the solver is created and initialized it's given a pointer b to a jmp_buf internal to 387 * the context. If the solver fails in some way during internalization, it can call 388 * longjmp(*b, error_code) to interrupt the internalization and return control to the 389 * context. For arithmetic solvers, the following error codes should be used: 390 * 391 * FORMULA_NOT_IDL (the solver supports only integer difference logic) 392 * FORMULA_NOT_RDL (the solver supports only real difference logic) 393 * FORMULA_NOT_LINEAR (the solver supports only linear arithmetic) 394 * TOO_MANY_ARITH_VARS (solver limit is reached) 395 * TOO_MANY_ARITH_ATOMS (solver limit is reached) 396 * ARITHSOLVER_EXCEPTION (any other failure) 397 * 398 */ 399 typedef thvar_t (*create_arith_var_fun_t)(void *solver, bool is_int); 400 typedef thvar_t (*create_arith_const_fun_t)(void *solver, rational_t *q); 401 typedef thvar_t (*create_arith_poly_fun_t)(void *solver, polynomial_t *p, thvar_t *map); 402 typedef thvar_t (*create_arith_pprod_fun_t)(void *solver, pprod_t *p, thvar_t *map); 403 404 typedef literal_t (*create_arith_atom_fun_t)(void *solver, thvar_t x); 405 typedef literal_t (*create_arith_patom_fun_t)(void *solver, polynomial_t *p, thvar_t *map); 406 typedef literal_t (*create_arith_vareq_atom_fun_t)(void *solver, thvar_t x, thvar_t y); 407 408 typedef void (*assert_arith_axiom_fun_t)(void *solver, thvar_t x, bool tt); 409 typedef void (*assert_arith_paxiom_fun_t)(void *solver, polynomial_t *p, thvar_t *map, bool tt); 410 typedef void (*assert_arith_vareq_axiom_fun_t)(void *solver, thvar_t x, thvar_t y, bool tt); 411 typedef void (*assert_arith_cond_vareq_axiom_fun_t)(void* solver, literal_t c, thvar_t x, thvar_t y); 412 typedef void (*assert_arith_clause_vareq_axiom_fun_t)(void* solver, uint32_t n, literal_t *c, thvar_t x, thvar_t y); 413 414 typedef void (*attach_eterm_fun_t)(void *solver, thvar_t v, eterm_t t); 415 typedef eterm_t (*eterm_of_var_fun_t)(void *solver, thvar_t v); 416 417 typedef void (*build_model_fun_t)(void *solver); 418 typedef void (*free_model_fun_t)(void *solver); 419 typedef bool (*arith_val_in_model_fun_t)(void *solver, thvar_t x, rational_t *v); 420 421 typedef bool (*arith_var_is_int_fun_t)(void *solver, thvar_t x); 422 423 typedef struct arith_interface_s { 424 create_arith_var_fun_t create_var; 425 create_arith_const_fun_t create_const; 426 create_arith_poly_fun_t create_poly; 427 create_arith_pprod_fun_t create_pprod; 428 429 create_arith_atom_fun_t create_eq_atom; 430 create_arith_atom_fun_t create_ge_atom; 431 create_arith_patom_fun_t create_poly_eq_atom; 432 create_arith_patom_fun_t create_poly_ge_atom; 433 create_arith_vareq_atom_fun_t create_vareq_atom; 434 435 assert_arith_axiom_fun_t assert_eq_axiom; 436 assert_arith_axiom_fun_t assert_ge_axiom; 437 assert_arith_paxiom_fun_t assert_poly_eq_axiom; 438 assert_arith_paxiom_fun_t assert_poly_ge_axiom; 439 assert_arith_vareq_axiom_fun_t assert_vareq_axiom; 440 assert_arith_cond_vareq_axiom_fun_t assert_cond_vareq_axiom; 441 assert_arith_clause_vareq_axiom_fun_t assert_clause_vareq_axiom; 442 443 attach_eterm_fun_t attach_eterm; 444 eterm_of_var_fun_t eterm_of_var; 445 446 build_model_fun_t build_model; 447 free_model_fun_t free_model; 448 arith_val_in_model_fun_t value_in_model; 449 450 arith_var_is_int_fun_t arith_var_is_int; 451 } arith_interface_t; 452 453 454 455 /******************************** 456 * BITVECTOR SOLVER INTERFACE * 457 *******************************/ 458 459 /* 460 * Term constructors 461 * ----------------- 462 * 1) thvar_t create_var(void *solver, uint32_t n) 463 * - must return the index of a new bitvector variable (no eterm attached) 464 * - n = number of bits of that variable 465 * 466 * 2a) thvar_t create_const(void *solver, bvconst_term_t *const) 467 * 2b) thvar_t create_const64(void *solver, bvconst64_term_t *const) 468 * - must return the index of a variable x equal to the constant const 469 * - const->nbits = number of bits 470 * - const->bits = array of uint32_t words (constant value) 471 * 472 * 2c) thvar_t create_zero(void *solver, uint32_t n) 473 * - must create the zero constant of n bits 474 * 475 * 3a) thvar_t create_poly(void *solver, bvpoly_t *p, thvar_t *map) 476 * 3b) thvar_t create_poly64(void *solver, bvpoly64_t *p, thvar_t *map) 477 * - must return a theory variable that represents p with variables renamed as 478 * defined by map: 479 * p is a_0 t_0 + ... + a_n t_n and map[i] = variable x_i mapped to t_i 480 * with the exception that map[0] = null_thvar if x_0 is const_idx 481 * 482 * 4) thvar_t create_pprod(void *solver, pprod_t *r, thvar_t *map) 483 * - return a theory variable to represent the product (t_0 ^ d_0 ... t_n ^ d_n) 484 * - map is an array of n+1 theory variables x_0 ... x_n such that 485 * x_i is mapped to t_i in the internalization table. 486 * 487 * 5) thvar_t create_bvarray(void *solver, literal_t *a, uint32_t n) 488 * - must return a theory variable that represent the array a[0 ... n-1] 489 * - a[0 ... n-1] are all literals in the core 490 * - a[0] is the low order bit, a[n-1] is the high order bit 491 * 492 * 6) thvar_t create_bvite(void *solver, literal_t c, thvar_t x, thvar_t y) 493 * - create (ite c x y): x and y are two theory variables in solver, 494 * and c is a literal in the core. 495 * 496 * 7) binary operators 497 * thvar_t create_bvdiv(void *solver, thvar_t x, thvar_t y) 498 * thvar_t create_bvrem(void *solver, thvar_t x, thvar_t y) 499 * thvar_t create_bvsdiv(void *solver, thvar_t x, thvar_t y) 500 * thvar_t create_bvsrem(void *solver, thvar_t x, thvar_t y) 501 * thvar_t create_bvsmod(void *solver, thvar_t x, thvar_t y) 502 * thvar_t create_bvshl(void *solver, thvar_t x, thvar_t y) 503 * thvar_t create_bvlshr(void *solver, thvar_t x, thvar_t y) 504 * thvar_t create_bvashr(void *solver, thvar_t x, thvar_t y) 505 * 506 * 8) bit extraction 507 * literal_t select_bit(void *solver, thvar_t x, uint32_t i) 508 * - must return bit i of theory variable x as a literal in the core 509 * 510 * Atom creation 511 * ------------- 512 * 9) literal_t create_eq_atom(void *solver, thvar_t x, thvar_t y) 513 * 10) literal_t create_ge_atom(void *solver, thvar_t x, thvar_t y) 514 * 11) literal_t create_sge_atom(void *solver, thvar_t x, thvar_t y) 515 * 516 * Axiom assertion 517 * --------------- 518 * assert axiom if tt is true, the negation of axiom otherwise 519 * 12) void assert_eq_axiom(void *solver, thvar_t x, thvar_t y, bool tt) 520 * 13) void assert_ge_axiom(void *solver, thvar_t x, thvar_t y, bool tt) 521 * 14) void assert_sge_axiom(void *solver, thvar_t x, thvar_t y, bool tt) 522 * 523 * 15) void set_bit(void *solver, thvar_t x, uint32_t i, bool tt) 524 * - assign bit i of x to true or false (depending on tt) 525 * 526 * Egraph interface 527 * ---------------- 528 * 16) void attach_eterm(void *solver, thvar_t v, eterm_t t) 529 * - attach egraph term t to theory variable v of solver 530 * 531 * 17) eterm_t eterm_of_var(void *solver, thvar_t v) 532 * - return the egraph term attached to v in solver (or null_eterm 533 * if v has no egraph term attached). 534 * 535 * Model construction 536 * ------------------ 537 * Same functions as for the arithmetic solvers 538 * 539 * 18) void build_model(void *solver) 540 * - build a model (that maps solver variables to bitvector constants) 541 * 542 * 19) void free_model(void *solver) 543 * - notify the solver that the model is no longer needed 544 * 545 * 20) bool value_in_model(void *solver, thvar_t x, bvconstant_t *v): 546 * - copy the value of x into v and return true. 547 * - if model construction is not supported or the value is not available, return false. 548 */ 549 typedef thvar_t (*create_bv_var_fun_t)(void *solver, uint32_t nbits); 550 typedef thvar_t (*create_bv_const_fun_t)(void *solver, bvconst_term_t *c); 551 typedef thvar_t (*create_bv64_const_fun_t)(void *solver, bvconst64_term_t *c); 552 typedef thvar_t (*create_bv_zero_fun_t)(void *solver, uint32_t nbits); 553 typedef thvar_t (*create_bv_poly_fun_t)(void *solver, bvpoly_t *p, thvar_t *map); 554 typedef thvar_t (*create_bv64_poly_fun_t)(void *solver, bvpoly64_t *p, thvar_t *map); 555 typedef thvar_t (*create_bv_pprod_fun_t)(void *solver, pprod_t *p, thvar_t *map); 556 typedef thvar_t (*create_bv_array_fun_t)(void *solver, literal_t *a, uint32_t n); 557 typedef thvar_t (*create_bv_ite_fun_t)(void *solver, literal_t c, thvar_t x, thvar_t y); 558 typedef thvar_t (*create_bv_binop_fun_t)(void *solver, thvar_t x, thvar_t y); 559 typedef literal_t (*create_bv_atom_fun_t)(void *solver, thvar_t x, thvar_t y); 560 typedef literal_t (*select_bit_fun_t)(void *solver, thvar_t x, uint32_t i); 561 typedef void (*assert_bv_axiom_fun_t)(void *solver, thvar_t x, thvar_t y, bool tt); 562 typedef void (*set_bit_fun_t)(void *solver, thvar_t x, uint32_t i, bool tt); 563 typedef bool (*bv_val_in_model_fun_t)(void *solver, thvar_t x, bvconstant_t *v); 564 565 typedef struct bv_interface_s { 566 create_bv_var_fun_t create_var; 567 create_bv_const_fun_t create_const; 568 create_bv64_const_fun_t create_const64; 569 create_bv_zero_fun_t create_zero; 570 create_bv_poly_fun_t create_poly; 571 create_bv64_poly_fun_t create_poly64; 572 create_bv_pprod_fun_t create_pprod; 573 create_bv_array_fun_t create_bvarray; 574 create_bv_ite_fun_t create_bvite; 575 create_bv_binop_fun_t create_bvdiv; 576 create_bv_binop_fun_t create_bvrem; 577 create_bv_binop_fun_t create_bvsdiv; 578 create_bv_binop_fun_t create_bvsrem; 579 create_bv_binop_fun_t create_bvsmod; 580 create_bv_binop_fun_t create_bvshl; 581 create_bv_binop_fun_t create_bvlshr; 582 create_bv_binop_fun_t create_bvashr; 583 584 select_bit_fun_t select_bit; 585 create_bv_atom_fun_t create_eq_atom; 586 create_bv_atom_fun_t create_ge_atom; 587 create_bv_atom_fun_t create_sge_atom; 588 589 assert_bv_axiom_fun_t assert_eq_axiom; 590 assert_bv_axiom_fun_t assert_ge_axiom; 591 assert_bv_axiom_fun_t assert_sge_axiom; 592 set_bit_fun_t set_bit; 593 594 attach_eterm_fun_t attach_eterm; 595 eterm_of_var_fun_t eterm_of_var; 596 597 build_model_fun_t build_model; 598 free_model_fun_t free_model; 599 bv_val_in_model_fun_t value_in_model; 600 } bv_interface_t; 601 602 603 604 /****************************** 605 * DIFFERENCE LOGIC PROFILE * 606 *****************************/ 607 608 /* 609 * For difference logic, we can use either the simplex solver 610 * or a specialized Floyd-Warshall solver. The decision is 611 * based on the following parameters: 612 * - density = number of atoms / number of variables 613 * - path_bound = an upper bound on the length of any simple 614 * path between two variables 615 * - num_eqs = number of equalities (among all atoms) 616 * dl_data stores the relevant data 617 */ 618 typedef struct dl_data_s { 619 rational_t path_bound; 620 uint32_t num_vars; 621 uint32_t num_atoms; 622 uint32_t num_eqs; 623 } dl_data_t; 624 625 626 627 628 629 /************** 630 * CONTEXT * 631 *************/ 632 633 struct context_s { 634 // mode + architecture + logic code 635 context_mode_t mode; 636 context_arch_t arch; 637 smt_logic_t logic; 638 639 // theories flag 640 uint32_t theories; 641 642 // options flag 643 uint32_t options; 644 645 // base_level == number of calls to push 646 uint32_t base_level; 647 648 // core and theory solvers 649 smt_core_t *core; 650 egraph_t *egraph; 651 mcsat_solver_t *mcsat; 652 void *arith_solver; 653 void *bv_solver; 654 void *fun_solver; 655 656 // solver internalization interfaces 657 arith_interface_t arith; 658 bv_interface_t bv; 659 660 // input are all from the following tables (from yices_globals.h) 661 type_table_t *types; 662 term_table_t *terms; 663 664 // hash table for Boolean gates 665 gate_manager_t gate_manager; 666 667 // internalization table 668 intern_tbl_t intern; 669 670 // result of flattening and simplification 671 ivector_t top_eqs; 672 ivector_t top_atoms; 673 ivector_t top_formulas; 674 ivector_t top_interns; 675 676 // auxiliary buffers and structures for internalization 677 ivector_t subst_eqs; 678 ivector_t aux_eqs; 679 ivector_t aux_atoms; 680 ivector_t aux_vector; 681 int_queue_t queue; 682 int_stack_t istack; 683 684 // data about shared subterms 685 sharing_map_t sharing; 686 687 // store for the conditional descriptors 688 object_store_t cstore; 689 690 // assumption stack 691 assumption_stack_t assumptions; 692 693 // optional components: allocated if needed 694 pseudo_subst_t *subst; 695 mark_vector_t *marks; 696 int_bvset_t *cache; 697 int_hset_t *small_cache; 698 int_rat_hmap_t *edge_map; 699 pmap2_t *eq_cache; 700 divmod_tbl_t *divmod_table; 701 bfs_explorer_t *explorer; 702 703 // buffer to store difference-logic data 704 dl_data_t *dl_profile; 705 706 // buffers for arithmetic simplification/internalization 707 rba_buffer_t *arith_buffer; 708 poly_buffer_t *poly_buffer; 709 polynomial_t *aux_poly; 710 uint32_t aux_poly_size; // number of monomials in aux_poly 711 712 // buffers for bitvector simplification 713 bvpoly_buffer_t *bvpoly_buffer; 714 715 // auxiliary buffers for model construction 716 rational_t aux; 717 bvconstant_t bv_buffer; 718 719 // for exception handling 720 jmp_buf env; 721 722 // for verbose output (default NULL) 723 tracer_t *trace; 724 725 // options for the mcsat solver 726 mcsat_options_t mcsat_options; 727 }; 728 729 730 731 /* 732 * Default initial size of auxiliary buffers and vectors 733 */ 734 #define CTX_DEFAULT_VECTOR_SIZE 10 735 736 737 /* 738 * Default initial size for the solvers 739 */ 740 #define CTX_DEFAULT_CORE_SIZE 100 741 742 743 /* 744 * Error and return codes used by internalization procedures: 745 * - negative codes indicate an error 746 * - these codes can also be used by the theory solvers to report exceptions. 747 */ 748 enum { 749 TRIVIALLY_UNSAT = 1, // simplifies to false 750 CTX_NO_ERROR = 0, // internalization succeeds/not solved 751 // bugs 752 INTERNAL_ERROR = -1, 753 TYPE_ERROR = -2, 754 // general errors 755 FREE_VARIABLE_IN_FORMULA = -3, 756 LOGIC_NOT_SUPPORTED = -4, 757 UF_NOT_SUPPORTED = -5, 758 SCALAR_NOT_SUPPORTED = -6, 759 TUPLE_NOT_SUPPORTED = -7, 760 UTYPE_NOT_SUPPORTED = -8, 761 ARITH_NOT_SUPPORTED = -9, 762 BV_NOT_SUPPORTED = -10, 763 FUN_NOT_SUPPORTED = -11, 764 QUANTIFIERS_NOT_SUPPORTED = -12, 765 LAMBDAS_NOT_SUPPORTED = -13, 766 // arithmetic solver errors 767 FORMULA_NOT_IDL = -14, 768 FORMULA_NOT_RDL = -15, 769 FORMULA_NOT_LINEAR = -16, 770 TOO_MANY_ARITH_VARS = -17, 771 TOO_MANY_ARITH_ATOMS = -18, 772 ARITHSOLVER_EXCEPTION = -19, 773 // bv solver errors 774 BVSOLVER_EXCEPTION = -20, 775 // mcsat errors 776 MCSAT_EXCEPTION_UNSUPPORTED_THEORY = -21 777 }; 778 779 780 /* 781 * NUM_INTERNALIZATION_ERRORS: must be (1 + number of negative codes) 782 */ 783 #define NUM_INTERNALIZATION_ERRORS 22 784 785 786 787 #endif /* __CONTEXT_TYPES_H */ 788