bool isFalse(BooleanEdge b);
void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
- void setSatSolverTimeout(long seconds){ satsolverTimeout = seconds;}
+ void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
bool isUnSAT() { return unsat; }
-
+ bool isBooleanVarUsed(){return booleanVarUsed;}
void printConstraint(BooleanEdge boolean);
void printConstraints();
void autoTune(uint budget);
void inferFixedOrders();
void inferFixedOrder(Order *order);
-
-
+ void setAlloyEncoder();
+ bool useAlloyCompiler() {return alloyEncoder != NULL;}
void setTuner(Tuner *_tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
long long getEncodeTime();
SATEncoder *satEncoder;
bool unsat;
- Tuner *tuner;
+ bool booleanVarUsed;
+ Tuner *tuner;
long long elapsedTime;
- long satsolverTimeout;
+ long satsolverTimeout;
+ AlloyEnc *alloyEncoder;
friend class ElementOpt;
+ friend class VarOrderingOpt;
};
inline CompOp flipOp(CompOp op) {