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

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 56be737..1f8253a 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -44,6 +44,7 @@ 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);
@@ -55,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);
@@ -63,12 +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);