source: vis_dev/cusp-1.1/src/sat/sat.h @ 54

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

cusp added
File size: 29.4 KB
RevLine 
[12]1#include <stdio.h>
2#include <stdint.h>
3#include <zlib.h>
4
5#if defined(__GNUC__)
6# define DD_INLINE __inline__
7# if (__GNUC__ >2 || __GNUC_MINOR__ >=7)
8#   define DD_UNUSED __attribute__ ((__unused__))
9# else
10#   define DD_UNUSED
11# endif
12#else
13# if defined(__cplusplus)
14#   define DD_INLINE inline
15# else
16#   define DD_INLINE
17# endif
18# define DD_UNUSED
19#endif
20
21
22typedef struct satManagerStruct satManager_t;
23typedef struct satClauseStruct satClause_t;
24typedef struct satArrayStruct satArray_t;
25typedef struct satHeapStruct satHeap_t;
26typedef struct satSmtManagerStruct satSmtManager_t; /** sateen: smt manager **/ 
27typedef struct satSmtVarStruct satSmtVar_t;         /** sateen: smt variable **/ 
28typedef struct satTernaryStruct satTernary_t;       /** alembic: ternary structure **/
29typedef struct satTrieStruct satTrie_t;             /** alembic: trie structure **/
30typedef struct satQueueStruct satQueue_t;           /** varelim: queue structure **/
31
32typedef struct satStackStruct satStack_t;           /** standard stack structure **/
33typedef struct satSCCStruct satSCC_t;               /** SCC structure **/
34
35#define SMT_ADD_THEORY
36#define OPTIMIZE_CLAUSE
37#define LUBY_RESTART
38
39struct satHeapStruct {
40        long size;
41        int (*compare)(void *, const void *, const void *);
42        long *heap;
43        long *indices;
44};
45
46struct satArrayStruct {
47        long total;
48        long size;
49        long space[0];
50};
51
52struct satQueueStruct {
53        long max;               /* max size of queue */
54        long size;              /* The number of entries */
55        long first;             /* The front index of entries */
56        long last;              /* The last index of entries */
57        long elems[0];          /* The location to save entries */ 
58};
59
60struct satStackStruct {
61        long max;               /* max size of queue */
62        /*long size;*/          /* The number of entries */
63        long top;               /* The top index of entries */
64        long elems[0];          /* The location to save entries */ 
65};
66
67struct satSCCStruct {
68        unsigned idx;
69        unsigned min;
70        int done;
71};
72
73struct satTernaryStruct {
74        satTernary_t *lokid;            /* lower child */
75        union { satTernary_t *eqkid[2]; /* equal child */ 
76                satClause_t *c; }eqleaf;/* pointer of a clause */ 
77        satTernary_t *hikid;            /* higher child */
78        int valid;                      /* valid mark */ 
79        long id;                        /* node id */
80};
81
82struct satTrieStruct{
83        long id;                        /* node id or clause index */
84        long depth;                     /* depth in a tree */
85        satArray_t *child[2];           /* children */
86        satTrie_t *parent;              /* parent */
87        int valid;                      /* valid mark */
88};
89
90
91struct satClauseStruct {
92        long size; 
93        union { double activity; long abstract; } info;
94        satArray_t *dependent;
95        long lits[0];
96};
97
98struct satManagerStruct {
99        long status;
100        long nVars;
101        long nClauses;
102        satArray_t *clauses; /*array of satClause_t * */
103        satArray_t *learned; /*array of satClause_t * */
104        satArray_t *blocking; /*array of satClause_t * */
105        satArray_t *theory; /*array of satClause_t * */
106        satArray_t *deleted; /*array of satClause_t * */
107        satArray_t *shortClauses; /*array of satClause_t * */
108        satHeap_t *variableHeap;
109        satArray_t *decisionStackSeperator; /* array of long */
110        satArray_t *previousDecisionHistory; /* array of long */
111
112        char    *values; 
113        char    *marks; 
114        char    *visits; 
115        long    *dominator; 
116        long    *dominator2; 
117        char    *dummy; 
118        char    *equi;
119        char    *pure;
120        char    *bvars;  /** HH: boolean variables marked by Sateen **/
121        satArray_t **wls; 
122        satClause_t **antes; 
123
124       
125        long *levels; 
126        long *decisionStack; /* array of long */
127        long *maps;
128        long curPos; /* first unimplicated variable  */
129        long curBinPos; /* first unimplicated variable  */
130        long stackPos; /* position of last assigned variable */
131        long nCurConflicts;
132        long preLevelZeroStackPos;
133        long polarityChangeLimit;
134
135        char    *removable; 
136        char    *unremovable; 
137        int     minimizeConflictLimit;
138        double  *activity;
139        int     minimizeAssert;
140        int     minimizeAssertLimit;
141        int     implydepth;
142        long    minimizeAssertTry;
143
144        long    nRestarts;
145        double  progress;
146
147        double  varDecay;
148        double  clauseDecay;
149        double  varInc;
150        double  clauseInc;
151        double  learnedSizeFactor;
152        double  learnedSizeInc;
153
154        double  restartFirst;
155#ifdef LUBY_RESTART
156        long    restartInc;
157#endif
158#ifndef LUBY_RESTART
159        double  restartInc;
160#endif
161        long    restartIndex;
162        double  randomSeed;
163        double  randomFrequency;
164
165        long  reduceClausesThresh;
166
167        satArray_t *clearned;
168        satArray_t *elearned;
169        satArray_t *cclearned;
170        satArray_t *redundant;
171        satArray_t *tlearned;
172        satArray_t *dependent;
173        satArray_t *temp;
174        satArray_t *tempUnitClauses;
175        satArray_t *seen;
176        satArray_t *subsumedClauseArray;
177        satArray_t *mdominatorClause;
178
179        double nStarts, nDecisions, nRandomDecisions;
180        double nHistoryDecisions, nTHistoryDecisions;
181        double nImplications, nConflicts;
182        double nCurClauseLits, nCurLearnedLits;
183        double nTotalClauseLits, nTotalLearnedLits;
184        double nTotalLearnedClauses, nCurLearnedClauses;
185        double preTotalLearnedCl, preTotalLearnedLit;
186        double nCurBlockingClauses, nCurBlockingLits;
187        double nTotalBlockingClauses, nTotalBlockingLits;
188        double nSubsumedClauses, nSubsumedDeletedLiterals;
189        int    nSimplify;
190
191        double preJumpCl;
192        double nForceRestart;
193        double nPolarityChange;
194
195        long nReduceClauses;
196        long nFirstUip;
197        long simpDBAssigns;
198        long simpDBProps;
199        long n2LitClauses;
200        long nJump;
201        long nLevel;
202        long bsAssigns;
203        long nLearnedDom;
204        long nLearnedMDom;
205
206        double  readTime;
207        double  solveTime;
208        double  preJump;
209        double  preLit;
210
211        int enableFrequentRestart;
212        int buildBridge;
213        int useRandom;
214        int defaultSign;
215        int polarityMode;
216        int changeDirection;
217        int allSat;
218        int coreGeneration;
219        int includeLevelZero;
220        int enableSimplify;
221        int usePreviousDecisionHistory;
222        int checkSubsumption;
223        int printModel;
224        int enableAddTheoryClause; /* Hyondeuk Kim */
225        int enableOptimizeClause; /* Hyondeuk Kim */
226
227        satClause_t *nullClause;
228
229        void *SMTManager; /* sateen pointer */
230        satArray_t *explanation; /*array of int */
231
232        /** HHJ: Elements for Alembic/distillation **/
233        long tempInt;                   /* Temporary usage */
234        int verbosity;                  /* Verbose level */
235        char *cnfFileName;              /* Name of cnf file */
236        FILE *LGF;                      /* Name of log file */
237        char *outfile;                  /* Name of output cnf file */
238        long *scores;                   /* Scores of literals */
239        long *clausesList;              /* Clauses list of literals */
240        long *clausesLearnedList;       /* Clauses learned list of literals */
241        satArray_t *candidates;         /* candidates for simplification */
242        satTernary_t *ternary;          /* Ternary root */
243               
244        /** Options **/
245        char *simpCnf;                  /* Simplified CNF */
246        int substitute;                 /* turn on equivalent variables substitution */ 
247        int writeCnf;                   /* Writing simplified CNF */
248        int simplify;                   /* Simplification mode */
249        int eliminateVar;               /* Variable elimination only mode */ 
250        int distill;                    /* Distillation mode */
251        int computeSCC;                 /* Computation of strongly connected component */
252        int nIteratePreprocess;         /* N interations of preprocessing */ 
253        int subsumeInConflict;          /* Subsumption check in conflict analysis */
254        int minimizeConflict;           /* Conflict clause minimization */
255        int writeSimplifiedCNF;         /* Exit after writing a simplified CNF file */
256        int periodicDistill;            /* Periodic distillation */
257        int writeStatistics;            /* Write a statistics file */
258        int limitDistill; 
259        long distillMin;                /* Minimum length of clause to distill */
260        long distillMax;                /* Maximum length of clause to distill */
261        long preLearnedPos;             /* Index of the array of new conflicts */
262       
263        double distillInc;              /* Periode of distillation */
264     
265        double reductionWithDistill;    /* Threshold for periodic distillation */
266        long boundPeriodicDistill;      /* Value to bound periodic distillation */
267        long nRejectDistill;            /* The number of rejects to distill */ 
268        double distillTime;             /* Time spent for distillations */
269        double elimTime;                /* Time spent for eliminations */
270        double nImplicationsInDistill;   /* The number of implications in distillation */
271 
272        long nTernaryNodes;             /* The number of built trie node */
273        long nVisitedTernaryNodes;              /* The number of visited tries nodes */
274        long nInClForDistill;           /* The number of input clauses for distillation */
275        long nInLitForDistill;          /* The number of input literals for distillation */
276        long nInLearnedClForDistill;    /* The number of input learned clauses for distillation */
277        long nInLearnedLitForDistill;   /* The number of input learned literals for distillation */
278        long nOutClForDistill;          /* The number of output clauses for distillation */
279        long nOutLitForDistill;         /* The number of output literals for distillation */
280        long nOutLearnedClForDistill;   /* The number of output learned clauses for distillation */
281        long nOutLearnedLitForDistill;  /* The number of output learned literals for distillation */
282        long nDeletedVar;               /* The number of delete variables */
283        long nOldLearnedInDistill;      /* The number of old conflicts in distillation */
284        long nLearnedInDistill;         /* The number of conflicts in distillation */
285        long nResolvedInDistill;        /* The number of resolvents in distillation */
286        long nDistill;                  /* The number of distillation */
287        long nSATCl;                    /* The number of clauses satisfied */
288        long nLearnedClInDistill;       /* The number of learned clauses in distillation */
289        long nLearnedLitInDistill;      /* The number of learned literals in distillation */
290        long nLearnedUnitClInDistill;   /* The number of learned unit clauses in distillation */
291        long nUIPConflictClauses;       
292        long nUIPConflictLits;
293
294        /** HH : On-the-fly clause improvement **/
295        long nExtraSubsumes;
296        long depthOfConflict;
297        long depthOfStrong;
298        long depthOfOTS;
299        long nDistillInConflict;        /* The number of subsumptions with OCI */
300        long nEliminatedClsInConflict;  /* The number of clauses eliminated in OCI */
301        long nEliminatedLitsInConflict; /* The number of literals eliminated in OCI */
302        long nOmittedConflictClauses;   /* The number of omitted conflict clauses */
303        long nOmittedConflictLits;      /* The number of omitted conflict literals */
304
305        long nAuxLearnedClauses;        /* The number of auxilary learned clauses */
306        long nAuxLearnedLits;           /* The number of auxilary learned literals */
307        long nAuxConflictAnalysis;      /* The number of auxilary conflict analysis */ 
308
309        /** HHJ : Variable Elimination **/
310        satHeap_t *varElimHeap;         /* Heap for variable elimination */
311        satQueue_t *satQueue;           /* Queue for sat */
312        satStack_t *satStack;           /* Stack for sat */
313        satArray_t *resolvents;         /* Literal pool of resolvent created by variable elimination */
314        satArray_t *elimtable;          /* Array of the elimtable variables */
315        char *litMarks;                 /* Array of the marks of the literals */
316        long majorityClauseLength;      /* Majority clause length */
317        long minorityClauseLength;      /* Non majority clause length */
318        long *clausesHistogram;         /* Statistics of clause sizes */
319        long grow;                      /* Bound of the number of clauses increases */
320        long nInputVars;
321        long nInputClauses;
322        long nInputLiterals;
323        long nEquiVars;                 /* The number of variables in equivalent relation */
324        long nVarElimTry;               /* The number of variables check in elimination */     
325        long nVarElimReject;            /* The number of variables declined in elimination */   
326        long nSubsumeTry;               /* The number of calls of backward subsumption */
327        long nLits;                     /* The number of original literals */
328        long nResolvents;               /* The number of resolvents generated */
329        long nResolventLits;            /* The number of resolvent literals */
330        long nEliminatedCls;            /* The number of eliminated original clauses */
331        long nEliminatedLits;           /* The number of eliminated literals */
332        long nEliminatedVars;           /* The number of eliminated variables */
333        long nSelfsubsume;              /* The number of selfsubsumptions in resolution */
334        long nBackwardSelfsubsume;      /* The number of selfsubsumptions in backward check */
335        long nLitStrengthened;          /* The number of literals removed by slefsubsumption */
336        long nNewUnitLits;              /* The number of unit literals generated */
337        long nDuplicates;               /* The number of duplicate literals by substitution */
338        long nNewTautologies;           /* The number of additional tautology cases by substitution */
339
340        int conflictLevels[5];
341        int *mcla;
342        int mclaSize;
343        int mclaTotal;
344        int maxContiguousLevel;
345        int maxContiguousLevelTotal;
346        int maxContiguousLevelCount;
347        int maxContiguousLimit;
348        double preThickTail;
349        int maxContiguousDataCollect;
350        int maxContiguousData[6];
351        int nStrongConflictClauses;
352        int nSupplementalConflictClauses;
353
354        /** HH: Dominator based learning **/
355#ifdef HH_BINARY
356        long *binWls;          /** HH: the number of binary clauses in each watched literal list **/
357#endif
358        long nBinImplications;  /** HH: the number of binary implications **/
359        long nDomSubsumes;      /** HH: the number of subsuming dominator clauses **/
360        long nDomStrengthened;  /** HH: the number of subsuming dominator clauses **/
361        long nMDomStrengthened;  /** HH: the number of subsuming multiple dominator clauses **/
362        long nDomEliminated;  /** HH: the number of eliminated dominator
363                                clauses **/
364        long nMergeUnit;      /** HH: the number of unit clauses by merging
365                                two literal clauses **/
366        long simplimit;      /** HH: limit of simplification **/ 
367
368
369        long nCurImps;          /** HH: the number of implications at the current level **/
370        long nPerSimVars;
371        long nPerSimCls;
372        long nPerSimLearnd; 
373        long nPerSimLits;
374        long nPerSimLearnedLits;
375        long nPerSim;
376
377        long *repr;
378        long equiv;
379        long mergedv;
380        long nSCCs;
381        long nMerged;
382        long nDuplicateLits;
383};
384
385/** HHJ : The number of flag bits of clause
386 *        has been changed from 4.
387 **/
388#define SATCsizeShift           5
389#define SATCLearned             1
390#define SATCBlocking            2
391#define SATCTheory              4
392#define SATCVisited             8
393#define SATCIrredundant         16     
394#define SATCMask                31
395#define SATCTypeMask            7
396#define SATSizeClause(c)        (c->size >> SATCsizeShift)
397#define SATVar(l)               (l >> 1)
398#define SATSign(l)              (l & 1)
399#define SATValue(m, l)          ((m->values(SATVar(l))) ^ SATsign(l))
400#define SATCurLevel(m)          (m->decisionStackSeperator->size)
401#define SATClauseLearned(c)     (c->size & 1)
402#define SATClauseBlock(c)       (c->size & 2)
403
404/** HHJ : New macros **/
405#define SATClauseOriginal(c)    ((c->size & 15) == 0)
406#define SATClauseIrredundant(c) (c->size & SATCIrredundant)
407#define SATClauseVisited(c)     (c->size & SATCVisited)
408/*---------------------------------------------------------------------------*/
409/* Constant declarations                                                     */
410/*---------------------------------------------------------------------------*/
411#ifndef CUR_DATE
412#define CUR_DATE        "<compile date not supplied>"
413#endif
414
415#ifndef CUR_VER
416#define CUR_VER         "U of Colorado/Boulder, CirCUs Release 2.0"
417#endif
418
419
420void TimeOutHandle(void);
421void MemOutHandle(void);
422char * DateReadFromDateString( char * datestr);
423long sat_mem_used(int field);
424
425satArray_t *sat_array_alloc(long num);
426satArray_t *sat_array_insert(satArray_t *arr, long datum);
427satArray_t *sat_array_alloc_insert(satArray_t *arr, long datum);
428satArray_t *sat_array_copy(satArray_t *arr1, satArray_t *arr2);
429satArray_t *sat_array_realloc(satArray_t *arr, long size);
430satQueue_t *sat_queue_alloc(long num);
431
432int sat_main(char * filename, int timeout, satArray_t* options);
433
434int sat_read_cnf(satManager_t *m, char *filename);
435satHeap_t *sat_heap_init(satManager_t *m, int (*compare_heap)(void *, const void *, const void *));
436void sat_heap_free(satHeap_t *h);
437void sat_heap_insert(satManager_t *m, satHeap_t *h, long n);
438void sat_heap_remove_var_assigned_level_zero(satManager_t *m, satHeap_t *h);
439long sat_heap_remove_min(satManager_t *m, satHeap_t *h);
440int sat_heap_check(satManager_t *m, satHeap_t *h, long i);
441void sat_heap_update(satManager_t *m, satHeap_t *h, long n);
442void sat_heap_resize(satManager_t *m, satHeap_t *h, long prenVars);
443int compare_sort_learned(const void *x1, const void *y1);
444int compare_sort_variable_id(const void *x1, const void *y1);
445int compare_sort_learned(const void *x1, const void *y1);
446int compare_sort_theory(const void *x1, const void *y1);
447int compare_sort_block(const void *x1, const void *y1);
448void sat_generate_next_restart_bound(satManager_t *m);
449void sat_print_clause_array(satManager_t *m, satArray_t *learned);
450void sat_decide_polarity_new(satManager_t *m);
451void sat_reduce_blocking_clauses(satManager_t *m);
452int sat_compare_activity(void *activity, const void *x, const void *y);
453int sat_print_unsat_core(satManager_t *m, char *cnfFilename);
454void sat_print_assignment(satManager_t *m);
455
456satArray_t *sat_optimize_clause_with_implication_graph(satManager_t *m, satArray_t *clearned);
457void sat_array_delete_elem(satArray_t *arr, long elem);
458void sat_enqueue_check(satManager_t *m, long lit, satClause_t *ante);
459void sat_circus_solve(satManager_t *m);
460void sat_dpll(satManager_t *m, long nConflicts);
461int sat_backward_subsumption_check(satManager_t *m);
462void sat_enqueue(satManager_t *m, long lit, satClause_t *ante);
463void sat_add_watched_literal(satManager_t *m, satClause_t *c);
464void sat_delete_watched_literal(satManager_t *m, satClause_t *c);
465void sat_delete_clause(satManager_t *m, satClause_t *c);
466void sat_simplify(satManager_t *m);
467void sat_undo(satManager_t *m, long level);
468void sat_reduce_learned_clauses(satManager_t *m);
469void sat_update_clause_activity(satManager_t *m, satClause_t *c);
470void sat_update_variable_activity(satManager_t *m, long v);
471void sat_update_clause_decay(satManager_t *m);
472void sat_update_variable_decay(satManager_t *m);
473void sat_print_literal(satManager_t *m, long lit, FILE *fp);
474void sat_print_clause(satManager_t *m, satClause_t *c);
475void sat_verify(satManager_t *m);
476int sat_verify_original_cnf(satManager_t *m, char *filename);
477void sat_remove_satisfied_clauses(satManager_t *m, satArray_t *arr);
478void sat_report_result(satManager_t *m);
479void sat_free_manager(satManager_t *m);
480void sat_conflict_analysis_for_literal(satManager_t *m, long tLit);
481void sat_conflict_analysis_strong(satManager_t *m, satClause_t *conflicting, long sLimit, long implLimit);
482void sat_conflict_analysis_supplemental(satManager_t *m, satClause_t *conflicting, long refV, long sLimit);
483long sat_conflict_analysis_empowerment(satManager_t *m, satClause_t *conflicting, long rLevel);
484void sat_init_variable_activity(satManager_t *m, satClause_t *c);
485void sat_check_equivalent_relation(satManager_t *m);
486void sat_print_dot_for_implication_graph( satManager_t *m, satClause_t *c, long level, int iAllLevel);
487void sat_print_clause_simple(satManager_t *m, satClause_t *c);
488void sat_print_clauses(satManager_t *m, satArray_t *learned);
489void sat_print_cnf(satManager_t *m, long iter);
490void sat_clean_up_equi_job(satManager_t *m, satArray_t *save0);
491void sat_update_equivalent_class(satManager_t *m, satArray_t *arr, long leanred);
492void sat_decide_polarity(satManager_t *m);
493
494
495satClause_t *sat_implication(satManager_t *m);
496satClause_t *sat_add_clause(satManager_t *m, satArray_t *arr, long learned);
497satClause_t *sat_add_clause_only(satManager_t *m, satArray_t *arr, long learned);
498satClause_t *sat_new_clause(satArray_t *arr, long learned);
499satClause_t *sat_check_equivalent_relation_aux(satManager_t *m);
500
501long sat_get_mapped_index(satManager_t *m, long index);
502long sat_abstract_level(satManager_t *m, long v);
503long sat_make_decision(satManager_t *m);
504long sat_conflict_analysis(satManager_t *m, satClause_t *conflicting);
505void sat_estimate_progress(satManager_t *m);
506void sat_print_cnf_less_than(FILE *fp, satArray_t *arr, long limit);
507void sat_print_implication_graph(satManager_t *m, long level);
508void sat_print_database(satManager_t *m);
509void sat_print_variables(satManager_t *m);
510int sat_read_cnf(satManager_t *m, char *filename);
511void sat_create_database(satManager_t *m);
512int sat_check_complementary(int depth, int nLits, double avg);
513void sat_change_search_direction(satManager_t *m);
514int sat_is_redundant_lit(satManager_t *m, long lit, long absLevel);
515void sat_check_marks(satManager_t *m);
516void sat_decide_restart(satManager_t *m, long nConflicts);
517satClause_t * sat_add_learned_clause(satManager_t *m, satArray_t *learned);
518void sat_reduce_theory_clauses(satManager_t *m);
519void sat_make_dependent_graph(satManager_t *m, satClause_t *c);
520void sat_generate_unsat_core_main(satManager_t *m);
521void sat_generate_unsat_core(satManager_t *m, satClause_t *cl);
522void sat_free_clause_array(satArray_t *arr);
523
524char *sat_remove_space(char *line);
525char *sat_copy_word(char *lp, char *word);
526double sat_drand(satManager_t *m);
527satManager_t * sat_init_manager();
528void sat_mark_for_pure_lits(satManager_t *m, satClause_t *c);
529satArray_t * sat_generate_unsat_core_clauses_index_array(satManager_t *m);
530satClause_t * sat_add_theory_clause(satManager_t *m, satArray_t *learned);
531satClause_t * sat_add_blocking_clause(satManager_t *m, satArray_t *learned);
532void sat_add_blocking_clause_for_theorem_prover(satManager_t *m, satArray_t *arr);
533
534int smt_get_size_of_atomic_variable(satManager_t *m);
535int smt_call_theory_solver(satManager_t *m, long bound);
536void smt_theory_undo(satManager_t *m);
537void sat_print_clause_in_dimacs(FILE *fp, satArray_t *arr);
538
539void sat_init_options_for_varelim(satManager_t *m);
540void sat_init_options_for_distill(satManager_t *m);
541
542void sat_distill_clauses_array(satManager_t *m, satArray_t* clauses, long learned);
543void sat_choose_candidates_for_distillation(satManager_t *m, satArray_t* clauses);
544void sat_reshape_cnf_database_with_distilled_clauses(satManager_t *m, int checkSubsumption);
545void sat_squeeze_clauses_array(satManager_t *m, int checkSubsumption);
546void sat_build_ternary_tree(satManager_t *m, satArray_t *clauses);
547void sat_ternary_tree_based_implication(satManager_t *m, satTernary_t *ternary, int depth, long learned);
548void sat_distill_clauses_with_restarting(satManager_t *m);
549void sat_distill_clauses_with_preprocessing(satManager_t *m);
550void sat_distill_clauses(satManager_t *m);
551void sat_report_result_for_distillation(satManager_t *m);
552void sat_print_array_as_clause(satManager_t *m, satArray_t *arr);
553void sat_add_all_watched_literal(satManager_t *m, satClause_t *c);
554void sat_sort_literal_by_score(satArray_t *arr, long *scores);
555void sat_sort_literal_by_score_aux(long *lits, long *scores, long size);
556void sat_insert_ternary_tree(satTernary_t *root, satArray_t *clause);
557void sat_free_clause(satClause_t *c);
558void sat_make_decision_based_on_trie(satManager_t *m, long lit);
559void sat_conflict_analysis_on_decisions(satManager_t *m, satArray_t *clearned, satClause_t *traversed, long learned);
560void sat_ternary_tree_based_undo(satManager_t *m, long level);
561void sat_print_scores(satManager_t *m);
562void sat_assert_pure_literals(satManager_t *m);
563void sat_delete_unmakred_clauses_for_simplification(satManager_t *m);
564void sat_free_ternary(satTernary_t *ternary);
565void sat_sort_clause_array_by_length(satArray_t *cl);
566void sat_strengthen_clause_in_conflict_analysis(satManager_t *m, satClause_t *c, int marked);
567int sat_check_subsumption_resolvent_and_clause(satManager_t *m, satClause_t *c, long nMarks);
568long sat_conflict_analysis_with_distillation(satManager_t *m, satClause_t *conflicting, long learned);
569int sat_check_subsumption_in_conflict_analysis(satManager_t *m, satClause_t *cp, satClause_t *cq);
570int sat_recompute_var_score(satManager_t *m);
571satClause_t* sat_resolvent_analysis(satManager_t *m, satTernary_t *t, long learned);
572satClause_t * sat_implication_for_simplification(satManager_t *m);
573satClause_t* sat_add_distilled_clause(satManager_t *m, satArray_t *arr, long learned);
574long sat_get_decision_lit(satManager_t *m, long level);
575void sat_check_marked_variables_on_decision_stack(satManager_t *m);
576void sat_traverse_ternary_tree_to_print_out_dot(satManager_t *m, FILE *fp, satTernary_t *ternary, long *nNode);
577
578
579int sat_eliminate_var_main(satManager_t *m);
580int sat_eliminate_var(satManager_t *m, long v);
581int sat_merge_sort_literals(satManager_t *m, satClause_t *cp, satClause_t *cq, long cpindex, long cqindex, long v);
582int sat_strengthen_clause(satManager_t *m, satClause_t *c, long index);
583int sat_elimination_progress(satManager_t *m);
584void sat_extend_model(satManager_t *m);
585void sat_reset_all_watched_lists(satManager_t *m);
586void sat_build_occurrence_list(satManager_t *m);
587satClause_t * sat_implication_on_all_watched_literals(satManager_t *m);
588int sat_backward_subsumption_check(satManager_t *m);
589void sat_gather_touched_clauses(satManager_t *m);
590void sat_recover_clauses_DB(satManager_t *m);
591int sat_squeeze_clause(satManager_t *m, satClause_t *c);
592void sat_remove_marked_clauses(satManager_t *m, satArray_t *arr);
593void sat_init_clauses_statistics(satManager_t *m);
594void sat_update_clauses_statistics(satManager_t *m, satClause_t *c);
595long sat_check_clauses_high_density(satManager_t *m);
596void sat_print_clauses_histogram(satManager_t *m);
597void sat_check_duplications_in_clauses(satArray_t *clauses);
598int sat_check_clauses_duplicate(satClause_t *cp, satClause_t *cq);
599void sat_strengthen_clause_in_conflict_analysis(satManager_t *m, satClause_t *c, int marked);
600void sat_strengthen_set_of_clauses_in_conflict_analysis(satManager_t *m);
601int sat_check_subsumption_in_conflict_analysis(satManager_t *m, satClause_t *cp, satClause_t *cq);
602int sat_check_subsumption_resolvent_and_clause(satManager_t *m, satClause_t *c, long nMarks);
603satClause_t *sat_copy_clause(satManager_t *m, satClause_t *c);
604void sat_calculate_restart_bound_new(satManager_t *m);
605void sat_check_duplicate_literals(satManager_t *m, satClause_t *c);
606int sat_minimize_conflict(satManager_t *m, long v, int depth);
607void sat_cleanup_for_minimize_conflict(satManager_t *m, satArray_t *arr);
608void sat_check_duplicate_literals(satManager_t *m, satClause_t *c);
609long sat_number_of_current_implications(satManager_t *m);
610satClause_t * sat_binary_implication(satManager_t *m);
611satClause_t* sat_find_binary_clause(satManager_t *m, long a, long b);
612void sat_print_options(satManager_t *m);
613void sat_assert_pure_literals(satManager_t *m);
614int sat_minimize_asserting(satManager_t *m, long v, int depth);
615void sat_cleanup_for_minimize_assert(satManager_t *m, satArray_t *arr);
616void sat_insert_clauses_into_subsumption_check_queue(satManager_t *m, satArray_t *clauses);
617long sat_get_literal_index_of_clause(satManager_t *m, satClause_t *c, long lit);
618void sat_set_clause_deleted(satManager_t *m, satClause_t *c);
619
620void sat_add_resolvents_from_lit_pool(satManager_t *m, satArray_t *pool);
621void sat_report_result_for_var_elim(satManager_t *m);
622long sat_get_literal_index_of_clause(satManager_t *m, satClause_t *c, long lit);
623void sat_calculate_clause_abs(satClause_t *c);
624void sat_clean_all_watched_lists_of_clause(satManager_t *m, satClause_t *c);
625void sat_clean_all_watched_list_of_literal(satManager_t *m, long lit);
626void sat_clean_all_watched_list_of_variable(satManager_t *m, long v);
627long sat_get_num_assignments_of_a_level(satManager_t *m, long level);
628void sat_clean_resolvents_DB(satManager_t *m, long v, long begin);
629void sat_mark_clauses_of_var_deleted(satManager_t *m, long v);
630void sat_mark_occur_list_to_be_deleted(satManager_t *m, long index);
631void sat_find_value_of_eliminated_var_on_clauses(satManager_t *m, satArray_t *clauses, long v);
632void sat_make_resolution_graph(satClause_t *c, satClause_t *ct);
633void sat_delete_dependencies_of_clause_array(satArray_t *arr);
634long sat_delete_redundant_resolvents(satManager_t *m, satClause_t *cp);
635void sat_check_resolvent_dependencies(satManager_t *m, satClause_t *cp, satClause_t *cq, satClause_t *c);
636void sat_print_clause_array_part(satManager_t *m, satArray_t *arr, long begin, long end);
637void sat_print_current_DB_to_cnf(satManager_t *m, char *cnfFilename);
638void sat_write_eliminated_DB(satManager_t *m, int turnOffClauses);
639void sat_check_all_watched_list_of_eliminsated_variables(satManager_t *m);
640long sat_check_unit_clause(satManager_t *m, satClause_t *c);
641int sat_check_clause_after_merge_sort(satManager_t *m, satArray_t *arr, long begin);
642int sat_check_all_clauses_sorted(satManager_t *m);
643int sat_delete_clause_from_watched_list(satManager_t *m, satClause_t *c, long wlindex, long cindex);
644int sat_verify_watched_literal(satManager_t *m, satClause_t *c);
645
646inline long sat_subsume_on_sorted_clauses(satManager_t *m, satClause_t *cp, satClause_t *cq); 
647inline long sat_subsume_on_clauses(satManager_t *m, satClause_t *cp, satClause_t *cq);
648
649int sat_compress_clause(satManager_t *m, satClause_t *c);
650void sat_sort_literal_aux(long *lits, long size);
651void sat_sort_clause_array(satArray_t *arr, int (*compare_sort)(const void *, const void *));
652void sat_sort_clause_array_aux(long *carr, long size,  int (*compare_sort)(const void *, const void *));
653void sat_literal_array_sort(satArray_t *arr);
654void sat_sort_clause_literal(satClause_t *c);
655
656void sat_heap_up(satManager_t *m, satHeap_t *h, long i);
657void sat_heap_down(satManager_t *m, satHeap_t *h, long i);
658
659satQueue_t* sat_queue_init(long maxElements);
660void sat_queue_clear(satQueue_t *Q);
661void sat_queue_free(satQueue_t *Q);
662void sat_queue_insert(satQueue_t *Q, long n);
663long sat_queue_pop(satQueue_t *Q);
664void sat_queue_print(satQueue_t *Q);
665void vel_heap_remove_var_eliminated(satManager_t *m);
666void vel_heap_up(satManager_t *m, long i);
667void vel_heap_down(satManager_t *m, long i);
668long vel_heap_remove_min(satManager_t *m);
669void vel_heap_clear(satManager_t *m);
670void vel_heap_update(satManager_t *m, long n);
671void vel_heap_init(satManager_t *m, long size);
672void vel_heap_print(satManager_t *m);
673void vel_heap_free(satManager_t *m);
674int vel_heap_check(satManager_t *m, long i);
675int vel_heap_inHeap(satManager_t *m, long n);
676void vel_heap_insert(satManager_t *m, long n);
677
678satStack_t* sat_stack_init(long maxElements);
679void sat_stack_clear(satStack_t *stack);
680void sat_stack_free(satStack_t *stack);
681satStack_t* sat_stack_push(satStack_t *stack, long n);
682long sat_stack_pop(satStack_t *stack);
683void sat_stack_print(satStack_t *stack);
684satSCC_t * sat_scc_alloc(long size);
685long sat_find_repr(satManager_t *m, long lit);
686void sat_update_repr(satManager_t *m, long litp, long litq);
687void sat_strongly_connected_component(satManager_t *m);
688
689
Note: See TracBrowser for help on using the repository browser.