libs/ezsat/demo_vec.cc

   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 #include "ezminisat.h"
  21 #include <assert.h>
  22
  23 #define INIT_X 123456789
  24 #define INIT_Y 362436069
  25 #define INIT_Z 521288629
  26 #define INIT_W  88675123
  27
  28 uint32_t xorshift128() {
  29         static uint32_t x = INIT_X;
  30         static uint32_t y = INIT_Y;
  31         static uint32_t z = INIT_Z;
  32         static uint32_t w = INIT_W;
  33         uint32_t t = x ^ (x << 11);
  34         x = y; y = z; z = w;
  35         w ^= (w >> 19) ^ t ^ (t >> 8);
  36         return w;
  37 }
  38
  39 void xorshift128_sat(ezSAT &sat, std::vector<int> &x, std::vector<int> &y, std::vector<int> &z, std::vector<int> &w)
  40 {
  41         std::vector<int> t = sat.vec_xor(x, sat.vec_shl(x, 11));
  42         x = y; y = z; z = w;
  43         w = sat.vec_xor(sat.vec_xor(w, sat.vec_shr(w, 19)), sat.vec_xor(t, sat.vec_shr(t, 8)));
  44 }
  45
  46 void find_xorshift128_init_state(uint32_t &x, uint32_t &y, uint32_t &z, uint32_t &w, uint32_t w1, uint32_t w2, uint32_t w3, uint32_t w4)
  47 {
  48         ezMiniSAT sat;
  49
  50         std::vector<int> vx = sat.vec_var("x", 32);
  51         std::vector<int> vy = sat.vec_var("y", 32);
  52         std::vector<int> vz = sat.vec_var("z", 32);
  53         std::vector<int> vw = sat.vec_var("w", 32);
  54
  55         xorshift128_sat(sat, vx, vy, vz, vw);
  56         sat.vec_set_unsigned(vw, w1);
  57
  58         xorshift128_sat(sat, vx, vy, vz, vw);
  59         sat.vec_set_unsigned(vw, w2);
  60
  61         xorshift128_sat(sat, vx, vy, vz, vw);
  62         sat.vec_set_unsigned(vw, w3);
  63
  64         xorshift128_sat(sat, vx, vy, vz, vw);
  65         sat.vec_set_unsigned(vw, w4);
  66
  67         std::vector<int> modelExpressions;
  68         std::vector<bool> modelValues;
  69
  70         sat.vec_append(modelExpressions, sat.vec_var("x", 32));
  71         sat.vec_append(modelExpressions, sat.vec_var("y", 32));
  72         sat.vec_append(modelExpressions, sat.vec_var("z", 32));
  73         sat.vec_append(modelExpressions, sat.vec_var("w", 32));
  74
  75         // sat.printDIMACS(stdout);
  76
  77         if (!sat.solve(modelExpressions, modelValues)) {
  78                 fprintf(stderr, "SAT solver failed to find a model!\n");
  79                 abort();
  80         }
  81
  82         x = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("x", 32));
  83         y = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("y", 32));
  84         z = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("z", 32));
  85         w = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("w", 32));
  86 }
  87
  88 int main()
  89 {
  90         uint32_t w1 = xorshift128();
  91         uint32_t w2 = xorshift128();
  92         uint32_t w3 = xorshift128();
  93         uint32_t w4 = xorshift128();
  94         uint32_t x, y, z, w;
  95
  96         printf("\n");
  97
  98         find_xorshift128_init_state(x, y, z, w, w1, w2, w3, w4);
  99
 100         printf("x = %9u (%s)\n", (unsigned int)x, x == INIT_X ? "ok" : "ERROR");
 101         printf("y = %9u (%s)\n", (unsigned int)y, y == INIT_Y ? "ok" : "ERROR");
 102         printf("z = %9u (%s)\n", (unsigned int)z, z == INIT_Z ? "ok" : "ERROR");
 103         printf("w = %9u (%s)\n", (unsigned int)w, w == INIT_W ? "ok" : "ERROR");
 104
 105         if (x != INIT_X || y != INIT_Y || z != INIT_Z || w != INIT_W)
 106                 abort();
 107
 108         printf("\n");
 109
 110         return 0;
 111 }
 112