1 /*  Boolector: Satisfiability Modulo Theories (SMT) solver.
2  *
3  *  Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4  *
5  *  This file is part of Boolector.
6  *  See COPYING for more information on using this software.
7  */
8 
9 #ifndef BTORSLVSLS_H_INCLUDED
10 #define BTORSLVSLS_H_INCLUDED
11 
12 #include "utils/btornodemap.h"
13 #ifndef NDEBUG
14 #include "btorbv.h"
15 #endif
16 
17 #include "btorslv.h"
18 #include "utils/btorhashint.h"
19 #include "utils/btorstack.h"
20 
21 enum BtorSLSMoveKind
22 {
23   BTOR_SLS_MOVE_FLIP = 0,
24   BTOR_SLS_MOVE_INC,
25   BTOR_SLS_MOVE_DEC,
26   BTOR_SLS_MOVE_NOT,
27   BTOR_SLS_MOVE_FLIP_RANGE,
28   BTOR_SLS_MOVE_FLIP_SEGMENT,
29   BTOR_SLS_MOVE_DONE,
30   BTOR_SLS_MOVE_RAND,
31   BTOR_SLS_MOVE_RAND_WALK,
32   BTOR_SLS_MOVE_PROP,
33 };
34 typedef enum BtorSLSMoveKind BtorSLSMoveKind;
35 
36 struct BtorSLSMove
37 {
38   BtorIntHashTable *cans;
39   double sc;
40 };
41 typedef struct BtorSLSMove BtorSLSMove;
42 
43 struct BtorSLSConstrData
44 {
45   int64_t weight;
46   int64_t selected;
47 };
48 typedef struct BtorSLSConstrData BtorSLSConstrData;
49 
50 BTOR_DECLARE_STACK (BtorSLSMovePtr, BtorSLSMove *);
51 
52 /*------------------------------------------------------------------------*/
53 
54 #define BTOR_SLS_SOLVER(btor) ((BtorSLSSolver *) (btor)->slv)
55 
56 struct BtorSLSSolver
57 {
58   BTOR_SOLVER_STRUCT;
59 
60   BtorIntHashTable *roots;   /* must be map (for common local search funs)
61                                 but does not maintain anything */
62   BtorIntHashTable *weights; /* also maintains assertion weights */
63   BtorIntHashTable *score;   /* sls score */
64 
65   uint32_t nflips; /* limit, disabled if 0 */
66   bool terminate;
67 
68   BtorSLSMovePtrStack moves; /* record moves for prob rand walk */
69   uint32_t npropmoves;       /* record #no moves for prop moves */
70   uint32_t nslsmoves;        /* record #no moves for sls moves */
71   double sum_score;          /* record sum of all scores for prob rand walk */
72 
73   /* prop moves only */
74   uint32_t prop_flip_cond_const_prob;
75   int32_t prop_flip_cond_const_prob_delta;
76   uint32_t prop_nflip_cond_const;
77 
78   /* the following maintain data for the next move (i.e. either the move
79    * with the maximum score of all tried moves, or a random walk, or a
80    * randomized move). */
81   BtorIntHashTable *max_cans; /* list of (can, neigh) */
82   double max_score;
83   BtorSLSMoveKind max_move; /* move kind (for stats) */
84   int32_t max_gw;           /* is groupwise move? (for stats) */
85 
86   /* statistics */
87   struct
88   {
89     uint32_t restarts;
90     uint32_t moves;
91     uint32_t flips;
92     uint32_t props;
93     uint32_t move_flip;
94     uint32_t move_inc;
95     uint32_t move_dec;
96     uint32_t move_not;
97     uint32_t move_range;
98     uint32_t move_seg;
99     uint32_t move_rand;
100     uint32_t move_rand_walk;
101     uint32_t move_prop;
102     uint32_t move_prop_rec_conf;
103     uint32_t move_prop_non_rec_conf;
104     uint32_t move_gw_flip;
105     uint32_t move_gw_inc;
106     uint32_t move_gw_dec;
107     uint32_t move_gw_not;
108     uint32_t move_gw_range;
109     uint32_t move_gw_seg;
110     uint32_t move_gw_rand;
111     uint32_t move_gw_rand_walk;
112     uint64_t updates;
113   } stats;
114 
115   struct
116   {
117     double update_cone;
118     double update_cone_reset;
119     double update_cone_model_gen;
120     double update_cone_compute_score;
121   } time;
122 };
123 
124 typedef struct BtorSLSSolver BtorSLSSolver;
125 
126 BtorSolver *btor_new_sls_solver (Btor *btor);
127 
128 #endif
129