Extend Must Analysis

[satune.git] / src / csolver.h

diff --git a/src/csolver.h b/src/csolver.h
index 99cba299e389e121afaff8140bb480c13f16b95d..b35f80100b278d6846b77eaefaa3e3aded85e134 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -87,8 +87,7 @@ Predicate * createPredicateTable(CSolver *solver, Table* table, UndefinedBehavio
 
 Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range);
 
-Table * createTablePredicate(CSolver *solver, Set **domains, uint numDomain);
-
+Table * createTableForPredicate(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);
@@ -103,6 +102,8 @@ Element * applyFunction(CSolver *, Function * function, Element ** array, uint n
 
 /** This function applies a predicate to the Elements in its input. */
 
+Boolean * applyPredicateTable(CSolver *, Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus);
+
 Boolean * applyPredicate(CSolver *, Predicate * predicate, Element ** inputs, uint numInputs);
 
 /** This function applies a logical operation to the Booleans in its input. */