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 BTORCORE_H_INCLUDED 10 #define BTORCORE_H_INCLUDED 11 12 #include "btorass.h" 13 #include "btormsg.h" 14 #include "btornode.h" 15 #include "btoropt.h" 16 #include "btorrwcache.h" 17 #include "btorsat.h" 18 #include "btorslv.h" 19 #include "btorsort.h" 20 #include "btortypes.h" 21 #include "utils/btorhashint.h" 22 #include "utils/btormem.h" 23 #include "utils/btorrng.h" 24 25 #include <stdbool.h> 26 27 /*------------------------------------------------------------------------*/ 28 29 #ifndef BTOR_USE_LINGELING 30 #define BTOR_DO_NOT_PROCESS_SKELETON 31 #endif 32 33 // Currently, 'BoolectorNode' (external) vs. 'BtorNode' (internal) 34 // syntactically hides internal nodes. Hence, we assume that both structs 35 // 'BoolectorNode' and 'BtorNode' have/ the same structure and provide the 36 // following macros for type conversion (via typecasting). We further assume 37 // that external 'boolector_xxx' functions provide the same functionality as 38 // their internal counter part 'btor_xxx' (except for API tracing and contract 39 // checks). 40 // 41 // If the assumption above does not hold, we have to provide 42 // real containers for 'BoolectorNode' (cf. 'BoolectorNodeMap'). 43 44 #define BTOR_IMPORT_BOOLECTOR_NODE(node) (((BtorNode *) (node))) 45 #define BTOR_IMPORT_BOOLECTOR_NODE_ARRAY(array) (((BtorNode **) (array))) 46 #define BTOR_EXPORT_BOOLECTOR_NODE(node) (((BoolectorNode *) (node))) 47 #define BTOR_IMPORT_BOOLECTOR_SORT(sort) (((BtorSortId) (long) (sort))) 48 #define BTOR_EXPORT_BOOLECTOR_SORT(sort) (((BoolectorSort) (long) (sort))) 49 50 /*------------------------------------------------------------------------*/ 51 52 struct BtorNodeUniqueTable 53 { 54 uint32_t size; 55 uint32_t num_elements; 56 BtorNode **chains; 57 }; 58 59 typedef struct BtorNodeUniqueTable BtorNodeUniqueTable; 60 61 struct BtorCallbacks 62 { 63 struct 64 { 65 /* the function to use for (checking) termination 66 * (we need to distinguish between callbacks from C and Python) */ 67 int32_t (*termfun) (void *); 68 69 void *fun; /* termination callback function */ 70 void *state; /* termination callback function arguments */ 71 int32_t done; 72 } term; 73 }; 74 75 typedef struct BtorCallbacks BtorCallbacks; 76 77 struct BtorConstraintStats 78 { 79 uint32_t varsubst; 80 uint32_t embedded; 81 uint32_t unsynthesized; 82 uint32_t synthesized; 83 }; 84 85 typedef struct BtorConstraintStats BtorConstraintStats; 86 87 struct Btor 88 { 89 BtorMemMgr *mm; 90 BtorSolver *slv; 91 BtorCallbacks cbs; 92 93 BtorBVAssList *bv_assignments; 94 BtorFunAssList *fun_assignments; 95 96 BtorNodePtrStack nodes_id_table; 97 BtorNodeUniqueTable nodes_unique_table; 98 BtorSortUniqueTable sorts_unique_table; 99 100 BtorAIGVecMgr *avmgr; 101 102 BtorPtrHashTable *symbols; 103 BtorPtrHashTable *node2symbol; 104 105 BtorPtrHashTable *inputs; 106 BtorPtrHashTable *bv_vars; 107 BtorPtrHashTable *ufs; 108 BtorPtrHashTable *lambdas; 109 BtorPtrHashTable *quantifiers; 110 BtorPtrHashTable *exists_vars; 111 BtorPtrHashTable *forall_vars; 112 BtorPtrHashTable *feqs; 113 BtorPtrHashTable *parameterized; 114 115 BtorPtrHashTable *substitutions; 116 117 BtorNode *true_exp; 118 119 BtorIntHashTable *bv_model; 120 BtorIntHashTable *fun_model; 121 BtorNodePtrStack functions_with_model; 122 BtorNodePtrStack outputs; /* used to synthesize BTOR2 outputs */ 123 124 uint32_t rec_rw_calls; /* calls for recursive rewriting */ 125 uint32_t valid_assignments; 126 BtorRwCache *rw_cache; 127 128 int32_t vis_idx; /* file index for visualizing expressions */ 129 130 bool inconsistent; 131 bool found_constraint_false; 132 133 uint32_t external_refs; /* external references (library mode) */ 134 uint32_t btor_sat_btor_called; /* how often is btor_check_sat been called */ 135 BtorSolverResult last_sat_result; /* status of last SAT call (SAT/UNSAT) */ 136 137 BtorPtrHashTable *varsubst_constraints; 138 BtorPtrHashTable *embedded_constraints; 139 BtorPtrHashTable *unsynthesized_constraints; 140 BtorPtrHashTable *synthesized_constraints; 141 142 /* maintains simplified assumptions, these are the assumptions that are 143 * actually bit-blasted and assumed to the SAT solver */ 144 BtorPtrHashTable *assumptions; 145 /* maintains the non-simplified (original) assumptions */ 146 BtorPtrHashTable *orig_assumptions; 147 /* maintains non-simplified assumptions as assumed via boolector_assume, 148 * this stack is needed for boolector_get_failed_assumptions only */ 149 BtorNodePtrStack failed_assumptions; 150 151 /* maintain assertions for different contexts push/pop */ 152 BtorNodePtrStack assertions; 153 /* caches the assertions on stack 'assertions' */ 154 BtorIntHashTable *assertions_cache; 155 /* saves the number of assertions on each push */ 156 BtorUIntStack assertions_trail; 157 /* Number of push/pop calls (used for unique symbol prefixes) */ 158 uint32_t num_push_pop; 159 160 #ifndef NDEBUG 161 Btor *clone; /* shadow clone (debugging only) */ 162 #endif 163 164 char *parse_error_msg; 165 166 FILE *apitrace; 167 int8_t close_apitrace; 168 169 BtorOpt *options; 170 BtorPtrHashTable *str2opt; 171 172 BtorMsg *msg; 173 BtorRNG rng; 174 175 struct 176 { 177 uint32_t cur, max; 178 } ops[BTOR_NUM_OPS_NODE]; 179 180 struct 181 { 182 uint32_t max_rec_rw_calls; /* maximum number of recursive rewrite calls */ 183 uint32_t var_substitutions; /* number substituted vars */ 184 uint32_t uf_substitutions; /* num substituted uninterpreted functions */ 185 uint32_t ec_substitutions; /* embedded constraint substitutions */ 186 uint32_t linear_equations; /* number of linear equations */ 187 uint32_t gaussian_eliminations; /* number of gaussian eliminations */ 188 uint32_t eliminated_slices; /* number of eliminated slices */ 189 uint32_t skeleton_constraints; /* number of skeleton constraints */ 190 uint32_t adds_normalized; /* number of add chains normalizations */ 191 uint32_t ands_normalized; /* number of and chains normalizations */ 192 uint32_t muls_normalized; /* number of mul chains normalizations */ 193 uint32_t ackermann_constraints; 194 uint_least64_t prop_apply_lambda; /* number of static props over lambdas */ 195 uint_least64_t prop_apply_update; /* number of static props over updates */ 196 uint32_t bv_uc_props; 197 uint32_t fun_uc_props; 198 uint32_t param_uc_props; 199 uint_least64_t lambdas_merged; 200 BtorConstraintStats constraints; 201 BtorConstraintStats oldconstraints; 202 uint_least64_t expressions; 203 uint_least64_t clone_calls; 204 size_t node_bytes_alloc; 205 uint_least64_t beta_reduce_calls; 206 uint_least64_t betap_reduce_calls; 207 #ifndef NDEBUG 208 BtorPtrHashTable *rw_rules_applied; 209 #endif 210 uint_least64_t rewrite_synth; 211 } stats; 212 213 struct 214 { 215 double sat; 216 double simplify; 217 double subst; 218 double subst_rebuild; 219 double elimapplies; 220 double embedded; 221 double slicing; 222 double skel; 223 double propagate; 224 double beta; 225 double betap; 226 double failed; 227 double cloning; 228 double synth_exp; 229 double model_gen; 230 double ucopt; 231 double merge; 232 double extract; 233 double ack; 234 double rewrite; 235 double occurrence; 236 } time; 237 }; 238 239 /* Creates new boolector instance. */ 240 Btor *btor_new (void); 241 242 /* Deletes boolector. */ 243 void btor_delete (Btor *btor); 244 245 /* Gets version. */ 246 const char *btor_version (const Btor *btor); 247 248 /* Gets id. */ 249 const char *btor_git_id (const Btor *btor); 250 251 /* Set termination callback. */ 252 void btor_set_term (Btor *btor, int32_t (*fun) (void *), void *state); 253 254 /* Determine if boolector has been terminated via termination callback. */ 255 int32_t btor_terminate (Btor *btor); 256 257 /* Set verbosity message prefix. */ 258 void btor_set_msg_prefix (Btor *btor, const char *prefix); 259 260 /* Prints statistics. */ 261 void btor_print_stats (Btor *btor); 262 263 /* Reset time statistics. */ 264 void btor_reset_time (Btor *btor); 265 266 /* Reset other statistics. */ 267 void btor_reset_stats (Btor *btor); 268 269 /* Adds top level constraint. */ 270 void btor_assert_exp (Btor *btor, BtorNode *exp); 271 272 /* Adds assumption. */ 273 void btor_assume_exp (Btor *btor, BtorNode *exp); 274 275 /* Determines if expression has been previously assumed. */ 276 bool btor_is_assumption_exp (Btor *btor, BtorNode *exp); 277 278 /* Determines if assumption is a failed assumption. */ 279 bool btor_failed_exp (Btor *btor, BtorNode *exp); 280 281 /* Adds assumptions as assertions and resets the assumptions. */ 282 void btor_fixate_assumptions (Btor *btor); 283 284 /* Resets assumptions */ 285 void btor_reset_assumptions (Btor *btor); 286 287 /* Solves instance, but with lemmas on demand limit 'lod_limit' and conflict 288 * limit for the underlying SAT solver 'sat_limit'. */ 289 int32_t btor_check_sat (Btor *btor, int32_t lod_limit, int32_t sat_limit); 290 291 BtorSATMgr *btor_get_sat_mgr (const Btor *btor); 292 BtorAIGMgr *btor_get_aig_mgr (const Btor *btor); 293 294 void btor_push (Btor *btor, uint32_t level); 295 296 void btor_pop (Btor *btor, uint32_t level); 297 298 /*------------------------------------------------------------------------*/ 299 300 /* Check whether the sorts of given arguments match the signature of the 301 * function. If sorts are correct -1 is returned, otherwise the position of 302 * the invalid argument is returned. */ 303 int32_t btor_fun_sort_check (Btor *btor, 304 BtorNode *args[], 305 uint32_t argc, 306 BtorNode *fun); 307 308 /* Synthesizes expression of arbitrary length to an AIG vector. Adds string 309 * back annotation to the hash table, if the hash table is a non zero ptr. 310 * The strings in 'data.asStr' are owned by the caller. The hash table 311 * is a map from AIG variables to strings. 312 */ 313 BtorAIGVec *btor_exp_to_aigvec (Btor *btor, 314 BtorNode *exp, 315 BtorPtrHashTable *table); 316 317 /* Checks for existing substitutions, finds most simplified expression and 318 * shortens path to it */ 319 BtorNode *btor_simplify_exp (Btor *btor, BtorNode *exp); 320 321 void btor_synthesize_exp (Btor *btor, 322 BtorNode *exp, 323 BtorPtrHashTable *backannotation); 324 325 /* Finds most simplified expression and shortens path to it */ 326 BtorNode *btor_node_get_simplified (Btor *btor, BtorNode *exp); 327 328 void btor_release_all_ext_refs (Btor *btor); 329 330 void btor_init_substitutions (Btor *); 331 void btor_delete_substitutions (Btor *); 332 void btor_insert_substitution (Btor *, BtorNode *, BtorNode *, bool); 333 BtorNode *btor_find_substitution (Btor *, BtorNode *); 334 335 /* Create a new node with 'node' substituted by 'subst' in root. */ 336 BtorNode *btor_substitute_node (Btor *btor, 337 BtorNode *root, 338 BtorNode *node, 339 BtorNode *subst); 340 341 /* Create a new node with 'substs' substituted in root. */ 342 BtorNode *btor_substitute_nodes (Btor *btor, 343 BtorNode *root, 344 BtorNodeMap *substs); 345 346 /* Create a new term with 'substs' substituted in root. If 'node_map' is given 347 * it creates an id map from old nodes to new nodes. */ 348 BtorNode *btor_substitute_nodes_node_map (Btor *btor, 349 BtorNode *root, 350 BtorNodeMap *substs, 351 BtorIntHashTable *node_map); 352 353 // TODO (ma): make these functions public until we have a common framework for 354 // calling sat simplify etc. 355 void btor_reset_incremental_usage (Btor *btor); 356 void btor_add_again_assumptions (Btor *btor); 357 void btor_process_unsynthesized_constraints (Btor *btor); 358 void btor_insert_unsynthesized_constraint (Btor *btor, BtorNode *constraint); 359 void btor_set_simplified_exp (Btor *btor, BtorNode *exp, BtorNode *simplified); 360 void btor_delete_varsubst_constraints (Btor *btor); 361 #endif 362