1 /**************************************************************************************************
2 MiniSat -- Copyright (c) 2005, Niklas Sorensson
3 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
4
5 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6 associated documentation files (the "Software"), to deal in the Software without restriction,
7 including without limitation the rights to use, copy, modify, merge, publish, distribute,
8 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in all copies or
12 substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19 **************************************************************************************************/
20 // Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
21
22 #ifndef ABC__sat__bsat__satSolver_h
23 #define ABC__sat__bsat__satSolver_h
24
25
26 #include <stdio.h>
27 #include <stdlib.h>
28 #include <string.h>
29 #include <assert.h>
30
31 #include "satVec.h"
32 #include "satClause.h"
33 #include "misc/util/utilDouble.h"
34
35 ABC_NAMESPACE_HEADER_START
36
37 //=================================================================================================
38 // Public interface:
39
40 struct sat_solver_t;
41 typedef struct sat_solver_t sat_solver;
42
43 extern sat_solver* sat_solver_new(void);
44 extern sat_solver* zsat_solver_new_seed(double seed);
45 extern void sat_solver_delete(sat_solver* s);
46
47 extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
48 extern int sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt);
49 extern int sat_solver_simplify(sat_solver* s);
50 extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
51 extern int sat_solver_solve_internal(sat_solver* s);
52 extern int sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits);
53 extern int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit );
54 extern int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit );
55 extern int sat_solver_push(sat_solver* s, int p);
56 extern void sat_solver_pop(sat_solver* s);
57 extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
58 extern void sat_solver_restart( sat_solver* s );
59 extern void zsat_solver_restart_seed( sat_solver* s, double seed );
60 extern void sat_solver_rollback( sat_solver* s );
61
62 extern int sat_solver_nvars(sat_solver* s);
63 extern int sat_solver_nclauses(sat_solver* s);
64 extern int sat_solver_nconflicts(sat_solver* s);
65 extern double sat_solver_memory(sat_solver* s);
66 extern int sat_solver_count_assigned(sat_solver* s);
67
68 extern int sat_solver_addvar(sat_solver* s);
69 extern void sat_solver_setnvars(sat_solver* s,int n);
70 extern int sat_solver_get_var_value(sat_solver* s, int v);
71 extern void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars);
72
73 extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
74 extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
75 extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );
76 extern void Sat_SolverDoubleClauses( sat_solver * p, int iVar );
77
78 // trace recording
79 extern void Sat_SolverTraceStart( sat_solver * pSat, char * pName );
80 extern void Sat_SolverTraceStop( sat_solver * pSat );
81 extern void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot );
82
83 // clause storage
84 extern void sat_solver_store_alloc( sat_solver * s );
85 extern void sat_solver_store_write( sat_solver * s, char * pFileName );
86 extern void sat_solver_store_free( sat_solver * s );
87 extern void sat_solver_store_mark_roots( sat_solver * s );
88 extern void sat_solver_store_mark_clauses_a( sat_solver * s );
89 extern void * sat_solver_store_release( sat_solver * s );
90
91 //=================================================================================================
92 // Solver representation:
93
94 //struct clause_t;
95 //typedef struct clause_t clause;
96
97 struct varinfo_t;
98 typedef struct varinfo_t varinfo;
99
100 struct sat_solver_t
101 {
102 int size; // nof variables
103 int cap; // size of varmaps
104 int qhead; // Head index of queue.
105 int qtail; // Tail index of queue.
106
107 // clauses
108 Sat_Mem_t Mem;
109 int hLearnts; // the first learnt clause
110 int hBinary; // the special binary clause
111 clause * binary;
112 veci* wlists; // watcher lists
113
114 // rollback
115 int iVarPivot; // the pivot for variables
116 int iTrailPivot; // the pivot for trail
117 int hProofPivot; // the pivot for proof records
118
119 // activities
120 int VarActType;
121 int ClaActType;
122 word var_inc; // Amount to bump next variable with.
123 word var_inc2; // Amount to bump next variable with.
124 word var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
125 word* activity; // A heuristic measurement of the activity of a variable.
126 word* activity2; // backup variable activity
127 unsigned cla_inc; // Amount to bump next clause with.
128 unsigned cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
129 veci act_clas; // contain clause activities
130
131 char * pFreqs; // how many times this variable was assigned a value
132 int nVarUsed;
133
134 // varinfo * vi; // variable information
135 int* levels; //
136 char* assigns; // Current values of variables.
137 char* polarity; //
138 char* tags; //
139 char* loads; //
140
141 int* orderpos; // Index in variable order.
142 int* reasons; //
143 lit* trail;
144 veci tagged; // (contains: var)
145 veci stack; // (contains: var)
146
147 veci order; // Variable order. (heap) (contains: var)
148 veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
149 // veci model; // If problem is solved, this vector contains the model (contains: lbool).
150 int * model; // If problem is solved, this vector contains the model (contains: lbool).
151 veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
152 // this vector represent the final conflict clause expressed in the assumptions.
153
154 int root_level; // Level of first proper decision.
155 int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
156 int simpdb_props; // Number of propagations before next 'simplifyDB()'.
157 double random_seed;
158 double progress_estimate;
159 int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
160 int fVerbose;
161 int fPrintClause;
162
163 stats_t stats;
164 int nLearntMax; // max number of learned clauses
165 int nLearntStart; // starting learned clause limit
166 int nLearntDelta; // delta of learned clause limit
167 int nLearntRatio; // ratio percentage of learned clauses
168 int nDBreduces; // number of DB reductions
169
170 ABC_INT64_T nConfLimit; // external limit on the number of conflicts
171 ABC_INT64_T nInsLimit; // external limit on the number of implications
172 abctime nRuntimeLimit; // external limit on runtime
173
174 veci act_vars; // variables whose activity has changed
175 double* factors; // the activity factors
176 int nRestarts; // the number of local restarts
177 int nCalls; // the number of local restarts
178 int nCalls2; // the number of local restarts
179 veci unit_lits; // variables whose activity has changed
180 veci pivot_vars; // pivot variables
181
182 int fSkipSimplify; // set to one to skip simplification of the clause database
183 int fNotUseRandom; // do not allow random decisions with a fixed probability
184 int fNoRestarts; // disables periodic restarts
185
186 int * pGlobalVars; // for experiments with global vars during interpolation
187 // clause store
188 void * pStore;
189 int fSolved;
190
191 // trace recording
192 FILE * pFile;
193 int nClauses;
194 int nRoots;
195
196 veci temp_clause; // temporary storage for a CNF clause
197
198 // assignment storage
199 veci user_vars; // variable IDs
200 veci user_values; // values of these variables
201
202 // CNF loading
203 void * pCnfMan; // external CNF manager
204 int(*pCnfFunc)(void * p, int); // external callback
205
206 // termination callback
207 int RunId; // SAT id in this run
208 int(*pFuncStop)(int); // callback to terminate
209 };
210
clause_read(sat_solver * s,cla h)211 static inline clause * clause_read( sat_solver * s, cla h )
212 {
213 return Sat_MemClauseHand( &s->Mem, h );
214 }
215
sat_solver_var_value(sat_solver * s,int v)216 static inline int sat_solver_var_value( sat_solver* s, int v )
217 {
218 assert( v >= 0 && v < s->size );
219 return (int)(s->model[v] == l_True);
220 }
sat_solver_var_literal(sat_solver * s,int v)221 static inline int sat_solver_var_literal( sat_solver* s, int v )
222 {
223 assert( v >= 0 && v < s->size );
224 return toLitCond( v, s->model[v] != l_True );
225 }
sat_solver_flip_print_clause(sat_solver * s)226 static inline void sat_solver_flip_print_clause( sat_solver* s )
227 {
228 s->fPrintClause ^= 1;
229 }
sat_solver_act_var_clear(sat_solver * s)230 static inline void sat_solver_act_var_clear(sat_solver* s)
231 {
232 int i;
233 if ( s->VarActType == 0 )
234 {
235 for (i = 0; i < s->size; i++)
236 s->activity[i] = (1 << 10);
237 s->var_inc = (1 << 5);
238 }
239 else if ( s->VarActType == 1 )
240 {
241 for (i = 0; i < s->size; i++)
242 s->activity[i] = 0;
243 s->var_inc = 1;
244 }
245 else if ( s->VarActType == 2 )
246 {
247 for (i = 0; i < s->size; i++)
248 s->activity[i] = Xdbl_Const1();
249 s->var_inc = Xdbl_Const1();
250 }
251 else assert(0);
252 }
sat_solver_compress(sat_solver * s)253 static inline void sat_solver_compress(sat_solver* s)
254 {
255 if ( s->qtail != s->qhead )
256 {
257 int RetValue = sat_solver_simplify(s);
258 assert( RetValue != 0 );
259 (void) RetValue;
260 }
261 }
sat_solver_delete_p(sat_solver ** ps)262 static inline void sat_solver_delete_p( sat_solver ** ps )
263 {
264 if ( *ps )
265 sat_solver_delete( *ps );
266 *ps = NULL;
267 }
sat_solver_clean_polarity(sat_solver * s,int * pVars,int nVars)268 static inline void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
269 {
270 int i;
271 for ( i = 0; i < nVars; i++ )
272 s->polarity[pVars[i]] = 0;
273 }
sat_solver_set_polarity(sat_solver * s,int * pVars,int nVars)274 static inline void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
275 {
276 int i;
277 for ( i = 0; i < s->size; i++ )
278 s->polarity[i] = 0;
279 for ( i = 0; i < nVars; i++ )
280 s->polarity[pVars[i]] = 1;
281 }
sat_solver_set_literal_polarity(sat_solver * s,int * pLits,int nLits)282 static inline void sat_solver_set_literal_polarity(sat_solver* s, int * pLits, int nLits )
283 {
284 int i;
285 for ( i = 0; i < nLits; i++ )
286 s->polarity[Abc_Lit2Var(pLits[i])] = !Abc_LitIsCompl(pLits[i]);
287 }
288
sat_solver_final(sat_solver * s,int ** ppArray)289 static inline int sat_solver_final(sat_solver* s, int ** ppArray)
290 {
291 *ppArray = s->conf_final.ptr;
292 return s->conf_final.size;
293 }
294
sat_solver_set_runtime_limit(sat_solver * s,abctime Limit)295 static inline abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit)
296 {
297 abctime nRuntimeLimit = s->nRuntimeLimit;
298 s->nRuntimeLimit = Limit;
299 return nRuntimeLimit;
300 }
301
sat_solver_set_random(sat_solver * s,int fNotUseRandom)302 static inline int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
303 {
304 int fNotUseRandomOld = s->fNotUseRandom;
305 s->fNotUseRandom = fNotUseRandom;
306 return fNotUseRandomOld;
307 }
308
sat_solver_bookmark(sat_solver * s)309 static inline void sat_solver_bookmark(sat_solver* s)
310 {
311 assert( s->qhead == s->qtail );
312 s->iVarPivot = s->size;
313 s->iTrailPivot = s->qhead;
314 Sat_MemBookMark( &s->Mem );
315 if ( s->activity2 )
316 {
317 s->var_inc2 = s->var_inc;
318 memcpy( s->activity2, s->activity, sizeof(word) * s->iVarPivot );
319 }
320 }
sat_solver_set_pivot_variables(sat_solver * s,int * pPivots,int nPivots)321 static inline void sat_solver_set_pivot_variables( sat_solver* s, int * pPivots, int nPivots )
322 {
323 s->pivot_vars.cap = nPivots;
324 s->pivot_vars.size = nPivots;
325 s->pivot_vars.ptr = pPivots;
326 }
sat_solver_count_usedvars(sat_solver * s)327 static inline int sat_solver_count_usedvars(sat_solver* s)
328 {
329 int i, nVars = 0;
330 for ( i = 0; i < s->size; i++ )
331 if ( s->pFreqs[i] )
332 {
333 s->pFreqs[i] = 0;
334 nVars++;
335 }
336 return nVars;
337 }
sat_solver_set_runid(sat_solver * s,int id)338 static inline void sat_solver_set_runid( sat_solver *s, int id )
339 {
340 s->RunId = id;
341 }
sat_solver_set_stop_func(sat_solver * s,int (* fnct)(int))342 static inline void sat_solver_set_stop_func( sat_solver *s, int (*fnct)(int) )
343 {
344 s->pFuncStop = fnct;
345 }
346
sat_solver_add_const(sat_solver * pSat,int iVar,int fCompl)347 static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
348 {
349 lit Lits[1];
350 int Cid;
351 assert( iVar >= 0 );
352
353 Lits[0] = toLitCond( iVar, fCompl );
354 Cid = sat_solver_addclause( pSat, Lits, Lits + 1 );
355 assert( Cid );
356 return 1;
357 }
sat_solver_add_buffer(sat_solver * pSat,int iVarA,int iVarB,int fCompl)358 static inline int sat_solver_add_buffer( sat_solver * pSat, int iVarA, int iVarB, int fCompl )
359 {
360 lit Lits[2];
361 int Cid;
362 assert( iVarA >= 0 && iVarB >= 0 );
363
364 Lits[0] = toLitCond( iVarA, 0 );
365 Lits[1] = toLitCond( iVarB, !fCompl );
366 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
367 if ( Cid == 0 )
368 return 0;
369 assert( Cid );
370
371 Lits[0] = toLitCond( iVarA, 1 );
372 Lits[1] = toLitCond( iVarB, fCompl );
373 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
374 if ( Cid == 0 )
375 return 0;
376 assert( Cid );
377 return 2;
378 }
sat_solver_add_buffer_enable(sat_solver * pSat,int iVarA,int iVarB,int iVarEn,int fCompl)379 static inline int sat_solver_add_buffer_enable( sat_solver * pSat, int iVarA, int iVarB, int iVarEn, int fCompl )
380 {
381 lit Lits[3];
382 int Cid;
383 assert( iVarA >= 0 && iVarB >= 0 && iVarEn >= 0 );
384
385 Lits[0] = toLitCond( iVarA, 0 );
386 Lits[1] = toLitCond( iVarB, !fCompl );
387 Lits[2] = toLitCond( iVarEn, 1 );
388 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
389 assert( Cid );
390
391 Lits[0] = toLitCond( iVarA, 1 );
392 Lits[1] = toLitCond( iVarB, fCompl );
393 Lits[2] = toLitCond( iVarEn, 1 );
394 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
395 assert( Cid );
396 return 2;
397 }
sat_solver_add_and(sat_solver * pSat,int iVar,int iVar0,int iVar1,int fCompl0,int fCompl1,int fCompl)398 static inline int sat_solver_add_and( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
399 {
400 lit Lits[3];
401 int Cid;
402
403 Lits[0] = toLitCond( iVar, !fCompl );
404 Lits[1] = toLitCond( iVar0, fCompl0 );
405 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
406 assert( Cid );
407
408 Lits[0] = toLitCond( iVar, !fCompl );
409 Lits[1] = toLitCond( iVar1, fCompl1 );
410 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
411 assert( Cid );
412
413 Lits[0] = toLitCond( iVar, fCompl );
414 Lits[1] = toLitCond( iVar0, !fCompl0 );
415 Lits[2] = toLitCond( iVar1, !fCompl1 );
416 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
417 assert( Cid );
418 return 3;
419 }
sat_solver_add_xor(sat_solver * pSat,int iVarA,int iVarB,int iVarC,int fCompl)420 static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
421 {
422 lit Lits[3];
423 int Cid;
424 assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
425
426 Lits[0] = toLitCond( iVarA, !fCompl );
427 Lits[1] = toLitCond( iVarB, 1 );
428 Lits[2] = toLitCond( iVarC, 1 );
429 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
430 assert( Cid );
431
432 Lits[0] = toLitCond( iVarA, !fCompl );
433 Lits[1] = toLitCond( iVarB, 0 );
434 Lits[2] = toLitCond( iVarC, 0 );
435 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
436 assert( Cid );
437
438 Lits[0] = toLitCond( iVarA, fCompl );
439 Lits[1] = toLitCond( iVarB, 1 );
440 Lits[2] = toLitCond( iVarC, 0 );
441 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
442 assert( Cid );
443
444 Lits[0] = toLitCond( iVarA, fCompl );
445 Lits[1] = toLitCond( iVarB, 0 );
446 Lits[2] = toLitCond( iVarC, 1 );
447 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
448 assert( Cid );
449 return 4;
450 }
sat_solver_add_mux(sat_solver * pSat,int iVarZ,int iVarC,int iVarT,int iVarE,int iComplC,int iComplT,int iComplE,int iComplZ)451 static inline int sat_solver_add_mux( sat_solver * pSat, int iVarZ, int iVarC, int iVarT, int iVarE, int iComplC, int iComplT, int iComplE, int iComplZ )
452 {
453 lit Lits[3];
454 int Cid;
455 assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 );
456
457 Lits[0] = toLitCond( iVarC, 1 ^ iComplC );
458 Lits[1] = toLitCond( iVarT, 1 ^ iComplT );
459 Lits[2] = toLitCond( iVarZ, 0 );
460 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
461 assert( Cid );
462
463 Lits[0] = toLitCond( iVarC, 1 ^ iComplC );
464 Lits[1] = toLitCond( iVarT, 0 ^ iComplT );
465 Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ );
466 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
467 assert( Cid );
468
469 Lits[0] = toLitCond( iVarC, 0 ^ iComplC );
470 Lits[1] = toLitCond( iVarE, 1 ^ iComplE );
471 Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ );
472 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
473 assert( Cid );
474
475 Lits[0] = toLitCond( iVarC, 0 ^ iComplC );
476 Lits[1] = toLitCond( iVarE, 0 ^ iComplE );
477 Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ );
478 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
479 assert( Cid );
480
481 if ( iVarT == iVarE )
482 return 4;
483
484 Lits[0] = toLitCond( iVarT, 0 ^ iComplT );
485 Lits[1] = toLitCond( iVarE, 0 ^ iComplE );
486 Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ );
487 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
488 assert( Cid );
489
490 Lits[0] = toLitCond( iVarT, 1 ^ iComplT );
491 Lits[1] = toLitCond( iVarE, 1 ^ iComplE );
492 Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ );
493 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
494 assert( Cid );
495 return 6;
496 }
sat_solver_add_mux41(sat_solver * pSat,int iVarZ,int iVarC0,int iVarC1,int iVarD0,int iVarD1,int iVarD2,int iVarD3)497 static inline int sat_solver_add_mux41( sat_solver * pSat, int iVarZ, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3 )
498 {
499 lit Lits[4];
500 int Cid;
501 assert( iVarC0 >= 0 && iVarC1 >= 0 && iVarD0 >= 0 && iVarD1 >= 0 && iVarD2 >= 0 && iVarD3 >= 0 && iVarZ >= 0 );
502
503 Lits[0] = toLitCond( iVarD0, 1 );
504 Lits[1] = toLitCond( iVarC0, 0 );
505 Lits[2] = toLitCond( iVarC1, 0 );
506 Lits[3] = toLitCond( iVarZ, 0 );
507 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
508 assert( Cid );
509
510 Lits[0] = toLitCond( iVarD1, 1 );
511 Lits[1] = toLitCond( iVarC0, 1 );
512 Lits[2] = toLitCond( iVarC1, 0 );
513 Lits[3] = toLitCond( iVarZ, 0 );
514 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
515 assert( Cid );
516
517 Lits[0] = toLitCond( iVarD2, 1 );
518 Lits[1] = toLitCond( iVarC0, 0 );
519 Lits[2] = toLitCond( iVarC1, 1 );
520 Lits[3] = toLitCond( iVarZ, 0 );
521 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
522 assert( Cid );
523
524 Lits[0] = toLitCond( iVarD3, 1 );
525 Lits[1] = toLitCond( iVarC0, 1 );
526 Lits[2] = toLitCond( iVarC1, 1 );
527 Lits[3] = toLitCond( iVarZ, 0 );
528 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
529 assert( Cid );
530
531
532 Lits[0] = toLitCond( iVarD0, 0 );
533 Lits[1] = toLitCond( iVarC0, 0 );
534 Lits[2] = toLitCond( iVarC1, 0 );
535 Lits[3] = toLitCond( iVarZ, 1 );
536 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
537 assert( Cid );
538
539 Lits[0] = toLitCond( iVarD1, 0 );
540 Lits[1] = toLitCond( iVarC0, 1 );
541 Lits[2] = toLitCond( iVarC1, 0 );
542 Lits[3] = toLitCond( iVarZ, 1 );
543 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
544 assert( Cid );
545
546 Lits[0] = toLitCond( iVarD2, 0 );
547 Lits[1] = toLitCond( iVarC0, 0 );
548 Lits[2] = toLitCond( iVarC1, 1 );
549 Lits[3] = toLitCond( iVarZ, 1 );
550 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
551 assert( Cid );
552
553 Lits[0] = toLitCond( iVarD3, 0 );
554 Lits[1] = toLitCond( iVarC0, 1 );
555 Lits[2] = toLitCond( iVarC1, 1 );
556 Lits[3] = toLitCond( iVarZ, 1 );
557 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
558 assert( Cid );
559 return 8;
560 }
sat_solver_add_xor_and(sat_solver * pSat,int iVarF,int iVarA,int iVarB,int iVarC)561 static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC )
562 {
563 // F = (a (+) b) * c
564 lit Lits[4];
565 int Cid;
566 assert( iVarF >= 0 && iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
567
568 Lits[0] = toLitCond( iVarF, 1 );
569 Lits[1] = toLitCond( iVarA, 1 );
570 Lits[2] = toLitCond( iVarB, 1 );
571 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
572 assert( Cid );
573
574 Lits[0] = toLitCond( iVarF, 1 );
575 Lits[1] = toLitCond( iVarA, 0 );
576 Lits[2] = toLitCond( iVarB, 0 );
577 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
578 assert( Cid );
579
580 Lits[0] = toLitCond( iVarF, 1 );
581 Lits[1] = toLitCond( iVarC, 0 );
582 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
583 assert( Cid );
584
585 Lits[0] = toLitCond( iVarF, 0 );
586 Lits[1] = toLitCond( iVarA, 1 );
587 Lits[2] = toLitCond( iVarB, 0 );
588 Lits[3] = toLitCond( iVarC, 1 );
589 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
590 assert( Cid );
591
592 Lits[0] = toLitCond( iVarF, 0 );
593 Lits[1] = toLitCond( iVarA, 0 );
594 Lits[2] = toLitCond( iVarB, 1 );
595 Lits[3] = toLitCond( iVarC, 1 );
596 Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
597 assert( Cid );
598 return 5;
599 }
sat_solver_add_constraint(sat_solver * pSat,int iVar,int iVar2,int fCompl)600 static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int iVar2, int fCompl )
601 {
602 lit Lits[2];
603 int Cid;
604 assert( iVar >= 0 );
605
606 Lits[0] = toLitCond( iVar, fCompl );
607 Lits[1] = toLitCond( iVar2, 0 );
608 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
609 assert( Cid );
610
611 Lits[0] = toLitCond( iVar, fCompl );
612 Lits[1] = toLitCond( iVar2, 1 );
613 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
614 assert( Cid );
615 return 2;
616 }
617
sat_solver_add_half_sorter(sat_solver * pSat,int iVarA,int iVarB,int iVar0,int iVar1)618 static inline int sat_solver_add_half_sorter( sat_solver * pSat, int iVarA, int iVarB, int iVar0, int iVar1 )
619 {
620 lit Lits[3];
621 int Cid;
622
623 Lits[0] = toLitCond( iVarA, 0 );
624 Lits[1] = toLitCond( iVar0, 1 );
625 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
626 assert( Cid );
627
628 Lits[0] = toLitCond( iVarA, 0 );
629 Lits[1] = toLitCond( iVar1, 1 );
630 Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
631 assert( Cid );
632
633 Lits[0] = toLitCond( iVarB, 0 );
634 Lits[1] = toLitCond( iVar0, 1 );
635 Lits[2] = toLitCond( iVar1, 1 );
636 Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
637 assert( Cid );
638 return 3;
639 }
640
641
642 ABC_NAMESPACE_HEADER_END
643
644 #endif
645