Skip to content

Commit

Permalink
address compiler messages
Browse files Browse the repository at this point in the history
  • Loading branch information
Simon Felix committed Feb 29, 2024
1 parent 0f3253e commit a3089c8
Show file tree
Hide file tree
Showing 5 changed files with 65 additions and 75 deletions.
24 changes: 7 additions & 17 deletions MaxMaze/Program.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,30 +44,20 @@ class Program
"...........# XXXX............." +
"...........# ............ ";

static void Main(string[] args)
static void Main()
{
using var m = new Model();

var free = new BoolExpr[W, H];
for (int y = 0; y < H; y++)
for (int x = 0; x < W; x++)
{
switch (input[30 * y + x])
free[x, y] = input[30 * y + x] switch
{
case '.':
free[x, y] = m.AddVar();
break;
case ' ':
free[x, y] = true;
break;
case '#':
case 'X':
free[x, y] = false;
break;
default:
throw new Exception();
}
}
'.' => m.AddVar(),
' ' => (BoolExpr)true,
'#' or 'X' => (BoolExpr)false,
_ => throw new Exception(),
};

free[0, 0] = true;
free[W - 1, H - 1] = true;
Expand Down
14 changes: 7 additions & 7 deletions SATInterface/LinExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ public class LinExpr //<T> where T:struct,IBinaryInteger<T>
/// </summary>
public LinExpr()
{
Weights = new();
Weights = [];
Offset = T.Zero;
}

Expand All @@ -40,15 +40,15 @@ public LinExpr()
/// </summary>
public LinExpr(T _c)
{
Weights = new();
Weights = [];
Offset = _c;
}

internal LinExpr(UIntVar _src)
{
Model = _src.Model;

Weights = new();
Weights = [];
Offset = T.Zero;
for (var i = 0; i < _src.Bits.Length; i++)
AddTerm(_src.bit[i], T.One << i);
Expand Down Expand Up @@ -625,7 +625,7 @@ void Visit(int _s)
_rhs -= weights[_s];

if (_rhs < T.Zero)
resolvent.Add(active.ToArray());
resolvent.Add([.. active]);
else
for (var i = _s + 1; i < weights.Length; i++)
Visit(i);
Expand Down Expand Up @@ -671,7 +671,7 @@ void Visit(int _s)
_rhs -= weights[_s];
if (_rhs < T.Zero)
{
resolvent.Add(count.ToArray());
resolvent.Add([.. count]);
break;
}
else if (_rhs >= T.Zero && _s + 1 < weights.Length)
Expand Down Expand Up @@ -721,7 +721,7 @@ void Visit(int _s)
{
for (var i = _s + 1; i < _weights.Length; i++)
active.Push(!vars[i]);
res.Add(active.ToArray());
res.Add([.. active]);
for (var i = _s + 1; i < _weights.Length; i++)
active.Pop();
}
Expand Down Expand Up @@ -775,7 +775,7 @@ void Visit(int _s, int _cnt)
_rhs -= weights[_s] * T.CreateChecked(_cnt);

if (_rhs == T.Zero)
validAssignments.Add(count.ToArray());
validAssignments.Add([.. count]);
else if (_rhs > T.Zero && _s + 1 < weights.Length)
for (var i = 0; i <= max[_s + 1]; i++)
Visit(_s + 1, i);
Expand Down
66 changes: 33 additions & 33 deletions SATInterface/Model.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ public class Model : IDisposable //<T> : IDisposable where T : struct, IBinaryIn
public static readonly BoolExpr True = new BoolVar(null!, int.MaxValue);
public static readonly BoolExpr False = new BoolVar(null!, int.MaxValue - 1);

private readonly List<bool> varsX = new();
private readonly List<bool> varsX = [];

public State State { get; internal set; } = State.Undecided;

Expand All @@ -40,14 +40,14 @@ internal class Counter
{
internal Counter(Model _m) : this(_m, 0, 0) { }
internal Counter(Model _m, int _v, int _c) { Model = _m; Variables = _v; Clauses = _c; }
Model Model;
private readonly Model Model;
internal int Variables;
internal int Clauses;

int StartVariables;
int StartClauses;

Dictionary<int, int> Histogram = new();
readonly Dictionary<int, int> Histogram = [];

internal void Start(int _value)
{
Expand All @@ -74,7 +74,7 @@ public override string ToString()
}
}

private Dictionary<string, Counter> Statistics = new();
private readonly Dictionary<string, Counter> Statistics = [];
private string? ActiveStatKey = null;

[Conditional("DEBUG")]
Expand Down Expand Up @@ -417,7 +417,7 @@ public void EnumerateSolutions(IEnumerable<BoolExpr> _modelVariables, Action _so
bool[]? lastAssignment = null;
for (; ; )
{
(var state, var assignment) = InvokeSolver(timeout, assumptions.ToArray());
(var state, var assignment) = InvokeSolver(timeout, [.. assumptions]);

if (state == State.Undecided)
AbortOptimization = true;
Expand Down Expand Up @@ -653,7 +653,7 @@ private void Optimize(LinExpr _obj, Action? _solutionCallback, bool _minimizatio
Console.WriteLine($"Maximizing objective, range {(lb + objOffset)} - {(ub + objOffset)}, testing {(cur + objOffset)}");
}

(var subState, var assignment) = State == State.Unsatisfiable ? (State, null) : InvokeSolver(timeout, assumptions.ToArray());
(var subState, var assignment) = State == State.Unsatisfiable ? (State, null) : InvokeSolver(timeout, [.. assumptions]);

if (subState == State.Satisfiable)
{
Expand Down Expand Up @@ -703,8 +703,8 @@ private void Optimize(LinExpr _obj, Action? _solutionCallback, bool _minimizatio
finally
{
if (Configuration.SetVariablePhaseFromObjective)
foreach (var t in _obj.Terms)
if (t.Var is BoolVar bv)
foreach (var (Var, _) in _obj.Terms)
if (Var is BoolVar bv)
bv.SetPhase(null);

InOptimization = false;
Expand Down Expand Up @@ -884,7 +884,7 @@ void AddXorConstr(BoolExpr[] _elems)
case 6:
{
var r = AddVar();
AddXorConstr(_elems.Append(!r).ToArray());
AddXorConstr([.. _elems, !r]);
return r;
}
default:
Expand Down Expand Up @@ -967,7 +967,7 @@ UIntVar SumTwo(BoolVar _a, BoolVar _b)
else if (Configuration.AddArcConstistencyClauses.HasFlag(ArcConstistencyClauses.PartialArith))
AddConstr(OrExpr.Create(!carry, !sum));

return UIntSumTwoCache[(_a, _b)] = new UIntVar(this, T.CreateChecked(2), new[] { sum, carry }, false);
return UIntSumTwoCache[(_a, _b)] = new UIntVar(this, T.CreateChecked(2), [sum, carry], false);
}

UIntVar SumThree(BoolVar _a, BoolVar _b, BoolVar _c)
Expand Down Expand Up @@ -997,7 +997,7 @@ UIntVar SumThree(BoolVar _a, BoolVar _b, BoolVar _c)
AddConstr(OrExpr.Create(carry, sum, !_c));
}

return UIntSumThreeCache[(_a, _b, _c)] = new UIntVar(this, T.CreateChecked(3), new[] { sum, carry }, false);
return UIntSumThreeCache[(_a, _b, _c)] = new UIntVar(this, T.CreateChecked(3), [sum, carry], false);
}

var beCount = 0;
Expand Down Expand Up @@ -1145,11 +1145,11 @@ public int GetHashCode([DisallowNull] int[] _x)
}
}

private readonly Dictionary<(BoolExpr, BoolExpr), UIntVar> UIntSumTwoCache = new();
private readonly Dictionary<(BoolExpr, BoolExpr, BoolExpr), UIntVar> UIntSumThreeCache = new();
internal readonly Dictionary<(UIntVar, UIntVar), UIntVar> UIntSumCache = new();
private readonly Dictionary<(BoolExpr, BoolExpr), UIntVar> UIntSumTwoCache = [];
private readonly Dictionary<(BoolExpr, BoolExpr, BoolExpr), UIntVar> UIntSumThreeCache = [];
internal readonly Dictionary<(UIntVar, UIntVar), UIntVar> UIntSumCache = [];
internal readonly Dictionary<LinExpr, UIntVar> UIntCache = new(new IgnoreLinExprOffsetComparer());
private readonly Dictionary<T, UIntVar> UIntConstCache = new();
private readonly Dictionary<T, UIntVar> UIntConstCache = [];
internal readonly Dictionary<(LinExpr, T), BoolExpr> LinExprEqCache = new(new IgnoreLinExprOffsetTupleComparer());
internal readonly Dictionary<(LinExpr, T), BoolExpr> LinExprLECache = new(new IgnoreLinExprOffsetTupleComparer());
private readonly Dictionary<int[], BoolExpr[]> SortCache = new(new IntArrayComparer());
Expand Down Expand Up @@ -1256,8 +1256,8 @@ public BoolExpr ITE(BoolExpr _if, BoolExpr _then, BoolExpr _else)
return ITECache[(_if, _then, _else)] = ITEInternal(_if, _then, _else);
}

private readonly Dictionary<(BoolExpr _i, BoolExpr _t, BoolExpr _e), BoolExpr> ITECache = new();
internal Dictionary<OrExpr, int> OrCache = new();
private readonly Dictionary<(BoolExpr _i, BoolExpr _t, BoolExpr _e), BoolExpr> ITECache = [];
internal readonly Dictionary<OrExpr, int> OrCache = [];

private BoolExpr ITEInternal(BoolExpr _if, BoolExpr _then, BoolExpr _else)
{
Expand Down Expand Up @@ -1486,7 +1486,7 @@ public BoolExpr AtMostOneOf(ReadOnlySpan<BoolExpr> _expr, AtMostOneOfMethod? _me
case AtMostOneOfMethod.Heule:
return AtMostOneOfHeule(expr);
default:
throw new ArgumentOutOfRangeException($"Invalid method specified: {nameof(_method)}");
throw new ArgumentOutOfRangeException(nameof(_method), $"Invalid method specified");
}
}
finally
Expand Down Expand Up @@ -1640,7 +1640,7 @@ public BoolExpr ExactlyOneOf(ReadOnlySpan<BoolExpr> _expr, ExactlyOneOfMethod? _
case ExactlyOneOfMethod.OneHot:
return ExactlyOneOfOneHot(expr);
default:
throw new ArgumentOutOfRangeException($"Invalid _method specified: {nameof(_method)}");
throw new ArgumentOutOfRangeException(nameof(_method), $"Invalid method specified");
}
}
finally
Expand Down Expand Up @@ -1717,11 +1717,11 @@ private BoolExpr AtMostOneOfPairwiseTree(ReadOnlySpan<BoolExpr> _expr)
var d = _expr[ic..];

return AndExpr.Create(
AtMostOneOfPairwise(new[] {
AtMostOneOfPairwise([
OrExpr.Create(a).Flatten(),
OrExpr.Create(b).Flatten(),
OrExpr.Create(c).Flatten(),
OrExpr.Create(d).Flatten() }),
OrExpr.Create(d).Flatten() ]),
AtMostOneOfPairwiseTree(a),
AtMostOneOfPairwiseTree(b),
AtMostOneOfPairwiseTree(c),
Expand Down Expand Up @@ -1753,11 +1753,11 @@ private BoolExpr ExactlyOneOfPairwiseTree(ReadOnlySpan<BoolExpr> _expr)
var d = _expr[ic..];

return AndExpr.Create(
ExactlyOneOfPairwise(new[] {
ExactlyOneOfPairwise([
OrExpr.Create(a).Flatten(),
OrExpr.Create(b).Flatten(),
OrExpr.Create(c).Flatten(),
OrExpr.Create(d).Flatten() }),
OrExpr.Create(d).Flatten() ]),
AtMostOneOfPairwiseTree(a),
AtMostOneOfPairwiseTree(b),
AtMostOneOfPairwiseTree(c),
Expand Down Expand Up @@ -1894,7 +1894,7 @@ public BoolExpr ExactlyKOf(IEnumerable<BoolExpr> _expr, int _k, KOfMethod? _meth
return v[_k - 1] & !v[_k];

default:
throw new ArgumentOutOfRangeException("Invalid method", nameof(_method));
throw new ArgumentOutOfRangeException(nameof(_method), "Invalid method");
}
}
finally
Expand Down Expand Up @@ -1968,7 +1968,7 @@ internal BoolExpr AtMostKOf(IEnumerable<BoolExpr> _expr, int _k, KOfMethod? _met
return !v[_k];

default:
throw new ArgumentOutOfRangeException("Invalid method", nameof(_method));
throw new ArgumentOutOfRangeException(nameof(_method), "Invalid method");
}
}
finally
Expand Down Expand Up @@ -2028,11 +2028,11 @@ public BoolExpr[] SortPairwise(ReadOnlySpan<BoolExpr> _elems)
switch (_elems.Length)
{
case 0:
return Array.Empty<BoolExpr>();
return [];
case 1:
return new BoolExpr[] { _elems[0] };
return [_elems[0]];
case 2:
return new BoolExpr[] { OrExpr.Create(_elems).Flatten(), AndExpr.Create(_elems).Flatten() };
return [OrExpr.Create(_elems).Flatten(), AndExpr.Create(_elems).Flatten()];
default:
var R = new BoolExpr[_elems.Length];
var cacheKey = new int[_elems.Length];
Expand Down Expand Up @@ -2108,11 +2108,11 @@ public BoolExpr[] SortTotalizer(ReadOnlySpan<BoolExpr> _elems)
switch (_elems.Length)
{
case 0:
return Array.Empty<BoolExpr>();
return [];
case 1:
return new BoolExpr[] { _elems[0] };
return [_elems[0]];
case 2:
return new BoolExpr[] { OrExpr.Create(_elems).Flatten(), AndExpr.Create(_elems).Flatten() };
return [OrExpr.Create(_elems).Flatten(), AndExpr.Create(_elems).Flatten()];
default:
var elems = _elems.ToArray();
var cacheKey = new int[_elems.Length];
Expand All @@ -2132,8 +2132,8 @@ public BoolExpr[] SortTotalizer(ReadOnlySpan<BoolExpr> _elems)
R[i] = AddVar();
R[^1] = False;

var A = new BoolExpr[] { True }.Concat(SortTotalizer(elems[..(elems.Length / 2)])).Append(False).ToArray();
var B = new BoolExpr[] { True }.Concat(SortTotalizer(elems[(elems.Length / 2)..])).Append(False).ToArray();
var A = new BoolExpr[] { True }.Concat(SortTotalizer(elems.AsSpan()[..(elems.Length / 2)])).Append(False).ToArray();
var B = new BoolExpr[] { True }.Concat(SortTotalizer(elems.AsSpan()[(elems.Length / 2)..])).Append(False).ToArray();
for (var a = 0; a < A.Length - 1; a++)
for (var b = 0; b < B.Length - 1; b++)
{
Expand Down
Loading

0 comments on commit a3089c8

Please sign in to comment.