source: vis_dev/zchaff/zchaff_wrapper.wrp @ 14

Last change on this file since 14 was 10, checked in by cecile, 13 years ago

Zchaff
File size: 14.6 KB
RevLine 
[10]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:
5//
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.
18//
19//
20// --- This software and any associated documentation is provided "as is"
21//
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.
27//
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// ********************************************************************
35
36#include <fstream>
37#include <iostream>
38#include <vector>
39#include <queue>
40#include <set>
41#include <map>
42using namespace std;
43
44#include "zchaff_solver.h"
45#include "zchaff_clsgen.h"
46
47#ifndef SAT_Manager
48#define SAT_Manager void *
49#endif
50
51// =====================================================================
52// Following are wrapper functions for C/C++ callers.
53//
54// =====================================================================
55
56EXTERN SAT_Manager SAT_InitManager(void) {
57  CSolver * solver = new CSolver;
58  return (SAT_Manager)solver;
59}
60
61EXTERN const char * SAT_Version(SAT_Manager mng) {
62  CSolver * solver = (CSolver*) mng;
63  return solver->version();
64}
65
66EXTERN void SAT_SetNumVariables(SAT_Manager mng, int n_var) {
67  CSolver * solver = (CSolver*) mng;
68  solver->set_variable_number(n_var);
69}
70
71EXTERN void SAT_ReleaseManager(SAT_Manager mng) {
72  CSolver * solver = (CSolver*) mng;
73  delete solver;
74}
75
76EXTERN int SAT_AddVariable(SAT_Manager mng) {
77  CSolver * solver = (CSolver*) mng;
78  int vid = solver->add_variable();
79  return vid;
80}
81
82EXTERN void  SAT_EnableVarBranch(SAT_Manager mng, int vid) {
83  CSolver * solver = (CSolver*) mng;
84  solver->mark_var_branchable(vid);
85}
86
87EXTERN void SAT_DisableVarBranch(SAT_Manager mng, int vid) {
88  CSolver * solver = (CSolver*) mng;
89  solver->mark_var_unbranchable(vid);
90}
91
92EXTERN void SAT_SetTimeLimit(SAT_Manager mng, float runtime) {
93  CSolver * solver = (CSolver*) mng;
94  solver->set_time_limit(runtime);
95}
96
97EXTERN void SAT_SetMemLimit(SAT_Manager mng, int mem_limit) {
98  CSolver * solver = (CSolver*) mng;
99  solver->set_mem_limit(mem_limit);
100}
101
102EXTERN void SAT_AddClause(SAT_Manager           mng,
103                          int *                 clause_lits,
104                          int                   num_lits,
105                          int                   gid = 0) {
106  CSolver * solver = (CSolver*) mng;
107  solver->add_orig_clause(clause_lits, num_lits, gid);
108}
109
110EXTERN void SAT_DeleteClauseGroup(SAT_Manager   mng,
111                                  int           gid) {
112  CSolver * solver = (CSolver*) mng;
113  solver->delete_clause_group(gid);
114}
115
116EXTERN void SAT_Reset(SAT_Manager mng) {
117  CSolver * solver = (CSolver*) mng;
118  solver->reset();
119}
120
121EXTERN int SAT_MergeClauseGroup(SAT_Manager     mng,
122                                int             gid1,
123                                int             gid2) {
124  CSolver * solver = (CSolver*) mng;
125  int g = solver->merge_clause_group(gid1, gid2);
126  return g;
127}
128
129EXTERN int SAT_AllocClauseGroupID(SAT_Manager mng) {
130  CSolver * solver = (CSolver*) mng;
131  int gid = solver->alloc_gid();
132  return gid;
133}
134
135EXTERN int SAT_GetGlobalGroupID(SAT_Manager mng) {
136  return 0;
137}
138
139EXTERN int SAT_GetVolatileGroupID(SAT_Manager mng) {
140  return -1;
141}
142
143EXTERN int SAT_Solve(SAT_Manager mng) {
144  CSolver * solver = (CSolver*) mng;
145  int result = solver->solve();
146  return result;
147}
148
149EXTERN void SAT_AddHookFun(SAT_Manager          mng,
150                           void(*fun)(void *),
151                           int                  interval) {
152  CSolver * solver = (CSolver*) mng;
153  solver->add_hook(fun, interval);
154}
155
156EXTERN void SAT_MakeDecision(SAT_Manager        mng,
157                             int                vid,
158                             int                sign) {
159  CSolver * solver = (CSolver*) mng;
160  solver->make_decision(vid+vid+sign);
161}
162
163EXTERN void SAT_SetRandomness(SAT_Manager        mng,
164                              int                n) {
165  CSolver * solver = (CSolver*) mng;
166  solver->set_randomness(n);
167}
168
169EXTERN void SAT_SetRandSeed(SAT_Manager         mng,
170                            int                 seed) {
171  CSolver * solver = (CSolver*) mng;
172  solver->set_random_seed(seed);
173}
174
175EXTERN int SAT_GetVarAsgnment(SAT_Manager       mng,
176                              int               v_idx) {
177  CSolver * solver = (CSolver*) mng;
178  assert(v_idx > 0 && v_idx < (int) solver->variables()->size());
179  int v = solver->variable(v_idx).value();
180  return v;
181}
182
183EXTERN int SAT_EstimateMemUsage(SAT_Manager mng) {
184  CSolver * solver = (CSolver*) mng;
185  int usage = solver->estimate_mem_usage();
186  return usage;
187}
188
189EXTERN float SAT_GetElapsedCPUTime(SAT_Manager mng) {
190  CSolver * solver = (CSolver*) mng;
191  float time = solver->elapsed_cpu_time();
192  return time;
193}
194
195EXTERN float SAT_GetCurrentCPUTime(SAT_Manager mng) {
196  float time = get_cpu_time() / 1000.0;
197  return time;
198}
199
200EXTERN float SAT_GetCPUTime(SAT_Manager mng) {
201  CSolver * solver = (CSolver*) mng;
202  float time = solver->cpu_run_time();
203  return time;
204}
205
206EXTERN int SAT_NumLiterals(SAT_Manager mng) {
207  CSolver * solver = (CSolver*) mng;
208  int n = solver->num_literals();
209  return n;
210}
211
212EXTERN int SAT_NumClauses(SAT_Manager mng) {
213  CSolver * solver = (CSolver*) mng;
214  int n = solver->num_clauses();
215  return n;
216}
217
218EXTERN int SAT_NumVariables(SAT_Manager mng) {
219  CSolver * solver = (CSolver*) mng;
220  int n = solver->num_variables();
221  return n;
222}
223
224EXTERN int SAT_InitNumLiterals(SAT_Manager mng) {
225  CSolver * solver = (CSolver*) mng;
226  int n = solver->init_num_literals();
227  return n;
228}
229
230EXTERN int SAT_InitNumClauses(SAT_Manager mng) {
231  CSolver * solver = (CSolver*) mng;
232  int n = solver->init_num_clauses();
233  return n;
234}
235
236EXTERN long64 SAT_NumAddedLiterals(SAT_Manager mng) {
237  CSolver * solver = (CSolver*) mng;
238  long64 n = solver->num_added_literals();
239  return n;
240}
241
242EXTERN int SAT_NumAddedClauses(SAT_Manager mng) {
243  CSolver * solver = (CSolver*) mng;
244  int  n =  solver->num_added_clauses();
245  return n;
246}
247
248EXTERN int SAT_NumDeletedClauses(SAT_Manager mng) {
249  CSolver * solver = (CSolver*) mng;
250  int n = solver->num_deleted_clauses();
251  return n;
252}
253
254EXTERN int SAT_NumDelOrigCls(SAT_Manager mng) {
255  CSolver * solver = (CSolver*) mng;
256  int n = solver->num_del_orig_cls();
257  return n;
258}
259
260EXTERN long64 SAT_NumDeletedLiterals(SAT_Manager mng) {
261  CSolver * solver = (CSolver*) mng;
262  long64 n = solver->num_deleted_literals();
263  return n;
264}
265
266EXTERN int SAT_NumDecisions(SAT_Manager mng) {
267  CSolver * solver = (CSolver*) mng;
268  int n = solver->num_decisions();
269  return n;
270}
271
272EXTERN int SAT_NumDecisionsStackConf(SAT_Manager mng) {
273  CSolver * solver = (CSolver*) mng;
274  int n = solver->num_decisions_stack_conf();
275  return n;
276}
277
278EXTERN int SAT_NumDecisionsVsids(SAT_Manager mng) {
279  CSolver * solver = (CSolver*) mng;
280  int n = solver->num_decisions_vsids();
281  return n;
282}
283
284EXTERN int SAT_NumDecisionsShrinking(SAT_Manager mng) {
285  CSolver * solver = (CSolver*) mng;
286  int n = solver->num_decisions_shrinking();
287  return n;
288}
289
290EXTERN int SAT_NumShrinkings(SAT_Manager mng) {
291  CSolver * solver = (CSolver*) mng;
292  int n = solver->num_shrinkings();
293  return n;
294}
295
296EXTERN int SAT_Random_Seed(SAT_Manager mng) {
297  CSolver * solver = (CSolver*) mng;
298  int n = solver->random_seed();
299  return n;
300}
301
302EXTERN long64 SAT_NumImplications(SAT_Manager mng) {
303  CSolver * solver = (CSolver*) mng;
304  long64 n = solver->num_implications();
305  return n;
306}
307
308EXTERN int SAT_MaxDLevel(SAT_Manager mng) {
309  CSolver * solver = (CSolver*) mng;
310  int n = solver->max_dlevel();
311  return n;
312}
313
314EXTERN 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());
318  return n;
319}
320
321EXTERN 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) {
325      return i;
326    }
327  return -1;
328}
329
330EXTERN int SAT_GetClauseType(SAT_Manager mng, int cl_idx) {
331  CSolver * solver = (CSolver*) mng;
332  int type = solver->clause(cl_idx).status();
333  return type;
334}
335
336EXTERN 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);
339  return r;
340}
341
342EXTERN void SAT_ClearClauseGroupID(SAT_Manager mng, int cl_idx, int id) {
343  CSolver * solver = (CSolver*) mng;
344  solver->clause(cl_idx).clear_gid(id);
345}
346
347EXTERN void SAT_SetClauseGroupID(SAT_Manager mng, int cl_idx, int id) {
348  CSolver * solver = (CSolver*) mng;
349  solver->clause(cl_idx).set_gid(id);
350}
351
352EXTERN 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) {
356      return i;
357    }
358  return -1;
359}
360
361EXTERN int SAT_GetClauseNumLits(SAT_Manager mng, int cl_idx) {
362  CSolver * solver = (CSolver*) mng;
363  int n = solver->clause(cl_idx).num_lits();
364  return n;
365}
366
367EXTERN 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();
371  }
372}
373
374EXTERN void SAT_EnableConfClsDeletion(SAT_Manager mng) {
375  CSolver * solver = (CSolver*) mng;
376  solver->enable_cls_deletion(true);
377}
378
379EXTERN void SAT_DisableConfClsDeletion(SAT_Manager mng) {
380  CSolver * solver = (CSolver*) mng;
381  solver->enable_cls_deletion(false);
382}
383
384EXTERN void SAT_CleanUpDatabase(SAT_Manager mng) {
385  CSolver * solver = (CSolver*) mng;
386  solver->clean_up_dbase();
387}
388
389EXTERN void SAT_GenClsAnd2(SAT_Manager          mng,
390                           int                  a,
391                           int                  b,
392                           int                  o,
393                           int                  gid = 0) {
394  CSolver * solver = (CSolver*) mng;
395  CClause_Gen cls_gen;
396  cls_gen.and2(*solver, a, b, o, gid);
397}
398
399EXTERN void SAT_GenClsAndN(SAT_Manager          mng,
400                           int *                inputs,
401                           int                  num_inputs,
402                           int                  o,
403                           int                  gid = 0) {
404  CSolver * solver = (CSolver*) mng;
405  CClause_Gen cls_gen;
406  cls_gen.and_n(*solver, inputs, num_inputs, o, gid);
407}
408
409EXTERN void SAT_GenClsOr2(SAT_Manager           mng,
410                          int                   a,
411                          int                   b,
412                          int                   o,
413                          int                   gid = 0) {
414  CSolver * solver = (CSolver*) mng;
415  CClause_Gen cls_gen;
416  cls_gen.or2(*solver, a, b, o, gid);
417}
418
419EXTERN void SAT_GenClsOrN(SAT_Manager           mng,
420                          int *                 inputs,
421                          int                   num_inputs,
422                          int                   o,
423                          int                   gid = 0) {
424  CSolver * solver = (CSolver*) mng;
425  CClause_Gen cls_gen;
426  cls_gen.or_n(*solver, inputs, num_inputs, o, gid);
427}
428
429EXTERN void SAT_GenClsNand2(SAT_Manager         mng,
430                            int                 a,
431                            int                 b,
432                            int                 o,
433                            int                 gid = 0) {
434  CSolver * solver = (CSolver*) mng;
435  CClause_Gen cls_gen;
436  cls_gen.nand2(*solver, a, b, o, gid);
437}
438
439
440EXTERN void SAT_GenClsNandN(SAT_Manager         mng,
441                            int *               inputs,
442                            int                 num_inputs,
443                            int                 o,
444                            int                 gid = 0) {
445  CSolver * solver = (CSolver*) mng;
446  CClause_Gen cls_gen;
447  cls_gen.nand_n(*solver, inputs, num_inputs, o, gid);
448}
449
450
451EXTERN void SAT_GenClsNor2(SAT_Manager          mng,
452                           int                  a,
453                           int                  b,
454                           int                  o,
455                           int                  gid = 0) {
456  CSolver * solver = (CSolver*) mng;
457  CClause_Gen cls_gen;
458  cls_gen.nor2(*solver, a, b, o, gid);
459}
460
461
462EXTERN void SAT_GenClsNorN(SAT_Manager          mng,
463                           int *                inputs,
464                           int                  num_inputs,
465                           int                  o,
466                           int                  gid = 0) {
467  CSolver * solver = (CSolver*) mng;
468  CClause_Gen cls_gen;
469  cls_gen.nor_n(*solver, inputs, num_inputs, o, gid);
470}
471
472EXTERN void SAT_GenClsXor(SAT_Manager           mng,
473                          int                   a,
474                          int                   b,
475                          int                   o,
476                          int                   gid = 0) {
477  CSolver * solver = (CSolver*) mng;
478  CClause_Gen cls_gen;
479  cls_gen.xor2(*solver, a, b, o, gid);
480}
481
482EXTERN void SAT_GenClsNot(SAT_Manager           mng,
483                          int                   a,
484                          int                   o,
485                          int                   gid = 0) {
486  CSolver * solver = (CSolver*) mng;
487  CClause_Gen cls_gen;
488  cls_gen.not1(*solver, a, o, gid);
489}
Note: See TracBrowser for help on using the repository browser.