From 8b74ebb2b6ebc5466ac2462c13cffb8b0d555379 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Tue, 8 Feb 2022 04:18:55 -0500 Subject: [PATCH 1/4] adding new solver engine and shell script --- scripts/ga-infer.sh | 12 ++ .../solver/UniverseGASolverEngine.java | 137 ++++++++++++++++++ 2 files changed, 149 insertions(+) create mode 100755 scripts/ga-infer.sh create mode 100644 src/main/java/universe/solver/UniverseGASolverEngine.java diff --git a/scripts/ga-infer.sh b/scripts/ga-infer.sh new file mode 100755 index 0000000..9981f7a --- /dev/null +++ b/scripts/ga-infer.sh @@ -0,0 +1,12 @@ +#!/bin/bash +set -e + +export MYDIR=`dirname $0` +. ./$MYDIR/setup.sh + +CHECKER=universe.UniverseInferenceChecker + +SOLVER=universe.solver.UniverseGASolverEngine +IS_HACK=true + +$CFI/scripts/inference-dev --checker "$CHECKER" --solver "$SOLVER" --solverArgs="collectStatistics=true,outputCNF=true" --hacks="$IS_HACK" -m ROUNDTRIP -afud ./annotated "$@" diff --git a/src/main/java/universe/solver/UniverseGASolverEngine.java b/src/main/java/universe/solver/UniverseGASolverEngine.java new file mode 100644 index 0000000..6bfeeaf --- /dev/null +++ b/src/main/java/universe/solver/UniverseGASolverEngine.java @@ -0,0 +1,137 @@ +package universe.solver; + +import checkers.inference.model.Constraint; +import checkers.inference.model.Slot; +import checkers.inference.solver.SolverEngine; +import checkers.inference.solver.backend.Solver; +import checkers.inference.solver.backend.SolverFactory; +import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolver; +import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolverFactory; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; +import checkers.inference.solver.backend.maxsat.MaxSatSolverFactory; +import checkers.inference.solver.frontend.Lattice; +import checkers.inference.solver.util.SolverEnvironment; +import io.jenetics.IntegerGene; +import io.jenetics.MeanAlterer; +import io.jenetics.Mutator; +import io.jenetics.Optimize; +import io.jenetics.RouletteWheelSelector; +import io.jenetics.TournamentSelector; +import io.jenetics.engine.Codecs; +import io.jenetics.engine.Engine; +import io.jenetics.engine.EvolutionResult; +import io.jenetics.engine.EvolutionStatistics; +import io.jenetics.util.IntRange; +import org.sat4j.maxsat.WeightedMaxSatDecorator; +import org.sat4j.maxsat.reader.WDimacsReader; +import org.sat4j.pb.IPBSolver; +import org.sat4j.reader.ParseFormatException; +import org.sat4j.specs.ContradictionException; +import org.sat4j.specs.TimeoutException; + +import javax.lang.model.element.AnnotationMirror; +import java.io.ByteArrayInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.nio.charset.StandardCharsets; +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import java.util.Map; + +import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; +import static io.jenetics.engine.Limits.bySteadyFitness; + +public class UniverseGASolverEngine extends SolverEngine { + @Override + protected SolverFactory createSolverFactory() { + return new GeneticMaxSatSolverFactory() { + @Override + public MaxSatFormatTranslator createFormatTranslator(Lattice lattice) { + return new UniverseFormatTranslator(lattice); + } + + @Override + public Solver createSolver(SolverEnvironment solverEnvironment, Collection slots, + Collection constraints, Lattice lattice) { + MaxSatFormatTranslator formatTranslator = createFormatTranslator(lattice); + return new GeneticMaxSatSolver(solverEnvironment, slots, constraints, formatTranslator, lattice){ + + public int fitness(final int[] chromosome) { + IPBSolver solver = org.sat4j.maxsat.SolverFactory.newDefault();; + WDimacsReader reader = new WDimacsReader(new WeightedMaxSatDecorator(solver)); + Map solutions; + int fitness_count = 0; + + String WCNFModInput = changeSoftWeights(chromosome, this.softWeightsCounter, this.wcnfFileContent, false); + + InputStream stream = new ByteArrayInputStream(WCNFModInput.getBytes(StandardCharsets.UTF_8)); + + try { + solver = (IPBSolver) reader.parseInstance(stream); + } catch (ContradictionException | IOException | ParseFormatException e) { + System.out.println(e); + } + + try { + if (solver.isSatisfiable()){ + solutions = decode(solver.model()); + + List sol = new ArrayList<>(solutions.values()); + + for (AnnotationMirror sol_0 : sol){ + if (sol_0.toString().equals("@universe.qual.Rep")) + { + fitness_count += 1; + } + } + } + else { + System.out.println("UNSAT at " + chromosome[0]); + } + } catch (TimeoutException e) { + e.printStackTrace(); + } + +// System.out.println("Rep count: " + fitness_count); + + return fitness_count; + } + + @Override + public void fit() { + final Engine engine = Engine + .builder( + this::fitness, + Codecs.ofVector(IntRange.of(0, 700), this.uniqueSoftWeightsCount)) + .populationSize(500) + .offspringFraction(0.7) + .survivorsSelector(new RouletteWheelSelector<>()) + .offspringSelector(new TournamentSelector<>()) + .optimize(Optimize.MAXIMUM) + .alterers( + new Mutator<>(0.03), + new MeanAlterer<>(0.6)) + .build(); + + final EvolutionStatistics + statistics = EvolutionStatistics.ofNumber(); + + final EvolutionResult best_res = engine.stream() + .limit(bySteadyFitness(7)) + .limit(100) + .peek(statistics) + .collect(toBestEvolutionResult()); + + System.out.println(statistics); + System.out.println(best_res.genotypes().length()); + System.out.println(best_res.bestPhenotype()); + System.out.println(best_res.worstPhenotype()); + } + + }; + } + + }; + } +} From 1f1ca3c80bd39f16ed68b7a1b5d1b6c3aced43b9 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Tue, 8 Feb 2022 08:01:37 -0500 Subject: [PATCH 2/4] cleanup and added all soft weights to chromosome --- scripts/infer.sh | 2 +- .../universe/UniverseInferenceVisitor.java | 5 + .../solver/GeneticMaxSatSolverFactory.java | 30 +++++ .../solver/UniverseGASolverEngine.java | 101 ++------------ .../solver/UniverseGeneticMaxSatSolver.java | 123 ++++++++++++++++++ 5 files changed, 167 insertions(+), 94 deletions(-) create mode 100644 src/main/java/universe/solver/GeneticMaxSatSolverFactory.java create mode 100644 src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java diff --git a/scripts/infer.sh b/scripts/infer.sh index e0a85fb..a7d8f0a 100755 --- a/scripts/infer.sh +++ b/scripts/infer.sh @@ -9,4 +9,4 @@ CHECKER=universe.UniverseInferenceChecker SOLVER=universe.solver.UniverseSolverEngine IS_HACK=true -$CFI/scripts/inference-dev --checker "$CHECKER" --solver "$SOLVER" --solverArgs="collectStatistics=true" --hacks="$IS_HACK" -m ROUNDTRIP -afud ./annotated "$@" +$CFI/scripts/inference-dev --checker "$CHECKER" --solver "$SOLVER" --solverArgs="collectStatistics=true,outputCNF=true" --hacks="$IS_HACK" -m ROUNDTRIP -afud ./annotated "$@" diff --git a/src/main/java/universe/UniverseInferenceVisitor.java b/src/main/java/universe/UniverseInferenceVisitor.java index 25bd4c2..22c48fb 100644 --- a/src/main/java/universe/UniverseInferenceVisitor.java +++ b/src/main/java/universe/UniverseInferenceVisitor.java @@ -3,6 +3,7 @@ import static universe.UniverseAnnotationMirrorHolder.ANY; import static universe.UniverseAnnotationMirrorHolder.BOTTOM; import static universe.UniverseAnnotationMirrorHolder.LOST; +import static universe.UniverseAnnotationMirrorHolder.PEER; import static universe.UniverseAnnotationMirrorHolder.REP; import static universe.UniverseAnnotationMirrorHolder.SELF; @@ -92,6 +93,10 @@ public Void visitVariable(VariableTree node, Void p) { InferenceMain.getInstance().getConstraintManager(); ConstantSlot rep = slotManager.createConstantSlot(REP); constraintManager.addPreferenceConstraint((VariableSlot) slot, rep, 80); + ConstantSlot peer = slotManager.createConstantSlot(PEER); + constraintManager.addPreferenceConstraint((VariableSlot) slot, peer, 50); + ConstantSlot any = slotManager.createConstantSlot(ANY); + constraintManager.addPreferenceConstraint((VariableSlot) slot, any, 10); } } return super.visitVariable(node, p); diff --git a/src/main/java/universe/solver/GeneticMaxSatSolverFactory.java b/src/main/java/universe/solver/GeneticMaxSatSolverFactory.java new file mode 100644 index 0000000..079020d --- /dev/null +++ b/src/main/java/universe/solver/GeneticMaxSatSolverFactory.java @@ -0,0 +1,30 @@ +package universe.solver; + +import java.util.Collection; + +import checkers.inference.model.Constraint; +import checkers.inference.model.Slot; +import checkers.inference.solver.backend.AbstractSolverFactory; +import checkers.inference.solver.backend.Solver; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; +import checkers.inference.solver.frontend.Lattice; +import checkers.inference.solver.util.SolverEnvironment; + +public class GeneticMaxSatSolverFactory extends AbstractSolverFactory { + + @Override + public MaxSatFormatTranslator createFormatTranslator(Lattice lattice) { + return new UniverseFormatTranslator(lattice); + } + + @Override + public Solver createSolver( + SolverEnvironment solverEnvironment, + Collection slots, + Collection constraints, + Lattice lattice) { + MaxSatFormatTranslator formatTranslator = createFormatTranslator(lattice); + return new UniverseGeneticMaxSatSolver(solverEnvironment, slots, constraints, formatTranslator, lattice); + } +} + diff --git a/src/main/java/universe/solver/UniverseGASolverEngine.java b/src/main/java/universe/solver/UniverseGASolverEngine.java index 6bfeeaf..0b532c3 100644 --- a/src/main/java/universe/solver/UniverseGASolverEngine.java +++ b/src/main/java/universe/solver/UniverseGASolverEngine.java @@ -1,16 +1,19 @@ package universe.solver; +import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; +import static io.jenetics.engine.Limits.bySteadyFitness; + import checkers.inference.model.Constraint; import checkers.inference.model.Slot; import checkers.inference.solver.SolverEngine; import checkers.inference.solver.backend.Solver; import checkers.inference.solver.backend.SolverFactory; import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolver; -import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolverFactory; +//import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolverFactory; import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; -import checkers.inference.solver.backend.maxsat.MaxSatSolverFactory; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.SolverEnvironment; + import io.jenetics.IntegerGene; import io.jenetics.MeanAlterer; import io.jenetics.Mutator; @@ -22,6 +25,7 @@ import io.jenetics.engine.EvolutionResult; import io.jenetics.engine.EvolutionStatistics; import io.jenetics.util.IntRange; + import org.sat4j.maxsat.WeightedMaxSatDecorator; import org.sat4j.maxsat.reader.WDimacsReader; import org.sat4j.pb.IPBSolver; @@ -29,7 +33,6 @@ import org.sat4j.specs.ContradictionException; import org.sat4j.specs.TimeoutException; -import javax.lang.model.element.AnnotationMirror; import java.io.ByteArrayInputStream; import java.io.IOException; import java.io.InputStream; @@ -39,99 +42,11 @@ import java.util.List; import java.util.Map; -import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; -import static io.jenetics.engine.Limits.bySteadyFitness; +import javax.lang.model.element.AnnotationMirror; public class UniverseGASolverEngine extends SolverEngine { @Override protected SolverFactory createSolverFactory() { - return new GeneticMaxSatSolverFactory() { - @Override - public MaxSatFormatTranslator createFormatTranslator(Lattice lattice) { - return new UniverseFormatTranslator(lattice); - } - - @Override - public Solver createSolver(SolverEnvironment solverEnvironment, Collection slots, - Collection constraints, Lattice lattice) { - MaxSatFormatTranslator formatTranslator = createFormatTranslator(lattice); - return new GeneticMaxSatSolver(solverEnvironment, slots, constraints, formatTranslator, lattice){ - - public int fitness(final int[] chromosome) { - IPBSolver solver = org.sat4j.maxsat.SolverFactory.newDefault();; - WDimacsReader reader = new WDimacsReader(new WeightedMaxSatDecorator(solver)); - Map solutions; - int fitness_count = 0; - - String WCNFModInput = changeSoftWeights(chromosome, this.softWeightsCounter, this.wcnfFileContent, false); - - InputStream stream = new ByteArrayInputStream(WCNFModInput.getBytes(StandardCharsets.UTF_8)); - - try { - solver = (IPBSolver) reader.parseInstance(stream); - } catch (ContradictionException | IOException | ParseFormatException e) { - System.out.println(e); - } - - try { - if (solver.isSatisfiable()){ - solutions = decode(solver.model()); - - List sol = new ArrayList<>(solutions.values()); - - for (AnnotationMirror sol_0 : sol){ - if (sol_0.toString().equals("@universe.qual.Rep")) - { - fitness_count += 1; - } - } - } - else { - System.out.println("UNSAT at " + chromosome[0]); - } - } catch (TimeoutException e) { - e.printStackTrace(); - } - -// System.out.println("Rep count: " + fitness_count); - - return fitness_count; - } - - @Override - public void fit() { - final Engine engine = Engine - .builder( - this::fitness, - Codecs.ofVector(IntRange.of(0, 700), this.uniqueSoftWeightsCount)) - .populationSize(500) - .offspringFraction(0.7) - .survivorsSelector(new RouletteWheelSelector<>()) - .offspringSelector(new TournamentSelector<>()) - .optimize(Optimize.MAXIMUM) - .alterers( - new Mutator<>(0.03), - new MeanAlterer<>(0.6)) - .build(); - - final EvolutionStatistics - statistics = EvolutionStatistics.ofNumber(); - - final EvolutionResult best_res = engine.stream() - .limit(bySteadyFitness(7)) - .limit(100) - .peek(statistics) - .collect(toBestEvolutionResult()); - - System.out.println(statistics); - System.out.println(best_res.genotypes().length()); - System.out.println(best_res.bestPhenotype()); - System.out.println(best_res.worstPhenotype()); - } - - }; - } - - }; + return new GeneticMaxSatSolverFactory(); } } diff --git a/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java b/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java new file mode 100644 index 0000000..32f4f4c --- /dev/null +++ b/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java @@ -0,0 +1,123 @@ +package universe.solver; + +import checkers.inference.model.Constraint; +import checkers.inference.model.Slot; +import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolver; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; +import checkers.inference.solver.frontend.Lattice; +import checkers.inference.solver.util.SolverEnvironment; +import io.jenetics.IntegerGene; +import io.jenetics.MeanAlterer; +import io.jenetics.Mutator; +import io.jenetics.Optimize; +import io.jenetics.RouletteWheelSelector; +import io.jenetics.TournamentSelector; +import io.jenetics.engine.Codecs; +import io.jenetics.engine.Engine; +import io.jenetics.engine.EvolutionResult; +import io.jenetics.engine.EvolutionStatistics; +import io.jenetics.util.IntRange; +import org.sat4j.maxsat.WeightedMaxSatDecorator; +import org.sat4j.maxsat.reader.WDimacsReader; +import org.sat4j.pb.IPBSolver; +import org.sat4j.reader.ParseFormatException; +import org.sat4j.specs.ContradictionException; +import org.sat4j.specs.TimeoutException; + +import javax.lang.model.element.AnnotationMirror; +import java.io.ByteArrayInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.nio.charset.StandardCharsets; +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import java.util.Map; + +import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; +import static io.jenetics.engine.Limits.bySteadyFitness; + +public class UniverseGeneticMaxSatSolver extends GeneticMaxSatSolver { + public UniverseGeneticMaxSatSolver(SolverEnvironment solverEnvironment, Collection slots, Collection constraints, MaxSatFormatTranslator formatTranslator, Lattice lattice) { + super(solverEnvironment, slots, constraints, formatTranslator, lattice); + } + + public int fitness(final int[] chromosome) { + IPBSolver solver = org.sat4j.maxsat.SolverFactory.newDefault(); + WDimacsReader reader = + new WDimacsReader(new WeightedMaxSatDecorator(solver)); + Map solutions; + int fitness_count = 0; + + String WCNFModInput = + changeSoftWeights( + chromosome, + this.wcnfFileContent, + false); + + InputStream stream = + new ByteArrayInputStream( + WCNFModInput.getBytes(StandardCharsets.UTF_8)); + + try { + solver = (IPBSolver) reader.parseInstance(stream); + } catch (ContradictionException | IOException | ParseFormatException e) { + System.out.println(e); + } + + try { + if (solver.isSatisfiable()) { + solutions = decode(solver.model()); + + List sol = new ArrayList<>(solutions.values()); + + for (AnnotationMirror sol_0 : sol) { + if (sol_0.toString().equals("@universe.qual.Rep")) { + fitness_count += 1; + } + } + } else { + System.out.println("UNSAT at " + chromosome[0]); + } + } catch (TimeoutException e) { + e.printStackTrace(); + } + + // System.out.println("Rep count: " + fitness_count); + + return fitness_count; + } + + @Override + public void fit() { + final Engine engine = + Engine.builder( + this::fitness, + Codecs.ofVector( + IntRange.of(0, 700), + this.allSoftWeightsCount)) + .populationSize(500) + .offspringFraction(0.7) + .survivorsSelector(new RouletteWheelSelector<>()) + .offspringSelector(new TournamentSelector<>()) + .optimize(Optimize.MAXIMUM) + .alterers(new Mutator<>(0.03), new MeanAlterer<>(0.6)) + .build(); + + final EvolutionStatistics statistics = + EvolutionStatistics.ofNumber(); + + final EvolutionResult best_res = + engine.stream() + .limit(bySteadyFitness(7)) + .limit(100) + .peek(statistics) + .collect(toBestEvolutionResult()); + + System.out.println(statistics); + System.out.println("Genotype length: " + best_res.genotypes().length()); + System.out.println("Best Phenotype: " + best_res.bestPhenotype()); + System.out.println("Worst Phenotype: " + best_res.worstPhenotype()); + } + +} From 6668a3389cd941640bc5deea583b8c56845f8b36 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Tue, 8 Feb 2022 08:16:23 -0500 Subject: [PATCH 3/4] added comments --- .../solver/UniverseGASolverEngine.java | 41 ------------------- .../solver/UniverseGeneticMaxSatSolver.java | 3 ++ 2 files changed, 3 insertions(+), 41 deletions(-) diff --git a/src/main/java/universe/solver/UniverseGASolverEngine.java b/src/main/java/universe/solver/UniverseGASolverEngine.java index 0b532c3..5f441d4 100644 --- a/src/main/java/universe/solver/UniverseGASolverEngine.java +++ b/src/main/java/universe/solver/UniverseGASolverEngine.java @@ -1,48 +1,7 @@ package universe.solver; -import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; -import static io.jenetics.engine.Limits.bySteadyFitness; - -import checkers.inference.model.Constraint; -import checkers.inference.model.Slot; import checkers.inference.solver.SolverEngine; -import checkers.inference.solver.backend.Solver; import checkers.inference.solver.backend.SolverFactory; -import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolver; -//import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolverFactory; -import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; -import checkers.inference.solver.frontend.Lattice; -import checkers.inference.solver.util.SolverEnvironment; - -import io.jenetics.IntegerGene; -import io.jenetics.MeanAlterer; -import io.jenetics.Mutator; -import io.jenetics.Optimize; -import io.jenetics.RouletteWheelSelector; -import io.jenetics.TournamentSelector; -import io.jenetics.engine.Codecs; -import io.jenetics.engine.Engine; -import io.jenetics.engine.EvolutionResult; -import io.jenetics.engine.EvolutionStatistics; -import io.jenetics.util.IntRange; - -import org.sat4j.maxsat.WeightedMaxSatDecorator; -import org.sat4j.maxsat.reader.WDimacsReader; -import org.sat4j.pb.IPBSolver; -import org.sat4j.reader.ParseFormatException; -import org.sat4j.specs.ContradictionException; -import org.sat4j.specs.TimeoutException; - -import java.io.ByteArrayInputStream; -import java.io.IOException; -import java.io.InputStream; -import java.nio.charset.StandardCharsets; -import java.util.ArrayList; -import java.util.Collection; -import java.util.List; -import java.util.Map; - -import javax.lang.model.element.AnnotationMirror; public class UniverseGASolverEngine extends SolverEngine { @Override diff --git a/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java b/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java index 32f4f4c..a399bdd 100644 --- a/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java +++ b/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java @@ -42,6 +42,9 @@ public UniverseGeneticMaxSatSolver(SolverEnvironment solverEnvironment, Collecti super(solverEnvironment, slots, constraints, formatTranslator, lattice); } + /** + * The fitness function in this case is the count of {@link universe.qual.Rep} + */ public int fitness(final int[] chromosome) { IPBSolver solver = org.sat4j.maxsat.SolverFactory.newDefault(); WDimacsReader reader = From d7da066dd94304f4d361e7ba45fa69d734e09c85 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Wed, 16 Feb 2022 16:00:09 -0500 Subject: [PATCH 4/4] formatted files --- .../solver/GeneticMaxSatSolverFactory.java | 8 ++-- .../solver/UniverseGeneticMaxSatSolver.java | 42 +++++++++---------- 2 files changed, 23 insertions(+), 27 deletions(-) diff --git a/src/main/java/universe/solver/GeneticMaxSatSolverFactory.java b/src/main/java/universe/solver/GeneticMaxSatSolverFactory.java index 079020d..8573593 100644 --- a/src/main/java/universe/solver/GeneticMaxSatSolverFactory.java +++ b/src/main/java/universe/solver/GeneticMaxSatSolverFactory.java @@ -1,7 +1,5 @@ package universe.solver; -import java.util.Collection; - import checkers.inference.model.Constraint; import checkers.inference.model.Slot; import checkers.inference.solver.backend.AbstractSolverFactory; @@ -10,6 +8,8 @@ import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.SolverEnvironment; +import java.util.Collection; + public class GeneticMaxSatSolverFactory extends AbstractSolverFactory { @Override @@ -24,7 +24,7 @@ public Solver createSolver( Collection constraints, Lattice lattice) { MaxSatFormatTranslator formatTranslator = createFormatTranslator(lattice); - return new UniverseGeneticMaxSatSolver(solverEnvironment, slots, constraints, formatTranslator, lattice); + return new UniverseGeneticMaxSatSolver( + solverEnvironment, slots, constraints, formatTranslator, lattice); } } - diff --git a/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java b/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java index a399bdd..7c85d50 100644 --- a/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java +++ b/src/main/java/universe/solver/UniverseGeneticMaxSatSolver.java @@ -1,11 +1,15 @@ package universe.solver; +import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; +import static io.jenetics.engine.Limits.bySteadyFitness; + import checkers.inference.model.Constraint; import checkers.inference.model.Slot; import checkers.inference.solver.backend.geneticmaxsat.GeneticMaxSatSolver; import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.SolverEnvironment; + import io.jenetics.IntegerGene; import io.jenetics.MeanAlterer; import io.jenetics.Mutator; @@ -17,6 +21,7 @@ import io.jenetics.engine.EvolutionResult; import io.jenetics.engine.EvolutionStatistics; import io.jenetics.util.IntRange; + import org.sat4j.maxsat.WeightedMaxSatDecorator; import org.sat4j.maxsat.reader.WDimacsReader; import org.sat4j.pb.IPBSolver; @@ -24,7 +29,6 @@ import org.sat4j.specs.ContradictionException; import org.sat4j.specs.TimeoutException; -import javax.lang.model.element.AnnotationMirror; import java.io.ByteArrayInputStream; import java.io.IOException; import java.io.InputStream; @@ -34,33 +38,29 @@ import java.util.List; import java.util.Map; -import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; -import static io.jenetics.engine.Limits.bySteadyFitness; +import javax.lang.model.element.AnnotationMirror; public class UniverseGeneticMaxSatSolver extends GeneticMaxSatSolver { - public UniverseGeneticMaxSatSolver(SolverEnvironment solverEnvironment, Collection slots, Collection constraints, MaxSatFormatTranslator formatTranslator, Lattice lattice) { + public UniverseGeneticMaxSatSolver( + SolverEnvironment solverEnvironment, + Collection slots, + Collection constraints, + MaxSatFormatTranslator formatTranslator, + Lattice lattice) { super(solverEnvironment, slots, constraints, formatTranslator, lattice); } - /** - * The fitness function in this case is the count of {@link universe.qual.Rep} - */ + /** The fitness function in this case is the count of {@link universe.qual.Rep} */ public int fitness(final int[] chromosome) { IPBSolver solver = org.sat4j.maxsat.SolverFactory.newDefault(); - WDimacsReader reader = - new WDimacsReader(new WeightedMaxSatDecorator(solver)); + WDimacsReader reader = new WDimacsReader(new WeightedMaxSatDecorator(solver)); Map solutions; int fitness_count = 0; - String WCNFModInput = - changeSoftWeights( - chromosome, - this.wcnfFileContent, - false); + String WCNFModInput = changeSoftWeights(chromosome, this.wcnfFileContent, false); InputStream stream = - new ByteArrayInputStream( - WCNFModInput.getBytes(StandardCharsets.UTF_8)); + new ByteArrayInputStream(WCNFModInput.getBytes(StandardCharsets.UTF_8)); try { solver = (IPBSolver) reader.parseInstance(stream); @@ -95,10 +95,8 @@ public int fitness(final int[] chromosome) { public void fit() { final Engine engine = Engine.builder( - this::fitness, - Codecs.ofVector( - IntRange.of(0, 700), - this.allSoftWeightsCount)) + this::fitness, + Codecs.ofVector(IntRange.of(0, 700), this.allSoftWeightsCount)) .populationSize(500) .offspringFraction(0.7) .survivorsSelector(new RouletteWheelSelector<>()) @@ -107,8 +105,7 @@ public void fit() { .alterers(new Mutator<>(0.03), new MeanAlterer<>(0.6)) .build(); - final EvolutionStatistics statistics = - EvolutionStatistics.ofNumber(); + final EvolutionStatistics statistics = EvolutionStatistics.ofNumber(); final EvolutionResult best_res = engine.stream() @@ -122,5 +119,4 @@ public void fit() { System.out.println("Best Phenotype: " + best_res.bestPhenotype()); System.out.println("Worst Phenotype: " + best_res.worstPhenotype()); } - }