ezSAT Class Reference

#include <ezsat.h>

Inheritance diagram for ezSAT:

Data Structures
struct	_V

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

Public Member Functions
	ezSAT ()
virtual	~ezSAT ()
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
virtual bool	solver (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, 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 ()
virtual void	clear ()
virtual void	freeze (int id)
virtual bool	eliminated (int idx)
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 Member Functions
void	add_clause (const std::vector< int > &args)
void	add_clause (const std::vector< int > &args, bool argsPolarity, int a=0, int b=0, int c=0)
void	add_clause (int a, int b=0, int c=0)
int	bind_cnf_not (const std::vector< int > &args)
int	bind_cnf_and (const std::vector< int > &args)
int	bind_cnf_or (const std::vector< int > &args)

Private Attributes
bool	flag_keep_cnf
bool	flag_non_incremental
bool	non_incremental_solve_used_up
std::map< std::string, int >	literalsCache
std::vector< std::string >	literals
std::map< std::pair< OpId, std::vector< int > >, int >	expressionsCache
std::vector< std::pair< OpId, std::vector< int > > >	expressions
bool	cnfConsumed
int	cnfVariableCount
int	cnfClausesCount
std::vector< int >	cnfLiteralVariables
std::vector< int >	cnfExpressionVariables
std::vector< std::vector< int > >	cnfClauses
std::vector< std::vector< int > >	cnfClausesBackup

Detailed Description

Definition at line 30 of file ezsat.h.

Member Enumeration Documentation

enum ezSAT::OpId

Enumerator
OpNot
OpAnd
OpOr
OpXor
OpIFF
OpITE

Definition at line 44 of file ezsat.h.

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

Constructor & Destructor Documentation

ezSAT::ezSAT

(

)

Definition at line 43 of file ezsat.cc.

{
    flag_keep_cnf = false;
    flag_non_incremental = false;

    non_incremental_solve_used_up = false;

    cnfConsumed = false;
    cnfVariableCount = 0;
    cnfClausesCount = 0;

    solverTimeout = 0;
    solverTimoutStatus = false;

    literal("CONST_TRUE");
    literal("CONST_FALSE");

    assert(literal("CONST_TRUE") == CONST_TRUE);
    assert(literal("CONST_FALSE") == CONST_FALSE);
}

Here is the call graph for this function:

ezSAT::~ezSAT ( )

virtual

Definition at line 64 of file ezsat.cc.

{
}

Member Function Documentation

void ezSAT::add_clause ( const std::vector< int > &  args )

private

Definition at line 430 of file ezsat.cc.

{
    cnfClauses.push_back(args);
    cnfClausesCount++;
}

Here is the caller graph for this function:

void ezSAT::add_clause ( const std::vector< int > &  args, bool  argsPolarity, int  a = 0, int  b = 0, int  c = 0  )

private

Definition at line 436 of file ezsat.cc.

{
    std::vector<int> clause;
    for (auto arg : args)
        clause.push_back(argsPolarity ? +arg : -arg);
    if (a != 0)
        clause.push_back(a);
    if (b != 0)
        clause.push_back(b);
    if (c != 0)
        clause.push_back(c);
    add_clause(clause);
}

Here is the call graph for this function:

void ezSAT::add_clause ( int  a, int  b = 0, int  c = 0  )

private

Definition at line 450 of file ezsat.cc.

{
    std::vector<int> clause;
    if (a != 0)
        clause.push_back(a);
    if (b != 0)
        clause.push_back(b);
    if (c != 0)
        clause.push_back(c);
    add_clause(clause);
}

Here is the call 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  )

inline

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

)

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
	)

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:

int ezSAT::bind_cnf_and ( const std::vector< int > &  args )

private

Definition at line 468 of file ezsat.cc.

{
    assert(args.size() >= 2);

    int idx = ++cnfVariableCount;
    add_clause(args, false, idx);

    for (auto arg : args)
        add_clause(-idx, arg);

    return idx;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int ezSAT::bind_cnf_not ( const std::vector< int > &  args )

private

Definition at line 462 of file ezsat.cc.

{
    assert(args.size() == 1);
    return -args[0];
}

Here is the caller graph for this function:

int ezSAT::bind_cnf_or ( const std::vector< int > &  args )

private

Definition at line 481 of file ezsat.cc.

{
    assert(args.size() >= 2);

    int idx = ++cnfVariableCount;
    add_clause(args, true, -idx);

    for (auto arg : args)
        add_clause(idx, -arg);

    return idx;
}

Here is the call graph for this function:

Here is the caller graph for this function:

ezSATbit ezSAT::bit

(

_V

a

)

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

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 ezSAT::clear ( )

virtual

Reimplemented in ezMiniSAT.

Definition at line 369 of file ezsat.cc.

{
    cnfConsumed = false;
    cnfVariableCount = 0;
    cnfClausesCount = 0;
    cnfLiteralVariables.clear();
    cnfExpressionVariables.clear();
    cnfClauses.clear();
}

Here is the caller graph for this function:

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

inline

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

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

(

)

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

)

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:

bool ezSAT::eliminated ( int  idx )

virtual

Reimplemented in ezMiniSAT.

Definition at line 383 of file ezsat.cc.

{
    return false;
}

Here is the caller graph for this function:

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

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
	)

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
	)

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:

void ezSAT::freeze ( int  id )

virtual

Reimplemented in ezMiniSAT.

Definition at line 379 of file ezsat.cc.

{
}

Here is the caller graph for this function:

int ezSAT::frozen_literal

(

)

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

)

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

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 ( )

inline

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  )

inline

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  )

inline

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 ( )

inline

Definition at line 86 of file ezsat.h.

{ flag_keep_cnf = true; }

Here is the caller graph for this function:

int ezSAT::literal

(

)

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

)

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

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

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

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

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
	)

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

inline

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

inline

Definition at line 90 of file ezsat.h.

{ return flag_non_incremental; }

Here is the caller graph for this function:

void ezSAT::non_incremental ( )

inline

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 )

inline

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

inline

Definition at line 167 of file ezsat.h.

{ return cnfClausesCount; }

Here is the caller graph for this function:

int ezSAT::numCnfVariables ( ) const

inline

Definition at line 166 of file ezsat.h.

{ return cnfVariableCount; }

Here is the caller graph for this function:

int ezSAT::numExpressions ( ) const

inline

Definition at line 112 of file ezsat.h.

{ return expressions.size(); }

int ezSAT::numLiterals ( ) const

inline

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
	)

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  )

inline

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
	)

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

)

Definition at line 232 of file ezsat.cc.

{
    abort();
}

void ezSAT::preSolverCallback ( )

protected

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

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

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  )

inline

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 )

inline

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  )

inline

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  )

inline

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  )

inline

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 ezSAT::solver ( const std::vector< int > &  modelExpressions, std::vector< bool > &  modelValues, const std::vector< int > &  assumptions  )

virtual

Reimplemented in ezMiniSAT.

Definition at line 639 of file ezsat.cc.

{
    preSolverCallback();
    fprintf(stderr, "************************************************************************\n");
    fprintf(stderr, "ERROR: You are trying to use the solve() method of the ezSAT base class!\n");
    fprintf(stderr, "Use a dervied class like ezMiniSAT instead.\n");
    fprintf(stderr, "************************************************************************\n");
    abort();
}

Here is the call graph for this function:

Here is the caller graph for this function:

std::string ezSAT::to_string

(

int

id

)

const

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

)

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 )

inline

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

)

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
	)

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
	)

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

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
	)

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
	)

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
	)

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
	)

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

)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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

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

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
	)

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

)

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

)

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
	)

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

)

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

)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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
	)

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  )

inline

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
	)

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  )

inline

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
	)

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

)

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
	)

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
	)

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  )

inline

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

std::vector<std::vector<int> > ezSAT::cnfClauses

private

Definition at line 66 of file ezsat.h.

std::vector<std::vector<int> > ezSAT::cnfClausesBackup

private

Definition at line 66 of file ezsat.h.

int ezSAT::cnfClausesCount

private

Definition at line 64 of file ezsat.h.

bool ezSAT::cnfConsumed

private

Definition at line 63 of file ezsat.h.

std::vector<int> ezSAT::cnfExpressionVariables

private

Definition at line 65 of file ezsat.h.

std::vector<int> ezSAT::cnfLiteralVariables

private

Definition at line 65 of file ezsat.h.

int ezSAT::cnfVariableCount

private

Definition at line 64 of file ezsat.h.

const int ezSAT::CONST_FALSE = 2

static

Definition at line 49 of file ezsat.h.

const int ezSAT::CONST_TRUE = 1

static

Definition at line 48 of file ezsat.h.

std::vector<std::pair<OpId, std::vector<int> > > ezSAT::expressions

private

Definition at line 61 of file ezsat.h.

std::map<std::pair<OpId, std::vector<int> >, int> ezSAT::expressionsCache

private

Definition at line 60 of file ezsat.h.

bool ezSAT::flag_keep_cnf

private

Definition at line 52 of file ezsat.h.

bool ezSAT::flag_non_incremental

private

Definition at line 53 of file ezsat.h.

std::vector<std::string> ezSAT::literals

private

Definition at line 58 of file ezsat.h.

std::map<std::string, int> ezSAT::literalsCache

private

Definition at line 57 of file ezsat.h.

bool ezSAT::non_incremental_solve_used_up

private

Definition at line 55 of file ezsat.h.

int ezSAT::solverTimeout

Definition at line 80 of file ezsat.h.

bool ezSAT::solverTimoutStatus

Definition at line 81 of file ezsat.h.

---

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

• ezsat.h
• ezsat.cc