zchaff64/zchaff_wrapper.wrp

   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>
  42 using 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
  56 EXTERN SAT_Manager SAT_InitManager(void) {
  57   CSolver * solver = new CSolver;
  58   return (SAT_Manager)solver;
  59 }
  60
  61 EXTERN char * SAT_Version(SAT_Manager mng) {
  62   CSolver * solver = (CSolver*) mng;
  63   return solver->version();
  64 }
  65
  66 EXTERN void SAT_SetNumVariables(SAT_Manager mng, int n_var) {
  67   CSolver * solver = (CSolver*) mng;
  68   solver->set_variable_number(n_var);
  69 }
  70
  71 EXTERN void SAT_ReleaseManager(SAT_Manager mng) {
  72   CSolver * solver = (CSolver*) mng;
  73   delete solver;
  74 }
  75
  76 EXTERN int SAT_AddVariable(SAT_Manager mng) {
  77   CSolver * solver = (CSolver*) mng;
  78   int vid = solver->add_variable();
  79   return vid;
  80 }
  81
  82 EXTERN void  SAT_EnableVarBranch(SAT_Manager mng, int vid) {
  83   CSolver * solver = (CSolver*) mng;
  84   solver->mark_var_branchable(vid);
  85 }
  86
  87 EXTERN void SAT_DisableVarBranch(SAT_Manager mng, int vid) {
  88   CSolver * solver = (CSolver*) mng;
  89   solver->mark_var_unbranchable(vid);
  90 }
  91
  92 EXTERN void SAT_SetTimeLimit(SAT_Manager mng, float runtime) {
  93   CSolver * solver = (CSolver*) mng;
  94   solver->set_time_limit(runtime);
  95 }
  96
  97 EXTERN void SAT_SetMemLimit(SAT_Manager mng, int mem_limit) {
  98   CSolver * solver = (CSolver*) mng;
  99   solver->set_mem_limit(mem_limit);
 100 }
 101
 102 EXTERN 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
 110 EXTERN void SAT_DeleteClauseGroup(SAT_Manager   mng,
 111                                   int           gid) {
 112   CSolver * solver = (CSolver*) mng;
 113   solver->delete_clause_group(gid);
 114 }
 115
 116 EXTERN void SAT_Reset(SAT_Manager mng) {
 117   CSolver * solver = (CSolver*) mng;
 118   solver->reset();
 119 }
 120
 121 EXTERN 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
 129 EXTERN int SAT_AllocClauseGroupID(SAT_Manager mng) {
 130   CSolver * solver = (CSolver*) mng;
 131   int gid = solver->alloc_gid();
 132   return gid;
 133 }
 134
 135 EXTERN int SAT_GetGlobalGroupID(SAT_Manager mng) {
 136   return 0;
 137 }
 138
 139 EXTERN int SAT_GetVolatileGroupID(SAT_Manager mng) {
 140   return -1;
 141 }
 142
 143 EXTERN int SAT_Solve(SAT_Manager mng) {
 144   CSolver * solver = (CSolver*) mng;
 145   int result = solver->solve();
 146   return result;
 147 }
 148
 149 EXTERN 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
 156 EXTERN 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
 163 EXTERN void SAT_SetRandomness(SAT_Manager        mng,
 164                               int                n) {
 165   CSolver * solver = (CSolver*) mng;
 166   solver->set_randomness(n);
 167 }
 168
 169 EXTERN void SAT_SetRandSeed(SAT_Manager         mng,
 170                             int                 seed) {
 171   CSolver * solver = (CSolver*) mng;
 172   solver->set_random_seed(seed);
 173 }
 174
 175 EXTERN 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
 183 EXTERN int SAT_EstimateMemUsage(SAT_Manager mng) {
 184   CSolver * solver = (CSolver*) mng;
 185   int usage = solver->estimate_mem_usage();
 186   return usage;
 187 }
 188
 189 EXTERN float SAT_GetElapsedCPUTime(SAT_Manager mng) {
 190   CSolver * solver = (CSolver*) mng;
 191   float time = solver->elapsed_cpu_time();
 192   return time;
 193 }
 194
 195 EXTERN float SAT_GetCurrentCPUTime(SAT_Manager mng) {
 196   float time = get_cpu_time() / 1000.0;
 197   return time;
 198 }
 199
 200 EXTERN float SAT_GetCPUTime(SAT_Manager mng) {
 201   CSolver * solver = (CSolver*) mng;
 202   float time = solver->cpu_run_time();
 203   return time;
 204 }
 205
 206 EXTERN int SAT_NumLiterals(SAT_Manager mng) {
 207   CSolver * solver = (CSolver*) mng;
 208   int n = solver->num_literals();
 209   return n;
 210 }
 211
 212 EXTERN int SAT_NumClauses(SAT_Manager mng) {
 213   CSolver * solver = (CSolver*) mng;
 214   int n = solver->num_clauses();
 215   return n;
 216 }
 217
 218 EXTERN int SAT_NumVariables(SAT_Manager mng) {
 219   CSolver * solver = (CSolver*) mng;
 220   int n = solver->num_variables();
 221   return n;
 222 }
 223
 224 EXTERN int SAT_InitNumLiterals(SAT_Manager mng) {
 225   CSolver * solver = (CSolver*) mng;
 226   int n = solver->init_num_literals();
 227   return n;
 228 }
 229
 230 EXTERN int SAT_InitNumClauses(SAT_Manager mng) {
 231   CSolver * solver = (CSolver*) mng;
 232   int n = solver->init_num_clauses();
 233   return n;
 234 }
 235
 236 EXTERN long64 SAT_NumAddedLiterals(SAT_Manager mng) {
 237   CSolver * solver = (CSolver*) mng;
 238   long64 n = solver->num_added_literals();
 239   return n;
 240 }
 241
 242 EXTERN int SAT_NumAddedClauses(SAT_Manager mng) {
 243   CSolver * solver = (CSolver*) mng;
 244   int  n =  solver->num_added_clauses();
 245   return n;
 246 }
 247
 248 EXTERN int SAT_NumDeletedClauses(SAT_Manager mng) {
 249   CSolver * solver = (CSolver*) mng;
 250   int n = solver->num_deleted_clauses();
 251   return n;
 252 }
 253
 254 EXTERN int SAT_NumDelOrigCls(SAT_Manager mng) {
 255   CSolver * solver = (CSolver*) mng;
 256   int n = solver->num_del_orig_cls();
 257   return n;
 258 }
 259
 260 EXTERN long64 SAT_NumDeletedLiterals(SAT_Manager mng) {
 261   CSolver * solver = (CSolver*) mng;
 262   long64 n = solver->num_deleted_literals();
 263   return n;
 264 }
 265
 266 EXTERN int SAT_NumDecisions(SAT_Manager mng) {
 267   CSolver * solver = (CSolver*) mng;
 268   int n = solver->num_decisions();
 269   return n;
 270 }
 271
 272 EXTERN int SAT_NumDecisionsStackConf(SAT_Manager mng) {
 273   CSolver * solver = (CSolver*) mng;
 274   int n = solver->num_decisions_stack_conf();
 275   return n;
 276 }
 277
 278 EXTERN int SAT_NumDecisionsVsids(SAT_Manager mng) {
 279   CSolver * solver = (CSolver*) mng;
 280   int n = solver->num_decisions_vsids();
 281   return n;
 282 }
 283
 284 EXTERN int SAT_NumDecisionsShrinking(SAT_Manager mng) {
 285   CSolver * solver = (CSolver*) mng;
 286   int n = solver->num_decisions_shrinking();
 287   return n;
 288 }
 289
 290 EXTERN int SAT_NumShrinkings(SAT_Manager mng) {
 291   CSolver * solver = (CSolver*) mng;
 292   int n = solver->num_shrinkings();
 293   return n;
 294 }
 295
 296 EXTERN int SAT_Random_Seed(SAT_Manager mng) {
 297   CSolver * solver = (CSolver*) mng;
 298   int n = solver->random_seed();
 299   return n;
 300 }
 301
 302 EXTERN long64 SAT_NumImplications(SAT_Manager mng) {
 303   CSolver * solver = (CSolver*) mng;
 304   long64 n = solver->num_implications();
 305   return n;
 306 }
 307
 308 EXTERN int SAT_MaxDLevel(SAT_Manager mng) {
 309   CSolver * solver = (CSolver*) mng;
 310   int n = solver->max_dlevel();
 311   return n;
 312 }
 313
 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());
 318   return n;
 319 }
 320
 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) {
 325       return i;
 326     }
 327   return -1;
 328 }
 329
 330 EXTERN 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
 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);
 339   return r;
 340 }
 341
 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);
 345 }
 346
 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);
 350 }
 351
 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) {
 356       return i;
 357     }
 358   return -1;
 359 }
 360
 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();
 364   return n;
 365 }
 366
 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();
 371   }
 372 }
 373
 374 EXTERN void SAT_EnableConfClsDeletion(SAT_Manager mng) {
 375   CSolver * solver = (CSolver*) mng;
 376   solver->enable_cls_deletion(true);
 377 }
 378
 379 EXTERN void SAT_DisableConfClsDeletion(SAT_Manager mng) {
 380   CSolver * solver = (CSolver*) mng;
 381   solver->enable_cls_deletion(false);
 382 }
 383
 384 EXTERN void SAT_CleanUpDatabase(SAT_Manager mng) {
 385   CSolver * solver = (CSolver*) mng;
 386   solver->clean_up_dbase();
 387 }
 388
 389 EXTERN 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
 399 EXTERN 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
 409 EXTERN 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
 419 EXTERN 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
 429 EXTERN 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
 440 EXTERN 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
 451 EXTERN 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
 462 EXTERN 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
 472 EXTERN 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
 482 EXTERN 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 }