I have been playing around with LINQ to Z3 for fun (not production use).
I've ended up with this syntax as a start:
var i = 123;
var test2 = from t in TheormProver.NewTheorm()
let f = TheormProver.Func<int, bool>()
let a = TheormProver.Int
let g = TheormProver.Func<bool, int>()
where !f(a * 2) && g(f(g(f(4)))) == i * a && a < g(f(a))
select new { f = f.ToString(), g = g.ToString(), a, asd = "Test extra property" };
var solution = test2.Solve(); // Edited in for clarification
// note that test2 is a TheormProver<T> which has a "T Solve()" method defined.
The static TheromProver.Int
and TheormProver.Func
methods/properties simply return a basic type (as per their name) currently.
Moving forwards I want to make a sort of Variable<T>
type that contains more information than just a value.
TL;DR: The problem I'm having is that I want f
and g
variables to be a custom type that I can add fields and properties to, but I still want to be able to use them with the syntax I've got in the where clause (i.e. as a method/Func
).
So, How do I create a custom type that can be used in method syntax while adding/having my own properties?
Note that I don't care if calling the method does nothing, or doesn't work as I'll be manipulating the where clause so they'll never get invoked/executed.
Example:
var test2 = from t in TheormProver.NewTheorm()
let f = TheormProver.Func<int, bool>()
let a = TheormProver.Int
where !f(a * 2) && a > 3 // f is used to create a method call expression
select new { f , a };
var testSolution = test2.Solve();
var fSolution = testSolution.f; // F is its own type with unique properties/fields.
var fConstraints = fSolution.Constraints;
var fSomeProperty = fSolution.SomeProperty;
foreach(var constraint in fConstraints)
{
//.....
}
I've mocked up a quick example of the work in progress syntax I have so far:
http://liveworkspace.org/code/3Fm6JM$0
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Linq.Expressions;
namespace ConsoleApplication1
{
class TheormProver
{
public static int Int { get { return default(int); } } // Really this would return my Variable<int>
public static Func<T, TResult> Func<T, TResult>() { return default(Func<T, TResult>); } // Really this would return my Variable<Func<T, TResult>>
protected List<Expression> Constraints; // Holds constraints / where clauses that get translated into the Z3 language
//This gets called when we do the first "let" and gets us into the correctly typed world with a generic parameter
public virtual TheormProver<T> Select<T>(Func<TheormProver, T> sel)
{
return new TheormProver<T>(Constraints);
}
}
// This is what the user of the library sees and is returned by a from t in new TheormProver(). T will be the anonymous type from the last let
class TheormProver<T> : TheormProver
{
public TheormProver(List<Expression> Constraints)
{
}
// This gets called on subsequent "let"s, going from the anonymous type with one property "f" to one with 2, "f, g". Chaining this way allows as many lets as we want
public virtual TheormProver<U> Select<U>(Expression<Func<T, U>> sel)
{
return new TheormProver<T, U>(sel, Constraints.ToList());
}
public virtual TheormProver<T> Where(Expression<Func<T, bool>> constraint)
{
var result = (TheormProver<T>)this; // This should be a clone to allow composable queries
result.Constraints.Add(constraint);
return result;
}
public virtual T Solve(out bool foundSolution)
{
// TODO: Call Z3 and get a solution
foundSolution = false;
return default(T);
}
}
internal class TheormProver<T, U> : TheormProver<U>
{
private LambdaExpression Selector;
private TheormProver<T> InternalTheorumProver;
public TheormProver(Expression<Func<T, U>> selector, List<Expression> constraints)
: base(constraints)
{
Selector = selector;
InternalTheorumProver = new TheormProver<T>(constraints);
}
}
class Program
{
static void Main(string[] args)
{
var test = from t in new TheormProver()
let f = TheormProver.Func<int, bool>()
let g = TheormProver.Func<bool, int>()
let a = TheormProver.Int
where g(f(a)) == 0
select new { f, g, a };
bool foundSolution;
var testSolution = test.Solve(out foundSolution);
}
}
}
I've created a simple 'testbed' for your original code: http://liveworkspace.org/code/3Bl7wC$0.
With, a bit of dynamic magic, you can have the following class as a drop-in replacement for
Func<T1, T2>
:As you can see, it defines you class as being "dynamic" and allows you to try and invoke it as if it were a delegate/function/... a general callable:
Here's proof it works: http://liveworkspace.org/code/4kBypd$0
Output:
Full code for reference:
You can't add custom members to delegate types and you cannot overload
operator ()
in C#. That leaves you with extension methods.Now, you don't want to add extensions to very general delegate types like
Func<int, int>
because that pollutes the namespace. I suggest you create custom delegates like this:Then you can add extensions to
Z3Func
.The extension calls will end up as static method calls in the expression tree you are analyzing.