ezMiniSAT Class Reference

#include <ezminisat.h>

Inheritance diagram for ezMiniSAT:

Collaboration diagram for ezMiniSAT:

Public Types
enum	OpId {   OpNot, OpAnd, OpOr, OpXor,   OpIFF, OpITE }

Public Member Functions
	ezMiniSAT ()
virtual	~ezMiniSAT ()
virtual void	clear ()
virtual void	freeze (int id)
virtual bool	eliminated (int idx)
virtual bool	solver (const std::vector< int > &modelExpressions, std::vector< bool > &modelValues, const std::vector< int > &assumptions)
void	keep_cnf ()
void	non_incremental ()
bool	mode_keep_cnf () const
bool	mode_non_incremental () const
int	value (bool val)
int	literal ()
int	literal (const std::string &name)
int	frozen_literal ()
int	frozen_literal (const std::string &name)
int	expression (OpId op, int a=0, int b=0, int c=0, int d=0, int e=0, int f=0)
int	expression (OpId op, const std::vector< int > &args)
void	lookup_literal (int id, std::string &name) const
const std::string &	lookup_literal (int id) const
void	lookup_expression (int id, OpId &op, std::vector< int > &args) const
const std::vector< int > &	lookup_expression (int id, OpId &op) const
int	parse_string (const std::string &text)
std::string	to_string (int id) const
int	numLiterals () const
int	numExpressions () const
int	eval (int id, const std::vector< int > &values) const
bool	solve (const std::vector< int > &modelExpressions, std::vector< bool > &modelValues, const std::vector< int > &assumptions)
bool	solve (const std::vector< int > &modelExpressions, std::vector< bool > &modelValues, int a=0, int b=0, int c=0, int d=0, int e=0, int f=0)
bool	solve (int a=0, int b=0, int c=0, int d=0, int e=0, int f=0)
void	setSolverTimeout (int newTimeoutSeconds)
bool	getSolverTimoutStatus ()
void	assume (int id)
int	bind (int id, bool auto_freeze=true)
int	bound (int id) const
int	numCnfVariables () const
int	numCnfClauses () const
const std::vector< std::vector < int > > &	cnf () const
void	consumeCnf ()
void	consumeCnf (std::vector< std::vector< int >> &cnf)
void	getFullCnf (std::vector< std::vector< int >> &full_cnf) const
std::string	cnfLiteralInfo (int idx) const
int	VAR (_V a)
int	NOT (_V a)
int	AND (_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
int	OR (_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
int	XOR (_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
int	IFF (_V a, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
int	ITE (_V a, _V b, _V c)
void	SET (_V a, _V b)
std::vector< int >	vec_const (const std::vector< bool > &bits)
std::vector< int >	vec_const_signed (int64_t value, int numBits)
std::vector< int >	vec_const_unsigned (uint64_t value, int numBits)
std::vector< int >	vec_var (int numBits)
std::vector< int >	vec_var (std::string name, int numBits)
std::vector< int >	vec_cast (const std::vector< int > &vec1, int toBits, bool signExtend=false)
std::vector< int >	vec_not (const std::vector< int > &vec1)
std::vector< int >	vec_and (const std::vector< int > &vec1, const std::vector< int > &vec2)
std::vector< int >	vec_or (const std::vector< int > &vec1, const std::vector< int > &vec2)
std::vector< int >	vec_xor (const std::vector< int > &vec1, const std::vector< int > &vec2)
std::vector< int >	vec_iff (const std::vector< int > &vec1, const std::vector< int > &vec2)
std::vector< int >	vec_ite (const std::vector< int > &vec1, const std::vector< int > &vec2, const std::vector< int > &vec3)
std::vector< int >	vec_ite (int sel, const std::vector< int > &vec1, const std::vector< int > &vec2)
std::vector< int >	vec_count (const std::vector< int > &vec, int numBits, bool clip=true)
std::vector< int >	vec_add (const std::vector< int > &vec1, const std::vector< int > &vec2)
std::vector< int >	vec_sub (const std::vector< int > &vec1, const std::vector< int > &vec2)
std::vector< int >	vec_neg (const std::vector< int > &vec)
void	vec_cmp (const std::vector< int > &vec1, const std::vector< int > &vec2, int &carry, int &overflow, int &sign, int &zero)
int	vec_lt_signed (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_le_signed (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_ge_signed (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_gt_signed (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_lt_unsigned (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_le_unsigned (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_ge_unsigned (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_gt_unsigned (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_eq (const std::vector< int > &vec1, const std::vector< int > &vec2)
int	vec_ne (const std::vector< int > &vec1, const std::vector< int > &vec2)
std::vector< int >	vec_shl (const std::vector< int > &vec1, int shift, bool signExtend=false)
std::vector< int >	vec_srl (const std::vector< int > &vec1, int shift)
std::vector< int >	vec_shr (const std::vector< int > &vec1, int shift, bool signExtend=false)
std::vector< int >	vec_srr (const std::vector< int > &vec1, int shift)
std::vector< int >	vec_shift (const std::vector< int > &vec1, int shift, int extend_left, int extend_right)
std::vector< int >	vec_shift_right (const std::vector< int > &vec1, const std::vector< int > &vec2, bool vec2_signed, int extend_left, int extend_right)
std::vector< int >	vec_shift_left (const std::vector< int > &vec1, const std::vector< int > &vec2, bool vec2_signed, int extend_left, int extend_right)
void	vec_append (std::vector< int > &vec, const std::vector< int > &vec1) const
void	vec_append_signed (std::vector< int > &vec, const std::vector< int > &vec1, int64_t value)
void	vec_append_unsigned (std::vector< int > &vec, const std::vector< int > &vec1, uint64_t value)
int64_t	vec_model_get_signed (const std::vector< int > &modelExpressions, const std::vector< bool > &modelValues, const std::vector< int > &vec1) const
uint64_t	vec_model_get_unsigned (const std::vector< int > &modelExpressions, const std::vector< bool > &modelValues, const std::vector< int > &vec1) const
int	vec_reduce_and (const std::vector< int > &vec1)
int	vec_reduce_or (const std::vector< int > &vec1)
void	vec_set (const std::vector< int > &vec1, const std::vector< int > &vec2)
void	vec_set_signed (const std::vector< int > &vec1, int64_t value)
void	vec_set_unsigned (const std::vector< int > &vec1, uint64_t value)
struct ezSATbit	bit (_V a)
struct ezSATvec	vec (const std::vector< int > &vec)
void	printDIMACS (FILE *f, bool verbose=false) const
void	printInternalState (FILE *f) const
int	onehot (const std::vector< int > &vec, bool max_only=false)
int	manyhot (const std::vector< int > &vec, int min_hot, int max_hot=-1)
int	ordered (const std::vector< int > &vec1, const std::vector< int > &vec2, bool allow_equal=true)

Data Fields
int	solverTimeout
bool	solverTimoutStatus

Static Public Attributes
static const int	CONST_TRUE = 1
static const int	CONST_FALSE = 2

Protected Member Functions
void	preSolverCallback ()

Private Types
typedef Minisat::SimpSolver	Solver

Static Private Member Functions
static void	alarmHandler (int)

Private Attributes
Solver *	minisatSolver
std::vector< int >	minisatVars
bool	foundContradiction
std::set< int >	cnfFrozenVars

Static Private Attributes
static ezMiniSAT *	alarmHandlerThis = NULL
static clock_t	alarmHandlerTimeout = 0

Detailed Description

Definition at line 38 of file ezminisat.h.

Member Typedef Documentation

typedef Minisat::SimpSolver ezMiniSAT::Solver

private

Definition at line 42 of file ezminisat.h.

Member Enumeration Documentation

enum ezSAT::OpId

inherited

Enumerator
OpNot
OpAnd
OpOr
OpXor
OpIFF
OpITE

Definition at line 44 of file ezsat.h.

              {
        OpNot, OpAnd, OpOr, OpXor, OpIFF, OpITE
    };

Constructor & Destructor Documentation

ezMiniSAT::ezMiniSAT

(

)

Definition at line 38 of file ezminisat.cc.

                     : minisatSolver(NULL)
{
    minisatSolver = NULL;
    foundContradiction = false;

    freeze(CONST_TRUE);
    freeze(CONST_FALSE);
}

Here is the call graph for this function:

ezMiniSAT::~ezMiniSAT ( )

virtual

Definition at line 47 of file ezminisat.cc.

{
    if (minisatSolver != NULL)
        delete minisatSolver;
}

Member Function Documentation

void ezMiniSAT::alarmHandler ( int  )

staticprivate

Definition at line 87 of file ezminisat.cc.

{
    if (clock() > alarmHandlerTimeout) {
        alarmHandlerThis->minisatSolver->interrupt();
        alarmHandlerTimeout = 0;
    } else
        alarm(1);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::AND ( _V  a = 0, _V  b = 0, _V  c = 0, _V  d = 0, _V  e = 0, _V  f = 0  )

inlineinherited

Definition at line 201 of file ezsat.h.

                                                                        {
        return expression(OpAnd, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this));
    }

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::assume ( int  id )

inherited

Definition at line 388 of file ezsat.cc.

{
    if (id < 0)
    {
        assert(0 < -id && -id <= int(expressions.size()));
        cnfExpressionVariables.resize(expressions.size());

        if (cnfExpressionVariables[-id-1] == 0)
        {
            OpId op;
            std::vector<int> args;
            lookup_expression(id, op, args);

            if (op == OpNot) {
                int idx = bind(args[0]);
                cnfClauses.push_back(std::vector<int>(1, -idx));
                cnfClausesCount++;
                return;
            }
            if (op == OpOr) {
                std::vector<int> clause;
                for (int arg : args)
                    clause.push_back(bind(arg));
                cnfClauses.push_back(clause);
                cnfClausesCount++;
                return;
            }
            if (op == OpAnd) {
                for (int arg : args) {
                    cnfClauses.push_back(std::vector<int>(1, bind(arg)));
                    cnfClausesCount++;
                }
                return;
            }
        }
    }

    int idx = bind(id);
    cnfClauses.push_back(std::vector<int>(1, idx));
    cnfClausesCount++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::bind ( int  id, bool  auto_freeze = true  )

inherited

Definition at line 520 of file ezsat.cc.

{
    if (id >= 0) {
        assert(0 < id && id <= int(literals.size()));
        cnfLiteralVariables.resize(literals.size());
        if (eliminated(cnfLiteralVariables[id-1])) {
            fprintf(stderr, "ezSAT: Missing freeze on literal `%s'.\n", to_string(id).c_str());
            abort();
        }
        if (cnfLiteralVariables[id-1] == 0) {
            cnfLiteralVariables[id-1] = ++cnfVariableCount;
            if (id == CONST_TRUE)
                add_clause(+cnfLiteralVariables[id-1]);
            if (id == CONST_FALSE)
                add_clause(-cnfLiteralVariables[id-1]);
        }
        return cnfLiteralVariables[id-1];
    }

    assert(0 < -id && -id <= int(expressions.size()));
    cnfExpressionVariables.resize(expressions.size());

    if (eliminated(cnfExpressionVariables[-id-1]))
    {
        cnfExpressionVariables[-id-1] = 0;

        // this will recursively call bind(id). within the recursion
        // the cnf is pre-set to 0. an idx is allocated there, then it
        // is frozen, then it returns here with the new idx already set.
        if (auto_freeze)
            freeze(id);
    }

    if (cnfExpressionVariables[-id-1] == 0)
    {
        OpId op;
        std::vector<int> args;
        lookup_expression(id, op, args);
        int idx = 0;

        if (op == OpXor) {
            while (args.size() > 1) {
                std::vector<int> newArgs;
                for (int i = 0; i < int(args.size()); i += 2)
                    if (i+1 == int(args.size()))
                        newArgs.push_back(args[i]);
                    else
                        newArgs.push_back(OR(AND(args[i], NOT(args[i+1])), AND(NOT(args[i]), args[i+1])));
                args.swap(newArgs);
            }
            idx = bind(args.at(0), false);
            goto assign_idx;
        }

        if (op == OpIFF) {
            std::vector<int> invArgs;
            for (auto arg : args)
                invArgs.push_back(NOT(arg));
            idx = bind(OR(expression(OpAnd, args), expression(OpAnd, invArgs)), false);
            goto assign_idx;
        }

        if (op == OpITE) {
            idx = bind(OR(AND(args[0], args[1]), AND(NOT(args[0]), args[2])), false);
            goto assign_idx;
        }

        for (int i = 0; i < int(args.size()); i++)
            args[i] = bind(args[i], false);

        switch (op)
        {
            case OpNot: idx = bind_cnf_not(args); break;
            case OpAnd: idx = bind_cnf_and(args); break;
            case OpOr:  idx = bind_cnf_or(args);  break;
            default: abort();
        }

    assign_idx:
        assert(idx != 0);
        cnfExpressionVariables[-id-1] = idx;
    }

    return cnfExpressionVariables[-id-1];
}

Here is the call graph for this function:

Here is the caller graph for this function:

ezSATbit ezSAT::bit ( _V  a )

inherited

Definition at line 1178 of file ezsat.cc.

{
    return ezSATbit(*this, a);
}

Here is the caller graph for this function:

int ezSAT::bound ( int  id ) const

inherited

Definition at line 494 of file ezsat.cc.

{
    if (id > 0 && id <= int(cnfLiteralVariables.size()))
        return cnfLiteralVariables[id-1];
    if (-id > 0 && -id <= int(cnfExpressionVariables.size()))
        return cnfExpressionVariables[-id-1];
    return 0;
}

Here is the caller graph for this function:

void ezMiniSAT::clear ( )

virtual

Reimplemented from ezSAT.

Definition at line 53 of file ezminisat.cc.

{
    if (minisatSolver != NULL) {
        delete minisatSolver;
        minisatSolver = NULL;
    }
    foundContradiction = false;
    minisatVars.clear();
#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
    cnfFrozenVars.clear();
#endif
    ezSAT::clear();
}

Here is the call graph for this function:

const std::vector<std::vector<int> >& ezSAT::cnf ( ) const

inlineinherited

Definition at line 168 of file ezsat.h.

{ return cnfClauses; }

Here is the caller graph for this function:

std::string ezSAT::cnfLiteralInfo ( int  idx ) const

inherited

Definition at line 503 of file ezsat.cc.

{
    for (int i = 0; i < int(cnfLiteralVariables.size()); i++) {
        if (cnfLiteralVariables[i] == idx)
            return to_string(i+1);
        if (cnfLiteralVariables[i] == -idx)
            return "NOT " + to_string(i+1);
    }
    for (int i = 0; i < int(cnfExpressionVariables.size()); i++) {
        if (cnfExpressionVariables[i] == idx)
            return to_string(-i-1);
        if (cnfExpressionVariables[i] == -idx)
            return "NOT " + to_string(-i-1);
    }
    return "<unnamed>";
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::consumeCnf ( )

inherited

Definition at line 606 of file ezsat.cc.

{
    if (mode_keep_cnf())
        cnfClausesBackup.insert(cnfClausesBackup.end(), cnfClauses.begin(), cnfClauses.end());
    else
        cnfConsumed = true;
    cnfClauses.clear();
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::consumeCnf ( std::vector< std::vector< int >> &  cnf )

inherited

Definition at line 615 of file ezsat.cc.

{
    if (mode_keep_cnf())
        cnfClausesBackup.insert(cnfClausesBackup.end(), cnfClauses.begin(), cnfClauses.end());
    else
        cnfConsumed = true;
    cnf.swap(cnfClauses);
    cnfClauses.clear();
}

Here is the call graph for this function:

virtual bool ezMiniSAT::eliminated ( int  idx )

virtual

Reimplemented from ezSAT.

int ezSAT::eval ( int  id, const std::vector< int > &  values  ) const

inherited

Definition at line 293 of file ezsat.cc.

{
    if (id > 0) {
        if (id <= int(values.size()) && (values[id-1] == CONST_TRUE || values[id-1] == CONST_FALSE || values[id-1] == 0))
            return values[id-1];
        return 0;
    }

    OpId op;
    const std::vector<int> &args = lookup_expression(id, op);
    int a, b;

    switch (op)
    {
    case OpNot:
        assert(args.size() == 1);
        a = eval(args[0], values);
        if (a == CONST_TRUE)
            return CONST_FALSE;
        if (a == CONST_FALSE)
            return CONST_TRUE;
        return 0;
    case OpAnd:
        a = CONST_TRUE;
        for (auto arg : args) {
            b = eval(arg, values);
            if (b != CONST_TRUE && b != CONST_FALSE)
                a = 0;
            if (b == CONST_FALSE)
                return CONST_FALSE;
        }
        return a;
    case OpOr:
        a = CONST_FALSE;
        for (auto arg : args) {
            b = eval(arg, values);
            if (b != CONST_TRUE && b != CONST_FALSE)
                a = 0;
            if (b == CONST_TRUE)
                return CONST_TRUE;
        }
        return a;
    case OpXor:
        a = CONST_FALSE;
        for (auto arg : args) {
            b = eval(arg, values);
            if (b != CONST_TRUE && b != CONST_FALSE)
                return 0;
            if (b == CONST_TRUE)
                a = a == CONST_TRUE ? CONST_FALSE : CONST_TRUE;
        }
        return a;
    case OpIFF:
        assert(args.size() > 0);
        a = eval(args[0], values);
        for (auto arg : args) {
            b = eval(arg, values);
            if (b != CONST_TRUE && b != CONST_FALSE)
                return 0;
            if (b != a)
                return CONST_FALSE;
        }
        return CONST_TRUE;
    case OpITE:
        assert(args.size() == 3);
        a = eval(args[0], values);
        if (a == CONST_TRUE)
            return eval(args[1], values);
        if (a == CONST_FALSE)
            return eval(args[2], values);
        return 0;
    default:
        abort();
    }
}

Here is the call graph for this function:

int ezSAT::expression ( OpId  op, int  a = 0, int  b = 0, int  c = 0, int  d = 0, int  e = 0, int  f = 0  )

inherited

Definition at line 102 of file ezsat.cc.

{
    std::vector<int> args(6);
    args[0] = a, args[1] = b, args[2] = c;
    args[3] = d, args[4] = e, args[5] = f;
    return expression(op, args);
}

Here is the caller graph for this function:

int ezSAT::expression ( OpId  op, const std::vector< int > &  args  )

inherited

Definition at line 110 of file ezsat.cc.

{
    std::vector<int> myArgs;
    myArgs.reserve(args.size());
    bool xorRemovedOddTrues = false;

    for (auto arg : args)
    {
        if (arg == 0)
            continue;
        if (op == OpAnd && arg == CONST_TRUE)
            continue;
        if ((op == OpOr || op == OpXor) && arg == CONST_FALSE)
            continue;
        if (op == OpXor && arg == CONST_TRUE) {
            xorRemovedOddTrues = !xorRemovedOddTrues;
            continue;
        }
        myArgs.push_back(arg);
    }

    if (myArgs.size() > 0 && (op == OpAnd || op == OpOr || op == OpXor || op == OpIFF)) {
        std::sort(myArgs.begin(), myArgs.end());
        int j = 0;
        for (int i = 1; i < int(myArgs.size()); i++)
            if (j < 0 || myArgs[j] != myArgs[i])
                myArgs[++j] = myArgs[i];
            else if (op == OpXor)
                j--;
        myArgs.resize(j+1);
    }

    switch (op)
    {
    case OpNot:
        assert(myArgs.size() == 1);
        if (myArgs[0] == CONST_TRUE)
            return CONST_FALSE;
        if (myArgs[0] == CONST_FALSE)
            return CONST_TRUE;
        break;

    case OpAnd:
        if (myArgs.size() == 0)
            return CONST_TRUE;
        if (myArgs.size() == 1)
            return myArgs[0];
        break;

    case OpOr:
        if (myArgs.size() == 0)
            return CONST_FALSE;
        if (myArgs.size() == 1)
            return myArgs[0];
        break;

    case OpXor:
        if (myArgs.size() == 0)
            return xorRemovedOddTrues ? CONST_TRUE : CONST_FALSE;
        if (myArgs.size() == 1)
            return xorRemovedOddTrues ? NOT(myArgs[0]) : myArgs[0];
        break;

    case OpIFF:
        assert(myArgs.size() >= 1);
        if (myArgs.size() == 1)
            return CONST_TRUE;
        // FIXME: Add proper const folding
        break;

    case OpITE:
        assert(myArgs.size() == 3);
        if (myArgs[0] == CONST_TRUE)
            return myArgs[1];
        if (myArgs[0] == CONST_FALSE)
            return myArgs[2];
        break;

    default:
        abort();
    }

    std::pair<OpId, std::vector<int>> myExpr(op, myArgs);
    int id = 0;

    if (expressionsCache.count(myExpr) > 0) {
        id = expressionsCache.at(myExpr);
    } else {
        id = -(int(expressions.size()) + 1);
        expressionsCache[myExpr] = id;
        expressions.push_back(myExpr);
    }

    return xorRemovedOddTrues ? NOT(id) : id;
}

Here is the call graph for this function:

virtual void ezMiniSAT::freeze ( int  id )

virtual

Reimplemented from ezSAT.

Here is the caller graph for this function:

int ezSAT::frozen_literal ( )

inherited

Definition at line 88 of file ezsat.cc.

{
    int id = literal();
    freeze(id);
    return id;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::frozen_literal ( const std::string &  name )

inherited

Definition at line 95 of file ezsat.cc.

{
    int id = literal(name);
    freeze(id);
    return id;
}

Here is the call graph for this function:

void ezSAT::getFullCnf ( std::vector< std::vector< int >> &  full_cnf ) const

inherited

Definition at line 625 of file ezsat.cc.

{
    assert(full_cnf.empty());
    full_cnf.insert(full_cnf.end(), cnfClausesBackup.begin(), cnfClausesBackup.end());
    full_cnf.insert(full_cnf.end(), cnfClauses.begin(), cnfClauses.end());
}

Here is the caller graph for this function:

bool ezSAT::getSolverTimoutStatus ( )

inlineinherited

Definition at line 153 of file ezsat.h.

                                 {
        return solverTimoutStatus;
    }

int ezSAT::IFF ( _V  a, _V  b = 0, _V  c = 0, _V  d = 0, _V  e = 0, _V  f = 0  )

inlineinherited

Definition at line 213 of file ezsat.h.

                                                                    {
        return expression(OpIFF, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this));
    }

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::ITE ( _V  a, _V  b, _V  c  )

inlineinherited

Definition at line 217 of file ezsat.h.

                              {
        return expression(OpITE, a.get(this), b.get(this), c.get(this));
    }

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::keep_cnf ( )

inlineinherited

Definition at line 86 of file ezsat.h.

{ flag_keep_cnf = true; }

Here is the caller graph for this function:

int ezSAT::literal ( )

inherited

Definition at line 73 of file ezsat.cc.

{
    literals.push_back(std::string());
    return literals.size();
}

Here is the caller graph for this function:

int ezSAT::literal ( const std::string &  name )

inherited

Definition at line 79 of file ezsat.cc.

{
    if (literalsCache.count(name) == 0) {
        literals.push_back(name);
        literalsCache[name] = literals.size();
    }
    return literalsCache.at(name);
}

void ezSAT::lookup_expression ( int  id, OpId &  op, std::vector< int > &  args  ) const

inherited

Definition at line 218 of file ezsat.cc.

{
    assert(0 < -id && -id <= int(expressions.size()));
    op = expressions[-id - 1].first;
    args = expressions[-id - 1].second;
}

Here is the caller graph for this function:

const std::vector< int > & ezSAT::lookup_expression ( int  id, OpId &  op  ) const

inherited

Definition at line 225 of file ezsat.cc.

{
    assert(0 < -id && -id <= int(expressions.size()));
    op = expressions[-id - 1].first;
    return expressions[-id - 1].second;
}

void ezSAT::lookup_literal ( int  id, std::string &  name  ) const

inherited

Definition at line 206 of file ezsat.cc.

{
    assert(0 < id && id <= int(literals.size()));
    name = literals[id - 1];
}

Here is the caller graph for this function:

const std::string & ezSAT::lookup_literal ( int  id ) const

inherited

Definition at line 212 of file ezsat.cc.

{
    assert(0 < id && id <= int(literals.size()));
    return literals[id - 1];
}

int ezSAT::manyhot ( const std::vector< int > &  vec, int  min_hot, int  max_hot = -1  )

inherited

Definition at line 1333 of file ezsat.cc.

{
    // many-hot encoding using a simple sorting network

    if (max_hot < 0)
        max_hot = min_hot;
    
    std::vector<int> formula;
    int M = max_hot+1, N = vec.size();
    std::map<std::pair<int,int>, int> x;

    for (int i = -1; i < N; i++)
    for (int j = -1; j < M; j++)
        x[std::pair<int,int>(i,j)] = j < 0 ? CONST_TRUE : i < 0 ? CONST_FALSE : literal();

    for (int i = 0; i < N; i++)
    for (int j = 0; j < M; j++) {
        formula.push_back(OR(NOT(vec[i]), x[std::pair<int,int>(i-1,j-1)], NOT(x[std::pair<int,int>(i,j)])));
        formula.push_back(OR(NOT(vec[i]), NOT(x[std::pair<int,int>(i-1,j-1)]), x[std::pair<int,int>(i,j)]));
        formula.push_back(OR(vec[i], x[std::pair<int,int>(i-1,j)], NOT(x[std::pair<int,int>(i,j)])));
        formula.push_back(OR(vec[i], NOT(x[std::pair<int,int>(i-1,j)]), x[std::pair<int,int>(i,j)]));
#if 0
        // explicit resolution clauses -- in tests it was better to let the sat solver figure those out
        formula.push_back(OR(NOT(x[std::pair<int,int>(i-1,j-1)]), NOT(x[std::pair<int,int>(i-1,j)]), x[std::pair<int,int>(i,j)]));
        formula.push_back(OR(x[std::pair<int,int>(i-1,j-1)], x[std::pair<int,int>(i-1,j)], NOT(x[std::pair<int,int>(i,j)])));
#endif
    }

    for (int j = 0; j < M; j++) {
        if (j+1 <= min_hot)
            formula.push_back(x[std::pair<int,int>(N-1,j)]);
        else if (j+1 > max_hot)
            formula.push_back(NOT(x[std::pair<int,int>(N-1,j)]));
    }

    return expression(OpAnd, formula);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool ezSAT::mode_keep_cnf ( ) const

inlineinherited

Definition at line 89 of file ezsat.h.

{ return flag_keep_cnf; }

Here is the caller graph for this function:

bool ezSAT::mode_non_incremental ( ) const

inlineinherited

Definition at line 90 of file ezsat.h.

{ return flag_non_incremental; }

Here is the caller graph for this function:

void ezSAT::non_incremental ( )

inlineinherited

Definition at line 87 of file ezsat.h.

{ flag_non_incremental = true; }

Here is the caller graph for this function:

int ezSAT::NOT ( _V  a )

inlineinherited

Definition at line 197 of file ezsat.h.

                  {
        return expression(OpNot, a.get(this));
    }

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::numCnfClauses ( ) const

inlineinherited

Definition at line 167 of file ezsat.h.

{ return cnfClausesCount; }

Here is the caller graph for this function:

int ezSAT::numCnfVariables ( ) const

inlineinherited

Definition at line 166 of file ezsat.h.

{ return cnfVariableCount; }

Here is the caller graph for this function:

int ezSAT::numExpressions ( ) const

inlineinherited

Definition at line 112 of file ezsat.h.

{ return expressions.size(); }

int ezSAT::numLiterals ( ) const

inlineinherited

Definition at line 111 of file ezsat.h.

{ return literals.size(); }

Here is the caller graph for this function:

int ezSAT::onehot ( const std::vector< int > &  vec, bool  max_only = false  )

inherited

Definition at line 1303 of file ezsat.cc.

{
    // Mixed one-hot/binary encoding as described by Claessen in Sec. 4.2 of
    // "Successful SAT Encoding Techniques. Magnus Bjiirk. 25th July 2009".
    // http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf

    std::vector<int> formula;

    // add at-leat-one constraint
    if (max_only == false)
        formula.push_back(expression(OpOr, vec));

    // create binary vector
    int num_bits = ceil(log2(vec.size()));
    std::vector<int> bits;
    for (int k = 0; k < num_bits; k++)
        bits.push_back(literal());

    // add at-most-one clauses using binary encoding
    for (size_t i = 0; i < vec.size(); i++)
        for (int k = 0; k < num_bits; k++) {
            std::vector<int> clause;
            clause.push_back(NOT(vec[i]));
            clause.push_back((i & (1 << k)) != 0 ? bits[k] : NOT(bits[k]));
            formula.push_back(expression(OpOr, clause));
        }

    return expression(OpAnd, formula);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::OR ( _V  a = 0, _V  b = 0, _V  c = 0, _V  d = 0, _V  e = 0, _V  f = 0  )

inlineinherited

Definition at line 205 of file ezsat.h.

                                                                       {
        return expression(OpOr, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this));
    }

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::ordered ( const std::vector< int > &  vec1, const std::vector< int > &  vec2, bool  allow_equal = true  )

inherited

Definition at line 1371 of file ezsat.cc.

{
    std::vector<int> formula;
    int last_x = CONST_FALSE;

    assert(vec1.size() == vec2.size());
    for (size_t i = 0; i < vec1.size(); i++)
    {
        int a = vec1[i], b = vec2[i];
        formula.push_back(OR(NOT(a), b, last_x));

        int next_x = i+1 < vec1.size() ? literal() : allow_equal ? CONST_FALSE : CONST_TRUE;
        formula.push_back(OR(a, b, last_x, NOT(next_x)));
        formula.push_back(OR(NOT(a), NOT(b), last_x, NOT(next_x)));
        last_x = next_x;
    }

    return expression(OpAnd, formula);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::parse_string ( const std::string &  text )

inherited

Definition at line 232 of file ezsat.cc.

{
    abort();
}

void ezSAT::preSolverCallback ( )

protectedinherited

Definition at line 632 of file ezsat.cc.

{
    assert(!non_incremental_solve_used_up);
    if (mode_non_incremental())
        non_incremental_solve_used_up = true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::printDIMACS ( FILE *  f, bool  verbose = false  ) const

inherited

Definition at line 1188 of file ezsat.cc.

{
    if (cnfConsumed) {
        fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!");
        abort();
    }

    int digits = ceil(log10f(cnfVariableCount)) + 2;

    fprintf(f, "c generated by ezSAT\n");

    if (verbose)
    {
        fprintf(f, "c\n");
        fprintf(f, "c mapping of variables to literals:\n");
        for (int i = 0; i < int(cnfLiteralVariables.size()); i++)
            if (cnfLiteralVariables[i] != 0)
                fprintf(f, "c %*d: %s\n", digits, cnfLiteralVariables[i], literals[i].c_str());

        fprintf(f, "c\n");
        fprintf(f, "c mapping of variables to expressions:\n");
        for (int i = 0; i < int(cnfExpressionVariables.size()); i++)
            if (cnfExpressionVariables[i] != 0)
                fprintf(f, "c %*d: %d\n", digits, cnfExpressionVariables[i], -i-1);

        if (mode_keep_cnf()) {
            fprintf(f, "c\n");
            fprintf(f, "c %d clauses from backup, %d from current buffer\n",
                    int(cnfClausesBackup.size()), int(cnfClauses.size()));
        }

        fprintf(f, "c\n");
    }

    std::vector<std::vector<int>> all_clauses;
    getFullCnf(all_clauses);
    assert(cnfClausesCount == int(all_clauses.size()));

    fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount);
    int maxClauseLen = 0;
    for (auto &clause : all_clauses)
        maxClauseLen = std::max(int(clause.size()), maxClauseLen);
    if (!verbose)
        maxClauseLen = std::min(maxClauseLen, 3);
    for (auto &clause : all_clauses) {
        for (auto idx : clause)
            fprintf(f, " %*d", digits, idx);
        if (maxClauseLen >= int(clause.size()))
            fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
        else
            fprintf(f, " %*d\n", digits, 0);
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::printInternalState ( FILE *  f ) const

inherited

Definition at line 1263 of file ezsat.cc.

{
    fprintf(f, "--8<-- snip --8<--\n");

    fprintf(f, "literalsCache:\n");
    for (auto &it : literalsCache)
        fprintf(f, "    `%s' -> %d\n", it.first.c_str(), it.second);

    fprintf(f, "literals:\n");
    for (int i = 0; i < int(literals.size()); i++)
        fprintf(f, "    %d: `%s'\n", i+1, literals[i].c_str());

    fprintf(f, "expressionsCache:\n");
    for (auto &it : expressionsCache)
        fprintf(f, "    `%s' -> %d\n", expression2str(it.first).c_str(), it.second);

    fprintf(f, "expressions:\n");
    for (int i = 0; i < int(expressions.size()); i++)
        fprintf(f, "    %d: `%s'\n", -i-1, expression2str(expressions[i]).c_str());

    fprintf(f, "cnfVariables (count=%d):\n", cnfVariableCount);
    for (int i = 0; i < int(cnfLiteralVariables.size()); i++)
        if (cnfLiteralVariables[i] != 0)
            fprintf(f, "    literal %d -> %d (%s)\n", i+1, cnfLiteralVariables[i], to_string(i+1).c_str());
    for (int i = 0; i < int(cnfExpressionVariables.size()); i++)
        if (cnfExpressionVariables[i] != 0)
            fprintf(f, "    expression %d -> %d (%s)\n", -i-1, cnfExpressionVariables[i], to_string(-i-1).c_str());

    fprintf(f, "cnfClauses:\n");
    for (auto &i1 : cnfClauses) {
        for (auto &i2 : i1)
            fprintf(f, " %4d", i2);
        fprintf(f, "\n");
    }
    if (cnfConsumed)
        fprintf(f, " *** more clauses consumed via cnfConsume() ***\n");

    fprintf(f, "--8<-- snap --8<--\n");
}

Here is the call graph for this function:

void ezSAT::SET ( _V  a, _V  b  )

inlineinherited

Definition at line 221 of file ezsat.h.

                         {
        assume(IFF(a.get(this), b.get(this)));
    }

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::setSolverTimeout ( int  newTimeoutSeconds )

inlineinherited

Definition at line 149 of file ezsat.h.

                                                 {
        solverTimeout = newTimeoutSeconds;
    }

bool ezSAT::solve ( const std::vector< int > &  modelExpressions, std::vector< bool > &  modelValues, const std::vector< int > &  assumptions  )

inlineinherited

Definition at line 122 of file ezsat.h.

                                                                                                                        {
        return solver(modelExpressions, modelValues, assumptions);
    }

Here is the call graph for this function:

Here is the caller graph for this function:

bool ezSAT::solve ( const std::vector< int > &  modelExpressions, std::vector< bool > &  modelValues, int  a = 0, int  b = 0, int  c = 0, int  d = 0, int  e = 0, int  f = 0  )

inlineinherited

Definition at line 126 of file ezsat.h.

                                                                                                                                                       {
        std::vector<int> assumptions;
        if (a != 0) assumptions.push_back(a);
        if (b != 0) assumptions.push_back(b);
        if (c != 0) assumptions.push_back(c);
        if (d != 0) assumptions.push_back(d);
        if (e != 0) assumptions.push_back(e);
        if (f != 0) assumptions.push_back(f);
        return solver(modelExpressions, modelValues, assumptions);
    }

Here is the call graph for this function:

bool ezSAT::solve ( int  a = 0, int  b = 0, int  c = 0, int  d = 0, int  e = 0, int  f = 0  )

inlineinherited

Definition at line 137 of file ezsat.h.

                                                                                 {
        std::vector<int> assumptions, modelExpressions;
        std::vector<bool> modelValues;
        if (a != 0) assumptions.push_back(a);
        if (b != 0) assumptions.push_back(b);
        if (c != 0) assumptions.push_back(c);
        if (d != 0) assumptions.push_back(d);
        if (e != 0) assumptions.push_back(e);
        if (f != 0) assumptions.push_back(f);
        return solver(modelExpressions, modelValues, assumptions);
    }

Here is the call graph for this function:

bool ezMiniSAT::solver ( const std::vector< int > &  modelExpressions, std::vector< bool > &  modelValues, const std::vector< int > &  assumptions  )

virtual

Reimplemented from ezSAT.

Definition at line 97 of file ezminisat.cc.

{
    preSolverCallback();

    solverTimoutStatus = false;

    if (0) {
contradiction:
        delete minisatSolver;
        minisatSolver = NULL;
        minisatVars.clear();
        foundContradiction = true;
        return false;
    }

    if (foundContradiction) {
        consumeCnf();
        return false;
    }

    std::vector<int> extraClauses, modelIdx;

    for (auto id : assumptions)
        extraClauses.push_back(bind(id));
    for (auto id : modelExpressions)
        modelIdx.push_back(bind(id));

    if (minisatSolver == NULL) {
        minisatSolver = new Solver;
        minisatSolver->verbosity = EZMINISAT_VERBOSITY;
    }

#if EZMINISAT_INCREMENTAL
    std::vector<std::vector<int>> cnf;
    consumeCnf(cnf);
#else
    const std::vector<std::vector<int>> &cnf = this->cnf();
#endif

    while (int(minisatVars.size()) < numCnfVariables())
        minisatVars.push_back(minisatSolver->newVar());

#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
    for (auto idx : cnfFrozenVars)
        minisatSolver->setFrozen(minisatVars.at(idx > 0 ? idx-1 : -idx-1), true);
    cnfFrozenVars.clear();
#endif

    for (auto &clause : cnf) {
        Minisat::vec<Minisat::Lit> ps;
        for (auto idx : clause) {
            if (idx > 0)
                ps.push(Minisat::mkLit(minisatVars.at(idx-1)));
            else
                ps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
#if EZMINISAT_SIMPSOLVER
            if (minisatSolver->isEliminated(minisatVars.at(idx > 0 ? idx-1 : -idx-1))) {
                fprintf(stderr, "Assert in %s:%d failed! Missing call to ezsat->freeze(): %s (lit=%d)\n",
                        __FILE__, __LINE__, cnfLiteralInfo(idx).c_str(), idx);
                abort();
            }
#endif
        }
        if (!minisatSolver->addClause(ps))
            goto contradiction;
    }

    if (cnf.size() > 0 && !minisatSolver->simplify())
        goto contradiction;

    Minisat::vec<Minisat::Lit> assumps;

    for (auto idx : extraClauses) {
        if (idx > 0)
            assumps.push(Minisat::mkLit(minisatVars.at(idx-1)));
        else
            assumps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
#if EZMINISAT_SIMPSOLVER
        if (minisatSolver->isEliminated(minisatVars.at(idx > 0 ? idx-1 : -idx-1))) {
            fprintf(stderr, "Assert in %s:%d failed! Missing call to ezsat->freeze(): %s\n", __FILE__, __LINE__, cnfLiteralInfo(idx).c_str());
            abort();
        }
#endif
    }

#ifndef _WIN32
    struct sigaction sig_action;
    struct sigaction old_sig_action;
    int old_alarm_timeout = 0;

    if (solverTimeout > 0) {
        sig_action.sa_handler = alarmHandler;
        sigemptyset(&sig_action.sa_mask);
        sig_action.sa_flags = SA_RESTART;
        alarmHandlerThis = this;
        alarmHandlerTimeout = clock() + solverTimeout*CLOCKS_PER_SEC;
        old_alarm_timeout = alarm(0);
        sigaction(SIGALRM, &sig_action, &old_sig_action);
        alarm(1);
    }
#endif

    bool foundSolution = minisatSolver->solve(assumps);

#ifndef _WIN32
    if (solverTimeout > 0) {
        if (alarmHandlerTimeout == 0)
            solverTimoutStatus = true;
        alarm(0);
        sigaction(SIGALRM, &old_sig_action, NULL);
        alarm(old_alarm_timeout);
    }
#endif

    if (!foundSolution) {
#if !EZMINISAT_INCREMENTAL
        delete minisatSolver;
        minisatSolver = NULL;
        minisatVars.clear();
#endif
        return false;
    }

    modelValues.clear();
    modelValues.resize(modelIdx.size());

    for (size_t i = 0; i < modelIdx.size(); i++)
    {
        int idx = modelIdx[i];
        bool refvalue = true;

        if (idx < 0)
            idx = -idx, refvalue = false;

        using namespace Minisat;
        lbool value = minisatSolver->modelValue(minisatVars.at(idx-1));
        modelValues[i] = (value == Minisat::lbool(refvalue));
    }

#if !EZMINISAT_INCREMENTAL
    delete minisatSolver;
    minisatSolver = NULL;
    minisatVars.clear();
#endif
    return true;
}

Here is the call graph for this function:

std::string ezSAT::to_string ( int  id ) const

inherited

Definition at line 237 of file ezsat.cc.

{
    std::string text;

    if (id > 0)
    {
        lookup_literal(id, text);
    }
    else
    {
        OpId op;
        std::vector<int> args;
        lookup_expression(id, op, args);

        switch (op)
        {
        case OpNot:
            text = "not(";
            break;

        case OpAnd:
            text = "and(";
            break;

        case OpOr:
            text = "or(";
            break;

        case OpXor:
            text = "xor(";
            break;

        case OpIFF:
            text = "iff(";
            break;

        case OpITE:
            text = "ite(";
            break;

        default:
            abort();
        }

        for (int i = 0; i < int(args.size()); i++) {
            if (i > 0)
                text += ", ";
            text += to_string(args[i]);
        }

        text += ")";
    }

    return text;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::value ( bool  val )

inherited

Definition at line 68 of file ezsat.cc.

{
    return val ? CONST_TRUE : CONST_FALSE;
}

Here is the caller graph for this function:

int ezSAT::VAR ( _V  a )

inlineinherited

Definition at line 193 of file ezsat.h.

                  {
        return a.get(this);
    }

Here is the call graph for this function:

Here is the caller graph for this function:

ezSATvec ezSAT::vec ( const std::vector< int > &  vec )

inherited

Definition at line 1183 of file ezsat.cc.

{
    return ezSATvec(*this, vec);
}

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_add ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 819 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    std::vector<int> vec(vec1.size());
    int carry = CONST_FALSE;
    for (int i = 0; i < int(vec1.size()); i++)
        fulladder(this, vec1[i], vec2[i], carry, carry, vec[i]);

#if 0
    printf("ADD> vec1=[");
    for (int i = int(vec1.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec1[i]).c_str(), i ? ", " : "");
    printf("], vec2=[");
    for (int i = int(vec2.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec2[i]).c_str(), i ? ", " : "");
    printf("], result=[");
    for (int i = int(vec.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec[i]).c_str(), i ? ", " : "");
    printf("]\n");
#endif

    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_and ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 709 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    std::vector<int> vec(vec1.size());
    for (int i = 0; i < int(vec1.size()); i++)
        vec[i] = AND(vec1[i], vec2[i]);
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::vec_append ( std::vector< int > &  vec, const std::vector< int > &  vec1  ) const

inherited

Definition at line 1083 of file ezsat.cc.

{
    for (auto bit : vec1)
        vec.push_back(bit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::vec_append_signed ( std::vector< int > &  vec, const std::vector< int > &  vec1, int64_t  value  )

inherited

Definition at line 1089 of file ezsat.cc.

{
    assert(int(vec1.size()) <= 64);
    for (int i = 0; i < int(vec1.size()); i++) {
        if (((value >> i) & 1) != 0)
            vec.push_back(vec1[i]);
        else
            vec.push_back(NOT(vec1[i]));
    }
}

Here is the call graph for this function:

void ezSAT::vec_append_unsigned ( std::vector< int > &  vec, const std::vector< int > &  vec1, uint64_t  value  )

inherited

Definition at line 1100 of file ezsat.cc.

{
    assert(int(vec1.size()) <= 64);
    for (int i = 0; i < int(vec1.size()); i++) {
        if (((value >> i) & 1) != 0)
            vec.push_back(vec1[i]);
        else
            vec.push_back(NOT(vec1[i]));
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_cast ( const std::vector< int > &  vec1, int  toBits, bool  signExtend = false  )

inherited

Definition at line 690 of file ezsat.cc.

{
    std::vector<int> vec;
    for (int i = 0; i < toBits; i++)
        if (i >= int(vec1.size()))
            vec.push_back(signExtend ? vec1.back() : CONST_FALSE);
        else
            vec.push_back(vec1[i]);
    return vec;
}

Here is the call graph for this function:

void ezSAT::vec_cmp ( const std::vector< int > &  vec1, const std::vector< int > &  vec2, int &  carry, int &  overflow, int &  sign, int &  zero  )

inherited

Definition at line 873 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    carry = CONST_TRUE;
    zero = CONST_FALSE;
    for (int i = 0; i < int(vec1.size()); i++) {
        overflow = carry;
        fulladder(this, vec1[i], NOT(vec2[i]), carry, carry, sign);
        zero = OR(zero, sign);
    }
    overflow = XOR(overflow, carry);
    carry = NOT(carry);
    zero = NOT(zero);

#if 0
    printf("CMP> vec1=[");
    for (int i = int(vec1.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec1[i]).c_str(), i ? ", " : "");
    printf("], vec2=[");
    for (int i = int(vec2.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec2[i]).c_str(), i ? ", " : "");
    printf("], carry=%s, overflow=%s, sign=%s, zero=%s\n", to_string(carry).c_str(), to_string(overflow).c_str(), to_string(sign).c_str(), to_string(zero).c_str());
#endif
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_const ( const std::vector< bool > &  bits )

inherited

Definition at line 649 of file ezsat.cc.

{
    std::vector<int> vec;
    for (auto bit : bits)
        vec.push_back(bit ? CONST_TRUE : CONST_FALSE);
    return vec;
}

Here is the call graph for this function:

std::vector< int > ezSAT::vec_const_signed ( int64_t  value, int  numBits  )

inherited

Definition at line 657 of file ezsat.cc.

{
    std::vector<int> vec;
    for (int i = 0; i < numBits; i++)
        vec.push_back(((value >> i) & 1) != 0 ? CONST_TRUE : CONST_FALSE);
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_const_unsigned ( uint64_t  value, int  numBits  )

inherited

Definition at line 665 of file ezsat.cc.

{
    std::vector<int> vec;
    for (int i = 0; i < numBits; i++)
        vec.push_back(((value >> i) & 1) != 0 ? CONST_TRUE : CONST_FALSE);
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_count ( const std::vector< int > &  vec, int  numBits, bool  clip = true  )

inherited

Definition at line 789 of file ezsat.cc.

{
    std::vector<int> sum = vec_const_unsigned(0, numBits);
    std::vector<int> carry_vector;

    for (auto bit : vec) {
        int carry = bit;
        for (int i = 0; i < numBits; i++)
            halfadder(this, carry, sum[i], carry, sum[i]);
        carry_vector.push_back(carry);
    }

    if (clip) {
        int overflow = vec_reduce_or(carry_vector);
        sum = vec_ite(overflow, vec_const_unsigned(~0, numBits), sum);
    }

#if 0
    printf("COUNT> vec=[");
    for (int i = int(vec.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec[i]).c_str(), i ? ", " : "");
    printf("], result=[");
    for (int i = int(sum.size())-1; i >= 0; i--)
        printf("%s%s", to_string(sum[i]).c_str(), i ? ", " : "");
    printf("]\n");
#endif

    return sum;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_eq ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 954 of file ezsat.cc.

{
    return vec_reduce_and(vec_iff(vec1, vec2));
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_ge_signed ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 912 of file ezsat.cc.

{
    int carry, overflow, sign, zero;
    vec_cmp(vec1, vec2, carry, overflow, sign, zero);
    return OR(AND(NOT(overflow), NOT(sign)), AND(overflow, sign));
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_ge_unsigned ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 940 of file ezsat.cc.

{
    int carry, overflow, sign, zero;
    vec_cmp(vec1, vec2, carry, overflow, sign, zero);
    return NOT(carry);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_gt_signed ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 919 of file ezsat.cc.

{
    int carry, overflow, sign, zero;
    vec_cmp(vec1, vec2, carry, overflow, sign, zero);
    return AND(OR(AND(NOT(overflow), NOT(sign)), AND(overflow, sign)), NOT(zero));
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_gt_unsigned ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 947 of file ezsat.cc.

{
    int carry, overflow, sign, zero;
    vec_cmp(vec1, vec2, carry, overflow, sign, zero);
    return AND(NOT(carry), NOT(zero));
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_iff ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 736 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    std::vector<int> vec(vec1.size());
    for (int i = 0; i < int(vec1.size()); i++)
        vec[i] = IFF(vec1[i], vec2[i]);
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_ite ( const std::vector< int > &  vec1, const std::vector< int > &  vec2, const std::vector< int > &  vec3  )

inherited

Definition at line 745 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size() && vec2.size() == vec3.size());
    std::vector<int> vec(vec1.size());
    for (int i = 0; i < int(vec1.size()); i++)
        vec[i] = ITE(vec1[i], vec2[i], vec3[i]);
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_ite ( int  sel, const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 755 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    std::vector<int> vec(vec1.size());
    for (int i = 0; i < int(vec1.size()); i++)
        vec[i] = ITE(sel, vec1[i], vec2[i]);
    return vec;
}

Here is the call graph for this function:

int ezSAT::vec_le_signed ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 905 of file ezsat.cc.

{
    int carry, overflow, sign, zero;
    vec_cmp(vec1, vec2, carry, overflow, sign, zero);
    return OR(AND(NOT(overflow), sign), AND(overflow, NOT(sign)), zero);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_le_unsigned ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 933 of file ezsat.cc.

{
    int carry, overflow, sign, zero;
    vec_cmp(vec1, vec2, carry, overflow, sign, zero);
    return OR(carry, zero);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_lt_signed ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 898 of file ezsat.cc.

{
    int carry, overflow, sign, zero;
    vec_cmp(vec1, vec2, carry, overflow, sign, zero);
    return OR(AND(NOT(overflow), sign), AND(overflow, NOT(sign)));
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_lt_unsigned ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 926 of file ezsat.cc.

{
    int carry, overflow, sign, zero;
    vec_cmp(vec1, vec2, carry, overflow, sign, zero);
    return carry;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int64_t ezSAT::vec_model_get_signed ( const std::vector< int > &  modelExpressions, const std::vector< bool > &  modelValues, const std::vector< int > &  vec1  ) const

inherited

Definition at line 1111 of file ezsat.cc.

{
    int64_t value = 0;
    std::map<int, bool> modelMap;
    assert(modelExpressions.size() == modelValues.size());
    for (int i = 0; i < int(modelExpressions.size()); i++)
        modelMap[modelExpressions[i]] = modelValues[i];
    for (int i = 0; i < 64; i++) {
        int j = i < int(vec1.size()) ? i : vec1.size()-1;
        if (modelMap.at(vec1[j]))
            value |= int64_t(1) << i;
    }
    return value;
}

Here is the call graph for this function:

uint64_t ezSAT::vec_model_get_unsigned ( const std::vector< int > &  modelExpressions, const std::vector< bool > &  modelValues, const std::vector< int > &  vec1  ) const

inherited

Definition at line 1126 of file ezsat.cc.

{
    uint64_t value = 0;
    std::map<int, bool> modelMap;
    assert(modelExpressions.size() == modelValues.size());
    for (int i = 0; i < int(modelExpressions.size()); i++)
        modelMap[modelExpressions[i]] = modelValues[i];
    for (int i = 0; i < int(vec1.size()); i++)
        if (modelMap.at(vec1[i]))
            value |= uint64_t(1) << i;
    return value;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_ne ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 959 of file ezsat.cc.

{
    return NOT(vec_reduce_and(vec_iff(vec1, vec2)));
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_neg ( const std::vector< int > &  vec )

inherited

Definition at line 867 of file ezsat.cc.

{
    std::vector<int> zero(vec.size(), CONST_FALSE);
    return vec_sub(zero, vec);
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_not ( const std::vector< int > &  vec1 )

inherited

Definition at line 701 of file ezsat.cc.

{
    std::vector<int> vec;
    for (auto bit : vec1)
        vec.push_back(NOT(bit));
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_or ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 718 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    std::vector<int> vec(vec1.size());
    for (int i = 0; i < int(vec1.size()); i++)
        vec[i] = OR(vec1[i], vec2[i]);
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_reduce_and ( const std::vector< int > &  vec1 )

inherited

Definition at line 1139 of file ezsat.cc.

{
    return expression(OpAnd, vec1);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::vec_reduce_or ( const std::vector< int > &  vec1 )

inherited

Definition at line 1144 of file ezsat.cc.

{
    return expression(OpOr, vec1);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::vec_set ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 1149 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    for (int i = 0; i < int(vec1.size()); i++)
        SET(vec1[i], vec2[i]);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void ezSAT::vec_set_signed ( const std::vector< int > &  vec1, int64_t  value  )

inherited

Definition at line 1156 of file ezsat.cc.

{
    assert(int(vec1.size()) <= 64);
    for (int i = 0; i < int(vec1.size()); i++) {
        if (((value >> i) & 1) != 0)
            assume(vec1[i]);
        else
            assume(NOT(vec1[i]));
    }
}

Here is the call graph for this function:

void ezSAT::vec_set_unsigned ( const std::vector< int > &  vec1, uint64_t  value  )

inherited

Definition at line 1167 of file ezsat.cc.

{
    assert(int(vec1.size()) <= 64);
    for (int i = 0; i < int(vec1.size()); i++) {
        if (((value >> i) & 1) != 0)
            assume(vec1[i]);
        else
            assume(NOT(vec1[i]));
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_shift ( const std::vector< int > &  vec1, int  shift, int  extend_left, int  extend_right  )

inherited

Definition at line 993 of file ezsat.cc.

{
    std::vector<int> vec;
    for (int i = 0; i < int(vec1.size()); i++) {
        int j = i+shift;
        if (j < 0)
            vec.push_back(extend_right);
        else if (j >= int(vec1.size()))
            vec.push_back(extend_left);
        else
            vec.push_back(vec1[j]);
    }
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_shift_left ( const std::vector< int > &  vec1, const std::vector< int > &  vec2, bool  vec2_signed, int  extend_left, int  extend_right  )

inherited

Definition at line 1059 of file ezsat.cc.

{
    // vec2_signed is not implemented in vec_shift_left() yet
    assert(vec2_signed == false);

    int vec2_bits = std::min(my_clog2(vec1.size()), int(vec2.size()));

    std::vector<int> overflow_bits(vec2.begin() + vec2_bits, vec2.end());
    int overflow = vec_reduce_or(overflow_bits);

    std::vector<int> buffer = vec1;
    std::vector<int> overflow_pattern_right(buffer.size(), extend_right);
    buffer = vec_ite(overflow, overflow_pattern_right, buffer);

    for (int i = 0; i < vec2_bits; i++) {
        std::vector<int> shifted_buffer;
        shifted_buffer = vec_shift(buffer, -(1 << i), extend_left, extend_right);
        buffer = vec_ite(vec2[i], shifted_buffer, buffer);
    }

    buffer.resize(vec1.size());
    return buffer;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_shift_right ( const std::vector< int > &  vec1, const std::vector< int > &  vec2, bool  vec2_signed, int  extend_left, int  extend_right  )

inherited

Definition at line 1016 of file ezsat.cc.

{
    int vec2_bits = std::min(my_clog2(vec1.size()) + (vec2_signed ? 1 : 0), int(vec2.size()));

    std::vector<int> overflow_bits(vec2.begin() + vec2_bits, vec2.end());
    int overflow_left = CONST_FALSE, overflow_right = CONST_FALSE;

    if (vec2_signed) {
        int overflow = CONST_FALSE;
        for (auto bit : overflow_bits)
            overflow = OR(overflow, XOR(bit, vec2[vec2_bits-1]));
        overflow_left = AND(overflow, NOT(vec2.back()));
        overflow_right = AND(overflow, vec2.back());
    } else
        overflow_left = vec_reduce_or(overflow_bits);

    std::vector<int> buffer = vec1;

    if (vec2_signed)
        while (buffer.size() < vec1.size() + (1 << vec2_bits))
            buffer.push_back(extend_left);

    std::vector<int> overflow_pattern_left(buffer.size(), extend_left);
    std::vector<int> overflow_pattern_right(buffer.size(), extend_right);

    buffer = vec_ite(overflow_left, overflow_pattern_left, buffer);

    if (vec2_signed)
        buffer = vec_ite(overflow_right, overflow_pattern_left, buffer);

    for (int i = vec2_bits-1; i >= 0; i--) {
        std::vector<int> shifted_buffer;
        if (vec2_signed && i == vec2_bits-1)
            shifted_buffer = vec_shift(buffer, -(1 << i), extend_left, extend_right);
        else
            shifted_buffer = vec_shift(buffer, 1 << i, extend_left, extend_right);
        buffer = vec_ite(vec2[i], shifted_buffer, buffer);
    }

    buffer.resize(vec1.size());
    return buffer;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_shl ( const std::vector< int > &  vec1, int  shift, bool  signExtend = false  )

inherited

Definition at line 964 of file ezsat.cc.

{
    std::vector<int> vec;
    for (int i = 0; i < int(vec1.size()); i++) {
        int j = i-shift;
        if (int(vec1.size()) <= j)
            vec.push_back(signExtend ? vec1.back() : CONST_FALSE);
        else if (0 <= j)
            vec.push_back(vec1[j]);
        else
            vec.push_back(CONST_FALSE);
    }
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector<int> ezSAT::vec_shr ( const std::vector< int > &  vec1, int  shift, bool  signExtend = false  )

inlineinherited

Definition at line 266 of file ezsat.h.

{ return vec_shl(vec1, -shift, signExtend); }

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_srl ( const std::vector< int > &  vec1, int  shift  )

inherited

Definition at line 979 of file ezsat.cc.

{
    std::vector<int> vec;
    for (int i = 0; i < int(vec1.size()); i++) {
        int j = i-shift;
        while (j < 0)
            j += vec1.size();
        while (j >= int(vec1.size()))
            j -= vec1.size();
        vec.push_back(vec1[j]);
    }
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector<int> ezSAT::vec_srr ( const std::vector< int > &  vec1, int  shift  )

inlineinherited

Definition at line 267 of file ezsat.h.

{ return vec_srl(vec1, -shift); }

Here is the call graph for this function:

std::vector< int > ezSAT::vec_sub ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 843 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    std::vector<int> vec(vec1.size());
    int carry = CONST_TRUE;
    for (int i = 0; i < int(vec1.size()); i++)
        fulladder(this, vec1[i], NOT(vec2[i]), carry, carry, vec[i]);

#if 0
    printf("SUB> vec1=[");
    for (int i = int(vec1.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec1[i]).c_str(), i ? ", " : "");
    printf("], vec2=[");
    for (int i = int(vec2.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec2[i]).c_str(), i ? ", " : "");
    printf("], result=[");
    for (int i = int(vec.size())-1; i >= 0; i--)
        printf("%s%s", to_string(vec[i]).c_str(), i ? ", " : "");
    printf("]\n");
#endif

    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_var ( int  numBits )

inherited

Definition at line 673 of file ezsat.cc.

{
    std::vector<int> vec;
    for (int i = 0; i < numBits; i++)
        vec.push_back(literal());
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::vector< int > ezSAT::vec_var ( std::string  name, int  numBits  )

inherited

Definition at line 681 of file ezsat.cc.

{
    std::vector<int> vec;
    for (int i = 0; i < numBits; i++) {
        vec.push_back(VAR(name + my_int_to_string(i)));
    }
    return vec;
}

Here is the call graph for this function:

std::vector< int > ezSAT::vec_xor ( const std::vector< int > &  vec1, const std::vector< int > &  vec2  )

inherited

Definition at line 727 of file ezsat.cc.

{
    assert(vec1.size() == vec2.size());
    std::vector<int> vec(vec1.size());
    for (int i = 0; i < int(vec1.size()); i++)
        vec[i] = XOR(vec1[i], vec2[i]);
    return vec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::XOR ( _V  a = 0, _V  b = 0, _V  c = 0, _V  d = 0, _V  e = 0, _V  f = 0  )

inlineinherited

Definition at line 209 of file ezsat.h.

                                                                        {
        return expression(OpXor, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this));
    }

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

ezMiniSAT * ezMiniSAT::alarmHandlerThis = NULL

staticprivate

Definition at line 55 of file ezminisat.h.

clock_t ezMiniSAT::alarmHandlerTimeout = 0

staticprivate

Definition at line 56 of file ezminisat.h.

std::set<int> ezMiniSAT::cnfFrozenVars

private

Definition at line 51 of file ezminisat.h.

const int ezSAT::CONST_FALSE = 2

staticinherited

Definition at line 49 of file ezsat.h.

const int ezSAT::CONST_TRUE = 1

staticinherited

Definition at line 48 of file ezsat.h.

bool ezMiniSAT::foundContradiction

private

Definition at line 48 of file ezminisat.h.

Solver* ezMiniSAT::minisatSolver

private

Definition at line 46 of file ezminisat.h.

std::vector<int> ezMiniSAT::minisatVars

private

Definition at line 47 of file ezminisat.h.

int ezSAT::solverTimeout

inherited

Definition at line 80 of file ezsat.h.

bool ezSAT::solverTimoutStatus

inherited

Definition at line 81 of file ezsat.h.

---

The documentation for this class was generated from the following files:

• ezminisat.h
• ezminisat.cc