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;
}
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);
#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));
}
Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior){
+ ASSERT(table->range == NULL);
PredicateTable* This = ourmalloc(sizeof(PredicateTable));
GETPREDICATETYPE(This) = TABLEPRED;
This->table=table;
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));
}
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);
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};
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};
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};
--- /dev/null
+
+#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
+++ /dev/null
-
-#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
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;
}
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. */