X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.h;h=0ff566e53cee07fd935e35a58a60d63d668943ea;hp=c6044864313280cb71e21a01528d73d0d87b0a36;hb=081e954fa3566ad9a2522ca45bef8e29472d2a72;hpb=c53a5c97df5189f82b618e510bb7fcad8671e5ff

diff --git a/src/csolver.h b/src/csolver.h
index c604486..0ff566e 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -101,8 +101,11 @@ public:
 
 	BooleanEdge applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
 
+	/** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/
+	BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize);
+	
 	/** This function applies a logical operation to the Booleans in its input. */
-
+	
 	BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
 
 	/** This function applies a logical operation to the Booleans in its input. */
@@ -141,7 +144,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;}
+	bool isBooleanVarUsed() {return booleanVarUsed;}
 	void printConstraint(BooleanEdge boolean);
 	void printConstraints();
 
@@ -161,16 +164,17 @@ public:
 	void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
 	CSolver *clone();
 	void serialize();
-	static CSolver *deserialize(const char *file);
+	static CSolver *deserialize(const char *file, InterpreterType itype = SATUNE);
 	void autoTune(uint budget);
 	void inferFixedOrders();
 	void inferFixedOrder(Order *order);
-
-
+	void setInterpreter(InterpreterType type);
+	bool useInterpreter() {return interpreter != NULL;}
 	void setTuner(Tuner *_tuner) { tuner = _tuner; }
 	long long getElapsedTime() { return elapsedTime; }
 	long long getEncodeTime();
 	long long getSolveTime();
+	long getSatSolverTimeout() { return satsolverTimeout;}
 
 	CMEMALLOC;
 
@@ -218,10 +222,11 @@ private:
 
 	SATEncoder *satEncoder;
 	bool unsat;
-        bool booleanVarUsed;
-        Tuner *tuner;
+	bool booleanVarUsed;
+	Tuner *tuner;
 	long long elapsedTime;
 	long satsolverTimeout;
+	Interpreter *interpreter;
 	friend class ElementOpt;
 	friend class VarOrderingOpt;
 };