always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix SAT solver test output

Browse Source
This commit is contained in:
Alexander Ignatovich
2024-07-27 14:49:33 +03:00
committed by Laurent Perron
parent 754d6a4d0f
commit 0abbe38ad7
1 changed files with 115 additions and 96 deletions
Download Patch File Download Diff File Expand all files Collapse all files

211
ortools/sat/csharp/SatSolverTests.cs
View File

@@ -13,8 +13,10 @@
using System;
using System.Collections.Generic;
using System.Text;
using Xunit;
using Google.OrTools.Sat;
using Xunit.Abstractions;
public class SolutionCounter : CpSolverSolutionCallback
{
@@ -43,58 +45,75 @@ public class SolutionCounter : CpSolverSolutionCallback
public class SolutionDivisionCounter : SolutionCounter
{
public SolutionDivisionCounter(int result, IntVar a, IntVar b) : base()
public SolutionDivisionCounter(int result, IntVar a, IntVar b, ITestOutputHelper output)
{
result_ = result;
a_ = a;
b_ = b;
output_ = output;
}
public override void OnSolutionCallback()
{
base.OnSolutionCallback();
var solutionVariablesReport = new StringBuilder();
foreach (IntVar v in new IntVar[] { a_, b_ })
{
Console.Write($"{v.ToString()}={Value(v)} ");
solutionVariablesReport.Append($"{v}={Value(v)} ");
}
Console.WriteLine();
solutionVariablesReport.AppendLine();
output_.WriteLine(solutionVariablesReport.ToString());
Assert.Equal(result_, Value(a_) / Value(b_));
}
private int result_;
private IntVar a_;
private IntVar b_;
private readonly int result_;
private readonly IntVar a_;
private readonly IntVar b_;
private readonly ITestOutputHelper output_;
}
public class SolutionModuloCounter : SolutionCounter
{
public SolutionModuloCounter(int result, IntVar a, IntVar b) : base()
public SolutionModuloCounter(int result, IntVar a, IntVar b, ITestOutputHelper output)
{
result_ = result;
a_ = a;
b_ = b;
output_ = output;
}
public override void OnSolutionCallback()
{
base.OnSolutionCallback();
var solutionVariablesReport = new StringBuilder();
foreach (IntVar v in new IntVar[] { a_, b_ })
{
Console.Write($"{v.ToString()}={Value(v)} ");
solutionVariablesReport.Append($"{v}={Value(v)} ");
}
Console.WriteLine();
solutionVariablesReport.AppendLine();
output_.WriteLine(solutionVariablesReport.ToString());
Assert.Equal(result_, Value(a_) % Value(b_));
}
private int result_;
private IntVar a_;
private IntVar b_;
private readonly int result_;
private readonly IntVar a_;
private readonly IntVar b_;
private readonly ITestOutputHelper output_;
}
namespace Google.OrTools.Tests
{
public class SatSolverTest
{
private readonly ITestOutputHelper output_;
public SatSolverTest(ITestOutputHelper output)
{
this.output_ = output;
}
static IntegerVariableProto NewIntegerVariable(long lb, long ub)
{
IntegerVariableProto var = new IntegerVariableProto();
@@ -278,12 +297,12 @@ public class SatSolverTest
model.Add(delta == x - 5);
model.AddMultiplicationEquality(squaredDelta, new IntVar[] { delta, delta });
model.Minimize(squaredDelta);
// Console.WriteLine("model = " + model.Model.ToString());
// output_.WriteLine("model = " + model.Model);
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);
CpSolverResponse response = solver.Response;
Console.WriteLine("response = " + response.ToString());
output_.WriteLine($"response = {response}");
Assert.Equal(CpSolverStatus.Optimal, status);
@@ -332,7 +351,7 @@ public class SatSolverTest
model.AddDivisionEquality(3, v1, v2);
// Console.WriteLine(model.Model);
SolutionDivisionCounter solution_callback = new SolutionDivisionCounter(3, v1, v2);
SolutionDivisionCounter solution_callback = new SolutionDivisionCounter(3, v1, v2, output_);
CpSolver solver = new CpSolver();
// Tell the solver to search for all solutions.
@@ -357,7 +376,7 @@ public class SatSolverTest
model.AddModuloEquality(3, v1, v2);
// Console.WriteLine(model.Model);
SolutionModuloCounter solution_callback = new SolutionModuloCounter(3, v1, v2);
SolutionModuloCounter solution_callback = new SolutionModuloCounter(3, v1, v2, output_);
CpSolver solver = new CpSolver();
// Tell the solver to search for all solutions.
@@ -390,7 +409,7 @@ public class SatSolverTest
model.Minimize(LinearExpr.WeightedSum(vars, coeffs));
watch.Stop();
var elapsedMs = watch.ElapsedMilliseconds;
Console.WriteLine($"Long: Elapsed time {elapsedMs}");
output_.WriteLine($"Long: Elapsed time {elapsedMs}");
}
[Fact]
@@ -410,7 +429,7 @@ public class SatSolverTest
model.Minimize(LinearExpr.WeightedSum(vars, coeffs));
watch.Stop();
var elapsedMs = watch.ElapsedMilliseconds;
Console.WriteLine($"Int: Elapsed time {elapsedMs}");
output_.WriteLine($"Int: Elapsed time {elapsedMs}");
}
[Fact]
@@ -428,7 +447,7 @@ public class SatSolverTest
model.Minimize(LinearExpr.Sum(exprs));
watch.Stop();
var elapsedMs = watch.ElapsedMilliseconds;
Console.WriteLine($"Exprs: Elapsed time {elapsedMs}");
output_.WriteLine($"Exprs: Elapsed time {elapsedMs}");
}
[Fact]
@@ -453,13 +472,13 @@ public class SatSolverTest
model.Minimize(obj);
watch.Stop();
var elapsedMs = watch.ElapsedMilliseconds;
Console.WriteLine($"Proto: Elapsed time {elapsedMs}");
output_.WriteLine($"Proto: Elapsed time {elapsedMs}");
}
[Fact]
public void LinearExprStaticCompileTest()
{
Console.WriteLine("LinearExprStaticCompileTest");
output_.WriteLine("LinearExprStaticCompileTest");
CpModel model = new CpModel();
IntVar v1 = model.NewIntVar(-10, 10, "v1");
IntVar v2 = model.NewIntVar(-10, 10, "v2");
@@ -468,29 +487,29 @@ public class SatSolverTest
long[] c1 = new long[] { 2L, 4L };
int[] c2 = new int[] { 2, 4 };
LinearExpr e1 = LinearExpr.Sum(new IntVar[] { v1, v2 });
Console.WriteLine(e1.ToString());
output_.WriteLine(e1.ToString());
LinearExpr e2 = LinearExpr.Sum(new ILiteral[] { b1, b2 });
Console.WriteLine(e2.ToString());
output_.WriteLine(e2.ToString());
LinearExpr e3 = LinearExpr.Sum(new BoolVar[] { b1, b2 });
Console.WriteLine(e3.ToString());
output_.WriteLine(e3.ToString());
LinearExpr e4 = LinearExpr.WeightedSum(new IntVar[] { v1, v2 }, c1);
Console.WriteLine(e4.ToString());
output_.WriteLine(e4.ToString());
LinearExpr e5 = LinearExpr.WeightedSum(new ILiteral[] { b1, b2 }, c1);
Console.WriteLine(e5.ToString());
output_.WriteLine(e5.ToString());
LinearExpr e6 = LinearExpr.WeightedSum(new BoolVar[] { b1, b2 }, c1);
Console.WriteLine(e6.ToString());
output_.WriteLine(e6.ToString());
LinearExpr e7 = LinearExpr.WeightedSum(new IntVar[] { v1, v2 }, c2);
Console.WriteLine(e7.ToString());
output_.WriteLine(e7.ToString());
LinearExpr e8 = LinearExpr.WeightedSum(new ILiteral[] { b1, b2 }, c2);
Console.WriteLine(e8.ToString());
output_.WriteLine(e8.ToString());
LinearExpr e9 = LinearExpr.WeightedSum(new BoolVar[] { b1, b2 }, c2);
Console.WriteLine(e9.ToString());
output_.WriteLine(e9.ToString());
}
[Fact]
public void LinearExprBuilderCompileTest()
{
Console.WriteLine("LinearExprBuilderCompileTest");
output_.WriteLine("LinearExprBuilderCompileTest");
CpModel model = new CpModel();
IntVar v1 = model.NewIntVar(-10, 10, "v1");
IntVar v2 = model.NewIntVar(-10, 10, "v2");
@@ -499,155 +518,155 @@ public class SatSolverTest
long[] c1 = new long[] { 2L, 4L };
int[] c2 = new int[] { 2, 4 };
LinearExpr e1 = LinearExpr.NewBuilder().AddSum(new IntVar[] { v1, v2 });
Console.WriteLine(e1.ToString());
output_.WriteLine(e1.ToString());
LinearExpr e2 = LinearExpr.NewBuilder().AddSum(new ILiteral[] { b1, b2 });
Console.WriteLine(e2.ToString());
output_.WriteLine(e2.ToString());
LinearExpr e3 = LinearExpr.NewBuilder().AddSum(new BoolVar[] { b1, b2 });
Console.WriteLine(e3.ToString());
output_.WriteLine(e3.ToString());
LinearExpr e4 = LinearExpr.NewBuilder().AddWeightedSum(new IntVar[] { v1, v2 }, c1);
Console.WriteLine(e4.ToString());
output_.WriteLine(e4.ToString());
LinearExpr e5 = LinearExpr.NewBuilder().AddWeightedSum(new ILiteral[] { b1, b2 }, c1);
Console.WriteLine(e5.ToString());
output_.WriteLine(e5.ToString());
LinearExpr e6 = LinearExpr.NewBuilder().AddWeightedSum(new BoolVar[] { b1, b2 }, c1);
Console.WriteLine(e6.ToString());
output_.WriteLine(e6.ToString());
LinearExpr e7 = LinearExpr.NewBuilder().AddWeightedSum(new IntVar[] { v1, v2 }, c2);
Console.WriteLine(e7.ToString());
output_.WriteLine(e7.ToString());
LinearExpr e8 = LinearExpr.NewBuilder().AddWeightedSum(new ILiteral[] { b1, b2 }, c2);
Console.WriteLine(e8.ToString());
output_.WriteLine(e8.ToString());
LinearExpr e9 = LinearExpr.NewBuilder().AddWeightedSum(new BoolVar[] { b1, b2 }, c2);
Console.WriteLine(e9.ToString());
output_.WriteLine(e9.ToString());
LinearExpr e10 = LinearExpr.NewBuilder().Add(v1);
Console.WriteLine(e10.ToString());
output_.WriteLine(e10.ToString());
LinearExpr e11 = LinearExpr.NewBuilder().Add(b1);
Console.WriteLine(e11.ToString());
output_.WriteLine(e11.ToString());
LinearExpr e12 = LinearExpr.NewBuilder().Add(b1.Not());
Console.WriteLine(e12.ToString());
output_.WriteLine(e12.ToString());
LinearExpr e13 = LinearExpr.NewBuilder().AddTerm(v1, -1);
Console.WriteLine(e13.ToString());
output_.WriteLine(e13.ToString());
LinearExpr e14 = LinearExpr.NewBuilder().AddTerm(b1, -1);
Console.WriteLine(e14.ToString());
output_.WriteLine(e14.ToString());
LinearExpr e15 = LinearExpr.NewBuilder().AddTerm(b1.Not(), -2);
Console.WriteLine(e15.ToString());
output_.WriteLine(e15.ToString());
}
[Fact]
public void LinearExprIntVarOperatorTest()
{
Console.WriteLine("LinearExprIntVarOperatorTest");
output_.WriteLine("LinearExprIntVarOperatorTest");
CpModel model = new CpModel();
IntVar v = model.NewIntVar(-10, 10, "v");
LinearExpr e = v * 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 * v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v + 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 + v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = -v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 1 - v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v - 1;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
}
[Fact]
public void LinearExprBoolVarOperatorTest()
{
Console.WriteLine("LinearExprBoolVarOperatorTest");
output_.WriteLine("LinearExprBoolVarOperatorTest");
CpModel model = new CpModel();
BoolVar v = model.NewBoolVar("v");
LinearExpr e = v * 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 * v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v + 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 + v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = -v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 1 - v;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v - 1;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
}
[Fact]
public void TrueLiteralAsExpressionTest()
{
Console.WriteLine("TrueLiteralAsExpressionTest");
output_.WriteLine("TrueLiteralAsExpressionTest");
CpModel model = new CpModel();
ILiteral v = model.TrueLiteral();
LinearExpr e = v.AsExpr() * 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 * v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.AsExpr() + 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 + v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = -v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 1 - v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.AsExpr() - 1;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
}
[Fact]
public void FalseLiteralAsExpressionTest()
{
Console.WriteLine("FalseLiteralAsExpressionTest");
output_.WriteLine("FalseLiteralAsExpressionTest");
CpModel model = new CpModel();
ILiteral v = model.FalseLiteral();
LinearExpr e = v.AsExpr() * 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 * v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.AsExpr() + 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 + v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = -v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 1 - v.AsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.AsExpr() - 1;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
}
[Fact]
public void LinearExprNotBoolVarOperatorTest()
{
Console.WriteLine("LinearExprBoolVarNotOperatorTest");
output_.WriteLine("LinearExprBoolVarNotOperatorTest");
CpModel model = new CpModel();
ILiteral v = model.NewBoolVar("v");
LinearExpr e = v.NotAsExpr() * 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 * v.NotAsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.NotAsExpr() + 2;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 2 + v.NotAsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.NotAsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = -v.NotAsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = 1 - v.NotAsExpr();
Console.WriteLine(e);
output_.WriteLine(e.ToString());
e = v.NotAsExpr() - 1;
Console.WriteLine(e);
output_.WriteLine(e.ToString());
}
[Fact]
public void ExportModel()
@@ -658,7 +677,7 @@ public class SatSolverTest
model.Add(-100000 <= v1 + 2 * v2 <= 100000);
model.Minimize(v1 - 2 * v2);
Assert.True(model.ExportToFile("test_model_dotnet.pbtxt"));
Console.WriteLine("Model written to file");
output_.WriteLine("Model written to file");
}
[Fact]
@@ -696,13 +715,13 @@ public class SatSolverTest
CpModelProto model = Google.Protobuf.JsonParser.Default.Parse<CpModelProto>(model_str);
SolveWrapper solve_wrapper = new SolveWrapper();
CpSolverResponse response = solve_wrapper.Solve(model);
Console.WriteLine(response);
output_.WriteLine(response.ToString());
}
[Fact]
public void CaptureLog()
{
Console.WriteLine("CaptureLog test");
output_.WriteLine("CaptureLog test");
CpModel model = new CpModel();
IntVar v1 = model.NewIntVar(-10, 10, "v1");
IntVar v2 = model.NewIntVar(-10, 10, "v2");
@@ -716,7 +735,7 @@ public class SatSolverTest
CpSolver solver = new CpSolver();
solver.StringParameters = "log_search_progress:true log_to_stdout:false";
string log = "";
solver.SetLogCallback(message => log += message + "\n");
solver.SetLogCallback(message => log += $"{message}\n");
solver.Solve(model);
Assert.NotEmpty(log);
Assert.Contains("OPTIMAL", log);
@@ -725,7 +744,7 @@ public class SatSolverTest
[Fact]
public void TestInterval()
{
Console.WriteLine("TestInterval test");
output_.WriteLine("TestInterval test");
CpModel model = new CpModel();
IntVar v = model.NewIntVar(-10, 10, "v");
IntervalVar i = model.NewFixedSizeIntervalVar(v, 3, "i");