[12] | 1 | /**CHeaderFile***************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [smt.h] |
---|
| 4 | |
---|
| 5 | PackageName [smt] |
---|
| 6 | |
---|
| 7 | Synopsis [Internal declarations.] |
---|
| 8 | |
---|
| 9 | Author [Hyondeuk Kim] |
---|
| 10 | |
---|
| 11 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
| 12 | |
---|
| 13 | All rights reserved. |
---|
| 14 | |
---|
| 15 | Redistribution and use in source and binary forms, with or without |
---|
| 16 | modification, are permitted provided that the following conditions |
---|
| 17 | are met: |
---|
| 18 | |
---|
| 19 | Redistributions of source code must retain the above copyright |
---|
| 20 | notice, this list of conditions and the following disclaimer. |
---|
| 21 | |
---|
| 22 | Redistributions in binary form must reproduce the above copyright |
---|
| 23 | notice, this list of conditions and the following disclaimer in the |
---|
| 24 | documentation and/or other materials provided with the distribution. |
---|
| 25 | |
---|
| 26 | Neither the name of the University of Colorado nor the names of its |
---|
| 27 | contributors may be used to endorse or promote products derived from |
---|
| 28 | this software without specific prior written permission. |
---|
| 29 | |
---|
| 30 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
| 31 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
| 32 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
| 33 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
| 34 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
| 35 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
| 36 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
| 37 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
| 38 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
| 39 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
| 40 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
| 41 | POSSIBILITY OF SUCH DAMAGE.] |
---|
| 42 | |
---|
| 43 | ******************************************************************************/ |
---|
| 44 | |
---|
| 45 | |
---|
| 46 | /*---------------------------------------------------------------------------*/ |
---|
| 47 | /* Nested includes */ |
---|
| 48 | /*---------------------------------------------------------------------------*/ |
---|
| 49 | |
---|
| 50 | #include <gmp.h> |
---|
| 51 | |
---|
| 52 | #ifdef __cplusplus |
---|
| 53 | extern "C" { |
---|
| 54 | #endif |
---|
| 55 | |
---|
| 56 | #include <stdint.h> |
---|
| 57 | #include <string.h> |
---|
| 58 | #include <stdlib.h> |
---|
| 59 | #include <stdio.h> |
---|
| 60 | #include <math.h> |
---|
| 61 | #include <limits.h> |
---|
| 62 | #include <setjmp.h> |
---|
| 63 | #include <signal.h> |
---|
| 64 | #include "sat.h" |
---|
| 65 | #include "aig.h" |
---|
| 66 | #include "util.h" |
---|
| 67 | #include "st.h" |
---|
| 68 | |
---|
| 69 | /*---------------------------------------------------------------------------*/ |
---|
| 70 | /* Constant declarations */ |
---|
| 71 | /*---------------------------------------------------------------------------*/ |
---|
| 72 | #ifndef CUR_DATE |
---|
| 73 | #define CUR_DATE "<compile date not supplied>" |
---|
| 74 | #endif |
---|
| 75 | |
---|
| 76 | #ifndef CUR_VER |
---|
| 77 | #define CUR_VER "U of Colorado/Boulder, CUSP Release 1.0" |
---|
| 78 | #endif |
---|
| 79 | |
---|
| 80 | |
---|
| 81 | /** Global Variable & Smt Manager **/ |
---|
| 82 | #define SAT_MASK 0x1 |
---|
| 83 | #define RESET_SAT_MASK 0xfffffffe |
---|
| 84 | #define UNKNOWN_MASK 0x2 |
---|
| 85 | #define RESET_UNKNOWN_MASK 0xfffffffd |
---|
| 86 | #define CNF_MASK 0x4 |
---|
| 87 | #define RESET_CNF_MASK 0xfffffffb |
---|
| 88 | #define TERM_ITE_MASK 0x8 |
---|
| 89 | #define RESET_TERM_ITE_MASK 0xfffffff7 |
---|
| 90 | #define MP_CONST_MASK 0x10 |
---|
| 91 | #define RESET_MP_CONST_MASK 0xffffffef |
---|
| 92 | |
---|
| 93 | |
---|
| 94 | #define IDL_MASK 0x1000 |
---|
| 95 | #define RESET_IDL_MASK 0xffffefff |
---|
| 96 | #define RDL_MASK 0x2000 |
---|
| 97 | #define RESET_RDL_MASK 0xffffdfff |
---|
| 98 | #define LIA_MASK 0x4000 |
---|
| 99 | #define RESET_LIA_MASK 0xffffbfff |
---|
| 100 | #define LRA_MASK 0x8000 |
---|
| 101 | #define RESET_LRA_MASK 0xffff7fff |
---|
| 102 | |
---|
| 103 | |
---|
| 104 | /** Graph **/ |
---|
| 105 | #define FRINGE_MASK 0x1 |
---|
| 106 | #define RESET_FRINGE_MASK 0xfffffffe |
---|
| 107 | #define REACHED_MASK 0x2 |
---|
| 108 | #define RESET_REACHED_MASK 0xfffffffd |
---|
| 109 | #define DES_MASK 0x4 |
---|
| 110 | #define RESET_DES_MASK 0xfffffffb |
---|
| 111 | |
---|
| 112 | #define RESET_MST_MASK 0xfffffff8 |
---|
| 113 | |
---|
| 114 | #define VISITED_MASK 0x8 |
---|
| 115 | #define RESET_VISITED_MASK 0xfffffff7 |
---|
| 116 | |
---|
| 117 | #define BFRINGE_MASK 0x1000 |
---|
| 118 | #define RESET_BFRINGE_MASK 0xffffefff |
---|
| 119 | #define BREACHED_MASK 0x2000 |
---|
| 120 | #define RESET_BREACHED_MASK 0xffffdfff |
---|
| 121 | #define BDES_MASK 0x4000 |
---|
| 122 | #define RESET_BDES_MASK 0xffffbfff |
---|
| 123 | |
---|
| 124 | #define RESET_BMST_MASK 0xffff8fff |
---|
| 125 | |
---|
| 126 | #define BVISITED_MASK 0x8000 |
---|
| 127 | #define RESET_BVISITED_MASK 0xffff7fff |
---|
| 128 | |
---|
| 129 | #define FFRINGE_MASK 0x10000 |
---|
| 130 | #define RESET_FFRINGE_MASK 0xfffeffff |
---|
| 131 | #define FREACHED_MASK 0x20000 |
---|
| 132 | #define RESET_FREACHED_MASK 0xfffdffff |
---|
| 133 | #define FDES_MASK 0x40000 |
---|
| 134 | #define RESET_FDES_MASK 0xfffbffff |
---|
| 135 | |
---|
| 136 | #define RESET_FMST_MASK 0xfff8ffff |
---|
| 137 | |
---|
| 138 | #define FVISITED_MASK 0x80000 |
---|
| 139 | #define RESET_FVISITED_MASK 0xfff7ffff |
---|
| 140 | |
---|
| 141 | #define BARR_MASK 0x100000 |
---|
| 142 | #define RESET_BARR_MASK 0xffefffff |
---|
| 143 | |
---|
| 144 | #define FARR_MASK 0x200000 |
---|
| 145 | #define RESET_FARR_MASK 0xffdfffff |
---|
| 146 | |
---|
| 147 | |
---|
| 148 | |
---|
| 149 | /** Fml **/ |
---|
| 150 | #define FML_VISITED_MASK 0x200 |
---|
| 151 | #define RESET_FML_VISITED_MASK 0xfffffdff |
---|
| 152 | #define ITE_CHAIN_MASK 0x400 |
---|
| 153 | #define RESET_ITE_CHAIN_MASK 0xfffffbff |
---|
| 154 | #define TRUE_MASK 0x800 |
---|
| 155 | #define RESET_TRUE_MASK 0xfffff7ff |
---|
| 156 | #define FALSE_MASK 0x1000 |
---|
| 157 | #define RESET_FALSE_MASK 0xffffefff |
---|
| 158 | #define IN_ARR_MASK 0x2000 |
---|
| 159 | #define RESET_IN_ARR_MASK 0xffffdfff |
---|
| 160 | #define QUEUED_MASK 0x4000 |
---|
| 161 | #define RESET_QUEUED_MASK 0xffffbfff |
---|
| 162 | #define NEG_MASK 0x8000 |
---|
| 163 | #define RESET_NEG_MASK 0xffff7fff |
---|
| 164 | |
---|
| 165 | |
---|
| 166 | /** Avar **/ |
---|
| 167 | #define IMPLIED_MASK 0x1 |
---|
| 168 | #define RESET_IMPLIED_MASK 0xfffffffe |
---|
| 169 | #define TPROP_MASK 0x2 |
---|
| 170 | #define RESET_TPROP_MASK 0xfffffffd |
---|
| 171 | #define BOUND_MASK 0x4 |
---|
| 172 | #define RESET_BOUND_MASK 0xfffffffb |
---|
| 173 | #define DIFF_MASK 0x8 |
---|
| 174 | #define RESET_DIFF_MASK 0xfffffff7 |
---|
| 175 | #define UNIT_LA_MASK 0x10 |
---|
| 176 | #define RESET_UNIT_LA_MASK 0xffffffef |
---|
| 177 | #define LA_MASK 0x20 |
---|
| 178 | #define RESET_LA_MASK 0xffffffdf |
---|
| 179 | #define SIGNED_MASK 0x40 |
---|
| 180 | #define RESET_SIGNED_MASK 0xffffffbf |
---|
| 181 | |
---|
| 182 | |
---|
| 183 | /** Bvar **/ |
---|
| 184 | #define BTRUE_MASK 0x1 |
---|
| 185 | #define RESET_BTRUE_MASK 0xfffffffe |
---|
| 186 | #define BFALSE_MASK 0x2 |
---|
| 187 | #define RESET_BFALSE_MASK 0xfffffffd |
---|
| 188 | |
---|
| 189 | |
---|
| 190 | /** Nvar **/ |
---|
| 191 | #define BASIC_MASK 0x1 |
---|
| 192 | #define RESET_BASIC_MASK 0xfffffffe |
---|
| 193 | #define BOUNDED_MASK 0x2 |
---|
| 194 | #define RESET_BOUNDED_MASK 0xfffffffd |
---|
| 195 | #define UNBOUNDED_MASK 0x4 |
---|
| 196 | #define RESET_UNBOUNDED_MASK 0xfffffffb |
---|
| 197 | |
---|
| 198 | |
---|
| 199 | /** System **/ |
---|
| 200 | #define YYMAXDEPTH 1000000 |
---|
| 201 | #define YY_NO_INPUT |
---|
| 202 | |
---|
| 203 | /*---------------------------------------------------------------------------*/ |
---|
| 204 | /* Type declarations */ |
---|
| 205 | /*---------------------------------------------------------------------------*/ |
---|
| 206 | |
---|
| 207 | typedef enum { |
---|
| 208 | /* boolean */ |
---|
| 209 | IMP_c, /* 0 */ |
---|
| 210 | IFF_c, |
---|
| 211 | AND_c, |
---|
| 212 | OR_c, |
---|
| 213 | XOR_c, |
---|
| 214 | NAND_c, /* 5 */ |
---|
| 215 | NOT_c, |
---|
| 216 | ITE_c, |
---|
| 217 | TITE_c, |
---|
| 218 | |
---|
| 219 | EQ_c, |
---|
| 220 | NEQ_c, /* 10 */ |
---|
| 221 | LT_c, |
---|
| 222 | GT_c, |
---|
| 223 | LE_c, |
---|
| 224 | GE_c, |
---|
| 225 | |
---|
| 226 | LET_c, /* 15 */ |
---|
| 227 | FLET_c, |
---|
| 228 | |
---|
| 229 | /* arithmetic */ |
---|
| 230 | MUL_c, |
---|
| 231 | DIV_c, |
---|
| 232 | REM_c, /* remainder */ |
---|
| 233 | ADD_c, /* 20 */ |
---|
| 234 | SUB_c, |
---|
| 235 | MINUS_c, |
---|
| 236 | NUM_c, |
---|
| 237 | NONE_c, |
---|
| 238 | |
---|
| 239 | /* parsing */ |
---|
| 240 | FUN_c, |
---|
| 241 | PRED_c, |
---|
| 242 | TVAR_c, /* term var */ |
---|
| 243 | FVAR_c, /* fml var */ |
---|
| 244 | NVAR_c, |
---|
| 245 | |
---|
| 246 | ATOM_c, |
---|
| 247 | REAL_c, |
---|
| 248 | INT_c, |
---|
| 249 | ARRAY_c |
---|
| 250 | } smtFmlType_t; |
---|
| 251 | |
---|
| 252 | typedef struct smtManagerStruct smtManager_t; |
---|
| 253 | typedef struct smtStatsStruct smtStats_t; |
---|
| 254 | typedef struct smtGlobalVarStruct smtGlobalVar_t; |
---|
| 255 | typedef struct smtClauseStruct smtCls_t; |
---|
| 256 | typedef struct smtFormulaStruct smtFml_t; |
---|
| 257 | typedef struct smtAvarStruct smtAvar_t; |
---|
| 258 | typedef struct smtBvarStruct smtBvar_t; |
---|
| 259 | typedef struct smtNvarStruct smtNvar_t; |
---|
| 260 | typedef struct smtBoundStruct smtBound_t; |
---|
| 261 | typedef struct smtFletStruct smtFlet_t; |
---|
| 262 | typedef struct smtMpStruct smtMp_t; |
---|
| 263 | typedef struct smtGraphStruct smtGraph_t; |
---|
| 264 | typedef struct smtVertexStruct smtVertex_t; |
---|
| 265 | typedef struct smtEdgeStruct smtEdge_t; |
---|
| 266 | typedef struct smtQueueStruct smtQueue_t; |
---|
| 267 | |
---|
| 268 | /*---------------------------------------------------------------------------*/ |
---|
| 269 | /* Structure declarations */ |
---|
| 270 | /*---------------------------------------------------------------------------*/ |
---|
| 271 | |
---|
| 272 | struct smtManagerStruct { |
---|
| 273 | satArray_t * clsArr; |
---|
| 274 | satArray_t * la_clsArr; |
---|
| 275 | satArray_t * avarArr; |
---|
| 276 | satArray_t * bvarArr; |
---|
| 277 | satArray_t * nvarArr; |
---|
| 278 | satArray_t * tmp_nvars; |
---|
| 279 | satArray_t * tab_avars; |
---|
| 280 | satArray_t * tab_nvars; |
---|
| 281 | satArray_t * slacks; |
---|
| 282 | satArray_t * basics; |
---|
| 283 | satArray_t * fmlArr; |
---|
| 284 | satArray_t * avfmlArr; |
---|
| 285 | satArray_t * iff_fmlArr; |
---|
| 286 | satArray_t * ite_fmlArr; |
---|
| 287 | satArray_t * fletArr; |
---|
| 288 | satArray_t * id2var; |
---|
| 289 | satArray_t * litArr; |
---|
| 290 | satArray_t * lemma; |
---|
| 291 | satArray_t * tplits; |
---|
| 292 | |
---|
| 293 | long * id2slack; |
---|
| 294 | int * node2id; /* aig node index to var id */ |
---|
| 295 | int * node2ins; /* aig node index to node indegree */ |
---|
| 296 | smtFml_t ** node2fml; |
---|
| 297 | |
---|
| 298 | satManager_t * cm; |
---|
| 299 | Aig_Manager_t * bm; |
---|
| 300 | smtMp_t * mp; |
---|
| 301 | smtGraph_t * cG; |
---|
| 302 | smtBound_t * bounds; |
---|
| 303 | double * tab; |
---|
| 304 | |
---|
| 305 | st_table * fml_table; |
---|
| 306 | st_table * sis_table; |
---|
| 307 | |
---|
| 308 | smtFml_t * fml; |
---|
| 309 | |
---|
| 310 | smtStats_t * stats; |
---|
| 311 | |
---|
| 312 | double * rvalues; |
---|
| 313 | double * prvalues; |
---|
| 314 | |
---|
| 315 | double epsilon; |
---|
| 316 | double epsilonless; |
---|
| 317 | |
---|
| 318 | int flag; |
---|
| 319 | |
---|
| 320 | int num_var; |
---|
| 321 | int num_constants; |
---|
| 322 | int cur_index; |
---|
| 323 | int limit; |
---|
| 324 | |
---|
| 325 | int aig_one_id; |
---|
| 326 | int aig_zero_id; |
---|
| 327 | int aig_none; |
---|
| 328 | |
---|
| 329 | AigEdge_t obj; |
---|
| 330 | |
---|
| 331 | int * avalues; |
---|
| 332 | int * ivalues; |
---|
| 333 | |
---|
| 334 | char * filename; |
---|
| 335 | }; |
---|
| 336 | |
---|
| 337 | struct smtStatsStruct { |
---|
| 338 | /* double parse_time; |
---|
| 339 | double preprocess_time; */ |
---|
| 340 | double solve_time; |
---|
| 341 | double num_bf_call; |
---|
| 342 | double num_bf_conf; |
---|
| 343 | double num_assert_call; |
---|
| 344 | double num_assert_conf; |
---|
| 345 | double num_check_call; |
---|
| 346 | double num_check_conf; |
---|
| 347 | |
---|
| 348 | double num_tprop_call; |
---|
| 349 | double num_tprop; |
---|
| 350 | double num_simp_tprop_call; |
---|
| 351 | double num_simp_tprop; |
---|
| 352 | |
---|
| 353 | int num_eq; |
---|
| 354 | int num_ceq; |
---|
| 355 | int num_ineq; |
---|
| 356 | int num_eq2ineq; |
---|
| 357 | int num_lzero_eq; |
---|
| 358 | int num_lzero_ineq; |
---|
| 359 | int num_inter_bvar; |
---|
| 360 | int num_velm_cand; |
---|
| 361 | int num_static_cls; |
---|
| 362 | int num_static_pred; |
---|
| 363 | int num_avar; |
---|
| 364 | int num_row; |
---|
| 365 | int num_col; |
---|
| 366 | }; |
---|
| 367 | |
---|
| 368 | struct smtGlobalVarStruct { |
---|
| 369 | smtFml_t * fml; |
---|
| 370 | smtFml_t * tfml; |
---|
| 371 | |
---|
| 372 | smtBvar_t * bvar; |
---|
| 373 | smtNvar_t * nvar; |
---|
| 374 | |
---|
| 375 | satArray_t * fmlArr; |
---|
| 376 | satArray_t * tfmlArr; |
---|
| 377 | satArray_t * avfmlArr; |
---|
| 378 | satArray_t * bvarArr; |
---|
| 379 | satArray_t * nvarArr; |
---|
| 380 | satArray_t * fletArr; |
---|
| 381 | |
---|
| 382 | double epsilon; /* may not need */ |
---|
| 383 | double epsilonless; /* may not need */ |
---|
| 384 | |
---|
| 385 | long status; |
---|
| 386 | int flag; |
---|
| 387 | |
---|
| 388 | char * filename; |
---|
| 389 | char * str; |
---|
| 390 | |
---|
| 391 | st_table * fun_table; |
---|
| 392 | st_table * pred_table; |
---|
| 393 | st_table * fml_var_table; |
---|
| 394 | st_table * term_var_table; |
---|
| 395 | st_table * term_table; |
---|
| 396 | st_table * num_table; |
---|
| 397 | }; |
---|
| 398 | |
---|
| 399 | struct smtClauseStruct { |
---|
| 400 | satArray_t * litArr; |
---|
| 401 | }; |
---|
| 402 | |
---|
| 403 | struct smtFormulaStruct { |
---|
| 404 | int id; |
---|
| 405 | int flag; |
---|
| 406 | |
---|
| 407 | /*smtFmlType_t type;*/ |
---|
| 408 | long type; |
---|
| 409 | satArray_t * subfmlArr; |
---|
| 410 | |
---|
| 411 | AigEdge_t aig_node; |
---|
| 412 | |
---|
| 413 | smtAvar_t * avar; |
---|
| 414 | smtBvar_t * bvar; |
---|
| 415 | smtNvar_t * nvar; |
---|
| 416 | |
---|
| 417 | int nNeg; |
---|
| 418 | int ins; |
---|
| 419 | int value; |
---|
| 420 | }; |
---|
| 421 | |
---|
| 422 | struct smtAvarStruct { |
---|
| 423 | char * name; |
---|
| 424 | int id; |
---|
| 425 | int flag; |
---|
| 426 | |
---|
| 427 | /*smtFmlType_t type;*/ |
---|
| 428 | long type; |
---|
| 429 | |
---|
| 430 | satArray_t * nvars; |
---|
| 431 | array_t * coeffs; |
---|
| 432 | array_t * sis_avars; |
---|
| 433 | |
---|
| 434 | double constant; |
---|
| 435 | |
---|
| 436 | AigEdge_t aig_node; |
---|
| 437 | }; |
---|
| 438 | |
---|
| 439 | struct smtBvarStruct { |
---|
| 440 | char * name; |
---|
| 441 | int id; |
---|
| 442 | int flag; |
---|
| 443 | |
---|
| 444 | AigEdge_t aig_node; |
---|
| 445 | }; |
---|
| 446 | |
---|
| 447 | struct smtNvarStruct { |
---|
| 448 | char * name; |
---|
| 449 | int id; |
---|
| 450 | int flag; |
---|
| 451 | |
---|
| 452 | satArray_t * avarArr; |
---|
| 453 | }; |
---|
| 454 | |
---|
| 455 | struct smtBoundStruct { |
---|
| 456 | double ub; |
---|
| 457 | double lb; |
---|
| 458 | }; |
---|
| 459 | |
---|
| 460 | struct smtFletStruct { |
---|
| 461 | smtFml_t * fvar_fml; |
---|
| 462 | smtFml_t * fml; |
---|
| 463 | }; |
---|
| 464 | |
---|
| 465 | struct smtMpStruct { |
---|
| 466 | mpq_t * pool; |
---|
| 467 | mpq_t * values; /* nvar values */ |
---|
| 468 | mpq_t * pvalues; /* nvar values */ |
---|
| 469 | mpq_t * constants; |
---|
| 470 | mpq_t * weights; |
---|
| 471 | |
---|
| 472 | mpq_t zero; |
---|
| 473 | mpq_t one; |
---|
| 474 | mpq_t m_one; |
---|
| 475 | |
---|
| 476 | int num_avar; |
---|
| 477 | int num_nvar; |
---|
| 478 | int plimit; |
---|
| 479 | }; |
---|
| 480 | |
---|
| 481 | struct smtGraphStruct { |
---|
| 482 | satArray_t * nvarArr; |
---|
| 483 | satArray_t * avarArr; |
---|
| 484 | satArray_t * cur_edges; |
---|
| 485 | satArray_t * neg_edges; |
---|
| 486 | satArray_t * bvArr; |
---|
| 487 | satArray_t * fvArr; |
---|
| 488 | satArray_t * imp_edges; |
---|
| 489 | |
---|
| 490 | smtVertex_t * vHead; |
---|
| 491 | smtVertex_t ** paths; |
---|
| 492 | smtVertex_t ** bpaths; |
---|
| 493 | smtVertex_t ** fpaths; |
---|
| 494 | |
---|
| 495 | smtEdge_t * eHead; |
---|
| 496 | |
---|
| 497 | smtQueue_t * queue; |
---|
| 498 | |
---|
| 499 | double * rdists; |
---|
| 500 | double * brdists; |
---|
| 501 | double * frdists; |
---|
| 502 | |
---|
| 503 | double epsilonless; |
---|
| 504 | |
---|
| 505 | int * flags; |
---|
| 506 | int * idists; |
---|
| 507 | int * bidists; |
---|
| 508 | int * fidists; |
---|
| 509 | |
---|
| 510 | int vsize; |
---|
| 511 | int esize; |
---|
| 512 | }; |
---|
| 513 | |
---|
| 514 | struct smtVertexStruct { |
---|
| 515 | satArray_t * ins; |
---|
| 516 | satArray_t * outs; |
---|
| 517 | satArray_t * targets; |
---|
| 518 | |
---|
| 519 | int index; |
---|
| 520 | }; |
---|
| 521 | |
---|
| 522 | struct smtEdgeStruct { |
---|
| 523 | int index; |
---|
| 524 | |
---|
| 525 | smtVertex_t * src; |
---|
| 526 | smtVertex_t * dest; |
---|
| 527 | |
---|
| 528 | satArray_t * implied; |
---|
| 529 | |
---|
| 530 | smtAvar_t * avar; |
---|
| 531 | |
---|
| 532 | double weight; |
---|
| 533 | }; |
---|
| 534 | |
---|
| 535 | struct smtQueueStruct { |
---|
| 536 | long max; /* max size of queue */ |
---|
| 537 | long size; /* the number of current entries */ |
---|
| 538 | long front; /* front index of entries */ |
---|
| 539 | long rear; /* rear index of entries */ |
---|
| 540 | long * array; /* the location to save entries */ |
---|
| 541 | }; |
---|
| 542 | |
---|
| 543 | /*---------------------------------------------------------------------------*/ |
---|
| 544 | /* Variable declarations */ |
---|
| 545 | /*---------------------------------------------------------------------------*/ |
---|
| 546 | |
---|
| 547 | #ifndef SMT_GLOBAL_VARIABLE |
---|
| 548 | #define SMT_GLOBAL_VARIABLE |
---|
| 549 | extern smtGlobalVar_t * gvar; |
---|
| 550 | #endif |
---|
| 551 | |
---|
| 552 | |
---|
| 553 | /*---------------------------------------------------------------------------*/ |
---|
| 554 | /* Macro declarations */ |
---|
| 555 | /*---------------------------------------------------------------------------*/ |
---|
| 556 | |
---|
| 557 | |
---|
| 558 | /**AutomaticStart*************************************************************/ |
---|
| 559 | |
---|
| 560 | /*---------------------------------------------------------------------------*/ |
---|
| 561 | /* Function prototypes */ |
---|
| 562 | /*---------------------------------------------------------------------------*/ |
---|
| 563 | |
---|
| 564 | /* main.c */ |
---|
| 565 | |
---|
| 566 | |
---|
| 567 | /* smt.c */ |
---|
| 568 | int smt_main(char * filename, int timeout, int is_model); |
---|
| 569 | void smt_read(char * str); |
---|
| 570 | void SmtFileSetup(FILE * fp); |
---|
| 571 | int SmtYyparse(void); |
---|
| 572 | smtManager_t * smt_init(void); |
---|
| 573 | smtManager_t * smt_dl_init(void); |
---|
| 574 | smtManager_t * smt_la_init(void); |
---|
| 575 | void smt_solve(smtManager_t * sm); |
---|
| 576 | void smt_report(smtManager_t * sm, int is_model); |
---|
| 577 | void smt_postprocess(smtManager_t * sm); |
---|
| 578 | void smt_init_global_variable(char * filename); |
---|
| 579 | void smt_free_global_variable(void); |
---|
| 580 | void smt_free_key_in_table(st_table * table); |
---|
| 581 | void smt_free_key_with_array_in_table(st_table * table); |
---|
| 582 | smtManager_t * smt_init_manager(void); |
---|
| 583 | void smt_free_manager(smtManager_t * sm); |
---|
| 584 | void smt_free_clauses(satArray_t * clsArr); |
---|
| 585 | void smt_free_clauses(satArray_t * clsArr); |
---|
| 586 | void smt_free_atom_variables(satArray_t * avarArr); |
---|
| 587 | void smt_free_atom_members(smtAvar_t * avar); |
---|
| 588 | void smt_free_bool_variables(satArray_t * bvarArr); |
---|
| 589 | void smt_free_numerical_variables(satArray_t * nvarArr); |
---|
| 590 | void smt_free_formulas(satArray_t * fmlArr); |
---|
| 591 | smtStats_t * smt_init_stats(void); |
---|
| 592 | void smt_circus_interface(smtManager_t * sm); |
---|
| 593 | void smt_circus_cnf_interface(smtManager_t * sm); |
---|
| 594 | satArray_t * smt_get_decision_order(smtManager_t * sm); |
---|
| 595 | |
---|
| 596 | |
---|
| 597 | |
---|
| 598 | |
---|
| 599 | /* smtPre.c */ |
---|
| 600 | void smt_preprocess(smtManager_t * sm); |
---|
| 601 | void smt_solve_bool_model(smtManager_t * sm); |
---|
| 602 | void smt_generate_level_zero_assignments(smtManager_t * sm); |
---|
| 603 | void smt_update_nvar_adjacent_avar_array(smtManager_t * sm); |
---|
| 604 | void smt_generate_adjacent_atom_array(smtManager_t * sm); |
---|
| 605 | void smt_dl_preprocess(smtManager_t * sm); |
---|
| 606 | void smt_convert_atom_to_dl_form(smtManager_t * sm); |
---|
| 607 | void smt_generate_avar_sister_array(smtManager_t * sm); |
---|
| 608 | void smt_la_preprocess(smtManager_t * sm); |
---|
| 609 | void smt_put_la_clause_to_clause_arr(smtManager_t * sm); |
---|
| 610 | void smt_convert_lac_into_unit_lac(smtManager_t * sm); |
---|
| 611 | void smt_init_convert_lac_into_unit_lac(smtManager_t * sm, int * num_nvars, int * num_lavars, int * max_coeffs, int * flags); |
---|
| 612 | satArray_t * smt_check_nvar_in_atom(smtManager_t * sm, int * num_nvars, int * max_coeffs, int * num_lavars); |
---|
| 613 | void smt_decide_lac_converting_criterion(smtManager_t * sm, int * flags, int * num_nvars, int * max_coeffs); |
---|
| 614 | void smt_create_avar_with_nvar_related_avar(smtManager_t * sm, smtNvar_t * new_nvar, smtNvar_t * nvar, int int_coeff); |
---|
| 615 | |
---|
| 616 | |
---|
| 617 | |
---|
| 618 | /* smtFml.c */ |
---|
| 619 | smtFml_t * smt_create_formula(smtFmlType_t ftype, satArray_t * subfmlArr); |
---|
| 620 | void smt_duplicate_formula(smtFml_t * new_fml, smtFml_t * org); |
---|
| 621 | smtFml_t * smt_create_identical_formula(smtFml_t * fml); |
---|
| 622 | smtFml_t * smt_simplify_formula(smtFml_t * fml); |
---|
| 623 | void smt_increase_subfml_ins(smtFml_t * fml); |
---|
| 624 | void smt_add_fml_to_array(smtFml_t * fml); |
---|
| 625 | smtFml_t * smt_create_returning_formula(smtFml_t * fml); |
---|
| 626 | smtFml_t * smt_create_function_symbol(char * fs_name); |
---|
| 627 | smtFml_t * smt_create_predicate_symbol(char * ps_name); |
---|
| 628 | smtFml_t * smt_create_constant_predicate_symbol(char * ps_name, int value); |
---|
| 629 | smtFml_t * smt_create_fml_variable(char * fname); |
---|
| 630 | smtFml_t * smt_create_term_variable(char * fs_name); |
---|
| 631 | smtFml_t * smt_create_constant_formula(char * cname); |
---|
| 632 | void smt_simplify_term_fml(smtFml_t * fml, st_table * num_table); |
---|
| 633 | void smt_save_flet_pair(smtFml_t * fvar_fml, smtFml_t * fml); |
---|
| 634 | void smt_init_formula_flag(smtManager_t * sm); |
---|
| 635 | void smt_init_fml_visited_flag(smtManager_t * sm); |
---|
| 636 | void smt_init_fml_queued_flag(smtManager_t * sm); |
---|
| 637 | char * smt_convert_fml_to_string(smtFml_t * fml); |
---|
| 638 | char * smt_convert_fml_to_string_with_subfml(smtFmlType_t type, satArray_t * subfmlArr); |
---|
| 639 | int smt_is_leaf_fml(smtFml_t * fml); |
---|
| 640 | int smt_is_abstract_leaf_fml(smtFml_t * fml); |
---|
| 641 | int smt_is_negated_abstract_leaf_fml(smtFml_t * fml); |
---|
| 642 | int smt_is_ite_chain_fml(smtFml_t * fml, int num_fml); |
---|
| 643 | int smt_is_atom_formula(smtFml_t * fml); |
---|
| 644 | int smt_is_negated_atom_formula(smtFml_t * fml); |
---|
| 645 | int smt_is_boolean_formula(smtFml_t * fml); |
---|
| 646 | int smt_is_negated_boolean_formula(smtFml_t * fml); |
---|
| 647 | int smt_is_arith_formula(smtFml_t * fml); |
---|
| 648 | int smt_is_multi_arith_formula(smtFml_t * fml); |
---|
| 649 | int smt_is_binary_arith_formula(smtFml_t * fml); |
---|
| 650 | int smt_is_unary_arith_formula(smtFml_t * fml); |
---|
| 651 | int smt_is_term_formula(smtFml_t * fml); |
---|
| 652 | int smt_is_bool_atom_fml(smtFml_t * fml); |
---|
| 653 | int smt_get_constant_value_in_fml(smtFml_t * fml, int * value); |
---|
| 654 | void smt_convert_term_ite_into_bool_ite_main(smtManager_t * sm); |
---|
| 655 | void smt_init_convert_term_ite_into_bool_ite(smtManager_t * sm); |
---|
| 656 | void smt_convert_term_ite_into_bool_ite(smtManager_t * sm, smtFml_t * fml); |
---|
| 657 | smtFml_t * smt_check_fml_for_term_ite_fml(smtFml_t * fml); |
---|
| 658 | void smt_convert_term_ite_into_bool_ite_sub(smtManager_t * sm, smtFml_t * fml, smtFml_t * ite_fml); |
---|
| 659 | smtFml_t * smt_create_ite_term_fml(smtManager_t * sm, smtFmlType_t type, satArray_t * subfmls, smtFml_t * subfml, int ite_index); |
---|
| 660 | void smt_assign_ite_terms_to_ite_fml(smtManager_t * sm, smtFml_t * new_ite, smtFml_t * cond_fml, smtFml_t * new_then, smtFml_t * new_else); |
---|
| 661 | int smt_check_ite_for_terminal_case(smtFml_t * ite_fml); |
---|
| 662 | void smt_convert_eq_fml_to_ineq_fml(smtManager_t * sm); |
---|
| 663 | void smt_add_flet_pair_formula(smtManager_t * sm); |
---|
| 664 | void smt_convert_eq_fml_into_ineq_and_fml(smtManager_t * sm, smtFml_t * fml); |
---|
| 665 | void smt_convert_diseq_fml_into_ineq_or_fml(smtManager_t * sm, smtFml_t * fml); |
---|
| 666 | satArray_t * smt_gather_bvar_in_fml(smtManager_t * sm, smtFml_t * fml); |
---|
| 667 | |
---|
| 668 | |
---|
| 669 | |
---|
| 670 | |
---|
| 671 | |
---|
| 672 | |
---|
| 673 | /* smtUtil.c */ |
---|
| 674 | smtCls_t * smt_create_clause(void); |
---|
| 675 | smtCls_t * smt_duplicate_clause(smtCls_t * cls); |
---|
| 676 | smtFmlType_t smt_get_ar_symbol(char * str); |
---|
| 677 | smtBvar_t * smt_create_bool_variable(char * name, smtFml_t * bvfml); |
---|
| 678 | smtBvar_t * smt_create_intermediate_bool_variable(smtManager_t * sm, AigEdge_t node); |
---|
| 679 | smtNvar_t * smt_create_numerical_variable(char * name, smtFml_t * nvfml); |
---|
| 680 | void smt_create_dl_atom_variable_main(smtManager_t * sm); |
---|
| 681 | void smt_create_la_atom_variable_main(smtManager_t * sm); |
---|
| 682 | void smt_convert_dl_atom_fml_to_bool_fml(smtFml_t * fml, smtAvar_t * avar); |
---|
| 683 | int smt_convert_atom_to_leq_form(smtManager_t * sm, smtAvar_t * avar); |
---|
| 684 | char * smt_get_avar_name(smtManager_t * sm, smtAvar_t * avar); |
---|
| 685 | char * smt_get_neg_avar_name(smtManager_t * sm, smtAvar_t * avar); |
---|
| 686 | smtAvar_t * smt_create_atom_variable(smtFml_t * avfml); |
---|
| 687 | smtAvar_t * smt_create_pure_atom_variable(void); |
---|
| 688 | void smt_init_atom_variable_values(smtManager_t * sm); |
---|
| 689 | void smt_init_numerical_variable_values(smtManager_t * sm); |
---|
| 690 | void smt_gather_atom_member(smtAvar_t * avar, smtFml_t * avfml); |
---|
| 691 | void smt_gather_atom_member_in_fml(smtAvar_t * avar, smtFml_t * fml, int nminus, double coeff); |
---|
| 692 | void smt_combine_root_fml_with_flet_fml(void); |
---|
| 693 | void smt_assign_boolean_variable_id(smtManager_t * sm); |
---|
| 694 | void smt_assign_numerical_variable_id(smtManager_t * sm); |
---|
| 695 | void smt_assign_numerical_variable_id_in_array(satArray_t * nvarArr); |
---|
| 696 | void smt_assign_bool_var_flag(smtManager_t * sm); |
---|
| 697 | void smt_sort_nvar_array_with_id(satArray_t * arr); |
---|
| 698 | void smt_sort_nvar_array_with_id_aux(long * arr, long size); |
---|
| 699 | smtQueue_t * smt_create_queue(long MaxElements); |
---|
| 700 | void smt_init_queue(smtQueue_t * Q); |
---|
| 701 | void smt_free_queue(smtQueue_t * Q); |
---|
| 702 | void smt_enqueue(smtQueue_t * Q, long v); |
---|
| 703 | long smt_dequeue(smtQueue_t * Q); |
---|
| 704 | int smt_timeout(int timeout); |
---|
| 705 | void smt_timeout_handle(void); |
---|
| 706 | void smt_none(void); |
---|
| 707 | |
---|
| 708 | |
---|
| 709 | |
---|
| 710 | |
---|
| 711 | |
---|
| 712 | |
---|
| 713 | |
---|
| 714 | |
---|
| 715 | |
---|
| 716 | /* smtCnf.c */ |
---|
| 717 | void smt_generate_cnf_main(smtManager_t * sm); |
---|
| 718 | int smt_generate_cnf(smtManager_t * sm); |
---|
| 719 | void smt_generate_cnf_with_aig(smtManager_t * sm); |
---|
| 720 | AigEdge_t smt_generate_aig(smtManager_t * sm); |
---|
| 721 | int smt_is_ite_terminal_case(AigEdge_t cond_node, AigEdge_t then_node, AigEdge_t else_node); |
---|
| 722 | void smt_convert_aig_into_cnf(smtManager_t * sm, AigEdge_t aig_node); |
---|
| 723 | void smt_compute_indegree_for_aig_node(smtManager_t * sm); |
---|
| 724 | void smt_init_var_id_for_aig_node(smtManager_t * sm); |
---|
| 725 | void smt_check_leaf_node_for_aig_node(smtManager_t * sm); |
---|
| 726 | satArray_t * smt_sort_formula_in_bfs_manner(smtManager_t * sm, smtFml_t * root); |
---|
| 727 | void smt_compute_indegree_in_formula(smtManager_t * sm); |
---|
| 728 | array_t * smt_gather_aig_node_from_formula_array(satArray_t * fmlArr); |
---|
| 729 | int smt_convert_aig_into_cnf_sub(smtManager_t * sm, AigEdge_t node, array_t * idArr, int * negated); |
---|
| 730 | int smt_add_var_id_for_node(smtManager_t * sm, AigEdge_t node, int * var_id, int * negated); |
---|
| 731 | void smt_generate_clause_with_aig(smtManager_t * sm, int cur_idx, int var_id, int lvar_id, int rvar_id, array_t * idArr); |
---|
| 732 | void smt_add_clause_for_object(smtManager_t * sm, AigEdge_t obj); |
---|
| 733 | void smt_add_clause_for_iff_fml(smtManager_t * sm); |
---|
| 734 | void smt_add_clause_for_iff_fml_sub(smtManager_t * sm, int z, int x, int y); |
---|
| 735 | void smt_add_clause_for_iff_children(smtManager_t * sm, AigEdge_t node_a, AigEdge_t node_b); |
---|
| 736 | void smt_add_clause_for_ite_fml(smtManager_t * sm); |
---|
| 737 | void smt_add_clause_for_ite_fml_sub(smtManager_t * sm, int x, int y, int z, int f); |
---|
| 738 | int smt_add_clause_for_ite_terminal_case(smtManager_t * sm, int x, int y, int z, int f); |
---|
| 739 | void smt_add_clause_for_ite_children(smtManager_t * sm, AigEdge_t node_a, AigEdge_t node_b, AigEdge_t node_c); |
---|
| 740 | void smt_add_clause_for_ite_chain_fml(smtManager_t * sm, smtFml_t * fml); |
---|
| 741 | satArray_t * smt_get_conjunct_in_fml(smtFml_t * fml, int num_fml); |
---|
| 742 | void smt_add_clause_for_ite_chain_fml_main(smtManager_t * sm); |
---|
| 743 | void smt_add_clause_for_ite_chain_fml(smtManager_t * sm, smtFml_t * fml); |
---|
| 744 | satArray_t * smt_get_conjunct_in_fml(smtFml_t * fml, int num_fml); |
---|
| 745 | void smt_add_clause_for_ite_chain_fml_sub(smtManager_t * sm, smtFml_t * ite_fml, satArray_t * condsArr, satArray_t * thensArr, satArray_t * elses); |
---|
| 746 | void smt_init_generate_cnf(smtManager_t * sm); |
---|
| 747 | int smt_create_clause_with_fml(smtManager_t * sm, smtFml_t * fml); |
---|
| 748 | int smt_put_lit_to_clause(smtCls_t * cls, smtFml_t * fml); |
---|
| 749 | int smt_put_lits_to_clause(smtCls_t * cls, smtFml_t * fml, array_t * conjs); |
---|
| 750 | void smt_create_clause_with_conjuncts(smtManager_t * sm, smtCls_t * cls, array_t * conjs); |
---|
| 751 | int smt_gather_conjuncts_in_and_fml(smtFml_t * fml, array_t * conjs); |
---|
| 752 | int smt_create_clause_with_ands_in_or_fml(smtManager_t * sm, smtFml_t * fml); |
---|
| 753 | /* satArray_t * smt_gather_conjuncts_in_and_fml(smtFml_t * fml); */ |
---|
| 754 | |
---|
| 755 | |
---|
| 756 | |
---|
| 757 | |
---|
| 758 | |
---|
| 759 | |
---|
| 760 | /* smtSat.c */ |
---|
| 761 | int smt_call_theory_solver(satManager_t * m, long bound); |
---|
| 762 | int smt_call_dl_theory_solver(smtManager_t * sm, long bound); |
---|
| 763 | int smt_call_la_theory_solver(smtManager_t * sm, long bound); |
---|
| 764 | void smt_call_dl_theory_solver_preprocess(smtManager_t *sm); |
---|
| 765 | void smt_call_la_theory_solver_preprocess(smtManager_t *sm); |
---|
| 766 | int smt_theory_solve(smtManager_t * sm); |
---|
| 767 | void smt_fit_decision_level_wrt_blocking_clause(satManager_t * m, satArray_t * arr); |
---|
| 768 | |
---|
| 769 | int smt_get_size_of_atom_variable(satManager_t * m); |
---|
| 770 | void smt_dl_theory_undo(smtManager_t * sm); |
---|
| 771 | void smt_la_theory_undo(smtManager_t * sm); |
---|
| 772 | void smt_update_edge_in_constraint_graph(smtManager_t * sm, smtAvar_t * avar); |
---|
| 773 | void smt_delete_edge_in_constraint_graph(smtManager_t * sm, smtEdge_t * e); |
---|
| 774 | smtEdge_t * smt_get_right_end_edge(smtManager_t * sm); |
---|
| 775 | int smt_get_right_end_edge_index(smtManager_t * sm); |
---|
| 776 | void smt_put_right_end_edge_to_deleted(smtEdge_t * deleted, smtEdge_t * rend_edge); |
---|
| 777 | void smt_update_nvar_bound_with_avar(smtManager_t * sm, smtAvar_t * avar); |
---|
| 778 | void smt_add_theory_clause(satManager_t * cm, smtAvar_t * avar, satArray_t * litArr); |
---|
| 779 | |
---|
| 780 | |
---|
| 781 | |
---|
| 782 | /* smtGraph.c */ |
---|
| 783 | smtVertex_t * smt_add_vertex(smtGraph_t * G, int vindex); |
---|
| 784 | smtEdge_t * smt_add_edge(smtGraph_t * G, smtVertex_t * s, smtVertex_t * d, smtAvar_t * avar, int eindex); |
---|
| 785 | smtEdge_t * smt_find_edge(smtVertex_t * s, smtVertex_t * d); |
---|
| 786 | |
---|
| 787 | |
---|
| 788 | |
---|
| 789 | |
---|
| 790 | |
---|
| 791 | |
---|
| 792 | /* smtDl.c */ |
---|
| 793 | int smt_idl_theory_solve(smtManager_t * sm); |
---|
| 794 | int smt_rdl_theory_solve(smtManager_t * sm); |
---|
| 795 | void smt_bellman_ford_main(smtManager_t * sm); |
---|
| 796 | void smt_dl_theory_propagation_main(smtManager_t * sm); |
---|
| 797 | void smt_generate_constraint_graph(smtManager_t * sm); |
---|
| 798 | void smt_init_constraint_graph(smtManager_t * sm); |
---|
| 799 | void smt_init_dists_in_constraint_graph(smtManager_t * sm); |
---|
| 800 | void smt_init_theory_prop_dists(smtManager_t * sm); |
---|
| 801 | void smt_free_constraint_graph(smtGraph_t * G); |
---|
| 802 | void smt_free_vertex(smtGraph_t * G); |
---|
| 803 | void smt_free_edge_implied(satArray_t * imp_edges); |
---|
| 804 | void smt_bellman_ford_algorithm(smtManager_t * sm); |
---|
| 805 | void smt_init_bellman_ford_algorithm(smtManager_t * sm); |
---|
| 806 | void smt_delete_subtree(smtGraph_t * G, smtVertex_t * v); |
---|
| 807 | void smt_collect_edges_in_neg_cycle(smtGraph_t * G, smtVertex_t * v); |
---|
| 808 | void smt_get_lemma_from_neg_cycle(smtManager_t * sm, satArray_t * neg_edges); |
---|
| 809 | void smt_retrieve_previous_distance(smtManager_t * sm); |
---|
| 810 | void smt_update_value_with_current_distance(smtManager_t * sm); |
---|
| 811 | void smt_init_dl_theory_propagation(smtGraph_t * G); |
---|
| 812 | void smt_idl_theory_propagation(smtManager_t * sm); |
---|
| 813 | void smt_rdl_theory_propagation(smtManager_t * sm); |
---|
| 814 | void smt_idl_gather_backward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar); |
---|
| 815 | void smt_idl_gather_forward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar); |
---|
| 816 | void smt_rdl_gather_backward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar); |
---|
| 817 | void smt_rdl_gather_forward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar); |
---|
| 818 | void smt_idl_traverse_backward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth); |
---|
| 819 | void smt_idl_traverse_forward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth); |
---|
| 820 | void smt_rdl_traverse_backward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth); |
---|
| 821 | void smt_rdl_traverse_forward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth); |
---|
| 822 | void smt_idl_gather_backward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * src, int * num_avar); |
---|
| 823 | void smt_rdl_gather_backward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * src, int * num_avar); |
---|
| 824 | void smt_idl_gather_forward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * dest, int * num_avar); |
---|
| 825 | void smt_rdl_gather_forward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * dest, int * num_avar); |
---|
| 826 | void smt_idl_theory_propagation_with_bv_arr(smtManager_t * sm, smtAvar_t * avar); |
---|
| 827 | void smt_idl_theory_propagation_with_fv_arr(smtManager_t * sm, smtAvar_t * avar); |
---|
| 828 | void smt_rdl_theory_propagation_with_bv_arr(smtManager_t * sm, smtAvar_t * avar); |
---|
| 829 | void smt_rdl_theory_propagation_with_fv_arr(smtManager_t * sm, smtAvar_t * avar); |
---|
| 830 | void smt_dl_simple_theory_propagation(smtManager_t * sm); |
---|
| 831 | void smt_get_theory_prop_reason(smtManager_t * sm, smtAvar_t * implying, smtAvar_t * implied, smtNvar_t * bnvar, smtNvar_t * fnvar); |
---|
| 832 | void smt_idl_init_reachable_vertex(smtGraph_t * G); |
---|
| 833 | void smt_rdl_init_reachable_vertex(smtGraph_t * G); |
---|
| 834 | |
---|
| 835 | |
---|
| 836 | |
---|
| 837 | /* smtLa.c */ |
---|
| 838 | int smt_la_theory_solve(smtManager_t *sm); |
---|
| 839 | int smt_la_assert(smtManager_t * sm); |
---|
| 840 | int smt_assert_upper(smtManager_t * sm, smtAvar_t * avar); |
---|
| 841 | int smt_assert_lower(smtManager_t * sm, smtAvar_t * avar); |
---|
| 842 | void smt_la_check(smtManager_t * sm); |
---|
| 843 | void smt_pivot(smtManager_t * sm, smtNvar_t * basic, int row, smtNvar_t * nbasic); |
---|
| 844 | int smt_get_infeasible_basic_row(smtManager_t * sm); |
---|
| 845 | int smt_update_basic_nvar_with_new_value(smtManager_t * sm, smtNvar_t * nvar, double constant); |
---|
| 846 | void smt_find_reason_for_upper_bound(smtManager_t * sm, smtNvar_t * nvar); |
---|
| 847 | void smt_find_reason_for_lower_bound(smtManager_t *sm, smtNvar_t * nvar); |
---|
| 848 | smtNvar_t * smt_get_non_basic_for_increase(smtManager_t * sm, int row); |
---|
| 849 | smtNvar_t * smt_get_non_basic_for_decrease(smtManager_t * sm, int row); |
---|
| 850 | void smt_update_basic_with_new_value(smtManager_t * sm, smtNvar_t * basic, smtNvar_t * nbasic, int row, double constant); |
---|
| 851 | void smt_retrieve_previous_nvar_value(smtManager_t * sm); |
---|
| 852 | void smt_save_current_nvar_value(smtManager_t * sm); |
---|
| 853 | void smt_la_theory_propagation_main(smtManager_t * sm); |
---|
| 854 | void smt_la_simple_theory_propagation(smtManager_t * sm); |
---|
| 855 | void smt_la_theory_init(smtManager_t * sm); |
---|
| 856 | void smt_la_bound_init(smtManager_t * sm); |
---|
| 857 | void smt_generate_tableau(smtManager_t * sm); |
---|
| 858 | void smt_gaussian_elimination(smtManager_t * sm); |
---|
| 859 | void smt_generate_slack_var_for_atom(smtManager_t * sm); |
---|
| 860 | satArray_t * smt_gather_atom_in_database(smtManager_t * sm); |
---|
| 861 | int smt_get_unbounded_nbasic_column_index(smtManager_t * sm, int row); |
---|
| 862 | |
---|
| 863 | |
---|
| 864 | |
---|
| 865 | |
---|
| 866 | /* smtMp.c */ |
---|
| 867 | smtMp_t * smt_mp_init(smtManager_t * sm); |
---|
| 868 | void smt_mp_init_pool(smtMp_t * mp); |
---|
| 869 | void smt_mp_init_nvar_values(smtManager_t * sm); |
---|
| 870 | void smt_mp_init_atom_constants(smtManager_t * sm); |
---|
| 871 | void smt_mp_free(smtMp_t * mp); |
---|
| 872 | void smt_mp_free_pool(smtMp_t * mp); |
---|
| 873 | void smt_mp_free_atom_constants(smtMp_t * mp); |
---|
| 874 | void smt_mp_free_nvar_values(smtMp_t * mp); |
---|
| 875 | void smt_mp_assign_atom_constants(smtManager_t * sm); |
---|
| 876 | void smt_mp_assign_atom_constant(smtMp_t * mp, smtFml_t * avfml); |
---|
| 877 | void smt_mp_get_atom_constant(smtMp_t * mp, smtFml_t * fml, mpq_t * mp_constant, mpq_t * coeff, int nminus); |
---|
| 878 | int smt_mp_dl_theory_solve(smtManager_t * sm); |
---|
| 879 | void smt_mp_bellman_ford_main(smtManager_t * sm); |
---|
| 880 | void smt_mp_generate_constraint_graph(smtManager_t * sm); |
---|
| 881 | void smt_mp_bellman_ford_algorithm(smtManager_t * sm); |
---|
| 882 | void smt_mp_init_bellman_ford_algorithm(smtManager_t * sm); |
---|
| 883 | void smt_mp_retrieve_previous_distance(smtManager_t * sm); |
---|
| 884 | void smt_mp_print_atom_constants(smtManager_t * sm); |
---|
| 885 | void smt_mp_print_value(mpq_t * value); |
---|
| 886 | |
---|
| 887 | |
---|
| 888 | |
---|
| 889 | |
---|
| 890 | /* smtDebug.c */ |
---|
| 891 | void smt_print_atom_variable(smtManager_t * sm); |
---|
| 892 | void smt_print_atom_variable_in_array(smtManager_t * sm, satArray_t * avarArr); |
---|
| 893 | void smt_print_numerical_variable(smtManager_t * sm); |
---|
| 894 | void smt_print_numerical_variable_in_array(satArray_t * nvarArr); |
---|
| 895 | void smt_print_nvar_with_value(smtManager_t * sm); |
---|
| 896 | void smt_print_nvar_value_in_tableau(smtManager_t * sm); |
---|
| 897 | void smt_check_nvar_value_with_tableau(smtManager_t * sm); |
---|
| 898 | void smt_print_nvar_bound_in_tableau(smtManager_t * sm); |
---|
| 899 | void smt_print_atom_for_slack(smtManager_t * sm); |
---|
| 900 | void smt_print_boolean_variable(smtManager_t * sm); |
---|
| 901 | void smt_print_flet_pair(smtManager_t * sm); |
---|
| 902 | void smt_print_cnf_to_smt_file(smtManager_t * sm); |
---|
| 903 | void smt_print_cnf_to_smt_file_with_avar(smtManager_t * sm); |
---|
| 904 | void smt_print_dimacs_to_smt_file(smtManager_t * sm); |
---|
| 905 | void smt_print_cnf_to_dimcas_file(smtManager_t * sm); |
---|
| 906 | void smt_print_fml_to_smt_file(smtManager_t * sm, smtFml_t * fml, int index); |
---|
| 907 | void smt_print_fml_to_file(smtManager_t * sm, smtFml_t * fml); |
---|
| 908 | void smt_print_aig_to_dot_file(Aig_Manager_t * bm); |
---|
| 909 | void smt_print_lit_in_array(smtManager_t * sm, satArray_t * litArr); |
---|
| 910 | void smt_print_lit_in_array_hor(smtManager_t * sm, satArray_t * litArr); |
---|
| 911 | void smt_print_sat_lit_in_array(smtManager_t * sm, satArray_t * litArr); |
---|
| 912 | void smt_print_idl_digraph_to_dot_file(smtGraph_t * G, char * filename); |
---|
| 913 | void smt_print_rdl_digraph_to_dot_file(smtGraph_t * G, char * filename); |
---|
| 914 | int smt_check_dl_lemma_with_yices(smtManager_t * sm); |
---|
| 915 | int smt_check_dl_lit_arr_with_yices(smtManager_t * sm); |
---|
| 916 | void smt_print_variable_to_smt_file(smtManager_t * sm, FILE * fp); |
---|
| 917 | void smt_print_equation_in_tableau(smtManager_t * sm); |
---|
| 918 | void smt_report_result(smtManager_t * sm, int is_model); |
---|
| 919 | void smt_dl_report_result(smtManager_t * sm); |
---|
| 920 | void smt_dl_report_intermediate_result(smtManager_t * sm); |
---|
| 921 | void smt_la_report_result(smtManager_t * sm); |
---|
| 922 | void smt_check_result(smtManager_t * sm); |
---|
| 923 | void smt_print_unknown(void); |
---|
| 924 | void smt_print_watched_lits(satManager_t * cm); |
---|
| 925 | char * smt_convert_atom_to_string(smtAvar_t * avar); |
---|
| 926 | int smt_check_solution(smtManager_t *sm); |
---|
| 927 | int smt_mp_check_solution(smtManager_t *sm); |
---|
| 928 | void smt_print_solution(smtManager_t * sm); |
---|
| 929 | void smt_mp_print_solution(smtManager_t * sm); |
---|
| 930 | |
---|
| 931 | #ifdef __cplusplus |
---|
| 932 | } |
---|
| 933 | #endif |
---|
| 934 | |
---|