From 4394bc865944ba0c24fcc0cf5b39af1ec64b83bc Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 20 Mar 2019 22:07:55 +0200
Subject: Add special handling of script-level assertions.

---
 src/base/cmd/cmdApi.c | 100 +++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 98 insertions(+), 2 deletions(-)

(limited to 'src/base/cmd')

diff --git a/src/base/cmd/cmdApi.c b/src/base/cmd/cmdApi.c
index 29e13837..64e11ae8 100644
--- a/src/base/cmd/cmdApi.c
+++ b/src/base/cmd/cmdApi.c
@@ -85,6 +85,100 @@ void Cmd_CommandAdd( Abc_Frame_t * pAbc, const char * sGroup, const char * sName
     assert( !fStatus );  // the command should not be in the table
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cmd_CommandHandleSpecial( Abc_Frame_t * pAbc, const char * sCommand )
+{
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int piCountNew = pNtk ? Abc_NtkCiNum(pNtk)         : 0, piCount = 0;
+    int poCountNew = pNtk ? Abc_NtkCoNum(pNtk)         : 0, poCount = 0;
+    int ndCountNew = pNtk ? Abc_NtkNodeNum(pNtk)       : 0, ndCount = 0;
+    double AreaNew = pNtk ? Abc_NtkGetMappedArea(pNtk) : 0, Area    = 0;
+    int DepthNew   = pNtk ? Abc_NtkLevel(pNtk)         : 0, Depth   = 0;
+    if ( strstr(sCommand, "#PS") ) 
+    {
+        printf( "pi=%d ",   piCountNew );
+        printf( "po=%d ",   poCountNew );
+        printf( "fn=%d ",   ndCountNew );
+        printf( "ma=%.1f ", AreaNew    );
+        printf( "de=%d ",   DepthNew   );
+        printf( "\n" );
+        return 1;
+    }
+    if ( strstr(sCommand, "#CEC") ) 
+    {
+        //int proofStatus = Abc_NtkVerifyUsingCec(pNtk);
+        int proofStatus = 1;
+        // -1 (undecided), 0 (different), 1 (equivalent)
+        printf( "proofStatus=%d\n", proofStatus );
+        return 1;
+    }
+    if ( strstr(sCommand, "#ASSERT") ) 
+    {
+        int Status    = 0;
+        char * pNumb  = strrchr( sCommand, '=' );
+        if ( strstr(sCommand, "_PI_") ) 
+        {
+            piCount = pNumb ? atoi(pNumb+1) : 0;
+            if ( strstr( sCommand, "==" ) )
+                Status = piCountNew == piCount;
+            else if ( strstr( sCommand, "<=" ) )
+                Status = piCountNew <= piCount;
+            else return 0;
+        }
+        else if ( strstr(sCommand, "_PO_") ) 
+        {
+            poCount = pNumb ? atoi(pNumb+1) : 0;
+            if ( strstr( sCommand, "==" ) )
+                Status = poCountNew == poCount;
+            else if ( strstr( sCommand, "<=" ) )
+                Status = poCountNew <= poCount;
+            else return 0;
+        }
+        else if ( strstr(sCommand, "_NODE_") ) 
+        {
+            ndCount = pNumb ? atoi(pNumb+1) : 0;
+            if ( strstr( sCommand, "==" ) )
+                Status = ndCountNew == ndCount;
+            else if ( strstr( sCommand, "<=" ) )
+                Status = ndCountNew <= ndCount;
+            else return 0;
+        }
+        else if ( strstr(sCommand, "_AREA_") ) 
+        {
+            double Eplison = 1.0;
+            Area = pNumb ? atof(pNumb+1) : 0;
+            if ( strstr( sCommand, "==" ) )
+                Status = AreaNew >= Area - Eplison && AreaNew <= Area + Eplison;
+            else if ( strstr( sCommand, "<=" ) )
+                Status = AreaNew <= Area + Eplison;
+            else return 0;
+        }
+        else if ( strstr(sCommand, "_DEPTH_") ) 
+        {
+            Depth = pNumb ? atoi(pNumb+1) : 0;
+            if ( strstr( sCommand, "==" ) )
+                Status = DepthNew == Depth;
+            else if ( strstr( sCommand, "<=" ) )
+                Status = DepthNew <= Depth;
+            else return 0;
+        }
+        else return 0;
+        printf( "%s\n", Status ? "succeeded" : "failed" );
+        return 1;
+    }
+    return 0;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -107,12 +201,14 @@ int Cmd_CommandExecute( Abc_Frame_t * pAbc, const char * sCommand )
     sCommandNext = sCommand;
     do 
     {
-           sCommandNext = CmdSplitLine( pAbc, sCommandNext, &argc, &argv );
+        if ( sCommandNext[0] == '#' && Cmd_CommandHandleSpecial( pAbc, sCommandNext ) )
+            break;
+        sCommandNext = CmdSplitLine( pAbc, sCommandNext, &argc, &argv );
         loop = 0;
         fStatus = CmdApplyAlias( pAbc, &argc, &argv, &loop );
         if ( fStatus == 0 ) 
             fStatus = CmdCommandDispatch( pAbc, &argc, &argv );
-           CmdFreeArgv( argc, argv );
+        CmdFreeArgv( argc, argv );
     } 
     while ( fStatus == 0 && *sCommandNext != '\0' );
     return fStatus;
-- 
cgit v1.2.3