diff --git a/.idea/workspace.xml b/.idea/workspace.xml
index eeb497a56f231fa0dcb5980c7e02f55d557f2866..a9393e0a26aff732125d991213330c3f40522c5e 100644
--- a/.idea/workspace.xml
+++ b/.idea/workspace.xml
@@ -4,12 +4,10 @@
<option name="autoReloadType" value="SELECTIVE" />
</component>
<component name="ChangeListManager">
- <list default="true" id="a17b64ea-8b68-4cd2-aba6-1780c674b35e" name="Changes" comment="Create">
- <change afterPath="$PROJECT_DIR$/src/test/java/fr/univamu/solver/TestInterval.java" afterDir="false" />
- <change afterPath="$PROJECT_DIR$/src/test/java/fr/univamu/solver/TestSolver.java" afterDir="false" />
- <change beforePath="$PROJECT_DIR$/.gitignore" beforeDir="false" afterPath="$PROJECT_DIR$/.gitignore" afterDir="false" />
+ <list default="true" id="a17b64ea-8b68-4cd2-aba6-1780c674b35e" name="Changes" comment="Add tests">
<change beforePath="$PROJECT_DIR$/.idea/workspace.xml" beforeDir="false" afterPath="$PROJECT_DIR$/.idea/workspace.xml" afterDir="false" />
- <change beforePath="$PROJECT_DIR$/src/main/java/fr/univamu/solver/Main.java" beforeDir="false" afterPath="$PROJECT_DIR$/src/main/java/fr/univamu/solver/Main.java" afterDir="false" />
+ <change beforePath="$PROJECT_DIR$/src/main/java/fr/univamu/solver/Interval.java" beforeDir="false" afterPath="$PROJECT_DIR$/src/main/java/fr/univamu/solver/Interval.java" afterDir="false" />
+ <change beforePath="$PROJECT_DIR$/src/main/java/fr/univamu/solver/Solver.java" beforeDir="false" afterPath="$PROJECT_DIR$/src/main/java/fr/univamu/solver/Solver.java" afterDir="false" />
</list>
<option name="SHOW_DIALOG" value="false" />
<option name="HIGHLIGHT_CONFLICTS" value="true" />
@@ -133,7 +131,7 @@
<option name="number" value="Default" />
<option name="presentableId" value="Default" />
<updated>1727967430355</updated>
- <workItem from="1727967431394" duration="749000" />
+ <workItem from="1727967431394" duration="4281000" />
</task>
<task id="LOCAL-00001" summary="Create">
<option name="closed" value="true" />
@@ -151,7 +149,15 @@
<option name="project" value="LOCAL" />
<updated>1727967931296</updated>
</task>
- <option name="localTasksCounter" value="3" />
+ <task id="LOCAL-00003" summary="Add tests">
+ <option name="closed" value="true" />
+ <created>1727968278226</created>
+ <option name="number" value="00003" />
+ <option name="presentableId" value="LOCAL-00003" />
+ <option name="project" value="LOCAL" />
+ <updated>1727968278226</updated>
+ </task>
+ <option name="localTasksCounter" value="4" />
<servers />
</component>
<component name="TypeScriptGeneratedFilesManager">
@@ -159,6 +165,7 @@
</component>
<component name="VcsManagerConfiguration">
<MESSAGE value="Create" />
- <option name="LAST_COMMIT_MESSAGE" value="Create" />
+ <MESSAGE value="Add tests" />
+ <option name="LAST_COMMIT_MESSAGE" value="Add tests" />
</component>
</project>
\ No newline at end of file
diff --git a/src/main/java/fr/univamu/solver/Interval.java b/src/main/java/fr/univamu/solver/Interval.java
index 976e9b741a87c6f598594ff93b5a2c0f2f0e5d22..c035b340a330e16d73891286a4d57241c0afeb9e 100644
--- a/src/main/java/fr/univamu/solver/Interval.java
+++ b/src/main/java/fr/univamu/solver/Interval.java
@@ -1,8 +1,8 @@
package fr.univamu.solver;
public class Interval {
- public static int MIN_VALUE = -1000000000;
- public static int MAX_VALUE = +1000000000;
+ public static int MIN_VALUE = -1_000_000_000;
+ public static int MAX_VALUE = 1_000_000_000;
private int min = MIN_VALUE;
private int max = MAX_VALUE;
@@ -15,7 +15,7 @@ public class Interval {
this.min = min;
this.max = max;
} else {
- this.min = +1;
+ this.min = 1;
this.max = -1;
}
}
@@ -35,13 +35,13 @@ public class Interval {
var oldMin = min;
var oldMax = max;
if (newMin > newMax) {
- min = +1;
+ min = 1;
max = -1;
} else {
- min = (newMin > min) ? newMin : min;
- max = (newMax < max) ? newMax : max;
+ min = Integer.max(newMin, min);
+ max = Integer.min(newMax, max);
if (min > max) {
- min = +1;
+ min = 1;
max = -1;
}
}
@@ -125,7 +125,7 @@ public class Interval {
}
int min = Integer.MAX_VALUE;
int max = Integer.MIN_VALUE;
- int divisors[] = { i.min, -1, 1, i.max };
+ int[] divisors = { i.min, -1, 1, i.max };
for (int divisor : divisors) {
if (divisor == 0)
continue;
@@ -141,8 +141,7 @@ public class Interval {
return new Interval(min, max);
}
- // XXXX
- public Interval div2(Interval i) {
+ public Interval inverseMul(Interval i) {
if (isEmpty() || i.isEmpty()) {
return empty();
}
@@ -151,7 +150,7 @@ public class Interval {
}
int min = Integer.MAX_VALUE;
int max = Integer.MIN_VALUE;
- int divisors[] = { i.min, -1, 1, i.max };
+ int[] divisors = { i.min, -1, 1, i.max };
for (int divisor : divisors) {
if (!i.contains(divisor))
continue;
@@ -165,14 +164,12 @@ public class Interval {
if (getSign() * i.getSign() == 1) {
// same sign, result is > 0
- if (min <= 0)
- min = 1;
+ min = Integer.max(1, min);
}
if (getSign() * i.getSign() == -1) {
// different sign, result is < 0
- if (max >= 0)
- max = -1;
+ max = Integer.min(-1, max);
}
return new Interval(min, max);
diff --git a/src/main/java/fr/univamu/solver/Solver.java b/src/main/java/fr/univamu/solver/Solver.java
index 21a9fec8480f9ac3f443549c7741df8e66b1b5ae..4ca94b1167ac8ca140dab135e961bb11810b0aba 100644
--- a/src/main/java/fr/univamu/solver/Solver.java
+++ b/src/main/java/fr/univamu/solver/Solver.java
@@ -4,415 +4,401 @@ import java.util.LinkedList;
import java.util.List;
class Constraint {
- private char type;
- private Variable result;
- private Variable var1;
- private Variable var2;
-
- public String toString() {
- return String.format("%s(%s,%s,%s)", type, result, var1, var2);
- }
-
- public Constraint(char type, Variable result, Variable var1, Variable var2) {
- this.type = type;
- this.result = result;
- this.var1 = var1;
- this.var2 = var2;
- }
-
- public char getType() {
- return type;
- }
-
- public Variable getResult() {
- return result;
- }
-
- public Variable getVar1() {
- return var1;
- }
-
- public Variable getVar2() {
- return var2;
- }
+ final private char type;
+ final private Variable result;
+ final private Variable var1;
+ final private Variable var2;
+
+ public String toString() {
+ return String.format("%s(%s,%s,%s)", type, result, var1, var2);
+ }
+
+ public Constraint(char type, Variable result, Variable var1, Variable var2) {
+ this.type = type;
+ this.result = result;
+ this.var1 = var1;
+ this.var2 = var2;
+ }
+
+ public char getType() {
+ return type;
+ }
+
+ public Variable getResult() {
+ return result;
+ }
+
+ public Variable getVar1() {
+ return var1;
+ }
+
+ public Variable getVar2() {
+ return var2;
+ }
}
public class Solver {
- private static final int CHECK_INTERVALS_STRATEGY = 1;
- private static final int REDUCE_AND_CHECK_INTERVALS_STRATEGY = 2;
-
- private List<Constraint> constraints = new LinkedList<>();
- private List<Variable> variables = new LinkedList<>();
- private int strategy = CHECK_INTERVALS_STRATEGY;
-
- private long solutionsCounter = 0;
- private long nodesCounter = 0;
- private long maxNodes = 1000_000_000L;
- private boolean verbose = true;
-
- public void reduceAndCheckIntervalsStrategy() {
- strategy = REDUCE_AND_CHECK_INTERVALS_STRATEGY;
- }
-
- private boolean checkAddConstraintIntervalsStrategy(Constraint c) {
- return c.getVar1().add(c.getVar2()).inter(c.getResult()).isNotEmpty();
- }
-
- private boolean checkMulConstraintIntervalsStrategy(Constraint c) {
- return c.getVar1().mul(c.getVar2()).inter(c.getResult()).isNotEmpty();
- }
-
- private boolean checkDivConstraintIntervalsStrategy(Constraint c) {
- return c.getVar1().div(c.getVar2()).inter(c.getResult()).isNotEmpty();
- }
-
- private boolean checkDiffConstraintIntervalsStrategy(Constraint c) {
- var result = c.getResult();
- var ko = result.equals(c.getVar1()) && result.isFixed();
- return (!ko);
- }
-
- private boolean reduceAddConstraint(Constraint c) {
- var change = c.getResult().reduce(c.getVar1().add(c.getVar2()));
- change = c.getVar1().reduce(c.getResult().sub(c.getVar2())) || change;
- change = c.getVar2().reduce(c.getResult().sub(c.getVar1())) || change;
- return change;
- }
-
- private boolean reduceMulConstraint(Constraint c) {
- var change = false;
- for (int i = 0; i < 3; i++) {
- change = c.getResult().reduce(c.getVar1().mul(c.getVar2())) || change;
- change = c.getVar2().reduce(c.getResult().div2(c.getVar1())) || change;
- change = c.getVar1().reduce(c.getResult().div2(c.getVar2())) || change;
- }
- return change;
- }
-
- private boolean checkConstraintIntervalsStrategy(Constraint c) {
- switch (c.getType()) {
- case '+':
- return checkAddConstraintIntervalsStrategy(c);
- case '#':
- return checkDiffConstraintIntervalsStrategy(c);
- case '*':
- return checkMulConstraintIntervalsStrategy(c);
- case '/':
- return checkDivConstraintIntervalsStrategy(c);
- default:
- break;
- }
- throw new IllegalArgumentException("bad constraint: " + c);
- }
-
- private boolean reduce(Constraint c) {
- switch (c.getType()) {
- case '+':
- return reduceAddConstraint(c);
- case '*':
- return reduceMulConstraint(c);
-// case '#':
-// case '/':
- }
- return false;
- }
-
- private boolean checkConstraint(Constraint c) {
- switch (strategy) {
- case CHECK_INTERVALS_STRATEGY:
- case REDUCE_AND_CHECK_INTERVALS_STRATEGY:
- return checkConstraintIntervalsStrategy(c);
- }
- throw new IllegalStateException("bad strategy: " + strategy);
- }
-
- private boolean checkConstraints() {
- for (Constraint c : constraints) {
- if (!checkConstraint(c)) {
- return false;
- }
- }
- return true;
- }
-
- public Variable findVariable() {
- Variable best = null;
- for (Variable v : variables) {
- if (v.isFixed()) {
- // ne pas choisir
- } else if (best == null) {
- best = v;
- } else if (v.getSize() < best.getSize()) {
- best = v;
- }
- }
- return best;
- }
-
- public boolean findSolutions() {
- if (++nodesCounter > maxNodes) {
- throw new IllegalStateException("too many nodes");
- }
- if (checkConstraints() == false) {
- return false;
- }
- var v = findVariable();
- if (v == null) {
- solutionsCounter++;
- if (verbose) {
- variables.stream().filter(Variable::isNamed).forEach(System.out::println);
- System.out.println();
- }
- return true;
- }
-
- boolean result = false;
- int min = v.getMin();
- int max = v.getMax();
-
- // Comment découper le domaine ?
- int step = 1;
- if (v.getSize() > 1000) {
- if (min < 0 && max >= 0) {
- step = -min;
- } else {
- int mid = (min + max) / 2;
- step = (1 + mid - min);
- }
- }
-
- // explorer le domaine
- for (int value = min; value <= max; value += step) {
- v.setMin(value);
- v.setMax(Math.min(value + step - 1, max));
- if (findSolutions()) {
- result = true;
- }
- }
- v.setMin(min);
- v.setMax(max);
- return result;
- }
-
- public Variable newVar() {
- var v = new Variable(variables.size());
- variables.add(v);
- return v;
- }
-
- public Variable newVar(String name) {
- var v = new Variable(name);
- variables.add(v);
- return v;
- }
-
- public Variable newConstant(int value) {
- return newVar().domain(value);
- }
-
- public void eq(Variable a, Variable b) {
- sub(newConstant(0), a, b); // 0 = A - B
- }
-
- public void gt(Variable a, Variable b) {
- sub(newVar().domain(1, Variable.MAX_VALUE), a, b); // Z=A-B,Z>0
- }
-
- public void get(Variable a, Variable b) {
- sub(newVar().domain(0, Variable.MAX_VALUE), a, b); // Z=A-B, Z>=0
- }
-
- public void lt(Variable a, Variable b) {
- gt(b, a);
- }
-
- public void let(Variable a, Variable b) {
- get(b, a);
- }
-
- public void diff(Variable a, Variable b) {
- constraints.add(new Constraint('#', a, b, null));
- }
-
- public void allDiff(Variable... variables) {
- for (int i = 0; i < variables.length; i++)
- for (int j = i + 1; j < variables.length; j++) {
- diff(variables[i], variables[j]);
- }
- }
-
- private void add(Variable result, Variable a, Variable b) {
- constraints.add(new Constraint('+', result, a, b));
- }
-
- private void sub(Variable result, Variable a, Variable b) {
- add(a, result, b);
- }
-
- private void mul(Variable result, Variable a, Variable b) {
- constraints.add(new Constraint('*', result, a, b));
- }
-
- private void div(Variable result, Variable a, Variable b) {
- constraints.add(new Constraint('/', result, a, b));
- }
-
- private Variable parseSimpleTerm(List<Object> terms) {
- var first = terms.removeFirst();
- if (first instanceof Variable var) {
- return var;
- }
- if (first instanceof Integer cst) {
- return this.newConstant(cst);
- }
- throw new IllegalArgumentException("bad expression: " + first);
- }
-
- private boolean parseToken(String token, List<Object> terms) {
- if (!terms.isEmpty()) {
- if (token.equals(terms.getFirst())) {
- terms.removeFirst();
- return true;
- }
- }
- return false;
- }
-
- private Variable parseMultiplicationTerm(List<Object> terms) {
- var first = parseSimpleTerm(terms);
- if (parseToken("*", terms)) {
- var second = parseMultiplicationTerm(terms);
- var result = newVar();
- mul(result, first, second);
- return result;
- }
- if (parseToken("/", terms)) {
- var second = parseMultiplicationTerm(terms);
- var result = newVar();
- div(result, first, second);
- return result;
- }
- return first;
- }
-
- private Variable parseAdditionTerm(List<Object> terms) {
- var first = parseMultiplicationTerm(terms);
- if (parseToken("+", terms)) {
- var second = parseAdditionTerm(terms);
- var result = newVar();
- add(result, first, second);
- return result;
- }
- if (parseToken("-", terms)) {
- var second = parseAdditionTerm(terms);
- var result = newVar();
- add(first, result, second);
- return result;
- }
- return first;
- }
-
- public void addConstraint(Object... terms) {
- var termsList = new LinkedList<>();
- termsList.addAll(List.of(terms));
- var var1 = parseAdditionTerm(termsList);
- var relation = termsList.removeFirst();
- var var2 = parseAdditionTerm(termsList);
- if (!termsList.isEmpty()) {
- throw new IllegalArgumentException("bad expression: " + termsList);
- }
- if (relation instanceof String carRelation) {
- switch (carRelation) {
- case "=":
- eq(var1, var2);
- return;
- case ">":
- gt(var1, var2);
- return;
- case ">=":
- get(var1, var2);
- return;
- case "<":
- lt(var1, var2);
- return;
- case "<=":
- let(var1, var2);
- return;
- case "<>":
- diff(var1, var2);
- return;
- }
- }
- throw new IllegalArgumentException("bad relation: " + relation);
- }
-
- public Variable expression2(Object... terms) {
- var termsList = new LinkedList<>(List.of(terms));
- var result = parseAdditionTerm(termsList);
- if (!termsList.isEmpty()) {
- throw new IllegalArgumentException("bad expression: " + termsList);
- }
- return result;
- }
-
- private void reduce() {
- if (verbose) {
- System.out.println("Variables before reduction:");
- variables.forEach(System.out::println);
- }
-
- for (boolean change = true; change;) {
- change = false;
- for (Constraint c : constraints) {
- if (reduce(c)) {
- change = true;
- }
- }
- }
-
- if (verbose) {
- System.out.println("Variables after reduction:");
- variables.forEach(System.out::println);
- }
- }
-
- public long solve() {
- this.solutionsCounter = 0;
- this.nodesCounter = 0;
- if (strategy == REDUCE_AND_CHECK_INTERVALS_STRATEGY) {
- reduce();
- }
- findSolutions();
- return solutionsCounter;
- }
-
- public int getStrategy() {
- return strategy;
- }
-
- public long getNodesCounter() {
- return nodesCounter;
- }
-
- public long getMaxNodes() {
- return maxNodes;
- }
-
- public void setStrategy(int strategy) {
- this.strategy = strategy;
- }
-
- public void setMaxNodes(long maxNodes) {
- this.maxNodes = maxNodes;
- }
-
- public boolean isVerbose() {
- return verbose;
- }
-
- public void setVerbose(boolean verbose) {
- this.verbose = verbose;
- }
+ private static final int CHECK_INTERVALS_STRATEGY = 1;
+ private static final int REDUCE_AND_CHECK_INTERVALS_STRATEGY = 2;
+
+ private final List<Constraint> constraints = new LinkedList<>();
+ private final List<Variable> variables = new LinkedList<>();
+ private int strategy = CHECK_INTERVALS_STRATEGY;
+
+ private long solutionsCounter = 0;
+ private long nodesCounter = 0;
+ private long maxNodes = 1000_000_000L;
+ private boolean verbose = true;
+
+ public void reduceAndCheckIntervalsStrategy() {
+ strategy = REDUCE_AND_CHECK_INTERVALS_STRATEGY;
+ }
+
+ private boolean checkAddConstraintIntervalsStrategy(Constraint c) {
+ return c.getVar1().add(c.getVar2()).inter(c.getResult()).isNotEmpty();
+ }
+
+ private boolean checkMulConstraintIntervalsStrategy(Constraint c) {
+ return c.getVar1().mul(c.getVar2()).inter(c.getResult()).isNotEmpty();
+ }
+
+ private boolean checkDivConstraintIntervalsStrategy(Constraint c) {
+ return c.getVar1().div(c.getVar2()).inter(c.getResult()).isNotEmpty();
+ }
+
+ private boolean checkDiffConstraintIntervalsStrategy(Constraint c) {
+ var result = c.getResult();
+ var ko = result.equals(c.getVar1()) && result.isFixed();
+ return (!ko);
+ }
+
+ private boolean reduceAddConstraint(Constraint c) {
+ var change = c.getResult().reduce(c.getVar1().add(c.getVar2()));
+ change = c.getVar1().reduce(c.getResult().sub(c.getVar2())) || change;
+ change = c.getVar2().reduce(c.getResult().sub(c.getVar1())) || change;
+ return change;
+ }
+
+ private boolean reduceMulConstraint(Constraint c) {
+ var change = false;
+ for (int i = 0; i < 3; i++) {
+ change = c.getResult().reduce(c.getVar1().mul(c.getVar2())) || change;
+ change = c.getVar2().reduce(c.getResult().inverseMul(c.getVar1())) || change;
+ change = c.getVar1().reduce(c.getResult().inverseMul(c.getVar2())) || change;
+ }
+ return change;
+ }
+
+ private boolean checkConstraintIntervalsStrategy(Constraint c) {
+ return switch (c.getType()) {
+ case '+' -> checkAddConstraintIntervalsStrategy(c);
+ case '#' -> checkDiffConstraintIntervalsStrategy(c);
+ case '*' -> checkMulConstraintIntervalsStrategy(c);
+ case '/' -> checkDivConstraintIntervalsStrategy(c);
+ default -> throw new IllegalArgumentException("bad constraint: " + c);
+ };
+ }
+
+ private boolean reduce(Constraint c) {
+ return switch (c.getType()) {
+ case '+' -> reduceAddConstraint(c);
+ case '*' -> reduceMulConstraint(c);
+ default -> false;
+ };
+ }
+
+ private boolean checkConstraint(Constraint c) {
+ return switch (strategy) {
+ case CHECK_INTERVALS_STRATEGY, REDUCE_AND_CHECK_INTERVALS_STRATEGY -> checkConstraintIntervalsStrategy(c);
+ default -> throw new IllegalStateException("bad strategy: " + strategy);
+ };
+ }
+
+ private boolean checkConstraints() {
+ for (Constraint c : constraints) {
+ if (!checkConstraint(c)) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ public Variable findVariable() {
+ Variable best = null;
+ for (Variable v : variables) {
+ if (v.isFixed()) continue;
+ if (best == null) {
+ best = v;
+ } else if (v.getSize() < best.getSize()) {
+ best = v;
+ }
+ }
+ return best;
+ }
+
+ public boolean findSolutions() {
+ if (++nodesCounter > maxNodes) {
+ throw new IllegalStateException("too many nodes");
+ }
+ if (! checkConstraints()) {
+ return false;
+ }
+ var v = findVariable();
+ if (v == null) {
+ solutionsCounter++;
+ if (verbose) {
+ variables.stream().filter(Variable::isNamed).forEach(System.out::println);
+ System.out.println();
+ }
+ return true;
+ }
+
+ boolean result = false;
+ int min = v.getMin();
+ int max = v.getMax();
+
+ // Comment découper le domaine ?
+ int step = 1;
+ if (v.getSize() > 1000) {
+ if (min < 0 && max >= 0) {
+ step = -min;
+ } else {
+ int mid = (min + max) / 2;
+ step = (1 + mid - min);
+ }
+ }
+
+ // explorer le domaine
+ for (int value = min; value <= max; value += step) {
+ v.setMin(value);
+ v.setMax(Math.min(value + step - 1, max));
+ if (findSolutions()) {
+ result = true;
+ }
+ }
+ v.setMin(min);
+ v.setMax(max);
+ return result;
+ }
+
+ public Variable newVar() {
+ var v = new Variable(variables.size());
+ variables.add(v);
+ return v;
+ }
+
+ public Variable newVar(String name) {
+ var v = new Variable(name);
+ variables.add(v);
+ return v;
+ }
+
+ public Variable newConstant(int value) {
+ return newVar().domain(value);
+ }
+
+ public void eq(Variable a, Variable b) {
+ sub(newConstant(0), a, b); // 0 = A - B
+ }
+
+ public void gt(Variable a, Variable b) {
+ sub(newVar().domain(1, Variable.MAX_VALUE), a, b); // Z=A-B,Z>0
+ }
+
+ public void get(Variable a, Variable b) {
+ sub(newVar().domain(0, Variable.MAX_VALUE), a, b); // Z=A-B, Z>=0
+ }
+
+ public void lt(Variable a, Variable b) {
+ gt(b, a);
+ }
+
+ public void let(Variable a, Variable b) {
+ get(b, a);
+ }
+
+ public void diff(Variable a, Variable b) {
+ constraints.add(new Constraint('#', a, b, null));
+ }
+
+ public void allDiff(Variable... variables) {
+ for (int i = 0; i < variables.length; i++)
+ for (int j = i + 1; j < variables.length; j++) {
+ diff(variables[i], variables[j]);
+ }
+ }
+
+ private void add(Variable result, Variable a, Variable b) {
+ constraints.add(new Constraint('+', result, a, b));
+ }
+
+ private void sub(Variable result, Variable a, Variable b) {
+ add(a, result, b);
+ }
+
+ private void mul(Variable result, Variable a, Variable b) {
+ constraints.add(new Constraint('*', result, a, b));
+ }
+
+ private void div(Variable result, Variable a, Variable b) {
+ constraints.add(new Constraint('/', result, a, b));
+ }
+
+ private Variable parseSimpleTerm(List<Object> terms) {
+ var first = terms.removeFirst();
+ if (first instanceof Variable var) {
+ return var;
+ }
+ if (first instanceof Integer cst) {
+ return this.newConstant(cst);
+ }
+ throw new IllegalArgumentException("bad expression: " + first);
+ }
+
+ private boolean parseToken(String token, List<Object> terms) {
+ if (!terms.isEmpty()) {
+ if (token.equals(terms.getFirst())) {
+ terms.removeFirst();
+ return true;
+ }
+ }
+ return false;
+ }
+
+ private Variable parseMultiplicationTerm(List<Object> terms) {
+ var first = parseSimpleTerm(terms);
+ if (parseToken("*", terms)) {
+ var second = parseMultiplicationTerm(terms);
+ var result = newVar();
+ mul(result, first, second);
+ return result;
+ }
+ if (parseToken("/", terms)) {
+ var second = parseMultiplicationTerm(terms);
+ var result = newVar();
+ div(result, first, second);
+ return result;
+ }
+ return first;
+ }
+
+ private Variable parseAdditionTerm(List<Object> terms) {
+ var first = parseMultiplicationTerm(terms);
+ if (parseToken("+", terms)) {
+ var second = parseAdditionTerm(terms);
+ var result = newVar();
+ add(result, first, second);
+ return result;
+ }
+ if (parseToken("-", terms)) {
+ var second = parseAdditionTerm(terms);
+ var result = newVar();
+ add(first, result, second);
+ return result;
+ }
+ return first;
+ }
+
+ public void addConstraint(Object... terms) {
+ var termsList = new LinkedList<>(List.of(terms));
+ var var1 = parseAdditionTerm(termsList);
+ var relation = termsList.removeFirst();
+ var var2 = parseAdditionTerm(termsList);
+ if (!termsList.isEmpty()) {
+ throw new IllegalArgumentException("bad expression: " + termsList);
+ }
+ if (relation instanceof String carRelation) {
+ switch (carRelation) {
+ case "=":
+ eq(var1, var2);
+ return;
+ case ">":
+ gt(var1, var2);
+ return;
+ case ">=":
+ get(var1, var2);
+ return;
+ case "<":
+ lt(var1, var2);
+ return;
+ case "<=":
+ let(var1, var2);
+ return;
+ case "<>":
+ diff(var1, var2);
+ return;
+ }
+ }
+ throw new IllegalArgumentException("bad relation: " + relation);
+ }
+
+ public Variable expression2(Object... terms) {
+ var termsList = new LinkedList<>(List.of(terms));
+ var result = parseAdditionTerm(termsList);
+ if (!termsList.isEmpty()) {
+ throw new IllegalArgumentException("bad expression: " + termsList);
+ }
+ return result;
+ }
+
+ private void reduce() {
+ if (verbose) {
+ System.out.println("Variables before reduction:");
+ variables.forEach(System.out::println);
+ }
+
+ for (boolean change = true; change; ) {
+ change = false;
+ for (Constraint c : constraints) {
+ if (reduce(c)) {
+ change = true;
+ }
+ }
+ }
+
+ if (verbose) {
+ System.out.println("Variables after reduction:");
+ variables.forEach(System.out::println);
+ }
+ }
+
+ public long solve() {
+ this.solutionsCounter = 0;
+ this.nodesCounter = 0;
+ if (strategy == REDUCE_AND_CHECK_INTERVALS_STRATEGY) {
+ reduce();
+ }
+ findSolutions();
+ return solutionsCounter;
+ }
+
+ public int getStrategy() {
+ return strategy;
+ }
+
+ public long getNodesCounter() {
+ return nodesCounter;
+ }
+
+ public long getMaxNodes() {
+ return maxNodes;
+ }
+
+ public void setStrategy(int strategy) {
+ this.strategy = strategy;
+ }
+
+ public void setMaxNodes(long maxNodes) {
+ this.maxNodes = maxNodes;
+ }
+
+ public boolean isVerbose() {
+ return verbose;
+ }
+
+ public void setVerbose(boolean verbose) {
+ this.verbose = verbose;
+ }
}