Fix foreign keys smtlib gen

[agusaldasoro]

Problem

The SMT-LIB formula always asserts every foreign key in the schema, so each row of a referencing table must point at a row of the referenced table. get-value, however, only requested rows of the tables named in the query. For SELECT * FROM book WHERE pages > 10, Z3 returned a book row whose author matched an author row that was never requested or inserted. The database rejected the INSERT, and the query stayed empty.

A second problem was hidden behind the first. SMTResultParser stores the rows in a HashMap, so they came back in arbitrary order. Even with every row requested, a row could be inserted before the row it references.

Fix

• SmtLibGenerator: the tables passed to get-value now include every table reachable through foreign keys from the tables in the query.
• SMTLibZ3DbConstraintSolver: the rows of a solution are sorted so that each row comes after the rows it references, and rows of the same table come by row index. Self-references and cycles are ignored for ordering, because no order can satisfy them.

sqlZ3NumberOfRows (k) still applies to every table, including the tables added through foreign keys. A query now yields k INSERTs for each table in the query and for each table those tables reference, directly or indirectly.