From b04537e1ded8a7044d457147b7fb01bfb283258a Mon Sep 17 00:00:00 2001 From: Hamed Date: Thu, 20 Jul 2017 16:20:30 -0700 Subject: [PATCH] Adding edge cases for table-based predicate/function --- src/Backend/satfuncopencoder.c | 2 +- src/Backend/satfunctableencoder.c | 10 ++++++++-- 2 files changed, 9 insertions(+), 3 deletions(-) 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); -- 2.34.1