X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.h;h=523ac307194534f1c7e35a302247cef2cc8032a7;hp=41c46277804d85199054548450b7a12db297b306;hb=f3515cbdd584cff4c03a6896ab1eb3d068f1040c;hpb=0703630a40f4fcfd8c8dcad336472907f125c86c

diff --git a/src/csolver.h b/src/csolver.h
index 41c4627..523ac30 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -11,7 +11,7 @@ class CSolver {
 public:
 	CSolver();
 	~CSolver();
-
+	void resetSolver();
 	/** This function creates a set containing the elements passed in the array. */
 	Set *createSet(VarType type, uint64_t *elements, uint num);
 
@@ -20,7 +20,7 @@ public:
 	Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
 
 	VarType getSetVarType(Set *set);
-	
+
 	Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
 
 	/** This function creates a mutable set. */
@@ -37,11 +37,11 @@ public:
 	    items to the set. */
 
 	uint64_t createUniqueItem(MutableSet *set);
-	
+
 	/**
 	 * Freeze and finalize the mutableSet ...
 	 */
-	void finalizeMutableSet(MutableSet* set);
+	void finalizeMutableSet(MutableSet *set);
 
 	/** This function creates an element variable over a set. */
 
@@ -49,8 +49,8 @@ public:
 
 	/** This function creates an element constrant. */
 	Element *getElementConst(VarType type, uint64_t value);
-	
-	Set* getElementRange (Element* element);
+
+	Set *getElementRange (Element *element);
 
 	BooleanEdge getBooleanTrue();
 
@@ -132,25 +132,32 @@ public:
 	bool isFalse(BooleanEdge b);
 
 	void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
-
 	bool isUnSAT() { return unsat; }
 
+	void printConstraint(BooleanEdge boolean);
+	void printConstraints();
+
 	Vector<Order *> *getOrders() { return &allOrders;}
-	HashsetOrder * getActiveOrders() { return &activeOrders;}
+	HashsetOrder *getActiveOrders() { return &activeOrders;}
 
 	Tuner *getTuner() { return tuner; }
 
-	SetIteratorBooleanEdge * getConstraints() { return constraints.iterator(); }
+	SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
 
 	SATEncoder *getSATEncoder() {return satEncoder;}
 
 	void replaceBooleanWithTrue(BooleanEdge bexpr);
 	void replaceBooleanWithTrueNoRemove(BooleanEdge bexpr);
+	void replaceBooleanWithFalseNoRemove(BooleanEdge bexpr);
 	void replaceBooleanWithFalse(BooleanEdge bexpr);
 	void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
 	CSolver *clone();
 	void serialize();
+	static CSolver *deserialize(const char *file);
 	void autoTune(uint budget);
+	void inferFixedOrders();
+	void inferFixedOrder(Order *order);
+
 
 	void setTuner(Tuner *_tuner) { tuner = _tuner; }
 	long long getElapsedTime() { return elapsedTime; }
@@ -189,7 +196,7 @@ private:
 	Vector<Order *> allOrders;
 
 	HashsetOrder activeOrders;
-	
+
 	/** This is a vector of all function structs that we have allocated. */
 	Vector<Function *> allFunctions;