X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.h;h=22177772542ae6f5c3100862ec356f071339eb2f;hb=f3afe6e2ef7e4c2bcd95000ea3e1e17f9e538789;hp=25f6918238c99641cd9cc18b0556330c83b1ea2b;hpb=d46ee65a6767e2016cab629220a60c3e39b366f1;p=satune.git

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 25f6918..2217777 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -13,14 +13,16 @@ public:
 	int solve();
 	SATEncoder(CSolver *solver);
 	~SATEncoder();
+	void resetSATEncoder();
 	void encodeAllSATEncoder(CSolver *csolver);
-	Edge encodeConstraintSATEncoder(Boolean *constraint);
+	Edge encodeConstraintSATEncoder(BooleanEdge constraint);
 	CNF *getCNF() { return cnf;}
 	long long getSolveTime() { return cnf->solveTime; }
 	long long getEncodeTime() { return cnf->encodeTime; }
 
 	CMEMALLOC;
 private:
+	void shouldMemoize(Element *elem, uint64_t val, bool & memo);
 	Edge getNewVarSATEncoder();
 	void getArrayNewVarsSATEncoder(uint num, Edge *carray);
 	Edge encodeVarSATEncoder(BooleanVar *constraint);
@@ -30,11 +32,11 @@ private:
 	void encodeElementSATEncoder(Element *element);
 	void encodeElementFunctionSATEncoder(ElementFunction *function);
 	void encodeTableElementFunctionSATEncoder(ElementFunction *This);
-	Edge getElementValueOneHotConstraint(Element *elem, uint64_t value);
-	Edge getElementValueUnaryConstraint(Element *elem, uint64_t value);
-	Edge getElementValueBinaryIndexConstraint(Element *element, uint64_t value);
-	Edge getElementValueBinaryValueConstraint(Element *element, uint64_t value);
-	Edge getElementValueConstraint(Element *element, uint64_t value);
+	Edge getElementValueOneHotConstraint(Element *elem, Polarity p, uint64_t value);
+	Edge getElementValueUnaryConstraint(Element *elem, Polarity p, uint64_t value);
+	Edge getElementValueBinaryIndexConstraint(Element *element, Polarity p, uint64_t value);
+	Edge getElementValueBinaryValueConstraint(Element *element, Polarity p, uint64_t value);
+	Edge getElementValueConstraint(Element *element, Polarity p, uint64_t value);
 	void generateOneHotEncodingVars(ElementEncoding *encoding);
 	void generateUnaryEncodingVars(ElementEncoding *encoding);
 	void generateBinaryIndexEncodingVars(ElementEncoding *encoding);
@@ -47,11 +49,14 @@ private:
 	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);
@@ -60,9 +65,8 @@ private:
 	CNF *cnf;
 	CSolver *solver;
 	BooleanToEdgeMap booledgeMap;
-
+	VectorEdge *vector;
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
 #endif