1 // *********************************************************************
2 // Copyright 2000-2004, Princeton University. All rights reserved.
3 // By using this software the USER indicates that he or she has read,
4 // understood and will comply with the following:
6 // --- Princeton University hereby grants USER nonexclusive permission
7 // to use, copy and/or modify this software for internal, noncommercial,
8 // research purposes only. Any distribution, including commercial sale
9 // or license, of this software, copies of the software, its associated
10 // documentation and/or modifications of either is strictly prohibited
11 // without the prior consent of Princeton University. Title to copyright
12 // to this software and its associated documentation shall at all times
13 // remain with Princeton University. Appropriate copyright notice shall
14 // be placed on all software copies, and a complete copy of this notice
15 // shall be included in all copies of the associated documentation.
16 // No right is granted to use in advertising, publicity or otherwise
17 // any trademark, service mark, or the name of Princeton University.
20 // --- This software and any associated documentation is provided "as is"
22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
24 // PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR
25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
28 // Princeton University shall not be liable under any circumstances for
29 // any direct, indirect, special, incidental, or consequential damages
30 // with respect to any claim by USER or any third party on account of
31 // or arising from the use, or inability to use, this software or its
32 // associated documentation, even if Princeton University has been advised
33 // of the possibility of those damages.
34 // ********************************************************************
44 #include "zchaff_solver.h"
45 #include "zchaff_clsgen.h"
48 #define SAT_Manager void *
51 // =====================================================================
52 // Following are wrapper functions for C/C++ callers.
54 // =====================================================================
56 EXTERN SAT_Manager SAT_InitManager(void) {
57 CSolver * solver = new CSolver;
58 return (SAT_Manager)solver;
61 EXTERN char * SAT_Version(SAT_Manager mng) {
62 CSolver * solver = (CSolver*) mng;
63 return solver->version();
66 EXTERN void SAT_SetNumVariables(SAT_Manager mng, int n_var) {
67 CSolver * solver = (CSolver*) mng;
68 solver->set_variable_number(n_var);
71 EXTERN void SAT_ReleaseManager(SAT_Manager mng) {
72 CSolver * solver = (CSolver*) mng;
76 EXTERN int SAT_AddVariable(SAT_Manager mng) {
77 CSolver * solver = (CSolver*) mng;
78 int vid = solver->add_variable();
82 EXTERN void SAT_EnableVarBranch(SAT_Manager mng, int vid) {
83 CSolver * solver = (CSolver*) mng;
84 solver->mark_var_branchable(vid);
87 EXTERN void SAT_DisableVarBranch(SAT_Manager mng, int vid) {
88 CSolver * solver = (CSolver*) mng;
89 solver->mark_var_unbranchable(vid);
92 EXTERN void SAT_SetTimeLimit(SAT_Manager mng, float runtime) {
93 CSolver * solver = (CSolver*) mng;
94 solver->set_time_limit(runtime);
97 EXTERN void SAT_SetMemLimit(SAT_Manager mng, int mem_limit) {
98 CSolver * solver = (CSolver*) mng;
99 solver->set_mem_limit(mem_limit);
102 EXTERN void SAT_AddClause(SAT_Manager mng,
106 CSolver * solver = (CSolver*) mng;
107 solver->add_orig_clause(clause_lits, num_lits, gid);
110 EXTERN void SAT_DeleteClauseGroup(SAT_Manager mng,
112 CSolver * solver = (CSolver*) mng;
113 solver->delete_clause_group(gid);
116 EXTERN void SAT_Reset(SAT_Manager mng) {
117 CSolver * solver = (CSolver*) mng;
121 EXTERN int SAT_MergeClauseGroup(SAT_Manager mng,
124 CSolver * solver = (CSolver*) mng;
125 int g = solver->merge_clause_group(gid1, gid2);
129 EXTERN int SAT_AllocClauseGroupID(SAT_Manager mng) {
130 CSolver * solver = (CSolver*) mng;
131 int gid = solver->alloc_gid();
135 EXTERN int SAT_GetGlobalGroupID(SAT_Manager mng) {
139 EXTERN int SAT_GetVolatileGroupID(SAT_Manager mng) {
143 EXTERN int SAT_Solve(SAT_Manager mng) {
144 CSolver * solver = (CSolver*) mng;
145 int result = solver->solve();
149 EXTERN void SAT_AddHookFun(SAT_Manager mng,
152 CSolver * solver = (CSolver*) mng;
153 solver->add_hook(fun, interval);
156 EXTERN void SAT_MakeDecision(SAT_Manager mng,
159 CSolver * solver = (CSolver*) mng;
160 solver->make_decision(vid+vid+sign);
163 EXTERN void SAT_SetRandomness(SAT_Manager mng,
165 CSolver * solver = (CSolver*) mng;
166 solver->set_randomness(n);
169 EXTERN void SAT_SetRandSeed(SAT_Manager mng,
171 CSolver * solver = (CSolver*) mng;
172 solver->set_random_seed(seed);
175 EXTERN int SAT_GetVarAsgnment(SAT_Manager mng,
177 CSolver * solver = (CSolver*) mng;
178 assert(v_idx > 0 && v_idx < (int) solver->variables()->size());
179 int v = solver->variable(v_idx).value();
183 EXTERN int SAT_EstimateMemUsage(SAT_Manager mng) {
184 CSolver * solver = (CSolver*) mng;
185 int usage = solver->estimate_mem_usage();
189 EXTERN float SAT_GetElapsedCPUTime(SAT_Manager mng) {
190 CSolver * solver = (CSolver*) mng;
191 float time = solver->elapsed_cpu_time();
195 EXTERN float SAT_GetCurrentCPUTime(SAT_Manager mng) {
196 float time = get_cpu_time() / 1000.0;
200 EXTERN float SAT_GetCPUTime(SAT_Manager mng) {
201 CSolver * solver = (CSolver*) mng;
202 float time = solver->cpu_run_time();
206 EXTERN int SAT_NumLiterals(SAT_Manager mng) {
207 CSolver * solver = (CSolver*) mng;
208 int n = solver->num_literals();
212 EXTERN int SAT_NumClauses(SAT_Manager mng) {
213 CSolver * solver = (CSolver*) mng;
214 int n = solver->num_clauses();
218 EXTERN int SAT_NumVariables(SAT_Manager mng) {
219 CSolver * solver = (CSolver*) mng;
220 int n = solver->num_variables();
224 EXTERN int SAT_InitNumLiterals(SAT_Manager mng) {
225 CSolver * solver = (CSolver*) mng;
226 int n = solver->init_num_literals();
230 EXTERN int SAT_InitNumClauses(SAT_Manager mng) {
231 CSolver * solver = (CSolver*) mng;
232 int n = solver->init_num_clauses();
236 EXTERN long64 SAT_NumAddedLiterals(SAT_Manager mng) {
237 CSolver * solver = (CSolver*) mng;
238 long64 n = solver->num_added_literals();
242 EXTERN int SAT_NumAddedClauses(SAT_Manager mng) {
243 CSolver * solver = (CSolver*) mng;
244 int n = solver->num_added_clauses();
248 EXTERN int SAT_NumDeletedClauses(SAT_Manager mng) {
249 CSolver * solver = (CSolver*) mng;
250 int n = solver->num_deleted_clauses();
254 EXTERN int SAT_NumDelOrigCls(SAT_Manager mng) {
255 CSolver * solver = (CSolver*) mng;
256 int n = solver->num_del_orig_cls();
260 EXTERN long64 SAT_NumDeletedLiterals(SAT_Manager mng) {
261 CSolver * solver = (CSolver*) mng;
262 long64 n = solver->num_deleted_literals();
266 EXTERN int SAT_NumDecisions(SAT_Manager mng) {
267 CSolver * solver = (CSolver*) mng;
268 int n = solver->num_decisions();
272 EXTERN int SAT_NumDecisionsStackConf(SAT_Manager mng) {
273 CSolver * solver = (CSolver*) mng;
274 int n = solver->num_decisions_stack_conf();
278 EXTERN int SAT_NumDecisionsVsids(SAT_Manager mng) {
279 CSolver * solver = (CSolver*) mng;
280 int n = solver->num_decisions_vsids();
284 EXTERN int SAT_NumDecisionsShrinking(SAT_Manager mng) {
285 CSolver * solver = (CSolver*) mng;
286 int n = solver->num_decisions_shrinking();
290 EXTERN int SAT_NumShrinkings(SAT_Manager mng) {
291 CSolver * solver = (CSolver*) mng;
292 int n = solver->num_shrinkings();
296 EXTERN int SAT_Random_Seed(SAT_Manager mng) {
297 CSolver * solver = (CSolver*) mng;
298 int n = solver->random_seed();
302 EXTERN long64 SAT_NumImplications(SAT_Manager mng) {
303 CSolver * solver = (CSolver*) mng;
304 long64 n = solver->num_implications();
308 EXTERN int SAT_MaxDLevel(SAT_Manager mng) {
309 CSolver * solver = (CSolver*) mng;
310 int n = solver->max_dlevel();
314 EXTERN float SAT_AverageBubbleMove(SAT_Manager mng) {
315 CSolver * solver = (CSolver*) mng;
316 float n = ((float) solver->total_bubble_move()) /
317 (solver->num_added_literals() - solver->init_num_literals());
321 EXTERN int SAT_GetFirstClause(SAT_Manager mng) {
322 CSolver * solver = (CSolver*) mng;
323 for (unsigned i = 0; i < solver->clauses()->size(); ++i)
324 if (solver->clause(i).status() != DELETED_CL) {
330 EXTERN int SAT_GetClauseType(SAT_Manager mng, int cl_idx) {
331 CSolver * solver = (CSolver*) mng;
332 int type = solver->clause(cl_idx).status();
336 EXTERN int SAT_IsSetClauseGroupID(SAT_Manager mng, int cl_idx, int id) {
337 CSolver * solver = (CSolver*) mng;
338 int r = solver->clause(cl_idx).gid(id);
342 EXTERN void SAT_ClearClauseGroupID(SAT_Manager mng, int cl_idx, int id) {
343 CSolver * solver = (CSolver*) mng;
344 solver->clause(cl_idx).clear_gid(id);
347 EXTERN void SAT_SetClauseGroupID(SAT_Manager mng, int cl_idx, int id) {
348 CSolver * solver = (CSolver*) mng;
349 solver->clause(cl_idx).set_gid(id);
352 EXTERN int SAT_GetNextClause(SAT_Manager mng, int cl_idx) {
353 CSolver * solver = (CSolver*) mng;
354 for (unsigned i = cl_idx + 1; i < solver->clauses()->size(); ++i)
355 if (solver->clause(i).status() != DELETED_CL) {
361 EXTERN int SAT_GetClauseNumLits(SAT_Manager mng, int cl_idx) {
362 CSolver * solver = (CSolver*) mng;
363 int n = solver->clause(cl_idx).num_lits();
367 EXTERN void SAT_GetClauseLits(SAT_Manager mng, int cl_idx, int * lits) {
368 CSolver * solver = (CSolver*) mng;
369 for (unsigned i = 0; i < solver->clause(cl_idx).num_lits(); ++i) {
370 lits[i] = solver->clause(cl_idx).literal(i).s_var();
374 EXTERN void SAT_EnableConfClsDeletion(SAT_Manager mng) {
375 CSolver * solver = (CSolver*) mng;
376 solver->enable_cls_deletion(true);
379 EXTERN void SAT_DisableConfClsDeletion(SAT_Manager mng) {
380 CSolver * solver = (CSolver*) mng;
381 solver->enable_cls_deletion(false);
384 EXTERN void SAT_CleanUpDatabase(SAT_Manager mng) {
385 CSolver * solver = (CSolver*) mng;
386 solver->clean_up_dbase();
389 EXTERN void SAT_GenClsAnd2(SAT_Manager mng,
394 CSolver * solver = (CSolver*) mng;
396 cls_gen.and2(*solver, a, b, o, gid);
399 EXTERN void SAT_GenClsAndN(SAT_Manager mng,
404 CSolver * solver = (CSolver*) mng;
406 cls_gen.and_n(*solver, inputs, num_inputs, o, gid);
409 EXTERN void SAT_GenClsOr2(SAT_Manager mng,
414 CSolver * solver = (CSolver*) mng;
416 cls_gen.or2(*solver, a, b, o, gid);
419 EXTERN void SAT_GenClsOrN(SAT_Manager mng,
424 CSolver * solver = (CSolver*) mng;
426 cls_gen.or_n(*solver, inputs, num_inputs, o, gid);
429 EXTERN void SAT_GenClsNand2(SAT_Manager mng,
434 CSolver * solver = (CSolver*) mng;
436 cls_gen.nand2(*solver, a, b, o, gid);
440 EXTERN void SAT_GenClsNandN(SAT_Manager mng,
445 CSolver * solver = (CSolver*) mng;
447 cls_gen.nand_n(*solver, inputs, num_inputs, o, gid);
451 EXTERN void SAT_GenClsNor2(SAT_Manager mng,
456 CSolver * solver = (CSolver*) mng;
458 cls_gen.nor2(*solver, a, b, o, gid);
462 EXTERN void SAT_GenClsNorN(SAT_Manager mng,
467 CSolver * solver = (CSolver*) mng;
469 cls_gen.nor_n(*solver, inputs, num_inputs, o, gid);
472 EXTERN void SAT_GenClsXor(SAT_Manager mng,
477 CSolver * solver = (CSolver*) mng;
479 cls_gen.xor2(*solver, a, b, o, gid);
482 EXTERN void SAT_GenClsNot(SAT_Manager mng,
486 CSolver * solver = (CSolver*) mng;
488 cls_gen.not1(*solver, a, o, gid);