return element;
}
+Element * getElementConst(CSolver *This, VarType type, uint64_t value) {
+ Element * element=allocElementConst(value, type);
+ pushVectorElement(This->allElements, element);
+ return element;
+}
+
Boolean * getBooleanVar(CSolver *This, VarType type) {
Boolean* boolean= allocBooleanVar(type);
pushVectorBoolean(This->allBooleans, boolean);
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;
}
return constraint;
}
-void startEncoding(CSolver* This){
+int startEncoding(CSolver* This){
naiveEncodingDecision(This);
SATEncoder* satEncoder = This->satEncoder;
encodeAllSATEncoder(This, satEncoder);
model_print("%d, ", satEncoder->cnf->solver->solution[i]);
}
model_print("\n");
+ return result;
}
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);
+}
+