ezsat.cc File Reference

#include "ezsat.h"
#include <cmath>
#include <algorithm>
#include <cassert>
#include <string>
#include <stdlib.h>

Include dependency graph for ezsat.cc:

Go to the source code of this file.

Macros
#define	X(op)   case ezSAT::op: text += #op; break;

Functions
static std::string	my_int_to_string (int i)
static void	fulladder (ezSAT *that, int a, int b, int c, int &y, int &x)
static void	halfadder (ezSAT *that, int a, int b, int &y, int &x)
static int	my_clog2 (int x)
static std::string	expression2str (const std::pair< ezSAT::OpId, std::vector< int >> &data)

Macro Definition Documentation

#define X

(

op

)

case ezSAT::op: text += #op; break;

Function Documentation

static std::string expression2str ( const std::pair< ezSAT::OpId, std::vector< int >> &  data )

static

Definition at line 1242 of file ezsat.cc.

{
    std::string text;
    switch (data.first) {
#define X(op) case ezSAT::op: text += #op; break;
        X(OpNot)
        X(OpAnd)
        X(OpOr)
        X(OpXor)
        X(OpIFF)
        X(OpITE)
    default:
        abort();
#undef X
    }
    text += ":";
    for (auto it : data.second)
        text += " " + my_int_to_string(it);
    return text;
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void fulladder ( ezSAT *  that, int  a, int  b, int  c, int &  y, int &  x  )

static

Definition at line 765 of file ezsat.cc.

{
    int tmp = that->XOR(a, b);
    int new_x = that->XOR(tmp, c);
    int new_y = that->OR(that->AND(a, b), that->AND(c, tmp));
#if 0
    printf("FULLADD> a=%s, b=%s, c=%s, carry=%s, sum=%s\n", that->to_string(a).c_str(), that->to_string(b).c_str(),
            that->to_string(c).c_str(), that->to_string(new_y).c_str(), that->to_string(new_x).c_str());
#endif
    x = new_x, y = new_y;
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void halfadder ( ezSAT *  that, int  a, int  b, int &  y, int &  x  )

static

Definition at line 778 of file ezsat.cc.

{
    int new_x = that->XOR(a, b);
    int new_y = that->AND(a, b);
#if 0
    printf("HALFADD> a=%s, b=%s, carry=%s, sum=%s\n", that->to_string(a).c_str(), that->to_string(b).c_str(),
            that->to_string(new_y).c_str(), that->to_string(new_x).c_str());
#endif
    x = new_x, y = new_y;
}

Here is the call graph for this function:

Here is the caller graph for this function:

static int my_clog2 ( int  x )

static

Definition at line 1008 of file ezsat.cc.

{
    int result = 0;
    for (x--; x > 0; result++)
        x >>= 1;
    return result;
}

Here is the caller graph for this function:

static std::string my_int_to_string ( int  i )

static

Definition at line 32 of file ezsat.cc.

{
#ifdef __MINGW32__
    char buffer[64];
    snprintf(buffer, 64, "%d", i);
    return buffer;
#else
    return std::to_string(i);
#endif
}

Here is the caller graph for this function: