--- /dev/null
+#include "boolean.h"
--- /dev/null
+#ifndef BOOLEAN_H
+#define BOOLEAN_H
+#include "classlist.h"
+#include "mymemory.h"
+
+struct Boolean {
+};
+#endif
--- /dev/null
+#include "element.h"
+
+Element *allocElement(Set * s) {
+ Element * tmp=(Element *)ourmalloc(sizeof(Element));
+ tmp->set=s;
+ return tmp;
+}
+
+void deleteElement(Element *this) {
+ ourfree(this);
+}
--- /dev/null
+#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
--- /dev/null
+#include "function.h"
--- /dev/null
+#ifndef FUNCTION_H
+#define FUNCTION_H
+#include "classlist.h"
+#include "mymemory.h"
+
+struct Function {
+};
+#endif
--- /dev/null
+#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);
+}
--- /dev/null
+#ifndef MUTABLESET_H
+#define MUTABLESET_H
+#include "set.h"
+
+MutableSet * allocMutableSet(VarType t);
+void addElementMSet(MutableSet * set, uint64_t element);
+#endif
--- /dev/null
+#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
--- /dev/null
+#include "order.h"
--- /dev/null
+#ifndef ORDER_H
+#define ORDER_H
+#include "classlist.h"
+#include "mymemory.h"
+
+struct Order {
+};
+#endif
--- /dev/null
+#include "predicate.h"
--- /dev/null
+#ifndef PREDICATE_H
+#define PREDICATE_H
+#include "classlist.h"
+#include "mymemory.h"
+
+struct Predicate {
+
+};
+#endif
--- /dev/null
+#include "set.h"
+#include <stddef.h>
+
+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);
+}
--- /dev/null
+/*
+ * 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 */
+
--- /dev/null
+#include "table.h"
--- /dev/null
+#ifndef TABLE_H
+#define TABLE_H
+#include "classlist.h"
+#include "mymemory.h"
+
+struct Table {
+
+};
+
+Table * allocTable();
+#endif
--- /dev/null
+/* Copyright (c) 2015 Regents of the University of California
+ *
+ * Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ * 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;i<this->numoperandsorvar;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;i<this->numoperandsorvar;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;i<this->numoperandsorvar;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;i<this->numoperandsorvar;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<numvars;j++) {
+ carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
+ value=value>>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<numvars;j++) {
+ if ((val&1)==1)
+ orarray[ori++]=negateConstraint(vars[j]);
+ val=val>>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;i<numvars;i++) {
+ array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
+ array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));
+ }
+ return allocArrayConstraint(AND, numvars*2, array);
+}
+
+Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
+ Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2);
+ Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2)));
+
+ return allocConstraint(AND, imp1, imp2);
+}
+
+bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
+ for(uint i=0;i<getSizeVectorConstraint(from);i++) {
+ Constraint *c=getVectorConstraint(from, i);
+ if (c->type==TRUE)
+ continue;
+ if (c->type==FALSE) {
+ for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
+ freerecConstraint(getVectorConstraint(from,j));
+ for(uint j=0;j<getSizeVectorConstraint(to);j++)
+ freerecConstraint(getVectorConstraint(to, j));
+ clearVectorConstraint(to);
+ pushVectorConstraint(to, &ctrue);
+ deleteVectorConstraint(from);
+ return true;
+ }
+ pushVectorConstraint(to, c);
+ }
+ deleteVectorConstraint(from);
+ return false;
+}
+
+VectorConstraint * simplifyConstraint(Constraint * this) {
+ switch(this->type) {
+ 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;i<this->numoperandsorvar;i++) {
+ VectorConstraint * subvec=simplifyConstraint(this->operands[i]);
+ if (mergeandfree(vec, subvec)) {
+ for(uint j=i+1;j<this->numoperandsorvar;j++) {
+ freerecConstraint(this->operands[j]);
+ }
+ internalfreeConstraint(this);
+ return vec;
+ }
+ }
+ internalfreeConstraint(this);
+ return vec;
+ }
+ case OR: {
+ for(uint i=0;i<this->numoperandsorvar;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;j<this->numoperandsorvar;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;j<this->numoperandsorvar;j++)
+ if (j!=i)
+ array[index++]=this->operands[j];
+ for(uint j=0;j<c->numoperandsorvar;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;j<this->numoperandsorvar;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;j<c->numoperandsorvar;j++) {
+ //copy other elements
+ for(uint k=0;k<this->numoperandsorvar;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;i<this->numoperandsorvar;i++) {
+ this->operands[i]=negateConstraint(this->operands[i]);
+ }
+ this->type=(this->type==AND) ? OR : AND;
+ return this;
+ }
+ default:
+ ASSERT(0);
+ return NULL;
+ }
+}
--- /dev/null
+/* Copyright (c) 2015 Regents of the University of California
+ *
+ * Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ * 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
--- /dev/null
+/* Copyright (c) 2015 Regents of the University of California
+ *
+ * Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ * 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 <fcntl.h>
+#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;
+}
--- /dev/null
+/* Copyright (c) 2015 Regents of the University of California
+ *
+ * Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ * 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 <sys/types.h>
+#include <sys/wait.h>
+#include <unistd.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <signal.h>
+#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
--- /dev/null
+/* Copyright (c) 2015 Regents of the University of California
+ *
+ * Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ * 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
--- /dev/null
+/* Copyright (c) 2015 Regents of the University of California
+ *
+ * Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ * 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
--- /dev/null
+/* Copyright (c) 2015 Regents of the University of California
+ *
+ * Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ * 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 <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#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;i<tab->capacity;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__ */
--- /dev/null
+#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);
--- /dev/null
+#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
--- /dev/null
+#ifndef VECTOR_H
+#define VECTOR_H
+#include <string.h>
+
+#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
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
${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
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)
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)
+++ /dev/null
-#include "boolean.h"
+++ /dev/null
-#ifndef BOOLEAN_H
-#define BOOLEAN_H
-#include "classlist.h"
-#include "mymemory.h"
-
-struct Boolean {
-};
-#endif
+++ /dev/null
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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;i<this->numoperandsorvar;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;i<this->numoperandsorvar;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;i<this->numoperandsorvar;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;i<this->numoperandsorvar;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<numvars;j++) {
- carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
- value=value>>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<numvars;j++) {
- if ((val&1)==1)
- orarray[ori++]=negateConstraint(vars[j]);
- val=val>>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;i<numvars;i++) {
- array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
- array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));
- }
- return allocArrayConstraint(AND, numvars*2, array);
-}
-
-Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
- Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2);
- Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2)));
-
- return allocConstraint(AND, imp1, imp2);
-}
-
-bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
- for(uint i=0;i<getSizeVectorConstraint(from);i++) {
- Constraint *c=getVectorConstraint(from, i);
- if (c->type==TRUE)
- continue;
- if (c->type==FALSE) {
- for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
- freerecConstraint(getVectorConstraint(from,j));
- for(uint j=0;j<getSizeVectorConstraint(to);j++)
- freerecConstraint(getVectorConstraint(to, j));
- clearVectorConstraint(to);
- pushVectorConstraint(to, &ctrue);
- deleteVectorConstraint(from);
- return true;
- }
- pushVectorConstraint(to, c);
- }
- deleteVectorConstraint(from);
- return false;
-}
-
-VectorConstraint * simplifyConstraint(Constraint * this) {
- switch(this->type) {
- 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;i<this->numoperandsorvar;i++) {
- VectorConstraint * subvec=simplifyConstraint(this->operands[i]);
- if (mergeandfree(vec, subvec)) {
- for(uint j=i+1;j<this->numoperandsorvar;j++) {
- freerecConstraint(this->operands[j]);
- }
- internalfreeConstraint(this);
- return vec;
- }
- }
- internalfreeConstraint(this);
- return vec;
- }
- case OR: {
- for(uint i=0;i<this->numoperandsorvar;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;j<this->numoperandsorvar;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;j<this->numoperandsorvar;j++)
- if (j!=i)
- array[index++]=this->operands[j];
- for(uint j=0;j<c->numoperandsorvar;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;j<this->numoperandsorvar;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;j<c->numoperandsorvar;j++) {
- //copy other elements
- for(uint k=0;k<this->numoperandsorvar;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;i<this->numoperandsorvar;i++) {
- this->operands[i]=negateConstraint(this->operands[i]);
- }
- this->type=(this->type==AND) ? OR : AND;
- return this;
- }
- default:
- ASSERT(0);
- return NULL;
- }
-}
+++ /dev/null
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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
+++ /dev/null
-#include "element.h"
-
-Element *allocElement(Set * s) {
- Element * tmp=(Element *)ourmalloc(sizeof(Element));
- tmp->set=s;
- return tmp;
-}
-
-void deleteElement(Element *this) {
- ourfree(this);
-}
+++ /dev/null
-#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
+++ /dev/null
-#include "function.h"
+++ /dev/null
-#ifndef FUNCTION_H
-#define FUNCTION_H
-#include "classlist.h"
-#include "mymemory.h"
-
-struct Function {
-};
-#endif
+++ /dev/null
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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
+++ /dev/null
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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 <stdlib.h>
-#include <stdio.h>
-#include <string.h>
-#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;i<tab->capacity;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__ */
+++ /dev/null
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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 <fcntl.h>
-#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;
-}
+++ /dev/null
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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 <sys/types.h>
-#include <sys/wait.h>
-#include <unistd.h>
-#include <stdio.h>
-#include <stdlib.h>
-#include <signal.h>
-#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
+++ /dev/null
-#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);
-}
+++ /dev/null
-#ifndef MUTABLESET_H
-#define MUTABLESET_H
-#include "set.h"
-
-MutableSet * allocMutableSet(VarType t);
-void addElementMSet(MutableSet * set, uint64_t element);
-#endif
+++ /dev/null
-#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
+++ /dev/null
-#include "order.h"
+++ /dev/null
-#ifndef ORDER_H
-#define ORDER_H
-#include "classlist.h"
-#include "mymemory.h"
-
-struct Order {
-};
-#endif
+++ /dev/null
-#include "predicate.h"
+++ /dev/null
-#ifndef PREDICATE_H
-#define PREDICATE_H
-#include "classlist.h"
-#include "mymemory.h"
-
-struct Predicate {
-
-};
-#endif
+++ /dev/null
-#include "set.h"
-#include <stddef.h>
-
-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);
-}
+++ /dev/null
-/*
- * 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 */
-
+++ /dev/null
-/* Copyright (c) 2015 Regents of the University of California
- *
- * Author: Brian Demsky <bdemsky@uci.edu>
- *
- * 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
+++ /dev/null
-#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);
+++ /dev/null
-#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
+++ /dev/null
-#include "table.h"
+++ /dev/null
-#ifndef TABLE_H
-#define TABLE_H
-#include "classlist.h"
-#include "mymemory.h"
-
-struct Table {
-
-};
-
-Table * allocTable();
-#endif
+++ /dev/null
-#ifndef VECTOR_H
-#define VECTOR_H
-#include <string.h>
-
-#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
projects / satune.git / commitdiff