cadical基本数据结构分析2

1. 文字、变元

变元和文字iteration:
vars, lits

vals:
signed char * vals; // assignment [-max_var,max_var] //Internal数据成员，保存文字的赋值-同时其对应负文字的赋值也一并保存（更新）。
// 可以理解为vals中由两个对应位置保存有变元的真值（1或-1），通常只需要查询一个即可（另一个取值相反）。
// 查询文字的值使用函数 int tmp = val (lit)；传播队列中查询得到的tmp一定>0。
// 没有参与传播的变元对应两个位置取值为0；可以据此判断文字是否在传播队列中。
lit:
当前文字。cadical中变元从1开始编号，正负文字在求解器中与现实中一致，分别用正负数字表示；

clauses:
子句集合（元素为Clause*）。子句中文字literals同样与现实中表示是一致的，正负数字组成，并在internal中不再以0结尾。

vidx(lit) :
函数vidx(int)返回文字lit对应的绝对值idx

Var：
变元类型Var定义的对象包含了传播信息
//见文件var.hpp有类型Var的定义
Var & v = var (idx); //通过文字绝对值构造变元
v.level = level; //变元对应的层属性
v.trail = (int) trail.size (); //变元对应在Trail中的位置索引
v.reason = 0 / decision_reason / c; //变元进入Trai中时的reason子句

2. 文字、变元所对应的相关数据

//2.1

涉及变元对应的量会采用vidx(lit)作为索引；

 1 // Helper functions to access variable and literal data.
 2   //
 3   Var &var (int lit) { return vtab[vidx (lit)]; }
 4   Link &link (int lit) { return links[vidx (lit)]; }
 5   Flags &flags (int lit) { return ftab[vidx (lit)]; }
 6   int64_t &bumped (int lit) { return btab[vidx (lit)]; }
 7   double &score (int lit) { return stab[vidx (lit)]; }
 9 
10   const Flags &flags (int lit) const { return ftab[vidx (lit)]; }

//internal.hpp

//函数vidx(lit)对lit求绝对值，其结果作为索引

//=========================================

vector<Var> vtab; // variable table [1,max_var]

vector<Flags> ftab; // variable and literal flags

vector<int64_t> btab; // enqueue time stamps for queue

vector<int64_t> vgapctab; // gap length to conflict point

vector<int64_t> gtab; // time stamp table to recompute glue

ScoreSchedule scores; // score based decision priority queue
vector<double> stab; // table of variable scores [1,max_var]

//2.2 

涉及文字对应的量会将自然表示的文字转换为采用Unsigned LSB方式，转换后的文字方式做索引

 1   int &propfixed (int lit) { return ptab[vlit (lit)]; }
 2 
 3   double &score (int lit) { return stab[vidx (lit)]; } 
 4 
 5   Bins &bins (int lit) { return big[vlit (lit)]; }
 6 
 7   Occs &occs (int lit) { return otab[vlit (lit)]; }
 8 
 9   int64_t &noccs (int lit) { return ntab[vlit (lit)]; }
10 
11   Watches &watches (int lit) { return wtab[vlit (lit)]; }
12 
13 
14   bool occurring () const { return !otab.empty (); }
15   bool watching () const { return !wtab.empty (); }

//internal.hpp 

//使用vlit(lit)将lit映射为Unsigned LSB表示的方式，其结果作为索引

//=========================================

vector<Bins> big; // binary implication graph   // 在bin.hpp中有申明 typedef vector<Bin> Bins; 此处big为向量的向量

vector<Occs> otab; // table of occurrences for all literals

vector<int64_t> ntab; // number of one-sided occurrences table

vector<Watches> wtab; // table of watches for all literals

vector<int> ptab; // table for caching probing attempts

//----------------------------------------------------------------------------------------------------------------------------------------------------------

介绍以下Unsigned LSB文字表示方式：

 1   // Unsigned version with LSB denoting sign.  This is used in indexing
 2   // arrays by literals.  The idea is to keep the elements in such an array
 3   // for both the positive and negated version of a literal close together.
 4   //
 5   unsigned vlit (int lit) { return (lit < 0) + 2u * (unsigned) vidx (lit); }
 6 
 7   int u2i (unsigned u) {
 8     assert (u > 1);
 9     int res = u / 2;
10     assert (res <= max_var);
11     if (u & 1)
12       res = -res;
13     return res;
14   }  //only used in block.cpp 

 3. 关于蕴含图类型bin定义解读

//数据成员big出现的地方

---------- D:\SAT_study2024\snap-SAT\cadical-rel-1.9.4-scavel-01\src\assume.cpp
[18] const unsigned char bit = bign (lit);
[177] const unsigned bit = bign (failed);
[212] const unsigned bit = bign (-failed);
[240] assert (f.failed & bign (first_failed));
[310] const unsigned bit = bign (lit);
[335] const unsigned bit = bign (-lit);
[356] const unsigned bit = bign (-ign);
[467] const unsigned bit = bign (lit);
[511] const unsigned char bit = bign (lit);

---------- D:\SAT_study2024\snap-SAT\cadical-rel-1.9.4-scavel-01\src\bins.cpp
[10] assert (big.empty ());
[11] if (big.size () < 2 * vsize)
[12] big.resize (2 * vsize, Bins ());
[17] assert (!big.empty ());
[18] erase_vector (big);

---------- D:\SAT_study2024\snap-SAT\cadical-rel-1.9.4-scavel-01\src\compact.cpp
[449] if (!big.empty ())
[450] mapper.map2_vector (big);

---------- D:\SAT_study2024\snap-SAT\cadical-rel-1.9.4-scavel-01\src\elim.cpp
[522] LOG ("resolvent size %d too big after %" PRId64

---------- D:\SAT_study2024\snap-SAT\cadical-rel-1.9.4-scavel-01\src\internal.hpp
[222] vector<Bins> big; // binary implication graph
[407] Bins &bins (int lit) { return big[vlit (lit)]; }
[501] unsigned bit = bign (lit);
[505] marks[vidx (lit)] |= bign (lit);
[909] const unsigned bit = bign (lit);
[926] const unsigned bit = bign (lit);
[931] const unsigned bit = bign (lit);
[940] const unsigned bit = bign (lit);
[948] const unsigned bit = bign (lit);
[956] const unsigned bit = bign (lit);
[964] const unsigned bit = bign (lit);
[969] const unsigned bit = bign (lit);
[1123] const unsigned bit = bign (lit);

---------- D:\SAT_study2024\snap-SAT\cadical-rel-1.9.4-scavel-01\src\mobical.cpp
[40] " --big generate big formulas only\n"
[4007] else if (!strcmp (argv[i], "--big"))

---------- D:\SAT_study2024\snap-SAT\cadical-rel-1.9.4-scavel-01\src\util.hpp
[19] inline unsigned bign (int lit) { return 1 + (lit < 0); }

//bins.hpp

 1 #ifndef _bins_hpp_INCLUDED
 2 #define _bins_hpp_INCLUDED
 3 
 4 #include "util.hpp" // Alphabetically after 'bins'.
 5 
 6 namespace CaDiCaL {
 7 
 8 using namespace std;
 9 
10 struct Bin {
11   int lit;
12   uint64_t id;
13 };
14 
15 typedef vector<Bin> Bins;
16 
17 inline void shrink_bins (Bins &bs) { shrink_vector (bs); }
18 inline void erase_bins (Bins &bs) { erase_vector (bs); }
19 
20 } // namespace CaDiCaL
21 
22 #endif

//bins.cpp

 1 #include "internal.hpp"
 2 
 3 namespace CaDiCaL {
 4 
 5 /*------------------------------------------------------------------------*/
 6 
 7 // Binary implication graph lists.
 8 
 9 void Internal::init_bins () {
10   assert (big.empty ());
11   if (big.size () < 2 * vsize)
12     big.resize (2 * vsize, Bins ());
13   LOG ("initialized binary implication graph");
14 }
15 
16 void Internal::reset_bins () {
17   assert (!big.empty ());
18   erase_vector (big);
19   LOG ("reset binary implication graph");
20 }
21 
22 } // namespace CaDiCaL