Adding API for AtMostOneConstraint + bugfix for turning off the optimizations

[satune.git] / src / csolver.h

diff --git a/src/csolver.h b/src/csolver.h
index b27e3c00038d586908d6d17bb80f79a774b7eaed..5ef235d3d8ce9b26032380b30c4cea82c85bd0f2 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -103,6 +103,9 @@ public:
 
        /** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/
        BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize);
+       
+       /** This exactly one element of array can be true! (i.e. a1 => !a2 & !a3 & ... & !an)*/
+       BooleanEdge applyAtMostOneConstraint (BooleanEdge *array, uint asize);
 
        /** This function applies a logical operation to the Booleans in its input. */
 
@@ -141,7 +144,7 @@ public:
        uint64_t getElementValue(Element *element);
 
        void freezeElement(Element *e);
-
+       void turnoffOptimizations(){optimizationsOff = true;}
        /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
        bool getBooleanValue(BooleanEdge boolean);
 
@@ -237,10 +240,12 @@ private:
        bool unsat;
        bool booleanVarUsed;
        bool incrementalMode;
+       bool optimizationsOff;
        Tuner *tuner;
        long long elapsedTime;
        long satsolverTimeout;
        Interpreter *interpreter;
+       bool noOptimization;
        friend class ElementOpt;
        friend class VarOrderingOpt;
 };