kissat分析01_基本数据结构03_frame_trail

 1 #define INVALID_TRAIL UINT_MAX
 2 
 3 struct frame
 4 {
 5   unsigned decision;
 6   unsigned trail:LD_MAX_TRAIL;
 7   unsigned used:2;
 8   bool promote:1;
 9 };
10 
11 // *INDENT-OFF*
12 
13 typedef STACK (frame) frames;
14 
15 // *INDENT-ON*
16 
17 struct kissat;
18 
19 void kissat_push_frame (struct kissat *, unsigned decision);
20 
21 #define FRAME(LEVEL) \
22   (PEEK_STACK (solver->frames, (LEVEL)))
23 
24 #endif

#include "allocate.h"
#include "internal.h"

void
kissat_push_frame (kissat * solver, unsigned decision)
{
  const size_t trail = SIZE_STACK (solver->trail);
  assert (trail <= MAX_TRAIL);
  frame frame;
  frame.decision = decision;
  frame.trail = trail;
  frame.promote = false;
  frame.used = 0;
  PUSH_STACK (solver->frames, frame);
}

 1 ----------  D:\studySAT\studySAT2023_04_28\Kissat_MAB-HyWalk_hornFrist\src\decide.c
 2 [138]   kissat_push_frame (solver, lit);
 3 [152]   kissat_push_frame (solver, lit);
 4 
 5 ----------  D:\studySAT\studySAT2023_04_28\Kissat_MAB-HyWalk_hornFrist\src\frames.c
 6 [5] kissat_push_frame (kissat * solver, unsigned decision)
 7 
 8 ----------  D:\studySAT\studySAT2023_04_28\Kissat_MAB-HyWalk_hornFrist\src\frames.h
 9 [31] void kissat_push_frame (struct kissat *, unsigned decision);
10 
11 ----------  D:\studySAT\studySAT2023_04_28\Kissat_MAB-HyWalk_hornFrist\src\internal.c
12 [33]   kissat_push_frame (solver, INVALID_LIT);