/* * ezSAT -- A simple and easy to use CNF generator for SAT solvers * * Copyright (C) 2013 Clifford Wolf * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. * */ #ifndef EZSAT_H #define EZSAT_H #include #include #include #include #include class ezSAT { // each token (terminal or non-terminal) is represented by an interger number // // the zero token: // the number zero is not used as valid token number and is used to encode // unused parameters for the functions. // // positive numbers are literals, with 1 = TRUE and 2 = FALSE; // // negative numbers are non-literal expressions. each expression is represented // by an operator id and a list of expressions (literals or non-literals). public: enum OpId { OpNot, OpAnd, OpOr, OpXor, OpIFF, OpITE }; static const int TRUE; static const int FALSE; private: std::map literalsCache; std::vector literals; std::map>, int> expressionsCache; std::vector>> expressions; bool cnfConsumed; int cnfVariableCount, cnfClausesCount; std::vector cnfLiteralVariables, cnfExpressionVariables; std::vector> cnfClauses; std::set cnfAssumptions; void add_clause(const std::vector &args); void add_clause(const std::vector &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 &args); int bind_cnf_and(const std::vector &args); int bind_cnf_or(const std::vector &args); public: int solverTimeout; bool solverTimoutStatus; ezSAT(); virtual ~ezSAT(); // manage expressions int value(bool val); int literal(); int 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 &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 &args) const; const std::vector &lookup_expression(int id, OpId &op) const; int parse_string(const std::string &text); std::string to_string(int id) const; int numLiterals() const { return literals.size(); } int numExpressions() const { return expressions.size(); } int eval(int id, const std::vector &values) const; // SAT solver interface // If you are planning on using the solver API (and not simply create a CNF) you must use a child class // of ezSAT that actually implements a solver backend, such as ezMiniSAT (see ezminisat.h). // Note: Solvers that can output don't-care values for model variables return a twice as big modelValues // vector. The first half contains the values and the second half the don't-care flags. virtual bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions); bool solve(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { return solver(modelExpressions, modelValues, assumptions); } bool solve(const std::vector &modelExpressions, std::vector &modelValues, int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) { std::vector 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); } bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) { std::vector assumptions, modelExpressions; std::vector 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); } void setSolverTimeout(int newTimeoutSeconds) { solverTimeout = newTimeoutSeconds; } bool getSolverTimoutStatus() { return solverTimoutStatus; } // manage CNF (usually only accessed by SAT solvers) virtual void clear(); void assume(int id); int bind(int id); const std::set &assumed() const { return cnfAssumptions; } int bound(int id) const; int numCnfVariables() const { return cnfVariableCount; } int numCnfClauses() const { return cnfClausesCount; } const std::vector> &cnf() const { return cnfClauses; } void consumeCnf(); void consumeCnf(std::vector> &cnf); // simple helpers for build expressions easily struct _V { int id; std::string name; _V(int id) : id(id) { } _V(const char *name) : id(0), name(name) { } _V(const std::string &name) : id(0), name(name) { } int get(ezSAT *that) { if (name.empty()) return id; return that->literal(name); } }; int VAR(_V a) { return a.get(this); } int NOT(_V a) { return expression(OpNot, a.get(this)); } int AND(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) { return expression(OpAnd, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this)); } int OR(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) { return expression(OpOr, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this)); } int XOR(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) { return expression(OpXor, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this)); } int IFF(_V a, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) { return expression(OpIFF, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this)); } int ITE(_V a, _V b, _V c) { return expression(OpITE, a.get(this), b.get(this), c.get(this)); } void SET(_V a, _V b) { assume(IFF(a.get(this), b.get(this))); } // simple helpers for building expressions with bit vectors std::vector vec_const_signed(int64_t value, int bits); std::vector vec_const_unsigned(uint64_t value, int bits); std::vector vec_var(std::string name, int bits); std::vector vec_cast(const std::vector &vec1, int toBits, bool signExtend = false); std::vector vec_not(const std::vector &vec1); std::vector vec_and(const std::vector &vec1, const std::vector &vec2); std::vector vec_or(const std::vector &vec1, const std::vector &vec2); std::vector vec_xor(const std::vector &vec1, const std::vector &vec2); std::vector vec_iff(const std::vector &vec1, const std::vector &vec2); std::vector vec_ite(const std::vector &vec1, const std::vector &vec2, const std::vector &vec3); std::vector vec_ite(int sel, const std::vector &vec2, const std::vector &vec3); std::vector vec_count(const std::vector &vec, int bits, bool clip = true); std::vector vec_add(const std::vector &vec1, const std::vector &vec2); std::vector vec_sub(const std::vector &vec1, const std::vector &vec2); void vec_cmp(const std::vector &vec1, const std::vector &vec2, int &carry, int &overflow, int &sign, int &zero); int vec_lt_signed(const std::vector &vec1, const std::vector &vec2); int vec_le_signed(const std::vector &vec1, const std::vector &vec2); int vec_ge_signed(const std::vector &vec1, const std::vector &vec2); int vec_gt_signed(const std::vector &vec1, const std::vector &vec2); int vec_lt_unsigned(const std::vector &vec1, const std::vector &vec2); int vec_le_unsigned(const std::vector &vec1, const std::vector &vec2); int vec_ge_unsigned(const std::vector &vec1, const std::vector &vec2); int vec_gt_unsigned(const std::vector &vec1, const std::vector &vec2); int vec_eq(const std::vector &vec1, const std::vector &vec2); int vec_ne(const std::vector &vec1, const std::vector &vec2); std::vector vec_shl(const std::vector &vec1, int shift, bool signExtend = false); std::vector vec_srl(const std::vector &vec1, int shift); std::vector vec_shr(const std::vector &vec1, int shift, bool signExtend = false) { return vec_shl(vec1, -shift, signExtend); } std::vector vec_srr(const std::vector &vec1, int shift) { return vec_srl(vec1, -shift); } void vec_append(std::vector &vec, const std::vector &vec1) const; void vec_append_signed(std::vector &vec, const std::vector &vec1, int64_t value); void vec_append_unsigned(std::vector &vec, const std::vector &vec1, uint64_t value); int64_t vec_model_get_signed(const std::vector &modelExpressions, const std::vector &modelValues, const std::vector &vec1) const; uint64_t vec_model_get_unsigned(const std::vector &modelExpressions, const std::vector &modelValues, const std::vector &vec1) const; int vec_reduce_and(const std::vector &vec1); int vec_reduce_or(const std::vector &vec1); void vec_set(const std::vector &vec1, const std::vector &vec2); void vec_set_signed(const std::vector &vec1, int64_t value); void vec_set_unsigned(const std::vector &vec1, uint64_t value); // helpers for generating ezSATbit and ezSATvec objects struct ezSATbit bit(_V a); struct ezSATvec vec(const std::vector &vec); // printing CNF and internal state void printDIMACS(FILE *f, bool verbose = false) const; void printInternalState(FILE *f) const; // more sophisticated constraints (designed to be used directly with assume(..)) int onehot(const std::vector &vec, bool max_only = false); int manyhot(const std::vector &vec, int min_hot, int max_hot = -1); int ordered(const std::vector &vec1, const std::vector &vec2, bool allow_equal = true); }; // helper classes for using operator overloading when generating complex expressions struct ezSATbit { ezSAT &sat; int id; ezSATbit(ezSAT &sat, ezSAT::_V a) : sat(sat), id(sat.VAR(a)) { } ezSATbit operator ~() { return ezSATbit(sat, sat.NOT(id)); } ezSATbit operator &(const ezSATbit &other) { return ezSATbit(sat, sat.AND(id, other.id)); } ezSATbit operator |(const ezSATbit &other) { return ezSATbit(sat, sat.OR(id, other.id)); } ezSATbit operator ^(const ezSATbit &other) { return ezSATbit(sat, sat.XOR(id, other.id)); } ezSATbit operator ==(const ezSATbit &other) { return ezSATbit(sat, sat.IFF(id, other.id)); } ezSATbit operator !=(const ezSATbit &other) { return ezSATbit(sat, sat.NOT(sat.IFF(id, other.id))); } operator int() const { return id; } operator ezSAT::_V() const { return ezSAT::_V(id); } operator std::vector() const { return std::vector(1, id); } }; struct ezSATvec { ezSAT &sat; std::vector vec; ezSATvec(ezSAT &sat, const std::vector &vec) : sat(sat), vec(vec) { } ezSATvec operator ~() { return ezSATvec(sat, sat.vec_not(vec)); } ezSATvec operator &(const ezSATvec &other) { return ezSATvec(sat, sat.vec_and(vec, other.vec)); } ezSATvec operator |(const ezSATvec &other) { return ezSATvec(sat, sat.vec_or(vec, other.vec)); } ezSATvec operator ^(const ezSATvec &other) { return ezSATvec(sat, sat.vec_xor(vec, other.vec)); } ezSATvec operator +(const ezSATvec &other) { return ezSATvec(sat, sat.vec_add(vec, other.vec)); } ezSATvec operator -(const ezSATvec &other) { return ezSATvec(sat, sat.vec_sub(vec, other.vec)); } ezSATbit operator < (const ezSATvec &other) { return ezSATbit(sat, sat.vec_lt_unsigned(vec, other.vec)); } ezSATbit operator <=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_le_unsigned(vec, other.vec)); } ezSATbit operator ==(const ezSATvec &other) { return ezSATbit(sat, sat.vec_eq(vec, other.vec)); } ezSATbit operator !=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_ne(vec, other.vec)); } ezSATbit operator >=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_ge_unsigned(vec, other.vec)); } ezSATbit operator > (const ezSATvec &other) { return ezSATbit(sat, sat.vec_gt_unsigned(vec, other.vec)); } ezSATvec operator <<(int shift) { return ezSATvec(sat, sat.vec_shl(vec, shift)); } ezSATvec operator >>(int shift) { return ezSATvec(sat, sat.vec_shr(vec, shift)); } operator std::vector() const { return vec; } }; #endif