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

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 0ccf31c..827a904 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,7 @@ private:
 	void generateElementEncoding(Element *element);
 	Edge encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint);
 	Edge encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint);
+	Edge encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint);
 	void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
 	Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
 	Edge encodeOrderSATEncoder(BooleanOrder *constraint);
@@ -62,11 +63,13 @@ private:
 	void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
 	void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
 	void generateAnyValueBinaryIndexEncoding(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);