#include "orderedge.h"
#include "orderanalysis.h"
#include "elementopt.h"
+#include "varorderingopt.h"
#include <time.h>
#include <stdarg.h>
+#include "alloyenc.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
boolFalse(boolTrue.negate()),
unsat(false),
+ booleanVarUsed(false),
tuner(NULL),
- elapsedTime(0)
+ elapsedTime(0),
+ satsolverTimeout(NOTIMEOUT),
+ alloyEncoder(NULL)
{
satEncoder = new SATEncoder(this);
}
boolTrue = BooleanEdge(new BooleanConst(true));
boolFalse = boolTrue.negate();
unsat = false;
+ booleanVarUsed = false;
elapsedTime = 0;
tuner = NULL;
satEncoder->resetSATEncoder();
}
CSolver *CSolver::deserialize(const char *file) {
- model_print("deserializing ...\n");
+ model_print("deserializing %s ...\n", file);
Deserializer deserializer(file);
return deserializer.deserialize();
}
BooleanEdge CSolver::getBooleanVar(VarType type) {
Boolean *boolean = new BooleanVar(type);
allBooleans.push(boolean);
+ if(!booleanVarUsed)
+ booleanVarUsed = true;
return BooleanEdge(boolean);
}
}
}
-#define NANOSEC 1000000000.0
int CSolver::solve() {
long long startTime = getTimeNano();
bool deleteTuner = false;
eop.doTransform();
EncodingGraph eg(this);
- eg.buildGraph();
eg.encode();
naiveEncodingDecision(this);
// eg.validate();
-
+
+ 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("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+
model_print("Is problem UNSAT after encoding: %d\n", unsat);
- int result = unsat ? IS_UNSAT : satEncoder->solve();
- model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : " 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);
+ }
if (deleteTuner) {
delete tuner;
tuner = NULL;
return result;
}
+void CSolver::setAlloyEncode(){
+ alloyEncoder = new AlloyEnc(this);
+}
+
void CSolver::printConstraints() {
SetIteratorBooleanEdge *it = getConstraints();
while (it->hasNext()) {
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return getElementValueSATTranslator(this, element);
+ return alloyEncoder == NULL? getElementValueSATTranslator(this, element):
+ alloyEncoder->getValue(element);
default:
ASSERT(0);
}