diff options
Diffstat (limited to 'demo.c')
| -rw-r--r-- | demo.c | 115 |
1 files changed, 115 insertions, 0 deletions
@@ -0,0 +1,115 @@ +// Demo program for the static library project of ABC + +#include <stdio.h> +#include "src/sat/csat/csat_apis.h" + +// procedures to start and stop the ABC framework +extern void Abc_Start(); +extern void Abc_Stop(); + +// simple test prog +int main( int argc, char * argv[] ) +{ + CSAT_Manager_t * mng; + CSAT_Target_ResultT * pResult; + char * Names[2]; + int Values[2]; + int i; + + // start ABC + // (calling Abc_Start() for each problem is timeconsuming + // because it allocates some internal data structures used by decomposition packages + // so Abc_Start should be called once before creating many solution managers) + Abc_Start(); + + // start the solution manager + // (the manager can be reused for several targets if the targets + // use the same network and only differ in the asserted values; + // however, only one target can be loaded into the manager at any time) + mng = CSAT_InitManager(); + + // create a simple circuit + // PIs: A, B, C + // POs: F = ((AB)C) <+> (A(BC)) + // Internal nodes: + // X = AB U = XC + // Y = BC W = AY + // G = U <+> W + // F = G + + // PIs should be added first + CSAT_AddGate( mng, CSAT_BPI, "A", 0, NULL, 0 ); + CSAT_AddGate( mng, CSAT_BPI, "B", 0, NULL, 0 ); + CSAT_AddGate( mng, CSAT_BPI, "C", 0, NULL, 0 ); + // internal nodes should be added next + Names[0] = "A"; + Names[1] = "B"; + CSAT_AddGate( mng, CSAT_BAND, "X", 2, Names, 0 ); +// CSAT_AddGate( mng, CSAT_BOR, "X", 2, Names, 0 ); // use this line to make the problem SATISFIABLE + Names[0] = "X"; + Names[1] = "C"; + CSAT_AddGate( mng, CSAT_BAND, "U", 2, Names, 0 ); + Names[0] = "B"; + Names[1] = "C"; + CSAT_AddGate( mng, CSAT_BAND, "Y", 2, Names, 0 ); + Names[0] = "A"; + Names[1] = "Y"; + CSAT_AddGate( mng, CSAT_BAND, "W", 2, Names, 0 ); + Names[0] = "U"; + Names[1] = "W"; + CSAT_AddGate( mng, CSAT_BXOR, "G", 2, Names, 0 ); + // POs should be added last + Names[0] = "G"; + CSAT_AddGate( mng, CSAT_BPO, "F", 1, Names, 0 ); + + // check integrity of the manager (and finalize ABC network in the manager!) + if ( CSAT_Check_Integrity( mng ) ) + printf( "Integrity is okey.\n" ); + else + printf( "Integrity is NOT okey.\n" ); + + // dump the problem into a BENCH file + // currently BENCH file can only be written for an AIG + // so we will transform the network into AIG before dumping it + CSAT_EnableDump( mng, "simple.bench" ); + CSAT_Dump_Bench_File( mng ); + + // set the solving target (only one target at a time!) + // the target can be expressed sing PI/PO or internal nodes + Names[0] = "F"; + Values[0] = 1; + CSAT_AddTarget( mng, 1, Names, Values ); + + // initialize the sover + CSAT_SolveInit( mng ); + + // set the solving option (0 = brute-force SAT; 1 = resource-aware FRAIG) + CSAT_SetSolveOption( mng, 1 ); + + // solves the last added target + CSAT_Solve( mng ); + + // get the result of solving + pResult = CSAT_Get_Target_Result( mng, 0 ); + + // print the report + if ( pResult->status == UNDETERMINED ) + printf( "The problem is UNDETERMINED.\n" ); + else if ( pResult->status == UNSATISFIABLE ) + printf( "The problem is UNSATISFIABLE.\n" ); + else if ( pResult->status == SATISFIABLE ) + { + printf( "The problem is SATISFIABLE.\n" ); + printf( "Satisfying assignment is: " ); + for ( i = 0; i < pResult->no_sig; i++ ) + printf( "%s=%d ", pResult->names[i], pResult->values[i] ); + printf( "\n" ); + } + + // free everything to prevent memory leaks + CSAT_TargetResFree( pResult ); + CSAT_QuitManager( mng ); + Abc_Stop(); + return 0; +} + |