Commit b4fbd7a8 authored by Lonca Emmanuel's avatar Lonca Emmanuel
Browse files

Fixed some bugs that made the solver incorrect.

parent 37e71508
Pipeline #174 failed with stage
in 18 seconds
...@@ -68,7 +68,9 @@ public class CountingCtrBuilder { ...@@ -68,7 +68,9 @@ public class CountingCtrBuilder {
exprBuf.append(','); exprBuf.append(',');
} }
varId = list[list.length-1].id; varId = list[list.length-1].id;
exprBuf.append(CtrBuilderUtils.normalizeCspVarName(varId)); final int lastCoeff = coeffs[list.length-1];
final String normName = CtrBuilderUtils.normalizeCspVarName(varId);
exprBuf.append(lastCoeff == 1 ? normName : "mul("+lastCoeff+","+normName+")");
for(int i=0; i<list.length-1; ++i) { for(int i=0; i<list.length-1; ++i) {
exprBuf.append(')'); exprBuf.append(')');
} }
......
...@@ -387,7 +387,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder { ...@@ -387,7 +387,7 @@ public class TseitinBasedIntensionCtrEncoder implements IIntensionCtrEncoder {
Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator(); Iterator<Entry<Integer, Integer>> it2 = mappings.get(1).entrySet().iterator();
while(it2.hasNext()) { while(it2.hasNext()) {
Entry<Integer, Integer> entry2 = it2.next(); Entry<Integer, Integer> entry2 = it2.next();
buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey()==entry2.getKey()?1:0); buildImplVar(ret, entry1.getValue(), entry2.getValue(), entry1.getKey().equals(entry2.getKey())?1:0);
} }
} }
return ret; return ret;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment