[#110]: Don't search for an UNSAT core unless solver status is INFEASIBLE (#113)

Also adds a test case that is temporarily disabled until [#112] is fixed

Signed-off-by: Athinagoras Skiadopoulos <[email protected]>

Author: askiad

dcm/src/main/java/com/vmware/dcm/backend/ortools/OrToolsSolver.java

@@ -1003,10 +1003,17 @@ private void addSolvePhase(final MethodSpec.Builder output, final IRContext cont
         }
         output.addStatement("return result");
         output.endControlFlow();
+
+        output.beginControlFlow("else if (status == CpSolverStatus.INFEASIBLE)");
         output.addStatement("final List<String> failedConstraints = o.findSufficientAssumptions(solver)");
         output.addStatement("throw new $T(status.toString(), failedConstraints)", SolverException.class);
+        output.endControlFlow();
+        output.beginControlFlow("else");
+        output.addStatement("throw new $T(status.toString())", SolverException.class);
+        output.endControlFlow();
     }
 
+
     private static String tableNameStr(final String tableName) {
         return CaseFormat.UPPER_UNDERSCORE.to(CaseFormat.LOWER_CAMEL, tableName);
     }

dcm/src/test/java/com/vmware/dcm/ModelTest.java

@@ -2202,6 +2202,32 @@ public void corfuModel() {
         model.solve(Set.of("HOSTS", "STRIPES"));
     }
 
+    @Test
+    @Disabled("Enable when https://github.com/vmware/declarative-cluster-management/issues/112 is fixed")
+    public void testSolverTimeLimit() {
+        final String modelName = "testSolverTimeLimit";
+
+        final DSLContext conn = setup();
+        conn.execute("CREATE TABLE t1(k integer, controllable__p1 integer, controllable__p2 integer, primary key (k))");
+
+        final List<String> views = toListOfViews("CREATE VIEW constraint_product AS " +
+                "SELECT * FROM t1 " +
+                "check (controllable__p1 * controllable__p2) = 12;" +
+                "CREATE VIEW constraint_nontrivial_divisor AS " +
+                "SELECT * FROM t1 " +
+                "check controllable__p1 > 1 and controllable__p2 > 1;"
+        );
+
+        conn.execute("insert into t1 values (1, 2, 6)");
+        conn.execute("insert into t1 values (2, 4, 3)");
+
+        final Model model = buildModel(conn, SolverConfig.OrToolsSolver, views, modelName);
+
+        model.updateData();
+        final Result<? extends Record> fetch = model.solve("T1");
+        System.out.println(fetch);
+    }
+
     /**
      * Splits the supplied SQL by ';'
      */