- int 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");
- time2 = getTimeNano();
- elapsedTime = time2 - startTime;
- model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+ int result = IS_INDETER;
+ if(alloyEncoder != NULL){
+ alloyEncoder->encode();
+ result = alloyEncoder->solve();
+ }else{
+ 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");
+ time2 = getTimeNano();
+ elapsedTime = time2 - startTime;
+ model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+ }