Skip to content

Commit

Permalink
clearer exceptions
Browse files Browse the repository at this point in the history
  • Loading branch information
Simon Felix committed Jan 24, 2024
1 parent f678a3e commit b28ef77
Show file tree
Hide file tree
Showing 10 changed files with 29 additions and 52 deletions.
7 changes: 4 additions & 3 deletions SATInterface/AndExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,14 +74,15 @@ internal static BoolExpr Create(ReadOnlySpan<BoolExpr> _elems)

var count = 0;
foreach (var es in _elems)
if (es is null)
throw new ArgumentNullException(nameof(_elems));
else if (ReferenceEquals(es, Model.False))
{
ArgumentNullException.ThrowIfNull(es, nameof(_elems));
if (ReferenceEquals(es, Model.False))
return Model.False;
else if (es is AndExpr ae)
count += ae.Elements.Length;
else if (!ReferenceEquals(es, Model.True))
count++;
}

if (count == 0)
return Model.True;
Expand Down
31 changes: 4 additions & 27 deletions SATInterface/BoolExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,8 +75,7 @@ public override string ToString()

public static BoolExpr operator !(BoolExpr _v)
{
if (_v is null)
throw new ArgumentNullException(nameof(_v));
ArgumentNullException.ThrowIfNull(nameof(_v));

if (ReferenceEquals(_v, Model.False))
return Model.True;
Expand Down Expand Up @@ -113,8 +112,8 @@ public override string ToString()

public static BoolExpr operator ==(BoolExpr lhsS, BoolExpr rhsS)
{
if (lhsS is null || rhsS is null)
throw new NullReferenceException();
ArgumentNullException.ThrowIfNull(lhsS, nameof(lhsS));
ArgumentNullException.ThrowIfNull(rhsS, nameof(rhsS));

if (ReferenceEquals(lhsS, rhsS))
return Model.True;
Expand All @@ -131,29 +130,7 @@ public override string ToString()
if (ReferenceEquals(rhsS, Model.False))
return !lhsS;

//if (rhsS is AndExpr andExpr)
//{
// var other = lhsS.Flatten();
// var ands = new List<BoolExpr>(andExpr.Elements.Length + 1);
// ands.Add(OrExpr.Create(andExpr.Elements.Select(e => !e).Append(other).ToArray()).Flatten());
// foreach (var e in andExpr.Elements)
// ands.Add(e | !other);
// return AndExpr.Create(ands.ToArray());
//}
//if (rhsS is OrExpr orExpr)
//{
// var other = lhsS.Flatten();
// var ands = new List<BoolExpr>(orExpr.Elements.Length + 1);
// ands.Add(OrExpr.Create(orExpr.Elements.Append(!other).ToArray()).Flatten());
// foreach (var e in orExpr.Elements)
// ands.Add(!e | other);
// return AndExpr.Create(ands.ToArray());
//}
//if (!(rhsS is AndExpr) && lhsS is AndExpr)
// return (rhsS == lhsS);
//if (!(rhsS is OrExpr) && lhsS is OrExpr)
// return (rhsS == lhsS);

lhsS = lhsS.Flatten();
rhsS = rhsS.Flatten();
return lhsS.GetModel()!.ITE(lhsS, rhsS, !rhsS);
}
Expand Down
8 changes: 4 additions & 4 deletions SATInterface/LinExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1350,7 +1350,7 @@ public override string ToString()
else if (e.Value > T.One)
sb.Append($" + {e.Value}*");
else
throw new Exception();
throw new NotImplementedException();
}
sb.Append($"v{e.Key}");
}
Expand All @@ -1368,9 +1368,9 @@ private BoolExpr EqualsMod(T _rhs, T _b)
Debug.Assert(Model is not null);

if (_rhs < T.Zero)
throw new ArgumentException(nameof(_rhs));
throw new ArgumentOutOfRangeException(nameof(_rhs));
if (_b < T.One)
throw new ArgumentException(nameof(_b));
throw new ArgumentOutOfRangeException(nameof(_b));

if (_b == T.One)
return Model.True;
Expand Down Expand Up @@ -1476,7 +1476,7 @@ public void AddTerm(BoolExpr _be, T _weight)
}
}
else
throw new Exception();
throw new NotImplementedException();
}

public override int GetHashCode()
Expand Down
14 changes: 7 additions & 7 deletions SATInterface/Model.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -642,7 +642,7 @@ private void Optimize(LinExpr _obj, Action? _solutionCallback, bool _minimizatio
assumptions.Add(v.Id);
}
else
throw new Exception();
throw new NotImplementedException();
}

if (Configuration.Verbosity > 0)
Expand Down Expand Up @@ -737,7 +737,7 @@ public void Solve(BoolExpr[]? _assumptions = null)
BoolExpr be => be.Flatten() switch
{
BoolVar ibv => ibv.Id,
_ => throw new Exception()
_ => throw new NotImplementedException()
}
};
}
Expand Down Expand Up @@ -771,7 +771,7 @@ public void Write(string _path)
public void Write(TextWriter _out)
{
if (DIMACSBuffer is null)
throw new Exception("Configuration.EnableDIMACSWriting must be set");
throw new InvalidOperationException("Configuration.EnableDIMACSWriting must be set");

_out.WriteLine("c Created by SATInterface");
_out.WriteLine($"p cnf {VariableCount} {ClauseCount}");
Expand Down Expand Up @@ -1442,7 +1442,7 @@ public BoolExpr AtMostOneOf(ReadOnlySpan<BoolExpr> _expr, AtMostOneOfMethod? _me
case AtMostOneOfMethod.Heule:
return AtMostOneOfHeule(expr);
default:
throw new ArgumentException($"Invalid method specified: {nameof(_method)}");
throw new ArgumentOutOfRangeException($"Invalid method specified: {nameof(_method)}");
}
}
finally
Expand Down Expand Up @@ -1592,7 +1592,7 @@ public BoolExpr ExactlyOneOf(ReadOnlySpan<BoolExpr> _expr, ExactlyOneOfMethod? _
case ExactlyOneOfMethod.OneHot:
return ExactlyOneOfOneHot(expr);
default:
throw new ArgumentException($"Invalid _method specified: {nameof(_method)}");
throw new ArgumentOutOfRangeException($"Invalid _method specified: {nameof(_method)}");
}
}
finally
Expand Down Expand Up @@ -1845,7 +1845,7 @@ public BoolExpr ExactlyKOf(IEnumerable<BoolExpr> _expr, int _k, KOfMethod? _meth
return v[_k - 1] & !v[_k];

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

default:
throw new ArgumentException("Invalid method", nameof(_method));
throw new ArgumentOutOfRangeException("Invalid method", nameof(_method));
}
}
finally
Expand Down
5 changes: 2 additions & 3 deletions SATInterface/OrExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,9 +64,8 @@ internal static BoolExpr Create(ReadOnlySpan<BoolExpr> _elems)
var count = 0;
foreach (var es in _elems)
{
if (es is null)
throw new ArgumentNullException(nameof(_elems));
else if (ReferenceEquals(es, Model.True))
ArgumentNullException.ThrowIfNull(nameof(_elems));
if (ReferenceEquals(es, Model.True))
return Model.True;
else if (es is OrExpr oe)
count += oe.FlatCached ? 1 : oe.Elements.Length;
Expand Down
2 changes: 1 addition & 1 deletion SATInterface/Solver/CaDiCaL.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ public override (State State, bool[]? Vars) Solve(int _variableCount, long _time
return (State.Undecided, null);

default:
throw new Exception();
throw new NotImplementedException();
}
}
finally
Expand Down
2 changes: 1 addition & 1 deletion SATInterface/Solver/CryptoMiniSat.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ public override (State State, bool[]? Vars) Solve(int _variableCount, long _time

if (_timeout != long.MaxValue)
//CryptoMiniSatNative.cmsat_set_max_time(Handle, (_timeout - Environment.TickCount64) / 1000d);
throw new Exception("CryptoMiniSat does not support wall-clock time limits");
throw new NotImplementedException("CryptoMiniSat does not support wall-clock time limits");


CryptoMiniSatNative.c_lbool result;
Expand Down
2 changes: 1 addition & 1 deletion SATInterface/Solver/Kissat.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ public override (State State, bool[]? Vars) Solve(int _variableCount, long _time
return (State.Undecided, null);

default:
throw new Exception();
throw new NotImplementedException();
}
}
finally
Expand Down
2 changes: 1 addition & 1 deletion SATInterface/Solver/YalSAT.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ public override (State State, bool[]? Vars) Solve(int _variableCount, long _time
return (State.Undecided, null);

default:
throw new Exception();
throw new NotImplementedException();
}
}
finally
Expand Down
8 changes: 4 additions & 4 deletions SATInterface/UIntVar.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ public BoolExpr this[int _bitIndex]
internal UIntVar(Model _model, T _ub, BoolExpr[] _bits, bool _enforceUB = false)
{
if (T.IsNegative(_ub))
throw new ArgumentException("Invalid upper bound", nameof(_ub));
throw new ArgumentOutOfRangeException("Invalid upper bound", nameof(_ub));

Model = _model;
bit = _bits;
Expand Down Expand Up @@ -85,7 +85,7 @@ internal UIntVar(Model _model, T _ub, bool _enforceUB = true)
_model.StartStatistics("UInt", (int)_ub.GetBitLength());

if (T.IsNegative(_ub))
throw new ArgumentException("Invalid upper bound", nameof(_ub));
throw new ArgumentOutOfRangeException("Invalid upper bound", nameof(_ub));

Model = _model;
UB = _ub;
Expand Down Expand Up @@ -161,7 +161,7 @@ public override int GetHashCode()
internal static UIntVar Const(Model _model, T _c)
{
if (T.IsNegative(_c))
throw new ArgumentException($"Value may not be negative", nameof(_c));
throw new ArgumentOutOfRangeException($"Value may not be negative", nameof(_c));

var bits = new BoolExpr[_c.GetBitLength()];
for (var i = 0; i < bits.Length; i++)
Expand Down Expand Up @@ -460,7 +460,7 @@ public T X
public static UIntVar operator *(UIntVar _a, T _b)
{
if (_b < T.Zero)
throw new ArgumentException("Only multiplication by positive numbers supported.");
throw new ArgumentOutOfRangeException("Only multiplication by positive numbers supported.");
if (_b == T.Zero)
return _a.Model.AddUIntConst(T.Zero);
if (_b == T.One)
Expand Down

0 comments on commit b28ef77

Please sign in to comment.