boolFalse(boolTrue.negate()),
unsat(false),
tuner(NULL),
- elapsedTime(0)
+ elapsedTime(0),
+ satsolverTimeout(NOTIMEOUT)
{
satEncoder = new SATEncoder(this);
}
}
CSolver *CSolver::deserialize(const char *file) {
- model_print("deserializing ...\n");
+ model_print("deserializing %s ...\n", file);
Deserializer deserializer(file);
return deserializer.deserialize();
}
return set;
}
-bool CSolver::itemExistInSet(Set *set, uint64_t item){
- return set->exists(item);
+bool CSolver::itemExistInSet(Set *set, uint64_t item) {
+ return set->exists(item);
}
VarType CSolver::getSetVarType(Set *set) {
return element;
}
-void CSolver::mustHaveValue(Element *element){
- element->getElementEncoding()->anyValue = true;
+void CSolver::mustHaveValue(Element *element) {
+ element->anyValue = true;
}
Set *CSolver::getElementRange (Element *element) {
#define NANOSEC 1000000000.0
int CSolver::solve() {
- long long starttime = getTimeNano();
+ long long startTime = getTimeNano();
bool deleteTuner = false;
if (tuner == NULL) {
tuner = new DefaultTuner();
delete orderit;
}
computePolarities(this);
- long long time2 = getTimeNano();
- model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
+ long long time1 = getTimeNano();
+ model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
Preprocess pp(this);
pp.doTransform();
- long long time3 = getTimeNano();
- model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
+ long long time2 = getTimeNano();
+ model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
DecomposeOrderTransform dot(this);
dot.doTransform();
- long long time4 = getTimeNano();
- model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC);
+ time1 = getTimeNano();
+ model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
IntegerEncodingTransform iet(this);
iet.doTransform();
eop.doTransform();
EncodingGraph eg(this);
- eg.buildGraph();
eg.encode();
naiveEncodingDecision(this);
- long long time5 = getTimeNano();
- model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);
+// eg.validate();
+
+ time2 = getTimeNano();
+ model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
- long long startTime = getTimeNano();
satEncoder->encodeAllSATEncoder(this);
- long long endTime = getTimeNano();
+ time1 = getTimeNano();
- elapsedTime = endTime - startTime;
- model_print("Elapse Encode time: %f\n", elapsedTime / 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: %d\n", result);
-
+ 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);
if (deleteTuner) {
delete tuner;
tuner = NULL;