BooleanEdge applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
+ /** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/
+ BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize);
+
/** This function applies a logical operation to the Booleans in its input. */
-
+
BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
/** This function applies a logical operation to the Booleans in its input. */
void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
bool isUnSAT() { return unsat; }
-
+ bool isBooleanVarUsed() {return booleanVarUsed;}
void printConstraint(BooleanEdge boolean);
void printConstraints();
void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
CSolver *clone();
void serialize();
- static CSolver *deserialize(const char *file);
+ static CSolver *deserialize(const char *file, InterpreterType itype = SATUNE);
void autoTune(uint budget);
void inferFixedOrders();
void inferFixedOrder(Order *order);
-
-
+ void setInterpreter(InterpreterType type);
+ bool useInterpreter() {return interpreter != NULL;}
void setTuner(Tuner *_tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
long long getEncodeTime();
long long getSolveTime();
+ long getSatSolverTimeout() { return satsolverTimeout;}
CMEMALLOC;
SATEncoder *satEncoder;
bool unsat;
+ bool booleanVarUsed;
Tuner *tuner;
long long elapsedTime;
long satsolverTimeout;
+ Interpreter *interpreter;
friend class ElementOpt;
friend class VarOrderingOpt;
};