ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
rsbInt.h
Go to the documentation of this file.
1
20
21#ifndef ABC__bool_RsbInt_h
22#define ABC__bool_RsbInt_h
23
24
28
29#include <stdio.h>
30#include <stdlib.h>
31#include <string.h>
32#include <assert.h>
33
34#include "misc/vec/vec.h"
35#include "misc/util/utilTruth.h"
36#include "bool/kit/kit.h"
37#include "rsb.h"
38
42
44
48
49// truth table computation manager
51{
52 // parameters
53 int nLeafMax; // the max number of leaves of a cut
54 int nDivMax; // the max number of divisors to collect
55 int nDecMax; // the max number of decompositions
56 int fVerbose; // verbosity level
57 // decomposition
58 Vec_Wrd_t * vCexes; // counter-examples
59 Vec_Int_t * vDecPats; // decomposition patterns
60 Vec_Int_t * vFanins; // the result of decomposition
61 Vec_Int_t * vFaninsOld; // original fanins
62 Vec_Int_t * vTries; // intermediate
63};
64
68
72
73/*=== rsbMan.c ==========================================================*/
74
76
77
78
79#endif
80
84
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
INCLUDES ///.
Definition rsbInt.h:51
Vec_Int_t * vTries
Definition rsbInt.h:62
int fVerbose
Definition rsbInt.h:56
int nDecMax
Definition rsbInt.h:55
Vec_Wrd_t * vCexes
Definition rsbInt.h:58
Vec_Int_t * vFanins
Definition rsbInt.h:60
int nDivMax
Definition rsbInt.h:54
Vec_Int_t * vFaninsOld
Definition rsbInt.h:61
Vec_Int_t * vDecPats
Definition rsbInt.h:59
int nLeafMax
Definition rsbInt.h:53
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42