kissat的多输出-学习与修改2

 1 #include "arena.h"  //包含#include "reference.h"  #include "stack.h"  #include "utilities.h"
 2 #include "array.h"
 3 #include "assign.h" //包含 #include "reference.h"
 4 #include "averages.h"
 5 #include "check.h"
 6 #include "classify.h"
 7 #include "clause.h"
 8 #include "cover.h"
 9 #include "extend.h"
10 #include "flags.h"
11 #include "format.h"
12 #include "frames.h"
13 #include "heap.h"
14 #include "kimits.h"
15 #include "kissat.h"
16 #include "literal.h"
17 #include "mode.h"
18 #include "options.h"
19 #include "phases.h"
20 #include "profile.h"
21 #include "proof.h"
22 #include "queue.h"
23 #include "random.h"
24 #include "reluctant.h"
25 #include "rephase.h"
26 #include "smooth.h"
27 #include "stack.h"
28 #include "statistics.h"
29 #include "value.h"
30 #include "vector.h"
31 #include "watch.h"
32 
33 typedef struct datarank datarank;
34 
35 struct datarank {
36   unsigned data;
37   unsigned rank;
38 };
39 
40 typedef struct import import;
41 
42 struct import {
43   unsigned lit;
44   bool extension;
45   bool imported;
46   bool eliminated;
47 };
48 
49 typedef struct termination termination;
50 
51 struct termination {
52 #ifdef COVERAGE
53   volatile uint64_t flagged;
54 #else
55   volatile bool flagged;
56 #endif
57   volatile void *state;
58   int (*volatile terminate) (void *);
59 };
60 
61 // clang-format off
62 
63 typedef STACK (value) eliminated;
64 typedef STACK (import) imports;
65 typedef STACK (datarank) dataranks;
66 typedef STACK (watch) statches;
67 typedef STACK (watch *) patches;
68 
69 // clang-format on
70 
71 struct kitten;

  1 struct kissat {
  2 #if !defined(NDEBUG) || defined(METRICS)
  3   bool backbone_computing;
  4 #endif
  5 #ifdef LOGGING
  6   bool compacting;
  7 #endif
  8   bool extended;
  9   bool inconsistent;
 10   bool iterating;
 11   bool preprocessing;
 12   bool probing;
 13 #ifndef QUIET
 14   bool sectioned;
 15 #endif
 16   bool stable;
 17 #if !defined(NDEBUG) || defined(METRICS)
 18   bool transitive_reducing;
 19   bool vivifying;
 20 #endif
 21   bool warming;
 22   bool watching;
 23 
 24   bool large_clauses_watched_after_binary_clauses;  //最长名称的布尔型数据成员
 25 
 26   termination termination;
 27 
 28   unsigned vars;
 29   unsigned size;
 30   unsigned active;
 31   unsigned randec;
 32 
 33   ints export;
 34   ints units;
 35   imports import;
 36   extensions extend;
 37   unsigneds witness;
 38 
 39   assigned *assigned;
 40   flags *flags;
 41 
 42   mark *marks;
 43 
 44   value *values;
 45   phases phases;
 46 
 47   eliminated eliminated;
 48   unsigneds etrail;
 49 
 50   links *links;
 51   queue queue;
 52 
 53   heap scores;
 54   double scinc;
 55 
 56   heap schedule;
 57   double scoreshift;
 58 
 59   unsigned level;
 60   frames frames;
 61 
 62   unsigned_array trail;
 63   unsigned *propagate;
 64 
 65   unsigned best_assigned;
 66   unsigned target_assigned;
 67   unsigned unflushed;
 68   unsigned unassigned;
 69 
 70   unsigneds delayed;
 71 
 72 #if defined(LOGGING) || !defined(NDEBUG)
 73   unsigneds resolvent;
 74 #endif
 75   unsigned resolvent_size;
 76   unsigned antecedent_size;
 77 
 78   dataranks ranks;
 79 
 80   unsigneds analyzed;
 81   unsigneds levels;
 82   unsigneds minimize;
 83   unsigneds poisoned;
 84   unsigneds promote;
 85   unsigneds removable;
 86   unsigneds shrinkable;
 87 
 88   clause conflict;
 89 
 90   bool clause_satisfied;
 91   bool clause_shrink;
 92   bool clause_trivial;
 93 
 94   unsigneds clause;
 95   unsigneds shadow;
 96 
 97   arena arena;
 98   vectors vectors;
 99   reference first_reducible;
100   reference last_irredundant;
101   watches *watches;
102 
103   reference last_learned[4];
104 
105   sizes sorter;
106 
107   generator random;
108   averages averages[2];
109   unsigned tier1[2], tier2[2];
110   reluctant reluctant;
111 
112   bounds bounds;
113   classification classification;
114   delays delays;
115   enabled enabled;
116   limited limited;
117   limits limits;
118   remember last;
119   unsigned walked;
120 
121   mode mode;
122 
123   uint64_t ticks;
124 
125   format format;
126 
127   statches antecedents[2];
128   statches gates[2];
129   patches xorted[2];
130   unsigneds resolvents;
131   bool resolve_gate;
132 
133   struct kitten *kitten;
134 #ifdef METRICS
135   uint64_t *gate_eliminated;
136 #else
137   bool gate_eliminated;
138 #endif
139   bool sweep_incomplete;
140   unsigneds sweep_schedule;
141 
142 #if !defined(NDEBUG) || !defined(NPROOFS)
143   unsigneds added;
144   unsigneds removed;
145 #endif
146 
147 #if !defined(NDEBUG) || !defined(NPROOFS) || defined(LOGGING)
148   ints original;
149   size_t offset_of_last_original_clause;
150 #endif
151 
152 #ifndef QUIET
153   profiles profiles;
154 #endif
155 
156 #ifndef NOPTIONS
157   options options;
158 #endif
159 
160 #ifndef NDEBUG
161   checker *checker;
162 #endif
163 
164 #ifndef NPROOFS
165   proof *proof;
166 #endif
167 
168   statistics statistics;
169 };

注意区别： 类型unsigned、类型unsigneds 以及数据成员unsigned unassigned;

                   类型assigned；有没有assigneds？ 以及数据成员 assigned *assigned;

另： ints；

在文件reference.h中：

                  typedef unsigned reference;

                  typedef STACK (reference) references;

在文件stack.h中

                 typedef STACK (char) chars;
                 typedef STACK (int) ints;
                 typedef STACK (size_t) sizes;
                  typedef STACK (unsigned) unsigneds;

#define VARS (solver->vars)
#define LITS (2 * solver->vars)

#if 0
#define TIEDX (GET_OPTION (focusedtiers) ? 0 : solver->stable)
#define TIER1 (solver->tier1[TIEDX])
#define TIER2 (solver->tier2[TIEDX])
#else
#define TIER1 (solver->tier1[0])
#define TIER2 (solver->tier2[1])
#endif

#define SCORES (&solver->scores)

//internal.hpp
1 static inline unsigned kissat_assigned (kissat *solver) {
2   assert (VARS >= solver->unassigned);
3   return VARS - solver->unassigned;
4 }

//区别于没有ed的传播赋值函数函数 kissat_assign (kissat *solver);

 //inlineassign.h
 1 #ifdef FAST_ASSIGN
 2 #define kissat_assign kissat_fast_assign
 3 #endif
 4 
 5 static inline void kissat_assign (kissat *solver, const bool probing,
 6                                   const unsigned level,
 7 #ifdef FAST_ASSIGN
 8                                   value *values, assigned *assigned,
 9 #endif
10                                   bool binary, unsigned lit,
11                                   unsigned reason)  
12 {
13      ......
14 }  //这个函数至少有6各输出参数