[12] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [smtGraph.c] |
---|
| 4 | |
---|
| 5 | PackageName [smt] |
---|
| 6 | |
---|
| 7 | Synopsis [Routines for smt function.] |
---|
| 8 | |
---|
| 9 | Author [Hyondeuk Kim] |
---|
| 10 | |
---|
| 11 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
| 12 | |
---|
| 13 | All rights reserved. |
---|
| 14 | |
---|
| 15 | Redistribution and use in source and binary forms, with or without |
---|
| 16 | modification, are permitted provided that the following conditions |
---|
| 17 | are met: |
---|
| 18 | |
---|
| 19 | Redistributions of source code must retain the above copyright |
---|
| 20 | notice, this list of conditions and the following disclaimer. |
---|
| 21 | |
---|
| 22 | Redistributions in binary form must reproduce the above copyright |
---|
| 23 | notice, this list of conditions and the following disclaimer in the |
---|
| 24 | documentation and/or other materials provided with the distribution. |
---|
| 25 | |
---|
| 26 | Neither the name of the University of Colorado nor the names of its |
---|
| 27 | contributors may be used to endorse or promote products derived from |
---|
| 28 | this software without specific prior written permission. |
---|
| 29 | |
---|
| 30 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
| 31 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
| 32 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
| 33 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
| 34 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
| 35 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
| 36 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
| 37 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
| 38 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
| 39 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
| 40 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
| 41 | POSSIBILITY OF SUCH DAMAGE.] |
---|
| 42 | |
---|
| 43 | ******************************************************************************/ |
---|
| 44 | |
---|
| 45 | #ifdef HAVE_LIBGMP |
---|
| 46 | |
---|
| 47 | #include "smt.h" |
---|
| 48 | |
---|
| 49 | smtVertex_t * |
---|
| 50 | smt_add_vertex(smtGraph_t * G, int vindex) |
---|
| 51 | { |
---|
| 52 | smtVertex_t *v; |
---|
| 53 | |
---|
| 54 | v = &(G->vHead[vindex]); |
---|
| 55 | |
---|
| 56 | v->ins = sat_array_alloc(10); |
---|
| 57 | v->outs = sat_array_alloc(10); |
---|
| 58 | v->targets = sat_array_alloc(10); |
---|
| 59 | |
---|
| 60 | v->index = vindex; |
---|
| 61 | |
---|
| 62 | return(v); |
---|
| 63 | } |
---|
| 64 | |
---|
| 65 | smtEdge_t * |
---|
| 66 | smt_add_edge( |
---|
| 67 | smtGraph_t * G, |
---|
| 68 | smtVertex_t * s, |
---|
| 69 | smtVertex_t * d, |
---|
| 70 | smtAvar_t * avar, |
---|
| 71 | int eindex) |
---|
| 72 | { |
---|
| 73 | smtEdge_t *e; |
---|
| 74 | |
---|
| 75 | e = &(G->eHead[eindex]); |
---|
| 76 | e->index = eindex; |
---|
| 77 | |
---|
| 78 | e->src = s; |
---|
| 79 | e->dest = d; |
---|
| 80 | |
---|
| 81 | s->outs = sat_array_insert(s->outs, (long) e); |
---|
| 82 | d->ins = sat_array_insert(d->ins, (long) e); |
---|
| 83 | |
---|
| 84 | if (!e->implied) { |
---|
| 85 | e->implied = sat_array_alloc(8); |
---|
| 86 | G->imp_edges = sat_array_insert(G->imp_edges, (long) e); |
---|
| 87 | } |
---|
| 88 | |
---|
| 89 | e->avar = avar; |
---|
| 90 | |
---|
| 91 | return(e); |
---|
| 92 | } |
---|
| 93 | |
---|
| 94 | smtEdge_t * |
---|
| 95 | smt_find_edge(smtVertex_t * s, smtVertex_t * d) |
---|
| 96 | { |
---|
| 97 | smtEdge_t *e; |
---|
| 98 | int i; |
---|
| 99 | |
---|
| 100 | for(i = 0; i < s->outs->size; i++) { |
---|
| 101 | e = (smtEdge_t *) s->outs->space[i]; |
---|
| 102 | if(e->dest == d) |
---|
| 103 | return(e); |
---|
| 104 | } |
---|
| 105 | return(0); |
---|
| 106 | } |
---|
| 107 | |
---|
| 108 | #endif |
---|
| 109 | |
---|
| 110 | |
---|