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