Added ezSAT library

1 files changed, 313 insertions, 0 deletions

diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
new file mode 100644
index 00000000..29b7aca7
--- /dev/null
+++ b/libs/ezsat/ezsat.h
@@ -0,0 +1,313 @@
+/*
+ *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ *  Copyright (C) 2013  Clifford Wolf <clifford@clifford.at>
+ *  
+ *  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 <set>
+#include <map>
+#include <vector>
+#include <string>
+#include <stdio.h>
+
+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
+	};
+
+	const int TRUE = 1;
+	const int FALSE = 2;
+
+private:
+	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;
+	std::vector<int> cnfLiteralVariables, cnfExpressionVariables;
+	std::vector<std::vector<int>> cnfClauses;
+	std::set<int> cnfAssumptions;
+
+	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);
+
+public:
+	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<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 { return literals.size(); }
+	int numExpressions() const { return expressions.size(); }
+
+	int eval(int id, const std::vector<int> &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).
+
+	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) {
+		return solver(modelExpressions, modelValues, 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) {
+		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);
+	}
+
+	bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) {
+		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);
+	}
+
+	// manage CNF (usually only accessed by SAT solvers)
+
+	virtual void clear();
+	void assume(int id);
+	int bind(int id);
+
+	const std::set<int> &assumed() const { return cnfAssumptions; }
+	int bound(int id) const;
+
+	int numCnfVariables() const { return cnfVariableCount; }
+	const std::vector<std::vector<int>> &cnf() const { return cnfClauses; }
+
+	void consumeCnf();
+	void consumeCnf(std::vector<std::vector<int>> &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<int> vec_const_signed(int64_t value, int bits);
+	std::vector<int> vec_const_unsigned(uint64_t value, int bits);
+	std::vector<int> vec_var(std::string name, int bits);
+	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> &vec2, const std::vector<int> &vec3);
+
+	std::vector<int> vec_count(const std::vector<int> &vec, int bits, 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);
+
+	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) { return vec_shl(vec1, -shift, signExtend); }
+	std::vector<int> vec_srr(const std::vector<int> &vec1, int shift) { return vec_srl(vec1, -shift); }
+
+	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);
+
+	// helpers for generating ezSATbit and ezSATvec objects
+
+	struct ezSATbit bit(_V a);
+	struct ezSATvec vec(const std::vector<int> &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<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);
+};
+
+// 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<int>() const { return std::vector<int>(1, id); }
+};
+
+struct ezSATvec
+{
+	ezSAT &sat;
+	std::vector<int> vec;
+
+	ezSATvec(ezSAT &sat, const std::vector<int> &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<int>() const { return vec; }
+};
+
+#endif