X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=src%2Fcsolver.h;h=79428395dcdfe5372277ff6ae9787438d2f94c8c;hb=ef5d7a44cfe435c24e5f104e320b1a81835626e7;hp=92900a19468eb386ce861b8c427e91638279c9d1;hpb=7e245fe6ed87d92eba7da59f94bda439cd682c41;p=satune.git

diff --git a/src/csolver.h b/src/csolver.h
index 92900a1..7942839 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -1,8 +1,10 @@
 #ifndef CSOLVER_H
 #define CSOLVER_H
-#include "classlist.h"
+#include "classes.h"
 #include "ops.h"
-#include "structs.h"
+#include "corestructs.h"
+#include "asthash.h"
+#include "solver_interface.h"
 
 class CSolver {
 public:
@@ -16,6 +18,8 @@ public:
 
 	Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
 
+	Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
+		
 	/** This function creates a mutable set. */
 
 	MutableSet *createMutableSet(VarType type);
@@ -37,6 +41,10 @@ public:
 	/** This function creates an element constrant. */
 	Element *getElementConst(VarType type, uint64_t value);
 
+	Boolean *getBooleanTrue();
+
+	Boolean *getBooleanFalse();
+	
 	/** This function creates a boolean variable. */
 
 	Boolean *getBooleanVar(VarType type);
@@ -79,6 +87,14 @@ public:
 
 	Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
 
+		/** This function applies a logical operation to the Booleans in its input. */
+
+	Boolean *applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2);
+
+	/** This function applies a logical operation to the Booleans in its input. */
+
+	Boolean *applyLogicalOperation(LogicOp op, Boolean *arg);
+
 	/** This function adds a boolean constraint to the set of constraints
 	    to be satisfied */
 
@@ -91,7 +107,7 @@ public:
 	Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
 
 	/** When everything is done, the client calls this function and then csolver starts to encode*/
-	int startEncoding();
+	int solve();
 
 	/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
 	uint64_t getElementValue(Element *element);
@@ -101,6 +117,9 @@ public:
 
 	HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 
+	bool isTrue(Boolean *b);
+	bool isFalse(Boolean *b);
+	
 	void setUnSAT() { unsat = true; }
 
 	bool isUnSAT() { return unsat; }
@@ -108,8 +127,9 @@ public:
 	Vector<Order *> *getOrders() { return &allOrders;}
 
 	Tuner *getTuner() { return tuner; }
+	Transformer* getTransformer() {return transformer;}
 	
-	HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
+	SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
 
 	SATEncoder *getSATEncoder() {return satEncoder;}
 
@@ -119,12 +139,13 @@ public:
 	CSolver *clone();
 	void autoTune(uint budget);
 
+	void setTransformer(Transformer * _transformer) {  transformer = _transformer; }
 	void setTuner(Tuner * _tuner) { tuner = _tuner; }
 	long long getElapsedTime() { return elapsedTime; }
 	long long getEncodeTime();
 	long long getSolveTime();
 	
-	MEMALLOC;
+	CMEMALLOC;
 
 private:
 	void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
@@ -134,7 +155,7 @@ private:
 	void handleORFalse(BooleanLogic *bexpr, Boolean *child);
 
 	/** This is a vector of constraints that must be satisfied. */
-	HashSetBoolean constraints;
+	HashsetBoolean constraints;
 
 	/** This is a vector of all boolean structs that we have allocated. */
 	Vector<Boolean *> allBooleans;
@@ -157,10 +178,17 @@ private:
 	/** This is a vector of all function structs that we have allocated. */
 	Vector<Function *> allFunctions;
 
+	Boolean * boolTrue;
+	Boolean * boolFalse;
+	
+	/** These two tables are used for deduplicating entries. */
+	BooleanMatchMap boolMap;
+	ElementMatchMap elemMap;
+	
 	SATEncoder *satEncoder;
 	bool unsat;
 	Tuner *tuner;
-
+	Transformer* transformer;
 	long long elapsedTime;
 };
 #endif