demo_vec.cc File Reference

#include "ezminisat.h"
#include <assert.h>

Include dependency graph for demo_vec.cc:

Go to the source code of this file.

Macros
#define	INIT_X   123456789
#define	INIT_Y   362436069
#define	INIT_Z   521288629
#define	INIT_W   88675123

Functions
uint32_t	xorshift128 ()
void	xorshift128_sat (ezSAT &sat, std::vector< int > &x, std::vector< int > &y, std::vector< int > &z, std::vector< int > &w)
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)
int	main ()

Macro Definition Documentation

#define INIT_W   88675123

Definition at line 26 of file demo_vec.cc.

#define INIT_X   123456789

Definition at line 23 of file demo_vec.cc.

#define INIT_Y   362436069

Definition at line 24 of file demo_vec.cc.

#define INIT_Z   521288629

Definition at line 25 of file demo_vec.cc.

Function Documentation

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
	)

Definition at line 46 of file demo_vec.cc.

{
    ezMiniSAT sat;

    std::vector<int> vx = sat.vec_var("x", 32);
    std::vector<int> vy = sat.vec_var("y", 32);
    std::vector<int> vz = sat.vec_var("z", 32);
    std::vector<int> vw = sat.vec_var("w", 32);

    xorshift128_sat(sat, vx, vy, vz, vw);
    sat.vec_set_unsigned(vw, w1);

    xorshift128_sat(sat, vx, vy, vz, vw);
    sat.vec_set_unsigned(vw, w2);

    xorshift128_sat(sat, vx, vy, vz, vw);
    sat.vec_set_unsigned(vw, w3);

    xorshift128_sat(sat, vx, vy, vz, vw);
    sat.vec_set_unsigned(vw, w4);

    std::vector<int> modelExpressions;
    std::vector<bool> modelValues;

    sat.vec_append(modelExpressions, sat.vec_var("x", 32));
    sat.vec_append(modelExpressions, sat.vec_var("y", 32));
    sat.vec_append(modelExpressions, sat.vec_var("z", 32));
    sat.vec_append(modelExpressions, sat.vec_var("w", 32));

    // sat.printDIMACS(stdout);

    if (!sat.solve(modelExpressions, modelValues)) {
        fprintf(stderr, "SAT solver failed to find a model!\n");
        abort();
    }

    x = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("x", 32));
    y = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("y", 32));
    z = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("z", 32));
    w = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("w", 32));
}

Here is the call graph for this function:

Here is the caller graph for this function:

int main

(

)

Definition at line 88 of file demo_vec.cc.

{
    uint32_t w1 = xorshift128();
    uint32_t w2 = xorshift128();
    uint32_t w3 = xorshift128();
    uint32_t w4 = xorshift128();
    uint32_t x, y, z, w;

    printf("\n");

    find_xorshift128_init_state(x, y, z, w, w1, w2, w3, w4);

    printf("x = %9u (%s)\n", (unsigned int)x, x == INIT_X ? "ok" : "ERROR");
    printf("y = %9u (%s)\n", (unsigned int)y, y == INIT_Y ? "ok" : "ERROR");
    printf("z = %9u (%s)\n", (unsigned int)z, z == INIT_Z ? "ok" : "ERROR");
    printf("w = %9u (%s)\n", (unsigned int)w, w == INIT_W ? "ok" : "ERROR");

    if (x != INIT_X || y != INIT_Y || z != INIT_Z || w != INIT_W)
        abort();

    printf("\n");

    return 0;
}

Here is the call graph for this function:

uint32_t xorshift128

(

)

Definition at line 28 of file demo_vec.cc.

                       {
    static uint32_t x = INIT_X;
    static uint32_t y = INIT_Y;
    static uint32_t z = INIT_Z;
    static uint32_t w = INIT_W;
    uint32_t t = x ^ (x << 11);
    x = y; y = z; z = w;
    w ^= (w >> 19) ^ t ^ (t >> 8);
    return w;
}

Here is the caller graph for this function:

void xorshift128_sat	(	ezSAT &	sat,
		std::vector< int > &	x,
		std::vector< int > &	y,
		std::vector< int > &	z,
		std::vector< int > &	w
	)

Definition at line 39 of file demo_vec.cc.

{
    std::vector<int> t = sat.vec_xor(x, sat.vec_shl(x, 11));
    x = y; y = z; z = w;
    w = sat.vec_xor(sat.vec_xor(w, sat.vec_shr(w, 19)), sat.vec_xor(t, sat.vec_shr(t, 8)));
}

Here is the call graph for this function:

Here is the caller graph for this function: