#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->constraints = allocDefVectorBoolean();
+ This->unsat = false;
+ This->constraints = allocDefHashSetBoolean();
This->allBooleans = allocDefVectorBoolean();
This->allSets = allocDefVectorSet();
This->allElements = allocDefVectorElement();
This->allTables = allocDefVectorTable();
This->allOrders = allocDefVectorOrder();
This->allFunctions = allocDefVectorFunction();
- This->satEncoder = allocSATEncoder();
+ This->tuner = allocTuner();
+ This->satEncoder = allocSATEncoder(This);
return This;
}
/** This function tears down the solver and the entire AST */
void deleteSolver(CSolver *This) {
- deleteVectorBoolean(This->constraints);
+ deleteHashSetBoolean(This->constraints);
uint size = getSizeVectorBoolean(This->allBooleans);
for (uint i = 0; i < size; i++) {
}
deleteVectorFunction(This->allFunctions);
deleteSATEncoder(This->satEncoder);
+ deleteTuner(This->tuner);
ourfree(This);
}
}
void addConstraint(CSolver *This, Boolean *constraint) {
- pushVectorBoolean(This->constraints, constraint);
+ addHashSetBoolean(This->constraints, constraint);
}
Order *createOrder(CSolver *This, OrderType type, Set *set) {
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);