Checking for unsatisfiability when using ValueTuple

[NickRedwood]

Hi, thanks for publishing this library.

I found an issue with checking for unsatisfiability when using ValueTuple, as it will return the default all-zero. This is ambiguous as that could be a valid solution, or it could mean unsatisfiable.

using (var ctx = new Z3Context())
{
	
	var theorem = from t in ctx.NewTheorem<(int a, int b)>()
				  where t.a == t.b
				  where t.a > 4
				  where t.b < 2
				  select t;
	
	var result = theorem.Solve();
	
	Console.WriteLine(result);
	// (0,0)
}

Is there a better way?

I explored and found that it's possible to provide a nullable ValueTuple, though this then requires accessing Value explicitly everywhere.

	var theorem2 = from t in ctx.NewTheorem<(int a, int b)?>()
				  where t.Value.a == t.Value.b
				  where t.Value.a > 4
				  where t.Value.b < 2
				  select t;

	var result2 = theorem2.Solve();
	Console.WriteLine(result2);
	// null

Perhaps an improvement could be to provide an overload of Solve or NewTheorem for struct types that lifts them to Nullable?

[idg10]

Here's a hacky sort of a workaround:

var theorem = from t in ctx.NewTheorem<(int a, int b, bool solved)>()
              where t.a == t.b
              where t.a > 4
              where t.b < 2
              where t.solved == true
              select t;

var result = theorem.Solve();

Console.WriteLine(result.solved ? result.ToString() : "Not solved");

Since default(bool) is false, the solved property will be true only if it found a solution.

But this does make me think that maybe what this really needs is a TrySolve method that tells you whether it succeeded, so that we don't need to rely on detecting failing by looking for a default result.

[NickRedwood]

Thanks, that's a clever workaround - even if a little hacky it's better than my Nullable solution I think. A TrySolve type of method would work well in future though.