From eb8bfa610f09bc0c4ad37eb0ee2e6685ea7e6507 Mon Sep 17 00:00:00 2001 From: Hamed Date: Tue, 18 Jul 2017 15:42:19 -0700 Subject: [PATCH] Adding UndefinedBehavior + TablePredicate to client APIs --- src/AST/function.c | 3 ++- src/AST/function.h | 3 ++- src/AST/predicate.c | 2 ++ src/AST/table.c | 2 ++ src/Test/buildconstraintstest.c | 2 +- src/Test/funcencodingtest.c | 6 +++--- src/Test/{testorder.c => ordertest.c} | 0 src/csolver.c | 14 ++++++++++++-- src/csolver.h | 6 +++++- 9 files changed, 29 insertions(+), 9 deletions(-) rename src/Test/{testorder.c => ordertest.c} (100%) diff --git a/src/AST/function.c b/src/AST/function.c index 20e57b0..a67fe29 100644 --- a/src/AST/function.c +++ b/src/AST/function.c @@ -13,10 +13,11 @@ Function* allocFunctionOperator(ArithOp op, Set ** domain, uint numDomain, Set * return &This->base; } -Function* allocFunctionTable (Table* table){ +Function* allocFunctionTable (Table* table, UndefinedBehavior undefBehavior){ FunctionTable* This = (FunctionTable*) ourmalloc(sizeof(FunctionTable)); GETFUNCTIONTYPE(This)=TABLEFUNC; This->table = table; + This->undefBehavior = undefBehavior; return &This->base; } diff --git a/src/AST/function.h b/src/AST/function.h index 28f53c7..562d3e9 100644 --- a/src/AST/function.h +++ b/src/AST/function.h @@ -22,10 +22,11 @@ struct FunctionOperator { struct FunctionTable { Function base; Table* table; + UndefinedBehavior undefBehavior; }; Function* allocFunctionOperator(ArithOp op, Set ** domain, uint numDomain, Set * range, OverFlowBehavior overflowbehavior); -Function* allocFunctionTable (Table* table); +Function* allocFunctionTable (Table* table, UndefinedBehavior behavior); uint64_t applyFunctionOperator(FunctionOperator* This, uint numVals, uint64_t * values); bool isInRangeFunction(FunctionOperator *This, uint64_t val); void deleteFunction(Function* This); diff --git a/src/AST/predicate.c b/src/AST/predicate.c index 8f7b5ee..24d1f34 100644 --- a/src/AST/predicate.c +++ b/src/AST/predicate.c @@ -1,6 +1,7 @@ #include "predicate.h" #include "boolean.h" #include "set.h" +#include "table.h" Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain){ PredicateOperator* This = ourmalloc(sizeof(PredicateOperator)); @@ -11,6 +12,7 @@ Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain){ } Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior){ + ASSERT(table->range == NULL); PredicateTable* This = ourmalloc(sizeof(PredicateTable)); GETPREDICATETYPE(This) = TABLEPRED; This->table=table; diff --git a/src/AST/table.c b/src/AST/table.c index 72d23dd..f212ff9 100644 --- a/src/AST/table.c +++ b/src/AST/table.c @@ -15,6 +15,8 @@ Table * allocTable(Set **domains, uint numDomain, Set * range){ void addNewTableEntry(Table* This, uint64_t* inputs, uint inputSize, uint64_t result){ ASSERT(getSizeArraySet( &This->domains) == inputSize); + if(This->range==NULL) + ASSERT(result == true || result == false); pushVectorTableEntry(&This->entries, allocTableEntry(inputs, inputSize, result)); } diff --git a/src/Test/buildconstraintstest.c b/src/Test/buildconstraintstest.c index e795038..e8127ca 100644 --- a/src/Test/buildconstraintstest.c +++ b/src/Test/buildconstraintstest.c @@ -28,7 +28,7 @@ int main(int numargs, char ** argv) { addTableEntry(solver, table, row2, 2, 0); addTableEntry(solver, table, row3, 2, 2); addTableEntry(solver, table, row4, 2, 2); - Function * f2 = completeTable(solver, table); //its range would be as same as s + 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); diff --git a/src/Test/funcencodingtest.c b/src/Test/funcencodingtest.c index 0dacef0..6f3119a 100644 --- a/src/Test/funcencodingtest.c +++ b/src/Test/funcencodingtest.c @@ -26,7 +26,7 @@ int main(int numargs, char ** argv) { uint64_t row2[] = {6, 4}; addTableEntry(solver, t1, row1, 2, 3); addTableEntry(solver, t1, row2, 2, 1); - Function * f2 = completeTable(solver, t1); + Function * f2 = completeTable(solver, t1, IGNOREBEHAVIOR); Element * e4 = applyFunction(solver, f2, in1, 2, overflow); Set *d2[] = {s1}; @@ -34,7 +34,7 @@ int main(int numargs, char ** argv) { Table* t2 = createTable(solver, d2, 1, s1); uint64_t row3[] = {6}; addTableEntry(solver, t2, row3, 1, 6); - Function * f3 = completeTable(solver, t2); + Function * f3 = completeTable(solver, t2, IGNOREBEHAVIOR); Element * e5 = applyFunction(solver, f3, in2, 1, overflow); Set *d3[] = {s2, s3, s1}; @@ -48,7 +48,7 @@ int main(int numargs, char ** argv) { addTableEntry(solver, t3, row5, 3, 1); addTableEntry(solver, t3, row6, 3, 2); addTableEntry(solver, t3, row7, 3, 1); - Function * f4 = completeTable(solver, t3); + Function * f4 = completeTable(solver, t3, IGNOREBEHAVIOR); Element * e6 = applyFunction(solver, f4, in3, 3, overflow); Set* deq[] = {s5,s4}; diff --git a/src/Test/testorder.c b/src/Test/ordertest.c similarity index 100% rename from src/Test/testorder.c rename to src/Test/ordertest.c diff --git a/src/csolver.c b/src/csolver.c index cfef6f4..55ac230 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -132,18 +132,28 @@ Predicate * createPredicateOperator(CSolver *This, CompOp op, Set ** domain, uin return predicate; } +Predicate * createPredicateTable(CSolver *This, Table* table, UndefinedBehavior behavior){ + Predicate* predicate = allocPredicateTable(table, behavior); + pushVectorPredicate(This->allPredicates, predicate); + return predicate; +} + Table * createTable(CSolver *This, Set **domains, uint numDomain, Set * range) { Table* table= allocTable(domains,numDomain,range); pushVectorTable(This->allTables, table); return table; } +Table * createTableForPredicate(CSolver *solver, Set **domains, uint numDomain){ + return createTable(solver, domains, numDomain, NULL); +} + void addTableEntry(CSolver *This, Table* table, uint64_t* inputs, uint inputSize, uint64_t result) { addNewTableEntry(table,inputs, inputSize,result); } -Function * completeTable(CSolver *This, Table * table) { - Function* function = allocFunctionTable(table); +Function * completeTable(CSolver *This, Table * table, UndefinedBehavior behavior) { + Function* function = allocFunctionTable(table, behavior); pushVectorFunction(This->allFunctions,function); return function; } diff --git a/src/csolver.h b/src/csolver.h index 23c35e0..99cba29 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -81,17 +81,21 @@ Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, ui Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, uint numDomain); +Predicate * createPredicateTable(CSolver *solver, Table* table, UndefinedBehavior behavior); + /** This function creates an empty instance table.*/ Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range); +Table * createTablePredicate(CSolver *solver, Set **domains, uint numDomain); + /** This function adds an input output relation to a table. */ void addTableEntry(CSolver *solver, Table* table, uint64_t* inputs, uint inputSize, uint64_t result); /** This function converts a completed table into a function. */ -Function * completeTable(CSolver *, Table *); +Function * completeTable(CSolver *, Table *, UndefinedBehavior behavior); /** This function applies a function to the Elements in its input. */ -- 2.34.1