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 BTORSAT_H_INCLUDED 10 #define BTORSAT_H_INCLUDED 11 12 #include <stdbool.h> 13 #include <stdio.h> 14 15 #include "btortypes.h" 16 #include "utils/btormem.h" 17 #include "utils/btorstack.h" 18 19 /*------------------------------------------------------------------------*/ 20 21 typedef struct BtorSATMgr BtorSATMgr; 22 23 struct BtorSATMgr 24 { 25 /* Note: direct solver reference for PicoSAT, wrapper object for for 26 * Lingeling (BtorLGL) and MiniSAT (BtorMiniSAT). */ 27 void *solver; 28 Btor *btor; 29 30 const char *name; /* solver name */ 31 32 /* Note: do not change order! (btor_sat_mgr_clone relies on inc_required 33 * to come first of all fields following below.) */ 34 bool inc_required; 35 #ifdef BTOR_USE_LINGELING 36 bool fork; 37 #endif 38 FILE *output; 39 40 bool initialized; 41 int32_t satcalls; 42 int32_t clauses; 43 int32_t true_lit; 44 int32_t maxvar; 45 46 double sat_time; 47 48 struct 49 { 50 int32_t (*fun) (void *); /* termination callback */ 51 void *state; 52 } term; 53 54 bool have_restore; 55 struct 56 { 57 void (*add) (BtorSATMgr *, int32_t); /* required */ 58 void (*assume) (BtorSATMgr *, int32_t); 59 int32_t (*deref) (BtorSATMgr *, int32_t); /* required */ 60 void (*enable_verbosity) (BtorSATMgr *, int32_t); 61 int32_t (*failed) (BtorSATMgr *, int32_t); 62 int32_t (*fixed) (BtorSATMgr *, int32_t); 63 int32_t (*inc_max_var) (BtorSATMgr *); 64 void *(*init) (BtorSATMgr *); /* required */ 65 void (*melt) (BtorSATMgr *, int32_t); 66 int32_t (*repr) (BtorSATMgr *, int32_t); 67 void (*reset) (BtorSATMgr *); /* required */ 68 int32_t (*sat) (BtorSATMgr *, int32_t); /* required */ 69 void (*set_output) (BtorSATMgr *, FILE *); 70 void (*set_prefix) (BtorSATMgr *, const char *); 71 void (*stats) (BtorSATMgr *); 72 void *(*clone) (Btor *btor, BtorSATMgr *); 73 void (*setterm) (BtorSATMgr *); 74 } api; 75 }; 76 77 /*------------------------------------------------------------------------*/ 78 79 struct BtorCnfPrinter 80 { 81 FILE *out; 82 BtorIntStack clauses; 83 BtorIntStack assumptions; 84 BtorSATMgr *smgr; /* SAT manager wrapped by DIMACS printer. */ 85 }; 86 87 typedef struct BtorCnfPrinter BtorCnfPrinter; 88 89 /*------------------------------------------------------------------------*/ 90 91 /* Creates new SAT manager. 92 * A SAT manager is used by nearly all functions of the SAT layer. 93 */ 94 BtorSATMgr *btor_sat_mgr_new (Btor *btor); 95 96 bool btor_sat_mgr_has_clone_support (const BtorSATMgr *smgr); 97 98 bool btor_sat_mgr_has_incremental_support (const BtorSATMgr *smgr); 99 100 void btor_sat_mgr_set_term (BtorSATMgr *smgr, 101 int32_t (*fun) (void *), 102 void *state); 103 104 /* Clones existing SAT manager (and underlying SAT solver). */ 105 BtorSATMgr *btor_sat_mgr_clone (Btor *btor, BtorSATMgr *smgr); 106 107 /* Deletes SAT manager from memory. */ 108 void btor_sat_mgr_delete (BtorSATMgr *smgr); 109 110 /* Generates fresh CNF indices. 111 * Indices are generated in consecutive order. */ 112 int32_t btor_sat_mgr_next_cnf_id (BtorSATMgr *smgr); 113 114 /* Mark old CNF index as not used anymore. */ 115 void btor_sat_mgr_release_cnf_id (BtorSATMgr *smgr, int32_t); 116 117 #if 0 118 /* Returns the last CNF index that has been generated. */ 119 int32_t btor_get_last_cnf_id_sat_mgr (BtorSATMgr * smgr); 120 #endif 121 122 void btor_sat_enable_solver (BtorSATMgr *smgr); 123 124 /* Inits the SAT solver. */ 125 void btor_sat_init (BtorSATMgr *smgr); 126 127 /* Returns if the SAT solver has already been initialized */ 128 bool btor_sat_is_initialized (BtorSATMgr *smgr); 129 130 /* Sets the output file of the SAT solver. */ 131 void btor_sat_set_output (BtorSATMgr *smgr, FILE *output); 132 133 /* Prints statistics of SAT solver. */ 134 void btor_sat_print_stats (BtorSATMgr *smgr); 135 136 /* Adds literal to the current clause of the SAT solver. 137 * 0 terminates the current clause. 138 */ 139 void btor_sat_add (BtorSATMgr *smgr, int32_t lit); 140 141 /* Adds assumption to SAT solver. 142 * Requires that SAT solver supports this. 143 */ 144 void btor_sat_assume (BtorSATMgr *smgr, int32_t lit); 145 146 /* Checks whether an assumption failed during 147 * the last SAT solver call 'btor_sat_check_sat'. 148 */ 149 int32_t btor_sat_failed (BtorSATMgr *smgr, int32_t lit); 150 151 /* Solves the SAT instance. 152 * limit < 0 -> no limit. 153 */ 154 BtorSolverResult btor_sat_check_sat (BtorSATMgr *smgr, int32_t limit); 155 156 /* Gets assignment of a literal (in the SAT case). 157 * Do not call before calling btor_sat_check_sat. 158 */ 159 int32_t btor_sat_deref (BtorSATMgr *smgr, int32_t lit); 160 161 /* Gets equivalence class represenative of a literal 162 * or the literal itself if it is in a singleton 163 * equivalence, fixed or eliminated. 164 * Do not call before calling btor_sat_check_sat. 165 */ 166 int32_t btor_sat_repr (BtorSATMgr *smgr, int32_t lit); 167 168 /* Gets assignment of a literal (in the SAT case) 169 * similar to 'deref', but only consider top level. 170 * Do not call before calling btor_sat_check_sat. 171 */ 172 int32_t btor_sat_fixed (BtorSATMgr *smgr, int32_t lit); 173 174 /* Resets the status of the SAT solver. */ 175 void btor_sat_reset (BtorSATMgr *smgr); 176 177 #endif 178