libs/ezsat/demo_cmp.cc

   1 /*
   2  *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
   3  *
   4  *  Copyright (C) 2013  Clifford Wolf <clifford@clifford.at>
   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 test_cmp(uint32_t a, uint32_t b)
  40 {
  41         ezMiniSAT sat;
  42
  43         printf("A = %10u (%10d)\n", a, int32_t(a));
  44         printf("B = %10u (%10d)\n", b, int32_t(b));
  45         printf("\n");
  46
  47         std::vector<int> va = sat.vec_var("a", 32);
  48         std::vector<int> vb = sat.vec_var("b", 32);
  49
  50         sat.vec_set_unsigned(va, a);
  51         sat.vec_set_unsigned(vb, b);
  52
  53 #define MONITOR_VARS \
  54         X(carry) X(overflow) X(sign) X(zero) \
  55         X(lt_signed) X(le_signed) X(ge_signed) X(gt_signed) \
  56         X(lt_unsigned) X(le_unsigned) X(ge_unsigned) X(gt_unsigned)
  57
  58 #define X(_n) int _n; bool _n ## _master;
  59         MONITOR_VARS
  60 #undef X
  61
  62         carry_master = ((uint64_t(a) - uint64_t(b)) >> 32) & 1;
  63         overflow_master = (int32_t(a) - int32_t(b)) != (int64_t(int32_t(a)) - int64_t(int32_t(b)));
  64         sign_master = ((a - b) >> 31) & 1;
  65         zero_master = a == b;
  66
  67         sat.vec_cmp(va, vb, carry, overflow, sign, zero);
  68
  69         lt_signed_master = int32_t(a) <  int32_t(b);
  70         le_signed_master = int32_t(a) <= int32_t(b);
  71         ge_signed_master = int32_t(a) >= int32_t(b);
  72         gt_signed_master = int32_t(a) >  int32_t(b);
  73
  74         lt_unsigned_master = a <  b;
  75         le_unsigned_master = a <= b;
  76         ge_unsigned_master = a >= b;
  77         gt_unsigned_master = a >  b;
  78
  79         lt_signed = sat.vec_lt_signed(va, vb);
  80         le_signed = sat.vec_le_signed(va, vb);
  81         ge_signed = sat.vec_ge_signed(va, vb);
  82         gt_signed = sat.vec_gt_signed(va, vb);
  83
  84         lt_unsigned = sat.vec_lt_unsigned(va, vb);
  85         le_unsigned = sat.vec_le_unsigned(va, vb);
  86         ge_unsigned = sat.vec_ge_unsigned(va, vb);
  87         gt_unsigned = sat.vec_gt_unsigned(va, vb);
  88
  89         std::vector<int> modelExpressions;
  90         std::vector<bool> modelValues, modelMaster;
  91         std::vector<std::string> modelNames;
  92
  93 #define X(_n) modelExpressions.push_back(_n); modelNames.push_back(#_n); modelMaster.push_back(_n ## _master);
  94         MONITOR_VARS
  95 #undef X
  96
  97         std::vector<int> add_ab = sat.vec_add(va, vb);
  98         std::vector<int> sub_ab = sat.vec_sub(va, vb);
  99         std::vector<int> sub_ba = sat.vec_sub(vb, va);
 100
 101         sat.vec_append(modelExpressions, add_ab);
 102         sat.vec_append(modelExpressions, sub_ab);
 103         sat.vec_append(modelExpressions, sub_ba);
 104
 105         if (!sat.solve(modelExpressions, modelValues)) {
 106                 fprintf(stderr, "SAT solver failed to find a model!\n");
 107                 abort();
 108         }
 109
 110         bool found_error = false;
 111
 112         for (size_t i = 0; i < modelMaster.size(); i++) {
 113                 if (modelMaster.at(i) != int(modelValues.at(i)))
 114                         found_error = true;
 115                 printf("%-20s %d%s\n", modelNames.at(i).c_str(), int(modelValues.at(i)),
 116                                 modelMaster.at(i) != modelValues.at(i) ? "   !!!" : "");
 117         }
 118         printf("\n");
 119
 120         uint32_t add_ab_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, add_ab);
 121         uint32_t sub_ab_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, sub_ab);
 122         uint32_t sub_ba_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, sub_ba);
 123
 124         printf("%-20s %10u %10u%s\n", "result(a+b)", add_ab_value, a+b, add_ab_value != a+b ? "   !!!" : "");
 125         printf("%-20s %10u %10u%s\n", "result(a-b)", sub_ab_value, a-b, sub_ab_value != a-b ? "   !!!" : "");
 126         printf("%-20s %10u %10u%s\n", "result(b-a)", sub_ba_value, b-a, sub_ba_value != b-a ? "   !!!" : "");
 127         printf("\n");
 128
 129         if (found_error || add_ab_value != a+b || sub_ab_value != a-b || sub_ba_value != b-a)
 130                 abort();
 131 }
 132
 133 int main()
 134 {
 135         printf("\n");
 136         for (int i = 0; i < 1024; i++) {
 137                 printf("************** %d **************\n\n", i);
 138                 uint32_t a = xorshift128();
 139                 uint32_t b = xorshift128();
 140                 if (xorshift128() % 16 == 0)
 141                         a = b;
 142                 test_cmp(a, b);
 143         }
 144         return 0;
 145 }
 146