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