#include "satInt.h"
Include dependency graph for satInc.c:
Go to the source code of this file.
Functions | |
| static int | ScoreDistillCompare (const void *x, const void *y) |
| void | sat_IncrementalUsingDistill (satManager_t *cm) |
| satLevel_t * | sat_DecisionBasedOnTrie (satManager_t *cm, long v, int value) |
| void | sat_TrieBasedImplication (satManager_t *cm, satArray_t *trieArray, int depth) |
| void | sat_ConflictAnalysisOnTrie (satManager_t *cm, satLevel_t *d) |
| void | sat_GetConflictAsConflictClause (satManager_t *cm, satArray_t *clauseArray) |
| void | sat_RestoreForwardedClauses (satManager_t *cm, int objectFlag) |
| void | sat_CheckForwardedClauses (satManager_t *cm) |
| void | sat_SaveNonobjClauses (satManager_t *cm) |
| void | sat_SaveAllClauses (satManager_t *cm) |
| void | sat_BuildTrieForDistill (satManager_t *cm) |
| void | sat_BuildTrie (satManager_t *cm, satArray_t *trieArray, long *plit, int depth) |
| void | sat_FreeTrie (satManager_t *cm, satArray_t *arr) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: satInc.c,v 1.16 2009/04/11 18:26:37 fabio Exp $" |
| static satManager_t * | SatCm |
Function Documentation
| void sat_BuildTrie | ( | satManager_t * | cm, |
| satArray_t * | trieArray, | ||
| long * | plit, | ||
| int | depth | ||
| ) |
Function********************************************************************
Synopsis [ Build Trie with objective dependent conflict clauses]
Description [ When applying incremental SAT based on distillation build Trie with objective dependent conflict clauses.]
SideEffects [ ]
SeeAlso [ sat_BuildTrieForDistill ]
Definition at line 644 of file satInc.c.
{
int i, inverted;
long v;
satTrie_t *t;
while(1) {
if(*plit <= 0) return;
v = SATgetNode(*plit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
if(SATvalue(v) < 2)plit++;
else break;
}
for(i=0; i<trieArray->num; i++) {
t = (satTrie_t *)(trieArray->space[i]);
if(t->id == v) {
if(t->child[inverted] == 0)
t->child[inverted] = sat_ArrayAlloc(2);
plit++;
sat_BuildTrie(cm, t->child[inverted], plit, depth+1);
return;
}
}
t = ALLOC(satTrie_t, 1);
memset(t, 0, sizeof(satTrie_t));
t->id = v;
t->depth = depth;
sat_ArrayInsert(trieArray, (long)t);
if(t->child[inverted] == 0)
t->child[inverted] = sat_ArrayAlloc(2);
plit++;
sat_BuildTrie(cm, t->child[inverted], plit, depth+1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_BuildTrieForDistill | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Build Trie with objective dependent conflict clauses]
Description [ When applying incremental SAT based on distillation build Trie with objective dependent conflict clauses.]
SideEffects [ ]
SeeAlso [ sat_BuildTrie ]
Definition at line 540 of file satInc.c.
{
int limit, nCl, nLit;
int j, n;
int size, inverted;
long v, *plit, i;
int findFlag;
satVariable_t *var;
satArray_t *trieArray;
satArray_t *unitArray;
satTrie_t *t;
size = cm->initNumVariables * satNodeSize;
for(i=satNodeSize; i<size; i+= satNodeSize) {
var = SATgetVariable(i);
var->scores[0] = 0;
var->scores[1] = 0;
}
nCl = nLit = 0;
limit = cm->option->incNumObjLitsLimit;
for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
if(SATreadInUse(i) == 0) continue;
if(SATflags(i) & NonobjMask) continue;
size = SATnumLits(i);
if(size > limit) continue;
n = 0;
for(j=0, plit = (long*)SATfirstLit(i); j<size; j++, plit++) {
v = SATgetNode(*plit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
var = SATgetVariable(v);
var->scores[inverted] += 1;
if(SATvalue(v) < 2) continue;
n++;
}
if(n > 0) {
nCl++;
nLit += n;
}
}
if(cm->option->verbose > 1) {
fprintf(cm->stdOut, "%s Candidates for Distill %d clauses %d literals\n",
cm->comment, nCl, nLit);
}
trieArray = sat_ArrayAlloc(64);
cm->trieArray = trieArray;
unitArray = cm->objUnitLitArray;
if(unitArray) {
for(i=0; i<unitArray->num; i++) {
v = unitArray->space[i];
inverted = SATisInverted(v);
v = SATnormalNode(v);
findFlag = 0;
for(j=0; j<trieArray->num; j++) {
t = (satTrie_t *)(trieArray->space[j]);
if(t->id == v) {
if(t->child[inverted] == 0)
t->child[inverted] = sat_ArrayAlloc(2);
findFlag = 1;
}
}
if(findFlag == 0) {
t = ALLOC(satTrie_t, 1);
memset(t, 0, sizeof(satTrie_t));
t->id = v;
if(t->child[inverted] == 0)
t->child[inverted] = sat_ArrayAlloc(2);
sat_ArrayInsert(trieArray, (long)t);
}
}
}
for(i=cm->beginConflict; i<cm->nodesArraySize; i+=satNodeSize) {
if(SATreadInUse(i) == 0) continue;
if(SATflags(i) & NonobjMask) continue;
size = SATnumLits(i);
if(size > limit) continue;
plit = (long*)SATfirstLit(i);
SatCm = cm;
qsort(plit, size, sizeof(long), ScoreDistillCompare);
sat_BuildTrie(cm, trieArray, plit, 1);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_CheckForwardedClauses | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Check whether the given conflict clauses can be forwared ]
Description [ Check whether the given conflict clauses can be forwared ]
SideEffects [ ]
SeeAlso [ ]
Definition at line 352 of file satInc.c.
{
long *space, *start;
long nv;
int size, i;
int total;
int conflictFlag, inverted;
int j, value, level;
satLevel_t *d;
satArray_t *saved;
satArray_t *clause;
d = 0;
saved = cm->savedConflictClauses;
if(saved == 0)
return;
clause = sat_ArrayAlloc(50);
total = 0;
for(i=0, space=saved->space; i<saved->num; i++, space++){
if(*space < 0) {
start = space;
space++;
i++;
size = 0;
clause->num = 0;
conflictFlag = 0;
while(*space > 0) {
sat_ArrayInsert(clause, SATnot((*space)));
if(conflictFlag == 0) {
nv = *space;
inverted = (SATisInverted(nv));
nv = SATnormalNode(nv);
d = sat_AllocLevel(cm);
d->decisionNode = nv;
SATvalue(nv) = inverted;
SATmakeImplied(nv, d);
sat_Enqueue(cm->queue, nv);
SATflags(nv) |= InQueueMask;
sat_ImplicationMain(cm, d);
if(d->conflict) conflictFlag = 1;
}
size++;
i++;
space++;
}
if(d->conflict == 0) {
fprintf(cm->stdOut, "%s ERROR : %ld does not result in conflict\n",
cm->comment, *start);
for(j=0; j<clause->num; j++) {
nv = clause->space[j];
inverted = SATisInverted(nv);
nv = SATnormalNode(nv);
value = SATvalue(nv);
level = value>1 ? -1 : SATlevel(nv);
fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
nv, inverted ? '\'' : ' ', level, SATgetValueChar(value),
' ');
}
fprintf(cm->stdOut, "\n");
}
sat_Backtrack(cm, -1);
total++;
}
}
sat_ArrayFree(clause);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_ConflictAnalysisOnTrie | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Conflict analysis based on trie]
Description [ Conflict analysis based on trie]
SideEffects []
SeeAlso []
Definition at line 181 of file satInc.c.
{
int bLevel;
long v, learned, unitLit;
int objectFlag;
satArray_t *clauseArray;
satStatistics_t *stats;
bLevel = 0;
unitLit = -1;
clauseArray = cm->auxArray;
sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &unitLit);
if(clauseArray->num > (int)(cm->currentDecision*2)) {
sat_GetConflictAsConflictClause(cm, clauseArray);
}
if(clauseArray->num == 1) {
cm->status = SAT_BACKTRACK;
v = clauseArray->space[0];
if(objectFlag)
sat_ArrayInsert(cm->objUnitLitArray, SATnot(v));
else
sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(v));
}
else {
learned = sat_AddClauseIncremental(cm, clauseArray, objectFlag, 1);
}
stats = cm->each;
if(objectFlag) {
stats->nInitObjConflictCl++;
stats->nInitObjConflictLit += clauseArray->num;
stats->nObjConflictCl++;
stats->nObjConflictLit += clauseArray->num;
stats->nDistillObjConflictCl++;
stats->nDistillObjConflictLit += clauseArray->num;
}
else {
stats->nInitNonobjConflictCl++;
stats->nInitNonobjConflictLit += clauseArray->num;
stats->nObjConflictCl++;
stats->nObjConflictLit += clauseArray->num;
stats->nDistillNonobjConflictCl++;
stats->nDistillNonobjConflictLit += clauseArray->num;
}
stats->nConflictCl++;
stats->nConflictLit += clauseArray->num;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| satLevel_t* sat_DecisionBasedOnTrie | ( | satManager_t * | cm, |
| long | v, | ||
| int | value | ||
| ) |
Function********************************************************************
Synopsis [ Make decision based on trie when applying distillation ]
Description [ Make decision based on trie when applying distillation ]
SideEffects []
SeeAlso []
Definition at line 80 of file satInc.c.
{
satLevel_t *d;
d = sat_AllocLevel(cm);
d->decisionNode = v;
SATvalue(v) = value;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
return(d);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_FreeTrie | ( | satManager_t * | cm, |
| satArray_t * | arr | ||
| ) |
Function********************************************************************
Synopsis [ Free trie structure ]
Description [ Free trie structure ]
SideEffects [ ]
SeeAlso [ sat_BuildTrieForDistill ]
Definition at line 700 of file satInc.c.
{
int i;
satTrie_t *t;
if(arr == 0) return;
for(i=0; i<arr->num; i++) {
t = (satTrie_t *)(arr->space[i]);
if(t->child[0]) {
sat_FreeTrie(cm, t->child[0]);
sat_ArrayFree(t->child[0]);
}
if(t->child[1]) {
sat_FreeTrie(cm, t->child[1]);
sat_ArrayFree(t->child[1]);
}
free(t);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_GetConflictAsConflictClause | ( | satManager_t * | cm, |
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Get conflict clauses from the decision variables]
Description [ When applying distillation, get conflict clauses from the decision variables to create conflict clause ]
SideEffects [ ]
SeeAlso [ ]
Definition at line 247 of file satInc.c.
{
int i;
satLevel_t *d;
clauseArray->num = 0;
for(i=1; i<=cm->currentDecision; i++) {
d = SATgetDecision(i);
sat_ArrayInsert(clauseArray,
(d->decisionNode)^(!(SATvalue(d->decisionNode))));
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_IncrementalUsingDistill | ( | satManager_t * | cm | ) |
AutomaticEnd Function********************************************************************
Synopsis [ Apply distillation method to find the clauses that can be forwarded]
Description [ Apply distillation method to find the clauses that can be forwarded]
SideEffects []
SeeAlso []
Definition at line 58 of file satInc.c.
{
sat_TrieBasedImplication(cm, cm->trieArray, 1);
sat_FreeTrie(cm, cm->trieArray);
cm->trieArray = 0;
fprintf(cm->stdOut, "%s %d conflicts are forwarded from distillation,\n",
cm->comment,
cm->each->nDistillObjConflictCl + cm->each->nDistillNonobjConflictCl);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_RestoreForwardedClauses | ( | satManager_t * | cm, |
| int | objectFlag | ||
| ) |
Function********************************************************************
Synopsis [ Restore conflict clauses to use them for current run]
Description [ Restore conflict clauses to use them for current run]
SideEffects [ ]
SeeAlso [ sat_SaveNonobjClauses sat_SaveAllClauses ]
fprintf(cm->stdOut, "%s %d clauses are forwarded by reststoring non-objective\n", cm->comment, total) ;
Definition at line 274 of file satInc.c.
{
int i, size;
int total;
long *space, c, *start;
satArray_t *saved;
satArray_t *clause;
//Bing
int NotCoi = 0, ct=0;
if(cm->option->checkNonobjForwarding) {
sat_CheckForwardedClauses(cm);
}
saved = cm->savedConflictClauses;
if(saved == 0)
return;
clause = sat_ArrayAlloc(50);
total = 0;
for(i=0, space=saved->space; i<saved->num; i++, space++){
if(*space < 0) {
space++;
i++;
start = space;
size = 0;
clause->num = 0;
//Bing:
NotCoi = 0;
while(*space > 0) {
sat_ArrayInsert(clause, SATnot((*space)));
//Bing:
if(!(SATflags(*space)&CoiMask)){
NotCoi = 1;
}
size++;
i++;
space++;
}
//Bing:
if(cm->option->AbRf){
if(!NotCoi){
c = sat_AddClauseIncremental(cm, clause, objectFlag, 0);
total++;
}
else
ct++;
}
else{
c = sat_AddClauseIncremental(cm, clause, objectFlag, 0);
total++;
}
}
}
sat_ArrayFree(clause);
sat_ArrayFree(saved);
cm->savedConflictClauses = 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_SaveAllClauses | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Save all conflict clauses]
Description [ When applying incremental SAT for BMC, one can forward all the clauses They are restored by sat_RestoreForwardedClauses ]
SideEffects [ ]
SeeAlso [ sat_RestoreForwardedClauses ]
if(cm->option->verbose > 1) { fprintf(cm->stdOut, "%s %d clauses are forwarded\n", cm->comment, total); }
Definition at line 494 of file satInc.c.
{
int limit, total, passed;
int size, j;
long *plit, nv, v, i;
satArray_t *savedArray;
savedArray = sat_ArrayAlloc(1024);
total = passed = 0;
limit = cm->option->incNumNonobjLitsLimit;
for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
if(SATreadInUse(i) == 0) continue;
size = SATnumLits(i);
total++;
plit = (long*)SATfirstLit(i);
nv = (*(plit-1));
sat_ArrayInsert(savedArray, nv);
for(j=0; j<size; j++, plit++) {
v = SATgetNode(*plit);
sat_ArrayInsert(savedArray, v);
}
sat_ArrayInsert(savedArray, nv);
}
cm->savedConflictClauses = savedArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_SaveNonobjClauses | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Save objective independent conflict clauses]
Description [ When applying incremental SAT, one has to save objective independent conflict clause They are restored by sat_RestoreForwardedClauses ]
SideEffects [ ]
SeeAlso [ sat_RestoreForwardedClauses ]
Definition at line 440 of file satInc.c.
{
int limit, total, passed;
int size, j;
long *plit, nv, v, i;
satArray_t *savedArray;
savedArray = sat_ArrayAlloc(1024);
total = passed = 0;
limit = cm->option->incNumNonobjLitsLimit;
for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
if(SATreadInUse(i) == 0) continue;
if(!(SATflags(i) & NonobjMask)) {
continue;
}
size = SATnumLits(i);
if(size > limit) {
total++;
}
else {
total++;
passed++;
plit = (long*)SATfirstLit(i);
nv = (*(plit-1));
sat_ArrayInsert(savedArray, nv);
for(j=0; j<size; j++, plit++) {
v = SATgetNode(*plit);
sat_ArrayInsert(savedArray, v);
}
sat_ArrayInsert(savedArray, nv);
}
}
if(cm->option->verbose > 1) {
fprintf(cm->stdOut, "%s %d NonObjective Clauses forwarded out of %d\n",
cm->comment, passed, total);
}
cm->savedConflictClauses = savedArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_TrieBasedImplication | ( | satManager_t * | cm, |
| satArray_t * | trieArray, | ||
| int | depth | ||
| ) |
Function********************************************************************
Synopsis [ Apply implication based on trie]
Description [ Apply implication based on trie]
SideEffects []
SeeAlso []
Definition at line 111 of file satInc.c.
{
int i;
satTrie_t *t;
satLevel_t *d;
satArray_t *tArray;
if(trieArray == 0) return;
for(i=0; i<trieArray->num; i++) {
t = (satTrie_t *)(trieArray->space[i]);
if(SATvalue(t->id) < 2) continue;
tArray = t->child[0];
if(tArray) {
d = sat_DecisionBasedOnTrie(cm, t->id, 0);
sat_ImplicationMain(cm, d);
if(d->conflict) {
sat_ConflictAnalysisOnTrie(cm, d);
}
else if(cm->status == 0) {
sat_TrieBasedImplication(cm, tArray, depth+1);
}
sat_Backtrack(cm, depth-1);
}
tArray = t->child[1];
if(tArray && cm->status == 0) {
d = sat_DecisionBasedOnTrie(cm, t->id, 1);
sat_ImplicationMain(cm, d);
if(d->conflict) {
sat_ConflictAnalysisOnTrie(cm, d);
}
else if(cm->status == 0) {
sat_TrieBasedImplication(cm, tArray, depth+1);
}
sat_Backtrack(cm, depth-1);
}
if(cm->status == SAT_BACKTRACK && depth == 1) {
cm->status = 0;
d = SATgetDecision(0);
sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
sat_ImplyArray(cm, d, cm->objUnitLitArray);
sat_MarkObjectiveFlagToArray(cm, cm->objUnitLitArray);
sat_ImplicationMain(cm, d);
if(d->conflict) {
cm->status = SAT_UNSAT;
return;
}
i--;
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int ScoreDistillCompare | ( | const void * | x, |
| const void * | y | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [ sort variable order based on occurrence to build Trie ]
Description [ sort variable order based on occurrence to build Trie ]
SideEffects [ ]
SeeAlso [ sat_BuildTrieForDistill ]
Definition at line 733 of file satInc.c.
{
int n1, n2;
int i1, i2;
satVariable_t v1, v2;
n1 = *(int *)x;
n2 = *(int *)y;
n1 >>= 2;
n2 >>= 2;
i1 = SATisInverted(n1);
n1 = SATnormalNode(n1);
i2 = SATisInverted(n2);
n2 = SATnormalNode(n2);
v1 = SatCm->variableArray[SATnodeID(n1)];
v2 = SatCm->variableArray[SATnodeID(n2)];
if(v1.scores[i1] == v2.scores[i2]) {
return(n1 > n2);
}
return(v1.scores[i1] < v2.scores[i2]);
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: satInc.c,v 1.16 2009/04/11 18:26:37 fabio Exp $" [static] |
CFile***********************************************************************
FileName [satInc.c]
PackageName [sat]
Synopsis [Routines for sat incremental function.]
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.]
