Skip to content

Drop the constraints that only existed to dodge #51 #74

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
HowardvanRooijen wants to merge 1 commit into from
Open

Drop the constraints that only existed to dodge #51 #74

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion solutions/Z3.Linq.Tests/DistinctSelectorTheoremTests.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,6 @@ public void Distinct_SelectorOverDistinctMultipliers_Solves(int first, int secon
var result = (from t in context.NewTheorem<Symbols<int, int>>()
where Z3Methods.Distinct(multipliers.Select(m => t.X1 * m).ToArray())
where t.X1 > 0
where t.X2 == 0
select t).Solve();

// Assert
Expand Down
1 change: 0 additions & 1 deletion solutions/Z3.Linq.Tests/EnvironmentTypeTests.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -234,7 +234,6 @@ public void Solve_NestedObjectEnvironment_ConstrainsAcrossNestingLevels()
var result = context.NewTheorem<OuterEnvironment>()
.Where(t => t.Inner.A == t.Top * 2)
.Where(t => t.Top == 5)
.Where(t => t.Inner.B == 0)
.Solve();

// Assert
Expand Down
29 changes: 9 additions & 20 deletions solutions/Z3.Linq.Tests/OptimizationTests.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ public void Optimize_Minimize_ReturnsTheSmallestSatisfyingValue()
var result = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 5)
.Where(t => t.X1 <= 9)
.Where(t => t.X2 == 0)
.Optimize(Optimization.Minimize, t => t.X1);

// Assert
Expand All @@ -49,7 +48,6 @@ public void Optimize_Maximize_ReturnsTheLargestSatisfyingValue()
var result = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 5)
.Where(t => t.X1 <= 9)
.Where(t => t.X2 == 0)
.Optimize(Optimization.Maximize, t => t.X1);

// Assert
Expand All @@ -66,8 +64,7 @@ public void Optimize_MinimizeAndMaximizeOverTheSameTheorem_ReturnOppositeBounds(
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 5)
.Where(t => t.X1 <= 9)
.Where(t => t.X2 == 0);
.Where(t => t.X1 <= 9);

// Act
var minimum = theorem.Optimize(Optimization.Minimize, t => t.X1);
Expand All @@ -87,8 +84,7 @@ public void OrderBy_ProducesTheSameResultAsMinimize()
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 3)
.Where(t => t.X1 <= 8)
.Where(t => t.X2 == 0);
.Where(t => t.X1 <= 8);

// Act
var viaOptimize = theorem.Optimize(Optimization.Minimize, t => t.X1);
Expand All @@ -107,8 +103,7 @@ public void OrderByDescending_ProducesTheSameResultAsMaximize()
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 3)
.Where(t => t.X1 <= 8)
.Where(t => t.X2 == 0);
.Where(t => t.X1 <= 8);

// Act
var viaOptimize = theorem.Optimize(Optimization.Maximize, t => t.X1);
Expand All @@ -129,8 +124,7 @@ public void OrderBy_BeforeSolveIsCalled_DoesNotSolveAnything()
using var log = new StringWriter();
using var context = new Z3Context { Log = log };
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 3)
.Where(t => t.X2 == 0);
.Where(t => t.X1 >= 3);

// Act
var deferred = theorem.OrderBy(t => t.X1);
Expand All @@ -150,8 +144,7 @@ public void OrderByDescending_BeforeSolveIsCalled_DoesNotSolveAnything()
using var log = new StringWriter();
using var context = new Z3Context { Log = log };
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 3)
.Where(t => t.X2 == 0);
.Where(t => t.X1 >= 3);

// Act
var deferred = theorem.OrderByDescending(t => t.X1);
Expand Down Expand Up @@ -223,8 +216,7 @@ public void Optimize_MinimizingIsNotJustTheFirstSatisfyingModel()
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 5)
.Where(t => t.X1 <= 100)
.Where(t => t.X2 == 0);
.Where(t => t.X1 <= 100);

// Act
var minimised = theorem.Optimize(Optimization.Minimize, t => t.X1);
Expand All @@ -243,8 +235,7 @@ public void Optimize_CalledTwiceOnTheSameTheorem_LeavesItReusable()
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 1)
.Where(t => t.X1 <= 4)
.Where(t => t.X2 == 0);
.Where(t => t.X1 <= 4);

// Act
var first = theorem.Optimize(Optimization.Minimize, t => t.X1);
Expand All @@ -267,8 +258,7 @@ public void Optimize_WithUnrecognisedDirection_ThrowsArgumentOutOfRangeException
// than defaulting to one of them (Theorem.cs:118).
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 == 1)
.Where(t => t.X2 == 0);
.Where(t => t.X1 == 1);

// Act & Assert
Should.Throw<ArgumentOutOfRangeException>(
Expand Down Expand Up @@ -329,8 +319,7 @@ public void Optimize_AfterAdditionalWhere_RespectsTheNarrowedConstraints()
using var context = new Z3Context();
var parent = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 >= 1)
.Where(t => t.X1 <= 10)
.Where(t => t.X2 == 0);
.Where(t => t.X1 <= 10);
var child = parent.Where(t => t.X1 >= 6);

// Act
Expand Down
39 changes: 20 additions & 19 deletions solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,6 @@ public void Solve_IntSymbol_RoundTripsTheValue(int value)
// Act
var result = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 == value)
.Where(t => t.X2 == 0)
.Solve();

// Assert
Expand All @@ -65,7 +64,6 @@ public void Solve_LongSymbol_RoundTripsTheValue(long value)
// Act
var result = context.NewTheorem<Symbols<long, int>>()
.Where(t => t.X1 == value)
.Where(t => t.X2 == 0)
.Solve();

// Assert
Expand All @@ -84,7 +82,6 @@ public void Solve_BoolSymbol_RoundTripsTheValue(bool value)
// Act
var result = context.NewTheorem<Symbols<bool, int>>()
.Where(t => t.X1 == value)
.Where(t => t.X2 == 0)
.Solve();

// Assert
Expand All @@ -106,7 +103,6 @@ public void Solve_DoubleSymbol_RoundTripsTheValue(double value)
// Act
var result = context.NewTheorem<Symbols<double, int>>()
.Where(t => t.X1 == value)
.Where(t => t.X2 == 0)
.Solve();

// Assert
Expand All @@ -125,7 +121,6 @@ public void Solve_DecimalSymbol_RoundTripsTheValue()
// Act
var result = context.NewTheorem<Symbols<decimal, int>>()
.Where(t => t.X1 == Value)
.Where(t => t.X2 == 0)
.Solve();

// Assert
Expand All @@ -145,7 +140,6 @@ public void Solve_StringSymbol_RoundTripsTheValue(string value)
// Act
var result = context.NewTheorem<Symbols<string, int>>()
.Where(t => t.X1 == value)
.Where(t => t.X2 == 0)
.Solve();

// Assert
Expand All @@ -165,7 +159,6 @@ public void Solve_DoubleSymbolWithInequality_SatisfiesTheConstraint()
var result = context.NewTheorem<Symbols<double, int>>()
.Where(t => t.X1 > 10.5)
.Where(t => t.X1 < 11.0)
.Where(t => t.X2 == 0)
.Solve();

// Assert
Expand All @@ -190,8 +183,7 @@ public void Solve_ShortSymbol_ThrowsInvalidCastException()
// Arrange
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<short, short>>()
.Where(t => t.X1 == 7)
.Where(t => t.X2 == 1);
.Where(t => t.X1 == 7);

// Act & Assert
Should.Throw<InvalidCastException>(() => theorem.Solve());
Expand All @@ -212,8 +204,7 @@ public void Solve_FloatSymbol_ThrowsArgumentException()
// Arrange
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<float, int>>()
.Where(t => t.X1 == 1.5f)
.Where(t => t.X2 == 0);
.Where(t => t.X1 == 1.5f);

// Act & Assert
Should.Throw<ArgumentException>(() => theorem.Solve());
Expand All @@ -240,7 +231,6 @@ public void Solve_DateTimeSymbol_ReturnsTheSameInstantAsLocalTime()
// Act
var result = context.NewTheorem<Symbols<DateTime, int>>()
.Where(t => t.X1 == utc)
.Where(t => t.X2 == 0)
.Solve();

// Assert
Expand Down Expand Up @@ -309,7 +299,6 @@ public void Solve_DoubleSymbolUnderCommaDecimalCulture_ThrowsZ3ParserError()
using var context = new Z3Context();
_ = context.NewTheorem<Symbols<double, int>>()
.Where(t => t.X1 == 1.5)
.Where(t => t.X2 == 0)
.Solve();
}
catch (Exception ex)
Expand Down Expand Up @@ -337,25 +326,37 @@ public void Solve_DoubleSymbolUnderInvariantCulture_RoundTripsTheValue()
// that the two differ only by culture. This is what the defect above should look like
// once it is fixed.
double? value = null;
Exception? captured = null;

var thread = new Thread(() =>
{
CultureInfo.CurrentCulture = CultureInfo.InvariantCulture;

using var context = new Z3Context();
var result = context.NewTheorem<Symbols<double, int>>()
.Where(t => t.X1 == 1.5)
.Where(t => t.X2 == 0)
.Solve();
try
{
using var context = new Z3Context();
var result = context.NewTheorem<Symbols<double, int>>()
.Where(t => t.X1 == 1.5)
.Solve();

value = result?.X1;
value = result?.X1;
}
catch (Exception ex)
{
// Captured rather than left to escape: an exception on a bare thread is
// unhandled, so it takes down the test host and the run reports "zero tests
// ran" rather than one failed test. The pin above already does this; this
// counterpart did not, because it was not expected to throw.
captured = ex;
}
});

// Act
thread.Start();
thread.Join(SolveTimeout).ShouldBeTrue("the solve on the invariant-culture thread did not finish");

// Assert
captured.ShouldBeNull();
value.ShouldBe(1.5);
}

Expand Down
5 changes: 1 addition & 4 deletions solutions/Z3.Linq.Tests/TheoremCompositionTests.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,8 +68,7 @@ public void Where_OriginalTheorem_RemainsIndependentlySolvable()
// child's extra constraint did not leak backwards.
using var context = new Z3Context();
var parent = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 == 3)
.Where(t => t.X2 == 0);
.Where(t => t.X1 == 3);
var child = parent.Where(t => t.X1 == 4);

// Act
Expand Down Expand Up @@ -137,7 +136,6 @@ public void Log_WhenNotSet_SolvingDoesNotThrow()
// Act
var result = (from t in context.NewTheorem<Symbols<int, int>>()
where t.X1 == 1
where t.X2 == 0
select t).Solve();

// Assert
Expand All @@ -159,7 +157,6 @@ public void Dispose_CalledOnContext_LeavesTheContextUsable()

var result = (from t in context.NewTheorem<Symbols<int, int>>()
where t.X1 == 11
where t.X2 == 0
select t).Solve();

// Assert
Expand Down
10 changes: 3 additions & 7 deletions solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,7 @@ public void Solve_ConditionalExpression_ThrowsNotSupportedException()
// express if-then-else, so this is a gap rather than a fundamental limit.
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => (t.X1 > 0 ? t.X1 : 0) == 1)
.Where(t => t.X2 == 0);
.Where(t => (t.X1 > 0 ? t.X1 : 0) == 1);

// Act & Assert
Should.Throw<NotSupportedException>(() => theorem.Solve());
Expand All @@ -54,8 +53,7 @@ public void Solve_CallToAnUnrecognisedMethod_ThrowsNotSupportedException()
// (ExpressionVisitor.cs:277).
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => Increment(t.X1) == 2)
.Where(t => t.X2 == 0);
.Where(t => Increment(t.X1) == 2);

// Act & Assert
Should.Throw<NotSupportedException>(() => theorem.Solve());
Expand All @@ -70,8 +68,7 @@ public void Solve_UnsupportedCast_ThrowsNotImplementedException()
// than NotSupportedException - the throw sites are not consistent about which they use.
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => (long)t.X1 == 1L)
.Where(t => t.X2 == 0);
.Where(t => (long)t.X1 == 1L);

// Act & Assert
Should.Throw<NotImplementedException>(() => theorem.Solve());
Expand Down Expand Up @@ -162,7 +159,6 @@ public void Solve_SupportedExpressionsAlongsideRejectedOnes_StillRejects()
using var context = new Z3Context();
var theorem = context.NewTheorem<Symbols<int, int>>()
.Where(t => t.X1 > 0)
.Where(t => t.X2 == 0)
.Where(t => (t.X1 > 5 ? t.X1 : 0) == 6);

// Act & Assert
Expand Down
Loading