source: vis_dev/cusp-1.1/src/smt/smt.h @ 104

Last change on this file since 104 was 12, checked in by cecile, 13 years ago

cusp added
File size: 31.9 KB
Line 
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
53extern "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
207typedef 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 
252typedef struct smtManagerStruct smtManager_t;
253typedef struct smtStatsStruct smtStats_t;
254typedef struct smtGlobalVarStruct smtGlobalVar_t;
255typedef struct smtClauseStruct smtCls_t;
256typedef struct smtFormulaStruct smtFml_t;
257typedef struct smtAvarStruct smtAvar_t;
258typedef struct smtBvarStruct smtBvar_t;
259typedef struct smtNvarStruct smtNvar_t;
260typedef struct smtBoundStruct smtBound_t;
261typedef struct smtFletStruct smtFlet_t;
262typedef struct smtMpStruct smtMp_t;
263typedef struct smtGraphStruct smtGraph_t;
264typedef struct smtVertexStruct smtVertex_t;
265typedef struct smtEdgeStruct smtEdge_t;
266typedef struct smtQueueStruct smtQueue_t;
267 
268/*---------------------------------------------------------------------------*/
269/* Structure declarations                                                    */
270/*---------------------------------------------------------------------------*/
271
272struct 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
337struct 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
368struct 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
399struct smtClauseStruct {
400  satArray_t * litArr; 
401};
402
403struct 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
422struct 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
439struct smtBvarStruct {
440  char * name;
441  int id;
442  int flag;
443
444  AigEdge_t aig_node;
445};
446
447struct smtNvarStruct {
448  char * name;
449  int id; 
450  int flag;
451
452  satArray_t * avarArr;
453};
454
455struct smtBoundStruct {
456  double ub;
457  double lb;
458};
459
460struct smtFletStruct {
461  smtFml_t * fvar_fml;
462  smtFml_t * fml;
463};
464
465struct 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 
481struct 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
514struct smtVertexStruct {
515  satArray_t * ins;
516  satArray_t * outs;
517  satArray_t * targets;
518
519  int index; 
520};
521
522struct 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
535struct 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
549extern 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 */
568int smt_main(char * filename, int timeout, int is_model);
569void smt_read(char * str);
570void SmtFileSetup(FILE * fp);
571int SmtYyparse(void);
572smtManager_t * smt_init(void); 
573smtManager_t * smt_dl_init(void); 
574smtManager_t * smt_la_init(void); 
575void smt_solve(smtManager_t * sm);
576void smt_report(smtManager_t * sm, int is_model);
577void smt_postprocess(smtManager_t * sm);
578void smt_init_global_variable(char * filename);
579void smt_free_global_variable(void);
580void smt_free_key_in_table(st_table * table);
581void smt_free_key_with_array_in_table(st_table * table);
582smtManager_t * smt_init_manager(void);
583void smt_free_manager(smtManager_t * sm);
584void smt_free_clauses(satArray_t * clsArr);
585void smt_free_clauses(satArray_t * clsArr);
586void smt_free_atom_variables(satArray_t * avarArr);
587void smt_free_atom_members(smtAvar_t * avar);
588void smt_free_bool_variables(satArray_t * bvarArr);
589void smt_free_numerical_variables(satArray_t * nvarArr);
590void smt_free_formulas(satArray_t * fmlArr);
591smtStats_t * smt_init_stats(void);
592void smt_circus_interface(smtManager_t * sm);
593void smt_circus_cnf_interface(smtManager_t * sm);
594satArray_t * smt_get_decision_order(smtManager_t * sm);
595
596
597
598
599/* smtPre.c */
600void smt_preprocess(smtManager_t * sm);
601void smt_solve_bool_model(smtManager_t * sm);
602void smt_generate_level_zero_assignments(smtManager_t * sm);
603void smt_update_nvar_adjacent_avar_array(smtManager_t * sm);
604void smt_generate_adjacent_atom_array(smtManager_t * sm);
605void smt_dl_preprocess(smtManager_t * sm);
606void smt_convert_atom_to_dl_form(smtManager_t * sm);
607void smt_generate_avar_sister_array(smtManager_t * sm);
608void smt_la_preprocess(smtManager_t * sm);
609void smt_put_la_clause_to_clause_arr(smtManager_t * sm);
610void smt_convert_lac_into_unit_lac(smtManager_t * sm);
611void smt_init_convert_lac_into_unit_lac(smtManager_t * sm, int * num_nvars, int * num_lavars, int * max_coeffs, int * flags);
612satArray_t * smt_check_nvar_in_atom(smtManager_t * sm, int * num_nvars, int * max_coeffs, int * num_lavars);
613void smt_decide_lac_converting_criterion(smtManager_t * sm, int * flags, int * num_nvars, int * max_coeffs);
614void 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 */
619smtFml_t * smt_create_formula(smtFmlType_t ftype, satArray_t * subfmlArr);
620void smt_duplicate_formula(smtFml_t * new_fml, smtFml_t * org);
621smtFml_t * smt_create_identical_formula(smtFml_t * fml);
622smtFml_t * smt_simplify_formula(smtFml_t * fml);
623void smt_increase_subfml_ins(smtFml_t * fml);
624void smt_add_fml_to_array(smtFml_t * fml);
625smtFml_t * smt_create_returning_formula(smtFml_t * fml);
626smtFml_t * smt_create_function_symbol(char * fs_name);
627smtFml_t * smt_create_predicate_symbol(char * ps_name);
628smtFml_t * smt_create_constant_predicate_symbol(char * ps_name, int value);
629smtFml_t * smt_create_fml_variable(char * fname);
630smtFml_t * smt_create_term_variable(char * fs_name);
631smtFml_t * smt_create_constant_formula(char * cname);
632void smt_simplify_term_fml(smtFml_t * fml, st_table * num_table);
633void smt_save_flet_pair(smtFml_t * fvar_fml, smtFml_t * fml);
634void smt_init_formula_flag(smtManager_t * sm);
635void smt_init_fml_visited_flag(smtManager_t * sm);
636void smt_init_fml_queued_flag(smtManager_t * sm);
637char * smt_convert_fml_to_string(smtFml_t * fml);
638char * smt_convert_fml_to_string_with_subfml(smtFmlType_t type, satArray_t * subfmlArr);
639int smt_is_leaf_fml(smtFml_t * fml);
640int smt_is_abstract_leaf_fml(smtFml_t * fml);
641int smt_is_negated_abstract_leaf_fml(smtFml_t * fml);
642int smt_is_ite_chain_fml(smtFml_t * fml, int num_fml);
643int smt_is_atom_formula(smtFml_t * fml); 
644int smt_is_negated_atom_formula(smtFml_t * fml);
645int smt_is_boolean_formula(smtFml_t * fml);
646int smt_is_negated_boolean_formula(smtFml_t * fml);
647int smt_is_arith_formula(smtFml_t * fml);
648int smt_is_multi_arith_formula(smtFml_t * fml);
649int smt_is_binary_arith_formula(smtFml_t * fml);
650int smt_is_unary_arith_formula(smtFml_t * fml);
651int smt_is_term_formula(smtFml_t * fml);
652int smt_is_bool_atom_fml(smtFml_t * fml);
653int smt_get_constant_value_in_fml(smtFml_t * fml, int * value);
654void smt_convert_term_ite_into_bool_ite_main(smtManager_t * sm);
655void smt_init_convert_term_ite_into_bool_ite(smtManager_t * sm);
656void smt_convert_term_ite_into_bool_ite(smtManager_t * sm, smtFml_t * fml);
657smtFml_t * smt_check_fml_for_term_ite_fml(smtFml_t * fml);
658void smt_convert_term_ite_into_bool_ite_sub(smtManager_t * sm, smtFml_t * fml, smtFml_t * ite_fml);
659smtFml_t * smt_create_ite_term_fml(smtManager_t * sm, smtFmlType_t type, satArray_t * subfmls, smtFml_t * subfml, int ite_index);
660void 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);
661int smt_check_ite_for_terminal_case(smtFml_t * ite_fml);
662void smt_convert_eq_fml_to_ineq_fml(smtManager_t * sm);
663void smt_add_flet_pair_formula(smtManager_t * sm); 
664void smt_convert_eq_fml_into_ineq_and_fml(smtManager_t * sm, smtFml_t * fml);
665void smt_convert_diseq_fml_into_ineq_or_fml(smtManager_t * sm, smtFml_t * fml);
666satArray_t * smt_gather_bvar_in_fml(smtManager_t * sm, smtFml_t * fml);
667
668
669
670
671
672
673/* smtUtil.c */
674smtCls_t * smt_create_clause(void);
675smtCls_t * smt_duplicate_clause(smtCls_t * cls);
676smtFmlType_t smt_get_ar_symbol(char * str);
677smtBvar_t * smt_create_bool_variable(char * name, smtFml_t * bvfml);
678smtBvar_t * smt_create_intermediate_bool_variable(smtManager_t * sm, AigEdge_t node);
679smtNvar_t * smt_create_numerical_variable(char * name, smtFml_t * nvfml);
680void smt_create_dl_atom_variable_main(smtManager_t * sm);
681void smt_create_la_atom_variable_main(smtManager_t * sm);
682void smt_convert_dl_atom_fml_to_bool_fml(smtFml_t * fml, smtAvar_t * avar);
683int smt_convert_atom_to_leq_form(smtManager_t * sm, smtAvar_t * avar);
684char * smt_get_avar_name(smtManager_t * sm, smtAvar_t * avar);
685char * smt_get_neg_avar_name(smtManager_t * sm, smtAvar_t * avar);
686smtAvar_t * smt_create_atom_variable(smtFml_t * avfml);
687smtAvar_t * smt_create_pure_atom_variable(void);
688void smt_init_atom_variable_values(smtManager_t * sm);
689void smt_init_numerical_variable_values(smtManager_t * sm);
690void smt_gather_atom_member(smtAvar_t * avar, smtFml_t * avfml);
691void smt_gather_atom_member_in_fml(smtAvar_t * avar, smtFml_t * fml, int nminus, double coeff);
692void smt_combine_root_fml_with_flet_fml(void);
693void smt_assign_boolean_variable_id(smtManager_t * sm);
694void smt_assign_numerical_variable_id(smtManager_t * sm);
695void smt_assign_numerical_variable_id_in_array(satArray_t * nvarArr);
696void smt_assign_bool_var_flag(smtManager_t * sm); 
697void smt_sort_nvar_array_with_id(satArray_t * arr);
698void smt_sort_nvar_array_with_id_aux(long * arr, long size);
699smtQueue_t * smt_create_queue(long MaxElements);
700void smt_init_queue(smtQueue_t * Q);
701void smt_free_queue(smtQueue_t * Q);
702void smt_enqueue(smtQueue_t * Q, long v);
703long smt_dequeue(smtQueue_t * Q);
704int smt_timeout(int timeout);
705void smt_timeout_handle(void);
706void smt_none(void);
707
708
709
710
711
712
713
714
715
716/* smtCnf.c */ 
717void smt_generate_cnf_main(smtManager_t * sm);
718int smt_generate_cnf(smtManager_t * sm);
719void smt_generate_cnf_with_aig(smtManager_t * sm);
720AigEdge_t smt_generate_aig(smtManager_t * sm);
721int smt_is_ite_terminal_case(AigEdge_t cond_node, AigEdge_t then_node, AigEdge_t else_node);
722void smt_convert_aig_into_cnf(smtManager_t * sm, AigEdge_t aig_node);
723void smt_compute_indegree_for_aig_node(smtManager_t * sm);
724void smt_init_var_id_for_aig_node(smtManager_t * sm);
725void smt_check_leaf_node_for_aig_node(smtManager_t * sm);
726satArray_t * smt_sort_formula_in_bfs_manner(smtManager_t * sm, smtFml_t * root);
727void smt_compute_indegree_in_formula(smtManager_t * sm); 
728array_t * smt_gather_aig_node_from_formula_array(satArray_t * fmlArr);
729int smt_convert_aig_into_cnf_sub(smtManager_t * sm, AigEdge_t node, array_t * idArr, int * negated);
730int smt_add_var_id_for_node(smtManager_t * sm, AigEdge_t node, int * var_id, int * negated);
731void smt_generate_clause_with_aig(smtManager_t * sm, int cur_idx, int var_id, int lvar_id, int rvar_id, array_t * idArr);
732void smt_add_clause_for_object(smtManager_t * sm, AigEdge_t obj);
733void smt_add_clause_for_iff_fml(smtManager_t * sm);
734void smt_add_clause_for_iff_fml_sub(smtManager_t * sm, int z, int x, int y);
735void smt_add_clause_for_iff_children(smtManager_t * sm, AigEdge_t node_a, AigEdge_t node_b);
736void smt_add_clause_for_ite_fml(smtManager_t * sm);
737void smt_add_clause_for_ite_fml_sub(smtManager_t * sm, int x, int y, int z, int f);
738int smt_add_clause_for_ite_terminal_case(smtManager_t * sm, int x, int y, int z, int f);
739void smt_add_clause_for_ite_children(smtManager_t * sm, AigEdge_t node_a, AigEdge_t node_b, AigEdge_t node_c);
740void smt_add_clause_for_ite_chain_fml(smtManager_t * sm, smtFml_t * fml);
741satArray_t * smt_get_conjunct_in_fml(smtFml_t * fml, int num_fml);
742void smt_add_clause_for_ite_chain_fml_main(smtManager_t * sm);
743void smt_add_clause_for_ite_chain_fml(smtManager_t * sm, smtFml_t * fml);
744satArray_t * smt_get_conjunct_in_fml(smtFml_t * fml, int num_fml);
745void smt_add_clause_for_ite_chain_fml_sub(smtManager_t * sm, smtFml_t * ite_fml, satArray_t * condsArr, satArray_t * thensArr, satArray_t * elses);
746void smt_init_generate_cnf(smtManager_t * sm);
747int smt_create_clause_with_fml(smtManager_t * sm, smtFml_t * fml);
748int smt_put_lit_to_clause(smtCls_t * cls, smtFml_t * fml);
749int smt_put_lits_to_clause(smtCls_t * cls, smtFml_t * fml, array_t * conjs);
750void smt_create_clause_with_conjuncts(smtManager_t * sm, smtCls_t * cls, array_t * conjs);
751int smt_gather_conjuncts_in_and_fml(smtFml_t * fml, array_t * conjs);
752int 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 */
761int smt_call_theory_solver(satManager_t * m, long bound);
762int smt_call_dl_theory_solver(smtManager_t * sm, long bound);
763int smt_call_la_theory_solver(smtManager_t * sm, long bound);
764void smt_call_dl_theory_solver_preprocess(smtManager_t *sm);
765void smt_call_la_theory_solver_preprocess(smtManager_t *sm);
766int smt_theory_solve(smtManager_t * sm);
767void smt_fit_decision_level_wrt_blocking_clause(satManager_t * m, satArray_t * arr);
768
769int smt_get_size_of_atom_variable(satManager_t * m);
770void smt_dl_theory_undo(smtManager_t * sm);
771void smt_la_theory_undo(smtManager_t * sm);
772void smt_update_edge_in_constraint_graph(smtManager_t * sm, smtAvar_t * avar);
773void smt_delete_edge_in_constraint_graph(smtManager_t * sm, smtEdge_t * e);
774smtEdge_t * smt_get_right_end_edge(smtManager_t * sm);
775int smt_get_right_end_edge_index(smtManager_t * sm);
776void smt_put_right_end_edge_to_deleted(smtEdge_t * deleted, smtEdge_t * rend_edge);
777void smt_update_nvar_bound_with_avar(smtManager_t * sm, smtAvar_t * avar);
778void smt_add_theory_clause(satManager_t * cm, smtAvar_t * avar, satArray_t * litArr);
779
780
781
782/* smtGraph.c */
783smtVertex_t * smt_add_vertex(smtGraph_t * G, int vindex);
784smtEdge_t * smt_add_edge(smtGraph_t * G, smtVertex_t * s, smtVertex_t * d, smtAvar_t * avar, int eindex);
785smtEdge_t * smt_find_edge(smtVertex_t * s, smtVertex_t * d);
786
787
788
789
790
791
792/* smtDl.c */
793int smt_idl_theory_solve(smtManager_t * sm);
794int smt_rdl_theory_solve(smtManager_t * sm);
795void smt_bellman_ford_main(smtManager_t * sm);
796void smt_dl_theory_propagation_main(smtManager_t * sm);
797void smt_generate_constraint_graph(smtManager_t * sm);
798void smt_init_constraint_graph(smtManager_t * sm);
799void smt_init_dists_in_constraint_graph(smtManager_t * sm);
800void smt_init_theory_prop_dists(smtManager_t * sm);
801void smt_free_constraint_graph(smtGraph_t * G);
802void smt_free_vertex(smtGraph_t * G);
803void smt_free_edge_implied(satArray_t * imp_edges);
804void smt_bellman_ford_algorithm(smtManager_t * sm);
805void smt_init_bellman_ford_algorithm(smtManager_t * sm);
806void smt_delete_subtree(smtGraph_t * G, smtVertex_t * v);
807void smt_collect_edges_in_neg_cycle(smtGraph_t * G, smtVertex_t * v);
808void smt_get_lemma_from_neg_cycle(smtManager_t * sm, satArray_t * neg_edges);
809void smt_retrieve_previous_distance(smtManager_t * sm);
810void smt_update_value_with_current_distance(smtManager_t * sm);
811void smt_init_dl_theory_propagation(smtGraph_t * G);
812void smt_idl_theory_propagation(smtManager_t * sm);
813void smt_rdl_theory_propagation(smtManager_t * sm);
814void smt_idl_gather_backward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar);
815void smt_idl_gather_forward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar);
816void smt_rdl_gather_backward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar);
817void smt_rdl_gather_forward_reachable_vertex_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar);
818void smt_idl_traverse_backward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth);
819void smt_idl_traverse_forward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth);
820void smt_rdl_traverse_backward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth);
821void smt_rdl_traverse_forward_with_dfs(smtGraph_t * G, smtVertex_t * v, int * num_avar, int depth);
822void smt_idl_gather_backward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * src, int * num_avar);
823void smt_rdl_gather_backward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * src, int * num_avar);
824void smt_idl_gather_forward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * dest, int * num_avar);
825void smt_rdl_gather_forward_reachable_vertex_with_bfs(smtGraph_t * G, smtVertex_t * dest, int * num_avar);
826void smt_idl_theory_propagation_with_bv_arr(smtManager_t * sm, smtAvar_t * avar);
827void smt_idl_theory_propagation_with_fv_arr(smtManager_t * sm, smtAvar_t * avar);
828void smt_rdl_theory_propagation_with_bv_arr(smtManager_t * sm, smtAvar_t * avar);
829void smt_rdl_theory_propagation_with_fv_arr(smtManager_t * sm, smtAvar_t * avar);
830void smt_dl_simple_theory_propagation(smtManager_t * sm);
831void smt_get_theory_prop_reason(smtManager_t * sm, smtAvar_t * implying, smtAvar_t * implied, smtNvar_t * bnvar, smtNvar_t * fnvar);
832void smt_idl_init_reachable_vertex(smtGraph_t * G);
833void smt_rdl_init_reachable_vertex(smtGraph_t * G);
834
835
836
837/* smtLa.c */
838int smt_la_theory_solve(smtManager_t *sm);
839int smt_la_assert(smtManager_t * sm);
840int smt_assert_upper(smtManager_t * sm, smtAvar_t * avar);
841int smt_assert_lower(smtManager_t * sm, smtAvar_t * avar);
842void smt_la_check(smtManager_t * sm); 
843void smt_pivot(smtManager_t * sm, smtNvar_t * basic, int row, smtNvar_t * nbasic);
844int smt_get_infeasible_basic_row(smtManager_t * sm);
845int smt_update_basic_nvar_with_new_value(smtManager_t * sm, smtNvar_t * nvar, double constant);
846void smt_find_reason_for_upper_bound(smtManager_t * sm, smtNvar_t * nvar);
847void smt_find_reason_for_lower_bound(smtManager_t *sm, smtNvar_t * nvar);
848smtNvar_t * smt_get_non_basic_for_increase(smtManager_t * sm, int row);
849smtNvar_t * smt_get_non_basic_for_decrease(smtManager_t * sm, int row);
850void smt_update_basic_with_new_value(smtManager_t * sm, smtNvar_t * basic, smtNvar_t * nbasic, int row, double constant);
851void smt_retrieve_previous_nvar_value(smtManager_t * sm);
852void smt_save_current_nvar_value(smtManager_t * sm);
853void smt_la_theory_propagation_main(smtManager_t * sm);
854void smt_la_simple_theory_propagation(smtManager_t * sm);
855void smt_la_theory_init(smtManager_t * sm);
856void smt_la_bound_init(smtManager_t * sm);
857void smt_generate_tableau(smtManager_t * sm);
858void smt_gaussian_elimination(smtManager_t * sm);
859void smt_generate_slack_var_for_atom(smtManager_t * sm);
860satArray_t * smt_gather_atom_in_database(smtManager_t * sm);
861int smt_get_unbounded_nbasic_column_index(smtManager_t * sm, int row);
862
863
864
865
866/* smtMp.c */
867smtMp_t * smt_mp_init(smtManager_t * sm);
868void smt_mp_init_pool(smtMp_t * mp); 
869void smt_mp_init_nvar_values(smtManager_t * sm);
870void smt_mp_init_atom_constants(smtManager_t * sm);
871void smt_mp_free(smtMp_t * mp);
872void smt_mp_free_pool(smtMp_t * mp);
873void smt_mp_free_atom_constants(smtMp_t * mp);
874void smt_mp_free_nvar_values(smtMp_t * mp);
875void smt_mp_assign_atom_constants(smtManager_t * sm);
876void smt_mp_assign_atom_constant(smtMp_t * mp, smtFml_t * avfml);
877void smt_mp_get_atom_constant(smtMp_t * mp, smtFml_t * fml, mpq_t * mp_constant, mpq_t * coeff, int nminus);
878int smt_mp_dl_theory_solve(smtManager_t * sm);
879void smt_mp_bellman_ford_main(smtManager_t * sm);
880void smt_mp_generate_constraint_graph(smtManager_t * sm); 
881void smt_mp_bellman_ford_algorithm(smtManager_t * sm);
882void smt_mp_init_bellman_ford_algorithm(smtManager_t * sm);
883void smt_mp_retrieve_previous_distance(smtManager_t * sm);
884void smt_mp_print_atom_constants(smtManager_t * sm);
885void smt_mp_print_value(mpq_t * value); 
886
887
888
889 
890/* smtDebug.c */
891void smt_print_atom_variable(smtManager_t * sm);
892void smt_print_atom_variable_in_array(smtManager_t * sm, satArray_t * avarArr);
893void smt_print_numerical_variable(smtManager_t * sm);
894void smt_print_numerical_variable_in_array(satArray_t * nvarArr);
895void smt_print_nvar_with_value(smtManager_t * sm);
896void smt_print_nvar_value_in_tableau(smtManager_t * sm);
897void smt_check_nvar_value_with_tableau(smtManager_t * sm);
898void smt_print_nvar_bound_in_tableau(smtManager_t * sm);
899void smt_print_atom_for_slack(smtManager_t * sm); 
900void smt_print_boolean_variable(smtManager_t * sm);
901void smt_print_flet_pair(smtManager_t * sm);
902void smt_print_cnf_to_smt_file(smtManager_t * sm);
903void smt_print_cnf_to_smt_file_with_avar(smtManager_t * sm);
904void smt_print_dimacs_to_smt_file(smtManager_t * sm);
905void smt_print_cnf_to_dimcas_file(smtManager_t * sm);
906void smt_print_fml_to_smt_file(smtManager_t * sm, smtFml_t * fml, int index);
907void smt_print_fml_to_file(smtManager_t * sm, smtFml_t * fml); 
908void smt_print_aig_to_dot_file(Aig_Manager_t * bm);
909void smt_print_lit_in_array(smtManager_t * sm, satArray_t * litArr);
910void smt_print_lit_in_array_hor(smtManager_t * sm, satArray_t * litArr);
911void smt_print_sat_lit_in_array(smtManager_t * sm, satArray_t * litArr);
912void smt_print_idl_digraph_to_dot_file(smtGraph_t * G, char * filename);
913void smt_print_rdl_digraph_to_dot_file(smtGraph_t * G, char * filename);
914int smt_check_dl_lemma_with_yices(smtManager_t * sm);
915int smt_check_dl_lit_arr_with_yices(smtManager_t * sm);
916void smt_print_variable_to_smt_file(smtManager_t * sm, FILE * fp);
917void smt_print_equation_in_tableau(smtManager_t * sm);
918void smt_report_result(smtManager_t * sm, int is_model);
919void smt_dl_report_result(smtManager_t * sm);
920void smt_dl_report_intermediate_result(smtManager_t * sm);
921void smt_la_report_result(smtManager_t * sm);
922void smt_check_result(smtManager_t * sm);
923void smt_print_unknown(void);
924void smt_print_watched_lits(satManager_t * cm);
925char * smt_convert_atom_to_string(smtAvar_t * avar);
926int smt_check_solution(smtManager_t *sm); 
927int smt_mp_check_solution(smtManager_t *sm);
928void smt_print_solution(smtManager_t * sm);
929void smt_mp_print_solution(smtManager_t * sm);
930 
931#ifdef __cplusplus
932}
933#endif
934
Note: See TracBrowser for help on using the repository browser.