Adding a boolean for undefinedStatus

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 622c8a338ca83df1c21eee3eaec19bb4dccfc8bf..9f4b2191367e38e18e0ff587bb9a345b98376998 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -24,7 +24,7 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
        return & This -> base;
 }
 
-Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs){
+Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus){
        BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
        GETBOOLEANTYPE(This)= PREDICATEOP;
        This->predicate=predicate;
@@ -35,7 +35,7 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
                pushVectorASTNode(GETELEMENTPARENTS(inputs[i]), (ASTNode *)This);
        }
        initPredicateEncoding(&This->encoding, (Boolean *) This);
-
+       This->undefStatus = undefinedStatus;
        return & This->base;
 }
 

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 928ba41bc78fec2d252e5bb0b6da2cb559752dba..3d3a90639b8b7596c2849fdc749e233ae6ebecb8 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -44,11 +44,12 @@ struct BooleanPredicate {
        Predicate * predicate;
        FunctionEncoding encoding;
        ArrayElement inputs;
+       Boolean* undefStatus;
 };
 
 Boolean * allocBooleanVar(VarType t);
 Boolean * allocBooleanOrder(Order * order, uint64_t first, uint64_t second);
-Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs);
+Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus);
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize);
 void deleteBoolean(Boolean * This);
 

diff --git a/src/Test/buildconstraintstest.c b/src/Test/buildconstraintstest.c
index e8127ca4871e95ea6f03d02e8d667630b617623f..af65c2c00ab7976a8408d94e288ce9828ce5b051 100644 (file)
--- a/src/Test/buildconstraintstest.c
+++ b/src/Test/buildconstraintstest.c
@@ -12,7 +12,8 @@ int main(int numargs, char ** argv) {
        Set * domain[]={s, s};
        Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
        Element * inputs[]={e1, e2};
-       Boolean * b=applyPredicate(solver, equals, inputs, 2);
+       Boolean* overflow = getBooleanVar(solver , 2);
+       Boolean * b=applyPredicate(solver, equals, inputs, 2, overflow);
        addConstraint(solver, b);
 
        uint64_t set2[] = {2, 3};
@@ -30,13 +31,12 @@ int main(int numargs, char ** argv) {
        addTableEntry(solver, table, row4, 2, 2);
        Function * f2 = completeTable(solver, table, IGNOREBEHAVIOR); //its range would be as same as s
        
-       Boolean* overflow = getBooleanVar(solver , 2);
        Element * e3 = applyFunction(solver, f1, inputs, 2, overflow);
        Element * e4 = applyFunction(solver, f2, inputs, 2, overflow);
        Set* domain2[] = {s,rangef1};
        Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
        Element* inputs2 [] = {e4, e3};
-       Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
+       Boolean* pred = applyPredicate(solver, equal2, inputs2, 2, overflow);
        addConstraint(solver, pred);
        
        if (startEncoding(solver)==1)

diff --git a/src/Test/elemequalityunsattest.c b/src/Test/elemequalityunsattest.c
index 1b6addb9fa2806f69a9d96ac34e110379277f900..e433bf729531a4663ca1327f5bf3ad35768d1fb0 100644 (file)
--- a/src/Test/elemequalityunsattest.c
+++ b/src/Test/elemequalityunsattest.c
@@ -11,7 +11,7 @@ int main(int numargs, char ** argv) {
        Set * domain[]={s1, s2};
        Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
        Element * inputs[]={e1, e2};
-       Boolean *b=applyPredicate(solver, equals, inputs, 2);
+       Boolean *b=applyPredicate(solver, equals, inputs, 2, NULL);
        addConstraint(solver, b);
        
        if (startEncoding(solver)==1)

diff --git a/src/Test/funcencodingtest.c b/src/Test/funcencodingtest.c
index 6f3119a2a40851adb1619fd36238fb2b4f22e1a8..e376ca8f6be8ccadff05f7a4a374acea76c51224 100644 (file)
--- a/src/Test/funcencodingtest.c
+++ b/src/Test/funcencodingtest.c
@@ -54,7 +54,7 @@ int main(int numargs, char ** argv) {
        Set* deq[] = {s5,s4};
        Predicate* gt = createPredicateOperator(solver, GT, deq, 2);
        Element* inputs2 [] = {e7, e6};
-       Boolean* pred = applyPredicate(solver, gt, inputs2, 2);
+       Boolean* pred = applyPredicate(solver, gt, inputs2, 2, overflow);
        addConstraint(solver, pred);
        
        if (startEncoding(solver)==1)

diff --git a/src/Test/ltelemconsttest.c b/src/Test/ltelemconsttest.c
index e058b04bc786153e08e53996949505973e135d03..018e36adbbe58e2e77db26e62036ca7f1cd3f7de 100644 (file)
--- a/src/Test/ltelemconsttest.c
+++ b/src/Test/ltelemconsttest.c
@@ -11,7 +11,7 @@ int main(int numargs, char ** argv){
        Set * domain2[]={s1, s3};
        Predicate *lt=createPredicateOperator(solver, LT, domain2, 2);
        Element * inputs2[]={e1, e2};
-       Boolean *b=applyPredicate(solver, lt, inputs2, 2);
+       Boolean *b=applyPredicate(solver, lt, inputs2, 2, NULL);
        addConstraint(solver, b);
        if (startEncoding(solver)==1)
                printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));

diff --git a/src/csolver.c b/src/csolver.c
index 55ac2307d6a7ffb524e1074ce10d53f6585a5738..2f3210d5f2036b179c25e4718cc84661f1b0d16b 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -164,8 +164,8 @@ Element * applyFunction(CSolver *This, Function * function, Element ** array, ui
        return element;
 }
 
-Boolean * applyPredicate(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs) {
-       Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs);
+Boolean * applyPredicate(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus) {
+       Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
        pushVectorBoolean(This->allBooleans, boolean);
        return boolean;
 }

diff --git a/src/csolver.h b/src/csolver.h
index 99cba299e389e121afaff8140bb480c13f16b95d..2a3fea0332de425893522cee00255e7c2ff6e5ce 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -103,7 +103,7 @@ Element * applyFunction(CSolver *, Function * function, Element ** array, uint n
 
 /** This function applies a predicate to the Elements in its input. */
 
-Boolean * applyPredicate(CSolver *, Predicate * predicate, Element ** inputs, uint numInputs);
+Boolean * applyPredicate(CSolver *, Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus);
 
 /** This function applies a logical operation to the Booleans in its input. */