Deploy script ...

[satune.git] / src / csolver.h

diff --git a/src/csolver.h b/src/csolver.h
index e02e3407c626928aa9a810a96518ad951a5d5c16..c916c58499992b73450e294a26531801b8cc6791 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -57,7 +57,7 @@ public:
 
        Set *getElementRange (Element *element);
 
-        void mustHaveValue(Element *element);
+       void mustHaveValue(Element *element);
         
        BooleanEdge getBooleanTrue();
 
@@ -159,7 +159,6 @@ public:
        void replaceBooleanWithFalse(BooleanEdge bexpr);
        void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
        CSolver *clone();
-//        Set* addItemsToRange(Element* element, uint num, ...);
        void serialize();
        static CSolver *deserialize(const char *file);
        void autoTune(uint budget);
@@ -220,5 +219,38 @@ private:
        bool unsat;
        Tuner *tuner;
        long long elapsedTime;
+       friend class ElementOpt;
 };
+
+inline CompOp flipOp(CompOp op) {
+       switch (op) {
+       case SATC_EQUALS:
+               return SATC_EQUALS;
+       case SATC_LT:
+               return SATC_GT;
+       case SATC_GT:
+               return SATC_LT;
+       case SATC_LTE:
+               return SATC_GTE;
+       case SATC_GTE:
+               return SATC_LTE;
+       }
+       ASSERT(0);
+}
+
+inline CompOp negateOp(CompOp op) {
+       switch (op) {
+       case SATC_EQUALS:
+               ASSERT(0);
+       case SATC_LT:
+               return SATC_GTE;
+       case SATC_GT:
+               return SATC_LTE;
+       case SATC_LTE:
+               return SATC_GT;
+       case SATC_GTE:
+               return SATC_LT;
+       }
+       ASSERT(0);
+}
 #endif