add cli options for the generation model + add tests #34

Author: arnaud-m

src/main/java/cryptator/config/CryptagenConfig.java

@@ -13,7 +13,7 @@
 
 public class CryptagenConfig extends CryptaCmdConfig {
 
-	@Option(name="-d",handler=ExplicitBooleanOptionHandler.class,usage="dry run (generate but do not solve candidate cryptarithms)")
+	@Option(name="-d",handler=ExplicitBooleanOptionHandler.class, usage="dry run (generate but do not solve candidate cryptarithms)")
 	private boolean dryRun;
 
 	@Option(name="-ctry",usage="country code for doubly true cryptarithms)")
@@ -31,6 +31,11 @@ public class CryptagenConfig extends CryptaCmdConfig {
 	@Option(name="-maxop", usage="maximum number of left operands")
 	private int maxLeftOperands= -1;
 
+	@Option(name="-lightM", handler=ExplicitBooleanOptionHandler.class, usage="use less auxiliary variables")
+	private boolean lightModel;
+	
+	@Option(name="-lightP", handler=ExplicitBooleanOptionHandler.class, usage="use weak consistency")
+	private boolean lightPropagation;
 
 	public final boolean isDryRun() {
 		return dryRun;
@@ -56,9 +61,26 @@ public final int getMaxLeftOperands() {
 		return maxLeftOperands;
 	}
 
+	
+	public final boolean isLightModel() {
+		return lightModel;
+	}
+
+	public final void setLightModel(boolean lightModel) {
+		this.lightModel = lightModel;
+	}
+
+	public final boolean isLightPropagation() {
+		return lightPropagation;
+	}
+
+	public final void setLightPropagation(boolean lightPropagation) {
+		this.lightPropagation = lightPropagation;
+	}
+
 	@Override
 	public String toString() {
-		return super.toString() + "\nc LANG " + langCode + "\nc THREADS " + nthreads;
+		return super.toString() + "\nc LANG " + langCode + "\nc THREADS " + nthreads+"\nc LIGHT_MOD " + lightModel+"\nc LIGHT_PROPAG " + lightPropagation;
 	}
 
 

src/main/java/cryptator/gen/CryptaGenModel.java

@@ -20,20 +20,17 @@
 
 public class CryptaGenModel extends WordsListModel {
 
-	private final ICryptaGenModel left;
+	//private final ICryptaGenModel left;
+	 //private final CryptaMemberScalar left;
+	private final CryptaMemberLen left;
 
 	private final ICryptaGenModel right;
 
-	public CryptaGenModel(String[] words) {
+	public CryptaGenModel(String[] words, boolean lenOrCardModel) {
 		super(new Model("Generate"), words);		
-		//left = new CryptaMemberScalar(model, words, "L_");
-		left = new CryptaMemberScalar(model, words, "L_");
-		//right = new CryptaMemberScalar(model, words, "R_");
-		right = new CryptaMemberScalar(model, words, "R_");
+		left = lenOrCardModel ? new CryptaMemberLen(model, words, "L_") : new CryptaMemberCard(model, words, "L_");
+		right = new CryptaMemberElt(model, words, "R_");
 		this.buildModel();
-//		model.getSolver().showDecisions();
-//		model.getSolver().limitNode(20);
-
 	}
 
 
@@ -42,86 +39,88 @@ public void buildModel() {
 		super.buildModel();
 		left.buildModel();
 		right.buildModel();
-		postLeftOrRightMemberConstraints();
-		postMemberMaxLenConstraint();
+		postLeftOrRightConstraints();
+		postSymBreakLengthLenConstraint();
 	}
-		
 
-	private void postLeftOrRightMemberConstraints() {
+	
+	@Override
+	protected void postMaxLengthConstraints() {
+		model.max(maxLength, left.getMaxLength(), right.getMaxLength()).post();
+	}
+
+
+	private void postLeftOrRightConstraints() {
 		final BoolVar[] l = left.getWordVars();
 		final BoolVar[] r = right.getWordVars();
 		for (int i = 0; i < vwords.length; i++) {
 			l[i].add(r[i]).eq(vwords[i]).post();
 		}
 	}
 
-	
-	private void postMemberMaxLenConstraint() {
-		right.getMaxLength().ge(left.getMaxLength()).post();
-			
+
+	private void postSymBreakLengthLenConstraint() {
+		left.getMaxLength().le(right.getMaxLength());
+
 	}
 
-	public void postMemberCardConstraints(int min, int max) {
-		if(min > 1) left.getWordCount().ge(min).post();
-		else left.getWordCount().ge(2).post();
-		// FIXMW why ?
+	public void postLeftCountConstraints(int min, int max) {
+		min = Math.max(min, 2);
+		left.getWordCount().ge(min).post();
 		if(max >= min) left.getWordCount().le(max).post();
-		
-		// TODO Option to relax the constraint (allow subtractions in the bignum model)
-		// Would need to break reflexion symmetry
-		right.getWordCount().eq(1).post();
+
 	}
-	
-	public void postLeftMinCardConstraints(int base) {
-		IntVar diff = right.getMaxLength().sub(left.getMaxLength()).intVar();
-		final int n = getN();
+
+	public static void postMinLeftCountConstraints(int maxWordCount, IntVar leftCount, IntVar leftMaxLen,IntVar rightMaxLen, int base) {
+		IntVar diff = rightMaxLen.sub(leftMaxLen).intVar();
 		int prod = base;
 		int i = 2;
-		while(prod <= n) {
-			diff.ge(i).imp(left.getWordCount().ge(prod)).post();
+		while(prod <= maxWordCount) {
+			diff.ge(i).imp(leftCount.ge(prod + 1)).post();
 			prod *= base;
 			i++;
 		}
 		diff.lt(i).post();
 	}
-	
-	public void postRightMemberConstraint() {
+
+	public void postMinLeftCountConstraints(int base) {
+		left.postLentghSumConstraints(right.getMaxLength(), base);
+	}
+
+	public void postFixedRightMemberConstraint() {
 		final BoolVar[] vars = right.getWordVars();
 		vars[vars.length - 1].eq(1).post();
 	}
 
 	public void postDoublyTrueConstraint(int lb) {
 		final int n = getN();
 		final IntVar sum = model.intVar("SUM", lb, n - 1);
-		
+
 		final IntVar[] lvars = new IntVar[n+1];
 		System.arraycopy(left.getWordVars(), 0, lvars, 0, n);
 		lvars[n] = sum; 
-		
+
 		final IntVar[] rvars = new IntVar[n+1];
 		System.arraycopy(right.getWordVars(), 0, rvars, 0, n);
 		rvars[n] = sum; 
-		
+
 		final int[] coeffs = ArrayUtils.array(0, n);
 		coeffs[n] = -1;
-		
+
 		model.scalar(lvars, coeffs, "=", 0).post();
 		model.scalar(rvars, coeffs, "=", 0).post();
 	}
 
-	public final ICryptaNode recordCryptarithm() {		
-		// TODO Check that members are non-null. 
-		return new CryptaNode(CryptaOperator.EQ, recordAddition(left), recordAddition(right));
+	public final ICryptaNode recordCryptarithm() {	
+		final ICryptaNode l = recordAddition(left);
+		final ICryptaNode r = recordAddition(right);
+		return r == null || l == null ? null : new CryptaNode(CryptaOperator.EQ, l, r);
 	}
 
 
 	@Override
 	public String toString() {
 		return left.toString() + " = " + right.toString();
 	}
-	
-	
-	
-	
 
 }

src/main/java/cryptator/gen/CryptaListGenerator.java

@@ -57,11 +57,11 @@ public final int getErrorCount() {
 	}
 
 	private CryptaGenModel buildModel() {
-		final CryptaGenModel gen = new CryptaGenModel(words.getWords());
-		gen.postMemberCardConstraints(config.getMinLeftOperands(), config.getMaxLeftOperands());
+		final CryptaGenModel gen = new CryptaGenModel(words.getWords(), config.isLightModel());
+		gen.postLeftCountConstraints(config.getMinLeftOperands(), config.getMaxLeftOperands());
 		gen.postMaxSymbolCountConstraint(config.getArithmeticBase());
-		gen.postLeftMinCardConstraints(config.getArithmeticBase());
-		if(words.hasRightMember()) gen.postRightMemberConstraint();
+		if(!config.isLightPropagation()) gen.postMinLeftCountConstraints(config.getArithmeticBase());
+		if(words.hasRightMember()) gen.postFixedRightMemberConstraint();
 		if(words.isDoublyTrue()) gen.postDoublyTrueConstraint(words.getLB());
 		return gen;
 	}

src/main/java/cryptator/gen/CryptaMemberCard.java

@@ -12,6 +12,7 @@
 import java.util.stream.IntStream;
 
 import org.chocosolver.solver.Model;
+import org.chocosolver.solver.constraints.extension.Tuples;
 import org.chocosolver.solver.variables.IntVar;
 
 public class CryptaMemberCard extends CryptaMemberLen {
@@ -41,6 +42,30 @@ private void postGlobalCardLengthConstraint() {
 		model.globalCardinality(lengths, values, cardLengths, true).post();
 	}
 
+	public void postLentghSumConstraints(IntVar sumLength, int base) {
+
+		int[] maxCardLengths = getLengthCounts(words);
+		final int maxCard = IntStream.of(maxCardLengths).max().orElse(0);
+		
+		IntVar[] vars = Arrays.copyOf(cardLengths, maxCard);
+		vars[0] = model.intVar(0);
+		
+		IntVar x = model.intVar("Xk", 0, maxCard,false);
+		model.element(x, cardLengths, maxLength, 0).post();
+		
+		IntVar y = model.intVar("Yk", 0, maxCard,false);
+		model.element(y, cardLengths, maxLength.sub(1).intVar(), 0).post();
+		
+		IntVar z = model.intVar("Zk", 0, maxCard,false);
+		z.eq(wordCount.sub(x).sub(y)).decompose().post();
+		
+		WordSumTuplesBuilder builder = new WordSumTuplesBuilder(base);
+		Tuples tuples = builder.buildTuples(maxCardLengths);
+		
+		model.table(new IntVar[] {maxLength,  x, y, z, sumLength}, tuples).post();			
+	}
+	
+	
 	@Override
 	public void buildModel() {
 		super.buildModel();

src/main/java/cryptator/gen/CryptaMemberLen.java

@@ -40,4 +40,20 @@ protected void postMaxLengthConstraints() {
 		model.max(maxLength, lengths).post();
 	}
 
+	public void postLentghSumConstraints(IntVar sumLength, int base) {
+		IntVar diff = sumLength.sub(maxLength).intVar();
+		final int n = getN();
+		int prod = base;
+		int i = 2;
+		while(prod <= n) {
+			//System.err.println(i + " " + (prod + 1));
+			diff.ge(i).imp(wordCount.ge(prod + 1)).post();
+			prod *= base;
+			i++;
+		}
+		diff.lt(i).post();
+	}
+
+
+
 }

src/main/java/cryptator/gen/CryptaMemberScalar.java

@@ -17,7 +17,6 @@
 import cryptator.gen.CryptaMemberCard;
 import cryptator.gen.CryptaMemberElt;
 import cryptator.gen.CryptaMemberLen;
-import cryptator.gen.CryptaMemberScalar;
 import cryptator.gen.WordsListModel;
 import cryptator.specs.ICryptaGenModel;
 
@@ -30,7 +29,6 @@ public class GenModelTest {
 	@Before
 	public void buildGenModels() {
 		models = new ICryptaGenModel[] {
-			new CryptaMemberScalar(new Model(), words, ""),
 			new CryptaMemberLen(new Model(), words, ""),
 			new CryptaMemberCard(new Model(), words, ""),
 			new WordsListModel(new Model(), words)

src/test/java/cryptator/GenModelTest.java

@@ -27,49 +27,59 @@ public class GenerateTest {
 	public static void configureTestLoggers() {
 		JULogUtil.configureTestLoggers();
 	}
-	
-	public long testGenerate(WordArray wordArray) throws CryptaModelException {
+
+	public long testGenerate(WordArray wordArray, boolean lightModel, boolean lightPropagation) throws CryptaModelException {
 		final CryptagenConfig config = new CryptagenConfig();
+		config.setLightModel(lightModel);
+		config.setLightPropagation(lightPropagation);
 		final CryptaListGenerator gen = new CryptaListGenerator(wordArray, config, Cryptagen.LOGGER);
 		CryptaBiConsumer cons = new CryptaBiConsumer(Cryptagen.LOGGER);
 		cons.withSolutionCheck(config.getArithmeticBase());
 		gen.generate(cons);
 		assertEquals(0, cons.getErrorCount());
 		return cons.getSolutionCount();
 	}
+
+	
+	public void testGenerate(int expectedSolCount, WordArray wordArray) throws CryptaModelException {
+		assertEquals( expectedSolCount,testGenerate(wordArray, false, false));
+		assertEquals( expectedSolCount,testGenerate(wordArray, false, true));
+		assertEquals( expectedSolCount,testGenerate(wordArray, true, false));
+		assertEquals( expectedSolCount,testGenerate(wordArray, true, true));
+	}
 
-	public long testGenerate(String rightMember, String... words) throws CryptaModelException {
-		return testGenerate(new WordArray(Arrays.asList(words), rightMember));
+	public void testGenerate(int expectedSolCount, String rightMember, String... words) throws CryptaModelException {
+		testGenerate(expectedSolCount, new WordArray(Arrays.asList(words), rightMember));
 	}
 
 	@Test
 	public void testSendMoreMoney() throws CryptaModelException {
-	assertEquals(1, testGenerate(null, "send", "more", "money"));
+	testGenerate(1, null, "send", "more", "money");
 	}
 
 	@Test
 	public void testPlanets1() throws CryptaModelException {
-		assertEquals(2, testGenerate(null, "venus", "earth", "uranus", "saturn"));
+		testGenerate(2, null, "venus", "earth", "uranus", "saturn");
 	}
 
 	@Test
 	public void testPlanets2() throws CryptaModelException {
-		assertEquals(1, testGenerate("planets", "venus", "earth", "uranus", "saturn"));
+		testGenerate(1, "planets", "venus", "earth", "uranus", "saturn");
 	}
 
 	@Test
 	public void testDoublyTrue1() throws CryptaModelException {
-		assertEquals(0, testGenerate(new WordArray("FR", "fr", 0, 10)));
+		testGenerate(0, new WordArray("FR", "fr", 0, 10));
 	}
 
 	@Test
 	public void testDoublyTrue2() throws CryptaModelException {
-		assertEquals(1, testGenerate(new WordArray("FR", "fr", 30, 30)));
+		testGenerate(1, new WordArray("FR", "fr", 30, 30));
 	}
 
 	@Test
 	public void testDoublyTrue3() throws CryptaModelException {
-		assertEquals(3, testGenerate(new WordArray("IT", "it", 20, 30)));
+		testGenerate(3, new WordArray("IT", "it", 20, 30));
 	}