#include "satInt.h"#include "baig.h"
Include dependency graph for satImplication.c:
Go to the source code of this file.
Typedefs | |
| typedef int(* | IMPLY_FN )(satManager_t *cm, satLevel_t *d, long v, long left, long right) |
Functions | |
| int | sat_ImplyStop (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplySplit (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyConflict (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyLeftForward (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyRightForward (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyForwardOne (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyPropRight (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyPropRightOne (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyPropLeft (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyPropLeftOne (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | sat_ImplyPropLeftRight (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| void | sat_ImplyCNF (satManager_t *cm, satLevel_t *d, long v, satArray_t *wl) |
| int | sat_ImplyNode (satManager_t *cm, satLevel_t *d, long v) |
| void | sat_ImplicationMain (satManager_t *cm, satLevel_t *d) |
| void | sat_CleanImplicationQueue (satManager_t *cm) |
| void | sat_ImplyArray (satManager_t *cm, satLevel_t *d, satArray_t *arr) |
| void | sat_ImplyBDD (satManager_t *cm, satLevel_t *d, long v) |
| void | sat_BuildLevelZeroHyperImplicationGraph (satManager_t *cm) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: satImplication.c,v 1.10 2009/04/11 18:26:37 fabio Exp $" |
| IMPLY_FN | satImplicationFN [64] |
Typedef Documentation
| typedef int(* IMPLY_FN)(satManager_t *cm, satLevel_t *d, long v, long left, long right) |
AutomaticStart AutomaticEnd
Definition at line 38 of file satImplication.c.
Function Documentation
| void sat_BuildLevelZeroHyperImplicationGraph | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Build level zero hyper implication graph. ]
Description [Build level zero hyper implication graph. ]
SideEffects []
SeeAlso []
CONSIDER...
Definition at line 1027 of file satImplication.c.
{
}
Here is the caller graph for this function:
| void sat_CleanImplicationQueue | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Clean implication queue. ]
Description [Clean implication queue. ]
SideEffects []
SeeAlso []
Definition at line 869 of file satImplication.c.
{
satQueue_t *Q;
int i;
bAigEdge_t v;
Q = cm->queue;
if(Q->size <=0) return;
//Bing: important, can't be zero, since some var's value,which are now in
//implication queue will be erased. This may lead to not being able to
//identify conflict
if(cm->option->AbRf || cm->option->IP || cm->option->arosat){
if(Q->front <= Q->rear) {
for(i=Q->front; i<=Q->rear; i++) {
v = Q->array[i];
SATflags(v) &= ResetInQueueMask;
}
}
else {
for(i=Q->front; i<Q->max; i++) {
v = Q->array[i];
SATflags(v) &= ResetInQueueMask;
}
for(i=0; i<Q->rear; i++) {
v = Q->array[i];
SATflags(v) &= ResetInQueueMask;
}
}
}
#if 0
if(Q->front <= Q->rear) {
for(i=Q->front; i<=Q->rear; i++) {
v = Q->array[i];
SATflags(v) &= ResetInQueueMask;
SATante(v) = 0;
SATante2(v) = 0;
SATvalue(v) = 2;
}
}
else {
for(i=Q->front; i<Q->max; i++) {
v = Q->array[i];
SATflags(v) &= ResetInQueueMask;
SATante(v) = 0;
SATante2(v) = 0;
SATvalue(v) = 2;
}
for(i=0; i<Q->rear; i++) {
v = Q->array[i];
SATflags(v) &= ResetInQueueMask;
SATante(v) = 0;
SATante2(v) = 0;
SATvalue(v) = 2;
}
}
#endif
Q->size = 0;
Q->front = 1;
Q->rear = 0;
}
Here is the caller graph for this function:
| void sat_ImplicationMain | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [Apply implication until the implication queue is empty. ]
Description [ Apply implication until the implication queue is empty. Since the node can be part of AIG and CNF and BDD, the implications on three representation are applied]
SideEffects []
SeeAlso []
Definition at line 815 of file satImplication.c.
{
satQueue_t *Q, *BDDQ;
long v;
Q = cm->queue;
BDDQ = cm->BDDQueue;
while(1) {
v = sat_Dequeue(Q);
while(v && d->conflict == 0) {
sat_ImplyNode(cm, d, v);
SATflags(v) &= ResetInQueueMask;
v = sat_Dequeue(Q);
}
if(d->conflict)
break;
if(cm->option->BDDImplication) {
v = sat_Dequeue(Q);
while(v && d->conflict == 0) {
sat_ImplyBDD(cm, d, v);
SATflags(v) &= ResetInQueueMask;
v = sat_Dequeue(Q);
}
}
if(Q->size == 0 && BDDQ->size == 0)
break;
}
sat_CleanImplicationQueue(cm);
cm->implicatedSoFar += d->implied->num;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_ImplyArray | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| satArray_t * | arr | ||
| ) |
Function********************************************************************
Synopsis [Add nodes in array into implication queue. ]
Description [Add nodes in array into implication queue. ]
SideEffects []
SeeAlso []
Definition at line 947 of file satImplication.c.
{
int i, size;
long v;
int inverted, value;
satQueue_t *Q;
if(arr == 0) return;
if(cm->status)return;
size = arr->num;
Q = cm->queue;
for(i=0; i<size; i++) {
v = arr->space[i];
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = !inverted;
if(SATvalue(v) < 2) {
if(SATvalue(v) == value) continue;
else {
cm->status = SAT_UNSAT;
d->conflict = v;
//Bing:
return;
}
}
SATvalue(v) = value;
SATmakeImplied(v, d);
//Bing:
cm->each->nCNFImplications++;
if(cm->option->coreGeneration && cm->option->IP){
st_insert(cm->anteTable,(char *)SATnormalNode(v),(char *)SATnormalNode(v));
}
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(Q, v);
SATflags(v) |= InQueueMask;
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_ImplyBDD | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v | ||
| ) |
Function********************************************************************
Synopsis [Apply implication on BDD node. ]
Description [Apply implication on BDD node. ]
SideEffects []
SeeAlso []
CONSIDER ...
Definition at line 1006 of file satImplication.c.
{
}
Here is the caller graph for this function:
| void sat_ImplyCNF | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| satArray_t * | wl | ||
| ) |
Function********************************************************************
Synopsis [Implication based on clause.]
Description [Implication based two watched literal scheme ]
SideEffects []
SeeAlso []
conflict happens
implication
to identify the objective dependent clause for incremental SAT
move watched literal
Definition at line 596 of file satImplication.c.
{
int size, i, j;
long *space;
long lit, *plit, *tplit;
int dir;
long nv, tv, *oplit, *wlit;
int isInverted, value;
int tsize, inverted;
long cur, clit;
satStatistics_t *stats;
satOption_t *option;
satQueue_t *Q;
satVariable_t *var;
size = wl->num;
space = wl->space;
Q = cm->queue;
stats = cm->each;
option = cm->option;
nv = 0;
wlit = 0;
for(i=0; i<size; i++) {
plit = (long*)space[i];
if(plit == 0 || *plit == 0) {
size--;
space[i] = space[size];
i--;
continue;
}
lit = *plit;
dir = SATgetDir(lit);
oplit = plit;
while(1) {
oplit += dir;
if(*oplit <=0) {
if(dir == 1) nv =- (*oplit);
if(dir == SATgetDir(lit)) {
oplit = plit;
dir = -dir;
continue;
}
tv = SATgetNode(*wlit);
isInverted = SATisInverted(tv);
tv = SATnormalNode(tv);
value = SATvalue(tv) ^ isInverted;
if(value == 0) {
d->conflict = nv;
wl->num = size;
return;
}
else if(value > 1) {
SATvalue(tv) = !isInverted;
SATmakeImplied(tv, d);
SATante(tv) = nv;
if((SATflags(tv) & InQueueMask) == 0) {
sat_Enqueue(Q, tv);
SATflags(tv) |= InQueueMask;
}
stats->nCNFImplications++;
if(option->incTraceObjective == 1) {
tsize = SATnumLits(nv);
for(j=0, tplit=(long*)SATfirstLit(nv); j<tsize; j++, tplit++) {
cur = SATgetNode(*tplit);
cur = SATnormalNode(cur);
if(SATflags(cur) & ObjMask) {
SATflags(tv) |= ObjMask;
break;
}
}
}
}
break;
}
clit = *oplit;
tv = SATgetNode(clit);
inverted = SATisInverted(tv);
tv = SATnormalNode(tv);
value = SATvalue(tv) ^ inverted;
if(SATisWL(clit)) { /* found other watched literal */
wlit = oplit;
if(value == 1) {
break;
}
continue;
}
if(value == 0)
continue;
SATunsetWL(plit);
size--;
space[i] = space[size];
i--;
var = SATgetVariable(tv);
SATsetWL(oplit, dir);
inverted = !inverted;
if(var->wl[inverted]) {
sat_ArrayInsert(var->wl[inverted], (long)oplit);
}
else {
var->wl[inverted] = sat_ArrayAlloc(4);
sat_ArrayInsert(var->wl[inverted], (long)oplit);
}
break;
}
}
wl->num = size;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ImplyConflict | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [The conflict happens.]
Description [The conflict happens when 0 1 1 1 1 | | | | | --- --- --- --- --- / \ / \ / \ / \ / \ 1 1 X 0 0 X 1 0 0 1 ]
SideEffects []
SeeAlso []
Definition at line 191 of file satImplication.c.
{
if(left != 2) {
d->conflict = SATnormalNode(v);
}
return(0);
}
| int sat_ImplyForwardOne | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to output due to both child.]
Description [A value implied to output due to both child X | --- / \ 1 1 ]
SideEffects []
SeeAlso []
Definition at line 307 of file satImplication.c.
{
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATvalue(v) = 1;
SATmakeImplied(v, d);
SATante(v) = right;
SATante2(v) = left;
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
SATflags(v) |= (SATflags(right) & ObjMask);
SATflags(v) |= (SATflags(left) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int sat_ImplyLeftForward | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to output due to left child.]
Description [A value implied to output due to left child X X | | --- --- / \ / \ 0 1 0 X ]
SideEffects []
SeeAlso []
Definition at line 223 of file satImplication.c.
{
v = SATnormalNode(v);
left = SATnormalNode(left);
SATvalue(v) = 0;
SATmakeImplied(v, d);
SATante(v) = left;
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
SATflags(v) |= (SATflags(left) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int sat_ImplyNode | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v | ||
| ) |
Function********************************************************************
Synopsis [Apply implication on node. If the conflict happens then return 0, otherwise return 1]
Description [Apply implication on node. Since the node can be part of AIG and CNF and BDD, the implications on three representation are applied]
SideEffects []
SeeAlso []
implcation on CNF
implication on AIG
Definition at line 746 of file satImplication.c.
{
long *fan, cur;
int value;
int i, size;
long left, right;
satVariable_t *var;
satArray_t *wlArray;
value = SATvalue(v) ^ 1;
var = SATgetVariable(v);
wlArray = var->wl[value];
if(wlArray && wlArray->size) {
sat_ImplyCNF(cm, d, v, wlArray);
}
if(d->conflict)
return(0);
fan = (long *)SATfanout(v);
size = SATnFanout(v);
for(i=0; i<size; i++, fan++) {
cur = *fan;
cur = cur >> 1;
cur = SATnormalNode(cur);
left = SATleftChild(cur);
right = SATrightChild(cur);
value = SATgetValue(left, right, cur);
(satImplicationFN[value])(cm, d, cur, left, right);
if(d->conflict)
return(0);
}
left = SATleftChild(v);
right = SATrightChild(v);
value = SATgetValue(left, right, v);
(satImplicationFN[value])(cm, d, v, left, right);
if(d->conflict)
return(0);
return(1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ImplyPropLeft | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to left child due to both output and right.]
Description [A value implied to left child due to both output and right 0 | --- / \ X 1 ]
SideEffects []
SeeAlso []
Definition at line 445 of file satImplication.c.
{
int isInverted;
isInverted = SATisInverted(left);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(left, d);
SATante(left) = v;
SATante2(left) = right;
SATvalue(left) = isInverted;
sat_Enqueue(cm->queue, left);
SATflags(left) |= InQueueMask;
SATflags(left) |= (SATflags(v) & ObjMask);
SATflags(left) |= (SATflags(right) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int sat_ImplyPropLeftOne | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to left child due to both output and right.]
Description [A value implied to left child due to both output and right 1 | --- / \ X 1 ]
SideEffects []
SeeAlso []
Definition at line 495 of file satImplication.c.
{
int isInverted;
isInverted = SATisInverted(left);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(left, d);
SATante(left) = v;
SATvalue(left) = !isInverted;
sat_Enqueue(cm->queue, left);
SATflags(left) |= InQueueMask;
SATflags(left) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int sat_ImplyPropLeftRight | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to left and right child due to output.]
Description [A value implied to left and right child due to output 1 | --- / \ X X ]
SideEffects []
SeeAlso []
Definition at line 543 of file satImplication.c.
{
int isLeftInverted;
int isRightInverted;
if(left == right) return 1;
isLeftInverted = SATisInverted(left);
isRightInverted = SATisInverted(right);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(left, d);
SATmakeImplied(right, d);
SATante(left) = v;
SATante(right) = v;
SATvalue(left) = !isLeftInverted;
SATvalue(right) = !isRightInverted;
sat_Enqueue(cm->queue, left);
SATflags(left) |= InQueueMask;
sat_Enqueue(cm->queue, right);
SATflags(right) |= InQueueMask;
SATflags(left) |= (SATflags(v) & ObjMask);
SATflags(right) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications += 2;
return(0);
}
Here is the call graph for this function:
| int sat_ImplyPropRight | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to right child due to both output and left.]
Description [A value implied to right child due to both output and left 0 | --- / \ 1 X ]
SideEffects []
SeeAlso []
Definition at line 351 of file satImplication.c.
{
int isInverted;
isInverted = SATisInverted(right);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(right, d);
SATvalue(right) = isInverted;
SATante(right) = left;
SATante2(right) = v;
sat_Enqueue(cm->queue, right);
SATflags(right) |= InQueueMask;
SATflags(right) |= (SATflags(left) & ObjMask);
SATflags(right) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int sat_ImplyPropRightOne | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to right child due to both output and left.]
Description [A value implied to right child due to both output and left 1 | --- / \ 1 X ]
SideEffects []
SeeAlso []
Definition at line 398 of file satImplication.c.
{
int isInverted;
isInverted = SATisInverted(right);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(right, d);
SATante(right) = v;
SATvalue(right) = !isInverted;
sat_Enqueue(cm->queue, right);
SATflags(right) |= InQueueMask;
SATflags(right) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int sat_ImplyRightForward | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to output due to right child.]
Description [A value implied to output due to right child X X | | --- --- / \ / \ 1 0 X 0 ]
SideEffects []
SeeAlso []
Definition at line 265 of file satImplication.c.
{
v = SATnormalNode(v);
right = SATnormalNode(right);
SATvalue(v) = 0;
SATmakeImplied(v, d);
SATante(v) = right;
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
SATflags(v) |= (SATflags(right) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int sat_ImplySplit | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [No further implcation when this function is called.]
Description [No further implcation when this function is called. and need split on output. 0 | --- / \ X X ]
SideEffects []
SeeAlso []
Definition at line 163 of file satImplication.c.
{
return(0);
}
| int sat_ImplyStop | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [No further implcation when this function is called.]
Description [No further implcation when this function is called. 0 0 0 1 | | | | --- --- --- --- / \ / \ / \ / \ 0 X X 0 0 0 1 1 ]
SideEffects []
SeeAlso []
Definition at line 134 of file satImplication.c.
{
return(0);
}
Variable Documentation
Definition at line 41 of file satImplication.c.
char rcsid [] UNUSED = "$Id: satImplication.c,v 1.10 2009/04/11 18:26:37 fabio Exp $" [static] |
CFile***********************************************************************
FileName [satImplication.c]
PackageName [sat]
Synopsis [Routines for BCP.]
Author [HoonSang Jin]
Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 22 of file satImplication.c.
