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 #include "sat/btorcadical.h"
10 #include "btorabort.h"
11
12 /*------------------------------------------------------------------------*/
13 #ifdef BTOR_USE_CADICAL
14 /*------------------------------------------------------------------------*/
15
16 #include "btorcore.h"
17 #include "ccadical.h"
18
19 static void *
init(BtorSATMgr * smgr)20 init (BtorSATMgr *smgr)
21 {
22 (void) smgr;
23 CCaDiCaL *slv = ccadical_init ();
24 if (smgr->inc_required
25 && btor_opt_get (smgr->btor, BTOR_OPT_SAT_ENGINE_CADICAL_FREEZE))
26 {
27 ccadical_set_option (slv, "checkfrozen", 1);
28 }
29 return slv;
30 }
31
32 static void
add(BtorSATMgr * smgr,int32_t lit)33 add (BtorSATMgr *smgr, int32_t lit)
34 {
35 ccadical_add (smgr->solver, lit);
36 }
37
38 static void
assume(BtorSATMgr * smgr,int32_t lit)39 assume (BtorSATMgr *smgr, int32_t lit)
40 {
41 ccadical_assume (smgr->solver, lit);
42 }
43
44 static int32_t
deref(BtorSATMgr * smgr,int32_t lit)45 deref (BtorSATMgr *smgr, int32_t lit)
46 {
47 int32_t val;
48 val = ccadical_deref (smgr->solver, lit);
49 if (val > 0)
50 return 1;
51 if (val < 0)
52 return -1;
53 return 0;
54 }
55
56 static void
enable_verbosity(BtorSATMgr * smgr,int32_t level)57 enable_verbosity (BtorSATMgr *smgr, int32_t level)
58 {
59 if (level <= 1)
60 ccadical_set_option (smgr->solver, "quiet", 1);
61 else if (level >= 2)
62 ccadical_set_option (smgr->solver, "verbose", level - 2);
63 }
64
65 static int32_t
failed(BtorSATMgr * smgr,int32_t lit)66 failed (BtorSATMgr *smgr, int32_t lit)
67 {
68 return ccadical_failed (smgr->solver, lit);
69 }
70
71 static void
reset(BtorSATMgr * smgr)72 reset (BtorSATMgr *smgr)
73 {
74 ccadical_reset (smgr->solver);
75 smgr->solver = 0;
76 }
77
78 static int32_t
sat(BtorSATMgr * smgr,int32_t limit)79 sat (BtorSATMgr *smgr, int32_t limit)
80 {
81 (void) limit;
82 return ccadical_sat (smgr->solver);
83 }
84
85 static void
setterm(BtorSATMgr * smgr)86 setterm (BtorSATMgr *smgr)
87 {
88 /* for CaDiCaL, state is the first argument (unlike, e.g., Lingeling) */
89 ccadical_set_terminate (smgr->solver, smgr->term.state, smgr->term.fun);
90 }
91
92 /*------------------------------------------------------------------------*/
93 /* incremental API */
94 /*------------------------------------------------------------------------*/
95
96 static int32_t
inc_max_var(BtorSATMgr * smgr)97 inc_max_var (BtorSATMgr *smgr)
98 {
99 int32_t var = smgr->maxvar + 1;
100 if (smgr->inc_required)
101 {
102 ccadical_freeze (smgr->solver, var);
103 }
104 return var;
105 }
106
107 static void
melt(BtorSATMgr * smgr,int32_t lit)108 melt (BtorSATMgr *smgr, int32_t lit)
109 {
110 if (smgr->inc_required) ccadical_melt (smgr->solver, lit);
111 }
112
113 /*------------------------------------------------------------------------*/
114
115 bool
btor_sat_enable_cadical(BtorSATMgr * smgr)116 btor_sat_enable_cadical (BtorSATMgr *smgr)
117 {
118 assert (smgr != NULL);
119
120 BTOR_ABORT (smgr->initialized,
121 "'btor_sat_init' called before 'btor_sat_enable_cadical'");
122
123 smgr->name = "CaDiCaL";
124
125 BTOR_CLR (&smgr->api);
126 smgr->api.add = add;
127 smgr->api.assume = assume;
128 smgr->api.deref = deref;
129 smgr->api.enable_verbosity = enable_verbosity;
130 smgr->api.failed = failed;
131 smgr->api.fixed = 0;
132 smgr->api.inc_max_var = 0;
133 smgr->api.init = init;
134 smgr->api.melt = 0;
135 smgr->api.repr = 0;
136 smgr->api.reset = reset;
137 smgr->api.sat = sat;
138 smgr->api.set_output = 0;
139 smgr->api.set_prefix = 0;
140 smgr->api.stats = 0;
141 smgr->api.setterm = setterm;
142
143 if (btor_opt_get (smgr->btor, BTOR_OPT_SAT_ENGINE_CADICAL_FREEZE))
144 {
145 smgr->api.inc_max_var = inc_max_var;
146 smgr->api.melt = melt;
147 }
148 else
149 {
150 smgr->have_restore = true;
151 }
152
153 return true;
154 }
155
156 /*------------------------------------------------------------------------*/
157 #endif
158 /*------------------------------------------------------------------------*/
159