Adding an API for translating the value of an BooleanOrder

[satune.git] / src / csolver.h

diff --git a/src/csolver.h b/src/csolver.h
index ace6e78fb514f1d5803277d1df3f97b0a73a1163..1e697948e83518465a9c7412c8cdace3c9b24d99 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -5,6 +5,7 @@
 #include "structs.h"
 
 struct CSolver {
+       SATEncoder* satEncoder;
        /** This is a vector of constraints that must be satisfied. */
        VectorBoolean * constraints;
 
@@ -16,16 +17,16 @@ struct CSolver {
 
        /** This is a vector of all element structs that we have allocated. */
        VectorElement * allElements;
-       
+
        /** This is a vector of all predicate structs that we have allocated. */
        VectorPredicate * allPredicates;
-       
+
        /** This is a vector of all table structs that we have allocated. */
        VectorTable * allTables;
-       
+
        /** This is a vector of all order structs that we have allocated. */
        VectorOrder * allOrders;
-       
+
        /** This is a vector of all function structs that we have allocated. */
        VectorFunction* allFunctions;
 };
@@ -34,6 +35,10 @@ struct CSolver {
 
 CSolver * allocCSolver();
 
+/** Delete solver instance. */
+
+void deleteSolver(CSolver * This);
+
 /** This function creates a set containing the elements passed in the array. */
 
 Set * createSet(CSolver *, VarType type, uint64_t * elements, uint num);
@@ -60,6 +65,9 @@ uint64_t createUniqueItem(CSolver *, MutableSet * set);
 
 Element * getElementVar(CSolver *, Set * set);
 
+/** This function creates an element constrant. */
+Element * getElementConst(CSolver *, VarType type, uint64_t value);
+
 /** This function creates a boolean variable. */
 
 Boolean * getBooleanVar(CSolver *, VarType type);
@@ -100,11 +108,23 @@ Boolean * applyLogicalOperation(CSolver *, LogicOp op, Boolean ** array, uint as
 /** This function adds a boolean constraint to the set of constraints
     to be satisfied */
 
-void addBoolean(CSolver *, Boolean * constraint);
+void addConstraint(CSolver *, Boolean * constraint);
 
 /** This function instantiates an order of type type over the set set. */
 Order * createOrder(CSolver *, OrderType type, Set * set);
 
 /** This function instantiates a boolean on two items in an order. */
 Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
+
+/** When everything is done, the client calls this function and then csolver starts to encode*/
+int startEncoding(CSolver*);
+
+/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
+uint64_t getElementValue(CSolver*, Element* element);
+
+/** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
+bool getBooleanValue( CSolver* , Boolean* boolean);
+
+HappenedBefore getOrderConstraintValue(CSolver*, Boolean* orderConstr);
+
 #endif