Index: vis_dev/vis-2.3/models/debug/and2.ltl
===================================================================
--- vis_dev/vis-2.3/models/debug/and2.ltl (revision 40)
+++ vis_dev/vis-2.3/models/debug/and2.ltl (revision 41)
@@ -1,1 +1,1 @@
-X(c = 1);
+X(c = 0);
Index: vis_dev/vis-2.3/models/debug/test.script
===================================================================
--- vis_dev/vis-2.3/models/debug/test.script (revision 40)
+++ vis_dev/vis-2.3/models/debug/test.script (revision 41)
@@ -1,5 +1,5 @@
-rlmv and2.mv
+rlmv new_and.mv
init
_createAbn
aig
-_sat_debug -k 1 -p and2.ltl -o and2_prop.cnf -v 1
+_sat_debug -k 1 -v 1 -o new_and_prop.cnf and2.ltl
Index: vis_dev/vis-2.3/src/bmc/bmcInt.h
===================================================================
--- vis_dev/vis-2.3/src/bmc/bmcInt.h (revision 40)
+++ vis_dev/vis-2.3/src/bmc/bmcInt.h (revision 41)
@@ -184,5 +184,5 @@
EXTERN Ltl_Automaton_t * BmcAutLtlToAutomaton(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula);
EXTERN void BmcAutTerminationFree(BmcCheckForTermination_t *result);
-EXTERN int BmcBddSat(Ntk_Network_t *network, array_t *formulaArray, BmcOption_t *options);
+EXTERN int BmcBddSat(Ntk_Network_t *network, array_t *formulaArray, BmcOption_t *savons);
EXTERN Bmc_PropertyStatus BmcBddSatCheckLtlFormula(Ntk_Network_t *network, mdd_t *initialStates, mdd_t *targetStates, BmcOption_t *options, st_table *CoiTable);
EXTERN void BmcLtlVerifyProp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options);
Index: vis_dev/vis-2.3/src/debug/debug.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debug.c (revision 40)
+++ vis_dev/vis-2.3/src/debug/debug.c (revision 41)
@@ -65,4 +65,5 @@
static int CommandTransition(Hrc_Manager_t ** hmgr,int argc, char ** argv);
static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv);
+static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv);
@@ -94,4 +95,5 @@
Cmd_CommandAdd("_sat_debug", CommandSatDebug, 0);
Cmd_CommandAdd("_createAbn", CommandCreateAbnormal, 1);
+ Cmd_CommandAdd("print_network_cnf", CommandGenerateNetworkCNF, 0);
}
@@ -176,27 +178,4 @@
******************************************************************************/
-static int
-checkIndex(
- int index,
- BmcCnfClauses_t *cnfClauses)
-{
- int rtnValue = -1; /* it is not TRUE or FALSE*/
-
- if (index == 0){ /* TRUE or FALSE*/
- if (cnfClauses->emptyClause){ /* last added clause was empty = FALSE*/
- rtnValue = 0; /* FALSE */
- } else {
- /*
- if (cnfClauses->noOfClauses == 0)
- rtnValue = 1;
- }
- */
- rtnValue = 1; /* TRUE */
- }
- }
- return rtnValue;
-}
-
-
static int
CommandSatDebug(
@@ -206,145 +185,71 @@
int c,i;
int verbose = 0; /* default value */
-BmcOption_t *options = BmcOptionAlloc();
-Ntk_Network_t * network;
-bAig_Manager_t *manager;
-array_t *formulaArray;
-array_t *LTLformulaArray;
-char *ltlFileName = NIL(char);
+BmcOption_t * options = BmcOptionAlloc();
+Ntk_Network_t * network;
+bAig_Manager_t * manager;
+array_t * formulaArray;
+array_t * LTLformulaArray;
+char * ltlFileName = NIL(char);
+
/*
* Parse command line options.
*/
-util_getopt_reset();
-while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) {
- switch(c) {
- case 'v':
- verbose = 1;
- options->verbosityLevel = verbose;
- break;
- case 'h':
- goto usage;
- case 'm':
- for (i = 0; i < strlen(util_optarg); i++) {
- if (!isdigit((int)util_optarg[i])) {
- goto usage;
- }
- }
- options->minK = atoi(util_optarg);
- break;
- case 'k':
- for (i = 0; i < strlen(util_optarg); i++) {
- if (!isdigit((int)util_optarg[i])) {
- goto usage;
- }
- }
- options->maxK = atoi(util_optarg);
- break;
- case 'o':
- options->cnfFileName = util_strsav(util_optarg);
- break;
- case 'p':
- ltlFileName = util_strsav(util_optarg);
- break;
-
- default:
- goto usage;
- }
-}
+if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
+ return 1;
+}
+
+
printf("MAX K %d", options->maxK);
- if (options->minK > options->maxK){
- (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");
- goto usage;
- }
if (verbose) {
(void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
}
- /* create SAT Solver input file */
- if (options->cnfFileName == NIL(char)) {
- options->satInFile = BmcCreateTmpFile();
-}
- else {
- options->satInFile = options->cnfFileName;
- }
-
-/* create SAT Solver output file */
-options->satOutFile = BmcCreateTmpFile();
-if (options->satOutFile == NIL(char)){
+/*
+ * Read the network
+ */
+network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+if (network == NIL(Ntk_Network_t)) {
+ (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
BmcOptionFree(options);
- (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
return 1;
}
-
-options->verbosityLevel = 1;
-//options->satSolver
-//options->clauses
-
- /*
- * Read the network
- */
- network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
- if (network == NIL(Ntk_Network_t)) {
- (void) fprintf(vis_stdout, "** bmc error: No network\n");
- BmcOptionFree(options);
- return 1;
- }
- manager = Ntk_NetworkReadMAigManager(network);
- if (manager == NIL(mAig_Manager_t)) {
- (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
- BmcOptionFree(options);
- return 1;
- }
-
- /*
- We need the bdd when building the transition relation of the automaton
- */
- if(options->inductiveStep !=0){
- Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
-
- designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
- if (designFsm == NIL(Fsm_Fsm_t)) {
- (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
- return 1;
- }
- }
+manager = Ntk_NetworkReadMAigManager(network);
+if (manager == NIL(mAig_Manager_t)) {
+ (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
+ BmcOptionFree(options);
+ return 1;
+}
+
Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
-printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
-/*
- * Read the formula
- */
- /* Read LTL Formulae */
- if (!ltlFileName)
- goto usage;
-
- options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
- if (options->ltlFile == NIL(FILE)) {
- (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
- FREE(ltlFileName);
- BmcOptionFree(options);
- }
- FREE(ltlFileName);
-
- formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
- if (formulaArray == NIL(array_t)) {
- (void) fprintf(vis_stderr,
- "** bmc error: error in parsing CTL* Fromula from file\n");
- BmcOptionFree(options);
- return 1;
- }
- if (array_n(formulaArray) == 0) {
- (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
- BmcOptionFree(options);
- Ctlsp_FormulaArrayFree(formulaArray);
- return 1;
- }
- LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
+if(abn == NIL(Dbg_Abnormal_t)){
+ (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
+ return 1;
+}
+if(verbose)
+ printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
+
+
+formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
+if (formulaArray == NIL(array_t)) {
+ (void) fprintf(vis_stderr,
+ "** bmc error: error in parsing CTL* Fromula from file\n");
+ BmcOptionFree(options);
+ return 1;
+}
+if (array_n(formulaArray) == 0) {
+ (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
+ BmcOptionFree(options);
Ctlsp_FormulaArrayFree(formulaArray);
- if (LTLformulaArray == NIL(array_t)){
- (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
- BmcOptionFree(options);
- return 1;
- }
- Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
+ return 1;
+}
+LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
+Ctlsp_FormulaArrayFree(formulaArray);
+if (LTLformulaArray == NIL(array_t)){
+ (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
+ BmcOptionFree(options);
+ return 1;
+}
+Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
@@ -353,4 +258,5 @@
Compute the cone of influence
here : a list of state variables (latches)
+ TODO refine to COI of the property
*/
st_table *CoiTable = generateAllLatches(network);
@@ -359,33 +265,12 @@
clauses in BMC.
*/
- st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
- BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
- FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
- /*
- nodeToMvfAigTable maps each node to its multi-function And/Inv graph
- */
- nodeToMvfAigTable =
- (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
- assert(nodeToMvfAigTable != NIL(st_table));
-
- if(verbose)
+ if(verbose)
{
- (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
- printLatch(nodeToMvfAigTable);
(void) fprintf(vis_stdout, "------ COI ----\n");
printLatch(CoiTable);
(void) fprintf(vis_stdout, "--------------------------\n");
}
- /*
- Create a clause database
- */
- cnfClauses = BmcCnfClausesAlloc();
- /*
- Generate clauses for an initialized path of length k
- */
- Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
- fprintf(vis_stdout, "\n");
- BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
- cnfClauses, nodeToMvfAigTable, CoiTable);
+ BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable);
+
//Generate ltl CNF
@@ -393,4 +278,6 @@
// aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
// cf. BmcLtlVerifyGeneralLtl
+ Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
+ fprintf(vis_stdout, "\n");
int k = options->maxK;
int l;
@@ -398,6 +285,5 @@
int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
- int leftValue = checkIndex(noLoopIndex, cnfClauses);
- printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue);
+
array_t *objClause = NIL(array_t);
objClause = array_alloc(int, 0);
@@ -406,10 +292,33 @@
array_free(objClause);
-
-//TODO Add abnormal formula
-
-
-
-
+ //Add Abnormal
+ st_table * nodeToMvfAigTable = NIL(st_table);
+ nodeToMvfAigTable =
+(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+assert(nodeToMvfAigTable != NIL(st_table));
+
+ Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
+
+ //loop abnormal
+ int aIndex;
+ Ntk_Node_t * abnNode;
+ Dbg_ForEachAbnormal(abn,aIndex,abnNode){
+ if(aIndex<=0){
+ //set abnormal
+ int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
+ bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
+ int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
+ array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
+
+ FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
+ BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+ fclose(cnfFile);
+
+ //SAT procedure
+ int res = Dbg_SatCheck("assig",options->cnfFileName);
+
+ array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
+ }
+ }
if(verbose)
@@ -417,22 +326,150 @@
latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
- Ctlsp_FormulaArrayFree(LTLformulaArray);
- BmcWriteClauses(manager, cnfFile, cnfClauses, options);
-fclose(cnfFile);
+Ctlsp_FormulaArrayFree(LTLformulaArray);
BmcCnfClausesFree(cnfClauses);
BmcOptionFree(options);
return 0;
- usage:
- (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
- minimum length] [-o cnf_file] [-p ltl_file]\n");
- (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
- (void) fprintf(vis_stderr, " -v\t\tverbose\n");
- (void) fprintf(vis_stderr, " -m \tminimum length of counterexample to be checked (default is 0)\n");
+
+}
+/**Function********************************************************************
+
+ Synopsis [Implements the generate_network_cnf.]
+
+ CommandName [generate_network_cnf]
+
+ CommandSynopsis [generate a CNF view of the network]
+
+ CommandArguments [\[-h\] \[-v\] \[-k\] [fileName] ]
+
+ CommandDescription [This command geerate a CNF of the network in DMACS form.
+ The network may be unroll within k steps.
+
+
+ Command options:
+
+
+ - -h
+
- Print the command usage.
+
+
+ -v
+ Verbose mode.
+
+
+ -k
+ number of steps (default 1).
+
+ ]
+
+ SideEffects []
+
+******************************************************************************/
+
+static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv)
+{
+ BmcOption_t *options = BmcOptionAlloc();
+ int c;
+ unsigned int i;
+ Ntk_Network_t * network;
+ bAig_Manager_t * manager;
+ char * outName = NIL(char);
+ FILE *cnfFile;
+ if (!options){
+ return 1;
+ }
+ options->dbgOut = 0;
+ /*
+ * Parse command line options.
+ */
+ util_getopt_reset();
+ while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
+ switch(c) {
+ case 'h':
+ goto usage;
+ case 'k':
+ options->maxK = atoi(util_optarg);
+ break;
+ case 'v':
+ for (i = 0; i < strlen(util_optarg); i++) {
+ if (!isdigit((int)util_optarg[i])) {
+ goto usage;
+ }
+ }
+ options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
+ break;
+ default:
+ goto usage;
+ }
+ }
+ if (argc - util_optind != 0)
+ {
+ outName = util_strsav(argv[util_optind]);
+ /* create SAT Solver input file */
+ options->cnfFileName= outName;
+ options->satInFile = options->cnfFileName;
+ cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
+ }
+
+
+/*
+ * Read the network
+ */
+network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+if (network == NIL(Ntk_Network_t)) {
+ (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
+ BmcOptionFree(options);
+ return 1;
+}
+manager = Ntk_NetworkReadMAigManager(network);
+if (manager == NIL(mAig_Manager_t)) {
+ (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
+ BmcOptionFree(options);
+ return 1;
+}
+
+ /*
+ Compute the cone of influence
+ here : a list of state variables (latches)
+ */
+st_table *CoiTable = generateAllLatches(network);
+
+if(options->verbosityLevel)
+{
+ (void) fprintf(vis_stdout, "------ COI ----\n");
+ printLatch(CoiTable);
+ (void) fprintf(vis_stdout, "--------------------------\n");
+}
+BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable);
+ if(outName != NIL(char))
+ {
+ BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+ fclose(cnfFile);
+ }
+ else
+ BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
+
+if(options->verbosityLevel)
+{
+ (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
+ (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
+ st_count(CoiTable));
+}
+
+BmcOptionFree(options);
+ return 0;
+ usage:
+ (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] \n");
+ (void) fprintf(vis_stderr, " -h \tprint the command usage\n");
(void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n");
- (void) fprintf(vis_stderr, " -o contains CNF of the debug instance\n");
- (void) fprintf(vis_stderr, " -p contains the ltl formula\n");
- return 1; /* error exit */
-
-}
+ (void) fprintf(vis_stderr, " -v \n");
+ (void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n");
+ (void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n");
+ (void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n");
+ (void) fprintf(vis_stderr, " The output file containing CNF of the network.\n");
+
+ BmcOptionFree(options);
+ return 1;
+}
+
/**Function********************************************************************
Index: vis_dev/vis-2.3/src/debug/debug.h
===================================================================
--- vis_dev/vis-2.3/src/debug/debug.h (revision 40)
+++ vis_dev/vis-2.3/src/debug/debug.h (revision 41)
@@ -132,4 +132,12 @@
EXTERN array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal);
EXTERN Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network);
+EXTERN void Dbg_InitAbn(Dbg_Abnormal_t * abn, bAig_Manager_t * manager,
+st_table * nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses);
+EXTERN int Dbg_SatCheck(char * forceAssigName, char * cnfFileName);
+EXTERN BmcCnfClauses_t* Dbg_GenerateCNF(Ntk_Network_t * network,
+BmcOption_t * option, st_table *CoiTable);
+
+
+
/**AutomaticEnd***************************************************************/
Index: vis_dev/vis-2.3/src/debug/debugAbnormal.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debugAbnormal.c (revision 40)
+++ vis_dev/vis-2.3/src/debug/debugAbnormal.c (revision 41)
@@ -138,4 +138,6 @@
abn->abnormal = array_alloc(Ntk_Node_t*,0);
abn->freeInputs = array_alloc(Ntk_Node_t*,0);
+ abn->abnAigArray = NIL(array_t);
+ abn->abnCnfIndexArray = NIL(array_t);
abn->verbose = 0;
return abn;
@@ -158,4 +160,6 @@
array_free(abn->abnormal);
array_free(abn->freeInputs);
+ array_free(abn->abnCnfIndexArray);
+ array_free(abn->abnAigArray);
FREE(abn);
}
@@ -267,2 +271,64 @@
return abn;
}
+/**Function********************************************************************
+
+ Synopsis [Initialize the abnormal predicate in the clauses array abni =0]
+
+ Description [Fill the Dbg data structure, abnAigArray conains the set of Aig
+ for the set of abnormal perdicate. Each abnormal are set to zero in the clause
+ array.predicabnCnfIndexArray is the cnf index. The correspondance is made by
+ the index in the table, the index of a node in abnArray is the same in
+ abnAigArray and in abnIndexArray. If this array were alredy computed nothing
+ is done, if the aig or index information either.]
+
+ SideEffects [Fill abnAigArray and abnCnfIndexArray]
+
+ SeeAlso []
+
+******************************************************************************/
+void Dbg_InitAbn(Dbg_Abnormal_t * abn,
+bAig_Manager_t * manager,
+st_table * nodeToMvfAigTable,
+BmcCnfClauses_t *cnfClauses)
+{
+ if(abn->abnAigArray != NIL(array_t))
+ (void) fprintf(vis_stdout, "Abnormal aig alredy filled\n");
+ if(abn->abnCnfIndexArray != NIL(array_t)){
+ (void) fprintf(vis_stdout, "Abnormal index alredy filled\n");
+ return;
+ }
+ //Fill
+ int size = array_n(abn->abnormal);
+ array_t * abnAigArray = array_alloc(bAigEdge_t *,size);
+ array_t * abnIndexArray = array_alloc(int,size);
+ int aIndex;
+ Ntk_Node_t * abnNode;
+ Dbg_ForEachAbnormal(abn, aIndex,abnNode){
+ MvfAig_Function_t * abnMvfAig = Bmc_ReadMvfAig(abnNode, nodeToMvfAigTable);
+ if (abnMvfAig == NIL(MvfAig_Function_t)){
+ (void) fprintf(vis_stdout, "No multi-valued function for this node %s \
+ create abnormal predicate firs \n", Ntk_NodeReadName(abnNode));
+ return ;
+ }
+ int mvfSize = array_n(abnMvfAig);
+ int i;
+ bAigEdge_t * abnBAig = ALLOC(bAigEdge_t, mvfSize);
+
+ for(i=0; i< mvfSize; i++)
+ {
+ abnBAig[i] = bAig_GetCanonical(manager,
+ MvfAig_FunctionReadComponent(abnMvfAig, i));
+ }
+ array_insert(bAigEdge_t*,abnAigArray,aIndex,abnBAig);
+ int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],0,cnfClauses);
+ array_insert(int,abnIndexArray,aIndex,cnfClauses->nextIndex);
+ // Create clause
+ array_t *abnClause = NIL(array_t);
+ abnClause = array_alloc(int, 0);
+ array_insert_last(int, abnClause, abnIndex);
+ BmcCnfInsertClause(cnfClauses, abnClause);
+ array_free(abnClause);
+ }
+ abn->abnAigArray = abnAigArray;
+ abn->abnCnfIndexArray = abnIndexArray;
+}
Index: vis_dev/vis-2.3/src/debug/debugInt.h
===================================================================
--- vis_dev/vis-2.3/src/debug/debugInt.h (revision 40)
+++ vis_dev/vis-2.3/src/debug/debugInt.h (revision 41)
@@ -55,4 +55,6 @@
array_t * abnormal; /* Array of Ntk_Node_t* */
array_t * freeInputs; /* Array of Ntk_Node_t* */
+ array_t * abnAigArray; /* Array of bAigEdge_t* as many entries as possible value */
+ array_t * abnCnfIndexArray; /* Array of int */
int verbose;
};
Index: vis_dev/vis-2.3/src/debug/debugUtilities.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debugUtilities.c (revision 40)
+++ vis_dev/vis-2.3/src/debug/debugUtilities.c (revision 41)
@@ -87,2 +87,107 @@
return;
}
+/**Function********************************************************************
+
+ Synopsis [Performs the sat call]
+
+ Description [Retrun the result of SAT call, avec positionnement des options]
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+
+int Dbg_SatCheck(char * forceAssigName, char * cnfFileName
+)
+{
+ satManager_t *cm;
+ cm = sat_InitManager(0);
+ cm->comment = ALLOC(char, 2);
+ cm->comment[0] = ' ';
+ cm->comment[1] = '\0';
+ cm->stdOut = stdout;
+ cm->stdErr = stderr;
+
+
+ satOption_t *satOption;
+ array_t *result = NIL(array_t);
+ int maxSize;
+
+ satOption = sat_InitOption();
+ satOption->verbose = 2;
+ //satOption->unsatCoreFileName = "Ucore.txt";
+ satOption->clauseDeletionHeuristic = 0;
+ //satOption->coreGeneration = 1 ;
+ //satOption->minimizeConflictClause = 1;
+ if(forceAssigName != NULL)
+ satOption->forcedAssignArr = sat_ReadForcedAssignment(forceAssigName);
+ cm->option = satOption;
+ cm->each = sat_InitStatistics();
+
+ cm->unitLits = sat_ArrayAlloc(16);
+ cm->pureLits = sat_ArrayAlloc(16);
+
+ maxSize = 1024 << 8;
+ cm->nodesArray = ALLOC(long, maxSize);
+ cm->maxNodesArraySize = maxSize;
+ cm->nodesArraySize = satNodeSize;
+
+ sat_AllocLiteralsDB(cm);
+
+ sat_ReadCNF(cm,cnfFileName);
+ sat_Main(cm);
+
+ if(cm->status == SAT_UNSAT) {
+ if(cm->option->forcedAssignArr)
+ fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
+ cm->comment);
+ fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
+ fflush(cm->stdOut);
+ sat_ReportStatistics(cm, cm->each);
+ sat_FreeManager(cm);
+ }
+ else if(cm->status == SAT_SAT) {
+ fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
+ fflush(cm->stdOut);
+ sat_PrintSatisfyingAssignment(cm);
+ sat_ReportStatistics(cm, cm->each);
+ sat_FreeManager(cm);
+ }
+return cm->status;
+}
+/**Function********************************************************************
+
+ Synopsis [Generate a CNF of the network]
+
+ Description [Generate the set of clauses of the unroll network for a given
+ length and for a given cone of influence]
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+BmcCnfClauses_t*
+Dbg_GenerateCNF(Ntk_Network_t * network,
+BmcOption_t * options,
+st_table *CoiTable
+){
+st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
+BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
+/*
+ *nodeToMvfAigTable maps each node to its multi-function And/Inv graph
+ */
+nodeToMvfAigTable =
+(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+assert(nodeToMvfAigTable != NIL(st_table));
+/*
+ * Create a clause database
+ */
+cnfClauses = BmcCnfClausesAlloc();
+/*
+ * Generate clauses for an initialized path of length k
+ */
+BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
+ cnfClauses, nodeToMvfAigTable, CoiTable);
+return cnfClauses;
+
+}