#include "function.h"
#include "satencoder.h"
#include "sattranslator.h"
+#include "tunable.h"
+#include "orderencoder.h"
+#include "polarityassignment.h"
CSolver *allocCSolver() {
CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
+ This->unsat = false;
This->constraints = allocDefHashSetBoolean();
This->allBooleans = allocDefVectorBoolean();
This->allSets = allocDefVectorSet();
This->allTables = allocDefVectorTable();
This->allOrders = allocDefVectorOrder();
This->allFunctions = allocDefVectorFunction();
- This->satEncoder = allocSATEncoder();
+ This->tuner = allocTuner();
+ This->satEncoder = allocSATEncoder(This);
return This;
}
}
deleteVectorFunction(This->allFunctions);
deleteSATEncoder(This->satEncoder);
+ deleteTuner(This->tuner);
ourfree(This);
}
int startEncoding(CSolver *This) {
naiveEncodingDecision(This);
SATEncoder *satEncoder = This->satEncoder;
+ computePolarities(This);
+ orderAnalysis(This);
encodeAllSATEncoder(This, satEncoder);
int result = solveCNF(satEncoder->cnf);
model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);