#include "preprocess.h"
#include "serializer.h"
#include "deserializer.h"
+#include "encodinggraph.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
}
void CSolver::serialize() {
+ model_print("serializing ...\n");
{
Serializer serializer("dump");
SetIteratorBooleanEdge *it = getConstraints();
return element;
}
+void CSolver::finalizeMutableSet(MutableSet* set){
+ set->finalize();
+}
+
Element *CSolver::getElementVar(Set *set) {
Element *element = new ElementSet(set);
allElements.push(element);
Element *CSolver::getElementConst(VarType type, uint64_t value) {
uint64_t array[] = {value};
Set *set = new Set(type, array, 1);
- Element *element = new ElementConst(value, type, set);
+ Element *element = new ElementConst(value, set);
Element *e = elemMap.get(element);
if (e == NULL) {
allSets.push(set);
}
BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
- return applyPredicateTable(predicate, inputs, numInputs, NULL);
+ return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
}
BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
IntegerEncodingTransform iet(this);
iet.doTransform();
+ EncodingGraph eg(this);
+ eg.buildGraph();
+ eg.encode();
+
naiveEncodingDecision(this);
satEncoder->encodeAllSATEncoder(this);
int result = unsat ? IS_UNSAT : satEncoder->solve();