X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.h;h=1f8253ad030e07ef514856a825f210c7c9a47519;hp=0ccf31cfcdcb012ee00a533e81e1ed788dfea2c3;hb=e66c5d1e6f4a25e7f1d5ac01860d59cadcb57250;hpb=7c56d6882d286bd9a1062092fedb081be579641d

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 0ccf31c..1f8253a 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -10,7 +10,7 @@ typedef Hashtable<Boolean *, Node *, uintptr_t, 4> BooleanToEdgeMap;
 
 class SATEncoder {
 public:
-	int solve();
+	int solve(long timeout);
 	SATEncoder(CSolver *solver);
 	~SATEncoder();
 	void resetSATEncoder();
@@ -44,6 +44,8 @@ private:
 	void generateElementEncoding(Element *element);
 	Edge encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint);
 	Edge encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint);
+	Edge encodeUnaryPredicateSATEncoder(BooleanPredicate *constraint);
+	Edge encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint);
 	void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
 	Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
 	Edge encodeOrderSATEncoder(BooleanOrder *constraint);
@@ -54,6 +56,8 @@ private:
 	Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
 	void createAllTotalOrderConstraintsSATEncoder(Order *order);
 	void createAllPartialOrderConstraintsSATEncoder(Order *order);
+	void createAllTotalOrderConstraintsSATEncoderSparse(Order *order);
+	void createAllPartialOrderConstraintsSATEncoderSparse(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);
@@ -62,11 +66,14 @@ private:
 	void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
 	void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
 	void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
+	int getMaximumUsedSize(ElementEncoding *encoding);
+	void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
 	void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
 	CNF *cnf;
 	CSolver *solver;
 	BooleanToEdgeMap booledgeMap;
 	VectorEdge *vector;
+	friend class VarOrderingOpt;
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);