X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.h;h=08ec52707c2fe57988df6670022be6263085e888;hb=457ee300c637089a095444672c9d4628faf901e7;hp=94115cefbb467088d2dbcbd68dce9422ba8fc0d0;hpb=83849cbb24f9680d1ca7c09d09ecefc6fe461d66;p=satune.git

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 94115ce..08ec527 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -9,18 +9,18 @@
 typedef Hashtable<Boolean *, Node *, uintptr_t, 4> BooleanToEdgeMap;
 
 class SATEncoder {
- public:
+public:
 	int solve();
 	SATEncoder(CSolver *solver);
 	~SATEncoder();
 	void encodeAllSATEncoder(CSolver *csolver);
-	Edge encodeConstraintSATEncoder(Boolean *constraint);
-	CNF * getCNF() { return cnf;}
+	Edge encodeConstraintSATEncoder(BooleanEdge constraint);
+	CNF *getCNF() { return cnf;}
 	long long getSolveTime() { return cnf->solveTime; }
 	long long getEncodeTime() { return cnf->encodeTime; }
-	
+
 	CMEMALLOC;
- private:
+private:
 	Edge getNewVarSATEncoder();
 	void getArrayNewVarsSATEncoder(uint num, Edge *carray);
 	Edge encodeVarSATEncoder(BooleanVar *constraint);
@@ -47,16 +47,19 @@ class SATEncoder {
 	Edge encodeOrderSATEncoder(BooleanOrder *constraint);
 	Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
 	Edge getPairConstraint(Order *order, OrderPair *pair);
+	Edge getPartialPairConstraint(Order *order, OrderPair *pair);
 	Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint);
 	Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
 	void createAllTotalOrderConstraintsSATEncoder(Order *order);
+	void createAllPartialOrderConstraintsSATEncoder(Order *order);
 	Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
 	Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK);
+	Edge generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki);
 	Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint);
 	Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
 	void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
 	void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
-	
+
 	CNF *cnf;
 	CSolver *solver;
 	BooleanToEdgeMap booledgeMap;
@@ -64,5 +67,4 @@ class SATEncoder {
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
 #endif