Adding the c wrapper for CSolver

diff --git a/src/Test/Makefile b/src/Test/Makefile
index 5ec798914b18aa446f9922a6fc31727dd57e3516..f7c2929e7c4d79d2a5907ad628fdf0f8b5f89909 100644 (file)
--- a/src/Test/Makefile
+++ b/src/Test/Makefile
@@ -1,6 +1,7 @@
 BASE := ..
 
 OBJECTS := $(patsubst %.cc, ../bin/%, $(wildcard *.cc))
+COBJECTS := $(patsubst %.c, ../bin/%, $(wildcard *.c))
 
 include $(BASE)/common.mk
 
@@ -8,15 +9,18 @@ DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJ
 
 CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections -I$(BASE)/Backend -I$(BASE)/Tuner
 
-all: $(OBJECTS) ../bin/run.sh
+all: $(OBJECTS) $(COBJECTS) ../bin/run.sh
 
 -include $(DEPS)
 
 ../bin/%: %.cc
        $(CXX) -MMD -MF $(@D)/.$(@F).d -o ../bin/$@ $< $(CPPFLAGS) -L$(BASE)/bin/ -l_cons_comp
 
+../bin/%: %.c
+       $(CC) -MMD -MF $(@D)/.$(@F).d -o ../bin/$@ $< $(CPPFLAGS) -L$(BASE)/bin/ -l_cons_comp
+
 ../bin/run.sh: run.sh
        cp run.sh ../bin/run.sh
 
 clean::
-       rm -f $(OBJECTS) $(DEPS) ../bin/run.sh
+       rm -f $(OBJECTS) $(COBJECTS) $(DEPS) ../bin/run.sh

diff --git a/src/Test/ccsolvertest.c b/src/Test/ccsolvertest.c
new file mode 100644 (file)
index 0000000..3bcb3c6
--- /dev/null
+++ b/src/Test/ccsolvertest.c
@@ -0,0 +1,25 @@
+#include "ccsolver.h"
+#include <stdio.h>
+
+#define SATC_EQUALS 0
+
+int main (int num, char** args){
+       void* solver = CreateCCSolver();
+       long set1[] = {0, 1, 2};
+        long set2[] = {3, 1, 7};
+        void *s1 = createSet(solver,0, set1, 3);
+        void *s2 = createSet(solver,0, set2, 3);
+        void *e1 = getElementVar(solver,s1);
+        void *e2 = getElementVar(solver,s2);
+        void *domain[] = {s1, s2};
+        void *equals = createPredicateOperator(solver,SATC_EQUALS, domain, 2);
+        void *inputs[] = {e1, e2};
+        void* b = applyPredicate(solver,equals, inputs, 2);
+        addConstraint(solver,b);
+        if (solve(solver) == 1)
+                printf("e1=%ld \t e2=%ld\n", getElementValue(solver, e1), getElementValue(solver, e2));
+        else
+                printf("UNSAT\n");
+        deleteCCSolver(solver);
+}
+

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
new file mode 100644 (file)
index 0000000..c58f380
--- /dev/null
+++ b/src/ccsolver.cc
@@ -0,0 +1,139 @@
+#include "csolver.h"
+#include "ccsolver.h"
+
+#define CCSOLVER(solver) ((CSolver*)solver)
+
+void* CreateCCSolver(){
+       return (void*) new CSolver();
+}
+void deleteCCSolver(void* solver){
+       delete CCSOLVER(solver);
+}
+
+void *createSet(void* solver,unsigned int type, void *elements, unsigned int num){
+       return CCSOLVER(solver)->createSet((VarType) type, (uint64_t *)elements, (uint) num);
+}
+
+void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange){
+       return CCSOLVER(solver)->createRangeSet((VarType) type, (uint64_t) lowrange, (uint64_t) highrange);
+}
+
+void *createRangeVar(void* solver,unsigned type, long lowrange, long highrange){
+       return CCSOLVER(solver)->createRangeVar((VarType) type, (uint64_t) lowrange, (uint64_t) highrange);
+}
+
+void *createMutableSet(void* solver,unsigned type){
+       return CCSOLVER(solver)->createMutableSet((VarType) type);
+}
+
+void addItem(void* solver,void *set, long element){
+       CCSOLVER(solver)->addItem((MutableSet*) set, (uint64_t) element);
+}
+
+void finalizeMutableSet(void* solver,void *set){
+       CCSOLVER(solver)->finalizeMutableSet((MutableSet*) set);
+}
+
+void *getElementVar(void* solver,void *set){
+       return CCSOLVER(solver)->getElementVar((Set*) set);
+}
+
+void *getElementConst(void* solver,unsigned type, long value){
+       return CCSOLVER(solver)->getElementConst((VarType) type, (uint64_t) value);
+}
+
+void *getElementRange (void* solver,void *element){
+       return CCSOLVER(solver)->getElementRange ((Element*) element);
+}
+
+void* getBooleanVar(void* solver,unsigned int type){
+       return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
+}
+
+void *createFunctionOperator(void* solver,unsigned int op, void *domain, unsigned int numDomain, void *range,unsigned int overflowbehavior){
+       return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set **)domain, (uint) numDomain, (Set *)range, (OverFlowBehavior) overflowbehavior);
+}
+
+void *createPredicateOperator(void* solver,unsigned int op, void *domain, unsigned int numDomain){
+       return CCSOLVER(solver)->createPredicateOperator((CompOp) op, (Set **)domain, (uint) numDomain);
+}
+
+void *createPredicateTable(void* solver,void *table, unsigned int behavior){
+       return CCSOLVER(solver)->createPredicateTable((Table *)table, (UndefinedBehavior) behavior);
+}
+
+void *createTable(void* solver,void*domains, unsigned int numDomain, void *range){
+       return CCSOLVER(solver)->createTable((Set **)domains, (uint) numDomain, (Set *)range);
+}
+
+void *createTableForPredicate(void* solver,void*domains, unsigned int numDomain){
+       return CCSOLVER(solver)->createTableForPredicate((Set **)domains, (uint) numDomain);
+}
+
+void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result){
+       CCSOLVER(solver)->addTableEntry((Table *)table, (uint64_t *)inputs, (uint) inputSize, (uint64_t) result);
+}
+
+void *completeTable(void* solver,void *table, unsigned int behavior){
+       return CCSOLVER(solver)->completeTable((Table *) table, (UndefinedBehavior) behavior);
+}
+
+void *applyFunction(void* solver,void *function, void*array, unsigned int numArrays, void* overflowstatus){
+       return CCSOLVER(solver)->applyFunction((Function *)function, (Element **)array, (uint) numArrays, BooleanEdge ((Boolean*)overflowstatus));
+}
+
+void* applyPredicateTable(void* solver,void *predicate, void *inputs, unsigned int numInputs, void* undefinedStatus){
+       return CCSOLVER(solver)->applyPredicateTable((Predicate *)predicate, (Element **)inputs, (uint) numInputs, BooleanEdge((Boolean*) undefinedStatus)).getRaw();
+}
+
+void* applyPredicate(void* solver,void *predicate, void *inputs, unsigned int numInputs){
+       return CCSOLVER(solver)->applyPredicate((Predicate *)predicate, (Element **)inputs, (uint) numInputs).getRaw();
+}
+
+void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize){
+       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, (BooleanEdge *)array, (uint) asize).getRaw();
+}
+
+void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2){
+       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg1), BooleanEdge((Boolean*) arg2)).getRaw();
+}
+
+void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg){
+       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg)).getRaw();
+}
+
+void addConstraint(void* solver,void* constraint){
+       CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean*) constraint));
+}
+
+void *createOrder(void* solver,unsigned int type, void *set){
+       return CCSOLVER(solver)->createOrder((OrderType) type, (Set *)set);
+}
+
+void* orderConstraint(void* solver,void *order, long first, long second){
+       return CCSOLVER(solver)->orderConstraint((Order *)order, (uint64_t) first, (uint64_t) second).getRaw();
+}
+
+int solve(void* solver){
+       return CCSOLVER(solver)->solve();
+}
+
+long getElementValue(void* solver,void *element){
+       return (long) CCSOLVER(solver)->getElementValue((Element *)element);
+}
+
+int getBooleanValue(void* solver, void* boolean){
+       return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean*) boolean));
+}
+
+int getOrderConstraintValue(void* solver,void *order, long first, long second){
+       return CCSOLVER(solver)->getOrderConstraintValue((Order *)order, (uint64_t) first, (uint64_t) second);
+}
+
+void printConstraints(void* solver){
+       CCSOLVER(solver)->printConstraints();
+}
+
+
+
+

diff --git a/src/ccsolver.h b/src/ccsolver.h
new file mode 100644 (file)
index 0000000..c14a3e0
--- /dev/null
+++ b/src/ccsolver.h
@@ -0,0 +1,46 @@
+#ifndef __CCSOLVER_H
+#define __CCSOLVER_H
+
+
+typedef void* CCSolver;
+#ifdef __cplusplus
+extern "C" {
+#endif
+void* CreateCCSolver();
+void deleteCCSolver(void* solver);
+void *createSet(void* solver,unsigned int type, void *elements, unsigned int num);
+void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange);
+void *createRangeVar(void* solver,unsigned type, long lowrange, long highrange);
+void *createMutableSet(void* solver,unsigned type);
+void addItem(void* solver,void *set, long element);
+void finalizeMutableSet(void* solver,void *set);
+void *getElementVar(void* solver,void *set);
+void *getElementConst(void* solver,unsigned type, long value);
+void *getElementRange (void* solver,void *element);
+void* getBooleanVar(void* solver,unsigned int type);
+void *createFunctionOperator(void* solver,unsigned int op, void *domain, unsigned int numDomain, void *range,unsigned int overflowbehavior);
+void *createPredicateOperator(void* solver,unsigned int op, void *domain, unsigned int numDomain);
+void *createPredicateTable(void* solver,void *table, unsigned int behavior);
+void *createTable(void* solver,void*domains, unsigned int numDomain, void *range);
+void *createTableForPredicate(void* solver,void*domains, unsigned int numDomain);
+void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result);
+void *completeTable(void* solver,void *table, unsigned int behavior);
+void *applyFunction(void* solver,void *function, void*array, unsigned int numArrays, long overflowstatus);
+void* applyPredicateTable(void* solver,void *predicate, void *inputs, unsigned int numInputs, long undefinedStatus);
+void* applyPredicate(void* solver,void *predicate, void *inputs, unsigned int numInputs);
+void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize);
+void* applyLogicalOperationTwo(void* solver,unsigned int op, long arg1, long arg2);
+void* applyLogicalOperationOne(void* solver,unsigned int op, long arg);
+void addConstraint(void* solver,void* constraint);
+void *createOrder(void* solver,unsigned int type, void *set);
+void* orderConstraint(void* solver,void *order, long first, long second);
+int solve(void* solver);
+long getElementValue(void* solver,void *element);
+int getBooleanValue(void* solver,long boolean);
+int getOrderConstraintValue(void* solver,void *order, long first, long second);
+void printConstraints(void* solver);
+#ifdef __cplusplus
+}
+#endif
+
+#endif

diff --git a/src/common.h b/src/common.h
index 256aaf335a75431bc6cd99235dbded710164388b..3a0eeaa01c4dd3a0ad0c8e9f7416968ef323f968 100644 (file)
--- a/src/common.h
+++ b/src/common.h
@@ -19,7 +19,7 @@
 #include "time.h"
 
 
-#if 1
+#if 0
 extern int model_out;
 extern int model_err;
 extern int switch_alloc;

diff --git a/src/csolver.cc b/src/csolver.cc
index be657815fe789f4f50324ba23f07bb0a893845d6..900746773e9e3217f967d345a09929be64acd2b6 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -583,15 +583,13 @@ int CSolver::solve() {
                }
                delete orderit;
        }
-        model_print("*****************Before any modifications:************\n");
-        printConstraints();
        computePolarities(this);
        long long time2 = getTimeNano();
        model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
-//     Preprocess pp(this);
-//     pp.doTransform();
+       Preprocess pp(this);
+       pp.doTransform();
        long long time3 = getTimeNano();
-//     model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
+       model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
 
        DecomposeOrderTransform dot(this);
        dot.doTransform();
@@ -617,8 +615,6 @@ int CSolver::solve() {
        model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC);
 
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
-               model_print("########## After all modifications: #############\n");
-               printConstraints();
        int result = unsat ? IS_UNSAT : satEncoder->solve();
        model_print("Result Computed in CSolver: %d\n", result);
 

diff --git a/src/mymemory.h b/src/mymemory.h
index b87e2c8cb56dfb4529fefdba336d0e2f17773cba..b78eb5427697f887d87c2d034e73227611a3cc6a 100644 (file)
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -26,7 +26,7 @@
    void * ourrealloc(void *ptr, size_t size);
  */
 
-#if 1
+#if 0
 void *model_malloc(size_t size);
 void model_free(void *ptr);
 void *model_calloc(size_t count, size_t size);