abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraClau.c File Reference
#include "fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"

Go to the source code of this file.

Data Structures

struct  Cla_Man_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Cla_Man_t_ 
Cla_Man_t
 DECLARATIONS ///. More...
 

Functions

Vec_Int_tFra_ClauSaveLatchVars (Aig_Man_t *pMan, Cnf_Dat_t *pCnf, int fCsVars)
 FUNCTION DEFINITIONS ///. More...
 
Vec_Int_tFra_ClauSaveOutputVars (Aig_Man_t *pMan, Cnf_Dat_t *pCnf)
 
Vec_Int_tFra_ClauSaveInputVars (Aig_Man_t *pMan, Cnf_Dat_t *pCnf, int nStarting)
 
int * Fra_ClauCreateMapping (Vec_Int_t *vSatVarsFrom, Vec_Int_t *vSatVarsTo, int nVarsMax)
 
void Fra_ClauStop (Cla_Man_t *p)
 
Cla_Man_tFra_ClauStart (Aig_Man_t *pMan)
 
static Vec_Int_tVec_IntSplitHalf (Vec_Int_t *vVec)
 
static void Vec_IntComplement (Vec_Int_t *vVec)
 
int Fra_ClauCheckProperty (Cla_Man_t *p, Vec_Int_t *vCex)
 
int Fra_ClauCheckBmc (Cla_Man_t *p, Vec_Int_t *vClause)
 
void Fra_ClauRemapClause (int *pMap, Vec_Int_t *vClause, Vec_Int_t *vRemapped, int fInv)
 
int Fra_ClauCheckClause (Cla_Man_t *p, Vec_Int_t *vClause, Vec_Int_t *vCex)
 
void Fra_ClauReduceClause (Vec_Int_t *vMain, Vec_Int_t *vNew)
 
void Fra_ClauMinimizeClause_rec (Cla_Man_t *p, Vec_Int_t *vBasis, Vec_Int_t *vExtra)
 
void Fra_ClauMinimizeClause (Cla_Man_t *p, Vec_Int_t *vBasis, Vec_Int_t *vExtra)
 
void Fra_ClauPrintClause (Vec_Int_t *vSatCsVars, Vec_Int_t *vCex)
 
int Fra_Clau (Aig_Man_t *pMan, int nIters, int fVerbose, int fVeryVerbose)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Cla_Man_t_ Cla_Man_t

DECLARATIONS ///.

CFile****************************************************************

FileName [fraClau.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Induction with clause strengthening.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

]

Definition at line 38 of file fraClau.c.

Function Documentation

int Fra_Clau ( Aig_Man_t pMan,
int  nIters,
int  fVerbose,
int  fVeryVerbose 
)

Function*************************************************************

Synopsis [Takes the AIG with the single output to be checked.]

Description []

SideEffects []

SeeAlso []

Definition at line 637 of file fraClau.c.

638 {
639  Cla_Man_t * p;
640  int Iter, RetValue, fFailed, i;
641  assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
642  // create the manager
643  p = Fra_ClauStart( pMan );
644  if ( p == NULL )
645  {
646  printf( "The property is trivially inductive.\n" );
647  return 1;
648  }
649  // generate counter-examples and expand them
650  for ( Iter = 0; !Fra_ClauCheckProperty( p, p->vCexMain0 ) && Iter < nIters; Iter++ )
651  {
652  if ( fVerbose )
653  printf( "%4d : ", Iter );
654  // remap clause into the test manager
655  Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 );
656  if ( fVerbose && fVeryVerbose )
657  Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
658  // the main counter-example is in p->vCexMain
659  // intermediate counter-examples are in p->vCexTest
660  // generate the reduced counter-example to the inductive property
661  fFailed = 0;
662  for ( i = 0; !Fra_ClauCheckClause( p, p->vCexMain, p->vCexTest ); i++ )
663  {
664  Fra_ClauReduceClause( p->vCexMain, p->vCexTest );
665  Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 );
666 
667 // if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
668  if ( Vec_IntSize(p->vCexMain) < 1 )
669  {
670  Vec_IntComplement( p->vCexMain0 );
671  RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexMain0), Vec_IntArray(p->vCexMain0) + Vec_IntSize(p->vCexMain0) );
672  if ( RetValue == 0 )
673  {
674  printf( "\nProperty is proved after %d iterations.\n", Iter+1 );
675  return 0;
676  }
677  fFailed = 1;
678  break;
679  }
680  }
681  if ( fFailed )
682  {
683  if ( fVerbose )
684  printf( " Reducing failed after %d iterations (BMC failed).\n", i );
685  continue;
686  }
687  if ( Vec_IntSize(p->vCexMain) == 0 )
688  {
689  if ( fVerbose )
690  printf( " Reducing failed after %d iterations (nothing left).\n", i );
691  continue;
692  }
693  if ( fVerbose )
694  printf( " " );
695  if ( fVerbose && fVeryVerbose )
696  Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
697  if ( fVerbose )
698  printf( " LitsInd = %3d. ", Vec_IntSize(p->vCexMain) );
699  // minimize the inductive property
700  Vec_IntClear( p->vCexBase );
701  if ( Vec_IntSize(p->vCexMain) > 1 )
702 // Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain );
703  Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
704  assert( Vec_IntSize(p->vCexMain) > 0 );
705  if ( fVerbose && fVeryVerbose )
706  Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
707  if ( fVerbose )
708  printf( " LitsRed = %3d. ", Vec_IntSize(p->vCexMain) );
709  if ( fVerbose )
710  printf( "\n" );
711  // add the clause to the solver
712  Fra_ClauRemapClause( p->pMapCsTestToCsMain, p->vCexMain, p->vCexAssm, 1 );
713  RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm) );
714  if ( RetValue == 0 )
715  {
716  Iter++;
717  break;
718  }
719  if ( p->pSatMain->qtail != p->pSatMain->qhead )
720  {
721  RetValue = sat_solver_simplify(p->pSatMain);
722  assert( RetValue != 0 );
723  assert( p->pSatMain->qtail == p->pSatMain->qhead );
724  }
725  }
726 
727  // report the results
728  if ( Iter == nIters )
729  {
730  printf( "Property is not proved after %d iterations.\n", nIters );
731  return 0;
732  }
733  printf( "Property is proved after %d iterations.\n", Iter );
734  Fra_ClauStop( p );
735  return 1;
736 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
void Fra_ClauMinimizeClause(Cla_Man_t *p, Vec_Int_t *vBasis, Vec_Int_t *vExtra)
Definition: fraClau.c:566
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Fra_ClauPrintClause(Vec_Int_t *vSatCsVars, Vec_Int_t *vCex)
Definition: fraClau.c:598
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
void Fra_ClauReduceClause(Vec_Int_t *vMain, Vec_Int_t *vNew)
Definition: fraClau.c:473
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int Fra_ClauCheckClause(Cla_Man_t *p, Vec_Int_t *vClause, Vec_Int_t *vCex)
Definition: fraClau.c:425
static void Vec_IntComplement(Vec_Int_t *vVec)
Definition: fraClau.c:327
void Fra_ClauStop(Cla_Man_t *p)
Definition: fraClau.c:178
Cla_Man_t * Fra_ClauStart(Aig_Man_t *pMan)
Definition: fraClau.c:211
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void Fra_ClauRemapClause(int *pMap, Vec_Int_t *vClause, Vec_Int_t *vRemapped, int fInv)
Definition: fraClau.c:402
typedefABC_NAMESPACE_IMPL_START struct Cla_Man_t_ Cla_Man_t
DECLARATIONS ///.
Definition: fraClau.c:38
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int Fra_ClauCheckProperty(Cla_Man_t *p, Vec_Int_t *vCex)
Definition: fraClau.c:345
int Fra_ClauCheckBmc ( Cla_Man_t p,
Vec_Int_t vClause 
)

Function*************************************************************

Synopsis [Checks if the clause holds using BMC.]

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file fraClau.c.

380 {
381  int nBTLimit = 0;
382  int RetValue;
383  RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause),
384  (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
385  if ( RetValue == l_False )
386  return 1;
387  assert( RetValue == l_True );
388  return 0;
389 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
#define l_True
Definition: SolverTypes.h:84
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define l_False
Definition: SolverTypes.h:85
#define assert(ex)
Definition: util_old.h:213
int Fra_ClauCheckClause ( Cla_Man_t p,
Vec_Int_t vClause,
Vec_Int_t vCex 
)

Function*************************************************************

Synopsis [Checks if the clause holds. Returns counter example if not.]

Description [Uses test SAT solver.]

SideEffects []

SeeAlso []

Definition at line 425 of file fraClau.c.

426 {
427  int nBTLimit = 0;
428  int RetValue, iVar, i;
429  // complement literals
430  Vec_IntPush( vClause, toLit( p->nSatVarsTestCur++ ) ); // helper positive
431  Vec_IntComplement( vClause ); // helper negative (the clause is C v h')
432  // add the clause
433  RetValue = sat_solver_addclause( p->pSatTest, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
434  assert( RetValue == 1 );
435  // complement all literals
436  Vec_IntPop( vClause ); // helper removed
437  Vec_IntComplement( vClause );
438  // create the assumption in terms of NS variables
439  Fra_ClauRemapClause( p->pMapCsTestToNsTest, vClause, p->vCexAssm, 0 );
440  // add helper literals
441  for ( i = p->nSatVarsTestBeg; i < p->nSatVarsTestCur - 1; i++ )
442  Vec_IntPush( p->vCexAssm, toLitCond(i,1) ); // other helpers negative
443  Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper
444  // try to solve
445  RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm),
446  (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
447  if ( vCex )
448  Vec_IntClear( vCex );
449  if ( RetValue == l_False )
450  return 1;
451  assert( RetValue == l_True );
452  if ( vCex )
453  {
454  Vec_IntForEachEntry( p->vSatVarsTestCs, iVar, i )
455  Vec_IntPush( vCex, sat_solver_var_literal(p->pSatTest, iVar) );
456  }
457  return 0;
458 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
#define l_True
Definition: SolverTypes.h:84
static lit toLit(int v)
Definition: satVec.h:142
static lit toLitCond(int v, int c)
Definition: satVec.h:143
static void Vec_IntComplement(Vec_Int_t *vVec)
Definition: fraClau.c:327
static int Vec_IntPop(Vec_Int_t *p)
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void Fra_ClauRemapClause(int *pMap, Vec_Int_t *vClause, Vec_Int_t *vRemapped, int fInv)
Definition: fraClau.c:402
static int sat_solver_var_literal(sat_solver *s, int v)
Definition: satSolver.h:205
#define l_False
Definition: SolverTypes.h:85
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Fra_ClauCheckProperty ( Cla_Man_t p,
Vec_Int_t vCex 
)

Function*************************************************************

Synopsis [Checks if the property holds. Returns counter-example if not.]

Description []

SideEffects []

SeeAlso []

Definition at line 345 of file fraClau.c.

346 {
347  int nBTLimit = 0;
348  int RetValue, iVar, i;
349  sat_solver_act_var_clear( p->pSatMain );
350  RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
351  Vec_IntClear( vCex );
352  if ( RetValue == l_False )
353  return 1;
354  assert( RetValue == l_True );
355  Vec_IntForEachEntry( p->vSatVarsMainCs, iVar, i )
356  Vec_IntPush( vCex, sat_solver_var_literal(p->pSatMain, iVar) );
357 /*
358  {
359  int i;
360  for (i = 0; i < p->pSatMain->size; i++)
361  printf( "%d=%d ", i, p->pSatMain->model.ptr[i] == l_True );
362  printf( "\n" );
363  }
364 */
365  return 0;
366 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
#define l_True
Definition: SolverTypes.h:84
static void sat_solver_act_var_clear(sat_solver *s)
Definition: satSolver.h:210
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int sat_solver_var_literal(sat_solver *s, int v)
Definition: satSolver.h:205
#define l_False
Definition: SolverTypes.h:85
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int* Fra_ClauCreateMapping ( Vec_Int_t vSatVarsFrom,
Vec_Int_t vSatVarsTo,
int  nVarsMax 
)

Function*************************************************************

Synopsis [Saves variables corresponding to latch outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 154 of file fraClau.c.

155 {
156  int * pMapping, Var, i;
157  assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) );
158  pMapping = ABC_ALLOC( int, nVarsMax );
159  for ( i = 0; i < nVarsMax; i++ )
160  pMapping[i] = -1;
161  Vec_IntForEachEntry( vSatVarsFrom, Var, i )
162  pMapping[Var] = Vec_IntEntry(vSatVarsTo,i);
163  return pMapping;
164 }
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int Var
Definition: SolverTypes.h:42
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Fra_ClauMinimizeClause ( Cla_Man_t p,
Vec_Int_t vBasis,
Vec_Int_t vExtra 
)

Function*************************************************************

Synopsis [Minimizes the clauses using a simple method.]

Description [The input and output clause are in vExtra.]

SideEffects []

SeeAlso []

Definition at line 566 of file fraClau.c.

567 {
568  int iLit, iLit2, i, k;
569  Vec_IntForEachEntryReverse( vExtra, iLit, i )
570  {
571  // copy literals without the given one
572  Vec_IntClear( vBasis );
573  Vec_IntForEachEntry( vExtra, iLit2, k )
574  if ( k != i )
575  Vec_IntPush( vBasis, iLit2 );
576  // try whether it is inductive
577  if ( !Fra_ClauCheckClause( p, vBasis, NULL ) )
578  continue;
579  // the clause is inductive
580  // remove the literal
581  for ( k = i; k < Vec_IntSize(vExtra)-1; k++ )
582  Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) );
583  Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 );
584  }
585 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define Vec_IntForEachEntryReverse(vVec, pEntry, i)
Definition: vecInt.h:62
for(p=first;p->value< newval;p=p->next)
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
int Fra_ClauCheckClause(Cla_Man_t *p, Vec_Int_t *vClause, Vec_Int_t *vCex)
Definition: fraClau.c:425
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Fra_ClauMinimizeClause_rec ( Cla_Man_t p,
Vec_Int_t vBasis,
Vec_Int_t vExtra 
)

Function*************************************************************

Synopsis [Computes the minimal invariant that holds.]

Description [On entrace, vBasis does not hold, vBasis+vExtra holds but is not minimal. On exit, vBasis is unchanged, vBasis+vExtra is minimal.]

SideEffects []

SeeAlso []

Definition at line 515 of file fraClau.c.

516 {
517  Vec_Int_t * vExtra2;
518  int nSizeOld;
519  if ( Vec_IntSize(vExtra) == 1 )
520  return;
521  nSizeOld = Vec_IntSize( vBasis );
522  vExtra2 = Vec_IntSplitHalf( vExtra );
523 
524  // try the first half
525  Vec_IntAppend( vBasis, vExtra );
526  if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
527  {
528  Vec_IntShrink( vBasis, nSizeOld );
529  Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
530  return;
531  }
532  Vec_IntShrink( vBasis, nSizeOld );
533 
534  // try the second half
535  Vec_IntAppend( vBasis, vExtra2 );
536  if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
537  {
538  Vec_IntShrink( vBasis, nSizeOld );
539  Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
540  return;
541  }
542 // Vec_IntShrink( vBasis, nSizeOld );
543 
544  // find the smallest with the second half added
545  Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
546  Vec_IntShrink( vBasis, nSizeOld );
547  Vec_IntAppend( vBasis, vExtra );
548  // find the smallest with the second half added
549  Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
550  Vec_IntShrink( vBasis, nSizeOld );
551  Vec_IntAppend( vExtra, vExtra2 );
552  Vec_IntFree( vExtra2 );
553 }
void Fra_ClauMinimizeClause_rec(Cla_Man_t *p, Vec_Int_t *vBasis, Vec_Int_t *vExtra)
Definition: fraClau.c:515
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int Fra_ClauCheckClause(Cla_Man_t *p, Vec_Int_t *vClause, Vec_Int_t *vCex)
Definition: fraClau.c:425
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static Vec_Int_t * Vec_IntSplitHalf(Vec_Int_t *vVec)
Definition: fraClau.c:304
void Fra_ClauPrintClause ( Vec_Int_t vSatCsVars,
Vec_Int_t vCex 
)

Function*************************************************************

Synopsis [Prints the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 598 of file fraClau.c.

599 {
600  int LitM, VarM, VarN, i, j, k;
601  assert( Vec_IntSize(vCex) <= Vec_IntSize(vSatCsVars) );
602  for ( i = j = k = 0; i < Vec_IntSize(vCex) && j < Vec_IntSize(vSatCsVars); )
603  {
604  LitM = Vec_IntEntry( vCex, i );
605  VarM = lit_var( LitM );
606  VarN = Vec_IntEntry( vSatCsVars, j );
607  if ( VarM < VarN )
608  {
609  assert( 0 );
610  }
611  else if ( VarM > VarN )
612  {
613  j++;
614  printf( "-" );
615  }
616  else // if ( VarM == VarN )
617  {
618  i++;
619  j++;
620  printf( "%d", !lit_sign(LitM) );
621  }
622  }
623  assert( i == Vec_IntSize(vCex) );
624 }
static int lit_var(lit l)
Definition: satVec.h:145
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int lit_sign(lit l)
Definition: satVec.h:146
#define assert(ex)
Definition: util_old.h:213
void Fra_ClauReduceClause ( Vec_Int_t vMain,
Vec_Int_t vNew 
)

Function*************************************************************

Synopsis [Reduces the counter-example by removing complemented literals.]

Description [Removes literals from vMain that differ from those in the counter-example (vNew). Relies on the fact that the PI variables are assigned in the increasing order.]

SideEffects []

SeeAlso []

Definition at line 473 of file fraClau.c.

474 {
475  int LitM, LitN, VarM, VarN, i, j, k;
476  assert( Vec_IntSize(vMain) <= Vec_IntSize(vNew) );
477  for ( i = j = k = 0; i < Vec_IntSize(vMain) && j < Vec_IntSize(vNew); )
478  {
479  LitM = Vec_IntEntry( vMain, i );
480  LitN = Vec_IntEntry( vNew, j );
481  VarM = lit_var( LitM );
482  VarN = lit_var( LitN );
483  if ( VarM < VarN )
484  {
485  assert( 0 );
486  }
487  else if ( VarM > VarN )
488  {
489  j++;
490  }
491  else // if ( VarM == VarN )
492  {
493  i++;
494  j++;
495  if ( LitM == LitN )
496  Vec_IntWriteEntry( vMain, k++, LitM );
497  }
498  }
499  assert( i == Vec_IntSize(vMain) );
500  Vec_IntShrink( vMain, k );
501 }
static int lit_var(lit l)
Definition: satVec.h:145
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
#define assert(ex)
Definition: util_old.h:213
void Fra_ClauRemapClause ( int *  pMap,
Vec_Int_t vClause,
Vec_Int_t vRemapped,
int  fInv 
)

Function*************************************************************

Synopsis [Lifts the clause to depend on NS variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file fraClau.c.

403 {
404  int iLit, i;
405  Vec_IntClear( vRemapped );
406  Vec_IntForEachEntry( vClause, iLit, i )
407  {
408  assert( pMap[lit_var(iLit)] >= 0 );
409  iLit = toLitCond( pMap[lit_var(iLit)], lit_sign(iLit) ^ fInv );
410  Vec_IntPush( vRemapped, iLit );
411  }
412 }
static int lit_var(lit l)
Definition: satVec.h:145
static lit toLitCond(int v, int c)
Definition: satVec.h:143
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int lit_sign(lit l)
Definition: satVec.h:146
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Int_t* Fra_ClauSaveInputVars ( Aig_Man_t pMan,
Cnf_Dat_t pCnf,
int  nStarting 
)

Function*************************************************************

Synopsis [Saves variables corresponding to latch outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file fraClau.c.

129 {
130  Vec_Int_t * vVars;
131  Aig_Obj_t * pObj;
132  int i;
133  vVars = Vec_IntAlloc( Aig_ManCiNum(pMan) - nStarting );
134  Aig_ManForEachCi( pMan, pObj, i )
135  {
136  if ( i < nStarting )
137  continue;
138  Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
139  }
140  return vVars;
141 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int * pVarNums
Definition: cnf.h:63
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
int Id
Definition: aig.h:85
Vec_Int_t* Fra_ClauSaveLatchVars ( Aig_Man_t pMan,
Cnf_Dat_t pCnf,
int  fCsVars 
)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Saves variables corresponding to latch outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file fraClau.c.

85 {
86  Vec_Int_t * vVars;
87  Aig_Obj_t * pObjLo, * pObjLi;
88  int i;
89  vVars = Vec_IntAlloc( Aig_ManRegNum(pMan) );
90  Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
91  Vec_IntPush( vVars, pCnf->pVarNums[fCsVars? pObjLo->Id : pObjLi->Id] );
92  return vVars;
93 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_Int_t* Fra_ClauSaveOutputVars ( Aig_Man_t pMan,
Cnf_Dat_t pCnf 
)

Function*************************************************************

Synopsis [Saves variables corresponding to latch outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file fraClau.c.

107 {
108  Vec_Int_t * vVars;
109  Aig_Obj_t * pObj;
110  int i;
111  vVars = Vec_IntAlloc( Aig_ManCoNum(pMan) );
112  Aig_ManForEachCo( pMan, pObj, i )
113  Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
114  return vVars;
115 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cla_Man_t* Fra_ClauStart ( Aig_Man_t pMan)

Function*************************************************************

Synopsis [Takes the AIG with the single output to be checked.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file fraClau.c.

212 {
213  Cla_Man_t * p;
214  Cnf_Dat_t * pCnfMain;
215  Cnf_Dat_t * pCnfTest;
216  Cnf_Dat_t * pCnfBmc;
217  Aig_Man_t * pFramesMain;
218  Aig_Man_t * pFramesTest;
219  Aig_Man_t * pFramesBmc;
220  assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
221 
222  // start the manager
223  p = ABC_ALLOC( Cla_Man_t, 1 );
224  memset( p, 0, sizeof(Cla_Man_t) );
225  p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) );
226  p->vCexMain = Vec_IntAlloc( Aig_ManRegNum(pMan) );
227  p->vCexTest = Vec_IntAlloc( Aig_ManRegNum(pMan) );
228  p->vCexBase = Vec_IntAlloc( Aig_ManRegNum(pMan) );
229  p->vCexAssm = Vec_IntAlloc( Aig_ManRegNum(pMan) );
230  p->vCexBmc = Vec_IntAlloc( Aig_ManRegNum(pMan) );
231 
232  // derive two timeframes to be checked
233  pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs
234 //Aig_ManShow( pFramesMain, 0, NULL );
235  assert( Aig_ManCoNum(pFramesMain) == 2 );
236  Aig_ObjChild0Flip( Aig_ManCo(pFramesMain, 0) ); // complement the first output
237  pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
238 //Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
239  p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
240 /*
241  {
242  int i;
243  Aig_Obj_t * pObj;
244  Aig_ManForEachObj( pFramesMain, pObj, i )
245  printf( "%d -> %d \n", pObj->Id, pCnfMain->pVarNums[pObj->Id] );
246  printf( "\n" );
247  }
248 */
249 
250  // derive one timeframe to be checked
251  pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL );
252  assert( Aig_ManCoNum(pFramesTest) == Aig_ManRegNum(pMan) );
253  pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
254  p->pSatTest = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
255  p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
256 
257  // derive one timeframe to be checked for BMC
258  pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL );
259 //Aig_ManShow( pFramesBmc, 0, NULL );
260  assert( Aig_ManCoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
261  pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
262  p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
263 
264  // create variable sets
265  p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManCiNum(pMan)-Aig_ManRegNum(pMan)) );
266  p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 );
267  p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 );
268  p->vSatVarsBmcNs = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc );
269  assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsMainCs) );
270  assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsBmcNs) );
271 
272  // create mapping of CS into NS vars
273  p->pMapCsMainToCsTest = Fra_ClauCreateMapping( p->vSatVarsMainCs, p->vSatVarsTestCs, Aig_ManObjNumMax(pFramesMain) );
274  p->pMapCsTestToCsMain = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsMainCs, Aig_ManObjNumMax(pFramesTest) );
275  p->pMapCsTestToNsTest = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsTestNs, Aig_ManObjNumMax(pFramesTest) );
276  p->pMapCsTestToNsBmc = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsBmcNs, Aig_ManObjNumMax(pFramesTest) );
277 
278  // cleanup
279  Cnf_DataFree( pCnfMain );
280  Cnf_DataFree( pCnfTest );
281  Cnf_DataFree( pCnfBmc );
282  Aig_ManStop( pFramesMain );
283  Aig_ManStop( pFramesTest );
284  Aig_ManStop( pFramesBmc );
285  if ( p->pSatMain == NULL || p->pSatTest == NULL || p->pSatBmc == NULL )
286  {
287  Fra_ClauStop( p );
288  return NULL;
289  }
290  return p;
291 }
char * memset()
Vec_Int_t * Fra_ClauSaveLatchVars(Aig_Man_t *pMan, Cnf_Dat_t *pCnf, int fCsVars)
FUNCTION DEFINITIONS ///.
Definition: fraClau.c:84
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Vec_Int_t * Fra_ClauSaveInputVars(Aig_Man_t *pMan, Cnf_Dat_t *pCnf, int nStarting)
Definition: fraClau.c:128
Definition: cnf.h:56
Aig_Man_t * Aig_ManFrames(Aig_Man_t *pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t ***ppObjMap)
FUNCTION DEFINITIONS ///.
Definition: aigFrames.c:51
Vec_Int_t * Fra_ClauSaveOutputVars(Aig_Man_t *pMan, Cnf_Dat_t *pCnf)
Definition: fraClau.c:106
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
void Fra_ClauStop(Cla_Man_t *p)
Definition: fraClau.c:178
static void Aig_ObjChild0Flip(Aig_Obj_t *pObj)
Definition: aig.h:316
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
typedefABC_NAMESPACE_IMPL_START struct Cla_Man_t_ Cla_Man_t
DECLARATIONS ///.
Definition: fraClau.c:38
int * Fra_ClauCreateMapping(Vec_Int_t *vSatVarsFrom, Vec_Int_t *vSatVarsTo, int nVarsMax)
Definition: fraClau.c:154
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
#define assert(ex)
Definition: util_old.h:213
void Fra_ClauStop ( Cla_Man_t p)

Function*************************************************************

Synopsis [Deletes the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file fraClau.c.

179 {
180  ABC_FREE( p->pMapCsMainToCsTest );
181  ABC_FREE( p->pMapCsTestToCsMain );
182  ABC_FREE( p->pMapCsTestToNsTest );
183  ABC_FREE( p->pMapCsTestToNsBmc );
184  Vec_IntFree( p->vSatVarsMainCs );
185  Vec_IntFree( p->vSatVarsTestCs );
186  Vec_IntFree( p->vSatVarsTestNs );
187  Vec_IntFree( p->vSatVarsBmcNs );
188  Vec_IntFree( p->vCexMain0 );
189  Vec_IntFree( p->vCexMain );
190  Vec_IntFree( p->vCexTest );
191  Vec_IntFree( p->vCexBase );
192  Vec_IntFree( p->vCexAssm );
193  Vec_IntFree( p->vCexBmc );
194  if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
195  if ( p->pSatTest ) sat_solver_delete( p->pSatTest );
196  if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
197  ABC_FREE( p );
198 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
#define ABC_FREE(obj)
Definition: abc_global.h:232
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntComplement ( Vec_Int_t vVec)
static

Function*************************************************************

Synopsis [Complements all literals in the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file fraClau.c.

328 {
329  int i;
330  for ( i = 0; i < Vec_IntSize(vVec); i++ )
331  vVec->pArray[i] = lit_neg( vVec->pArray[i] );
332 }
static lit lit_neg(lit l)
Definition: satVec.h:144
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Vec_Int_t* Vec_IntSplitHalf ( Vec_Int_t vVec)
static

Function*************************************************************

Synopsis [Splits off second half and returns it as a new vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 304 of file fraClau.c.

305 {
306  Vec_Int_t * vPart;
307  int Entry, i;
308  assert( Vec_IntSize(vVec) > 1 );
309  vPart = Vec_IntAlloc( Vec_IntSize(vVec) / 2 + 1 );
310  Vec_IntForEachEntryStart( vVec, Entry, i, Vec_IntSize(vVec) / 2 )
311  Vec_IntPush( vPart, Entry );
312  Vec_IntShrink( vVec, Vec_IntSize(vVec) / 2 );
313  return vPart;
314 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
#define assert(ex)
Definition: util_old.h:213