Adding edge cases for table-based predicate/function

diff --git a/src/Backend/satfuncopencoder.c b/src/Backend/satfuncopencoder.c
index 5cbd86ca95f62d308afbd2f7df3d867957a1dc32..881839fb5cff6b2c784f8a993f24cc1e780b9503 100644 (file)
--- a/src/Backend/satfuncopencoder.c
+++ b/src/Backend/satfuncopencoder.c
@@ -188,7 +188,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
        }
        if(getSizeVectorEdge(clauses) == 0){
                deleteVectorEdge(clauses);
-               return E_False;
+               return;
        }
        Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        addConstraintCNF(This->cnf, cor);

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index c15e822656d64ad7503a454451b1d3bf2a14c492..6d11998eb24bbdc19c16044e55ac33b2359129e1 100644 (file)
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -147,7 +147,10 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
                        }
                }
        }
-
+       if(getSizeVectorEdge(clauses) == 0){
+               deleteVectorEdge(clauses);
+               return E_False;
+       }
        Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        deleteVectorEdge(clauses);
        return generateNegation ? constraintNegate(cor) : cor;
@@ -287,7 +290,10 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
                        }
                }
        }
-
+       if(getSizeVectorEdge(clauses) == 0){
+               deleteVectorEdge(clauses);
+               return;
+       }
        Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        addConstraintCNF(This->cnf, cor);
        deleteVectorEdge(clauses);