/** 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. */
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);
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;
};