1)Making naiveencoder and encoding graph use tuner 2)Adding timeout to the sat solver...

[satune.git] / src / Backend / satencoder.h

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 0ccf31cfcdcb012ee00a533e81e1ed788dfea2c3..2b2b42a333a10e410c5dff983bfad437433e87e7 100644 (file)
--- 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();
@@ -62,6 +62,7 @@ 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;