Convert constraint.c to C

diff --git a/src/Makefile b/src/Makefile
index 5694fe2f52e6dfb51bccb35fc4c981c5c8fefdc6..c9d26123475cee1fbe4b69838db7ee38ec30f575 100644 (file)
--- a/src/Makefile
+++ b/src/Makefile
@@ -4,7 +4,7 @@ PHONY += directories
 MKDIR_P = mkdir -p
 OBJ_DIR = bin
 
 MKDIR_P = mkdir -p
 OBJ_DIR = bin
 

-C_SOURCES := set.c mutableset.c element.c function.c order.c table.c predicate.c boolean.c csolver.c structs.c
+C_SOURCES := set.c mutableset.c element.c function.c order.c table.c predicate.c boolean.c csolver.c structs.c constraint.c

 
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 
 
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 

diff --git a/src/constraint.c b/src/constraint.c
index c8a622a3296248b357a8638d45fa96709979bcba..be7c73c884ce5a4ec4e4fe61417f89c5ef77399b 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -9,77 +9,73 @@
 
 #include "constraint.h"
 #include "mymemory.h"
 
 #include "constraint.h"
 #include "mymemory.h"

-#include "inc_solver.h"
+//#include "inc_solver.h"

 
 

-Constraint ctrue(TRUE);
-Constraint cfalse(FALSE);
+Constraint ctrue={TRUE, 0xffffffff, NULL, NULL};
+Constraint cfalse={FALSE, 0xffffffff, NULL, NULL};

 
 

-Constraint::Constraint(CType t, Constraint *l, Constraint *r) :
-       type(t),
-       numoperandsorvar(2),
-       operands((Constraint **)model_malloc(2*sizeof(Constraint *))),
-       neg(NULL)
-{
+Constraint * allocConstraint(CType t, Constraint *l, Constraint *r) {
+       Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint));
+       this->type=t;
+       this->numoperandsorvar=2;
+       this->operands=(Constraint **)ourmalloc(2*sizeof(Constraint *));
+       this->neg=NULL;

        ASSERT(l!=NULL);
        //if (type==IMPLIES) {
        //type=OR;
        //      operands[0]=l->negate();
        //      } else {
        ASSERT(l!=NULL);
        //if (type==IMPLIES) {
        //type=OR;
        //      operands[0]=l->negate();
        //      } else {

-       operands[0]=l;
+       this->operands[0]=l;

        //      }
        //      }

-       operands[1]=r;
+       this->operands[1]=r;
+       return this;

 }
 
 }
 

-Constraint::Constraint(CType t, Constraint *l) :
-       type(t),
-       numoperandsorvar(1),
-       operands((Constraint **)model_malloc(sizeof(Constraint *))),
-       neg(NULL)
-{
-       operands[0]=l;
+Constraint * allocUnaryConstraint(CType t, Constraint *l) {
+       Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint));
+       this->type=t;
+       this->numoperandsorvar=1;
+       this->operands=(Constraint **) ourmalloc(sizeof(Constraint *));
+       this->neg=NULL;
+       this->operands[0]=l;
+       return this;

 }
 
 }
 

-Constraint::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 * allocArrayConstraint(CType t, uint num, Constraint **array) {
+       Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint));
+       this->type=t;
+       this->numoperandsorvar=num;
+       this->operands=(Constraint **) ourmalloc(num*sizeof(Constraint *));
+       this->neg=NULL;
+       memcpy(this->operands, array, num*sizeof(Constraint *));
+       return this;

 }
 
 }
 

-Constraint::Constraint(CType t) :
-       type(t),
-       numoperandsorvar(0xffffffff),
-       operands(NULL),
-       neg(NULL)
-{
+Constraint * allocVarConstraint(CType t, uint v) {
+       Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint));
+       this->type=t;
+       this->numoperandsorvar=v;
+       this->operands=NULL;
+       this->neg=NULL;
+       return this;

 }
 
 }
 

-Constraint::Constraint(CType t, uint v) :
-       type(t),
-       numoperandsorvar(v),
-       operands(NULL),
-       neg(NULL)
-{
+void freeConstraint(Constraint *this) {
+       if (this->operands!=NULL)
+               ourfree(this->operands);

 }
 
 }
 

-Constraint::~Constraint() {
-       if (operands!=NULL)
-               model_free(operands);
-}
-
-void Constraint::dumpConstraint(IncrementalSolver *solver) {
-       if (type==VAR) {
-               solver->addClauseLiteral(numoperandsorvar);
+/*void dumpConstraint(Constraint * this, IncrementalSolver *solver) {
+       if (this->type==VAR) {
+               solver->addClauseLiteral(this->numoperandsorvar);

                solver->addClauseLiteral(0);
                solver->addClauseLiteral(0);

-       } else if (type==NOTVAR) {
-               solver->addClauseLiteral(-numoperandsorvar);
+       } else if (this->type==NOTVAR) {
+               solver->addClauseLiteral(-this->numoperandsorvar);

                solver->addClauseLiteral(0);
        } else {
                solver->addClauseLiteral(0);
        } else {

-               ASSERT(type==OR);
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       Constraint *c=operands[i];
+               ASSERT(this->type==OR);
+               for(uint i=0;i<this->numoperandsorvar;i++) {
+                       Constraint *c=this->operands[i];

                        if (c->type==VAR) {
                                solver->addClauseLiteral(c->numoperandsorvar);
                        } else if (c->type==NOTVAR) {
                        if (c->type==VAR) {
                                solver->addClauseLiteral(c->numoperandsorvar);
                        } else if (c->type==NOTVAR) {


@@ -88,10 +84,10 @@ void Constraint::dumpConstraint(IncrementalSolver *solver) {
                }
                solver->addClauseLiteral(0);
        }
                }
                solver->addClauseLiteral(0);
        }

-}
+       }*/

 
 

-void Constraint::free() {
-       switch(type) {
+void internalfreeConstraint(Constraint * this) {
+       switch(this->type) {

        case TRUE:
        case FALSE:
        case NOTVAR:
        case TRUE:
        case FALSE:
        case NOTVAR:


@@ -100,13 +96,13 @@ void Constraint::free() {
        case BOGUS:
                ASSERT(0);
        default:
        case BOGUS:
                ASSERT(0);
        default:

-               type=BOGUS;
-               delete this;
+               this->type=BOGUS;
+               ourfree(this);

        }
 }
 
        }
 }
 

-void Constraint::freerec() {
-       switch(type) {
+void freerecConstraint(Constraint *this) {
+       switch(this->type) {

        case TRUE:
        case FALSE:
        case NOTVAR:
        case TRUE:
        case FALSE:
        case NOTVAR:


@@ -115,18 +111,18 @@ void Constraint::freerec() {
        case BOGUS:
                ASSERT(0);
        default:
        case BOGUS:
                ASSERT(0);
        default:

-               if (operands!=NULL) {
-                       for(uint i=0;i<numoperandsorvar;i++)
-                               operands[i]->freerec();
+               if (this->operands!=NULL) {
+                       for(uint i=0;i<this->numoperandsorvar;i++)
+                               freerecConstraint(this->operands[i]);

                }
                }

-               type=BOGUS;
-               delete this;
+               this->type=BOGUS;
+               freeConstraint(this);

        }
 }
 
 
        }
 }
 
 

-void Constraint::print() {
-       switch(type) {
+void printConstraint(Constraint * this) {
+       switch(this->type) {

        case TRUE:
                model_print("true");
                break;
        case TRUE:
                model_print("true");
                break;


@@ -135,54 +131,54 @@ void Constraint::print() {
                break;
        case IMPLIES:
                model_print("(");
                break;
        case IMPLIES:
                model_print("(");

-               operands[0]->print();
+               printConstraint(this->operands[0]);

                model_print(")");
                model_print("=>");
                model_print("(");
                model_print(")");
                model_print("=>");
                model_print("(");

-               operands[1]->print();
+               printConstraint(this->operands[1]);

                model_print(")");
                break;
        case AND:
        case OR:
                model_print("(");
                model_print(")");
                break;
        case AND:
        case OR:
                model_print("(");

-               for(uint i=0;i<numoperandsorvar;i++) {
+               for(uint i=0;i<this->numoperandsorvar;i++) {

                        if (i!=0) {
                        if (i!=0) {

-                               if (type==AND)
+                               if (this->type==AND)

                                        model_print(" ^ ");
                                else
                                        model_print(" v ");
                        }
                                        model_print(" ^ ");
                                else
                                        model_print(" v ");
                        }

-                       operands[i]->print();
+                       printConstraint(this->operands[i]);

                }
                model_print(")");
                break;
        case VAR:
                }
                model_print(")");
                break;
        case VAR:

-               model_print("t%u",numoperandsorvar);
+               model_print("t%u",this->numoperandsorvar);

                break;
        case NOTVAR:
                break;
        case NOTVAR:

-               model_print("!t%u",numoperandsorvar);
+               model_print("!t%u",this->numoperandsorvar);

                break;
        default:
                ASSERT(0);
        }
 }
 
                break;
        default:
                ASSERT(0);
        }
 }
 

-Constraint * Constraint::clone() {
-       switch(type) {
+Constraint * cloneConstraint(Constraint * this) {
+       switch(this->type) {

        case TRUE:
        case FALSE:
        case VAR:
        case NOTVAR:
                return this;
        case IMPLIES:
        case TRUE:
        case FALSE:
        case VAR:
        case NOTVAR:
                return this;
        case IMPLIES:

-               return new Constraint(IMPLIES, operands[0]->clone(), operands[1]->clone());
+               return allocConstraint(IMPLIES, cloneConstraint(this->operands[0]), cloneConstraint(this->operands[1]));

        case AND:
        case OR: {
        case AND:
        case OR: {

-               Constraint *array[numoperandsorvar];
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       array[i]=operands[i]->clone();
+               Constraint *array[this->numoperandsorvar];
+               for(uint i=0;i<this->numoperandsorvar;i++) {
+                       array[i]=cloneConstraint(this->operands[i]);

                }
                }

-               return new Constraint(type, numoperandsorvar, array);
+               return allocArrayConstraint(this->type, this->numoperandsorvar, array);

        }
        default:
                ASSERT(0);
        }
        default:
                ASSERT(0);


@@ -193,11 +189,11 @@ Constraint * Constraint::clone() {
 Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value) {
        Constraint *carray[numvars];
        for(uint j=0;j<numvars;j++) {
 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();
+               carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);

                value=value>>1;
        }
 
                value=value>>1;
        }
 

-       return new Constraint(AND, numvars, carray);
+       return allocArrayConstraint(AND, numvars, carray);

 }
 
 /** Generates a constraint to ensure that all encodings are less than value */
 }
 
 /** Generates a constraint to ensure that all encodings are less than value */


@@ -211,160 +207,160 @@ Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value)
                uint ori=0;
                for(uint j=0;j<numvars;j++) {
                        if ((val&1)==1)
                uint ori=0;
                for(uint j=0;j<numvars;j++) {
                        if ((val&1)==1)

-                               orarray[ori++]=vars[j]->negate();
+                               orarray[ori++]=negateConstraint(vars[j]);

                        val=val>>1;
                }
                //no ones to flip, so bail now...
                if (ori==0) {
                        val=val>>1;
                }
                //no ones to flip, so bail now...
                if (ori==0) {

-                       return new Constraint(AND, andi, andarray);
+                       return allocArrayConstraint(AND, andi, andarray);

                }
                }

-               andarray[andi++]=new Constraint(OR, ori, orarray);
+               andarray[andi++]=allocArrayConstraint(OR, ori, orarray);

 
                value=value+(1<<(__builtin_ctz(value)));
                //flip the last one
        }
 }
 
 
                value=value+(1<<(__builtin_ctz(value)));
                //flip the last one
        }
 }
 

-Constraint * generateEquivConstraint(uint numvars, Constraint **var1, Constraint **var2) {
+Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) {

        if (numvars==0)
                return &ctrue;
        Constraint *array[numvars*2];
        for(uint i=0;i<numvars;i++) {
        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());
+               array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
+               array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));

        }
        }

-       return new Constraint(AND, numvars*2, array);
+       return allocArrayConstraint(AND, numvars*2, array);

 }
 
 Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
 }
 
 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);
+       Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2);
+       Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2)));
+                                                                                                                                               
+       return allocConstraint(AND, imp1, imp2);

 }
 
 }
 

-bool mergeandfree(ModelVector<Constraint *> * to, ModelVector<Constraint *> * from) {
-       for(uint i=0;i<from->size();i++) {
-               Constraint *c=(*from)[i];
+bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
+       for(uint i=0;i<getSizeVectorConstraint(from);i++) {
+               Constraint *c=getVectorConstraint(from, i);

                if (c->type==TRUE)
                        continue;
                if (c->type==FALSE) {
                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;
+                       for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
+                               freerecConstraint(getVectorConstraint(from,j));
+                       for(uint j=0;j<getSizeVectorConstraint(to);j++)
+                               freerecConstraint(getVectorConstraint(to, j));
+                       clearVectorConstraint(to);
+                       pushVectorConstraint(to, &ctrue);
+                       freeVectorConstraint(from);

                        return true;
                }
                        return true;
                }

-               to->push_back(c);
+               pushVectorConstraint(to, c);

        }
        }

-       delete from;
+       freeVectorConstraint(from);

        return false;
 }
 
        return false;
 }
 

-ModelVector<Constraint *> * Constraint::simplify() {
-       switch(type) {
+VectorConstraint * simplifyConstraint(Constraint * this) {
+       switch(this->type) {

        case TRUE:
        case VAR:
        case NOTVAR:
        case FALSE: {
        case TRUE:
        case VAR:
        case NOTVAR:
        case FALSE: {

-               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-               vec->push_back(this);
+               VectorConstraint * vec=allocDefVectorConstraint();
+               pushVectorConstraint(vec, this);

                return vec;
        }
        case AND: {
                return vec;
        }
        case AND: {

-               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-               for(uint i=0;i<numoperandsorvar;i++) {
-                       ModelVector<Constraint *> *subvec=operands[i]->simplify();
+               VectorConstraint *vec=allocDefVectorConstraint();
+               for(uint i=0;i<this->numoperandsorvar;i++) {
+                       VectorConstraint * subvec=simplifyConstraint(this->operands[i]);

                        if (mergeandfree(vec, subvec)) {
                        if (mergeandfree(vec, subvec)) {

-                               for(uint j=i+1;j<numoperandsorvar;j++) {
-                                       operands[j]->freerec();
+                               for(uint j=i+1;j<this->numoperandsorvar;j++) {
+                                       freerecConstraint(this->operands[j]);

                                }
                                }

-                               this->free();
+                               internalfreeConstraint(this);

                                return vec;
                        }
                }
                                return vec;
                        }
                }

-               this->free();
+               internalfreeConstraint(this);

                return vec;
        }
        case OR: {
                return vec;
        }
        case OR: {

-               for(uint i=0;i<numoperandsorvar;i++) {
-                       Constraint *c=operands[i];
+               for(uint i=0;i<this->numoperandsorvar;i++) {
+                       Constraint *c=this->operands[i];

                        switch(c->type) {
                        case TRUE: {
                        switch(c->type) {
                        case TRUE: {

-                               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-                               vec->push_back(c);
-                               this->freerec();
+                               VectorConstraint * vec=allocDefVectorConstraint();
+                               pushVectorConstraint(vec, c);
+                               freerecConstraint(this);

                                return vec;
                        }
                        case FALSE: {
                                return vec;
                        }
                        case FALSE: {

-                               Constraint *array[numoperandsorvar-1];
+                               Constraint *array[this->numoperandsorvar-1];

                                uint index=0;
                                uint index=0;

-                               for(uint j=0;j<numoperandsorvar;j++) {
+                               for(uint j=0;j<this->numoperandsorvar;j++) {

                                        if (j!=i)
                                        if (j!=i)

-                                               array[index++]=operands[j];
+                                               array[index++]=this->operands[j];

                                }
                                }

-                               Constraint *cn=new Constraint(OR, index, array);
-                               ModelVector<Constraint *> *vec=cn->simplify();
-                               this->free();
+                               Constraint *cn=allocArrayConstraint(OR, index, array);
+                               VectorConstraint *vec=simplifyConstraint(cn);
+                               internalfreeConstraint(this);

                                return vec;
                        }
                        case VAR:
                        case NOTVAR:
                                break;
                        case OR: {
                                return vec;
                        }
                        case VAR:
                        case NOTVAR:
                                break;
                        case OR: {

-                               uint nsize=numoperandsorvar+c->numoperandsorvar-1;
+                               uint nsize=this->numoperandsorvar+c->numoperandsorvar-1;

                                Constraint *array[nsize];
                                uint index=0;
                                Constraint *array[nsize];
                                uint index=0;

-                               for(uint j=0;j<numoperandsorvar;j++)
+                               for(uint j=0;j<this->numoperandsorvar;j++)

                                        if (j!=i)
                                        if (j!=i)

-                                               array[index++]=operands[j];
+                                               array[index++]=this->operands[j];

                                for(uint j=0;j<c->numoperandsorvar;j++)
                                        array[index++]=c->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();
+                               Constraint *cn=allocArrayConstraint(OR, nsize, array);
+                               VectorConstraint *vec=simplifyConstraint(cn);
+                               internalfreeConstraint(this);
+                               internalfreeConstraint(c);

                                return vec;
                        }
                        case IMPLIES: {
                                return vec;
                        }
                        case IMPLIES: {

-                               uint nsize=numoperandsorvar+1;
+                               uint nsize=this->numoperandsorvar+1;

                                Constraint *array[nsize];
                                uint index=0;
                                Constraint *array[nsize];
                                uint index=0;

-                               for(uint j=0;j<numoperandsorvar;j++)
+                               for(uint j=0;j<this->numoperandsorvar;j++)

                                        if (j!=i)
                                        if (j!=i)

-                                               array[index++]=operands[j];
-                               array[index++]=c->operands[0]->negate();
+                                               array[index++]=this->operands[j];
+                               array[index++]=negateConstraint(c->operands[0]);

                                array[index++]=c->operands[1];
                                array[index++]=c->operands[1];

-                               Constraint *cn=new Constraint(OR, nsize, array);
-                               ModelVector<Constraint *> *vec=cn->simplify();
-                               this->free();
-                               c->free();
+                               Constraint *cn=allocArrayConstraint(OR, nsize, array);
+                               VectorConstraint *vec=simplifyConstraint(cn);
+                               internalfreeConstraint(this);
+                               internalfreeConstraint(c);

                                return vec;
                        }
                        case AND: {
                                return vec;
                        }
                        case AND: {

-                               Constraint *array[numoperandsorvar];
+                               Constraint *array[this->numoperandsorvar];

 
 

-                               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
+                               VectorConstraint *vec=allocDefVectorConstraint();

                                for(uint j=0;j<c->numoperandsorvar;j++) {
                                        //copy other elements
                                for(uint j=0;j<c->numoperandsorvar;j++) {
                                        //copy other elements

-                                       for(uint k=0;k<numoperandsorvar;k++) {
+                                       for(uint k=0;k<this->numoperandsorvar;k++) {

                                                if (k!=i) {
                                                if (k!=i) {

-                                                       array[k]=operands[k]->clone();
+                                                       array[k]=cloneConstraint(this->operands[k]);

                                                }
                                        }
 
                                                }
                                        }
 

-                                       array[i]=c->operands[j]->clone();
-                                       Constraint *cn=new Constraint(OR, numoperandsorvar, array);
-                                       ModelVector<Constraint *> * newvec=cn->simplify();
+                                       array[i]=cloneConstraint(c->operands[j]);
+                                       Constraint *cn=allocArrayConstraint(OR, this->numoperandsorvar, array);
+                                       VectorConstraint * newvec=simplifyConstraint(cn);

                                        if (mergeandfree(vec, newvec)) {
                                        if (mergeandfree(vec, newvec)) {

-                                               this->freerec();
+                                               freerecConstraint(this);

                                                return vec;
                                        }
                                }
                                                return vec;
                                        }
                                }

-                               this->freerec();
+                               freerecConstraint(this);

                                return vec;
                        }
                        default:
                                return vec;
                        }
                        default:


@@ -372,19 +368,19 @@ ModelVector<Constraint *> * Constraint::simplify() {
                        }
                        //continue on to next item
                }
                        }
                        //continue on to next item
                }

-               ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
-               if (numoperandsorvar==1) {
-                       Constraint *c=operands[0];
-                       this->freerec();
-                       vec->push_back(c);
+               VectorConstraint * vec=allocDefVectorConstraint();
+               if (this->numoperandsorvar==1) {
+                       Constraint *c=this->operands[0];
+                       freerecConstraint(this);
+                       pushVectorConstraint(vec, c);

                } else
                } else

-                       vec->push_back(this);
+                       pushVectorConstraint(vec, this);

                return vec;
        }
        case IMPLIES: {
                return vec;
        }
        case IMPLIES: {

-               Constraint *cn=new Constraint(OR, operands[0]->negate(), operands[1]);
-               ModelVector<Constraint *> *vec=cn->simplify();
-               this->free();
+               Constraint *cn=allocConstraint(OR, negateConstraint(this->operands[0]), this->operands[1]);
+               VectorConstraint * vec=simplifyConstraint(cn);
+               internalfreeConstraint(this);

                return vec;
        }
        default:
                return vec;
        }
        default:


@@ -393,8 +389,8 @@ ModelVector<Constraint *> * Constraint::simplify() {
        }
 }
 
        }
 }
 

-Constraint * Constraint::negate() {
-       switch(type) {
+Constraint * negateConstraint(Constraint * this) {
+       switch(this->type) {

        case TRUE:
                return &cfalse;
        case FALSE:
        case TRUE:
                return &cfalse;
        case FALSE:


@@ -403,18 +399,18 @@ Constraint * Constraint::negate() {
        case VAR:
                return this->neg;
        case IMPLIES: {
        case VAR:
                return this->neg;
        case IMPLIES: {

-               Constraint *l=operands[0];
-               Constraint *r=operands[1];
-               operands[0]=r;
-               operands[1]=l;
+               Constraint *l=this->operands[0];
+               Constraint *r=this->operands[1];
+               this->operands[0]=r;
+               this->operands[1]=l;

                return this;
        }
        case AND:
        case OR: {
                return this;
        }
        case AND:
        case OR: {

-               for(uint i=0;i<numoperandsorvar;i++) {
-                       operands[i]=operands[i]->negate();
+               for(uint i=0;i<this->numoperandsorvar;i++) {
+                       this->operands[i]=negateConstraint(this->operands[i]);

                }
                }

-               type=(type==AND) ? OR : AND;
+               this->type=(this->type==AND) ? OR : AND;

                return this;
        }
        default:
                return this;
        }
        default:

diff --git a/src/constraint.h b/src/constraint.h
index f6b16959cc09d98c6925991b659020c347769af9..9f555d4527045499f9c187ad4c3d39e419b0ee28 100644 (file)
--- a/src/constraint.h
+++ b/src/constraint.h
@@ -10,7 +10,7 @@
 #ifndef CONSTRAINT_H
 #define CONSTRAINT_H
 #include "classlist.h"
 #ifndef CONSTRAINT_H
 #define CONSTRAINT_H
 #include "classlist.h"

-#include "stl-model.h"
+#include "structs.h"

 
 enum ConstraintType {
        TRUE, FALSE, IMPLIES, AND, OR, VAR, NOTVAR, BOGUS
 
 enum ConstraintType {
        TRUE, FALSE, IMPLIES, AND, OR, VAR, NOTVAR, BOGUS


@@ -18,41 +18,37 @@ enum ConstraintType {
 
 typedef enum ConstraintType CType;
 
 
 typedef enum ConstraintType CType;
 

-class Constraint {
-public:
-       Constraint(CType t, Constraint *l, Constraint *r);
-       Constraint(CType t, Constraint *l);
-       Constraint(CType t, uint num, Constraint ** array);
-       Constraint(CType t, uint var);
-       Constraint(CType t);
-       ~Constraint();
-       void print();
-       void dumpConstraint(IncrementalSolver *solver);
-       uint getVar() {ASSERT(type==VAR); return numoperandsorvar;}
-       ModelVector<Constraint *> * simplify();
-       CType getType() {return type;}
-       bool isFalse() {return type==FALSE;}
-       bool isTrue() {return type==TRUE;}
-       void free();
-       void freerec();
-       Constraint * clone();
-       void setNeg(Constraint *c) {neg=c;}
-       Constraint *negate();
-
-       MEMALLOC;
-private:
+struct Constraint {

        CType type;
        uint numoperandsorvar;
        Constraint ** operands;
        Constraint *neg;
        CType type;
        uint numoperandsorvar;
        Constraint ** operands;
        Constraint *neg;

-       friend bool mergeandfree(ModelVector<Constraint *> * to, ModelVector<Constraint *> * from);

 };
 
 };
 

+Constraint * allocConstraint(CType t, Constraint *l, Constraint *r);
+Constraint * allocUnaryConstraint(CType t, Constraint *l);
+Constraint * allocArrayConstraint(CType t, uint num, Constraint ** array);
+Constraint * allocVarConstraint(CType t, uint var);
+
+void freeConstraint(Constraint *);
+void printConstraint(Constraint * c);
+void dumpConstraint(Constraint * c, IncrementalSolver *solver);
+uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
+VectorConstraint * simplify(Constraint * c);
+CType getType(Constraint * c) {return c->type;}
+bool isFalse(Constraint * c) {return c->type==FALSE;}
+bool isTrue(Constraint * c) {return c->type==TRUE;}
+void freeConstraint(Constraint * c);
+void freerecConstraint(Constraint * c);
+Constraint * cloneConstraint(Constraint * c);
+void setNegConstraint(Constraint * this, Constraint *c) {this->neg=c;}
+Constraint *negateConstraint(Constraint * c);
+

 extern Constraint ctrue;
 extern Constraint cfalse;
 
 Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value);
 Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value);
 extern Constraint ctrue;
 extern Constraint cfalse;
 
 Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value);
 Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value);

-Constraint * generateEquivConstraint(uint numvars, Constraint **var1, Constraint **var2);
+Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2);

 Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2);
 #endif
 Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2);
 #endif

diff --git a/src/structs.c b/src/structs.c
index 058f62838a6fcc4b43707afcd329114881971a7a..4cfb51a271baabbee2b1922a9d43e9722755195f 100644 (file)
--- a/src/structs.c
+++ b/src/structs.c
@@ -4,5 +4,6 @@
 VectorImpl(Int, uint64_t, 4);
 VectorImpl(Boolean, Boolean *, 4);
 VectorImpl(Void, void *, 4);
 VectorImpl(Int, uint64_t, 4);
 VectorImpl(Boolean, Boolean *, 4);
 VectorImpl(Void, void *, 4);

+VectorImpl(Constraint, Constraint *, 4);

 HashTableImpl(Void, void *, void *, Ptr_hash_function, Ptr_equals);
 HashSetImpl(Void, void *, Ptr_hash_function, Ptr_equals);
 HashTableImpl(Void, void *, void *, Ptr_hash_function, Ptr_equals);
 HashSetImpl(Void, void *, Ptr_hash_function, Ptr_equals);

diff --git a/src/structs.h b/src/structs.h
index da5f863de13f1297b9b08dbe8f62f07151eaa38b..83ce58c3eaff28e93126e21db1b7657a80cb5a73 100644 (file)
--- a/src/structs.h
+++ b/src/structs.h
@@ -7,6 +7,7 @@
 
 VectorDef(Int, uint64_t, 4);
 VectorDef(Boolean, Boolean *, 4);
 
 VectorDef(Int, uint64_t, 4);
 VectorDef(Boolean, Boolean *, 4);

+VectorDef(Constraint, Constraint *, 4);

 VectorDef(Void, void *, 4);
 
 inline unsigned int Ptr_hash_function(void * hash) {
 VectorDef(Void, void *, 4);
 
 inline unsigned int Ptr_hash_function(void * hash) {

diff --git a/src/vector.h b/src/vector.h
index 9beccb387a3dda11a59e1da8c27031b3983a19fb..a867db62a32086916adc5901ba4a80a19b308d55 100644 (file)
--- a/src/vector.h
+++ b/src/vector.h
@@ -16,7 +16,8 @@
        type getVector ## name(Vector ## name *vector, uint index);                                             \
        void setVector ## name(Vector ## name *vector, uint index, type item); \
        uint getSizeVector ##name(Vector ##name *vector);                                                                                       \
        type getVector ## name(Vector ## name *vector, uint index);                                             \
        void setVector ## name(Vector ## name *vector, uint index, type item); \
        uint getSizeVector ##name(Vector ##name *vector);                                                                                       \

-       void freeVector ##name(Vector ##name *vector);
+       void freeVector ##name(Vector ##name *vector);                                                                                          \
+       void clearVector ##name(Vector ## name *vector);

 
 #define VectorImpl(name, type, defcap)                                                                                                                                 \
        Vector ## name * allocDefVector ## name() {                                                                                                             \
 
 #define VectorImpl(name, type, defcap)                                                                                                                                 \
        Vector ## name * allocDefVector ## name() {                                                                                                             \


@@ -53,5 +54,8 @@
        void freeVector ##name(Vector ##name *vector) {                                                                                         \
                ourfree(vector->array);                                                                                                                                                                                 \
                ourfree(vector);                                                                                                                                                                                                                \
        void freeVector ##name(Vector ##name *vector) {                                                                                         \
                ourfree(vector->array);                                                                                                                                                                                 \
                ourfree(vector);                                                                                                                                                                                                                \

+       }                                                                                                                                                                                                                                                                                       \
+       void clearVector ##name(Vector ## name *vector) {                                                                                       \
+               vector->size=0;                                                                                                                                                                                                                 \

        }
 #endif
        }
 #endif