From 51284423bbf2892559139c683c7df54d4fdf5e29 Mon Sep 17 00:00:00 2001 From: Hamed Date: Tue, 18 Jul 2017 16:14:45 -0700 Subject: [PATCH] Adding a boolean for undefinedStatus --- src/AST/boolean.c | 4 ++-- src/AST/boolean.h | 3 ++- src/Test/buildconstraintstest.c | 6 +++--- src/Test/elemequalityunsattest.c | 2 +- src/Test/funcencodingtest.c | 2 +- src/Test/ltelemconsttest.c | 2 +- src/csolver.c | 4 ++-- src/csolver.h | 2 +- 8 files changed, 13 insertions(+), 12 deletions(-) diff --git a/src/AST/boolean.c b/src/AST/boolean.c index 622c8a3..9f4b219 100644 --- 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 928ba41..3d3a906 100644 --- 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 e8127ca..af65c2c 100644 --- 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 1b6addb..e433bf7 100644 --- 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 6f3119a..e376ca8 100644 --- 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 e058b04..018e36a 100644 --- 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 55ac230..2f3210d 100644 --- 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 99cba29..2a3fea0 100644 --- 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. */ -- 2.34.1