Solver: avoid failing when nullable columns & Fix column name in join (#1476)

* Fix solver generation when comparision to null

* Add support for not equal

* Not fail when no support conditions happen

* Apply suggestions from code review

Co-authored-by: Agustina Aldasoro <agusaldasoro@users.noreply.github.com>

* Add more supported types and fix join column name

Author: agusaldasoro

core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/ast/SqlComparisonOperator.java

@@ -2,6 +2,7 @@
 
 public enum SqlComparisonOperator {
     EQUALS_TO("="),
+    NOT_EQUALS_TO("<>"),
     GREATER_THAN(">"),
     GREATER_THAN_OR_EQUAL(">="),
     LESS_THAN("<"),

core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java

@@ -310,8 +310,11 @@ public void visit(MinorThanEquals minorThanEquals) {
 
     @Override
     public void visit(NotEqualsTo notEqualsTo) {
-        // TODO This translation should be implemented
-        throw new RuntimeException("Extraction of condition not yet implemented");
+        notEqualsTo.getLeftExpression().accept(this);
+        SqlCondition left = stack.pop();
+        notEqualsTo.getRightExpression().accept(this);
+        SqlCondition right = stack.pop();
+        stack.push(new SqlComparisonCondition(left, SqlComparisonOperator.NOT_EQUALS_TO, right));
     }
 
     @Override

core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt

@@ -42,9 +42,12 @@ class SMTConditionVisitor(
      * @return The corresponding SMT node.
      */
     override fun visit(condition: SqlAndCondition, parameter: Void?): SMTNode {
-        val left = condition.leftExpr.accept(this, parameter) as AssertSMTNode
-        val right = condition.rightExpr.accept(this, parameter) as AssertSMTNode
-        return AssertSMTNode(AndAssertion(listOf(left.assertion, right.assertion)))
+        val left = condition.leftExpr.accept(this, parameter)
+        val right = condition.rightExpr.accept(this, parameter)
+        if (left is EmptySMTNode && right is EmptySMTNode) return EmptySMTNode()
+        if (left is EmptySMTNode) return right
+        if (right is EmptySMTNode) return left
+        return AssertSMTNode(AndAssertion(listOf((left as AssertSMTNode).assertion, (right as AssertSMTNode).assertion)))
     }
 
     /**
@@ -55,8 +58,11 @@ class SMTConditionVisitor(
      * @return The corresponding SMT node.
      */
     override fun visit(condition: SqlOrCondition, parameter: Void?): SMTNode {
-        val conditions = condition.orConditions.map { it.accept(this, parameter) as AssertSMTNode }
-        return AssertSMTNode(OrAssertion(conditions.map { it.assertion }))
+        val conditions = condition.orConditions.map { it.accept(this, parameter) }
+        val nonEmpty = conditions.filterIsInstance<AssertSMTNode>()
+        if (nonEmpty.isEmpty()) return EmptySMTNode()
+        if (nonEmpty.size == 1) return nonEmpty[0]
+        return AssertSMTNode(OrAssertion(nonEmpty.map { it.assertion }))
     }
 
     /**
@@ -67,6 +73,9 @@ class SMTConditionVisitor(
      * @return The corresponding SMT node.
      */
     override fun visit(condition: SqlComparisonCondition, parameter: Void?): SMTNode {
+        if (condition.leftOperand is SqlNullLiteralValue || condition.rightOperand is SqlNullLiteralValue) {
+            return EmptySMTNode() // TODO: Change this when we add support for nullable columns in the db schema
+        }
         val left = getVariableAndLiteral(condition.leftOperand)
         val right = getVariableAndLiteral(condition.rightOperand)
 

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

@@ -14,6 +14,7 @@ import org.evomaster.core.logging.LoggingUtil
 import org.evomaster.core.utils.StringUtils
 import org.evomaster.dbconstraint.ConstraintDatabaseType
 import org.evomaster.dbconstraint.ast.SqlCondition
+import net.sf.jsqlparser.JSQLParserException
 import org.evomaster.dbconstraint.parser.SqlConditionParserException
 import org.evomaster.dbconstraint.parser.jsql.JSqlConditionParser
 import org.evomaster.solver.smtlib.*
@@ -114,7 +115,9 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
                     smt.addNode(constraint)
                 }
             } catch (e: SqlConditionParserException) {
-                throw RuntimeException("Error parsing check expression: " + check.sqlCheckExpression, e)
+                LoggingUtil.getInfoLogger().warn("Could not translate CHECK constraint to SMT-LIB, skipping: ${check.sqlCheckExpression}. Reason: ${e.message}")
+            } catch (e: JSQLParserException) {
+                LoggingUtil.getInfoLogger().warn("Could not translate CHECK constraint to SMT-LIB, skipping: ${check.sqlCheckExpression}. Reason: ${e.message}")
             }
         }
     }
@@ -276,7 +279,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
         for (foreignKey in table.foreignKeys) {
             val referencedTable = findReferencedTable(foreignKey)
             val referencedTableName = referencedTable.id.name.lowercase()
-            val referencedColumnSelector = findReferencedPKSelector(referencedTable, foreignKey)
+            val referencedColumnSelector = findReferencedPKSelector(table, referencedTable, foreignKey)
 
             for (sourceColumn in foreignKey.sourceColumns) {
                 val nodes = assertForEqualsAny(
@@ -328,13 +331,24 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
      * @param foreignKey The foreign key constraint.
      * @return The primary key column name in the referenced table.
      */
-    private fun findReferencedPKSelector(referencedTable: TableDto, foreignKey: ForeignKeyDto): String {
+    private fun findReferencedPKSelector(sourceTable: TableDto, referencedTable: TableDto, foreignKey: ForeignKeyDto): String {
         val referencedPrimaryKeys = referencedTable.columns.filter { it.primaryKey }
-        if (referencedPrimaryKeys.isEmpty()) {
-            throw RuntimeException("Referenced table has no primary key: ${foreignKey.targetTable}")
+        val sourceColumnName = foreignKey.sourceColumns.firstOrNull()
+        val sourceSmtType = sourceColumnName?.let { scn ->
+            sourceTable.columns.firstOrNull { it.name.equals(scn, ignoreCase = true) }
+                ?.let { TYPE_MAP[it.type.uppercase()] }
         }
-        // Assuming single-column primary keys
-        return referencedPrimaryKeys[0].name
+        if (referencedPrimaryKeys.isNotEmpty() &&
+            (sourceSmtType == null || TYPE_MAP[referencedPrimaryKeys[0].type.uppercase()] == sourceSmtType)) {
+            return referencedPrimaryKeys[0].name
+        }
+        // No PK or type mismatch: find a type-compatible column
+        if (sourceSmtType != null) {
+            referencedTable.columns.firstOrNull { TYPE_MAP[it.type.uppercase()] == sourceSmtType }
+                ?.let { return it.name }
+        }
+        return referencedTable.columns.firstOrNull()?.name
+            ?: throw RuntimeException("Referenced table has no columns: ${foreignKey.targetTable}")
     }
 
     /**
@@ -364,11 +378,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
             val where = plainSelect.where
 
             if (where != null) {
-                val condition = parser.parse(where.toString(), toDBType(schema.databaseType))
-                val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first()
-                for (i in 1..numberOfRows) {
-                    val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i)
-                    smt.addNode(constraint)
+                try {
+                    val condition = parser.parse(where.toString(), toDBType(schema.databaseType))
+                    val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first()
+                    for (i in 1..numberOfRows) {
+                        val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i)
+                        smt.addNode(constraint)
+                    }
+                } catch (e: RuntimeException) {
+                    LoggingUtil.getInfoLogger().warn("Could not translate WHERE clause to SMT-LIB, skipping: ${where}. Reason: ${e.message}")
                 }
             }
         }
@@ -390,11 +408,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
                     val onExpressions = join.onExpressions
                     if (onExpressions.isNotEmpty()) {
                         val onExpression = onExpressions.elementAt(0)
-                        val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType))
-                        val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first()
-                        for (i in 1..numberOfRows) {
-                            val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i)
-                            smt.addNode(constraint)
+                        try {
+                            val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType))
+                            val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first()
+                            for (i in 1..numberOfRows) {
+                                val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i)
+                                smt.addNode(constraint)
+                            }
+                        } catch (e: RuntimeException) {
+                            LoggingUtil.getInfoLogger().warn("Could not translate JOIN ON clause to SMT-LIB, skipping: ${onExpression}. Reason: ${e.message}")
                         }
                     }
                 }
@@ -525,8 +547,12 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
             "BIGINT" to "Int",
             "BIT" to "Int",
             "INTEGER" to "Int",
+            "INT2" to "Int",
+            "INT4" to "Int",
+            "INT8" to "Int",
             "TINYINT" to "Int",
             "SMALLINT" to "Int",
+            "NUMERIC" to "Int",
             "TIMESTAMP" to "Int",
             "DATE" to "Int",
             "FLOAT" to "Real",
@@ -539,6 +565,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
             "TEXT" to "String",
             "CHARACTER LARGE OBJECT" to "String",
             "BOOLEAN" to "String",
+            "BOOL" to "String",
+            "UUID" to "String",
+            "JSONB" to "String",
+            "BYTEA" to "String",
         )
     }
 }

core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt

@@ -209,6 +209,27 @@ class SmtLibGeneratorTest {
         }
     }
 
+    /**
+     * Test that a <> (not-equals) condition in the WHERE clause is correctly translated
+     * to a distinct SMT-LIB assertion.
+     */
+    @Test
+    @Throws(JSQLParserException::class)
+    fun selectFromUsersWithNotEquals() {
+        val selectStatement: Statement = CCJSqlParserUtil.parse("SELECT * FROM Users WHERE age <> 30;")
+
+        val response: SMTLib = generator.generateSMT(selectStatement)
+
+        val expected = tableConstraints
+        expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(AGE users1)", "30"))))
+        expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(AGE users2)", "30"))))
+        expected.addNode(CheckSatSMTNode())
+        expected.addNode(GetValueSMTNode("users1"))
+        expected.addNode(GetValueSMTNode("users2"))
+
+        assertEquals(expected, response)
+    }
+
     /**
      * Test the generation of SMT from a simple select statement and a database schema
      * @throws JSQLParserException if the statement is not valid
@@ -383,6 +404,34 @@ class SmtLibGeneratorTest {
         assertEquals(expected, response)
     }
 
+    /**
+     * Test that NULL comparisons in the WHERE clause are skipped (not emitted as invalid SMT-LIB),
+     * and the remaining non-null constraints are still applied.
+     */
+    @Test
+    @Throws(JSQLParserException::class)
+    fun selectFromUsersWithNullComparison() {
+        val selectStatement: Statement = CCJSqlParserUtil.parse("SELECT * FROM Users WHERE name = NULL AND age > 30;")
+
+        val response: SMTLib = generator.generateSMT(selectStatement)
+
+        val expected = tableConstraints
+        // The NULL comparison is skipped; only the non-null constraint is emitted
+        expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users1)", "30")))
+        expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users2)", "30")))
+
+        val satConstraints = arrayOf(
+            CheckSatSMTNode(),
+            GetValueSMTNode("users1"),
+            GetValueSMTNode("users2")
+        )
+        for (constraint in satConstraints) {
+            expected.addNode(constraint)
+        }
+
+        assertEquals(expected, response)
+    }
+
     /**
      * Test that a BIT column type is translated to Int in the SMT-LIB representation.
      */