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