1

I would like to use Z3 to reason about a configuration problem using some data from a relational database containing physical properties of materials.

As suggested in this post, I could use an outer loop around the solver. But this works only for sorts with finite domains: I don't see how it would work on infinite domains.

I could represent the whole data tables by Z3 functions from primary keys to attributes, using the if-then-else construct, but the reasoning might use only a few rows in the table: it does not seem efficient.

Another approach would be to create a custom background theory solver that would determine the truth values of atoms by database lookup : has that been done before ?

Do you see some other ways to do it ?

Pierre Carbonnelle
  • 2,305
  • 19
  • 25
  • This [stackoverflow post](https://stackoverflow.com/questions/46508907/smt-solver-with-custom-theories) explains an alternative approach to custom theories. – Pierre Carbonnelle Jul 13 '19 at 13:26
  • I’m not sure why you say “this only works for finite domains.” Can you elaborate on that? Are you concerned with “infinite” search as the solver simply gives you the next assignment to check which again is inconsistent? – alias Jul 13 '19 at 17:41
  • Yes, exactly. The chance that the solver proposes the right instance of a relation is nil on infinite domains. – Pierre Carbonnelle Jul 14 '19 at 19:11
  • You can try modeling infinite domains with uninterpreted sorts; and see how far that takes you. For something like `Int`, you can try to approximate it with a small-bitvector; say 8-bit value. (If you're doing machine arithmetic, that's what you should be using anyhow.) Developing a custom solver is a lot of work, so I'd investigate all other options before diving into one. In particular, maintenance is an issue and unless you can convince z3 folks that you'll support it in perpetuity, it'll be a hard sell for them to incorporate it to main-line. – alias Jul 15 '19 at 01:07

0 Answers0