Switch to C for Zach
authorbdemsky <bdemsky@uci.edu>
Wed, 14 Jun 2017 22:44:45 +0000 (15:44 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 14 Jun 2017 22:44:45 +0000 (15:44 -0700)
23 files changed:
src/boolean.c [new file with mode: 0644]
src/boolean.cc [deleted file]
src/classlist.h
src/constraint.c [new file with mode: 0644]
src/constraint.cc [deleted file]
src/csolver.c [new file with mode: 0644]
src/element.c [new file with mode: 0644]
src/element.cc [deleted file]
src/function.c [new file with mode: 0644]
src/function.cc [deleted file]
src/inc_solver.c [new file with mode: 0644]
src/inc_solver.cc [deleted file]
src/mutableset.c [new file with mode: 0644]
src/mutableset.cc [deleted file]
src/mymemory.h
src/order.c [new file with mode: 0644]
src/order.cc [deleted file]
src/predicate.c [new file with mode: 0644]
src/predicate.cc [deleted file]
src/set.c [new file with mode: 0644]
src/set.cc [deleted file]
src/table.c [new file with mode: 0644]
src/table.cc [deleted file]

diff --git a/src/boolean.c b/src/boolean.c
new file mode 100644 (file)
index 0000000..13070fa
--- /dev/null
@@ -0,0 +1 @@
+#include "boolean.h"
diff --git a/src/boolean.cc b/src/boolean.cc
deleted file mode 100644 (file)
index 13070fa..0000000
+++ /dev/null
@@ -1 +0,0 @@
-#include "boolean.h"
index 4c48778..53555ed 100644 (file)
 #include "mymemory.h"
 #include <inttypes.h>
 
-class Constraint;
-class Boolean;
-class IncrementalSolver;
-class Set;
-class MutableSet;
-class Element;
-class Function;
-class Predicate;
-class Table;
-class Order;
+struct Constraint;
+typedef struct Constraint Constraint;
+
+struct Boolean;
+typedef struct Boolean Boolean;
+
+struct IncrementalSolver;
+typedef struct IncrementSolver IncrementalSolver;
+
+struct Set;
+typedef struct Set Set;
+
+typedef struct Set MutableSet;
+
+struct Element;
+typedef struct Element Element;
+
+struct Function;
+typedef struct Function Function;
+
+struct Predicate;
+typedef struct Predicat Predicate;
+
+struct Table;
+typedef struct Table Table;
+
+struct Order;
+typedef struct Order Order;
 
 typedef unsigned int uint;
 typedef uint64_t VarType;
diff --git a/src/constraint.c b/src/constraint.c
new file mode 100644 (file)
index 0000000..c8a622a
--- /dev/null
@@ -0,0 +1,424 @@
+/*      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);
+Constraint cfalse(FALSE);
+
+Constraint::Constraint(CType t, Constraint *l, Constraint *r) :
+       type(t),
+       numoperandsorvar(2),
+       operands((Constraint **)model_malloc(2*sizeof(Constraint *))),
+       neg(NULL)
+{
+       ASSERT(l!=NULL);
+       //if (type==IMPLIES) {
+       //type=OR;
+       //      operands[0]=l->negate();
+       //      } else {
+       operands[0]=l;
+       //      }
+       operands[1]=r;
+}
+
+Constraint::Constraint(CType t, Constraint *l) :
+       type(t),
+       numoperandsorvar(1),
+       operands((Constraint **)model_malloc(sizeof(Constraint *))),
+       neg(NULL)
+{
+       operands[0]=l;
+}
+
+Constraint::Constraint(CType t, uint num, Constraint **array) :
+       type(t),
+       numoperandsorvar(num),
+       operands((Constraint **)model_malloc(num*sizeof(Constraint *))),
+       neg(NULL)
+{
+       memcpy(operands, array, num*sizeof(Constraint *));
+}
+
+Constraint::Constraint(CType t) :
+       type(t),
+       numoperandsorvar(0xffffffff),
+       operands(NULL),
+       neg(NULL)
+{
+}
+
+Constraint::Constraint(CType t, uint v) :
+       type(t),
+       numoperandsorvar(v),
+       operands(NULL),
+       neg(NULL)
+{
+}
+
+Constraint::~Constraint() {
+       if (operands!=NULL)
+               model_free(operands);
+}
+
+void Constraint::dumpConstraint(IncrementalSolver *solver) {
+       if (type==VAR) {
+               solver->addClauseLiteral(numoperandsorvar);
+               solver->addClauseLiteral(0);
+       } else if (type==NOTVAR) {
+               solver->addClauseLiteral(-numoperandsorvar);
+               solver->addClauseLiteral(0);
+       } else {
+               ASSERT(type==OR);
+               for(uint i=0;i<numoperandsorvar;i++) {
+                       Constraint *c=operands[i];
+                       if (c->type==VAR) {
+                               solver->addClauseLiteral(c->numoperandsorvar);
+                       } else if (c->type==NOTVAR) {
+                               solver->addClauseLiteral(-c->numoperandsorvar);
+                       } else ASSERT(0);
+               }
+               solver->addClauseLiteral(0);
+       }
+}
+
+void Constraint::free() {
+       switch(type) {
+       case TRUE:
+       case FALSE:
+       case NOTVAR:
+       case VAR:
+               return;
+       case BOGUS:
+               ASSERT(0);
+       default:
+               type=BOGUS;
+               delete this;
+       }
+}
+
+void Constraint::freerec() {
+       switch(type) {
+       case TRUE:
+       case FALSE:
+       case NOTVAR:
+       case VAR:
+               return;
+       case BOGUS:
+               ASSERT(0);
+       default:
+               if (operands!=NULL) {
+                       for(uint i=0;i<numoperandsorvar;i++)
+                               operands[i]->freerec();
+               }
+               type=BOGUS;
+               delete this;
+       }
+}
+
+
+void Constraint::print() {
+       switch(type) {
+       case TRUE:
+               model_print("true");
+               break;
+       case FALSE:
+               model_print("false");
+               break;
+       case IMPLIES:
+               model_print("(");
+               operands[0]->print();
+               model_print(")");
+               model_print("=>");
+               model_print("(");
+               operands[1]->print();
+               model_print(")");
+               break;
+       case AND:
+       case OR:
+               model_print("(");
+               for(uint i=0;i<numoperandsorvar;i++) {
+                       if (i!=0) {
+                               if (type==AND)
+                                       model_print(" ^ ");
+                               else
+                                       model_print(" v ");
+                       }
+                       operands[i]->print();
+               }
+               model_print(")");
+               break;
+       case VAR:
+               model_print("t%u",numoperandsorvar);
+               break;
+       case NOTVAR:
+               model_print("!t%u",numoperandsorvar);
+               break;
+       default:
+               ASSERT(0);
+       }
+}
+
+Constraint * Constraint::clone() {
+       switch(type) {
+       case TRUE:
+       case FALSE:
+       case VAR:
+       case NOTVAR:
+               return this;
+       case IMPLIES:
+               return new Constraint(IMPLIES, operands[0]->clone(), operands[1]->clone());
+       case AND:
+       case OR: {
+               Constraint *array[numoperandsorvar];
+               for(uint i=0;i<numoperandsorvar;i++) {
+                       array[i]=operands[i]->clone();
+               }
+               return new Constraint(type, 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] : vars[j]->negate();
+               value=value>>1;
+       }
+
+       return new Constraint(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++]=vars[j]->negate();
+                       val=val>>1;
+               }
+               //no ones to flip, so bail now...
+               if (ori==0) {
+                       return new Constraint(AND, andi, andarray);
+               }
+               andarray[andi++]=new Constraint(OR, ori, orarray);
+
+               value=value+(1<<(__builtin_ctz(value)));
+               //flip the last one
+       }
+}
+
+Constraint * generateEquivConstraint(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]=new Constraint(OR, var1[i]->clone()->negate(), var2[i]);
+               array[i*2+1]=new Constraint(OR, var1[i], var2[i]->clone()->negate());
+       }
+       return new Constraint(AND, numvars*2, array);
+}
+
+Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
+       Constraint * imp1=new Constraint(OR, var1->clone()->negate(), var2);
+       Constraint * imp2=new Constraint(OR, var1, var2->clone()->negate());
+
+       return new Constraint(AND, imp1, imp2);
+}
+
+bool mergeandfree(ModelVector<Constraint *> * to, ModelVector<Constraint *> * from) {
+       for(uint i=0;i<from->size();i++) {
+               Constraint *c=(*from)[i];
+               if (c->type==TRUE)
+                       continue;
+               if (c->type==FALSE) {
+                       for(uint j=i+1;j<from->size();j++)
+                               (*from)[j]->freerec();
+                       for(uint j=0;j<to->size();j++)
+                               (*to)[j]->freerec();
+                       to->clear();
+                       to->push_back(&ctrue);
+                       delete from;
+                       return true;
+               }
+               to->push_back(c);
+       }
+       delete from;
+       return false;
+}
+
+ModelVector<Constraint *> * Constraint::simplify() {
+       switch(type) {
+       case TRUE:
+       case VAR:
+       case NOTVAR:
+       case FALSE: {
+               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
+               vec->push_back(this);
+               return vec;
+       }
+       case AND: {
+               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
+               for(uint i=0;i<numoperandsorvar;i++) {
+                       ModelVector<Constraint *> *subvec=operands[i]->simplify();
+                       if (mergeandfree(vec, subvec)) {
+                               for(uint j=i+1;j<numoperandsorvar;j++) {
+                                       operands[j]->freerec();
+                               }
+                               this->free();
+                               return vec;
+                       }
+               }
+               this->free();
+               return vec;
+       }
+       case OR: {
+               for(uint i=0;i<numoperandsorvar;i++) {
+                       Constraint *c=operands[i];
+                       switch(c->type) {
+                       case TRUE: {
+                               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
+                               vec->push_back(c);
+                               this->freerec();
+                               return vec;
+                       }
+                       case FALSE: {
+                               Constraint *array[numoperandsorvar-1];
+                               uint index=0;
+                               for(uint j=0;j<numoperandsorvar;j++) {
+                                       if (j!=i)
+                                               array[index++]=operands[j];
+                               }
+                               Constraint *cn=new Constraint(OR, index, array);
+                               ModelVector<Constraint *> *vec=cn->simplify();
+                               this->free();
+                               return vec;
+                       }
+                       case VAR:
+                       case NOTVAR:
+                               break;
+                       case OR: {
+                               uint nsize=numoperandsorvar+c->numoperandsorvar-1;
+                               Constraint *array[nsize];
+                               uint index=0;
+                               for(uint j=0;j<numoperandsorvar;j++)
+                                       if (j!=i)
+                                               array[index++]=operands[j];
+                               for(uint j=0;j<c->numoperandsorvar;j++)
+                                       array[index++]=c->operands[j];
+                               Constraint *cn=new Constraint(OR, nsize, array);
+                               ModelVector<Constraint *> *vec=cn->simplify();
+                               this->free();
+                               c->free();
+                               return vec;
+                       }
+                       case IMPLIES: {
+                               uint nsize=numoperandsorvar+1;
+                               Constraint *array[nsize];
+                               uint index=0;
+                               for(uint j=0;j<numoperandsorvar;j++)
+                                       if (j!=i)
+                                               array[index++]=operands[j];
+                               array[index++]=c->operands[0]->negate();
+                               array[index++]=c->operands[1];
+                               Constraint *cn=new Constraint(OR, nsize, array);
+                               ModelVector<Constraint *> *vec=cn->simplify();
+                               this->free();
+                               c->free();
+                               return vec;
+                       }
+                       case AND: {
+                               Constraint *array[numoperandsorvar];
+
+                               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
+                               for(uint j=0;j<c->numoperandsorvar;j++) {
+                                       //copy other elements
+                                       for(uint k=0;k<numoperandsorvar;k++) {
+                                               if (k!=i) {
+                                                       array[k]=operands[k]->clone();
+                                               }
+                                       }
+
+                                       array[i]=c->operands[j]->clone();
+                                       Constraint *cn=new Constraint(OR, numoperandsorvar, array);
+                                       ModelVector<Constraint *> * newvec=cn->simplify();
+                                       if (mergeandfree(vec, newvec)) {
+                                               this->freerec();
+                                               return vec;
+                                       }
+                               }
+                               this->freerec();
+                               return vec;
+                       }
+                       default:
+                               ASSERT(0);
+                       }
+                       //continue on to next item
+               }
+               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
+               if (numoperandsorvar==1) {
+                       Constraint *c=operands[0];
+                       this->freerec();
+                       vec->push_back(c);
+               } else
+                       vec->push_back(this);
+               return vec;
+       }
+       case IMPLIES: {
+               Constraint *cn=new Constraint(OR, operands[0]->negate(), operands[1]);
+               ModelVector<Constraint *> *vec=cn->simplify();
+               this->free();
+               return vec;
+       }
+       default:
+               ASSERT(0);
+               return NULL;
+       }
+}
+
+Constraint * Constraint::negate() {
+       switch(type) {
+       case TRUE:
+               return &cfalse;
+       case FALSE:
+               return &ctrue;
+       case NOTVAR:
+       case VAR:
+               return this->neg;
+       case IMPLIES: {
+               Constraint *l=operands[0];
+               Constraint *r=operands[1];
+               operands[0]=r;
+               operands[1]=l;
+               return this;
+       }
+       case AND:
+       case OR: {
+               for(uint i=0;i<numoperandsorvar;i++) {
+                       operands[i]=operands[i]->negate();
+               }
+               type=(type==AND) ? OR : AND;
+               return this;
+       }
+       default:
+               ASSERT(0);
+               return NULL;
+       }
+}
diff --git a/src/constraint.cc b/src/constraint.cc
deleted file mode 100644 (file)
index c8a622a..0000000
+++ /dev/null
@@ -1,424 +0,0 @@
-/*      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);
-Constraint cfalse(FALSE);
-
-Constraint::Constraint(CType t, Constraint *l, Constraint *r) :
-       type(t),
-       numoperandsorvar(2),
-       operands((Constraint **)model_malloc(2*sizeof(Constraint *))),
-       neg(NULL)
-{
-       ASSERT(l!=NULL);
-       //if (type==IMPLIES) {
-       //type=OR;
-       //      operands[0]=l->negate();
-       //      } else {
-       operands[0]=l;
-       //      }
-       operands[1]=r;
-}
-
-Constraint::Constraint(CType t, Constraint *l) :
-       type(t),
-       numoperandsorvar(1),
-       operands((Constraint **)model_malloc(sizeof(Constraint *))),
-       neg(NULL)
-{
-       operands[0]=l;
-}
-
-Constraint::Constraint(CType t, uint num, Constraint **array) :
-       type(t),
-       numoperandsorvar(num),
-       operands((Constraint **)model_malloc(num*sizeof(Constraint *))),
-       neg(NULL)
-{
-       memcpy(operands, array, num*sizeof(Constraint *));
-}
-
-Constraint::Constraint(CType t) :
-       type(t),
-       numoperandsorvar(0xffffffff),
-       operands(NULL),
-       neg(NULL)
-{
-}
-
-Constraint::Constraint(CType t, uint v) :
-       type(t),
-       numoperandsorvar(v),
-       operands(NULL),
-       neg(NULL)
-{
-}
-
-Constraint::~Constraint() {
-       if (operands!=NULL)
-               model_free(operands);
-}
-
-void Constraint::dumpConstraint(IncrementalSolver *solver) {
-       if (type==VAR) {
-               solver->addClauseLiteral(numoperandsorvar);
-               solver->addClauseLiteral(0);
-       } else if (type==NOTVAR) {
-               solver->addClauseLiteral(-numoperandsorvar);
-               solver->addClauseLiteral(0);
-       } else {
-               ASSERT(type==OR);
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       Constraint *c=operands[i];
-                       if (c->type==VAR) {
-                               solver->addClauseLiteral(c->numoperandsorvar);
-                       } else if (c->type==NOTVAR) {
-                               solver->addClauseLiteral(-c->numoperandsorvar);
-                       } else ASSERT(0);
-               }
-               solver->addClauseLiteral(0);
-       }
-}
-
-void Constraint::free() {
-       switch(type) {
-       case TRUE:
-       case FALSE:
-       case NOTVAR:
-       case VAR:
-               return;
-       case BOGUS:
-               ASSERT(0);
-       default:
-               type=BOGUS;
-               delete this;
-       }
-}
-
-void Constraint::freerec() {
-       switch(type) {
-       case TRUE:
-       case FALSE:
-       case NOTVAR:
-       case VAR:
-               return;
-       case BOGUS:
-               ASSERT(0);
-       default:
-               if (operands!=NULL) {
-                       for(uint i=0;i<numoperandsorvar;i++)
-                               operands[i]->freerec();
-               }
-               type=BOGUS;
-               delete this;
-       }
-}
-
-
-void Constraint::print() {
-       switch(type) {
-       case TRUE:
-               model_print("true");
-               break;
-       case FALSE:
-               model_print("false");
-               break;
-       case IMPLIES:
-               model_print("(");
-               operands[0]->print();
-               model_print(")");
-               model_print("=>");
-               model_print("(");
-               operands[1]->print();
-               model_print(")");
-               break;
-       case AND:
-       case OR:
-               model_print("(");
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       if (i!=0) {
-                               if (type==AND)
-                                       model_print(" ^ ");
-                               else
-                                       model_print(" v ");
-                       }
-                       operands[i]->print();
-               }
-               model_print(")");
-               break;
-       case VAR:
-               model_print("t%u",numoperandsorvar);
-               break;
-       case NOTVAR:
-               model_print("!t%u",numoperandsorvar);
-               break;
-       default:
-               ASSERT(0);
-       }
-}
-
-Constraint * Constraint::clone() {
-       switch(type) {
-       case TRUE:
-       case FALSE:
-       case VAR:
-       case NOTVAR:
-               return this;
-       case IMPLIES:
-               return new Constraint(IMPLIES, operands[0]->clone(), operands[1]->clone());
-       case AND:
-       case OR: {
-               Constraint *array[numoperandsorvar];
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       array[i]=operands[i]->clone();
-               }
-               return new Constraint(type, 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] : vars[j]->negate();
-               value=value>>1;
-       }
-
-       return new Constraint(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++]=vars[j]->negate();
-                       val=val>>1;
-               }
-               //no ones to flip, so bail now...
-               if (ori==0) {
-                       return new Constraint(AND, andi, andarray);
-               }
-               andarray[andi++]=new Constraint(OR, ori, orarray);
-
-               value=value+(1<<(__builtin_ctz(value)));
-               //flip the last one
-       }
-}
-
-Constraint * generateEquivConstraint(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]=new Constraint(OR, var1[i]->clone()->negate(), var2[i]);
-               array[i*2+1]=new Constraint(OR, var1[i], var2[i]->clone()->negate());
-       }
-       return new Constraint(AND, numvars*2, array);
-}
-
-Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
-       Constraint * imp1=new Constraint(OR, var1->clone()->negate(), var2);
-       Constraint * imp2=new Constraint(OR, var1, var2->clone()->negate());
-
-       return new Constraint(AND, imp1, imp2);
-}
-
-bool mergeandfree(ModelVector<Constraint *> * to, ModelVector<Constraint *> * from) {
-       for(uint i=0;i<from->size();i++) {
-               Constraint *c=(*from)[i];
-               if (c->type==TRUE)
-                       continue;
-               if (c->type==FALSE) {
-                       for(uint j=i+1;j<from->size();j++)
-                               (*from)[j]->freerec();
-                       for(uint j=0;j<to->size();j++)
-                               (*to)[j]->freerec();
-                       to->clear();
-                       to->push_back(&ctrue);
-                       delete from;
-                       return true;
-               }
-               to->push_back(c);
-       }
-       delete from;
-       return false;
-}
-
-ModelVector<Constraint *> * Constraint::simplify() {
-       switch(type) {
-       case TRUE:
-       case VAR:
-       case NOTVAR:
-       case FALSE: {
-               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-               vec->push_back(this);
-               return vec;
-       }
-       case AND: {
-               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       ModelVector<Constraint *> *subvec=operands[i]->simplify();
-                       if (mergeandfree(vec, subvec)) {
-                               for(uint j=i+1;j<numoperandsorvar;j++) {
-                                       operands[j]->freerec();
-                               }
-                               this->free();
-                               return vec;
-                       }
-               }
-               this->free();
-               return vec;
-       }
-       case OR: {
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       Constraint *c=operands[i];
-                       switch(c->type) {
-                       case TRUE: {
-                               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-                               vec->push_back(c);
-                               this->freerec();
-                               return vec;
-                       }
-                       case FALSE: {
-                               Constraint *array[numoperandsorvar-1];
-                               uint index=0;
-                               for(uint j=0;j<numoperandsorvar;j++) {
-                                       if (j!=i)
-                                               array[index++]=operands[j];
-                               }
-                               Constraint *cn=new Constraint(OR, index, array);
-                               ModelVector<Constraint *> *vec=cn->simplify();
-                               this->free();
-                               return vec;
-                       }
-                       case VAR:
-                       case NOTVAR:
-                               break;
-                       case OR: {
-                               uint nsize=numoperandsorvar+c->numoperandsorvar-1;
-                               Constraint *array[nsize];
-                               uint index=0;
-                               for(uint j=0;j<numoperandsorvar;j++)
-                                       if (j!=i)
-                                               array[index++]=operands[j];
-                               for(uint j=0;j<c->numoperandsorvar;j++)
-                                       array[index++]=c->operands[j];
-                               Constraint *cn=new Constraint(OR, nsize, array);
-                               ModelVector<Constraint *> *vec=cn->simplify();
-                               this->free();
-                               c->free();
-                               return vec;
-                       }
-                       case IMPLIES: {
-                               uint nsize=numoperandsorvar+1;
-                               Constraint *array[nsize];
-                               uint index=0;
-                               for(uint j=0;j<numoperandsorvar;j++)
-                                       if (j!=i)
-                                               array[index++]=operands[j];
-                               array[index++]=c->operands[0]->negate();
-                               array[index++]=c->operands[1];
-                               Constraint *cn=new Constraint(OR, nsize, array);
-                               ModelVector<Constraint *> *vec=cn->simplify();
-                               this->free();
-                               c->free();
-                               return vec;
-                       }
-                       case AND: {
-                               Constraint *array[numoperandsorvar];
-
-                               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-                               for(uint j=0;j<c->numoperandsorvar;j++) {
-                                       //copy other elements
-                                       for(uint k=0;k<numoperandsorvar;k++) {
-                                               if (k!=i) {
-                                                       array[k]=operands[k]->clone();
-                                               }
-                                       }
-
-                                       array[i]=c->operands[j]->clone();
-                                       Constraint *cn=new Constraint(OR, numoperandsorvar, array);
-                                       ModelVector<Constraint *> * newvec=cn->simplify();
-                                       if (mergeandfree(vec, newvec)) {
-                                               this->freerec();
-                                               return vec;
-                                       }
-                               }
-                               this->freerec();
-                               return vec;
-                       }
-                       default:
-                               ASSERT(0);
-                       }
-                       //continue on to next item
-               }
-               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-               if (numoperandsorvar==1) {
-                       Constraint *c=operands[0];
-                       this->freerec();
-                       vec->push_back(c);
-               } else
-                       vec->push_back(this);
-               return vec;
-       }
-       case IMPLIES: {
-               Constraint *cn=new Constraint(OR, operands[0]->negate(), operands[1]);
-               ModelVector<Constraint *> *vec=cn->simplify();
-               this->free();
-               return vec;
-       }
-       default:
-               ASSERT(0);
-               return NULL;
-       }
-}
-
-Constraint * Constraint::negate() {
-       switch(type) {
-       case TRUE:
-               return &cfalse;
-       case FALSE:
-               return &ctrue;
-       case NOTVAR:
-       case VAR:
-               return this->neg;
-       case IMPLIES: {
-               Constraint *l=operands[0];
-               Constraint *r=operands[1];
-               operands[0]=r;
-               operands[1]=l;
-               return this;
-       }
-       case AND:
-       case OR: {
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       operands[i]=operands[i]->negate();
-               }
-               type=(type==AND) ? OR : AND;
-               return this;
-       }
-       default:
-               ASSERT(0);
-               return NULL;
-       }
-}
diff --git a/src/csolver.c b/src/csolver.c
new file mode 100644 (file)
index 0000000..20e729a
--- /dev/null
@@ -0,0 +1,65 @@
+#include "csolver.h"
+
+CSolver * allocCSolver() {
+       CSolver * tmp=(CSolver *) ourmalloc(sizeof(CSolver));
+       tmp->constraint=allocVector();
+       return tmp;
+}
+
+Set * createSet(CSolver * solver, Type type, uint64_t ** elements) {
+       
+}
+
+Set * createSet(CSolver * solver, Type type, uint64_t lowrange, uint64_t highrange) {
+}
+
+MutableSet * createMutableSet(CSolver * solver, Type type) {
+}
+
+void CSolver::addItem(MutableSet * set, uint64_t element) {
+}
+
+int64_t CSolver::createUniqueItem(MutableSet * set) {
+}
+
+Element * CSolver::getElementVar(Set * set) {
+}
+
+Boolean * CSolver::getBooleanVar() {
+}
+
+Function * CSolver::createFunctionOperator(enum ArithOp op, Set ** domain, Set * range, enum OverFlowBehavior overflowbehavior, Boolean * overflowstatus) {
+}
+
+Function * CSolver::createFunctionOperator(enum ArithOp op) {
+}
+
+Predicate * CSolver::createPredicateOperator(enum CompOp op, Set ** domain) {
+}
+
+Table * CSolver::createTable(Set **domains, Set * range) {
+}
+
+void CSolver::addTableEntry(Element ** inputs, Element *result) {
+}
+
+Function * CSolver::completeTable(struct Table *) {
+}
+
+Element * CSolver::applyFunction(Function * function, Element ** array) {
+}
+
+Boolean * CSolver::applyPredicate(Predicate * predicate, Element ** inputs) {
+}
+
+Boolean * CSolver::applyLogicalOperation(enum LogicOp op, Boolean ** array) {
+}
+
+void CSolver::addBoolean(Boolean * constraint) {
+}
+
+Order * CSolver::createOrder(enum OrderType type, Set * set) {
+}
+
+Boolean * CSolver::orderedConstraint(Order * order, uint64_t first, uint64_t second) {
+}
diff --git a/src/element.c b/src/element.c
new file mode 100644 (file)
index 0000000..2b9d1e1
--- /dev/null
@@ -0,0 +1,5 @@
+#include "element.h"
+
+Element::Element(Set * s) :
+       set(s) {
+}
diff --git a/src/element.cc b/src/element.cc
deleted file mode 100644 (file)
index 2b9d1e1..0000000
+++ /dev/null
@@ -1,5 +0,0 @@
-#include "element.h"
-
-Element::Element(Set * s) :
-       set(s) {
-}
diff --git a/src/function.c b/src/function.c
new file mode 100644 (file)
index 0000000..d4b693e
--- /dev/null
@@ -0,0 +1 @@
+#include "function.h"
diff --git a/src/function.cc b/src/function.cc
deleted file mode 100644 (file)
index d4b693e..0000000
+++ /dev/null
@@ -1 +0,0 @@
-#include "function.h"
diff --git a/src/inc_solver.c b/src/inc_solver.c
new file mode 100644 (file)
index 0000000..97f050c
--- /dev/null
@@ -0,0 +1,164 @@
+/*      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>
+
+IncrementalSolver::IncrementalSolver() :
+       buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
+       solution(NULL),
+       solutionsize(0),
+       offset(0)
+{
+       createSolver();
+}
+
+IncrementalSolver::~IncrementalSolver() {
+       killSolver();
+       model_free(buffer);
+       if (solution != NULL)
+               model_free(solution);
+}
+
+void IncrementalSolver::reset() {
+       killSolver();
+       offset = 0;
+       createSolver();
+}
+
+void IncrementalSolver::addClauseLiteral(int literal) {
+       buffer[offset++]=literal;
+       if (offset==IS_BUFFERSIZE) {
+               flushBuffer();
+       }
+}
+
+void IncrementalSolver::finishedClauses() {
+       addClauseLiteral(0);
+}
+
+void IncrementalSolver::freeze(int variable) {
+       addClauseLiteral(IS_FREEZE);
+       addClauseLiteral(variable);
+}
+
+int IncrementalSolver::solve() {
+       //add an empty clause
+       startSolve();
+       return getSolution();
+}
+
+
+void IncrementalSolver::startSolve() {
+       addClauseLiteral(IS_RUNSOLVER);
+       flushBuffer();
+}
+
+int IncrementalSolver::getSolution() {
+       int result=readIntSolver();
+       if (result == IS_SAT) {
+               int numVars=readIntSolver();
+               if (numVars > solutionsize) {
+                       if (solution != NULL)
+                               model_free(solution);
+                       solution = (int *) model_malloc((numVars+1)*sizeof(int));
+                       solution[0] = 0;
+               }
+               readSolver(&solution[1], numVars * sizeof(int));
+       }
+       return result;
+}
+
+int IncrementalSolver::readIntSolver() {
+       int value;
+       readSolver(&value, 4);
+       return value;
+}
+
+void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
+       char *result = (char *) tmp;
+       ssize_t bytestoread=size;
+       ssize_t bytesread=0;
+       do {
+               ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
+               if (n == -1) {
+                       model_print("Read failure\n");
+                       exit(-1);
+               }
+               bytestoread -= n;
+               bytesread += n;
+       } while(bytestoread != 0);
+}
+
+bool IncrementalSolver::getValue(int variable) {
+       return solution[variable];
+}
+
+void IncrementalSolver::createSolver() {
+       int to_pipe[2];
+       int from_pipe[2];
+       if (pipe(to_pipe) || pipe(from_pipe)) {
+               model_print("Error creating pipe.\n");
+               exit(-1);
+       }
+       if ((solver_pid = fork()) == -1) {
+               model_print("Error forking.\n");
+               exit(-1);
+       }
+       if (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
+               to_solver_fd = to_pipe[1];
+               from_solver_fd = from_pipe[0];
+               close(to_pipe[0]);
+               close(from_pipe[1]);
+       }
+}
+
+void IncrementalSolver::killSolver() {
+       close(to_solver_fd);
+       close(from_solver_fd);
+       //Stop the solver
+       if (solver_pid > 0) {
+               int status;
+               kill(solver_pid, SIGKILL);
+               waitpid(solver_pid, &status, 0);
+       }
+}
+
+void IncrementalSolver::flushBuffer() {
+       ssize_t bytestowrite=sizeof(int)*offset;
+       ssize_t byteswritten=0;
+       do {
+               ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
+               if (n == -1) {
+                       perror("Write failure\n");
+                       model_print("to_solver_fd=%d\n",to_solver_fd);
+                       exit(-1);
+               }
+               bytestowrite -= n;
+               byteswritten += n;
+       } while(bytestowrite != 0);
+       offset = 0;
+}
diff --git a/src/inc_solver.cc b/src/inc_solver.cc
deleted file mode 100644 (file)
index 97f050c..0000000
+++ /dev/null
@@ -1,164 +0,0 @@
-/*      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>
-
-IncrementalSolver::IncrementalSolver() :
-       buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
-       solution(NULL),
-       solutionsize(0),
-       offset(0)
-{
-       createSolver();
-}
-
-IncrementalSolver::~IncrementalSolver() {
-       killSolver();
-       model_free(buffer);
-       if (solution != NULL)
-               model_free(solution);
-}
-
-void IncrementalSolver::reset() {
-       killSolver();
-       offset = 0;
-       createSolver();
-}
-
-void IncrementalSolver::addClauseLiteral(int literal) {
-       buffer[offset++]=literal;
-       if (offset==IS_BUFFERSIZE) {
-               flushBuffer();
-       }
-}
-
-void IncrementalSolver::finishedClauses() {
-       addClauseLiteral(0);
-}
-
-void IncrementalSolver::freeze(int variable) {
-       addClauseLiteral(IS_FREEZE);
-       addClauseLiteral(variable);
-}
-
-int IncrementalSolver::solve() {
-       //add an empty clause
-       startSolve();
-       return getSolution();
-}
-
-
-void IncrementalSolver::startSolve() {
-       addClauseLiteral(IS_RUNSOLVER);
-       flushBuffer();
-}
-
-int IncrementalSolver::getSolution() {
-       int result=readIntSolver();
-       if (result == IS_SAT) {
-               int numVars=readIntSolver();
-               if (numVars > solutionsize) {
-                       if (solution != NULL)
-                               model_free(solution);
-                       solution = (int *) model_malloc((numVars+1)*sizeof(int));
-                       solution[0] = 0;
-               }
-               readSolver(&solution[1], numVars * sizeof(int));
-       }
-       return result;
-}
-
-int IncrementalSolver::readIntSolver() {
-       int value;
-       readSolver(&value, 4);
-       return value;
-}
-
-void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
-       char *result = (char *) tmp;
-       ssize_t bytestoread=size;
-       ssize_t bytesread=0;
-       do {
-               ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
-               if (n == -1) {
-                       model_print("Read failure\n");
-                       exit(-1);
-               }
-               bytestoread -= n;
-               bytesread += n;
-       } while(bytestoread != 0);
-}
-
-bool IncrementalSolver::getValue(int variable) {
-       return solution[variable];
-}
-
-void IncrementalSolver::createSolver() {
-       int to_pipe[2];
-       int from_pipe[2];
-       if (pipe(to_pipe) || pipe(from_pipe)) {
-               model_print("Error creating pipe.\n");
-               exit(-1);
-       }
-       if ((solver_pid = fork()) == -1) {
-               model_print("Error forking.\n");
-               exit(-1);
-       }
-       if (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
-               to_solver_fd = to_pipe[1];
-               from_solver_fd = from_pipe[0];
-               close(to_pipe[0]);
-               close(from_pipe[1]);
-       }
-}
-
-void IncrementalSolver::killSolver() {
-       close(to_solver_fd);
-       close(from_solver_fd);
-       //Stop the solver
-       if (solver_pid > 0) {
-               int status;
-               kill(solver_pid, SIGKILL);
-               waitpid(solver_pid, &status, 0);
-       }
-}
-
-void IncrementalSolver::flushBuffer() {
-       ssize_t bytestowrite=sizeof(int)*offset;
-       ssize_t byteswritten=0;
-       do {
-               ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
-               if (n == -1) {
-                       perror("Write failure\n");
-                       model_print("to_solver_fd=%d\n",to_solver_fd);
-                       exit(-1);
-               }
-               bytestowrite -= n;
-               byteswritten += n;
-       } while(bytestowrite != 0);
-       offset = 0;
-}
diff --git a/src/mutableset.c b/src/mutableset.c
new file mode 100644 (file)
index 0000000..76bb779
--- /dev/null
@@ -0,0 +1,2 @@
+#include "mutableset.h"
+
diff --git a/src/mutableset.cc b/src/mutableset.cc
deleted file mode 100644 (file)
index 76bb779..0000000
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "mutableset.h"
-
index aabb169..d55c138 100644 (file)
@@ -13,7 +13,7 @@
 
 #ifndef _MY_MEMORY_H
 #define _MY_MEMORY_H
-#include <limits>
+#include <limits.h>
 #include <stddef.h>
 #include <stdlib.h>
 
diff --git a/src/order.c b/src/order.c
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/src/order.cc b/src/order.cc
deleted file mode 100644 (file)
index e69de29..0000000
diff --git a/src/predicate.c b/src/predicate.c
new file mode 100644 (file)
index 0000000..dcec97a
--- /dev/null
@@ -0,0 +1 @@
+#include "predicate.h"
diff --git a/src/predicate.cc b/src/predicate.cc
deleted file mode 100644 (file)
index dcec97a..0000000
+++ /dev/null
@@ -1 +0,0 @@
-#include "predicate.h"
diff --git a/src/set.c b/src/set.c
new file mode 100644 (file)
index 0000000..043aece
--- /dev/null
+++ b/src/set.c
@@ -0,0 +1,27 @@
+#include "set.h"
+#include <stddef.h>
+#include <cassert>
+
+Set::Set(VarType t, uint64_t* elements, int num) :
+       type (t),
+       isRange(false),
+       low(0),
+       high(0),
+       members(new ModelVector<uint64_t>()) {
+       members->reserve(num);
+       for(int i=0;i<num;i++)
+               members->push_back(elements[i]);
+}
+
+Set::Set(VarType t, uint64_t lowrange, uint64_t highrange) :
+       type(t),
+       isRange(true),
+       low(lowrange),
+       high(highrange),
+       members(NULL) {
+}
+
+Set::~Set() {
+       if (isRange)
+               delete members;
+}
diff --git a/src/set.cc b/src/set.cc
deleted file mode 100644 (file)
index 043aece..0000000
+++ /dev/null
@@ -1,27 +0,0 @@
-#include "set.h"
-#include <stddef.h>
-#include <cassert>
-
-Set::Set(VarType t, uint64_t* elements, int num) :
-       type (t),
-       isRange(false),
-       low(0),
-       high(0),
-       members(new ModelVector<uint64_t>()) {
-       members->reserve(num);
-       for(int i=0;i<num;i++)
-               members->push_back(elements[i]);
-}
-
-Set::Set(VarType t, uint64_t lowrange, uint64_t highrange) :
-       type(t),
-       isRange(true),
-       low(lowrange),
-       high(highrange),
-       members(NULL) {
-}
-
-Set::~Set() {
-       if (isRange)
-               delete members;
-}
diff --git a/src/table.c b/src/table.c
new file mode 100644 (file)
index 0000000..e89d72a
--- /dev/null
@@ -0,0 +1 @@
+#include "table.h"
diff --git a/src/table.cc b/src/table.cc
deleted file mode 100644 (file)
index e89d72a..0000000
+++ /dev/null
@@ -1 +0,0 @@
-#include "table.h"