Skip to content

Commit cfe3221

Browse files
lperronlperron
committed
[CP-SAT] polish c# code; remove failing DCHECK
1 parent f2b0044 commit cfe3221

File tree

4 files changed

+183
-29
lines changed

4 files changed

+183
-29
lines changed

‎ortools/sat/csharp/CpModel.cs

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ public BoolVar NewBoolVar(string name)
107107
*/
108108
public ILiteral TrueLiteral()
109109
{
110-
return true_literal_ ??= new BoolVar(model_, ConvertConstant(1));
110+
return true_literal_ ??= new BoolVar(model_, ConvertConstantWithName(1, "true"));
111111
}
112112

113113
/**
@@ -1173,6 +1173,24 @@ private int ConvertConstant(long value)
11731173
return index;
11741174
}
11751175

1176+
private int ConvertConstantWithName(long value, string name)
1177+
{
1178+
if (constant_map_.TryGetValue(value, out var index))
1179+
{
1180+
return index;
1181+
}
1182+
1183+
index = model_.Variables.Count;
1184+
IntegerVariableProto var = new IntegerVariableProto();
1185+
var.Domain.Capacity = 2;
1186+
var.Domain.Add(value);
1187+
var.Domain.Add(value);
1188+
var.Name = name;
1189+
constant_map_.Add(value, index);
1190+
model_.Variables.Add(var);
1191+
return index;
1192+
}
1193+
11761194
internal LinearExpr GetLinearExpr<X>(X x)
11771195
{
11781196
if (typeof(X) == typeof(IntVar))

‎ortools/sat/csharp/IntegerExpressions.cs

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,8 @@ public interface ILiteral
2828
ILiteral Not();
2929
/** <summary>Returns the logical index of the literal. </summary> */
3030
int GetIndex();
31+
/** <summary>Returns the literal as a linear expression.</summary> */
32+
LinearExpr AsExpr();
3133
/** <summary>Returns the Boolean negation of the literal as a linear expression.</summary> */
3234
LinearExpr NotAsExpr();
3335
}
@@ -603,6 +605,7 @@ public LinearExprBuilder AddWeightedSum(IEnumerable<BoolVar> vars, IEnumerable<i
603605
public override string ToString()
604606
{
605607
string result = "";
608+
bool need_parenthesis = false;
606609
foreach (Term term in terms_)
607610
{
608611
bool first = String.IsNullOrEmpty(result);
@@ -615,6 +618,7 @@ public override string ToString()
615618
if (!first)
616619
{
617620
result += " + ";
621+
need_parenthesis = true;
618622
}
619623

620624
result += term.expr.ToString();
@@ -623,6 +627,7 @@ public override string ToString()
623627
{
624628
if (!first)
625629
{
630+
need_parenthesis = true;
626631
result += " + ";
627632
}
628633

@@ -632,6 +637,7 @@ public override string ToString()
632637
{
633638
if (!first)
634639
{
640+
need_parenthesis = true;
635641
result += String.Format(" - {0}", term.expr.ToString());
636642
}
637643
else
@@ -643,6 +649,7 @@ public override string ToString()
643649
{
644650
if (!first)
645651
{
652+
need_parenthesis = true;
646653
result += String.Format(" - {0} * {1}", -term.coefficient, term.expr.ToString());
647654
}
648655
else
@@ -655,6 +662,7 @@ public override string ToString()
655662
{
656663
if (!String.IsNullOrEmpty(result))
657664
{
665+
need_parenthesis = true;
658666
result += String.Format(" + {0}", offset_);
659667
}
660668
else
@@ -666,13 +674,19 @@ public override string ToString()
666674
{
667675
if (!String.IsNullOrEmpty(result))
668676
{
677+
need_parenthesis = true;
669678
result += String.Format(" - {0}", -offset_);
670679
}
671680
else
672681
{
673682
result += String.Format("{0}", offset_);
674683
}
675684
}
685+
686+
if (need_parenthesis)
687+
{
688+
return string.Format("({0})", result);
689+
}
676690
return result;
677691
}
678692

@@ -803,6 +817,12 @@ public ILiteral Not()
803817
return negation_ ??= new NotBoolVar(this);
804818
}
805819

820+
/** <summary>Returns the literal as a linear expression.</summary> */
821+
public LinearExpr AsExpr()
822+
{
823+
return this;
824+
}
825+
806826
/** <summary> Returns the Boolean negation of that variable as a linear expression.</summary> */
807827
public LinearExpr NotAsExpr()
808828
{
@@ -836,9 +856,14 @@ public ILiteral Not()
836856
return boolvar_;
837857
}
838858

859+
public LinearExpr AsExpr()
860+
{
861+
return LinearExpr.Affine(boolvar_, -1, 1); // 1 - boolvar_.
862+
}
863+
839864
public LinearExpr NotAsExpr()
840865
{
841-
return (LinearExpr)Not();
866+
return boolvar_;
842867
}
843868

844869
public override string ToString()

‎ortools/sat/csharp/SatSolverTests.cs

Lines changed: 138 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,81 @@
1616
using Xunit;
1717
using Google.OrTools.Sat;
1818

19+
public class SolutionCounter : CpSolverSolutionCallback
20+
{
21+
public SolutionCounter()
22+
{
23+
Console.WriteLine("SolutionCounter Ctor");
24+
solution_count_ = 0;
25+
}
26+
27+
public override void OnSolutionCallback()
28+
{
29+
solution_count_ += 1;
30+
}
31+
32+
public int SolutionCount
33+
{
34+
get {
35+
return solution_count_;
36+
}
37+
set {
38+
solution_count_ = value;
39+
}
40+
}
41+
private int solution_count_;
42+
}
43+
44+
public class SolutionDivisionCounter : SolutionCounter
45+
{
46+
public SolutionDivisionCounter(int result, IntVar a, IntVar b) : base()
47+
{
48+
result_ = result;
49+
a_ = a;
50+
b_ = b;
51+
}
52+
53+
public override void OnSolutionCallback()
54+
{
55+
base.OnSolutionCallback();
56+
foreach (IntVar v in new IntVar[] { a_, b_ })
57+
{
58+
Console.Write(String.Format("{0}={1} ", v.ToString(), Value(v)));
59+
}
60+
Console.WriteLine();
61+
Assert.Equal(result_, Value(a_) / Value(b_));
62+
}
63+
64+
private int result_;
65+
private IntVar a_;
66+
private IntVar b_;
67+
}
68+
69+
public class SolutionModuloCounter : SolutionCounter
70+
{
71+
public SolutionModuloCounter(int result, IntVar a, IntVar b) : base()
72+
{
73+
result_ = result;
74+
a_ = a;
75+
b_ = b;
76+
}
77+
78+
public override void OnSolutionCallback()
79+
{
80+
base.OnSolutionCallback();
81+
foreach (IntVar v in new IntVar[] { a_, b_ })
82+
{
83+
Console.Write(String.Format("{0}={1} ", v.ToString(), Value(v)));
84+
}
85+
Console.WriteLine();
86+
Assert.Equal(result_, Value(a_) % Value(b_));
87+
}
88+
89+
private int result_;
90+
private IntVar a_;
91+
private IntVar b_;
92+
}
93+
1994
namespace Google.OrTools.Tests
2095
{
2196
public class SatSolverTest
@@ -257,15 +332,19 @@ public void Division()
257332
model.AddDivisionEquality(3, v1, v2);
258333
// Console.WriteLine(model.Model);
259334

335+
SolutionDivisionCounter solution_callback = new SolutionDivisionCounter(3, v1, v2);
336+
260337
CpSolver solver = new CpSolver();
261-
CpSolverStatus status = solver.Solve(model);
338+
// Tell the solver to search for all solutions.
339+
solver.StringParameters = "enumerate_all_solutions:true";
340+
CpSolverStatus status = solver.Solve(model, solution_callback);
341+
262342
Assert.Equal(CpSolverStatus.Optimal, status);
343+
Assert.Equal(0, solver.ObjectiveValue);
344+
345+
Assert.Equal(5, solution_callback.SolutionCount);
263346

264347
CpSolverResponse response = solver.Response;
265-
Assert.Equal(3, solver.Value(v1));
266-
Assert.Equal(1, solver.Value(v2));
267-
Assert.Equal(new long[] { 3, 1 }, response.Solution);
268-
Assert.Equal(0, response.ObjectiveValue);
269348
// Console.WriteLine("response = " + response.ToString());
270349
}
271350

@@ -278,15 +357,19 @@ public void Modulo()
278357
model.AddModuloEquality(3, v1, v2);
279358
// Console.WriteLine(model.Model);
280359

360+
SolutionModuloCounter solution_callback = new SolutionModuloCounter(3, v1, v2);
361+
281362
CpSolver solver = new CpSolver();
282-
CpSolverStatus status = solver.Solve(model);
363+
// Tell the solver to search for all solutions.
364+
solver.StringParameters = "enumerate_all_solutions:true";
365+
CpSolverStatus status = solver.Solve(model, solution_callback);
366+
283367
Assert.Equal(CpSolverStatus.Optimal, status);
368+
Assert.Equal(0, solver.ObjectiveValue);
369+
370+
Assert.Equal(11, solution_callback.SolutionCount);
284371

285372
CpSolverResponse response = solver.Response;
286-
Assert.Equal(3, solver.Value(v1));
287-
Assert.Equal(4, solver.Value(v2));
288-
Assert.Equal(new long[] { 3, 4 }, response.Solution);
289-
Assert.Equal(0, response.ObjectiveValue);
290373
// Console.WriteLine("response = " + response.ToString());
291374
}
292375

@@ -496,25 +579,59 @@ public void LinearExprBoolVarOperatorTest()
496579
}
497580

498581
[Fact]
499-
public void LinearExprNotBoolVarOperatorTest()
582+
public void TrueLiteralAsExpressionTest()
500583
{
501-
Console.WriteLine("LinearExprBoolVarNotOperatorTest");
584+
Console.WriteLine("TrueLiteralAsExpressionTest");
502585
CpModel model = new CpModel();
503-
ILiteral v = model.NewBoolVar("v");
504-
LinearExpr e = v.NotAsExpr() * 2;
586+
ILiteral v = model.TrueLiteral();
587+
LinearExpr e = v.AsExpr() * 2;
588+
Console.WriteLine(e);
589+
e = 2 * v.AsExpr();
505590
Console.WriteLine(e);
506-
e = 2 * v.NotAsExpr();
591+
e = v.AsExpr() + 2;
507592
Console.WriteLine(e);
508-
e = v.NotAsExpr() + 2;
593+
e = 2 + v.AsExpr();
509594
Console.WriteLine(e);
510-
e = 2 + v.NotAsExpr();
595+
e = v.AsExpr();
511596
Console.WriteLine(e);
512-
e = v.NotAsExpr();
597+
e = -v.AsExpr();
513598
Console.WriteLine(e);
514-
e = -v.NotAsExpr();
599+
e = 1 - v.AsExpr();
515600
Console.WriteLine(e);
516-
e = 1 - v.NotAsExpr();
601+
e = v.AsExpr() - 1;
517602
Console.WriteLine(e);
603+
}
604+
605+
[Fact]
606+
public void FalseLiteralAsExpressionTest()
607+
{
608+
Console.WriteLine("FalseLiteralAsExpressionTest");
609+
CpModel model = new CpModel();
610+
ILiteral v = model.FalseLiteral();
611+
LinearExpr e = v.AsExpr() * 2;
612+
Console.WriteLine(e);
613+
e = 2 * v.AsExpr();
614+
Console.WriteLine(e);
615+
e = v.AsExpr() + 2;
616+
Console.WriteLine(e);
617+
e = 2 + v.AsExpr();
618+
Console.WriteLine(e);
619+
e = v.AsExpr();
620+
Console.WriteLine(e);
621+
e = -v.AsExpr();
622+
Console.WriteLine(e);
623+
e = 1 - v.AsExpr();
624+
Console.WriteLine(e);
625+
e = v.AsExpr() - 1;
626+
Console.WriteLine(e);
627+
}
628+
629+
[Fact]
630+
public void LinearExprNotBoolVarOperatorTest()
631+
{
632+
Console.WriteLine("LinearExprBoolVarNotOperatorTest");
633+
CpModel model = new CpModel();
634+
ILiteral v = model.NewBoolVar("v");TestInter
518635
e = v.NotAsExpr() - 1;
519636
Console.WriteLine(e);
520637
}
@@ -600,7 +717,7 @@ public void TestInterval()
600717
IntervalVar i = model.NewFixedSizeIntervalVar(v, 3, "i");
601718
Assert.Equal("v", i.StartExpr().ToString());
602719
Assert.Equal("3", i.SizeExpr().ToString());
603-
Assert.Equal("v + 3", i.EndExpr().ToString());
720+
Assert.Equal("(v + 3)", i.EndExpr().ToString());
604721
}
605722
}
606723
} // namespace Google.OrTools.Tests

‎ortools/sat/feasibility_jump.cc

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -914,7 +914,6 @@ bool FeasibilityJumpSolver::DoSomeGeneralIterations() {
914914
// We already know the score of the only possible move (undoing what we
915915
// just did).
916916
jumps_.SetJump(var, prev_value - new_value, -score);
917-
DCHECK(state_->options.use_decay || jumps_.JumpIsUpToDate(var));
918917
}
919918

920919
if (state_->options.use_compound_moves && !backtrack) {
@@ -1072,11 +1071,6 @@ bool FeasibilityJumpSolver::ShouldScan(int var) const {
10721071

10731072
if (!jumps_.NeedRecomputation(var)) {
10741073
// We already have the score/jump of that variable.
1075-
//
1076-
// Note that the DCHECK will likely fail if you use decaying weights as they
1077-
// will have large magnitudes and the incremental update will be imprecise.
1078-
DCHECK(state_->options.use_decay || jumps_.JumpIsUpToDate(var))
1079-
<< var << " " << var_domains_[var] << " " << state_->options.name();
10801074
const double score = jumps_.Score(var);
10811075
return score < 0.0;
10821076
}

0 commit comments

Comments
 (0)