Solver: avoid failing when nullable columns & Fix column name in join

[agusaldasoro]

This pull request introduces several improvements and bug fixes to the SMT-LIB generation and SQL parsing logic, particularly around handling SQL conditions, foreign key resolution, and database type mappings. The changes add support for the <> (not equals) operator, improve robustness when parsing SQL (especially with nulls and type mismatches), and expand coverage for more database column types. Tests have also been added to ensure correct handling of these scenarios.

SQL condition handling and parsing improvements:

• Added support for the <> (not equals) SQL operator in both the AST and the parser, allowing such conditions to be correctly translated into SMT-LIB assertions. [1] [2] [3]
• Improved the SMTConditionVisitor to gracefully handle SQL conditions involving NULL by skipping them, and to better manage empty sub-conditions in AND/OR expressions. [1] [2] [3] [4]

SMT-LIB generator robustness:

• Enhanced error handling in the SMT-LIB generator to log warnings and skip problematic CHECK constraints, WHERE clauses, and JOIN ON clauses instead of throwing exceptions, including support for JSQLParser exceptions. [1] [2] [3] [4]

Foreign key and column type mapping:

• Improved foreign key resolution logic to better handle cases where the referenced table's primary key does not match the source column's type, falling back to type-compatible columns or the first available column if necessary. [1] [2]
• Expanded the mapping of SQL types to SMT-LIB types to cover more database-specific types (e.g., INT2, INT4, INT8, NUMERIC, BOOL, UUID, JSONB, BYTEA). [1] [2]

Testing:

• Added tests to verify correct SMT-LIB translation for <> (not equals) conditions and to ensure that NULL comparisons are skipped, with only valid constraints emitted. [1] [2]