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;
}
}
Boolean * applyPredicate(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs) {
- Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs);
+ return applyPredicateTable(This, predicate, inputs, numInputs, NULL);
+}
+Boolean * applyPredicateTable(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus) {
+ Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
pushVectorBoolean(This->allBooleans, boolean);
return boolean;
}
uint64_t getElementValue(CSolver* This, Element* element){
switch(GETELEMENTTYPE(element)){
case ELEMSET:
+ case ELEMCONST:
+ case ELEMFUNCRETURN:
return getElementValueSATTranslator(This, element);
default:
ASSERT(0);
}
exit(-1);
}
+
+HappenedBefore getOrderConstraintValue(CSolver* This, Order * order, uint64_t first, uint64_t second){
+ return getOrderConstraintValueSATTranslator(This, order, first, second);
+}
+