summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaSatoko.c126
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/base/abci/abc.c73
-rw-r--r--src/base/wlc/wlcShow.c4
4 files changed, 200 insertions, 4 deletions
diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c
new file mode 100644
index 00000000..62bc7713
--- /dev/null
+++ b/src/aig/gia/giaSatoko.c
@@ -0,0 +1,126 @@
+/**CFile****************************************************************
+
+ FileName [giaSatoko.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Interface to Satoko solver.]
+
+ Author [Alan Mishchenko, Bruno Schmitt]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaSatoko.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "sat/cnf/cnf.h"
+#include "sat/satoko/satoko.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p )
+{
+ satoko_t * pSat = satoko_create();
+ Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 1, 0 );
+ int i, status;
+ //sat_solver_setnvars( pSat, p->nVars );
+ for ( i = 0; i < pCnf->nClauses; i++ )
+ {
+ if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
+ {
+ Cnf_DataFree( pCnf );
+ satoko_destroy( pSat );
+ return NULL;
+ }
+ }
+ Cnf_DataFree( pCnf );
+ status = satoko_simplify(pSat);
+ if ( status == SATOKO_OK )
+ return pSat;
+ satoko_destroy( pSat );
+ return NULL;
+}
+void Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
+{
+ abctime clk = Abc_Clock();
+ satoko_t * pSat;
+ int status;
+
+ pSat = Gia_ManCreateSatoko( p );
+ if ( pSat )
+ {
+ satoko_configure(pSat, opts);
+ status = satoko_solve( pSat );
+ satoko_destroy( pSat );
+ }
+ else
+ status = SATOKO_UNSAT;
+
+ if ( iOutput >= 0 )
+ Abc_Print( 1, "Output %6d : ", iOutput );
+ else
+ Abc_Print( 1, "Total: " );
+
+ if ( status == SATOKO_UNDEC )
+ Abc_Print( 1, "UNDECIDED " );
+ else if ( status == SATOKO_SAT )
+ Abc_Print( 1, "SATISFIABLE " );
+ else
+ Abc_Print( 1, "UNSATISFIABLE " );
+
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit )
+{
+ if ( fSplit )
+ {
+ Gia_Man_t * pOne;
+ Gia_Obj_t * pRoot;
+ int i;
+ Gia_ManForEachCo( p, pRoot, i )
+ {
+ pOne = Gia_ManDupDfsCone( p, pRoot );
+ Gia_ManCallSatokoOne( pOne, opts, i );
+ Gia_ManStop( pOne );
+ }
+ return;
+ }
+ Gia_ManCallSatokoOne( p, opts, -1 );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 0066bfd2..0ddf9833 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -59,6 +59,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaSatLE.c \
src/aig/gia/giaSatLut.c \
src/aig/gia/giaSatMap.c \
+ src/aig/gia/giaSatoko.c \
src/aig/gia/giaScl.c \
src/aig/gia/giaScript.c \
src/aig/gia/giaShow.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 65974acb..1ecc5e68 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -310,6 +310,7 @@ static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSatoko ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Satoko ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -959,6 +960,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "xsat", Abc_CommandXSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "satoko", Abc_CommandSatoko, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "&satoko", Abc_CommandAbc9Satoko, 0 );
Cmd_CommandAdd( pAbc, "Verification", "psat", Abc_CommandPSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
@@ -23356,11 +23358,12 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
satoko_t * p;
int status;
- satoko_parse_dimacs( pFileName, &p );
+ status = satoko_parse_dimacs( pFileName, &p );
satoko_configure(p, &opts);
clk = Abc_Clock();
- status = satoko_solve( p );
+ if ( status == SATOKO_OK )
+ status = satoko_solve( p );
if ( status == SATOKO_UNDEC )
Abc_Print( 1, "UNDECIDED " );
@@ -23382,6 +23385,72 @@ usage:
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit );
+ int c, fSplit = 0;
+
+ satoko_opts_t opts;
+ satoko_default_opts(&opts);
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Csvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ opts.conf_limit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( opts.conf_limit < 0 )
+ goto usage;
+ break;
+ case 's':
+ fSplit ^= 1;
+ break;
+ case 'v':
+ opts.verbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Satoko(): There is no AIG.\n" );
+ return 1;
+ }
+ Gia_ManCallSatoko( pAbc->pGia, &opts, fSplit );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &satoko [-C num] [-svh]\n" );
+ Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
+ Abc_Print( -2, "\t-s : split multi-output miter into individual outputs [default = %s]\n", fSplit? "yes": "no" );
+ Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
Synopsis []
diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c
index 7914cd7a..1601d602 100644
--- a/src/base/wlc/wlcShow.c
+++ b/src/base/wlc/wlcShow.c
@@ -49,9 +49,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
Wlc_Obj_t * pNode;
int LevelMax, Prev, Level, i;
- if ( Wlc_NtkObjNum(p) > 1000 )
+ if ( Wlc_NtkObjNum(p) > 2000 )
{
- fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 1000 );
+ fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 2000 );
return;
}
if ( (pFile = fopen( pFileName, "w" )) == NULL )
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-17 18:16:24 +0000