The result of merging with recent PyABC changes.

7 files changed, 151 insertions, 36 deletions

diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c
index f97a2c6a..683d336e 100644
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@@ -454,7 +454,7 @@ FILE * CmdFileOpen( Abc_Frame_t * pAbc, char *sFileName, char *sMode, char **pFi
         else
         {
             // print the path/name of the resource file 'abc.rc' that is being loaded
-            if ( strlen(sRealName) >= 6 && strcmp( sRealName + strlen(sRealName) - 6, "abc.rc" ) == 0 )            
+            if ( !silent && strlen(sRealName) >= 6 && strcmp( sRealName + strlen(sRealName) - 6, "abc.rc" ) == 0 )            
                 printf( "Loading resource file \"%s\".\n", sRealName );
         }
     }
diff --git a/src/python/abcpy_test.py b/src/python/abcpy_test.py
index 912cae9f..28c3505b 100644
--- a/src/python/abcpy_test.py
+++ b/src/python/abcpy_test.py
@@ -34,7 +34,7 @@ import optparse
 def pytest3_cmd(args):
     usage = "usage: %prog [options]"
     
-    parser = optparse.OptionParser(usage)
+    parser = optparse.OptionParser(usage, prog="pytest3")
     
     parser.add_option("-c", "--cmd", dest="cmd", help="command to ask help for")
     parser.add_option("-v", "--version", action="store_true", dest="version", help="display Python Version")
diff --git a/src/python/module.make b/src/python/module.make
index 3f48bbaf..09e2de3f 100644
--- a/src/python/module.make
+++ b/src/python/module.make
@@ -57,7 +57,7 @@ pyabc.tgz : $(PROG) $(ABC_PYTHON_SRC:_wrap.c=.py) $(ABC_PYTHON_FILES_PREFIX)/abc
     $(ABC_PYTHON) $(ABC_PYTHON_FILES_PREFIX)/package.py \
         --abc=$(PROG) \
         --abc_sh=$(ABC_PYTHON_FILES_PREFIX)/abc.sh \
-        --pyabc=$(ABC_PYTHON_SRC:_wrap.c=.py) \
+        --pyabc=$(ABC_PYTHON_FILES_PREFIX) \
         --out=$@ \
         $(ABC_PYTHON_OPTIONS)
 
@@ -66,8 +66,6 @@ PYABC_INSTALL_TARGET := $(PYABC_INSTALL_TARGET)
 
 PYABC_INSTALL_DIR ?= /hd/common/pyabc/builds/pyabc_builds/
 
-.PHONY: zzz
-
 pyabc_install_target: pyabc_extension_bdist
     mkdir -p "$(PYABC_INSTALL_DIR)/$(PYABC_INSTALL_TARGET)"
     tar \
diff --git a/src/python/package.py b/src/python/package.py
index 9c79a944..1764ab6f 100644
--- a/src/python/package.py
+++ b/src/python/package.py
@@ -70,7 +70,10 @@ def package(abc_exe, abc_sh, pyabc, ofname, scripts_dir, use_sys):
                     add_file( tf, fullname, os.path.join("pyabc/scripts", fn), 0666, mtime)
     
     add_dir(tf, "pyabc/lib", mtime)
-    add_file( tf, pyabc, "pyabc/lib/pyabc.py", 0666, mtime)
+    
+    for entry in os.listdir(pyabc):
+        if entry.endswith('.py'):
+            add_file( tf, os.path.join(pyabc, entry), os.path.join("pyabc/lib", entry), 0666, mtime)
     
     if not use_sys:
         # ZIP standard library    
diff --git a/src/python/pyabc.i b/src/python/pyabc.i
index 44a880a7..1da81016 100644
--- a/src/python/pyabc.i
+++ b/src/python/pyabc.i
@@ -262,8 +262,6 @@ void pyabc_internal_set_command_callback( PyObject* callback )
     pyabc_internal_python_command_callback = callback;
 }
 
-PyThreadState *_save;
-
 static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, char ** argv)
 {
     int i;
@@ -271,13 +269,15 @@ static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, cha
     PyObject* args;
     PyObject* arglist;
     PyObject* res;
-
+    
+    PyGILState_STATE gstate;
+    
     long lres;
     
     if ( !pyabc_internal_python_command_callback )
             return 0;
             
-    Py_BLOCK_THREADS
+    gstate = PyGILState_Ensure();
             
     args = PyList_New(argc);
     
@@ -292,14 +292,14 @@ static int pyabc_internal_abc_command_callback(Abc_Frame_t * pAbc, int argc, cha
 
     if ( !res )
     {
-        Py_UNBLOCK_THREADS
+        PyGILState_Release(gstate);
         return -1;
     }
     
     lres = PyInt_AsLong(res);
     Py_DECREF(res);
 
-    Py_UNBLOCK_THREADS
+    PyGILState_Release(gstate);
     
     return lres;
 }
@@ -309,11 +309,11 @@ int run_command(char* cmd)
     Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
     int rc;
     
-    Py_UNBLOCK_THREADS
+    Py_BEGIN_ALLOW_THREADS
     
     rc = Cmd_CommandExecute(pAbc, cmd);
     
-    Py_BLOCK_THREADS
+    Py_END_ALLOW_THREADS
     
     return rc;
 }
@@ -401,13 +401,15 @@ int Util_SignalSystem(const char* cmd)
 {
     PyObject* arglist;
     PyObject* res;
+    
+    PyGILState_STATE gstate;
 
     long lres;
     
     if ( !pyabc_internal_system_callback )
             return -1;
             
-    Py_BLOCK_THREADS
+    gstate = PyGILState_Ensure();
             
     arglist = Py_BuildValue("(O)", PyString_FromString(cmd));
     Py_INCREF(arglist);
@@ -417,14 +419,14 @@ int Util_SignalSystem(const char* cmd)
 
     if ( !res )
     {
-        Py_UNBLOCK_THREADS
+        PyGILState_Release(gstate);
         return -1;
     }
     
     lres = PyInt_AsLong(res);
     Py_DECREF(res);
 
-    Py_UNBLOCK_THREADS
+    PyGILState_Release(gstate);
     
     return lres;
 }
@@ -437,12 +439,14 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
     PyObject* arglist;
     PyObject* res;
     
+    PyGILState_STATE gstate;
+    
     *out_name = NULL;
 
     if ( !pyabc_internal_tmpfile_callback )
             return 0;
             
-    Py_BLOCK_THREADS
+    gstate = PyGILState_Ensure();
             
     arglist = Py_BuildValue("(ss)", prefix, suffix);
     Py_INCREF(arglist);
@@ -452,7 +456,7 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
 
     if ( !res )
     {
-        Py_UNBLOCK_THREADS
+        PyGILState_Release(gstate);
         return -1;
     }
     
@@ -463,7 +467,7 @@ int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name)
     
     Py_DECREF(res);
 
-    Py_UNBLOCK_THREADS
+    PyGILState_Release(gstate);
     
     return open(*out_name, O_WRONLY);
 }
@@ -472,11 +476,13 @@ void Util_SignalTmpFileRemove(const char* fname, int fLeave)
 {
     PyObject* arglist;
     PyObject* res;
+    
+    PyGILState_STATE gstate;
 
     if ( !pyabc_internal_tmpfile_remove_callback )
             return;
             
-    Py_BLOCK_THREADS
+    gstate = PyGILState_Ensure();
             
     arglist = Py_BuildValue("(si)", fname, fLeave);
     Py_INCREF(arglist);
@@ -485,7 +491,7 @@ void Util_SignalTmpFileRemove(const char* fname, int fLeave)
     Py_DECREF(arglist);
     Py_XDECREF(res);
 
-    Py_UNBLOCK_THREADS
+    PyGILState_Release(gstate);
 }
 
 void pyabc_internal_set_util_callbacks( PyObject* system_callback, PyObject* tmpfile_callback, PyObject* tmpfile_remove_callback )
@@ -607,18 +613,18 @@ class _Cex(object):
         return _cex_get_frame(self.pCex)
        
 def cex_get_vector():
-	
-	res = []
-	
-	for i in xrange(_cex_get_vec_len()):
-		cex = _cex_get_vec(i)
-	
-		if cex is None:
-			res.append(None)
-		else:
-			res.append(_Cex(cex)) 		
-	
-	return res
+    
+    res = []
+    
+    for i in xrange(_cex_get_vec_len()):
+        cex = _cex_get_vec(i)
+
+        if cex is None:
+            res.append(None)
+        else:
+            res.append(_Cex(cex))
+    
+    return res
        
 def cex_get():
 
@@ -1045,7 +1051,7 @@ def cmd_python(cmd_args):
     
     usage = "usage: %prog [options] <Python files>"
     
-    parser = optparse.OptionParser(usage)
+    parser = optparse.OptionParser(usage, prog="python")
     
     parser.add_option("-c", "--cmd", dest="cmd", help="Execute Python command directly")
     parser.add_option("-v", "--version", action="store_true", dest="version", help="Display Python Version")
diff --git a/src/python/reachx_cmd.py b/src/python/reachx_cmd.py
new file mode 100644
index 00000000..8461cb1d
--- /dev/null
+++ b/src/python/reachx_cmd.py
@@ -0,0 +1,108 @@
+# You can use 'from pyabc import *' and then not need the pyabc. prefix everywhere
+
+import sys
+import optparse
+import subprocess
+import tempfile
+import threading
+import os
+import os.path
+from contextlib import contextmanager, nested
+
+import pyabc
+
+
+def popen_and_wait_with_timeout(timeout,cmd, *args, **kwargs):
+    """ Wait for a subprocess.Popen object to terminate, or until timeout (in seconds) expires. """
+
+    p = None
+    t = None
+
+    try:
+        p = subprocess.Popen(cmd, *args, **kwargs)
+
+        if timeout <= 0:
+            timeout = None
+        
+        t = threading.Thread(target=lambda: p.communicate())
+        t.start()
+        
+        t.join(timeout)
+        
+    finally:
+        
+        if p is not None and p.poll() is None:
+            p.kill()
+
+        if t is not None and t.is_alive():
+            t.join()
+        
+        if p is not None:
+            return p.returncode
+            
+        return -1
+
+@contextmanager
+def temp_file_name(suffix=""):
+    file = tempfile.NamedTemporaryFile(delete=False, suffix=suffix)
+    name = file.name
+    file.close()
+
+    try:
+        yield name
+    finally:
+        os.unlink(name)
+
+def cygpath(path):
+    if sys.platform == "win32":
+        if os.path.isabs(path):
+            drive, tail = os.path.splitdrive(path)
+            drive = drive.lower()
+            tail = tail.split(os.path.sep)
+            return '/cygdrive/%s'%drive[0] + '/'.join(tail) 
+        else:
+            path = path.split(os.path.sep)
+            return "/".join(path)
+    return path
+
+def run_reachx_cmd(effort, timeout):
+    with nested(temp_file_name(suffix=".aig"), temp_file_name()) as (tmpaig_name, tmplog_name):
+        pyabc.run_command("write %s"%tmpaig_name)
+        
+        cmdline = [ 
+            'read %s'%cygpath(tmpaig_name),
+            'qua_ffix -effort %d -L %s'%(effort, cygpath(tmplog_name)),
+            'quit'
+            ]
+
+        cmd = ["jabc", "-c", " ; ".join(cmdline)]
+        
+        rc = popen_and_wait_with_timeout(timeout, cmd, shell=False, stdout=sys.stdout, stderr=sys.stderr)
+
+        if rc != 0:
+            # jabc failed or stopped. Write a status file to update the status to unknown
+            with open(tmplog_name, "w") as f:
+                f.write('snl_UNK -1 unknown\n')
+                f.write('NULL\n')
+                f.write('NULL\n')
+            
+        pyabc.run_command("read_status %s"%tmplog_name)
+        
+        return rc
+
+def reachx_cmd(argv):
+    usage = "usage: %prog [options]"
+    
+    parser = optparse.OptionParser(usage, prog="reachx")
+    
+    parser.add_option("-e", "--effort", dest="effort", type=int, default=0, help="effort level. [default=0, means unlimited]")
+    parser.add_option("-t", "--timeout", dest="timeout", type=int, default=0, help="timeout in seconds [default=0, unlimited]")
+
+    options, args = parser.parse_args(argv)
+
+    rc = run_reachx_cmd(options.effort, options.timeout)
+    print "%s command: jabc returned: %d"%(argv[0], rc)
+    
+    return 0
+
+pyabc.add_abc_command(reachx_cmd, "Verification", "reachx", 0)
diff --git a/src/python/setup.py b/src/python/setup.py
index 3ef006af..68a4adae 100644
--- a/src/python/setup.py
+++ b/src/python/setup.py
@@ -63,5 +63,5 @@ setup(
     name='pyabc',
     version='1.0',
     ext_modules=[ext],
-    py_modules=['pyabc','getch','pyabc_split','redirect']
+    py_modules=['pyabc','getch','pyabc_split','redirect', 'reachx_cmd']
 )