Résumé | We have been designing a language in which programmers can mix
the logic and functional styles. In the functional style
programmers introduce variables and assign the variables
values be describing a computation that evaluates to the
answer desired.
In our language one can also introduce variables by describing
what properties their values should have using first order
logic. The language implementation automatically searches for
solutions.
The language lets the programmer mix computation based
programs with search based programs in a completely
transparent manner.
The kind of search is directed by the type of value being
sought, and the particular operands in the logic used to
describe its properties. we use general purpose tools like
SAT solvers, SMT solvers, the Simplex algorithm, and
Narrowing to actually perform the search.
Creation of the search tree, and the strategy of searching
the tree are separated, and the user can specify a different
strategy for each search, yet a single answer may involve
several searches, and all these are coordinated in a
transparent manner. |