libs/ezsat/ezsat.h

   1 /*
   2  *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
   3  *
   4  *  Copyright (C) 2013  Claire Xenia Wolf <claire@yosyshq.com>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #ifndef EZSAT_H
  21 #define EZSAT_H
  22
  23 #include <set>
  24 #include <map>
  25 #include <vector>
  26 #include <string>
  27 #include <stdio.h>
  28 #include <stdint.h>
  29
  30 class ezSAT
  31 {
  32         // each token (terminal or non-terminal) is represented by an integer number
  33         //
  34         // the zero token:
  35         // the number zero is not used as valid token number and is used to encode
  36         // unused parameters for the functions.
  37         //
  38         // positive numbers are literals, with 1 = CONST_TRUE and 2 = CONST_FALSE;
  39         //
  40         // negative numbers are non-literal expressions. each expression is represented
  41         // by an operator id and a list of expressions (literals or non-literals).
  42
  43 public:
  44         enum OpId {
  45                 OpNot, OpAnd, OpOr, OpXor, OpIFF, OpITE
  46         };
  47
  48         static const int CONST_TRUE;
  49         static const int CONST_FALSE;
  50
  51 private:
  52         bool flag_keep_cnf;
  53         bool flag_non_incremental;
  54
  55         bool non_incremental_solve_used_up;
  56
  57         std::map<std::string, int> literalsCache;
  58         std::vector<std::string> literals;
  59
  60         std::map<std::pair<OpId, std::vector<int>>, int> expressionsCache;
  61         std::vector<std::pair<OpId, std::vector<int>>> expressions;
  62
  63         bool cnfConsumed;
  64         int cnfVariableCount, cnfClausesCount;
  65         std::vector<int> cnfLiteralVariables, cnfExpressionVariables;
  66         std::vector<std::vector<int>> cnfClauses, cnfClausesBackup;
  67
  68         void add_clause(const std::vector<int> &args);
  69         void add_clause(const std::vector<int> &args, bool argsPolarity, int a = 0, int b = 0, int c = 0);
  70         void add_clause(int a, int b = 0, int c = 0);
  71
  72         int bind_cnf_not(const std::vector<int> &args);
  73         int bind_cnf_and(const std::vector<int> &args);
  74         int bind_cnf_or(const std::vector<int> &args);
  75
  76 protected:
  77         void preSolverCallback();
  78
  79 public:
  80         int solverTimeout;
  81         bool solverTimoutStatus;
  82
  83         ezSAT();
  84         virtual ~ezSAT();
  85
  86         unsigned int statehash;
  87         void addhash(unsigned int);
  88
  89         void keep_cnf() { flag_keep_cnf = true; }
  90         void non_incremental() { flag_non_incremental = true; }
  91
  92         bool mode_keep_cnf() const { return flag_keep_cnf; }
  93         bool mode_non_incremental() const { return flag_non_incremental; }
  94
  95         // manage expressions
  96
  97         int value(bool val);
  98         int literal();
  99         int literal(const std::string &name);
 100         int frozen_literal();
 101         int frozen_literal(const std::string &name);
 102         int expression(OpId op, int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0);
 103         int expression(OpId op, const std::vector<int> &args);
 104
 105         void lookup_literal(int id, std::string &name) const;
 106         const std::string &lookup_literal(int id) const;
 107
 108         void lookup_expression(int id, OpId &op, std::vector<int> &args) const;
 109         const std::vector<int> &lookup_expression(int id, OpId &op) const;
 110
 111         int parse_string(const std::string &text);
 112         std::string to_string(int id) const;
 113
 114         int numLiterals() const { return literals.size(); }
 115         int numExpressions() const { return expressions.size(); }
 116
 117         int eval(int id, const std::vector<int> &values) const;
 118
 119         // SAT solver interface
 120         // If you are planning on using the solver API (and not simply create a CNF) you must use a child class
 121         // of ezSAT that actually implements a solver backend, such as ezMiniSAT (see ezminisat.h).
 122
 123         virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
 124
 125         bool solve(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) {
 126                 return solver(modelExpressions, modelValues, assumptions);
 127         }
 128
 129         bool solve(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) {
 130                 std::vector<int> assumptions;
 131                 if (a != 0) assumptions.push_back(a);
 132                 if (b != 0) assumptions.push_back(b);
 133                 if (c != 0) assumptions.push_back(c);
 134                 if (d != 0) assumptions.push_back(d);
 135                 if (e != 0) assumptions.push_back(e);
 136                 if (f != 0) assumptions.push_back(f);
 137                 return solver(modelExpressions, modelValues, assumptions);
 138         }
 139
 140         bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) {
 141                 std::vector<int> assumptions, modelExpressions;
 142                 std::vector<bool> modelValues;
 143                 if (a != 0) assumptions.push_back(a);
 144                 if (b != 0) assumptions.push_back(b);
 145                 if (c != 0) assumptions.push_back(c);
 146                 if (d != 0) assumptions.push_back(d);
 147                 if (e != 0) assumptions.push_back(e);
 148                 if (f != 0) assumptions.push_back(f);
 149                 return solver(modelExpressions, modelValues, assumptions);
 150         }
 151
 152         void setSolverTimeout(int newTimeoutSeconds) {
 153                 solverTimeout = newTimeoutSeconds;
 154         }
 155
 156         bool getSolverTimoutStatus() {
 157                 return solverTimoutStatus;
 158         }
 159
 160         // manage CNF (usually only accessed by SAT solvers)
 161
 162         virtual void clear();
 163         virtual void freeze(int id);
 164         virtual bool eliminated(int idx);
 165         void assume(int id);
 166         void assume(int id, int context_id) { assume(OR(id, NOT(context_id))); }
 167         int bind(int id, bool auto_freeze = true);
 168         int bound(int id) const;
 169
 170         int numCnfVariables() const { return cnfVariableCount; }
 171         int numCnfClauses() const { return cnfClausesCount; }
 172         const std::vector<std::vector<int>> &cnf() const { return cnfClauses; }
 173
 174         void consumeCnf();
 175         void consumeCnf(std::vector<std::vector<int>> &cnf);
 176
 177         // use this function to get the full CNF in keep_cnf mode
 178         void getFullCnf(std::vector<std::vector<int>> &full_cnf) const;
 179
 180         std::string cnfLiteralInfo(int idx) const;
 181
 182         // simple helpers for build expressions easily
 183
 184         struct _V {
 185                 int id;
 186                 std::string name;
 187                 _V(int id) : id(id) { }
 188                 _V(const char *name) : id(0), name(name) { }
 189                 _V(const std::string &name) : id(0), name(name) { }
 190                 int get(ezSAT *that) {
 191                         if (name.empty())
 192                                 return id;
 193                         return that->frozen_literal(name);
 194                 }
 195         };
 196
 197         int VAR(_V a) {
 198                 return a.get(this);
 199         }
 200
 201         int NOT(_V a) {
 202                 return expression(OpNot, a.get(this));
 203         }
 204
 205         int AND(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) {
 206                 return expression(OpAnd, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this));
 207         }
 208
 209         int OR(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) {
 210                 return expression(OpOr, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this));
 211         }
 212
 213         int XOR(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) {
 214                 return expression(OpXor, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this));
 215         }
 216
 217         int IFF(_V a, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) {
 218                 return expression(OpIFF, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this));
 219         }
 220
 221         int ITE(_V a, _V b, _V c) {
 222                 return expression(OpITE, a.get(this), b.get(this), c.get(this));
 223         }
 224
 225         void SET(_V a, _V b) {
 226                 assume(IFF(a.get(this), b.get(this)));
 227         }
 228
 229         // simple helpers for building expressions with bit vectors
 230
 231         std::vector<int> vec_const(const std::vector<bool> &bits);
 232         std::vector<int> vec_const_signed(int64_t value, int numBits);
 233         std::vector<int> vec_const_unsigned(uint64_t value, int numBits);
 234         std::vector<int> vec_var(int numBits);
 235         std::vector<int> vec_var(std::string name, int numBits);
 236         std::vector<int> vec_cast(const std::vector<int> &vec1, int toBits, bool signExtend = false);
 237
 238         std::vector<int> vec_not(const std::vector<int> &vec1);
 239         std::vector<int> vec_and(const std::vector<int> &vec1, const std::vector<int> &vec2);
 240         std::vector<int> vec_or(const std::vector<int> &vec1, const std::vector<int> &vec2);
 241         std::vector<int> vec_xor(const std::vector<int> &vec1, const std::vector<int> &vec2);
 242
 243         std::vector<int> vec_iff(const std::vector<int> &vec1, const std::vector<int> &vec2);
 244         std::vector<int> vec_ite(const std::vector<int> &vec1, const std::vector<int> &vec2, const std::vector<int> &vec3);
 245         std::vector<int> vec_ite(int sel, const std::vector<int> &vec1, const std::vector<int> &vec2);
 246
 247         std::vector<int> vec_count(const std::vector<int> &vec, int numBits, bool clip = true);
 248         std::vector<int> vec_add(const std::vector<int> &vec1, const std::vector<int> &vec2);
 249         std::vector<int> vec_sub(const std::vector<int> &vec1, const std::vector<int> &vec2);
 250         std::vector<int> vec_neg(const std::vector<int> &vec);
 251
 252         void vec_cmp(const std::vector<int> &vec1, const std::vector<int> &vec2, int &carry, int &overflow, int &sign, int &zero);
 253
 254         int vec_lt_signed(const std::vector<int> &vec1, const std::vector<int> &vec2);
 255         int vec_le_signed(const std::vector<int> &vec1, const std::vector<int> &vec2);
 256         int vec_ge_signed(const std::vector<int> &vec1, const std::vector<int> &vec2);
 257         int vec_gt_signed(const std::vector<int> &vec1, const std::vector<int> &vec2);
 258
 259         int vec_lt_unsigned(const std::vector<int> &vec1, const std::vector<int> &vec2);
 260         int vec_le_unsigned(const std::vector<int> &vec1, const std::vector<int> &vec2);
 261         int vec_ge_unsigned(const std::vector<int> &vec1, const std::vector<int> &vec2);
 262         int vec_gt_unsigned(const std::vector<int> &vec1, const std::vector<int> &vec2);
 263
 264         int vec_eq(const std::vector<int> &vec1, const std::vector<int> &vec2);
 265         int vec_ne(const std::vector<int> &vec1, const std::vector<int> &vec2);
 266
 267         std::vector<int> vec_shl(const std::vector<int> &vec1, int shift, bool signExtend = false);
 268         std::vector<int> vec_srl(const std::vector<int> &vec1, int shift);
 269
 270         std::vector<int> vec_shr(const std::vector<int> &vec1, int shift, bool signExtend = false) { return vec_shl(vec1, -shift, signExtend); }
 271         std::vector<int> vec_srr(const std::vector<int> &vec1, int shift) { return vec_srl(vec1, -shift); }
 272
 273         std::vector<int> vec_shift(const std::vector<int> &vec1, int shift, int extend_left, int extend_right);
 274         std::vector<int> vec_shift_right(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right);
 275         std::vector<int> vec_shift_left(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right);
 276
 277         void vec_append(std::vector<int> &vec, const std::vector<int> &vec1) const;
 278         void vec_append_signed(std::vector<int> &vec, const std::vector<int> &vec1, int64_t value);
 279         void vec_append_unsigned(std::vector<int> &vec, const std::vector<int> &vec1, uint64_t value);
 280
 281         int64_t vec_model_get_signed(const std::vector<int> &modelExpressions, const std::vector<bool> &modelValues, const std::vector<int> &vec1) const;
 282         uint64_t vec_model_get_unsigned(const std::vector<int> &modelExpressions, const std::vector<bool> &modelValues, const std::vector<int> &vec1) const;
 283
 284         int vec_reduce_and(const std::vector<int> &vec1);
 285         int vec_reduce_or(const std::vector<int> &vec1);
 286
 287         void vec_set(const std::vector<int> &vec1, const std::vector<int> &vec2);
 288         void vec_set_signed(const std::vector<int> &vec1, int64_t value);
 289         void vec_set_unsigned(const std::vector<int> &vec1, uint64_t value);
 290
 291         // helpers for generating ezSATbit and ezSATvec objects
 292
 293         struct ezSATbit bit(_V a);
 294         struct ezSATvec vec(const std::vector<int> &vec);
 295
 296         // printing CNF and internal state
 297
 298         void printDIMACS(FILE *f, bool verbose = false) const;
 299         void printInternalState(FILE *f) const;
 300
 301         // more sophisticated constraints (designed to be used directly with assume(..))
 302
 303         int onehot(const std::vector<int> &vec, bool max_only = false);
 304         int manyhot(const std::vector<int> &vec, int min_hot, int max_hot = -1);
 305         int ordered(const std::vector<int> &vec1, const std::vector<int> &vec2, bool allow_equal = true);
 306 };
 307
 308 // helper classes for using operator overloading when generating complex expressions
 309
 310 struct ezSATbit
 311 {
 312         ezSAT &sat;
 313         int id;
 314
 315         ezSATbit(ezSAT &sat, ezSAT::_V a) : sat(sat), id(sat.VAR(a)) { }
 316
 317         ezSATbit operator ~() { return ezSATbit(sat, sat.NOT(id)); }
 318         ezSATbit operator &(const ezSATbit &other) { return ezSATbit(sat, sat.AND(id, other.id)); }
 319         ezSATbit operator |(const ezSATbit &other) { return ezSATbit(sat, sat.OR(id, other.id)); }
 320         ezSATbit operator ^(const ezSATbit &other) { return ezSATbit(sat, sat.XOR(id, other.id)); }
 321         ezSATbit operator ==(const ezSATbit &other) { return ezSATbit(sat, sat.IFF(id, other.id)); }
 322         ezSATbit operator !=(const ezSATbit &other) { return ezSATbit(sat, sat.NOT(sat.IFF(id, other.id))); }
 323
 324         operator int() const { return id; }
 325         operator ezSAT::_V() const { return ezSAT::_V(id); }
 326         operator std::vector<int>() const { return std::vector<int>(1, id); }
 327 };
 328
 329 struct ezSATvec
 330 {
 331         ezSAT &sat;
 332         std::vector<int> vec;
 333
 334         ezSATvec(ezSAT &sat, const std::vector<int> &vec) : sat(sat), vec(vec) { }
 335
 336         ezSATvec operator ~() { return ezSATvec(sat, sat.vec_not(vec)); }
 337         ezSATvec operator -() { return ezSATvec(sat, sat.vec_neg(vec)); }
 338
 339         ezSATvec operator &(const ezSATvec &other) { return ezSATvec(sat, sat.vec_and(vec, other.vec)); }
 340         ezSATvec operator |(const ezSATvec &other) { return ezSATvec(sat, sat.vec_or(vec, other.vec)); }
 341         ezSATvec operator ^(const ezSATvec &other) { return ezSATvec(sat, sat.vec_xor(vec, other.vec)); }
 342
 343         ezSATvec operator +(const ezSATvec &other) { return ezSATvec(sat, sat.vec_add(vec, other.vec)); }
 344         ezSATvec operator -(const ezSATvec &other) { return ezSATvec(sat, sat.vec_sub(vec, other.vec)); }
 345
 346         ezSATbit operator < (const ezSATvec &other) { return ezSATbit(sat, sat.vec_lt_unsigned(vec, other.vec)); }
 347         ezSATbit operator <=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_le_unsigned(vec, other.vec)); }
 348         ezSATbit operator ==(const ezSATvec &other) { return ezSATbit(sat, sat.vec_eq(vec, other.vec)); }
 349         ezSATbit operator !=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_ne(vec, other.vec)); }
 350         ezSATbit operator >=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_ge_unsigned(vec, other.vec)); }
 351         ezSATbit operator > (const ezSATvec &other) { return ezSATbit(sat, sat.vec_gt_unsigned(vec, other.vec)); }
 352
 353         ezSATvec operator <<(int shift) { return ezSATvec(sat, sat.vec_shl(vec, shift)); }
 354         ezSATvec operator >>(int shift) { return ezSATvec(sat, sat.vec_shr(vec, shift)); }
 355
 356         operator std::vector<int>() const { return vec; }
 357 };
 358
 359 #endif