X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.h;h=74d0bf6e2c64b9e237f7ab0e9381b6b40a3f7c63;hp=1bc24769a7edee9e78cf2025b0e855b8d3fbf423;hb=dbe12973cd2236f5e76a70c24f68a05aeb3660c5;hpb=e0ee8656d201f77504bd239612969ce43636c324

diff --git a/src/csolver.h b/src/csolver.h
index 1bc2476..74d0bf6 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -141,7 +141,7 @@ public:
 	void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
 	void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
 	bool isUnSAT() { return unsat; }
-
+        bool isBooleanVarUsed(){return booleanVarUsed;}
 	void printConstraint(BooleanEdge boolean);
 	void printConstraints();
 
@@ -161,12 +161,12 @@ public:
 	void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
 	CSolver *clone();
 	void serialize();
-	static CSolver *deserialize(const char *file);
+	static CSolver *deserialize(const char *file, bool alloy = false);
 	void autoTune(uint budget);
 	void inferFixedOrders();
 	void inferFixedOrder(Order *order);
-
-
+	void setAlloyEncoder();
+	bool useAlloyCompiler() {return alloyEncoder != NULL;}
 	void setTuner(Tuner *_tuner) { tuner = _tuner; }
 	long long getElapsedTime() { return elapsedTime; }
 	long long getEncodeTime();
@@ -218,11 +218,13 @@ private:
 
 	SATEncoder *satEncoder;
 	bool unsat;
-	Tuner *tuner;
+        bool booleanVarUsed;
+        Tuner *tuner;
 	long long elapsedTime;
 	long satsolverTimeout;
+	AlloyEnc *alloyEncoder;
 	friend class ElementOpt;
-        friend class VarOrderingOpt;
+	friend class VarOrderingOpt;
 };
 
 inline CompOp flipOp(CompOp op) {