From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 20 Jul 2017 23:20:30 +0000 (-0700)
Subject: Adding edge cases for table-based predicate/function
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=b04537e1ded8a7044d457147b7fb01bfb283258a;p=satune.git

Adding edge cases for table-based predicate/function
---

diff --git a/src/Backend/satfuncopencoder.c b/src/Backend/satfuncopencoder.c
index 5cbd86c..881839f 100644
--- 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 c15e822..6d11998 100644
--- 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);