zchaff64/zchaff_clsgen.h

   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 #ifndef __CLAUSE_GENERATOR__
  37 #define __CLAUSE_GENERATOR__
  38 #include "zchaff_solver.h"
  39
  40 class CClause_Gen {
  41   private:
  42     inline static int * ptr(vector<int>::iterator itr) {
  43       return &(*itr);
  44     }
  45     inline static int pos(int i) {
  46       return i;
  47     }
  48     inline static int neg(int i) {
  49       return i^0x1;
  50     }
  51
  52   public:
  53     static void and2(CSolver & solver, int a, int b, int o, int gid = 0) {
  54       // a*b=c <==> (a + o')( b + o')(a'+b'+o)
  55       vector <int> lits;
  56       lits.clear();
  57       lits.push_back(pos(a));
  58       lits.push_back(neg(o));
  59       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
  60       lits.clear();
  61       lits.push_back(pos(b));
  62       lits.push_back(neg(o));
  63       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
  64       lits.clear();
  65       lits.push_back(neg(a));
  66       lits.push_back(neg(b));
  67       lits.push_back(pos(o));
  68       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
  69     }
  70
  71     static void and_n(CSolver & solver, int * inputs, int num_input, int o,
  72                       int gid = 0) {
  73       vector <int> lits;
  74       int i;
  75       for (i = 0; i < num_input; ++i) {
  76         lits.clear();
  77         lits.push_back(pos(inputs[i]));
  78         lits.push_back(neg(o));
  79         solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
  80       }
  81       lits.clear();
  82       for (i = 0; i < num_input; ++i)
  83         lits.push_back(neg(inputs[i]));
  84       lits.push_back(pos(o));
  85       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
  86     }
  87
  88     static void or2(CSolver & solver, int a, int b, int o, int gid = 0) {
  89       // a+b=c <==> (a' + c)( b' + c)(a + b + c')
  90       vector <int> lits;
  91       lits.clear();
  92       lits.push_back(neg(a));
  93       lits.push_back(pos(o));
  94       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
  95       lits.clear();
  96       lits.push_back(neg(b));
  97       lits.push_back(pos(o));
  98       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
  99       lits.clear();
 100       lits.push_back(pos(a));
 101       lits.push_back(pos(b));
 102       lits.push_back(neg(o));
 103       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 104     }
 105
 106     static void or_n(CSolver & solver, int * inputs, int num_input, int o,
 107                      int gid = 0) {
 108       vector <int> lits;
 109       int i;
 110       for (i = 0; i < num_input; ++i) {
 111         lits.clear();
 112         lits.push_back(neg(inputs[i]));
 113         lits.push_back(pos(o));
 114         solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 115       }
 116       lits.clear();
 117       for (i = 0; i < num_input; ++i)
 118         lits.push_back(pos(inputs[i]));
 119       lits.push_back(neg(o));
 120       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 121     }
 122
 123     static void nand2(CSolver & solver, int a, int b, int o, int gid = 0) {
 124       // a Nand b = o <==> (a + o)( b + o)(a' + b' + o')
 125       vector <int> lits;
 126       lits.clear();
 127       lits.push_back(pos(a));
 128       lits.push_back(pos(o));
 129       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 130       lits.clear();
 131       lits.push_back(pos(b));
 132       lits.push_back(pos(o));
 133       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 134       lits.clear();
 135       lits.push_back(neg(a));
 136       lits.push_back(neg(b));
 137       lits.push_back(neg(o));
 138       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 139     }
 140
 141     static void nand_n(CSolver & solver, int * inputs, int num_input, int o,
 142                        int gid = 0) {
 143       vector <int> lits;
 144       int i;
 145       for (i = 0; i < num_input; ++i) {
 146         lits.clear();
 147         lits.push_back(pos(inputs[i]));
 148         lits.push_back(pos(o));
 149         solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 150       }
 151       lits.clear();
 152       for (i = 0; i < num_input; ++i)
 153         lits.push_back(neg(inputs[i]));
 154       lits.push_back(neg(o));
 155       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 156     }
 157
 158     static void nor2(CSolver & solver, int a, int b, int o, int gid = 0) {
 159       // a Nor b = o <==> (a' + o')( b' + o')(a + b + o)
 160       vector <int> lits;
 161       lits.clear();
 162       lits.push_back(neg(a));
 163       lits.push_back(neg(o));
 164       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 165       lits.clear();
 166       lits.push_back(neg(b));
 167       lits.push_back(neg(o));
 168       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 169       lits.clear();
 170       lits.push_back(pos(a));
 171       lits.push_back(pos(b));
 172       lits.push_back(pos(o));
 173       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 174     }
 175
 176     static void nor_n(CSolver & solver, int * inputs, int num_input, int o,
 177                int gid = 0) {
 178       vector <int> lits;
 179       int i;
 180       for (i = 0; i < num_input; ++i) {
 181         lits.clear();
 182         lits.push_back(neg(inputs[i]));
 183         lits.push_back(neg(o));
 184         solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 185       }
 186       lits.clear();
 187       for (i = 0; i < num_input; ++i)
 188         lits.push_back(pos(inputs[i]));
 189       lits.push_back(pos(o));
 190       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 191     }
 192
 193     static void xor2(CSolver & solver, int a, int b, int o, int gid = 0) {
 194       // a xor b = o <==> (a' + b' + o')
 195       //                  (a + b + o' )
 196       //                  (a' + b + o)
 197       //                         (a + b' + o)
 198       vector <int> lits;
 199       lits.clear();
 200       lits.push_back(neg(a));
 201       lits.push_back(neg(b));
 202       lits.push_back(neg(o));
 203       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 204       lits.clear();
 205       lits.push_back(pos(a));
 206       lits.push_back(pos(b));
 207       lits.push_back(neg(o));
 208       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 209       lits.clear();
 210       lits.push_back(neg(a));
 211       lits.push_back(pos(b));
 212       lits.push_back(pos(o));
 213       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 214       lits.clear();
 215       lits.push_back(pos(a));
 216       lits.push_back(neg(b));
 217       lits.push_back(pos(o));
 218       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 219     }
 220
 221     static void not1(CSolver & solver, int a, int o, int gid = 0) {
 222       // a' = o <==> (a' + o')( a + o)
 223       vector <int> lits;
 224       lits.clear();
 225       lits.push_back(neg(a));
 226       lits.push_back(neg(o));
 227       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 228       lits.clear();
 229       lits.push_back(pos(a));
 230       lits.push_back(pos(o));
 231       solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid);
 232     }
 233 };
 234 #endif