1) We are adding support for writing custom static properties as first-order formulas. There is a new tokenizer, parser, and evaluator for these formulas. They are directly added to the inference process, and also to the consistency validation check.
We will make a guide on formula writing in the future. Just as an example of how one can reason about uninterpreted or update functions:
\exists x, y: f(0, x) ^ h(x, y) to describe some complex relationship between functions f and h
\forall x, y: f_v3(0, x, y) => f_v3(1, x, y) to say variable v1 activates v3 (if we have a variable v3 with three regulators v1, v2, v3)
2) The whole inference computation now runs completely asynchronously. This means it no longer blocks the main backend thread. It now also reports progress to the front end and is partially cancellable (in particular checkpoints, such as just before starting the evaluation of some property). We also added error handling to the inference process. The symbolic context for each computation is now created automatically based on the properties. Different symbolic contexts are used for different kinds of properties.
In this PR, we are introducing two main concepts:
1) We are adding support for writing custom static properties as first-order formulas. There is a new tokenizer, parser, and evaluator for these formulas. They are directly added to the inference process, and also to the consistency validation check. We will make a guide on formula writing in the future. Just as an example of how one can reason about uninterpreted or update functions:
\exists x, y: f(0, x) ^ h(x, y)to describe some complex relationship between functionsfandh\forall x, y: f_v3(0, x, y) => f_v3(1, x, y)to say variablev1activatesv3(if we have a variablev3with three regulatorsv1,v2,v3)2) The whole inference computation now runs completely asynchronously. This means it no longer blocks the main backend thread. It now also reports progress to the front end and is partially cancellable (in particular checkpoints, such as just before starting the evaluation of some property). We also added error handling to the inference process. The symbolic context for each computation is now created automatically based on the properties. Different symbolic contexts are used for different kinds of properties.