Clean up code and make delete the convention for functions that free structs

diff --git a/src/Makefile b/src/Makefile
index c9d26123475cee1fbe4b69838db7ee38ec30f575..fd8e9a9d5801002dd263c9207ae1ff162c1f29c0 100644 (file)
--- a/src/Makefile
+++ b/src/Makefile
@@ -4,7 +4,7 @@ PHONY += directories
 MKDIR_P = mkdir -p
 OBJ_DIR = bin
 
 MKDIR_P = mkdir -p
 OBJ_DIR = bin
 

-C_SOURCES := set.c mutableset.c element.c function.c order.c table.c predicate.c boolean.c csolver.c structs.c constraint.c
+C_SOURCES := set.c mutableset.c element.c function.c order.c table.c predicate.c boolean.c csolver.c structs.c constraint.c inc_solver.c

 
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 
 
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 

diff --git a/src/constraint.c b/src/constraint.c
index be7c73c884ce5a4ec4e4fe61417f89c5ef77399b..921096fae0cefa7a61373d76de3d661a7cdaaa5a 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -9,7 +9,7 @@
 
 #include "constraint.h"
 #include "mymemory.h"
 
 #include "constraint.h"
 #include "mymemory.h"

-//#include "inc_solver.h"
+#include "inc_solver.h"

 
 Constraint ctrue={TRUE, 0xffffffff, NULL, NULL};
 Constraint cfalse={FALSE, 0xffffffff, NULL, NULL};
 
 Constraint ctrue={TRUE, 0xffffffff, NULL, NULL};
 Constraint cfalse={FALSE, 0xffffffff, NULL, NULL};


@@ -60,31 +60,31 @@ Constraint * allocVarConstraint(CType t, uint v) {
        return this;
 }
 
        return this;
 }
 

-void freeConstraint(Constraint *this) {
+void deleteConstraint(Constraint *this) {

        if (this->operands!=NULL)
                ourfree(this->operands);
 }
 
        if (this->operands!=NULL)
                ourfree(this->operands);
 }
 

-/*void dumpConstraint(Constraint * this, IncrementalSolver *solver) {
+void dumpConstraint(Constraint * this, IncrementalSolver *solver) {

        if (this->type==VAR) {
        if (this->type==VAR) {

-               solver->addClauseLiteral(this->numoperandsorvar);
-               solver->addClauseLiteral(0);
+               addClauseLiteral(solver, this->numoperandsorvar);
+               addClauseLiteral(solver, 0);

        } else if (this->type==NOTVAR) {
        } else if (this->type==NOTVAR) {

-               solver->addClauseLiteral(-this->numoperandsorvar);
-               solver->addClauseLiteral(0);
+               addClauseLiteral(solver, -this->numoperandsorvar);
+               addClauseLiteral(solver, 0);

        } else {
                ASSERT(this->type==OR);
                for(uint i=0;i<this->numoperandsorvar;i++) {
                        Constraint *c=this->operands[i];
                        if (c->type==VAR) {
        } else {
                ASSERT(this->type==OR);
                for(uint i=0;i<this->numoperandsorvar;i++) {
                        Constraint *c=this->operands[i];
                        if (c->type==VAR) {

-                               solver->addClauseLiteral(c->numoperandsorvar);
+                               addClauseLiteral(solver, c->numoperandsorvar);

                        } else if (c->type==NOTVAR) {
                        } else if (c->type==NOTVAR) {

-                               solver->addClauseLiteral(-c->numoperandsorvar);
+                               addClauseLiteral(solver, -c->numoperandsorvar);

                        } else ASSERT(0);
                }
                        } else ASSERT(0);
                }

-               solver->addClauseLiteral(0);
+               addClauseLiteral(solver, 0);

        }
        }

-       }*/
+}

 
 void internalfreeConstraint(Constraint * this) {
        switch(this->type) {
 
 void internalfreeConstraint(Constraint * this) {
        switch(this->type) {


@@ -116,7 +116,7 @@ void freerecConstraint(Constraint *this) {
                                freerecConstraint(this->operands[i]);
                }
                this->type=BOGUS;
                                freerecConstraint(this->operands[i]);
                }
                this->type=BOGUS;

-               freeConstraint(this);
+               deleteConstraint(this);

        }
 }
 
        }
 }
 


@@ -251,12 +251,12 @@ bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
                                freerecConstraint(getVectorConstraint(to, j));
                        clearVectorConstraint(to);
                        pushVectorConstraint(to, &ctrue);
                                freerecConstraint(getVectorConstraint(to, j));
                        clearVectorConstraint(to);
                        pushVectorConstraint(to, &ctrue);

-                       freeVectorConstraint(from);
+                       deleteVectorConstraint(from);

                        return true;
                }
                pushVectorConstraint(to, c);
        }
                        return true;
                }
                pushVectorConstraint(to, c);
        }

-       freeVectorConstraint(from);
+       deleteVectorConstraint(from);

        return false;
 }
 
        return false;
 }
 

diff --git a/src/constraint.h b/src/constraint.h
index 9f555d4527045499f9c187ad4c3d39e419b0ee28..06bb1d18f74488a6e3da4b760d45120edad2faa2 100644 (file)
--- a/src/constraint.h
+++ b/src/constraint.h
@@ -30,7 +30,7 @@ Constraint * allocUnaryConstraint(CType t, Constraint *l);
 Constraint * allocArrayConstraint(CType t, uint num, Constraint ** array);
 Constraint * allocVarConstraint(CType t, uint var);
 
 Constraint * allocArrayConstraint(CType t, uint num, Constraint ** array);
 Constraint * allocVarConstraint(CType t, uint var);
 

-void freeConstraint(Constraint *);
+void deleteConstraint(Constraint *);

 void printConstraint(Constraint * c);
 void dumpConstraint(Constraint * c, IncrementalSolver *solver);
 uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
 void printConstraint(Constraint * c);
 void dumpConstraint(Constraint * c, IncrementalSolver *solver);
 uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}


@@ -38,7 +38,7 @@ VectorConstraint * simplify(Constraint * c);
 CType getType(Constraint * c) {return c->type;}
 bool isFalse(Constraint * c) {return c->type==FALSE;}
 bool isTrue(Constraint * c) {return c->type==TRUE;}
 CType getType(Constraint * c) {return c->type;}
 bool isFalse(Constraint * c) {return c->type==FALSE;}
 bool isTrue(Constraint * c) {return c->type==TRUE;}

-void freeConstraint(Constraint * c);
+void internalfreeConstraint(Constraint * c);

 void freerecConstraint(Constraint * c);
 Constraint * cloneConstraint(Constraint * c);
 void setNegConstraint(Constraint * this, Constraint *c) {this->neg=c;}
 void freerecConstraint(Constraint * c);
 Constraint * cloneConstraint(Constraint * c);
 void setNegConstraint(Constraint * this, Constraint *c) {this->neg=c;}

diff --git a/src/hashset.h b/src/hashset.h
index fe186314053fcee29177755659bb3d9466f15517..6d87078786d9b071ef4f80a93247c2d12bca4b05 100644 (file)
--- a/src/hashset.h
+++ b/src/hashset.h
@@ -28,7 +28,7 @@
        typedef struct HSIterator ## Name HSIterator ## Name;                                                                   \
        HashTableDef(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals); \
        HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name *_curr, HashSet ## Name * _set); \
        typedef struct HSIterator ## Name HSIterator ## Name;                                                                   \
        HashTableDef(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals); \
        HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name *_curr, HashSet ## Name * _set); \

-       void freeIter ## Name(HSIterator ## Name *hsit);                                                                                        \
+       void deleteIter ## Name(HSIterator ## Name *hsit);                                                                                      \

        bool hasNext ## Name(HSIterator ## Name *hsit);                                                                                         \
        _Key next ## Name(HSIterator ## Name *hsit);                                                                                                    \
        _Key currKey ## Name(HSIterator ## Name *hsit);                                                                                         \
        bool hasNext ## Name(HSIterator ## Name *hsit);                                                                                         \
        _Key next ## Name(HSIterator ## Name *hsit);                                                                                                    \
        _Key currKey ## Name(HSIterator ## Name *hsit);                                                                                         \


@@ -41,7 +41,7 @@
        typedef struct HashSet ## Name HashSet ## Name;                                                                                         \
                                                                                                                                                                                                                                                                                                \
        HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor);   \
        typedef struct HashSet ## Name HashSet ## Name;                                                                                         \
                                                                                                                                                                                                                                                                                                \
        HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor);   \

-       void freeHashSet ## Name(struct HashSet ## Name * set);                                                         \
+       void deleteHashSet ## Name(struct HashSet ## Name * set);                                                               \

        HashSet ## Name * copy ## Name(HashSet ## Name * set);                                                          \
        void resetSet ## Name(HashSet ## Name * set);                                                                                                   \
        bool add ## Name(HashSet ## Name * set,_Key key);                                                                                       \
        HashSet ## Name * copy ## Name(HashSet ## Name * set);                                                          \
        void resetSet ## Name(HashSet ## Name * set);                                                                                                   \
        bool add ## Name(HashSet ## Name * set,_Key key);                                                                                       \


@@ -63,7 +63,7 @@
                return hsit;                                                                                                                                                                                                                            \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \
                return hsit;                                                                                                                                                                                                                            \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \

-       void freeIter ## Name(HSIterator ## Name *hsit) {                                                                                       \
+       void deleteIter ## Name(HSIterator ## Name *hsit) {                                                                             \

                ourfree(hsit);                                                                                                                                                                                                                  \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \
                ourfree(hsit);                                                                                                                                                                                                                  \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \


@@ -95,14 +95,14 @@
                return set;                                                                                                                                                                                                                                     \
 }                                                                                                                                                                                                                                                                                              \
                                                                                                                                                                                                                                                                                                \
                return set;                                                                                                                                                                                                                                     \
 }                                                                                                                                                                                                                                                                                              \
                                                                                                                                                                                                                                                                                                \

-       void freeHashSet ## Name(struct HashSet ## Name * set) {                                                        \
+       void deleteHashSet ## Name(struct HashSet ## Name * set) {                                              \

                LinkNode ## Name *tmp=set->list;                                                                                                                                                \
                while(tmp!=NULL) {                                                                                                                                                                                                      \
                        LinkNode ## Name *tmpnext=tmp->next;                                                                                                                    \
                        ourfree(tmp);                                                                                                                                                                                                                   \
                        tmp=tmpnext;                                                                                                                                                                                                                    \
                }                                                                                                                                                                                                                                                                               \
                LinkNode ## Name *tmp=set->list;                                                                                                                                                \
                while(tmp!=NULL) {                                                                                                                                                                                                      \
                        LinkNode ## Name *tmpnext=tmp->next;                                                                                                                    \
                        ourfree(tmp);                                                                                                                                                                                                                   \
                        tmp=tmpnext;                                                                                                                                                                                                                    \
                }                                                                                                                                                                                                                                                                               \

-               freeHashTable ## Name ## Set(set->table);                                                                                                                                       \
+               deleteHashTable ## Name ## Set(set->table);                                                                                                     \

                ourfree(set);                                                                                                                                                                                                                           \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \
                ourfree(set);                                                                                                                                                                                                                           \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \


@@ -111,7 +111,7 @@
                HSIterator ## Name * it=iterator ## Name(set);                                                                                  \
                while(hasNext ## Name(it))                                                                                                                                                                      \
                        add ## Name(copy, next ## Name(it));                                                                                                                    \
                HSIterator ## Name * it=iterator ## Name(set);                                                                                  \
                while(hasNext ## Name(it))                                                                                                                                                                      \
                        add ## Name(copy, next ## Name(it));                                                                                                                    \

-               freeIter ## Name(it);                                                                                                                                                                                                   \
+               deleteIter ## Name(it);                                                                                                                                                                                 \

                return copy;                                                                                                                                                                                                                            \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \
                return copy;                                                                                                                                                                                                                            \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \

diff --git a/src/hashtable.h b/src/hashtable.h
index 8a9ebb09b3ae2eca1ad7d653be579e88129b7538..e0db66570de685db427882f73497adb075936ce7 100644 (file)
--- a/src/hashtable.h
+++ b/src/hashtable.h
@@ -49,7 +49,7 @@
                                                                                                                                                                                                                                                                                                \
        typedef struct HashTable ## Name HashTable ## Name;                                                                             \
        HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor); \
                                                                                                                                                                                                                                                                                                \
        typedef struct HashTable ## Name HashTable ## Name;                                                                             \
        HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor); \

-       void freeHashTable ## Name(HashTable ## Name * tab);                                                                    \
+       void deleteHashTable ## Name(HashTable ## Name * tab);                                                                  \

        void reset ## Name(HashTable ## Name * tab);                                                                                                    \
        void resetandfree ## Name(HashTable ## Name * tab);                                                                             \
        void put ## Name(HashTable ## Name * tab, _Key key, _Val val);                          \
        void reset ## Name(HashTable ## Name * tab);                                                                                                    \
        void resetandfree ## Name(HashTable ## Name * tab);                                                                             \
        void put ## Name(HashTable ## Name * tab, _Key key, _Val val);                          \


@@ -75,7 +75,7 @@
                return tab;                                                                                                                                                                                                                                     \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \
                return tab;                                                                                                                                                                                                                                     \
        }                                                                                                                                                                                                                                                                                       \
                                                                                                                                                                                                                                                                                                \

-       void freeHashTable ## Name(HashTable ## Name * tab) {                                                                   \
+       void deleteHashTable ## Name(HashTable ## Name * tab) {                                                                 \

                ourfree(tab->table);                                                                                                                                                                                            \
                if (tab->zero)                                                                                                                                                                                                                  \
                        ourfree(tab->zero);                                                                                                                                                                                             \
                ourfree(tab->table);                                                                                                                                                                                            \
                if (tab->zero)                                                                                                                                                                                                                  \
                        ourfree(tab->zero);                                                                                                                                                                                             \

diff --git a/src/inc_solver.c b/src/inc_solver.c
index 97f050c63fb2f05d8cac5b8b02f2913a5acd1809..c25cfba9c870fa883e475112a48ba4edb3f396e2 100644 (file)
--- a/src/inc_solver.c
+++ b/src/inc_solver.c
@@ -10,84 +10,86 @@
 #include "inc_solver.h"
 #define SATSOLVER "sat_solver"
 #include <fcntl.h>
 #include "inc_solver.h"
 #define SATSOLVER "sat_solver"
 #include <fcntl.h>

-
-IncrementalSolver::IncrementalSolver() :
-       buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
-       solution(NULL),
-       solutionsize(0),
-       offset(0)
-{
-       createSolver();
+#include "common.h"
+
+IncrementalSolver * allocIncrementalSolver() {
+       IncrementalSolver *this=(IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
+       this->buffer=((int *)ourmalloc(sizeof(int)*IS_BUFFERSIZE));
+       this->solution=NULL;
+       this->solutionsize=0;
+       this->offset=0;
+       createSolver(this);
+       return this;

 }
 
 }
 

-IncrementalSolver::~IncrementalSolver() {
-       killSolver();
-       model_free(buffer);
-       if (solution != NULL)
-               model_free(solution);
+void deleteIncrementalSolver(IncrementalSolver * this) {
+       killSolver(this);
+       ourfree(this->buffer);
+       if (this->solution != NULL)
+               ourfree(this->solution);

 }
 
 }
 

-void IncrementalSolver::reset() {
-       killSolver();
-       offset = 0;
-       createSolver();
+void resetSolver(IncrementalSolver * this) {
+       killSolver(this);
+       this->offset = 0;
+       createSolver(this);

 }
 
 }
 

-void IncrementalSolver::addClauseLiteral(int literal) {
-       buffer[offset++]=literal;
-       if (offset==IS_BUFFERSIZE) {
-               flushBuffer();
+void addClauseLiteral(IncrementalSolver * this, int literal) {
+       this->buffer[this->offset++]=literal;
+       if (this->offset==IS_BUFFERSIZE) {
+               flushBufferSolver(this);

        }
 }
 
        }
 }
 

-void IncrementalSolver::finishedClauses() {
-       addClauseLiteral(0);
+void finishedClauses(IncrementalSolver * this) {
+       addClauseLiteral(this, 0);

 }
 
 }
 

-void IncrementalSolver::freeze(int variable) {
-       addClauseLiteral(IS_FREEZE);
-       addClauseLiteral(variable);
+void freeze(IncrementalSolver * this, int variable) {
+       addClauseLiteral(this, IS_FREEZE);
+       addClauseLiteral(this, variable);

 }
 
 }
 

-int IncrementalSolver::solve() {
+int solve(IncrementalSolver * this) {

        //add an empty clause
        //add an empty clause

-       startSolve();
-       return getSolution();
+       startSolve(this);
+       return getSolution(this);

 }
 
 
 }
 
 

-void IncrementalSolver::startSolve() {
-       addClauseLiteral(IS_RUNSOLVER);
-       flushBuffer();
+void startSolve(IncrementalSolver *this) {
+       addClauseLiteral(this, IS_RUNSOLVER);
+       flushBufferSolver(this);

 }
 
 }
 

-int IncrementalSolver::getSolution() {
-       int result=readIntSolver();
+int getSolution(IncrementalSolver * this) {
+       int result=readIntSolver(this);

        if (result == IS_SAT) {
        if (result == IS_SAT) {

-               int numVars=readIntSolver();
-               if (numVars > solutionsize) {
-                       if (solution != NULL)
-                               model_free(solution);
-                       solution = (int *) model_malloc((numVars+1)*sizeof(int));
-                       solution[0] = 0;
+               int numVars=readIntSolver(this);
+               if (numVars > this->solutionsize) {
+                       if (this->solution != NULL)
+                               ourfree(this->solution);
+                       this->solution = (int *) ourmalloc((numVars+1)*sizeof(int));
+                       this->solution[0] = 0;

                }
                }

-               readSolver(&solution[1], numVars * sizeof(int));
+               readSolver(this, &this->solution[1], numVars * sizeof(int));

        }
        return result;
 }
 
        }
        return result;
 }
 

-int IncrementalSolver::readIntSolver() {
+int readIntSolver(IncrementalSolver * this) {

        int value;
        int value;

-       readSolver(&value, 4);
+       readSolver(this, &value, 4);

        return value;
 }
 
        return value;
 }
 

-void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
+void readSolver(IncrementalSolver * this, void * tmp, ssize_t size) {

        char *result = (char *) tmp;
        ssize_t bytestoread=size;
        ssize_t bytesread=0;
        do {
        char *result = (char *) tmp;
        ssize_t bytestoread=size;
        ssize_t bytesread=0;
        do {

-               ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
+               ssize_t n=read(this->from_solver_fd, &((char *)result)[bytesread], bytestoread);

                if (n == -1) {
                        model_print("Read failure\n");
                        exit(-1);
                if (n == -1) {
                        model_print("Read failure\n");
                        exit(-1);


@@ -97,22 +99,22 @@ void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
        } while(bytestoread != 0);
 }
 
        } while(bytestoread != 0);
 }
 

-bool IncrementalSolver::getValue(int variable) {
-       return solution[variable];
+bool getValueSolver(IncrementalSolver * this, int variable) {
+       return this->solution[variable];

 }
 
 }
 

-void IncrementalSolver::createSolver() {
+void createSolver(IncrementalSolver * this) {

        int to_pipe[2];
        int from_pipe[2];
        if (pipe(to_pipe) || pipe(from_pipe)) {
                model_print("Error creating pipe.\n");
                exit(-1);
        }
        int to_pipe[2];
        int from_pipe[2];
        if (pipe(to_pipe) || pipe(from_pipe)) {
                model_print("Error creating pipe.\n");
                exit(-1);
        }

-       if ((solver_pid = fork()) == -1) {
+       if ((this->solver_pid = fork()) == -1) {

                model_print("Error forking.\n");
                exit(-1);
        }
                model_print("Error forking.\n");
                exit(-1);
        }

-       if (solver_pid == 0) {
+       if (this->solver_pid == 0) {

                //Solver process
                close(to_pipe[1]);
                close(from_pipe[0]);
                //Solver process
                close(to_pipe[1]);
                close(from_pipe[0]);


@@ -129,36 +131,36 @@ void IncrementalSolver::createSolver() {
                close(fd);
        } else {
                //Our process
                close(fd);
        } else {
                //Our process

-               to_solver_fd = to_pipe[1];
-               from_solver_fd = from_pipe[0];
+               this->to_solver_fd = to_pipe[1];
+               this->from_solver_fd = from_pipe[0];

                close(to_pipe[0]);
                close(from_pipe[1]);
        }
 }
 
                close(to_pipe[0]);
                close(from_pipe[1]);
        }
 }
 

-void IncrementalSolver::killSolver() {
-       close(to_solver_fd);
-       close(from_solver_fd);
+void killSolver(IncrementalSolver * this) {
+       close(this->to_solver_fd);
+       close(this->from_solver_fd);

        //Stop the solver
        //Stop the solver

-       if (solver_pid > 0) {
+       if (this->solver_pid > 0) {

                int status;
                int status;

-               kill(solver_pid, SIGKILL);
-               waitpid(solver_pid, &status, 0);
+               kill(this->solver_pid, SIGKILL);
+               waitpid(this->solver_pid, &status, 0);

        }
 }
 
        }
 }
 

-void IncrementalSolver::flushBuffer() {
-       ssize_t bytestowrite=sizeof(int)*offset;
+void flushBufferSolver(IncrementalSolver * this) {
+       ssize_t bytestowrite=sizeof(int)*this->offset;

        ssize_t byteswritten=0;
        do {
        ssize_t byteswritten=0;
        do {

-               ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
+               ssize_t n=write(this->to_solver_fd, &((char *)this->buffer)[byteswritten], bytestowrite);

                if (n == -1) {
                        perror("Write failure\n");
                if (n == -1) {
                        perror("Write failure\n");

-                       model_print("to_solver_fd=%d\n",to_solver_fd);
+                       model_print("to_solver_fd=%d\n",this->to_solver_fd);

                        exit(-1);
                }
                bytestowrite -= n;
                byteswritten += n;
        } while(bytestowrite != 0);
                        exit(-1);
                }
                bytestowrite -= n;
                byteswritten += n;
        } while(bytestowrite != 0);

-       offset = 0;
+       this->offset = 0;

 }
 }

diff --git a/src/inc_solver.h b/src/inc_solver.h
index 415dc8d720f1eb6a26d41c16a2aeb69866dda784..ead727fba25395146b7ae64fa57e3d0d8d91bc9c 100644 (file)
--- a/src/inc_solver.h
+++ b/src/inc_solver.h
@@ -18,27 +18,7 @@
 #include "solver_interface.h"
 #include "classlist.h"
 
 #include "solver_interface.h"
 #include "classlist.h"
 

-class IncrementalSolver {
-public:
-       IncrementalSolver();
-       ~IncrementalSolver();
-       void addClauseLiteral(int literal);
-       void finishedClauses();
-       void freeze(int variable);
-       int solve();
-       void startSolve();
-       int getSolution();
-
-       bool getValue(int variable);
-       void reset();
-       MEMALLOC;
-
-private:
-       void createSolver();
-       void killSolver();
-       void flushBuffer();
-       int readIntSolver();
-       void readSolver(void * buffer, ssize_t size);
+struct IncrementalSolver {

        int * buffer;
        int * solution;
        int solutionsize;
        int * buffer;
        int * solution;
        int solutionsize;


@@ -47,4 +27,20 @@ private:
        int to_solver_fd;
        int from_solver_fd;
 };
        int to_solver_fd;
        int from_solver_fd;
 };

+
+IncrementalSolver * allocIncrementalSolver();
+void deleteIncrementalSolver(IncrementalSolver * this);
+void addClauseLiteral(IncrementalSolver * this, int literal);
+void finishedClauses(IncrementalSolver * this);
+void freeze(IncrementalSolver * this, int variable);
+int solve(IncrementalSolver * this);
+void startSolve(IncrementalSolver * this);
+int getSolution(IncrementalSolver * this);
+bool getValueSolver(IncrementalSolver * this, int variable);
+void resetSolver(IncrementalSolver * this);
+void createSolver(IncrementalSolver * this);
+void killSolver(IncrementalSolver * this);
+void flushBufferSolver(IncrementalSolver * this);
+int readIntSolver(IncrementalSolver * this);
+void readSolver(IncrementalSolver * this, void * buffer, ssize_t size);

 #endif
 #endif

diff --git a/src/mymemory.h b/src/mymemory.h
index 5267ce2327e2fd4fc2243f4bf274344b40bc8c36..2fa964e6f8031779d21f958f2ae2a2b71d3c3f79 100644 (file)
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -19,35 +19,9 @@
 
 #include "config.h"
 
 
 #include "config.h"
 

-/** MEMALLOC declares the allocators for a class to allocate
- *     memory in the non-snapshotting heap. */
-/*
-#define MEMALLOC                                                                                \
-       void * operator new(size_t size) { \
-               return model_malloc(size); \
-       } \
-       void operator delete(void *p, size_t size) { \
-               model_free(p);                                   \
-       } \
-       void * operator new[](size_t size) { \
-               return model_malloc(size); \
-       } \
-       void operator delete[](void *p, size_t size) { \
-               model_free(p); \
-       } \
-       void * operator new(size_t size, void *p) {     \
-               return p;                                                                                                                                                               \
-       }
-*/
-

 void * ourmalloc(size_t size);
 void ourfree(void *ptr);
 void * ourcalloc(size_t count, size_t size);
 void * ourrealloc(void *ptr, size_t size);
 
 void * ourmalloc(size_t size);
 void ourfree(void *ptr);
 void * ourcalloc(size_t count, size_t size);
 void * ourrealloc(void *ptr, size_t size);
 

-void *model_malloc(size_t size);
-void *model_calloc(size_t count, size_t size);
-void * model_realloc(void *ptr, size_t size);
-void model_free(void *ptr);
-

 #endif/* _MY_MEMORY_H */
 #endif/* _MY_MEMORY_H */

diff --git a/src/set.c b/src/set.c
index ece4e8653fcd4acd7c958a9e8215355a883bf89b..1bab08e527f97e76c73a5fdc79c5703e4da9ea39 100644 (file)
--- a/src/set.c
+++ b/src/set.c
@@ -21,8 +21,8 @@ Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) {
        return tmp;
 }
 
        return tmp;
 }
 

-void freeSet(Set * set) {
+void deleteSet(Set * set) {

        if (set->isRange)
        if (set->isRange)

-               freeVectorInt(set->members);
+               deleteVectorInt(set->members);

        ourfree(set);
 }
        ourfree(set);
 }

diff --git a/src/set.h b/src/set.h
index dee406676f296c52c5ab0751a07d218550cefbe3..5000674059a598542930c44a10a9da6f4701f73b 100644 (file)
--- a/src/set.h
+++ b/src/set.h
@@ -22,6 +22,6 @@ struct Set {
 
 Set *allocSet(VarType t, uint64_t * elements, uint num);
 Set    * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange);
 
 Set *allocSet(VarType t, uint64_t * elements, uint num);
 Set    * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange);

-void freeSet(Set *set);
+void deleteSet(Set *set);

 #endif/* SET_H */
 
 #endif/* SET_H */
 

diff --git a/src/vector.h b/src/vector.h
index a867db62a32086916adc5901ba4a80a19b308d55..d131a275d46eae38d9f26664b32d7511d11a09d3 100644 (file)
--- a/src/vector.h
+++ b/src/vector.h
@@ -16,7 +16,7 @@
        type getVector ## name(Vector ## name *vector, uint index);                                             \
        void setVector ## name(Vector ## name *vector, uint index, type item); \
        uint getSizeVector ##name(Vector ##name *vector);                                                                                       \
        type getVector ## name(Vector ## name *vector, uint index);                                             \
        void setVector ## name(Vector ## name *vector, uint index, type item); \
        uint getSizeVector ##name(Vector ##name *vector);                                                                                       \

-       void freeVector ##name(Vector ##name *vector);                                                                                          \
+       void deleteVector ##name(Vector ##name *vector);                                                                                                \

        void clearVector ##name(Vector ## name *vector);
 
 #define VectorImpl(name, type, defcap)                                                                                                                                 \
        void clearVector ##name(Vector ## name *vector);
 
 #define VectorImpl(name, type, defcap)                                                                                                                                 \


@@ -51,7 +51,7 @@
        uint getSizeVector ## name(Vector ## name *vector) {                                                                    \
                return vector->size;                                                                                                                                                                                            \
        }                                                                                                                                                                                                                                                                                       \
        uint getSizeVector ## name(Vector ## name *vector) {                                                                    \
                return vector->size;                                                                                                                                                                                            \
        }                                                                                                                                                                                                                                                                                       \

-       void freeVector ##name(Vector ##name *vector) {                                                                                         \
+       void deleteVector ##name(Vector ##name *vector) {                                                                                       \

                ourfree(vector->array);                                                                                                                                                                                 \
                ourfree(vector);                                                                                                                                                                                                                \
        }                                                                                                                                                                                                                                                                                       \
                ourfree(vector->array);                                                                                                                                                                                 \
                ourfree(vector);                                                                                                                                                                                                                \
        }                                                                                                                                                                                                                                                                                       \