testbench.cc File Reference

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

Include dependency graph for testbench.cc:

Go to the source code of this file.

Data Structures
struct	xorshift128

Macros
#define	CHECK(_expr1, _expr2)   check(#_expr1, _expr1, #_expr2, _expr2)

Functions
bool	test (ezSAT &sat, int assumption=0)
void	test_simple ()
void	test_xorshift32_try (ezSAT &sat, uint32_t input_pattern)
void	test_xorshift32 ()
void	check (const char *expr1_str, bool expr1, const char *expr2_str, bool expr2)
void	test_signed (int8_t a, int8_t b, int8_t c)
void	test_unsigned (uint8_t a, uint8_t b, uint8_t c)
void	test_count (uint32_t x)
void	test_arith ()
void	test_onehot ()
void	test_manyhot ()
void	test_ordered ()
int	main ()

Macro Definition Documentation

#define CHECK	(		_expr1,
			_expr2
	)		check(#_expr1, _expr1, #_expr2, _expr2)

Definition at line 150 of file testbench.cc.

Function Documentation

void check	(	const char *	expr1_str,
		bool	expr1,
		const char *	expr2_str,
		bool	expr2
	)

Definition at line 152 of file testbench.cc.

{
    if (expr1 == expr2) {
        printf("[ %s ] == [ %s ] .. ok (%s == %s)\n", expr1_str, expr2_str, expr1 ? "true" : "false", expr2 ? "true" : "false");
    } else {
        printf("[ %s ] != [ %s ] .. ERROR (%s != %s)\n", expr1_str, expr2_str, expr1 ? "true" : "false", expr2 ? "true" : "false");
        abort();
    }
}

int main

(

)

Definition at line 430 of file testbench.cc.

{
    test_simple();
    test_xorshift32();
    test_arith();
    test_onehot();
    test_manyhot();
    test_ordered();
    printf("Passed all tests.\n\n");
    return 0;
}

Here is the call graph for this function:

bool test	(	ezSAT &	sat,
		int	assumption = 0
	)

Definition at line 39 of file testbench.cc.

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

    for (int id = 1; id <= sat.numLiterals(); id++)
        if (sat.bound(id))
            modelExpressions.push_back(id);

    if (sat.solve(modelExpressions, modelValues, assumption)) {
        printf("satisfiable:");
        for (int i = 0; i < int(modelExpressions.size()); i++)
            printf(" %s=%d", sat.to_string(modelExpressions[i]).c_str(), int(modelValues[i]));
        printf("\n\n");
        return true;
    } else {
        printf("not satisfiable.\n\n");
        return false;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_arith

(

)

Definition at line 232 of file testbench.cc.

{
    printf("==== %s ====\n\n", __PRETTY_FUNCTION__);

    xorshift128 rng;

    for (int i = 0; i < 100; i++)
        test_signed(rng() % 19 - 10, rng() % 19 - 10, rng() % 19 - 10);

    for (int i = 0; i < 100; i++)
        test_unsigned(rng() % 10, rng() % 10, rng() % 10);

    test_count(0x00000000);
    test_count(0xffffffff);
    for (int i = 0; i < 30; i++)
        test_count(rng());

    printf("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_count

(

uint32_t

x

)

Definition at line 203 of file testbench.cc.

{
    ezMiniSAT sat;

    int count = 0;
    for (int i = 0; i < 32; i++)
        if (((x >> i) & 1) != 0)
            count++;

    printf("Testing bit counting using x=0x%08x (%d set bits) .. ", x, count);

    std::vector<int> v = sat.vec_const_unsigned(x, 32);

    std::vector<int> cv6 = sat.vec_const_unsigned(count, 6);
    std::vector<int> cv4 = sat.vec_const_unsigned(count <= 15 ? count : 15, 4);

    if (cv6 != sat.vec_count(v, 6, false)) {
        fprintf(stderr, "FAILED 6bit-no-clipping test!\n");
        abort();
    }
    
    if (cv4 != sat.vec_count(v, 4, true)) {
        fprintf(stderr, "FAILED 4bit-clipping test!\n");
        abort();
    }
    
    printf("ok.\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_manyhot

(

)

Definition at line 308 of file testbench.cc.

{
    printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
    ezMiniSAT ez;

    int a = ez.frozen_literal("a");
    int b = ez.frozen_literal("b");
    int c = ez.frozen_literal("c");
    int d = ez.frozen_literal("d");

    std::vector<int> abcd;
    abcd.push_back(a);
    abcd.push_back(b);
    abcd.push_back(c);
    abcd.push_back(d);

    ez.assume(ez.manyhot(abcd, 1, 2));

    int solution_counter = 0;
    while (1)
    {
        std::vector<bool> modelValues;
        bool ok = ez.solve(abcd, modelValues);

        if (!ok)
            break;

        printf("Solution: %d %d %d %d\n", int(modelValues[0]), int(modelValues[1]), int(modelValues[2]), int(modelValues[3]));

        int count_hot = 0;
        std::vector<int> sol;
        for (int i = 0; i < 4; i++) {
            if (modelValues[i])
                count_hot++;
            sol.push_back(modelValues[i] ? abcd[i] : ez.NOT(abcd[i]));
        }
        ez.assume(ez.NOT(ez.expression(ezSAT::OpAnd, sol)));

        if (count_hot != 1 && count_hot != 2) {
            fprintf(stderr, "Wrong number of hot bits!\n");
            abort();
        }

        solution_counter++;
    }

    if (solution_counter != 4 + 4*3/2) {
        fprintf(stderr, "Wrong number of one-hot solutions!\n");
        abort();
    }

    printf("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_onehot

(

)

Definition at line 254 of file testbench.cc.

{
    printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
    ezMiniSAT ez;

    int a = ez.frozen_literal("a");
    int b = ez.frozen_literal("b");
    int c = ez.frozen_literal("c");
    int d = ez.frozen_literal("d");

    std::vector<int> abcd;
    abcd.push_back(a);
    abcd.push_back(b);
    abcd.push_back(c);
    abcd.push_back(d);

    ez.assume(ez.onehot(abcd));

    int solution_counter = 0;
    while (1)
    {
        std::vector<bool> modelValues;
        bool ok = ez.solve(abcd, modelValues);

        if (!ok)
            break;

        printf("Solution: %d %d %d %d\n", int(modelValues[0]), int(modelValues[1]), int(modelValues[2]), int(modelValues[3]));

        int count_hot = 0;
        std::vector<int> sol;
        for (int i = 0; i < 4; i++) {
            if (modelValues[i])
                count_hot++;
            sol.push_back(modelValues[i] ? abcd[i] : ez.NOT(abcd[i]));
        }
        ez.assume(ez.NOT(ez.expression(ezSAT::OpAnd, sol)));

        if (count_hot != 1) {
            fprintf(stderr, "Wrong number of hot bits!\n");
            abort();
        }

        solution_counter++;
    }

    if (solution_counter != 4) {
        fprintf(stderr, "Wrong number of one-hot solutions!\n");
        abort();
    }

    printf("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_ordered

(

)

Definition at line 362 of file testbench.cc.

{
    printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
    ezMiniSAT ez;

    int a = ez.frozen_literal("a");
    int b = ez.frozen_literal("b");
    int c = ez.frozen_literal("c");

    int x = ez.frozen_literal("x");
    int y = ez.frozen_literal("y");
    int z = ez.frozen_literal("z");

    std::vector<int> abc;
    abc.push_back(a);
    abc.push_back(b);
    abc.push_back(c);

    std::vector<int> xyz;
    xyz.push_back(x);
    xyz.push_back(y);
    xyz.push_back(z);

    ez.assume(ez.ordered(abc, xyz));

    int solution_counter = 0;

    while (1)
    {
        std::vector<int> modelVariables;
        std::vector<bool> modelValues;

        modelVariables.push_back(a);
        modelVariables.push_back(b);
        modelVariables.push_back(c);

        modelVariables.push_back(x);
        modelVariables.push_back(y);
        modelVariables.push_back(z);

        bool ok = ez.solve(modelVariables, modelValues);

        if (!ok)
            break;

        printf("Solution: %d %d %d | %d %d %d\n",
                int(modelValues[0]), int(modelValues[1]), int(modelValues[2]),
                int(modelValues[3]), int(modelValues[4]), int(modelValues[5]));

        std::vector<int> sol;
        for (size_t i = 0; i < modelVariables.size(); i++)
            sol.push_back(modelValues[i] ? modelVariables[i] : ez.NOT(modelVariables[i]));
        ez.assume(ez.NOT(ez.expression(ezSAT::OpAnd, sol)));

        solution_counter++;
    }

    if (solution_counter != 8+7+6+5+4+3+2+1) {
        fprintf(stderr, "Wrong number of solutions!\n");
        abort();
    }

    printf("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_signed	(	int8_t	a,
		int8_t	b,
		int8_t	c
	)

Definition at line 162 of file testbench.cc.

{
    ezMiniSAT sat;

    std::vector<int> av = sat.vec_const_signed(a, 8);
    std::vector<int> bv = sat.vec_const_signed(b, 8);
    std::vector<int> cv = sat.vec_const_signed(c, 8);

    printf("Testing signed arithmetic using: a=%+d, b=%+d, c=%+d\n", int(a), int(b), int(c));

    CHECK(a <  b+c, sat.solve(sat.vec_lt_signed(av, sat.vec_add(bv, cv))));
    CHECK(a <= b-c, sat.solve(sat.vec_le_signed(av, sat.vec_sub(bv, cv))));

    CHECK(a >  b+c, sat.solve(sat.vec_gt_signed(av, sat.vec_add(bv, cv))));
    CHECK(a >= b-c, sat.solve(sat.vec_ge_signed(av, sat.vec_sub(bv, cv))));

    printf("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_simple

(

)

Definition at line 62 of file testbench.cc.

{
    printf("==== %s ====\n\n", __PRETTY_FUNCTION__);

    ezMiniSAT sat;
    sat.non_incremental();
    sat.assume(sat.OR("A", "B"));
    sat.assume(sat.NOT(sat.AND("A", "B")));
    test(sat);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_unsigned	(	uint8_t	a,
		uint8_t	b,
		uint8_t	c
	)

Definition at line 181 of file testbench.cc.

{
    ezMiniSAT sat;

    if (b < c)
        b ^= c, c ^= b, b ^= c;

    std::vector<int> av = sat.vec_const_unsigned(a, 8);
    std::vector<int> bv = sat.vec_const_unsigned(b, 8);
    std::vector<int> cv = sat.vec_const_unsigned(c, 8);

    printf("Testing unsigned arithmetic using: a=%d, b=%d, c=%d\n", int(a), int(b), int(c));

    CHECK(a <  b+c, sat.solve(sat.vec_lt_unsigned(av, sat.vec_add(bv, cv))));
    CHECK(a <= b-c, sat.solve(sat.vec_le_unsigned(av, sat.vec_sub(bv, cv))));

    CHECK(a >  b+c, sat.solve(sat.vec_gt_unsigned(av, sat.vec_add(bv, cv))));
    CHECK(a >= b-c, sat.solve(sat.vec_ge_unsigned(av, sat.vec_sub(bv, cv))));

    printf("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_xorshift32

(

)

Definition at line 120 of file testbench.cc.

{
    printf("==== %s ====\n\n", __PRETTY_FUNCTION__);

    ezMiniSAT sat;
    sat.keep_cnf();

    xorshift128 rng;

    std::vector<int> bits = sat.vec_var("i", 32);

    bits = sat.vec_xor(bits, sat.vec_shl(bits, 13));
    bits = sat.vec_xor(bits, sat.vec_shr(bits, 17));
    bits = sat.vec_xor(bits, sat.vec_shl(bits,  5));

    sat.vec_set(bits, sat.vec_var("o", 32));

    test_xorshift32_try(sat, 0);
    test_xorshift32_try(sat, 314159265);
    test_xorshift32_try(sat, rng());
    test_xorshift32_try(sat, rng());
    test_xorshift32_try(sat, rng());
    test_xorshift32_try(sat, rng());

    sat.printDIMACS(stdout, true);
    printf("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void test_xorshift32_try	(	ezSAT &	sat,
		uint32_t	input_pattern
	)

Definition at line 75 of file testbench.cc.

{
    uint32_t output_pattern = input_pattern;
    output_pattern ^= output_pattern << 13;
    output_pattern ^= output_pattern >> 17;
    output_pattern ^= output_pattern << 5;

    std::vector<int> modelExpressions;
    std::vector<int> forwardAssumptions, backwardAssumptions;
    std::vector<bool> forwardModel, backwardModel;

    sat.vec_append(modelExpressions, sat.vec_var("i", 32));
    sat.vec_append(modelExpressions, sat.vec_var("o", 32));

    sat.vec_append_unsigned(forwardAssumptions,  sat.vec_var("i", 32), input_pattern);
    sat.vec_append_unsigned(backwardAssumptions,  sat.vec_var("o", 32), output_pattern);

    if (!sat.solve(modelExpressions, backwardModel, backwardAssumptions)) {
        printf("backward solving failed!\n");
        abort();
    }

    if (!sat.solve(modelExpressions, forwardModel, forwardAssumptions)) {
        printf("forward solving failed!\n");
        abort();
    }

    printf("xorshift32 test with input pattern 0x%08x:\n", input_pattern);

    printf("forward  solution: input=0x%08x output=0x%08x\n",
            (unsigned int)sat.vec_model_get_unsigned(modelExpressions, forwardModel, sat.vec_var("i", 32)),
            (unsigned int)sat.vec_model_get_unsigned(modelExpressions, forwardModel, sat.vec_var("o", 32)));

    printf("backward solution: input=0x%08x output=0x%08x\n",
            (unsigned int)sat.vec_model_get_unsigned(modelExpressions, backwardModel, sat.vec_var("i", 32)),
            (unsigned int)sat.vec_model_get_unsigned(modelExpressions, backwardModel, sat.vec_var("o", 32)));

    if (forwardModel != backwardModel) {
        printf("forward and backward results are inconsistend!\n");
        abort();
    }

    printf("passed.\n\n");
}

Here is the call graph for this function:

Here is the caller graph for this function: