From: bdemsky <bdemsky@uci.edu>
Date: Wed, 14 Jun 2017 22:44:45 +0000 (-0700)
Subject: Switch to C for Zach
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=8828582606732da9cc5396dd5a28c01d20ef4325;p=satune.git

Switch to C for Zach
---

diff --git a/src/boolean.c b/src/boolean.c
new file mode 100644
index 0000000..13070fa
--- /dev/null
+++ b/src/boolean.c
@@ -0,0 +1 @@
+#include "boolean.h"
diff --git a/src/boolean.cc b/src/boolean.cc
deleted file mode 100644
index 13070fa..0000000
--- a/src/boolean.cc
+++ /dev/null
@@ -1 +0,0 @@
-#include "boolean.h"
diff --git a/src/classlist.h b/src/classlist.h
index 4c48778..53555ed 100644
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -13,16 +13,34 @@
 #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
index 0000000..c8a622a
--- /dev/null
+++ b/src/constraint.c
@@ -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
index c8a622a..0000000
--- a/src/constraint.cc
+++ /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
index 0000000..20e729a
--- /dev/null
+++ b/src/csolver.c
@@ -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
index 0000000..2b9d1e1
--- /dev/null
+++ b/src/element.c
@@ -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
index 2b9d1e1..0000000
--- a/src/element.cc
+++ /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
index 0000000..d4b693e
--- /dev/null
+++ b/src/function.c
@@ -0,0 +1 @@
+#include "function.h"
diff --git a/src/function.cc b/src/function.cc
deleted file mode 100644
index d4b693e..0000000
--- a/src/function.cc
+++ /dev/null
@@ -1 +0,0 @@
-#include "function.h"
diff --git a/src/inc_solver.c b/src/inc_solver.c
new file mode 100644
index 0000000..97f050c
--- /dev/null
+++ b/src/inc_solver.c
@@ -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
index 97f050c..0000000
--- a/src/inc_solver.cc
+++ /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
index 0000000..76bb779
--- /dev/null
+++ b/src/mutableset.c
@@ -0,0 +1,2 @@
+#include "mutableset.h"
+
diff --git a/src/mutableset.cc b/src/mutableset.cc
deleted file mode 100644
index 76bb779..0000000
--- a/src/mutableset.cc
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "mutableset.h"
-
diff --git a/src/mymemory.h b/src/mymemory.h
index aabb169..d55c138 100644
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -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
index 0000000..e69de29
diff --git a/src/order.cc b/src/order.cc
deleted file mode 100644
index e69de29..0000000
diff --git a/src/predicate.c b/src/predicate.c
new file mode 100644
index 0000000..dcec97a
--- /dev/null
+++ b/src/predicate.c
@@ -0,0 +1 @@
+#include "predicate.h"
diff --git a/src/predicate.cc b/src/predicate.cc
deleted file mode 100644
index dcec97a..0000000
--- a/src/predicate.cc
+++ /dev/null
@@ -1 +0,0 @@
-#include "predicate.h"
diff --git a/src/set.c b/src/set.c
new file mode 100644
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
index 043aece..0000000
--- a/src/set.cc
+++ /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
index 0000000..e89d72a
--- /dev/null
+++ b/src/table.c
@@ -0,0 +1 @@
+#include "table.h"
diff --git a/src/table.cc b/src/table.cc
deleted file mode 100644
index e89d72a..0000000
--- a/src/table.cc
+++ /dev/null
@@ -1 +0,0 @@
-#include "table.h"