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 BTORSLVFUN_H_INCLUDED 10 #define BTORSLVFUN_H_INCLUDED 11 12 #include "btornode.h" 13 #include "btorslv.h" 14 #include "utils/btorhashptr.h" 15 16 #define BTOR_FUN_SOLVER(btor) ((BtorFunSolver *) (btor)->slv) 17 18 struct BtorFunSolver 19 { 20 BTOR_SOLVER_STRUCT; 21 22 BtorPtrHashTable *lemmas; 23 BtorNodePtrStack cur_lemmas; 24 25 BtorPtrHashTable *score; /* dcr score */ 26 27 // TODO (ma): make options for these 28 int32_t lod_limit; 29 int32_t sat_limit; 30 bool assume_lemmas; 31 32 struct 33 { 34 uint32_t lod_refinements; /* number of lemmas on demand refinements */ 35 uint32_t refinement_iterations; 36 37 uint32_t function_congruence_conflicts; 38 uint32_t beta_reduction_conflicts; 39 uint32_t extensionality_lemmas; 40 41 BtorUIntStack lemmas_size; /* distribution of n-size lemmas */ 42 uint_least64_t lemmas_size_sum; /* sum of the size of all added lemmas */ 43 44 uint32_t dp_failed_vars; /* number of vars in FA (dual prop) of last 45 sat call (final bv skeleton) */ 46 uint32_t dp_assumed_vars; 47 uint32_t dp_failed_applies; /* number of applies in FA (dual prop) of last 48 sat call (final bv skeleton) */ 49 uint32_t dp_assumed_applies; 50 uint32_t dp_failed_eqs; 51 uint32_t dp_assumed_eqs; 52 53 uint_least64_t eval_exp_calls; 54 uint_least64_t propagations; 55 uint_least64_t propagations_down; 56 } stats; 57 58 struct 59 { 60 double sat; 61 double eval; 62 double search_init_apps; 63 double search_init_apps_compute_scores; 64 double search_init_apps_compute_scores_merge_applies; 65 double search_init_apps_cloning; 66 double search_init_apps_sat; 67 double search_init_apps_collect_var_apps; 68 double search_init_apps_collect_fa; 69 double search_init_apps_collect_fa_cone; 70 double lemma_gen; 71 double find_prop_app; 72 double check_consistency; 73 double prop; 74 double betap; 75 double find_conf_app; 76 double check_extensionality; 77 double prop_cleanup; 78 } time; 79 }; 80 81 typedef struct BtorFunSolver BtorFunSolver; 82 83 BtorSolver *btor_new_fun_solver (Btor *btor); 84 85 // TODO (ma): this is just a fix for now, this should be moved elsewhere 86 /* Evaluates expression and returns its value. */ 87 BtorBitVector *btor_eval_exp (Btor *btor, BtorNode *exp); 88 #endif 89