We know how to invert the function and find the list of values of s such that String.isPrefix s "abcd" will return true. In fact it's a property of the String.isPrefix function.
So, we allow functions to declare inverters. In this case, the String.isPrefix function accepts the argument pattern "f a0 a1", and if argument 0 is the goal - the variable whose possible values we wish to enumerate - then we can generate the expression prefixesOf a1.
At first only built-in functions will be able to declare inverters. But later we will allow user-defined functions to define them. We may also convert existing logic - e.g. that a0 elem a1 can be inverted and a1 is the list of possible values of a0 - into inverters.
Consider the query
We know how to invert the function and find the list of values of
s
such thatString.isPrefix s "abcd"
will returntrue
. In fact it's a property of theString.isPrefix
function.So, we allow functions to declare inverters. In this case, the
String.isPrefix
function accepts the argument pattern "f a0 a1", and if argument 0 is the goal - the variable whose possible values we wish to enumerate - then we can generate the expressionprefixesOf a1
.At first only built-in functions will be able to declare inverters. But later we will allow user-defined functions to define them. We may also convert existing logic - e.g. that
a0 elem a1
can be inverted anda1
is the list of possible values ofa0
- into inverters.