src/aig/cnf/cnfCore.c File Reference
#include "cnf.h"
Include dependency graph for cnfCore.c:
Go to the source code of this file.
Functions | |
| Cnf_Dat_t * | Cnf_Derive (Aig_Man_t *pAig, int nOutputs) |
| Cnf_Man_t * | Cnf_ManRead () |
| void | Cnf_ClearMemory () |
Variables | |
| static Cnf_Man_t * | s_pManCnf = NULL |
Function Documentation
| void Cnf_ClearMemory | ( | ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
Description []
SideEffects []
SeeAlso []
Definition at line 44 of file cnfCore.c.
00045 { 00046 Cnf_Man_t * p; 00047 Cnf_Dat_t * pCnf; 00048 Vec_Ptr_t * vMapped; 00049 Aig_MmFixed_t * pMemCuts; 00050 int clk; 00051 // allocate the CNF manager 00052 if ( s_pManCnf == NULL ) 00053 s_pManCnf = Cnf_ManStart(); 00054 // connect the managers 00055 p = s_pManCnf; 00056 p->pManAig = pAig; 00057 00058 // generate cuts for all nodes, assign cost, and find best cuts 00059 clk = clock(); 00060 pMemCuts = Dar_ManComputeCuts( pAig, 10 ); 00061 p->timeCuts = clock() - clk; 00062 00063 // find the mapping 00064 clk = clock(); 00065 Cnf_DeriveMapping( p ); 00066 p->timeMap = clock() - clk; 00067 // Aig_ManScanMapping( p, 1 ); 00068 00069 // convert it into CNF 00070 clk = clock(); 00071 Cnf_ManTransferCuts( p ); 00072 vMapped = Cnf_ManScanMapping( p, 1, 1 ); 00073 pCnf = Cnf_ManWriteCnf( p, vMapped, nOutputs ); 00074 Vec_PtrFree( vMapped ); 00075 Aig_MmFixedStop( pMemCuts, 0 ); 00076 p->timeSave = clock() - clk; 00077 00078 // reset reference counters 00079 Aig_ManResetRefs( pAig ); 00080 //PRT( "Cuts ", p->timeCuts ); 00081 //PRT( "Map ", p->timeMap ); 00082 //PRT( "Saving ", p->timeSave ); 00083 return pCnf; 00084 }
| Cnf_Man_t* Cnf_ManRead | ( | ) |
Variable Documentation
CFile****************************************************************
FileName [cnfCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG-to-CNF conversion.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [
- Id
- cnfCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp
] DECLARATIONS ///
