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)
#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};
return this;
}
-void freeConstraint(Constraint *this) {
+void deleteConstraint(Constraint *this) {
if (this->operands!=NULL)
ourfree(this->operands);
}
-/*void dumpConstraint(Constraint * this, IncrementalSolver *solver) {
+void dumpConstraint(Constraint * this, IncrementalSolver *solver) {
if (this->type==VAR) {
- solver->addClauseLiteral(this->numoperandsorvar);
- solver->addClauseLiteral(0);
+ addClauseLiteral(solver, this->numoperandsorvar);
+ addClauseLiteral(solver, 0);
} 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) {
- solver->addClauseLiteral(c->numoperandsorvar);
+ addClauseLiteral(solver, c->numoperandsorvar);
} else if (c->type==NOTVAR) {
- solver->addClauseLiteral(-c->numoperandsorvar);
+ addClauseLiteral(solver, -c->numoperandsorvar);
} else ASSERT(0);
}
- solver->addClauseLiteral(0);
+ addClauseLiteral(solver, 0);
}
- }*/
+}
void internalfreeConstraint(Constraint * this) {
switch(this->type) {
freerecConstraint(this->operands[i]);
}
this->type=BOGUS;
- freeConstraint(this);
+ deleteConstraint(this);
}
}
freerecConstraint(getVectorConstraint(to, j));
clearVectorConstraint(to);
pushVectorConstraint(to, &ctrue);
- freeVectorConstraint(from);
+ deleteVectorConstraint(from);
return true;
}
pushVectorConstraint(to, c);
}
- freeVectorConstraint(from);
+ deleteVectorConstraint(from);
return false;
}
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;}
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;}
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); \
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); \
return hsit; \
} \
\
- void freeIter ## Name(HSIterator ## Name *hsit) { \
+ void deleteIter ## Name(HSIterator ## Name *hsit) { \
ourfree(hsit); \
} \
\
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; \
} \
- freeHashTable ## Name ## Set(set->table); \
+ deleteHashTable ## Name ## Set(set->table); \
ourfree(set); \
} \
\
HSIterator ## Name * it=iterator ## Name(set); \
while(hasNext ## Name(it)) \
add ## Name(copy, next ## Name(it)); \
- freeIter ## Name(it); \
+ deleteIter ## Name(it); \
return copy; \
} \
\
\
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); \
return tab; \
} \
\
- void freeHashTable ## Name(HashTable ## Name * tab) { \
+ void deleteHashTable ## Name(HashTable ## Name * tab) { \
ourfree(tab->table); \
if (tab->zero) \
ourfree(tab->zero); \
#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
- 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) {
- 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;
}
-int IncrementalSolver::readIntSolver() {
+int readIntSolver(IncrementalSolver * this) {
int value;
- readSolver(&value, 4);
+ readSolver(this, &value, 4);
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 {
- 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);
} 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);
}
- if ((solver_pid = fork()) == -1) {
+ if ((this->solver_pid = fork()) == -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]);
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]);
}
}
-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
- if (solver_pid > 0) {
+ if (this->solver_pid > 0) {
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 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");
- 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);
- offset = 0;
+ this->offset = 0;
}
#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 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
#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 *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 */
return tmp;
}
-void freeSet(Set * set) {
+void deleteSet(Set * set) {
if (set->isRange)
- freeVectorInt(set->members);
+ deleteVectorInt(set->members);
ourfree(set);
}
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 */
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) \
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); \
} \
projects / satune.git / commitdiff