Version abc50910

1 files changed, 0 insertions, 115 deletions

diff --git a/demo.c b/demo.c
deleted file mode 100644
index 2f9d1bff..00000000
--- a/demo.c
+++ /dev/null
@@ -1,115 +0,0 @@
-// 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;
-}
-