--- /dev/null
+#include "boolean.h"
+++ /dev/null
-#include "boolean.h"
#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;
--- /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);
+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;
+ }
+}
+++ /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);
-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;
- }
-}
--- /dev/null
+#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) {
+}
--- /dev/null
+#include "element.h"
+
+Element::Element(Set * s) :
+ set(s) {
+}
+++ /dev/null
-#include "element.h"
-
-Element::Element(Set * s) :
- set(s) {
-}
--- /dev/null
+#include "function.h"
+++ /dev/null
-#include "function.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>
+
+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;
+}
+++ /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>
-
-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;
-}
--- /dev/null
+#include "mutableset.h"
+
+++ /dev/null
-#include "mutableset.h"
-
#ifndef _MY_MEMORY_H
#define _MY_MEMORY_H
-#include <limits>
+#include <limits.h>
#include <stddef.h>
#include <stdlib.h>
--- /dev/null
+#include "predicate.h"
+++ /dev/null
-#include "predicate.h"
--- /dev/null
+#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;
+}
+++ /dev/null
-#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;
-}
--- /dev/null
+#include "table.h"
+++ /dev/null
-#include "table.h"
projects / satune.git / commitdiff