BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
ASSERT(first != second);
+ bool negate = false;
+ if (order->type == SATC_TOTAL) {
+ if (first > second) {
+ uint64_t tmp = first;
+ first = second;
+ second = tmp;
+ negate = true;
+ }
+ }
Boolean *constraint = new BooleanOrder(order, first, second);
- allBooleans.push(constraint);
- return BooleanEdge(constraint);
+ Boolean *b = boolMap.get(constraint);
+
+ if (b == NULL) {
+ allBooleans.push(constraint);
+ boolMap.put(constraint, constraint);
+ constraint->updateParents();
+ } else {
+ delete constraint;
+ constraint = b;
+ }
+
+ BooleanEdge be=BooleanEdge(constraint);
+ return negate ? be.negate() : be;
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if (constraint.isNegated())
- model_print("!");
- constraint.getBoolean()->print();
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
long long startTime = getTimeNano();
computePolarities(this);
- //Preprocess pp(this);
- //pp.doTransform();
-
- //DecomposeOrderTransform dot(this);
- // dot.doTransform();
+ Preprocess pp(this);
+ pp.doTransform();
- //IntegerEncodingTransform iet(this);
- // iet.doTransform();
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
- //EncodingGraph eg(this);
- //eg.buildGraph();
- //eg.encode();
+ IntegerEncodingTransform iet(this);
+ iet.doTransform();
+ EncodingGraph eg(this);
+ eg.buildGraph();
+ eg.encode();
+ printConstraints();
naiveEncodingDecision(this);
satEncoder->encodeAllSATEncoder(this);
model_print("Is problem UNSAT after encoding: %d\n", unsat);
return result;
}
+void CSolver::printConstraints() {
+ SetIteratorBooleanEdge *it = getConstraints();
+ while (it->hasNext()) {
+ BooleanEdge b = it->next();
+ if (b.isNegated())
+ model_print("!");
+ b->print();
+ model_print("\n");
+ }
+ delete it;
+
+}
+
uint64_t CSolver::getElementValue(Element *element) {
switch (element->type) {
case ELEMSET: