From: bdemsky Date: Fri, 16 Jun 2017 00:22:39 +0000 (-0700) Subject: Reorg code X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=2fdb3e8b65ae7e1490997e5df9ad8cc0929e1589;p=satune.git Reorg code --- diff --git a/src/AST/boolean.c b/src/AST/boolean.c new file mode 100644 index 0000000..13070fa --- /dev/null +++ b/src/AST/boolean.c @@ -0,0 +1 @@ +#include "boolean.h" diff --git a/src/AST/boolean.h b/src/AST/boolean.h new file mode 100644 index 0000000..5e8c5a5 --- /dev/null +++ b/src/AST/boolean.h @@ -0,0 +1,8 @@ +#ifndef BOOLEAN_H +#define BOOLEAN_H +#include "classlist.h" +#include "mymemory.h" + +struct Boolean { +}; +#endif diff --git a/src/AST/element.c b/src/AST/element.c new file mode 100644 index 0000000..191686c --- /dev/null +++ b/src/AST/element.c @@ -0,0 +1,11 @@ +#include "element.h" + +Element *allocElement(Set * s) { + Element * tmp=(Element *)ourmalloc(sizeof(Element)); + tmp->set=s; + return tmp; +} + +void deleteElement(Element *this) { + ourfree(this); +} diff --git a/src/AST/element.h b/src/AST/element.h new file mode 100644 index 0000000..8f0f082 --- /dev/null +++ b/src/AST/element.h @@ -0,0 +1,12 @@ +#ifndef ELEMENT_H +#define ELEMENT_H +#include "classlist.h" +#include "mymemory.h" + +struct Element { + Set * set; +}; + +Element * allocElement(Set *s); +void deleteElement(Element *this); +#endif diff --git a/src/AST/function.c b/src/AST/function.c new file mode 100644 index 0000000..d4b693e --- /dev/null +++ b/src/AST/function.c @@ -0,0 +1 @@ +#include "function.h" diff --git a/src/AST/function.h b/src/AST/function.h new file mode 100644 index 0000000..da5087b --- /dev/null +++ b/src/AST/function.h @@ -0,0 +1,8 @@ +#ifndef FUNCTION_H +#define FUNCTION_H +#include "classlist.h" +#include "mymemory.h" + +struct Function { +}; +#endif diff --git a/src/AST/mutableset.c b/src/AST/mutableset.c new file mode 100644 index 0000000..18f038b --- /dev/null +++ b/src/AST/mutableset.c @@ -0,0 +1,15 @@ +#include "mutableset.h" + +MutableSet * allocMutableSet(VarType t) { + MutableSet * tmp=(MutableSet *)ourmalloc(sizeof(MutableSet)); + tmp->type=t; + tmp->isRange=false; + tmp->low=0; + tmp->high=0; + tmp->members=allocDefVectorInt(); + return tmp; +} + +void addElementMSet(MutableSet * set, uint64_t element) { + pushVectorInt(set->members, element); +} diff --git a/src/AST/mutableset.h b/src/AST/mutableset.h new file mode 100644 index 0000000..fe089f4 --- /dev/null +++ b/src/AST/mutableset.h @@ -0,0 +1,7 @@ +#ifndef MUTABLESET_H +#define MUTABLESET_H +#include "set.h" + +MutableSet * allocMutableSet(VarType t); +void addElementMSet(MutableSet * set, uint64_t element); +#endif diff --git a/src/AST/ops.h b/src/AST/ops.h new file mode 100644 index 0000000..40e6f99 --- /dev/null +++ b/src/AST/ops.h @@ -0,0 +1,17 @@ +#ifndef OPS_H +#define OPS_H +enum LogicOp {AND, OR, NOT, XOR, IMPLIES}; +enum ArithOp {ADD, SUB}; +enum CompOp {EQUALS}; +enum OrderType {PARTIAL, TOTAL}; + +/** + * FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true + * OVERFLOWSETSFLAG -- sets the flag if the operation overflows + * FLAGIFFOVERFLOW -- flag is set iff the operation overflows + * IGNORE -- doesn't constrain output if the result cannot be represented + * WRAPAROUND -- wraps around like stand integer arithmetic + */ +enum OverFlowBehavior {IGNORE, WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW}; + +#endif diff --git a/src/AST/order.c b/src/AST/order.c new file mode 100644 index 0000000..727b2dd --- /dev/null +++ b/src/AST/order.c @@ -0,0 +1 @@ +#include "order.h" diff --git a/src/AST/order.h b/src/AST/order.h new file mode 100644 index 0000000..b164a11 --- /dev/null +++ b/src/AST/order.h @@ -0,0 +1,8 @@ +#ifndef ORDER_H +#define ORDER_H +#include "classlist.h" +#include "mymemory.h" + +struct Order { +}; +#endif diff --git a/src/AST/predicate.c b/src/AST/predicate.c new file mode 100644 index 0000000..dcec97a --- /dev/null +++ b/src/AST/predicate.c @@ -0,0 +1 @@ +#include "predicate.h" diff --git a/src/AST/predicate.h b/src/AST/predicate.h new file mode 100644 index 0000000..9a17669 --- /dev/null +++ b/src/AST/predicate.h @@ -0,0 +1,9 @@ +#ifndef PREDICATE_H +#define PREDICATE_H +#include "classlist.h" +#include "mymemory.h" + +struct Predicate { + +}; +#endif diff --git a/src/AST/set.c b/src/AST/set.c new file mode 100644 index 0000000..fc056a2 --- /dev/null +++ b/src/AST/set.c @@ -0,0 +1,28 @@ +#include "set.h" +#include + +Set * allocSet(VarType t, uint64_t* elements, uint num) { + Set * tmp=(Set *)ourmalloc(sizeof(Set)); + tmp->type=t; + tmp->isRange=false; + tmp->low=0; + tmp->high=0; + tmp->members=allocVectorArrayInt(num, elements); + return tmp; +} + +Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) { + Set * tmp=(Set *)ourmalloc(sizeof(Set)); + tmp->type=t; + tmp->isRange=true; + tmp->low=lowrange; + tmp->high=highrange; + tmp->members=NULL; + return tmp; +} + +void deleteSet(Set * set) { + if (!set->isRange) + deleteVectorInt(set->members); + ourfree(set); +} diff --git a/src/AST/set.h b/src/AST/set.h new file mode 100644 index 0000000..92315e2 --- /dev/null +++ b/src/AST/set.h @@ -0,0 +1,28 @@ +/* + * File: set.h + * Author: hamed + * + * Created on June 13, 2017, 3:01 PM + */ + +#ifndef SET_H +#define SET_H + +#include "classlist.h" +#include "structs.h" +#include "mymemory.h" + +struct Set { + VarType type; + bool isRange; + uint64_t low;//also used to count unique items + uint64_t high; + VectorInt * members; +}; + + +Set *allocSet(VarType t, uint64_t * elements, uint num); +Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange); +void deleteSet(Set *set); +#endif/* SET_H */ + diff --git a/src/AST/table.c b/src/AST/table.c new file mode 100644 index 0000000..e89d72a --- /dev/null +++ b/src/AST/table.c @@ -0,0 +1 @@ +#include "table.h" diff --git a/src/AST/table.h b/src/AST/table.h new file mode 100644 index 0000000..2bb9805 --- /dev/null +++ b/src/AST/table.h @@ -0,0 +1,11 @@ +#ifndef TABLE_H +#define TABLE_H +#include "classlist.h" +#include "mymemory.h" + +struct Table { + +}; + +Table * allocTable(); +#endif diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c new file mode 100644 index 0000000..8b38540 --- /dev/null +++ b/src/Backend/constraint.c @@ -0,0 +1,420 @@ +/* Copyright (c) 2015 Regents of the University of California + * + * Author: Brian Demsky + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * version 2 as published by the Free Software Foundation. + */ + +#include "constraint.h" +#include "mymemory.h" +#include "inc_solver.h" + +Constraint ctrue={TRUE, 0xffffffff, NULL, NULL}; +Constraint cfalse={FALSE, 0xffffffff, NULL, NULL}; + +Constraint * allocConstraint(CType t, Constraint *l, Constraint *r) { + Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint)); + this->type=t; + this->numoperandsorvar=2; + this->operands=(Constraint **)ourmalloc(2*sizeof(Constraint *)); + this->neg=NULL; + ASSERT(l!=NULL); + //if (type==IMPLIES) { + //type=OR; + // operands[0]=l->negate(); + // } else { + this->operands[0]=l; + // } + this->operands[1]=r; + return this; +} + +Constraint * allocUnaryConstraint(CType t, Constraint *l) { + Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint)); + this->type=t; + this->numoperandsorvar=1; + this->operands=(Constraint **) ourmalloc(sizeof(Constraint *)); + this->neg=NULL; + this->operands[0]=l; + return this; +} + +Constraint * allocArrayConstraint(CType t, uint num, Constraint **array) { + Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint)); + this->type=t; + this->numoperandsorvar=num; + this->operands=(Constraint **) ourmalloc(num*sizeof(Constraint *)); + this->neg=NULL; + memcpy(this->operands, array, num*sizeof(Constraint *)); + return this; +} + +Constraint * allocVarConstraint(CType t, uint v) { + Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint)); + this->type=t; + this->numoperandsorvar=v; + this->operands=NULL; + this->neg=NULL; + return this; +} + +void deleteConstraint(Constraint *this) { + if (this->operands!=NULL) + ourfree(this->operands); +} + +void dumpConstraint(Constraint * this, IncrementalSolver *solver) { + if (this->type==VAR) { + addClauseLiteral(solver, this->numoperandsorvar); + addClauseLiteral(solver, 0); + } else if (this->type==NOTVAR) { + addClauseLiteral(solver, -this->numoperandsorvar); + addClauseLiteral(solver, 0); + } else { + ASSERT(this->type==OR); + for(uint i=0;inumoperandsorvar;i++) { + Constraint *c=this->operands[i]; + if (c->type==VAR) { + addClauseLiteral(solver, c->numoperandsorvar); + } else if (c->type==NOTVAR) { + addClauseLiteral(solver, -c->numoperandsorvar); + } else ASSERT(0); + } + addClauseLiteral(solver, 0); + } +} + +void internalfreeConstraint(Constraint * this) { + switch(this->type) { + case TRUE: + case FALSE: + case NOTVAR: + case VAR: + return; + case BOGUS: + ASSERT(0); + default: + this->type=BOGUS; + ourfree(this); + } +} + +void freerecConstraint(Constraint *this) { + switch(this->type) { + case TRUE: + case FALSE: + case NOTVAR: + case VAR: + return; + case BOGUS: + ASSERT(0); + default: + if (this->operands!=NULL) { + for(uint i=0;inumoperandsorvar;i++) + freerecConstraint(this->operands[i]); + } + this->type=BOGUS; + deleteConstraint(this); + } +} + + +void printConstraint(Constraint * this) { + switch(this->type) { + case TRUE: + model_print("true"); + break; + case FALSE: + model_print("false"); + break; + case IMPLIES: + model_print("("); + printConstraint(this->operands[0]); + model_print(")"); + model_print("=>"); + model_print("("); + printConstraint(this->operands[1]); + model_print(")"); + break; + case AND: + case OR: + model_print("("); + for(uint i=0;inumoperandsorvar;i++) { + if (i!=0) { + if (this->type==AND) + model_print(" ^ "); + else + model_print(" v "); + } + printConstraint(this->operands[i]); + } + model_print(")"); + break; + case VAR: + model_print("t%u",this->numoperandsorvar); + break; + case NOTVAR: + model_print("!t%u",this->numoperandsorvar); + break; + default: + ASSERT(0); + } +} + +Constraint * cloneConstraint(Constraint * this) { + switch(this->type) { + case TRUE: + case FALSE: + case VAR: + case NOTVAR: + return this; + case IMPLIES: + return allocConstraint(IMPLIES, cloneConstraint(this->operands[0]), cloneConstraint(this->operands[1])); + case AND: + case OR: { + Constraint *array[this->numoperandsorvar]; + for(uint i=0;inumoperandsorvar;i++) { + array[i]=cloneConstraint(this->operands[i]); + } + return allocArrayConstraint(this->type, this->numoperandsorvar, array); + } + default: + ASSERT(0); + return NULL; + } +} + +Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value) { + Constraint *carray[numvars]; + for(uint j=0;j>1; + } + + return allocArrayConstraint(AND, numvars, carray); +} + +/** Generates a constraint to ensure that all encodings are less than value */ +Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) { + Constraint *orarray[numvars]; + Constraint *andarray[numvars]; + uint andi=0; + + while(true) { + uint val=value; + uint ori=0; + for(uint j=0;j>1; + } + //no ones to flip, so bail now... + if (ori==0) { + return allocArrayConstraint(AND, andi, andarray); + } + andarray[andi++]=allocArrayConstraint(OR, ori, orarray); + + value=value+(1<<(__builtin_ctz(value))); + //flip the last one + } +} + +Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) { + if (numvars==0) + return &ctrue; + Constraint *array[numvars*2]; + for(uint i=0;itype==TRUE) + continue; + if (c->type==FALSE) { + for(uint j=i+1;jtype) { + case TRUE: + case VAR: + case NOTVAR: + case FALSE: { + VectorConstraint * vec=allocDefVectorConstraint(); + pushVectorConstraint(vec, this); + return vec; + } + case AND: { + VectorConstraint *vec=allocDefVectorConstraint(); + for(uint i=0;inumoperandsorvar;i++) { + VectorConstraint * subvec=simplifyConstraint(this->operands[i]); + if (mergeandfree(vec, subvec)) { + for(uint j=i+1;jnumoperandsorvar;j++) { + freerecConstraint(this->operands[j]); + } + internalfreeConstraint(this); + return vec; + } + } + internalfreeConstraint(this); + return vec; + } + case OR: { + for(uint i=0;inumoperandsorvar;i++) { + Constraint *c=this->operands[i]; + switch(c->type) { + case TRUE: { + VectorConstraint * vec=allocDefVectorConstraint(); + pushVectorConstraint(vec, c); + freerecConstraint(this); + return vec; + } + case FALSE: { + Constraint *array[this->numoperandsorvar-1]; + uint index=0; + for(uint j=0;jnumoperandsorvar;j++) { + if (j!=i) + array[index++]=this->operands[j]; + } + Constraint *cn=allocArrayConstraint(OR, index, array); + VectorConstraint *vec=simplifyConstraint(cn); + internalfreeConstraint(this); + return vec; + } + case VAR: + case NOTVAR: + break; + case OR: { + uint nsize=this->numoperandsorvar+c->numoperandsorvar-1; + Constraint *array[nsize]; + uint index=0; + for(uint j=0;jnumoperandsorvar;j++) + if (j!=i) + array[index++]=this->operands[j]; + for(uint j=0;jnumoperandsorvar;j++) + array[index++]=c->operands[j]; + Constraint *cn=allocArrayConstraint(OR, nsize, array); + VectorConstraint *vec=simplifyConstraint(cn); + internalfreeConstraint(this); + internalfreeConstraint(c); + return vec; + } + case IMPLIES: { + uint nsize=this->numoperandsorvar+1; + Constraint *array[nsize]; + uint index=0; + for(uint j=0;jnumoperandsorvar;j++) + if (j!=i) + array[index++]=this->operands[j]; + array[index++]=negateConstraint(c->operands[0]); + array[index++]=c->operands[1]; + Constraint *cn=allocArrayConstraint(OR, nsize, array); + VectorConstraint *vec=simplifyConstraint(cn); + internalfreeConstraint(this); + internalfreeConstraint(c); + return vec; + } + case AND: { + Constraint *array[this->numoperandsorvar]; + + VectorConstraint *vec=allocDefVectorConstraint(); + for(uint j=0;jnumoperandsorvar;j++) { + //copy other elements + for(uint k=0;knumoperandsorvar;k++) { + if (k!=i) { + array[k]=cloneConstraint(this->operands[k]); + } + } + + array[i]=cloneConstraint(c->operands[j]); + Constraint *cn=allocArrayConstraint(OR, this->numoperandsorvar, array); + VectorConstraint * newvec=simplifyConstraint(cn); + if (mergeandfree(vec, newvec)) { + freerecConstraint(this); + return vec; + } + } + freerecConstraint(this); + return vec; + } + default: + ASSERT(0); + } + //continue on to next item + } + VectorConstraint * vec=allocDefVectorConstraint(); + if (this->numoperandsorvar==1) { + Constraint *c=this->operands[0]; + freerecConstraint(this); + pushVectorConstraint(vec, c); + } else + pushVectorConstraint(vec, this); + return vec; + } + case IMPLIES: { + Constraint *cn=allocConstraint(OR, negateConstraint(this->operands[0]), this->operands[1]); + VectorConstraint * vec=simplifyConstraint(cn); + internalfreeConstraint(this); + return vec; + } + default: + ASSERT(0); + return NULL; + } +} + +Constraint * negateConstraint(Constraint * this) { + switch(this->type) { + case TRUE: + return &cfalse; + case FALSE: + return &ctrue; + case NOTVAR: + case VAR: + return this->neg; + case IMPLIES: { + Constraint *l=this->operands[0]; + Constraint *r=this->operands[1]; + this->operands[0]=r; + this->operands[1]=l; + return this; + } + case AND: + case OR: { + for(uint i=0;inumoperandsorvar;i++) { + this->operands[i]=negateConstraint(this->operands[i]); + } + this->type=(this->type==AND) ? OR : AND; + return this; + } + default: + ASSERT(0); + return NULL; + } +} diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h new file mode 100644 index 0000000..06bb1d1 --- /dev/null +++ b/src/Backend/constraint.h @@ -0,0 +1,54 @@ +/* Copyright (c) 2015 Regents of the University of California + * + * Author: Brian Demsky + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * version 2 as published by the Free Software Foundation. + */ + +#ifndef CONSTRAINT_H +#define CONSTRAINT_H +#include "classlist.h" +#include "structs.h" + +enum ConstraintType { + TRUE, FALSE, IMPLIES, AND, OR, VAR, NOTVAR, BOGUS +}; + +typedef enum ConstraintType CType; + +struct Constraint { + CType type; + uint numoperandsorvar; + Constraint ** operands; + Constraint *neg; +}; + +Constraint * allocConstraint(CType t, Constraint *l, Constraint *r); +Constraint * allocUnaryConstraint(CType t, Constraint *l); +Constraint * allocArrayConstraint(CType t, uint num, Constraint ** array); +Constraint * allocVarConstraint(CType t, uint var); + +void deleteConstraint(Constraint *); +void printConstraint(Constraint * c); +void dumpConstraint(Constraint * c, IncrementalSolver *solver); +uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;} +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;} +void internalfreeConstraint(Constraint * c); +void freerecConstraint(Constraint * c); +Constraint * cloneConstraint(Constraint * c); +void setNegConstraint(Constraint * this, Constraint *c) {this->neg=c;} +Constraint *negateConstraint(Constraint * c); + +extern Constraint ctrue; +extern Constraint cfalse; + +Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value); +Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value); +Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2); +Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2); +#endif diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c new file mode 100644 index 0000000..c25cfba --- /dev/null +++ b/src/Backend/inc_solver.c @@ -0,0 +1,166 @@ +/* Copyright (c) 2015 Regents of the University of California + * + * Author: Brian Demsky + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * version 2 as published by the Free Software Foundation. + */ + +#include "inc_solver.h" +#define SATSOLVER "sat_solver" +#include +#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; +} + +void deleteIncrementalSolver(IncrementalSolver * this) { + killSolver(this); + ourfree(this->buffer); + if (this->solution != NULL) + ourfree(this->solution); +} + +void resetSolver(IncrementalSolver * this) { + killSolver(this); + this->offset = 0; + createSolver(this); +} + +void addClauseLiteral(IncrementalSolver * this, int literal) { + this->buffer[this->offset++]=literal; + if (this->offset==IS_BUFFERSIZE) { + flushBufferSolver(this); + } +} + +void finishedClauses(IncrementalSolver * this) { + addClauseLiteral(this, 0); +} + +void freeze(IncrementalSolver * this, int variable) { + addClauseLiteral(this, IS_FREEZE); + addClauseLiteral(this, variable); +} + +int solve(IncrementalSolver * this) { + //add an empty clause + startSolve(this); + return getSolution(this); +} + + +void startSolve(IncrementalSolver *this) { + addClauseLiteral(this, IS_RUNSOLVER); + flushBufferSolver(this); +} + +int getSolution(IncrementalSolver * this) { + int result=readIntSolver(this); + if (result == IS_SAT) { + 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(this, &this->solution[1], numVars * sizeof(int)); + } + return result; +} + +int readIntSolver(IncrementalSolver * this) { + int value; + readSolver(this, &value, 4); + return value; +} + +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(this->from_solver_fd, &((char *)result)[bytesread], bytestoread); + if (n == -1) { + model_print("Read failure\n"); + exit(-1); + } + bytestoread -= n; + bytesread += n; + } while(bytestoread != 0); +} + +bool getValueSolver(IncrementalSolver * this, int variable) { + return this->solution[variable]; +} + +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 ((this->solver_pid = fork()) == -1) { + model_print("Error forking.\n"); + exit(-1); + } + if (this->solver_pid == 0) { + //Solver process + close(to_pipe[1]); + close(from_pipe[0]); + int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU); + + if ((dup2(to_pipe[0], 0) == -1) || + (dup2(from_pipe[1], IS_OUT_FD) == -1) || + (dup2(fd, 1) == -1)) { + model_print("Error duplicating pipes\n"); + } + // setsid(); + execlp(SATSOLVER, SATSOLVER, NULL); + model_print("execlp Failed\n"); + close(fd); + } else { + //Our process + this->to_solver_fd = to_pipe[1]; + this->from_solver_fd = from_pipe[0]; + close(to_pipe[0]); + close(from_pipe[1]); + } +} + +void killSolver(IncrementalSolver * this) { + close(this->to_solver_fd); + close(this->from_solver_fd); + //Stop the solver + if (this->solver_pid > 0) { + int status; + kill(this->solver_pid, SIGKILL); + waitpid(this->solver_pid, &status, 0); + } +} + +void flushBufferSolver(IncrementalSolver * this) { + ssize_t bytestowrite=sizeof(int)*this->offset; + ssize_t byteswritten=0; + do { + 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",this->to_solver_fd); + exit(-1); + } + bytestowrite -= n; + byteswritten += n; + } while(bytestowrite != 0); + this->offset = 0; +} diff --git a/src/Backend/inc_solver.h b/src/Backend/inc_solver.h new file mode 100644 index 0000000..ead727f --- /dev/null +++ b/src/Backend/inc_solver.h @@ -0,0 +1,46 @@ +/* Copyright (c) 2015 Regents of the University of California + * + * Author: Brian Demsky + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * version 2 as published by the Free Software Foundation. + */ + +#ifndef INC_SOLVER_H +#define INC_SOLVER_H +#include +#include +#include +#include +#include +#include +#include "solver_interface.h" +#include "classlist.h" + +struct IncrementalSolver { + int * buffer; + int * solution; + int solutionsize; + int offset; + pid_t solver_pid; + 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 diff --git a/src/Backend/solver_interface.h b/src/Backend/solver_interface.h new file mode 100644 index 0000000..4fd2dea --- /dev/null +++ b/src/Backend/solver_interface.h @@ -0,0 +1,23 @@ +/* Copyright (c) 2015 Regents of the University of California + * + * Author: Brian Demsky + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * version 2 as published by the Free Software Foundation. + */ + +#ifndef SOLVER_INTERFACE_H +#define SOLVER_INTERFACE_H + +#define IS_OUT_FD 3 + +#define IS_UNSAT 0 +#define IS_SAT 1 +#define IS_INDETER 2 +#define IS_FREEZE 3 +#define IS_RUNSOLVER 4 + +#define IS_BUFFERSIZE 1024 + +#endif diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h new file mode 100644 index 0000000..6d87078 --- /dev/null +++ b/src/Collections/hashset.h @@ -0,0 +1,194 @@ +/* Copyright (c) 2015 Regents of the University of California + * + * Author: Brian Demsky + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * version 2 as published by the Free Software Foundation. + */ + +#ifndef HASH_SET_H +#define HASH_SET_H +#include "hashtable.h" + +#define HashSetDef(Name, _Key, hash_function, equals) \ + struct LinkNode ## Name { \ + _Key key; \ + struct LinkNode ## Name *prev; \ + struct LinkNode ## Name *next; \ + }; \ + typedef struct LinkNode ## Name LinkNode ## Name; \ + struct HashSet ## Name; \ + typedef struct HashSet ## Name HashSet ## Name; \ + struct HSIterator ## Name { \ + LinkNode ## Name *curr; \ + LinkNode ## Name *last; \ + 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 deleteIter ## Name(HSIterator ## Name *hsit); \ + bool hasNext ## Name(HSIterator ## Name *hsit); \ + _Key next ## Name(HSIterator ## Name *hsit); \ + _Key currKey ## Name(HSIterator ## Name *hsit); \ + void removeIter ## Name(HSIterator ## Name *hsit); \ + struct HashSet ## Name { \ + HashTable ## Name ## Set * table; \ + LinkNode ## Name *list; \ + LinkNode ## Name *tail; \ + }; \ + typedef struct HashSet ## Name HashSet ## Name; \ + \ + HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor); \ + 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); \ + _Key getSet ## Name(HashSet ## Name * set,_Key key); \ + _Key getFirstKey ## Name(HashSet ## Name * set); \ + bool containsSet ## Name(HashSet ## Name * set,_Key key); \ + bool removeSet ## Name(HashSet ## Name * set,_Key key); \ + unsigned int getSizeSet ## Name(HashSet ## Name * set); \ + bool isEmpty ## Name(HashSet ## Name * set); \ + HSIterator ## Name * iterator ## Name(HashSet ## Name * set); + + +#define HashSetImpl(Name, _Key, hash_function, equals) \ + HashTableImpl(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals); \ + HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name *_curr, HashSet ## Name * _set) { \ + HSIterator ## Name * hsit = (HSIterator ## Name *) ourmalloc(sizeof(HSIterator ## Name)); \ + hsit->curr=_curr; \ + hsit->set=_set; \ + return hsit; \ + } \ + \ + void deleteIter ## Name(HSIterator ## Name *hsit) { \ + ourfree(hsit); \ + } \ + \ + bool hasNext ## Name(HSIterator ## Name *hsit) { \ + return hsit->curr!=NULL; \ + } \ + \ + _Key next ## Name(HSIterator ## Name *hsit) { \ + _Key k=hsit->curr->key; \ + hsit->last=hsit->curr; \ + hsit->curr=hsit->curr->next; \ + return k; \ + } \ + \ + _Key currKey ## Name(HSIterator ## Name *hsit) { \ + return hsit->last->key; \ + } \ + \ + void removeIter ## Name(HSIterator ## Name *hsit) { \ + _Key k=hsit->last->key; \ + removeSet ## Name(hsit->set, k); \ + } \ + \ + HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor) { \ + HashSet ## Name * set = (HashSet ## Name *) ourmalloc(sizeof(struct HashSet ## Name)); \ + set->table=allocHashTable ## Name ## Set(initialcapacity, factor); \ + set->list=NULL; \ + set->tail=NULL; \ + return 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; \ + } \ + deleteHashTable ## Name ## Set(set->table); \ + ourfree(set); \ + } \ + \ + HashSet ## Name * copy ## Name(HashSet ## Name * set) { \ + HashSet ## Name *copy=allocHashSet ## Name(getCapacity ## Name ## Set(set->table), getLoadFactor ## Name ## Set(set->table)); \ + HSIterator ## Name * it=iterator ## Name(set); \ + while(hasNext ## Name(it)) \ + add ## Name(copy, next ## Name(it)); \ + deleteIter ## Name(it); \ + return copy; \ + } \ + \ + void resetSet ## Name(HashSet ## Name * set) { \ + LinkNode ## Name *tmp=set->list; \ + while(tmp!=NULL) { \ + LinkNode ## Name *tmpnext=tmp->next; \ + ourfree(tmp); \ + tmp=tmpnext; \ + } \ + set->list=set->tail=NULL; \ + reset ## Name ## Set(set->table); \ + } \ + \ + bool add ## Name(HashSet ## Name * set,_Key key) { \ + LinkNode ## Name * val=get ## Name ## Set(set->table, key); \ + if (val==NULL) { \ + LinkNode ## Name * newnode=(LinkNode ## Name *)ourmalloc(sizeof(struct LinkNode ## Name)); \ + newnode->prev=set->tail; \ + newnode->next=NULL; \ + newnode->key=key; \ + if (set->tail!=NULL) \ + set->tail->next=newnode; \ + else \ + set->list=newnode; \ + set->tail=newnode; \ + put ## Name ## Set(set->table, key, newnode); \ + return true; \ + } else \ + return false; \ + } \ + \ + _Key getSet ## Name(HashSet ## Name * set,_Key key) { \ + LinkNode ## Name * val=get ## Name ## Set(set->table, key); \ + if (val!=NULL) \ + return val->key; \ + else \ + return NULL; \ + } \ + \ + _Key getFirstKey ## Name(HashSet ## Name * set) { \ + return set->list->key; \ + } \ + \ + bool containsSet ## Name(HashSet ## Name * set,_Key key) { \ + return get ## Name ## Set(set->table, key)!=NULL; \ + } \ + \ + bool removeSet ## Name(HashSet ## Name * set,_Key key) { \ + LinkNode ## Name * oldlinknode; \ + oldlinknode=get ## Name ## Set(set->table, key); \ + if (oldlinknode==NULL) { \ + return false; \ + } \ + remove ## Name ## Set(set->table, key); \ + \ + if (oldlinknode->prev==NULL) \ + set->list=oldlinknode->next; \ + else \ + oldlinknode->prev->next=oldlinknode->next; \ + if (oldlinknode->next!=NULL) \ + oldlinknode->next->prev=oldlinknode->prev; \ + else \ + set->tail=oldlinknode->prev; \ + ourfree(oldlinknode); \ + return true; \ + } \ + \ + unsigned int getSizeSet ## Name(HashSet ## Name * set) { \ + return getSizeTable ## Name ## Set(set->table); \ + } \ + \ + bool isEmpty ## Name(HashSet ## Name * set) { \ + return getSizeSet ## Name(set)==0; \ + } \ + \ + HSIterator ## Name * iterator ## Name(HashSet ## Name * set) { \ + return allocHSIterator ## Name(set->list, set); \ + } +#endif diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h new file mode 100644 index 0000000..e0db665 --- /dev/null +++ b/src/Collections/hashtable.h @@ -0,0 +1,281 @@ +/* Copyright (c) 2015 Regents of the University of California + * + * Author: Brian Demsky + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * version 2 as published by the Free Software Foundation. + */ + +/** @file hashtable.h + * @brief Hashtable. Standard chained bucket variety. + */ + +#ifndef __HASHTABLE_H__ +#define __HASHTABLE_H__ + +#include +#include +#include +#include "mymemory.h" +#include "common.h" + +/** + * @brief A simple, custom hash table + * + * By default it is model_malloc, but you can pass in your own allocation + * functions. Note that this table does not support the value 0 (NULL) used as + * a key and is designed primarily with pointer-based keys in mind. Other + * primitive key types are supported only for non-zero values. + * + * @tparam _Key Type name for the key + * @tparam _Val Type name for the values to be stored + */ +#define HashTableDef(Name, _Key, _Val, hash_function, equals)\ + struct hashlistnode ## Name { \ + _Key key; \ + _Val val; \ + }; \ + \ + struct HashTable ## Name { \ + struct hashlistnode ## Name *table; \ + struct hashlistnode ## Name *zero; \ + unsigned int capacity; \ + unsigned int size; \ + unsigned int capacitymask; \ + unsigned int threshold; \ + double loadfactor; \ + }; \ + \ + typedef struct HashTable ## Name HashTable ## Name; \ + HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor); \ + 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); \ + _Val get ## Name(const HashTable ## Name * tab, _Key key); \ + _Val remove ## Name(HashTable ## Name * tab, _Key key); \ + unsigned int getSizeTable ## Name(const HashTable ## Name * tab); \ + bool contains ## Name(const HashTable ## Name * tab, _Key key); \ + void resize ## Name(HashTable ## Name * tab, unsigned int newsize); \ + double getLoadFactor ## Name(HashTable ## Name * tab); \ + unsigned int getCapacity ## Name(HashTable ## Name * tab); + +#define HashTableImpl(Name, _Key, _Val, hash_function, equals) \ + HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor) { \ + HashTable ## Name * tab = (HashTable ## Name *) ourmalloc(sizeof(HashTable ## Name)); \ + tab -> table = (struct hashlistnode ## Name *) ourcalloc(initialcapacity, sizeof(struct hashlistnode ## Name)); \ + tab->zero = NULL; \ + tab->loadfactor = factor; \ + tab->capacity = initialcapacity; \ + tab->capacitymask = initialcapacity - 1; \ + \ + tab->threshold = (unsigned int)(initialcapacity * factor); \ + tab->size = 0; \ + return tab; \ + } \ + \ + void deleteHashTable ## Name(HashTable ## Name * tab) { \ + ourfree(tab->table); \ + if (tab->zero) \ + ourfree(tab->zero); \ + ourfree(tab); \ + } \ + \ + void reset ## Name(HashTable ## Name * tab) { \ + memset(tab->table, 0, tab->capacity * sizeof(struct hashlistnode ## Name)); \ + if (tab->zero) { \ + ourfree(tab->zero); \ + tab->zero = NULL; \ + } \ + tab->size = 0; \ + } \ + \ + void resetandfree ## Name(HashTable ## Name * tab) { \ + for(unsigned int i=0;icapacity;i++) { \ + struct hashlistnode ## Name *bin = &tab->table[i]; \ + if (bin->key != NULL) { \ + bin->key = NULL; \ + if (bin->val != NULL) { \ + ourfree(bin->val); \ + bin->val = NULL; \ + } \ + } \ + } \ + if (tab->zero) { \ + if (tab->zero->val != NULL) \ + ourfree(tab->zero->val); \ + ourfree(tab->zero); \ + tab->zero = NULL; \ + } \ + tab->size = 0; \ + } \ + \ + void put ## Name(HashTable ## Name * tab, _Key key, _Val val) { \ + if (!key) { \ + if (!tab->zero) { \ + tab->zero=(struct hashlistnode ## Name *)ourmalloc(sizeof(struct hashlistnode ## Name)); \ + tab->size++; \ + } \ + tab->zero->key=key; \ + tab->zero->val=val; \ + return; \ + } \ + \ + if (tab->size > tab->threshold) \ + resize ## Name (tab, tab->capacity << 1); \ + \ + struct hashlistnode ## Name *search; \ + \ + unsigned int index = hash_function(key); \ + do { \ + index &= tab->capacitymask; \ + search = &tab->table[index]; \ + if (!search->key) { \ + break; \ + } \ + if (equals(search->key, key)) { \ + search->val = val; \ + return; \ + } \ + index++; \ + } while (true); \ + \ + search->key = key; \ + search->val = val; \ + tab->size++; \ + } \ + \ + _Val get ## Name(const HashTable ## Name * tab, _Key key) { \ + struct hashlistnode ## Name *search; \ + \ + if (!key) { \ + if (tab->zero) \ + return tab->zero->val; \ + else \ + return (_Val) 0; \ + } \ + \ + unsigned int oindex = hash_function(key) & tab->capacitymask; \ + unsigned int index=oindex; \ + do { \ + search = &tab->table[index]; \ + if (!search->key) { \ + if (!search->val) \ + break; \ + } else \ + if (equals(search->key, key)) \ + return search->val; \ + index++; \ + index &= tab->capacitymask; \ + if (index==oindex) \ + break; \ + } while (true); \ + return (_Val)0; \ + } \ + \ + _Val remove ## Name(HashTable ## Name * tab, _Key key) { \ + struct hashlistnode ## Name *search; \ + \ + if (!key) { \ + if (!tab->zero) { \ + return (_Val)0; \ + } else { \ + _Val v=tab->zero->val; \ + ourfree(tab->zero); \ + tab->zero=NULL; \ + tab->size--; \ + return v; \ + } \ + } \ + \ + unsigned int index = hash_function(key); \ + do { \ + index &= tab->capacitymask; \ + search = &tab->table[index]; \ + if (!search->key) { \ + if (!search->val) \ + break; \ + } else \ + if (equals(search->key, key)) { \ + _Val v=search->val; \ + search->val=(_Val) 1; \ + search->key=0; \ + tab->size--; \ + return v; \ + } \ + index++; \ + } while (true); \ + return (_Val)0; \ + } \ + \ + unsigned int getSizeTable ## Name(const HashTable ## Name * tab) { \ + return tab->size; \ + } \ + \ + \ + bool contains ## Name(const HashTable ## Name * tab, _Key key) { \ + struct hashlistnode ## Name *search; \ + if (!key) { \ + return tab->zero!=NULL; \ + } \ + unsigned int index = hash_function(key); \ + do { \ + index &= tab->capacitymask; \ + search = &tab->table[index]; \ + if (!search->key) { \ + if (!search->val) \ + break; \ + } else \ + if (equals(search->key, key)) \ + return true; \ + index++; \ + } while (true); \ + return false; \ + } \ + \ + void resize ## Name(HashTable ## Name * tab, unsigned int newsize) { \ + struct hashlistnode ## Name *oldtable = tab->table; \ + struct hashlistnode ## Name *newtable; \ + unsigned int oldcapacity = tab->capacity; \ + \ + if ((newtable = (struct hashlistnode ## Name *)ourcalloc(newsize, sizeof(struct hashlistnode ## Name))) == NULL) { \ + model_print("calloc error %s %d\n", __FILE__, __LINE__); \ + exit(EXIT_FAILURE); \ + } \ + \ + tab->table = newtable; \ + tab->capacity = newsize; \ + tab->capacitymask = newsize - 1; \ + \ + tab->threshold = (unsigned int)(newsize * tab->loadfactor); \ + \ + struct hashlistnode ## Name *bin = &oldtable[0]; \ + struct hashlistnode ## Name *lastbin = &oldtable[oldcapacity]; \ + for (;bin < lastbin;bin++) { \ + _Key key = bin->key; \ + \ + struct hashlistnode ## Name *search; \ + if (!key) \ + continue; \ + \ + unsigned int index = hash_function(key); \ + do { \ + index &= tab->capacitymask; \ + search = &tab->table[index]; \ + index++; \ + } while (search->key); \ + \ + search->key = key; \ + search->val = bin->val; \ + } \ + \ + ourfree(oldtable); \ + } \ + double getLoadFactor ## Name(HashTable ## Name * tab) {return tab->loadfactor;} \ + unsigned int getCapacity ## Name(HashTable ## Name * tab) {return tab->capacity;} + + + + +#endif/* __HASHTABLE_H__ */ diff --git a/src/Collections/structs.c b/src/Collections/structs.c new file mode 100644 index 0000000..30bca42 --- /dev/null +++ b/src/Collections/structs.c @@ -0,0 +1,11 @@ +#include "structs.h" +#include "mymemory.h" + +VectorImpl(Int, uint64_t, 4); +VectorImpl(Void, void *, 4); +VectorImpl(Boolean, Boolean *, 4); +VectorImpl(Constraint, Constraint *, 4); +VectorImpl(Set, Set *, 4); +VectorImpl(Element, Element *, 4); +HashTableImpl(Void, void *, void *, Ptr_hash_function, Ptr_equals); +HashSetImpl(Void, void *, Ptr_hash_function, Ptr_equals); diff --git a/src/Collections/structs.h b/src/Collections/structs.h new file mode 100644 index 0000000..888f359 --- /dev/null +++ b/src/Collections/structs.h @@ -0,0 +1,25 @@ +#ifndef STRUCTS_H +#define STRUCTS_H +#include "vector.h" +#include "hashtable.h" +#include "hashset.h" +#include "classlist.h" + +VectorDef(Int, uint64_t, 4); +VectorDef(Void, void *, 4); +VectorDef(Boolean, Boolean *, 4); +VectorDef(Constraint, Constraint *, 4); +VectorDef(Set, Set *, 4); +VectorDef(Element, Element *, 4); + +inline unsigned int Ptr_hash_function(void * hash) { + return (unsigned int)((uint64_t)hash >> 4); +} + +inline bool Ptr_equals(void * key1, void * key2) { + return key1 == key2; +} + +HashTableDef(Void, void *, void *, Ptr_hash_function, Ptr_equals); +HashSetDef(Void, void *, Ptr_hash_function, Ptr_equals); +#endif diff --git a/src/Collections/vector.h b/src/Collections/vector.h new file mode 100644 index 0000000..d131a27 --- /dev/null +++ b/src/Collections/vector.h @@ -0,0 +1,61 @@ +#ifndef VECTOR_H +#define VECTOR_H +#include + +#define VectorDef(name, type, defcap) \ + struct Vector ## name { \ + uint size; \ + uint capacity; \ + type * array; \ + }; \ + typedef struct Vector ## name Vector ## name; \ + Vector ## name * allocVector ## name(uint capacity); \ + Vector ## name * allocDefVector ## name(); \ + Vector ## name * allocVectorArray ## name(uint capacity, type * array); \ + void pushVector ## name(Vector ## name *vector, type item); \ + 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 deleteVector ##name(Vector ##name *vector); \ + void clearVector ##name(Vector ## name *vector); + +#define VectorImpl(name, type, defcap) \ + Vector ## name * allocDefVector ## name() { \ + return allocVector ## name(defcap); \ + } \ + Vector ## name * allocVector ## name(uint capacity) { \ + Vector ## name * tmp = (Vector ## name *) ourmalloc(sizeof(type)); \ + tmp->size = 0; \ + tmp->capacity = capacity; \ + tmp->array = (type *) ourcalloc(1, sizeof(type) * capacity); \ + return tmp; \ + } \ + Vector ## name * allocVectorArray ## name(uint capacity, type * array) { \ + Vector ## name * tmp = allocVector ## name(capacity); \ + memcpy(tmp->array, array, capacity * sizeof(type)); \ + return tmp; \ + } \ + void pushVector ## name(Vector ## name *vector, type item) { \ + if (vector->size >= vector->capacity) { \ + uint newcap=vector->capacity * 2; \ + vector->array=(type *)ourrealloc(vector->array, newcap); \ + } \ + vector->array[vector->size++] = item; \ + } \ + type getVector ## name(Vector ## name * vector, uint index) { \ + return vector->array[index]; \ + } \ + void setVector ## name(Vector ## name * vector, uint index, type item) { \ + vector->array[index]=item; \ + } \ + uint getSizeVector ## name(Vector ## name *vector) { \ + return vector->size; \ + } \ + void deleteVector ##name(Vector ##name *vector) { \ + ourfree(vector->array); \ + ourfree(vector); \ + } \ + void clearVector ##name(Vector ## name *vector) { \ + vector->size=0; \ + } +#endif diff --git a/src/Makefile b/src/Makefile index a5408be..1358986 100644 --- a/src/Makefile +++ b/src/Makefile @@ -4,13 +4,11 @@ PHONY += directories 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 inc_solver.c - -TABBING_H := boolean.h classlist.h common.h config.h constraint.h csolver.h element.h function.h inc_solver.h mutableset.h mymemory.h ops.h order.h predicate.h set.h solver_interface.h structs.h table.h +C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o) -CPPFLAGS += -Iinclude -I. +CFLAGS += -IAST -ICollections -IBackend -I. LDFLAGS := -ldl -lrt -rdynamic SHARED := -shared @@ -28,8 +26,11 @@ directories: ${OBJ_DIR} ${OBJ_DIR}: ${MKDIR_P} ${OBJ_DIR} + ${MKDIR_P} ${OBJ_DIR}/AST + ${MKDIR_P} ${OBJ_DIR}/Collections + ${MKDIR_P} ${OBJ_DIR}/Backend -debug: CPPFLAGS += -DCONFIG_DEBUG +debug: CFLAGS += -DCONFIG_DEBUG debug: all PHONY += docs @@ -37,16 +38,10 @@ docs: *.c *.cc *.h doxygen $(LIB_SO): $(OBJECTS) - $(CXX) -g $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS) + $(CC) -g $(SHARED) -o ${OBJ_DIR}/$(LIB_SO) $+ $(LDFLAGS) ${OBJ_DIR}/%.o: %.c - $(CC) -fPIC -c $< -o $@ $(CPPFLAGS) -Wno-unused-variable - -${OBJ_DIR}/%.o: %.cc - $(CXX) -MMD -MF $@.d -o $@ -fPIC -c $< $(CPPFLAGS) - -%.pdf: %.dot - dot -Tpdf $< -o $@ + $(CC) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable -include $(OBJECTS:%=$OBJ_DIR/.%.d) @@ -65,7 +60,7 @@ tags: tabbing: uncrustify -c C.cfg --no-backup *.c - uncrustify -c C.cfg --no-backup $(TABBING_H) + uncrustify -c C.cfg --no-backup *.h */*.h .PHONY: $(PHONY) diff --git a/src/boolean.c b/src/boolean.c deleted file mode 100644 index 13070fa..0000000 --- a/src/boolean.c +++ /dev/null @@ -1 +0,0 @@ -#include "boolean.h" diff --git a/src/boolean.h b/src/boolean.h deleted file mode 100644 index 5e8c5a5..0000000 --- a/src/boolean.h +++ /dev/null @@ -1,8 +0,0 @@ -#ifndef BOOLEAN_H -#define BOOLEAN_H -#include "classlist.h" -#include "mymemory.h" - -struct Boolean { -}; -#endif diff --git a/src/constraint.c b/src/constraint.c deleted file mode 100644 index 8b38540..0000000 --- a/src/constraint.c +++ /dev/null @@ -1,420 +0,0 @@ -/* Copyright (c) 2015 Regents of the University of California - * - * Author: Brian Demsky - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - -#include "constraint.h" -#include "mymemory.h" -#include "inc_solver.h" - -Constraint ctrue={TRUE, 0xffffffff, NULL, NULL}; -Constraint cfalse={FALSE, 0xffffffff, NULL, NULL}; - -Constraint * allocConstraint(CType t, Constraint *l, Constraint *r) { - Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint)); - this->type=t; - this->numoperandsorvar=2; - this->operands=(Constraint **)ourmalloc(2*sizeof(Constraint *)); - this->neg=NULL; - ASSERT(l!=NULL); - //if (type==IMPLIES) { - //type=OR; - // operands[0]=l->negate(); - // } else { - this->operands[0]=l; - // } - this->operands[1]=r; - return this; -} - -Constraint * allocUnaryConstraint(CType t, Constraint *l) { - Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint)); - this->type=t; - this->numoperandsorvar=1; - this->operands=(Constraint **) ourmalloc(sizeof(Constraint *)); - this->neg=NULL; - this->operands[0]=l; - return this; -} - -Constraint * allocArrayConstraint(CType t, uint num, Constraint **array) { - Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint)); - this->type=t; - this->numoperandsorvar=num; - this->operands=(Constraint **) ourmalloc(num*sizeof(Constraint *)); - this->neg=NULL; - memcpy(this->operands, array, num*sizeof(Constraint *)); - return this; -} - -Constraint * allocVarConstraint(CType t, uint v) { - Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint)); - this->type=t; - this->numoperandsorvar=v; - this->operands=NULL; - this->neg=NULL; - return this; -} - -void deleteConstraint(Constraint *this) { - if (this->operands!=NULL) - ourfree(this->operands); -} - -void dumpConstraint(Constraint * this, IncrementalSolver *solver) { - if (this->type==VAR) { - addClauseLiteral(solver, this->numoperandsorvar); - addClauseLiteral(solver, 0); - } else if (this->type==NOTVAR) { - addClauseLiteral(solver, -this->numoperandsorvar); - addClauseLiteral(solver, 0); - } else { - ASSERT(this->type==OR); - for(uint i=0;inumoperandsorvar;i++) { - Constraint *c=this->operands[i]; - if (c->type==VAR) { - addClauseLiteral(solver, c->numoperandsorvar); - } else if (c->type==NOTVAR) { - addClauseLiteral(solver, -c->numoperandsorvar); - } else ASSERT(0); - } - addClauseLiteral(solver, 0); - } -} - -void internalfreeConstraint(Constraint * this) { - switch(this->type) { - case TRUE: - case FALSE: - case NOTVAR: - case VAR: - return; - case BOGUS: - ASSERT(0); - default: - this->type=BOGUS; - ourfree(this); - } -} - -void freerecConstraint(Constraint *this) { - switch(this->type) { - case TRUE: - case FALSE: - case NOTVAR: - case VAR: - return; - case BOGUS: - ASSERT(0); - default: - if (this->operands!=NULL) { - for(uint i=0;inumoperandsorvar;i++) - freerecConstraint(this->operands[i]); - } - this->type=BOGUS; - deleteConstraint(this); - } -} - - -void printConstraint(Constraint * this) { - switch(this->type) { - case TRUE: - model_print("true"); - break; - case FALSE: - model_print("false"); - break; - case IMPLIES: - model_print("("); - printConstraint(this->operands[0]); - model_print(")"); - model_print("=>"); - model_print("("); - printConstraint(this->operands[1]); - model_print(")"); - break; - case AND: - case OR: - model_print("("); - for(uint i=0;inumoperandsorvar;i++) { - if (i!=0) { - if (this->type==AND) - model_print(" ^ "); - else - model_print(" v "); - } - printConstraint(this->operands[i]); - } - model_print(")"); - break; - case VAR: - model_print("t%u",this->numoperandsorvar); - break; - case NOTVAR: - model_print("!t%u",this->numoperandsorvar); - break; - default: - ASSERT(0); - } -} - -Constraint * cloneConstraint(Constraint * this) { - switch(this->type) { - case TRUE: - case FALSE: - case VAR: - case NOTVAR: - return this; - case IMPLIES: - return allocConstraint(IMPLIES, cloneConstraint(this->operands[0]), cloneConstraint(this->operands[1])); - case AND: - case OR: { - Constraint *array[this->numoperandsorvar]; - for(uint i=0;inumoperandsorvar;i++) { - array[i]=cloneConstraint(this->operands[i]); - } - return allocArrayConstraint(this->type, this->numoperandsorvar, array); - } - default: - ASSERT(0); - return NULL; - } -} - -Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value) { - Constraint *carray[numvars]; - for(uint j=0;j>1; - } - - return allocArrayConstraint(AND, numvars, carray); -} - -/** Generates a constraint to ensure that all encodings are less than value */ -Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) { - Constraint *orarray[numvars]; - Constraint *andarray[numvars]; - uint andi=0; - - while(true) { - uint val=value; - uint ori=0; - for(uint j=0;j>1; - } - //no ones to flip, so bail now... - if (ori==0) { - return allocArrayConstraint(AND, andi, andarray); - } - andarray[andi++]=allocArrayConstraint(OR, ori, orarray); - - value=value+(1<<(__builtin_ctz(value))); - //flip the last one - } -} - -Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) { - if (numvars==0) - return &ctrue; - Constraint *array[numvars*2]; - for(uint i=0;itype==TRUE) - continue; - if (c->type==FALSE) { - for(uint j=i+1;jtype) { - case TRUE: - case VAR: - case NOTVAR: - case FALSE: { - VectorConstraint * vec=allocDefVectorConstraint(); - pushVectorConstraint(vec, this); - return vec; - } - case AND: { - VectorConstraint *vec=allocDefVectorConstraint(); - for(uint i=0;inumoperandsorvar;i++) { - VectorConstraint * subvec=simplifyConstraint(this->operands[i]); - if (mergeandfree(vec, subvec)) { - for(uint j=i+1;jnumoperandsorvar;j++) { - freerecConstraint(this->operands[j]); - } - internalfreeConstraint(this); - return vec; - } - } - internalfreeConstraint(this); - return vec; - } - case OR: { - for(uint i=0;inumoperandsorvar;i++) { - Constraint *c=this->operands[i]; - switch(c->type) { - case TRUE: { - VectorConstraint * vec=allocDefVectorConstraint(); - pushVectorConstraint(vec, c); - freerecConstraint(this); - return vec; - } - case FALSE: { - Constraint *array[this->numoperandsorvar-1]; - uint index=0; - for(uint j=0;jnumoperandsorvar;j++) { - if (j!=i) - array[index++]=this->operands[j]; - } - Constraint *cn=allocArrayConstraint(OR, index, array); - VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(this); - return vec; - } - case VAR: - case NOTVAR: - break; - case OR: { - uint nsize=this->numoperandsorvar+c->numoperandsorvar-1; - Constraint *array[nsize]; - uint index=0; - for(uint j=0;jnumoperandsorvar;j++) - if (j!=i) - array[index++]=this->operands[j]; - for(uint j=0;jnumoperandsorvar;j++) - array[index++]=c->operands[j]; - Constraint *cn=allocArrayConstraint(OR, nsize, array); - VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(this); - internalfreeConstraint(c); - return vec; - } - case IMPLIES: { - uint nsize=this->numoperandsorvar+1; - Constraint *array[nsize]; - uint index=0; - for(uint j=0;jnumoperandsorvar;j++) - if (j!=i) - array[index++]=this->operands[j]; - array[index++]=negateConstraint(c->operands[0]); - array[index++]=c->operands[1]; - Constraint *cn=allocArrayConstraint(OR, nsize, array); - VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(this); - internalfreeConstraint(c); - return vec; - } - case AND: { - Constraint *array[this->numoperandsorvar]; - - VectorConstraint *vec=allocDefVectorConstraint(); - for(uint j=0;jnumoperandsorvar;j++) { - //copy other elements - for(uint k=0;knumoperandsorvar;k++) { - if (k!=i) { - array[k]=cloneConstraint(this->operands[k]); - } - } - - array[i]=cloneConstraint(c->operands[j]); - Constraint *cn=allocArrayConstraint(OR, this->numoperandsorvar, array); - VectorConstraint * newvec=simplifyConstraint(cn); - if (mergeandfree(vec, newvec)) { - freerecConstraint(this); - return vec; - } - } - freerecConstraint(this); - return vec; - } - default: - ASSERT(0); - } - //continue on to next item - } - VectorConstraint * vec=allocDefVectorConstraint(); - if (this->numoperandsorvar==1) { - Constraint *c=this->operands[0]; - freerecConstraint(this); - pushVectorConstraint(vec, c); - } else - pushVectorConstraint(vec, this); - return vec; - } - case IMPLIES: { - Constraint *cn=allocConstraint(OR, negateConstraint(this->operands[0]), this->operands[1]); - VectorConstraint * vec=simplifyConstraint(cn); - internalfreeConstraint(this); - return vec; - } - default: - ASSERT(0); - return NULL; - } -} - -Constraint * negateConstraint(Constraint * this) { - switch(this->type) { - case TRUE: - return &cfalse; - case FALSE: - return &ctrue; - case NOTVAR: - case VAR: - return this->neg; - case IMPLIES: { - Constraint *l=this->operands[0]; - Constraint *r=this->operands[1]; - this->operands[0]=r; - this->operands[1]=l; - return this; - } - case AND: - case OR: { - for(uint i=0;inumoperandsorvar;i++) { - this->operands[i]=negateConstraint(this->operands[i]); - } - this->type=(this->type==AND) ? OR : AND; - return this; - } - default: - ASSERT(0); - return NULL; - } -} diff --git a/src/constraint.h b/src/constraint.h deleted file mode 100644 index 06bb1d1..0000000 --- a/src/constraint.h +++ /dev/null @@ -1,54 +0,0 @@ -/* Copyright (c) 2015 Regents of the University of California - * - * Author: Brian Demsky - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - -#ifndef CONSTRAINT_H -#define CONSTRAINT_H -#include "classlist.h" -#include "structs.h" - -enum ConstraintType { - TRUE, FALSE, IMPLIES, AND, OR, VAR, NOTVAR, BOGUS -}; - -typedef enum ConstraintType CType; - -struct Constraint { - CType type; - uint numoperandsorvar; - Constraint ** operands; - Constraint *neg; -}; - -Constraint * allocConstraint(CType t, Constraint *l, Constraint *r); -Constraint * allocUnaryConstraint(CType t, Constraint *l); -Constraint * allocArrayConstraint(CType t, uint num, Constraint ** array); -Constraint * allocVarConstraint(CType t, uint var); - -void deleteConstraint(Constraint *); -void printConstraint(Constraint * c); -void dumpConstraint(Constraint * c, IncrementalSolver *solver); -uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;} -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;} -void internalfreeConstraint(Constraint * c); -void freerecConstraint(Constraint * c); -Constraint * cloneConstraint(Constraint * c); -void setNegConstraint(Constraint * this, Constraint *c) {this->neg=c;} -Constraint *negateConstraint(Constraint * c); - -extern Constraint ctrue; -extern Constraint cfalse; - -Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value); -Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value); -Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2); -Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2); -#endif diff --git a/src/element.c b/src/element.c deleted file mode 100644 index 191686c..0000000 --- a/src/element.c +++ /dev/null @@ -1,11 +0,0 @@ -#include "element.h" - -Element *allocElement(Set * s) { - Element * tmp=(Element *)ourmalloc(sizeof(Element)); - tmp->set=s; - return tmp; -} - -void deleteElement(Element *this) { - ourfree(this); -} diff --git a/src/element.h b/src/element.h deleted file mode 100644 index 8f0f082..0000000 --- a/src/element.h +++ /dev/null @@ -1,12 +0,0 @@ -#ifndef ELEMENT_H -#define ELEMENT_H -#include "classlist.h" -#include "mymemory.h" - -struct Element { - Set * set; -}; - -Element * allocElement(Set *s); -void deleteElement(Element *this); -#endif diff --git a/src/function.c b/src/function.c deleted file mode 100644 index d4b693e..0000000 --- a/src/function.c +++ /dev/null @@ -1 +0,0 @@ -#include "function.h" diff --git a/src/function.h b/src/function.h deleted file mode 100644 index da5087b..0000000 --- a/src/function.h +++ /dev/null @@ -1,8 +0,0 @@ -#ifndef FUNCTION_H -#define FUNCTION_H -#include "classlist.h" -#include "mymemory.h" - -struct Function { -}; -#endif diff --git a/src/hashset.h b/src/hashset.h deleted file mode 100644 index 6d87078..0000000 --- a/src/hashset.h +++ /dev/null @@ -1,194 +0,0 @@ -/* Copyright (c) 2015 Regents of the University of California - * - * Author: Brian Demsky - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - -#ifndef HASH_SET_H -#define HASH_SET_H -#include "hashtable.h" - -#define HashSetDef(Name, _Key, hash_function, equals) \ - struct LinkNode ## Name { \ - _Key key; \ - struct LinkNode ## Name *prev; \ - struct LinkNode ## Name *next; \ - }; \ - typedef struct LinkNode ## Name LinkNode ## Name; \ - struct HashSet ## Name; \ - typedef struct HashSet ## Name HashSet ## Name; \ - struct HSIterator ## Name { \ - LinkNode ## Name *curr; \ - LinkNode ## Name *last; \ - 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 deleteIter ## Name(HSIterator ## Name *hsit); \ - bool hasNext ## Name(HSIterator ## Name *hsit); \ - _Key next ## Name(HSIterator ## Name *hsit); \ - _Key currKey ## Name(HSIterator ## Name *hsit); \ - void removeIter ## Name(HSIterator ## Name *hsit); \ - struct HashSet ## Name { \ - HashTable ## Name ## Set * table; \ - LinkNode ## Name *list; \ - LinkNode ## Name *tail; \ - }; \ - typedef struct HashSet ## Name HashSet ## Name; \ - \ - HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor); \ - 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); \ - _Key getSet ## Name(HashSet ## Name * set,_Key key); \ - _Key getFirstKey ## Name(HashSet ## Name * set); \ - bool containsSet ## Name(HashSet ## Name * set,_Key key); \ - bool removeSet ## Name(HashSet ## Name * set,_Key key); \ - unsigned int getSizeSet ## Name(HashSet ## Name * set); \ - bool isEmpty ## Name(HashSet ## Name * set); \ - HSIterator ## Name * iterator ## Name(HashSet ## Name * set); - - -#define HashSetImpl(Name, _Key, hash_function, equals) \ - HashTableImpl(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals); \ - HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name *_curr, HashSet ## Name * _set) { \ - HSIterator ## Name * hsit = (HSIterator ## Name *) ourmalloc(sizeof(HSIterator ## Name)); \ - hsit->curr=_curr; \ - hsit->set=_set; \ - return hsit; \ - } \ - \ - void deleteIter ## Name(HSIterator ## Name *hsit) { \ - ourfree(hsit); \ - } \ - \ - bool hasNext ## Name(HSIterator ## Name *hsit) { \ - return hsit->curr!=NULL; \ - } \ - \ - _Key next ## Name(HSIterator ## Name *hsit) { \ - _Key k=hsit->curr->key; \ - hsit->last=hsit->curr; \ - hsit->curr=hsit->curr->next; \ - return k; \ - } \ - \ - _Key currKey ## Name(HSIterator ## Name *hsit) { \ - return hsit->last->key; \ - } \ - \ - void removeIter ## Name(HSIterator ## Name *hsit) { \ - _Key k=hsit->last->key; \ - removeSet ## Name(hsit->set, k); \ - } \ - \ - HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor) { \ - HashSet ## Name * set = (HashSet ## Name *) ourmalloc(sizeof(struct HashSet ## Name)); \ - set->table=allocHashTable ## Name ## Set(initialcapacity, factor); \ - set->list=NULL; \ - set->tail=NULL; \ - return 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; \ - } \ - deleteHashTable ## Name ## Set(set->table); \ - ourfree(set); \ - } \ - \ - HashSet ## Name * copy ## Name(HashSet ## Name * set) { \ - HashSet ## Name *copy=allocHashSet ## Name(getCapacity ## Name ## Set(set->table), getLoadFactor ## Name ## Set(set->table)); \ - HSIterator ## Name * it=iterator ## Name(set); \ - while(hasNext ## Name(it)) \ - add ## Name(copy, next ## Name(it)); \ - deleteIter ## Name(it); \ - return copy; \ - } \ - \ - void resetSet ## Name(HashSet ## Name * set) { \ - LinkNode ## Name *tmp=set->list; \ - while(tmp!=NULL) { \ - LinkNode ## Name *tmpnext=tmp->next; \ - ourfree(tmp); \ - tmp=tmpnext; \ - } \ - set->list=set->tail=NULL; \ - reset ## Name ## Set(set->table); \ - } \ - \ - bool add ## Name(HashSet ## Name * set,_Key key) { \ - LinkNode ## Name * val=get ## Name ## Set(set->table, key); \ - if (val==NULL) { \ - LinkNode ## Name * newnode=(LinkNode ## Name *)ourmalloc(sizeof(struct LinkNode ## Name)); \ - newnode->prev=set->tail; \ - newnode->next=NULL; \ - newnode->key=key; \ - if (set->tail!=NULL) \ - set->tail->next=newnode; \ - else \ - set->list=newnode; \ - set->tail=newnode; \ - put ## Name ## Set(set->table, key, newnode); \ - return true; \ - } else \ - return false; \ - } \ - \ - _Key getSet ## Name(HashSet ## Name * set,_Key key) { \ - LinkNode ## Name * val=get ## Name ## Set(set->table, key); \ - if (val!=NULL) \ - return val->key; \ - else \ - return NULL; \ - } \ - \ - _Key getFirstKey ## Name(HashSet ## Name * set) { \ - return set->list->key; \ - } \ - \ - bool containsSet ## Name(HashSet ## Name * set,_Key key) { \ - return get ## Name ## Set(set->table, key)!=NULL; \ - } \ - \ - bool removeSet ## Name(HashSet ## Name * set,_Key key) { \ - LinkNode ## Name * oldlinknode; \ - oldlinknode=get ## Name ## Set(set->table, key); \ - if (oldlinknode==NULL) { \ - return false; \ - } \ - remove ## Name ## Set(set->table, key); \ - \ - if (oldlinknode->prev==NULL) \ - set->list=oldlinknode->next; \ - else \ - oldlinknode->prev->next=oldlinknode->next; \ - if (oldlinknode->next!=NULL) \ - oldlinknode->next->prev=oldlinknode->prev; \ - else \ - set->tail=oldlinknode->prev; \ - ourfree(oldlinknode); \ - return true; \ - } \ - \ - unsigned int getSizeSet ## Name(HashSet ## Name * set) { \ - return getSizeTable ## Name ## Set(set->table); \ - } \ - \ - bool isEmpty ## Name(HashSet ## Name * set) { \ - return getSizeSet ## Name(set)==0; \ - } \ - \ - HSIterator ## Name * iterator ## Name(HashSet ## Name * set) { \ - return allocHSIterator ## Name(set->list, set); \ - } -#endif diff --git a/src/hashtable.h b/src/hashtable.h deleted file mode 100644 index e0db665..0000000 --- a/src/hashtable.h +++ /dev/null @@ -1,281 +0,0 @@ -/* Copyright (c) 2015 Regents of the University of California - * - * Author: Brian Demsky - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - -/** @file hashtable.h - * @brief Hashtable. Standard chained bucket variety. - */ - -#ifndef __HASHTABLE_H__ -#define __HASHTABLE_H__ - -#include -#include -#include -#include "mymemory.h" -#include "common.h" - -/** - * @brief A simple, custom hash table - * - * By default it is model_malloc, but you can pass in your own allocation - * functions. Note that this table does not support the value 0 (NULL) used as - * a key and is designed primarily with pointer-based keys in mind. Other - * primitive key types are supported only for non-zero values. - * - * @tparam _Key Type name for the key - * @tparam _Val Type name for the values to be stored - */ -#define HashTableDef(Name, _Key, _Val, hash_function, equals)\ - struct hashlistnode ## Name { \ - _Key key; \ - _Val val; \ - }; \ - \ - struct HashTable ## Name { \ - struct hashlistnode ## Name *table; \ - struct hashlistnode ## Name *zero; \ - unsigned int capacity; \ - unsigned int size; \ - unsigned int capacitymask; \ - unsigned int threshold; \ - double loadfactor; \ - }; \ - \ - typedef struct HashTable ## Name HashTable ## Name; \ - HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor); \ - 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); \ - _Val get ## Name(const HashTable ## Name * tab, _Key key); \ - _Val remove ## Name(HashTable ## Name * tab, _Key key); \ - unsigned int getSizeTable ## Name(const HashTable ## Name * tab); \ - bool contains ## Name(const HashTable ## Name * tab, _Key key); \ - void resize ## Name(HashTable ## Name * tab, unsigned int newsize); \ - double getLoadFactor ## Name(HashTable ## Name * tab); \ - unsigned int getCapacity ## Name(HashTable ## Name * tab); - -#define HashTableImpl(Name, _Key, _Val, hash_function, equals) \ - HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor) { \ - HashTable ## Name * tab = (HashTable ## Name *) ourmalloc(sizeof(HashTable ## Name)); \ - tab -> table = (struct hashlistnode ## Name *) ourcalloc(initialcapacity, sizeof(struct hashlistnode ## Name)); \ - tab->zero = NULL; \ - tab->loadfactor = factor; \ - tab->capacity = initialcapacity; \ - tab->capacitymask = initialcapacity - 1; \ - \ - tab->threshold = (unsigned int)(initialcapacity * factor); \ - tab->size = 0; \ - return tab; \ - } \ - \ - void deleteHashTable ## Name(HashTable ## Name * tab) { \ - ourfree(tab->table); \ - if (tab->zero) \ - ourfree(tab->zero); \ - ourfree(tab); \ - } \ - \ - void reset ## Name(HashTable ## Name * tab) { \ - memset(tab->table, 0, tab->capacity * sizeof(struct hashlistnode ## Name)); \ - if (tab->zero) { \ - ourfree(tab->zero); \ - tab->zero = NULL; \ - } \ - tab->size = 0; \ - } \ - \ - void resetandfree ## Name(HashTable ## Name * tab) { \ - for(unsigned int i=0;icapacity;i++) { \ - struct hashlistnode ## Name *bin = &tab->table[i]; \ - if (bin->key != NULL) { \ - bin->key = NULL; \ - if (bin->val != NULL) { \ - ourfree(bin->val); \ - bin->val = NULL; \ - } \ - } \ - } \ - if (tab->zero) { \ - if (tab->zero->val != NULL) \ - ourfree(tab->zero->val); \ - ourfree(tab->zero); \ - tab->zero = NULL; \ - } \ - tab->size = 0; \ - } \ - \ - void put ## Name(HashTable ## Name * tab, _Key key, _Val val) { \ - if (!key) { \ - if (!tab->zero) { \ - tab->zero=(struct hashlistnode ## Name *)ourmalloc(sizeof(struct hashlistnode ## Name)); \ - tab->size++; \ - } \ - tab->zero->key=key; \ - tab->zero->val=val; \ - return; \ - } \ - \ - if (tab->size > tab->threshold) \ - resize ## Name (tab, tab->capacity << 1); \ - \ - struct hashlistnode ## Name *search; \ - \ - unsigned int index = hash_function(key); \ - do { \ - index &= tab->capacitymask; \ - search = &tab->table[index]; \ - if (!search->key) { \ - break; \ - } \ - if (equals(search->key, key)) { \ - search->val = val; \ - return; \ - } \ - index++; \ - } while (true); \ - \ - search->key = key; \ - search->val = val; \ - tab->size++; \ - } \ - \ - _Val get ## Name(const HashTable ## Name * tab, _Key key) { \ - struct hashlistnode ## Name *search; \ - \ - if (!key) { \ - if (tab->zero) \ - return tab->zero->val; \ - else \ - return (_Val) 0; \ - } \ - \ - unsigned int oindex = hash_function(key) & tab->capacitymask; \ - unsigned int index=oindex; \ - do { \ - search = &tab->table[index]; \ - if (!search->key) { \ - if (!search->val) \ - break; \ - } else \ - if (equals(search->key, key)) \ - return search->val; \ - index++; \ - index &= tab->capacitymask; \ - if (index==oindex) \ - break; \ - } while (true); \ - return (_Val)0; \ - } \ - \ - _Val remove ## Name(HashTable ## Name * tab, _Key key) { \ - struct hashlistnode ## Name *search; \ - \ - if (!key) { \ - if (!tab->zero) { \ - return (_Val)0; \ - } else { \ - _Val v=tab->zero->val; \ - ourfree(tab->zero); \ - tab->zero=NULL; \ - tab->size--; \ - return v; \ - } \ - } \ - \ - unsigned int index = hash_function(key); \ - do { \ - index &= tab->capacitymask; \ - search = &tab->table[index]; \ - if (!search->key) { \ - if (!search->val) \ - break; \ - } else \ - if (equals(search->key, key)) { \ - _Val v=search->val; \ - search->val=(_Val) 1; \ - search->key=0; \ - tab->size--; \ - return v; \ - } \ - index++; \ - } while (true); \ - return (_Val)0; \ - } \ - \ - unsigned int getSizeTable ## Name(const HashTable ## Name * tab) { \ - return tab->size; \ - } \ - \ - \ - bool contains ## Name(const HashTable ## Name * tab, _Key key) { \ - struct hashlistnode ## Name *search; \ - if (!key) { \ - return tab->zero!=NULL; \ - } \ - unsigned int index = hash_function(key); \ - do { \ - index &= tab->capacitymask; \ - search = &tab->table[index]; \ - if (!search->key) { \ - if (!search->val) \ - break; \ - } else \ - if (equals(search->key, key)) \ - return true; \ - index++; \ - } while (true); \ - return false; \ - } \ - \ - void resize ## Name(HashTable ## Name * tab, unsigned int newsize) { \ - struct hashlistnode ## Name *oldtable = tab->table; \ - struct hashlistnode ## Name *newtable; \ - unsigned int oldcapacity = tab->capacity; \ - \ - if ((newtable = (struct hashlistnode ## Name *)ourcalloc(newsize, sizeof(struct hashlistnode ## Name))) == NULL) { \ - model_print("calloc error %s %d\n", __FILE__, __LINE__); \ - exit(EXIT_FAILURE); \ - } \ - \ - tab->table = newtable; \ - tab->capacity = newsize; \ - tab->capacitymask = newsize - 1; \ - \ - tab->threshold = (unsigned int)(newsize * tab->loadfactor); \ - \ - struct hashlistnode ## Name *bin = &oldtable[0]; \ - struct hashlistnode ## Name *lastbin = &oldtable[oldcapacity]; \ - for (;bin < lastbin;bin++) { \ - _Key key = bin->key; \ - \ - struct hashlistnode ## Name *search; \ - if (!key) \ - continue; \ - \ - unsigned int index = hash_function(key); \ - do { \ - index &= tab->capacitymask; \ - search = &tab->table[index]; \ - index++; \ - } while (search->key); \ - \ - search->key = key; \ - search->val = bin->val; \ - } \ - \ - ourfree(oldtable); \ - } \ - double getLoadFactor ## Name(HashTable ## Name * tab) {return tab->loadfactor;} \ - unsigned int getCapacity ## Name(HashTable ## Name * tab) {return tab->capacity;} - - - - -#endif/* __HASHTABLE_H__ */ diff --git a/src/inc_solver.c b/src/inc_solver.c deleted file mode 100644 index c25cfba..0000000 --- a/src/inc_solver.c +++ /dev/null @@ -1,166 +0,0 @@ -/* Copyright (c) 2015 Regents of the University of California - * - * Author: Brian Demsky - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - -#include "inc_solver.h" -#define SATSOLVER "sat_solver" -#include -#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; -} - -void deleteIncrementalSolver(IncrementalSolver * this) { - killSolver(this); - ourfree(this->buffer); - if (this->solution != NULL) - ourfree(this->solution); -} - -void resetSolver(IncrementalSolver * this) { - killSolver(this); - this->offset = 0; - createSolver(this); -} - -void addClauseLiteral(IncrementalSolver * this, int literal) { - this->buffer[this->offset++]=literal; - if (this->offset==IS_BUFFERSIZE) { - flushBufferSolver(this); - } -} - -void finishedClauses(IncrementalSolver * this) { - addClauseLiteral(this, 0); -} - -void freeze(IncrementalSolver * this, int variable) { - addClauseLiteral(this, IS_FREEZE); - addClauseLiteral(this, variable); -} - -int solve(IncrementalSolver * this) { - //add an empty clause - startSolve(this); - return getSolution(this); -} - - -void startSolve(IncrementalSolver *this) { - addClauseLiteral(this, IS_RUNSOLVER); - flushBufferSolver(this); -} - -int getSolution(IncrementalSolver * this) { - int result=readIntSolver(this); - if (result == IS_SAT) { - 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(this, &this->solution[1], numVars * sizeof(int)); - } - return result; -} - -int readIntSolver(IncrementalSolver * this) { - int value; - readSolver(this, &value, 4); - return value; -} - -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(this->from_solver_fd, &((char *)result)[bytesread], bytestoread); - if (n == -1) { - model_print("Read failure\n"); - exit(-1); - } - bytestoread -= n; - bytesread += n; - } while(bytestoread != 0); -} - -bool getValueSolver(IncrementalSolver * this, int variable) { - return this->solution[variable]; -} - -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 ((this->solver_pid = fork()) == -1) { - model_print("Error forking.\n"); - exit(-1); - } - if (this->solver_pid == 0) { - //Solver process - close(to_pipe[1]); - close(from_pipe[0]); - int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU); - - if ((dup2(to_pipe[0], 0) == -1) || - (dup2(from_pipe[1], IS_OUT_FD) == -1) || - (dup2(fd, 1) == -1)) { - model_print("Error duplicating pipes\n"); - } - // setsid(); - execlp(SATSOLVER, SATSOLVER, NULL); - model_print("execlp Failed\n"); - close(fd); - } else { - //Our process - this->to_solver_fd = to_pipe[1]; - this->from_solver_fd = from_pipe[0]; - close(to_pipe[0]); - close(from_pipe[1]); - } -} - -void killSolver(IncrementalSolver * this) { - close(this->to_solver_fd); - close(this->from_solver_fd); - //Stop the solver - if (this->solver_pid > 0) { - int status; - kill(this->solver_pid, SIGKILL); - waitpid(this->solver_pid, &status, 0); - } -} - -void flushBufferSolver(IncrementalSolver * this) { - ssize_t bytestowrite=sizeof(int)*this->offset; - ssize_t byteswritten=0; - do { - 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",this->to_solver_fd); - exit(-1); - } - bytestowrite -= n; - byteswritten += n; - } while(bytestowrite != 0); - this->offset = 0; -} diff --git a/src/inc_solver.h b/src/inc_solver.h deleted file mode 100644 index ead727f..0000000 --- a/src/inc_solver.h +++ /dev/null @@ -1,46 +0,0 @@ -/* Copyright (c) 2015 Regents of the University of California - * - * Author: Brian Demsky - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - -#ifndef INC_SOLVER_H -#define INC_SOLVER_H -#include -#include -#include -#include -#include -#include -#include "solver_interface.h" -#include "classlist.h" - -struct IncrementalSolver { - int * buffer; - int * solution; - int solutionsize; - int offset; - pid_t solver_pid; - 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 diff --git a/src/mutableset.c b/src/mutableset.c deleted file mode 100644 index 18f038b..0000000 --- a/src/mutableset.c +++ /dev/null @@ -1,15 +0,0 @@ -#include "mutableset.h" - -MutableSet * allocMutableSet(VarType t) { - MutableSet * tmp=(MutableSet *)ourmalloc(sizeof(MutableSet)); - tmp->type=t; - tmp->isRange=false; - tmp->low=0; - tmp->high=0; - tmp->members=allocDefVectorInt(); - return tmp; -} - -void addElementMSet(MutableSet * set, uint64_t element) { - pushVectorInt(set->members, element); -} diff --git a/src/mutableset.h b/src/mutableset.h deleted file mode 100644 index fe089f4..0000000 --- a/src/mutableset.h +++ /dev/null @@ -1,7 +0,0 @@ -#ifndef MUTABLESET_H -#define MUTABLESET_H -#include "set.h" - -MutableSet * allocMutableSet(VarType t); -void addElementMSet(MutableSet * set, uint64_t element); -#endif diff --git a/src/ops.h b/src/ops.h deleted file mode 100644 index 40e6f99..0000000 --- a/src/ops.h +++ /dev/null @@ -1,17 +0,0 @@ -#ifndef OPS_H -#define OPS_H -enum LogicOp {AND, OR, NOT, XOR, IMPLIES}; -enum ArithOp {ADD, SUB}; -enum CompOp {EQUALS}; -enum OrderType {PARTIAL, TOTAL}; - -/** - * FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true - * OVERFLOWSETSFLAG -- sets the flag if the operation overflows - * FLAGIFFOVERFLOW -- flag is set iff the operation overflows - * IGNORE -- doesn't constrain output if the result cannot be represented - * WRAPAROUND -- wraps around like stand integer arithmetic - */ -enum OverFlowBehavior {IGNORE, WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW}; - -#endif diff --git a/src/order.c b/src/order.c deleted file mode 100644 index 727b2dd..0000000 --- a/src/order.c +++ /dev/null @@ -1 +0,0 @@ -#include "order.h" diff --git a/src/order.h b/src/order.h deleted file mode 100644 index b164a11..0000000 --- a/src/order.h +++ /dev/null @@ -1,8 +0,0 @@ -#ifndef ORDER_H -#define ORDER_H -#include "classlist.h" -#include "mymemory.h" - -struct Order { -}; -#endif diff --git a/src/predicate.c b/src/predicate.c deleted file mode 100644 index dcec97a..0000000 --- a/src/predicate.c +++ /dev/null @@ -1 +0,0 @@ -#include "predicate.h" diff --git a/src/predicate.h b/src/predicate.h deleted file mode 100644 index 9a17669..0000000 --- a/src/predicate.h +++ /dev/null @@ -1,9 +0,0 @@ -#ifndef PREDICATE_H -#define PREDICATE_H -#include "classlist.h" -#include "mymemory.h" - -struct Predicate { - -}; -#endif diff --git a/src/set.c b/src/set.c deleted file mode 100644 index fc056a2..0000000 --- a/src/set.c +++ /dev/null @@ -1,28 +0,0 @@ -#include "set.h" -#include - -Set * allocSet(VarType t, uint64_t* elements, uint num) { - Set * tmp=(Set *)ourmalloc(sizeof(Set)); - tmp->type=t; - tmp->isRange=false; - tmp->low=0; - tmp->high=0; - tmp->members=allocVectorArrayInt(num, elements); - return tmp; -} - -Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) { - Set * tmp=(Set *)ourmalloc(sizeof(Set)); - tmp->type=t; - tmp->isRange=true; - tmp->low=lowrange; - tmp->high=highrange; - tmp->members=NULL; - return tmp; -} - -void deleteSet(Set * set) { - if (!set->isRange) - deleteVectorInt(set->members); - ourfree(set); -} diff --git a/src/set.h b/src/set.h deleted file mode 100644 index 92315e2..0000000 --- a/src/set.h +++ /dev/null @@ -1,28 +0,0 @@ -/* - * File: set.h - * Author: hamed - * - * Created on June 13, 2017, 3:01 PM - */ - -#ifndef SET_H -#define SET_H - -#include "classlist.h" -#include "structs.h" -#include "mymemory.h" - -struct Set { - VarType type; - bool isRange; - uint64_t low;//also used to count unique items - uint64_t high; - VectorInt * members; -}; - - -Set *allocSet(VarType t, uint64_t * elements, uint num); -Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange); -void deleteSet(Set *set); -#endif/* SET_H */ - diff --git a/src/solver_interface.h b/src/solver_interface.h deleted file mode 100644 index 4fd2dea..0000000 --- a/src/solver_interface.h +++ /dev/null @@ -1,23 +0,0 @@ -/* Copyright (c) 2015 Regents of the University of California - * - * Author: Brian Demsky - * - * This program is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * version 2 as published by the Free Software Foundation. - */ - -#ifndef SOLVER_INTERFACE_H -#define SOLVER_INTERFACE_H - -#define IS_OUT_FD 3 - -#define IS_UNSAT 0 -#define IS_SAT 1 -#define IS_INDETER 2 -#define IS_FREEZE 3 -#define IS_RUNSOLVER 4 - -#define IS_BUFFERSIZE 1024 - -#endif diff --git a/src/structs.c b/src/structs.c deleted file mode 100644 index 30bca42..0000000 --- a/src/structs.c +++ /dev/null @@ -1,11 +0,0 @@ -#include "structs.h" -#include "mymemory.h" - -VectorImpl(Int, uint64_t, 4); -VectorImpl(Void, void *, 4); -VectorImpl(Boolean, Boolean *, 4); -VectorImpl(Constraint, Constraint *, 4); -VectorImpl(Set, Set *, 4); -VectorImpl(Element, Element *, 4); -HashTableImpl(Void, void *, void *, Ptr_hash_function, Ptr_equals); -HashSetImpl(Void, void *, Ptr_hash_function, Ptr_equals); diff --git a/src/structs.h b/src/structs.h deleted file mode 100644 index 888f359..0000000 --- a/src/structs.h +++ /dev/null @@ -1,25 +0,0 @@ -#ifndef STRUCTS_H -#define STRUCTS_H -#include "vector.h" -#include "hashtable.h" -#include "hashset.h" -#include "classlist.h" - -VectorDef(Int, uint64_t, 4); -VectorDef(Void, void *, 4); -VectorDef(Boolean, Boolean *, 4); -VectorDef(Constraint, Constraint *, 4); -VectorDef(Set, Set *, 4); -VectorDef(Element, Element *, 4); - -inline unsigned int Ptr_hash_function(void * hash) { - return (unsigned int)((uint64_t)hash >> 4); -} - -inline bool Ptr_equals(void * key1, void * key2) { - return key1 == key2; -} - -HashTableDef(Void, void *, void *, Ptr_hash_function, Ptr_equals); -HashSetDef(Void, void *, Ptr_hash_function, Ptr_equals); -#endif diff --git a/src/table.c b/src/table.c deleted file mode 100644 index e89d72a..0000000 --- a/src/table.c +++ /dev/null @@ -1 +0,0 @@ -#include "table.h" diff --git a/src/table.h b/src/table.h deleted file mode 100644 index 2bb9805..0000000 --- a/src/table.h +++ /dev/null @@ -1,11 +0,0 @@ -#ifndef TABLE_H -#define TABLE_H -#include "classlist.h" -#include "mymemory.h" - -struct Table { - -}; - -Table * allocTable(); -#endif diff --git a/src/vector.h b/src/vector.h deleted file mode 100644 index d131a27..0000000 --- a/src/vector.h +++ /dev/null @@ -1,61 +0,0 @@ -#ifndef VECTOR_H -#define VECTOR_H -#include - -#define VectorDef(name, type, defcap) \ - struct Vector ## name { \ - uint size; \ - uint capacity; \ - type * array; \ - }; \ - typedef struct Vector ## name Vector ## name; \ - Vector ## name * allocVector ## name(uint capacity); \ - Vector ## name * allocDefVector ## name(); \ - Vector ## name * allocVectorArray ## name(uint capacity, type * array); \ - void pushVector ## name(Vector ## name *vector, type item); \ - 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 deleteVector ##name(Vector ##name *vector); \ - void clearVector ##name(Vector ## name *vector); - -#define VectorImpl(name, type, defcap) \ - Vector ## name * allocDefVector ## name() { \ - return allocVector ## name(defcap); \ - } \ - Vector ## name * allocVector ## name(uint capacity) { \ - Vector ## name * tmp = (Vector ## name *) ourmalloc(sizeof(type)); \ - tmp->size = 0; \ - tmp->capacity = capacity; \ - tmp->array = (type *) ourcalloc(1, sizeof(type) * capacity); \ - return tmp; \ - } \ - Vector ## name * allocVectorArray ## name(uint capacity, type * array) { \ - Vector ## name * tmp = allocVector ## name(capacity); \ - memcpy(tmp->array, array, capacity * sizeof(type)); \ - return tmp; \ - } \ - void pushVector ## name(Vector ## name *vector, type item) { \ - if (vector->size >= vector->capacity) { \ - uint newcap=vector->capacity * 2; \ - vector->array=(type *)ourrealloc(vector->array, newcap); \ - } \ - vector->array[vector->size++] = item; \ - } \ - type getVector ## name(Vector ## name * vector, uint index) { \ - return vector->array[index]; \ - } \ - void setVector ## name(Vector ## name * vector, uint index, type item) { \ - vector->array[index]=item; \ - } \ - uint getSizeVector ## name(Vector ## name *vector) { \ - return vector->size; \ - } \ - void deleteVector ##name(Vector ##name *vector) { \ - ourfree(vector->array); \ - ourfree(vector); \ - } \ - void clearVector ##name(Vector ## name *vector) { \ - vector->size=0; \ - } -#endif