unsat(false),
booleanVarUsed(false),
incrementalMode(false),
+ optimizationsOff(false),
tuner(NULL),
elapsedTime(0),
satsolverTimeout(NOTIMEOUT),
}
void CSolver::freezeElementsVariables() {
-
- for(uint i=0; i< allElements.getSize(); i++){
+
+ for (uint i = 0; i < allElements.getSize(); i++) {
Element *e = allElements.get(i);
- if(e->frozen){
+ if (e->frozen) {
satEncoder->freezeElementVariables(&e->encoding);
}
}
return applyLogicalOperation(op, newarray, asize);
}
-BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize){
+BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
BooleanEdge newarray[asize + 1];
newarray[asize] = applyLogicalOperation(SATC_OR, array, asize);
- for (uint i=0; i< asize; i++){
+ for (uint i = 0; i < asize; i++) {
BooleanEdge oprand1 = array[i];
- BooleanEdge carray [asize -1];
+ BooleanEdge carray [asize - 1];
uint index = 0;
- for( uint j =0; j< asize; j++){
- if(i != j){
+ for ( uint j = 0; j < asize; j++) {
+ if (i != j) {
BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
carray[index++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
}
}
- ASSERT(index == asize -1);
- newarray[i] = applyLogicalOperation(SATC_AND, carray, asize-1);
+ ASSERT(index == asize - 1);
+ newarray[i] = applyLogicalOperation(SATC_AND, carray, asize - 1);
}
- return applyLogicalOperation(SATC_AND, newarray, asize+1);
+ return applyLogicalOperation(SATC_AND, newarray, asize + 1);
}
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if (!useInterpreter()) {
+ if (!useInterpreter() && !optimizationsOff) {
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
if (isUnSAT()) {
return IS_UNSAT;
}
-
-
+
+
long long startTime = getTimeNano();
bool deleteTuner = false;
if (tuner == NULL) {
}
int result = IS_INDETER;
ASSERT (!useInterpreter());
-
- computePolarities(this);
+ if(!optimizationsOff){
+ computePolarities(this);
+ }
// long long time1 = getTimeNano();
// model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
// Preprocess pp(this);
//Doing element optimization on new constraints
// ElementOpt eop(this);
// eop.doTransform();
-
+
//Since no new element is added, we assuming adding new constraint
//has no impact on previous encoding decisions
// EncodingGraph eg(this);
time2 = getTimeNano();
elapsedTime = time2 - startTime;
model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
-
+
if (deleteTuner) {
delete tuner;
tuner = NULL;
}
delete orderit;
}
+ long long time1, time2;
+
computePolarities(this);
- long long time1 = getTimeNano();
- model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
- Preprocess pp(this);
- pp.doTransform();
- long long time2 = getTimeNano();
- model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
-
- DecomposeOrderTransform dot(this);
- dot.doTransform();
time1 = getTimeNano();
- model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
+ model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+ if(!optimizationsOff){
+ Preprocess pp(this);
+ pp.doTransform();
+ time2 = getTimeNano();
+ model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
- IntegerEncodingTransform iet(this);
- iet.doTransform();
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
+ time1 = getTimeNano();
+ model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
- ElementOpt eop(this);
- eop.doTransform();
+ IntegerEncodingTransform iet(this);
+ iet.doTransform();
- EncodingGraph eg(this);
- eg.encode();
+ ElementOpt eop(this);
+ eop.doTransform();
+ EncodingGraph eg(this);
+ eg.encode();
+ }
naiveEncodingDecision(this);
// eg.validate();
-
- VarOrderingOpt bor(this, satEncoder);
- bor.doTransform();
-
- time2 = getTimeNano();
- model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+ if(!optimizationsOff){
+ VarOrderingOpt bor(this, satEncoder);
+ bor.doTransform();
+ time2 = getTimeNano();
+ model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+ }
satEncoder->encodeAllSATEncoder(this);
time1 = getTimeNano();
model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
model_print("Is problem UNSAT after encoding: %d\n", unsat);
-
+
result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
exit(-1);
}
-void CSolver::freezeElement(Element *e){
+void CSolver::freezeElement(Element *e) {
e->freezeElement();
- if(!incrementalMode){
+ if (!incrementalMode) {
incrementalMode = true;
}
}