Adding UndefinedBehavior + TablePredicate to client APIs

diff --git a/src/AST/function.c b/src/AST/function.c
index 20e57b0d008acbdb5ec314ffa582807398440eed..a67fe291bfa4372d26d8b833fbc0707071f0dd77 100644 (file)
--- 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 28f53c7d79d4cd2fb2e489fe1ce3aa35ed7e945f..562d3e9e06f096ab89155aa3621418b94e333e52 100644 (file)
--- 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 8f7b5ee97130eed6ca32b080967d8447968f9593..24d1f3452ba52e04bdde2fd409c4c90d3d993f40 100644 (file)
--- 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 72d23ddf7f1f9b8d06427f072e9ae7dcaec8fe56..f212ff956ddb287123a7820fbc656a2ef98f0e28 100644 (file)
--- 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 e795038dfcacbb48a1d1dab6347f4b20773ae0fb..e8127ca4871e95ea6f03d02e8d667630b617623f 100644 (file)
--- 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 0dacef0a4b39dce55184711631efcc1425422230..6f3119a2a40851adb1619fd36238fb2b4f22e1a8 100644 (file)
--- 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/ordertest.c b/src/Test/ordertest.c
new file mode 100644 (file)
index 0000000..4970cac
--- /dev/null
+++ b/src/Test/ordertest.c
@@ -0,0 +1,23 @@
+
+#include "csolver.h"
+
+int main(int numargs, char ** argv) {
+       CSolver * solver=allocCSolver();
+       uint64_t set1[]={5, 1, 4};
+       Set * s=createSet(solver, 0, set1, 3);
+       Order* order = createOrder(solver, TOTAL, s);
+       Boolean* b1=  orderConstraint(solver, order, 5, 1);
+       Boolean* b2=  orderConstraint(solver, order, 1, 4);
+       addConstraint(solver, b1);
+       addConstraint(solver, b2);
+       if (startEncoding(solver)==1)
+               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d O(1111,5)=%d\n", 
+                       getOrderConstraintValue(solver, order, 5, 1), 
+                       getOrderConstraintValue(solver, order, 1, 4),
+                       getOrderConstraintValue(solver, order, 5, 4),
+                       getOrderConstraintValue(solver, order, 1, 5),
+                       getOrderConstraintValue(solver, order, 1111, 5));
+       else
+               printf("UNSAT\n");
+       deleteSolver(solver);
+}
\ No newline at end of file

diff --git a/src/Test/testorder.c b/src/Test/testorder.c
deleted file mode 100644 (file)
index 4970cac..0000000
--- a/src/Test/testorder.c
+++ /dev/null
@@ -1,23 +0,0 @@
-
-#include "csolver.h"
-
-int main(int numargs, char ** argv) {
-       CSolver * solver=allocCSolver();
-       uint64_t set1[]={5, 1, 4};
-       Set * s=createSet(solver, 0, set1, 3);
-       Order* order = createOrder(solver, TOTAL, s);
-       Boolean* b1=  orderConstraint(solver, order, 5, 1);
-       Boolean* b2=  orderConstraint(solver, order, 1, 4);
-       addConstraint(solver, b1);
-       addConstraint(solver, b2);
-       if (startEncoding(solver)==1)
-               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d O(1111,5)=%d\n", 
-                       getOrderConstraintValue(solver, order, 5, 1), 
-                       getOrderConstraintValue(solver, order, 1, 4),
-                       getOrderConstraintValue(solver, order, 5, 4),
-                       getOrderConstraintValue(solver, order, 1, 5),
-                       getOrderConstraintValue(solver, order, 1111, 5));
-       else
-               printf("UNSAT\n");
-       deleteSolver(solver);
-}
\ No newline at end of file

diff --git a/src/csolver.c b/src/csolver.c
index cfef6f4f8af780dba58f393bf47eaa856e1cab7b..55ac2307d6a7ffb524e1074ce10d53f6585a5738 100644 (file)
--- 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 23c35e059811ba3dee0aaabe6907def5478f7107..99cba299e389e121afaff8140bb480c13f16b95d 100644 (file)
--- 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. */