pysmt-install --cvc4 not working

[averm...@gmail.com]

Hello,

I am trying to install cvc4 to use with pySMT. I am running into the following issue:

sudo pysmt-install --cvc4
Runs for a while and then gives the message:

Traceback (most recent call last):
 File "/usr/local/bin/pysmt-install", line 11, in <module>
   sys.exit(main())
 File "/usr/local/lib/python3.5/dist-packages/pysmt/cmd/install.py", line 240, in main
   installer.install(force_redo=options.force_redo)
 File "/usr/local/lib/python3.5/dist-packages/pysmt/cmd/installers/base.py", line 144, in install
   self.move()
 File "/usr/local/lib/python3.5/dist-packages/pysmt/cmd/installers/cvc4.py", line 43, in move
   self.bindings_dir)
 File "/usr/local/lib/python3.5/dist-packages/pysmt/cmd/installers/base.py", line 243, in mv
   shutil.copy(source, dest)
 File "/usr/lib/python3.5/shutil.py", line 235, in copy
   copyfile(src, dst, follow_symlinks=follow_symlinks)
 File "/usr/lib/python3.5/shutil.py", line 114, in copyfile
   with open(src, 'rb') as fsrc:
FileNotFoundError: [Errno 2] No such file or directory: '/home/averma/.smt_solvers/python-bindings-3.5/CVC4_bin/lib/pyshared/_CVC4.so'

I tried placing the file _CVC4.so (downloaded from CVC4 github repository) in this location manually, then the script runs without complaining but I still can't import CVC4 or use it with pySMT.

Could someone please give any advice or suggestions on how to resolve this issue?

Thanks.

Regards,
Abhinav

[Marco Gario]

You need to look into what happens before the python error. The compilation process was not completed, and thus it did not generate the _CVC4.so file. Most likely you are missing some dependencies to compile the python bindings. You can send us the full log if you need help debugging.

Marco

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+unsubscribe@googlegroups.com.
To post to this group, send email to py...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/d0165798-05d7-4b29-92c0-9ece8e42cc08%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Abhinav Verma]

Hi Marco,

Thank you for the advice. I went over the messages generated during the process, but was unable to isolate the issue. I would be grateful for your help in finding the dependency that I am missing. I have attached the entire output (pysmtlog.txt) and just the stderr output (pysmtErrorlog.txt) to this email. I am also pasting the error logs in this email directly.

Thanks again for the help.

Regards,

Abhinav

-----------------------------------------------------------------------------------
Continue? [Y]es/[N]o: /bin/sed: couldn't flush stdout: Broken pipe
+ mkdir -p antlr-3.4/share/java
+ mkdir -p antlr-3.4/bin
+ mkdir -p antlr-3.4/src
+ cd antlr-3.4
+ webget http://www.antlr3.org/download/antlr-3.4-complete.jar share/java/antlr-3.4-complete.jar
+ which curl
+ which wget
+ wget -c -O share/java/antlr-3.4-complete.jar http://www.antlr3.org/download/antlr-3.4-complete.jar
--2017-07-21 18:24:47--  http://www.antlr3.org/download/antlr-3.4-complete.jar
Resolving www.antlr3.org (www.antlr3.org)... 151.101.16.133
Connecting to www.antlr3.org (www.antlr3.org)|151.101.16.133|:80... connected.
HTTP request sent, awaiting response... 416 Range Not Satisfiable

    The file is already fully retrieved; nothing to do.

+ webget http://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz src/libantlr3c-3.4.tar.gz
+ which curl
+ which wget
+ wget -c -O src/libantlr3c-3.4.tar.gz http://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz
--2017-07-21 18:24:47--  http://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz
Resolving www.antlr3.org (www.antlr3.org)... 151.101.16.133
Connecting to www.antlr3.org (www.antlr3.org)|151.101.16.133|:80... connected.
HTTP request sent, awaiting response... 200 OK
Length: 546039 (533K) [application/gzip]
Saving to: ‘src/libantlr3c-3.4.tar.gz’

     0K .......... .......... .......... .......... ..........  9% 1.08M 0s
    50K .......... .......... .......... .......... .......... 18% 2.84M 0s
   100K .......... .......... .......... .......... .......... 28% 2.93M 0s
   150K .......... .......... .......... .......... .......... 37% 5.48M 0s
   200K .......... .......... .......... .......... .......... 46% 6.50M 0s
   250K .......... .......... .......... .......... .......... 56% 2.97M 0s
   300K .......... .......... .......... .......... .......... 65% 6.03M 0s
   350K .......... .......... .......... .......... .......... 75% 38.6M 0s
   400K .......... .......... .......... .......... .......... 84% 6.19M 0s
   450K .......... .......... .......... .......... .......... 93% 6.37M 0s
   500K .......... .......... .......... ...                  100% 45.0M=0.1s

2017-07-21 18:24:47 (3.78 MB/s) - ‘src/libantlr3c-3.4.tar.gz’ saved [546039/546039]

+ tee bin/antlr3
++ pwd
+ chmod a+x bin/antlr3
+ cd src
+ gunzip -f libantlr3c-3.4.tar.gz
+ tar xfv libantlr3c-3.4.tar
+ cd libantlr3c-3.4
+ '[' x86_64 == x86_64 ']'
++ pwd
+ ./configure --enable-64bit --disable-shared --disable-antlrdebug --prefix=/home/averma/.smt_solvers/cvc4/CVC4-c15ff43597b41ea457befecb1b0e2402e28cb523/antlr-3.4/src/libantlr3c-3.4/../..
./configure: line 10723: #include: command not found
+ cp Makefile Makefile.orig
+ sed 's,^\(CFLAGS = .*\),\1 -fexceptions,' Makefile.orig
+ make
src/antlr3baserecognizer.c: In function 'mismatch':
src/antlr3baserecognizer.c:645:29: warning: variable 'tparser' set but not used [-Wunused-but-set-variable]
     pANTLR3_TREE_PARSER     tparser;
                             ^
src/antlr3baserecognizer.c: In function 'displayRecognitionError':
src/antlr3baserecognizer.c:1012:25: warning: variable 'is' set but not used [-Wunused-but-set-variable]
  pANTLR3_INT_STREAM     is;
                         ^
src/antlr3baserecognizer.c: In function 'getMissingSymbol':
src/antlr3baserecognizer.c:2169:31: warning: variable 'cts' set but not used [-Wunused-but-set-variable]
  pANTLR3_COMMON_TOKEN_STREAM  cts;
                               ^
src/antlr3basetree.c: In function 'replaceChildren':
src/antlr3basetree.c:428:17: warning: variable 'numToInsert' set but not used [-Wunused-but-set-variable]
   ANTLR3_UINT32 numToInsert;
                 ^
src/antlr3collections.c: In function 'intTrieDel':
src/antlr3collections.c:1893:29: warning: variable 'p' set but not used [-Wunused-but-set-variable]
     pANTLR3_INT_TRIE_NODE   p;
                             ^
src/antlr3commontreeadaptor.c:51:32: warning: 'getToken' declared 'static' but never defined [-Wunused-function]
 static pANTLR3_COMMON_TOKEN    getToken    (pANTLR3_BASE_TREE_ADAPTOR adaptor, pANTLR3_BASE_TREE t);
                                ^
src/antlr3commontreenodestream.c: In function 'replaceChildren':
src/antlr3commontreenodestream.c:933:31: warning: variable 'cta' set but not used [-Wunused-but-set-variable]
   pANTLR3_COMMON_TREE_ADAPTOR cta;
                               ^
src/antlr3string.c: In function 'toUTF8_UTF16':
src/antlr3string.c:367:22: warning: variable 'cResult' set but not used [-Wunused-but-set-variable]
     ConversionResult cResult;
                      ^
src/antlr3string.c: At top level:
src/antlr3string.c:335:1: warning: 'stringInitUTF8' defined but not used [-Wunused-function]
 stringInitUTF8  (pANTLR3_STRING string)
 ^
src/antlr3treeparser.c: In function 'getCurrentInputSymbol':
src/antlr3treeparser.c:192:37: warning: variable 'ctns' set but not used [-Wunused-but-set-variable]
     pANTLR3_COMMON_TREE_NODE_STREAM ctns;
                                     ^
ar: `u' modifier ignored since `D' is the default (see `U')
+ make install
+ cd ../..
+ mv lib/libantlr3c.a lib/libantlr3c-static.a
+ cd src/libantlr3c-3.4
+ make clean
+ '[' x86_64 == x86_64 ']'
++ pwd
+ ./configure --enable-64bit --with-pic --disable-shared --disable-antlrdebug --prefix=/home/averma/.smt_solvers/cvc4/CVC4-c15ff43597b41ea457befecb1b0e2402e28cb523/antlr-3.4/src/libantlr3c-3.4/../..
./configure: line 10723: #include: command not found
+ cp Makefile Makefile.orig
+ sed 's,^\(CFLAGS = .*\),\1 -fexceptions,' Makefile.orig
+ make
src/antlr3baserecognizer.c: In function 'mismatch':
src/antlr3baserecognizer.c:645:29: warning: variable 'tparser' set but not used [-Wunused-but-set-variable]
     pANTLR3_TREE_PARSER     tparser;
                             ^
src/antlr3baserecognizer.c: In function 'displayRecognitionError':
src/antlr3baserecognizer.c:1012:25: warning: variable 'is' set but not used [-Wunused-but-set-variable]
  pANTLR3_INT_STREAM     is;
                         ^
src/antlr3baserecognizer.c: In function 'getMissingSymbol':
src/antlr3baserecognizer.c:2169:31: warning: variable 'cts' set but not used [-Wunused-but-set-variable]
  pANTLR3_COMMON_TOKEN_STREAM  cts;
                               ^
src/antlr3basetree.c: In function 'replaceChildren':
src/antlr3basetree.c:428:17: warning: variable 'numToInsert' set but not used [-Wunused-but-set-variable]
   ANTLR3_UINT32 numToInsert;
                 ^
src/antlr3collections.c: In function 'intTrieDel':
src/antlr3collections.c:1893:29: warning: variable 'p' set but not used [-Wunused-but-set-variable]
     pANTLR3_INT_TRIE_NODE   p;
                             ^
src/antlr3commontreeadaptor.c:51:32: warning: 'getToken' declared 'static' but never defined [-Wunused-function]
 static pANTLR3_COMMON_TOKEN    getToken    (pANTLR3_BASE_TREE_ADAPTOR adaptor, pANTLR3_BASE_TREE t);
                                ^
src/antlr3commontreenodestream.c: In function 'replaceChildren':
src/antlr3commontreenodestream.c:933:31: warning: variable 'cta' set but not used [-Wunused-but-set-variable]
   pANTLR3_COMMON_TREE_ADAPTOR cta;
                               ^
src/antlr3string.c: In function 'toUTF8_UTF16':
src/antlr3string.c:367:22: warning: variable 'cResult' set but not used [-Wunused-but-set-variable]
     ConversionResult cResult;
                      ^
src/antlr3string.c: At top level:
src/antlr3string.c:335:1: warning: 'stringInitUTF8' defined but not used [-Wunused-function]
 stringInitUTF8  (pANTLR3_STRING string)
 ^
src/antlr3treeparser.c: In function 'getCurrentInputSymbol':
src/antlr3treeparser.c:192:37: warning: variable 'ctns' set but not used [-Wunused-but-set-variable]
     pANTLR3_COMMON_TREE_NODE_STREAM ctns;
                                     ^
ar: `u' modifier ignored since `D' is the default (see `U')
+ make install
+ cd ../..
+ mv lib/libantlr3c.la lib/libantlr3c.la.orig
+ awk '/^old_library=/ {print "old_library='\''libantlr3c-static.a'\''"} /^library_names=/ {print "library_names='\''libantlr3c.a'\''"} !/^old_library=/ && !/^library_names=/ {print}'
+ set +x
configure: WARNING: could not figure out which toolset name to use for g++
configure: WARNING:
configure: WARNING: You are electing to build unsupported language binding(s):
configure: WARNING:     python
configure: WARNING: Please be aware that these bindings may not compile, or
configure: WARNING: work, and the interface to CVC4 via these bindings may
configure: WARNING: change drastically in upcoming releases of CVC4.
configure: WARNING:
ar: `u' modifier ignored since `D' is the default (see `U')
Smt2Lexer.c: In function ‘ANTLR3_INT32 dfa15_sst(pSmt2Lexer, pANTLR3_BASE_RECOGNIZER, pANTLR3_INT_STREAM, pANTLR3_CYCLIC_DFA, ANTLR3_INT32)’:
Smt2Lexer.c:31059:24: warning: variable ‘LA15_320’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_320;
                        ^
Smt2Lexer.c:31158:24: warning: variable ‘LA15_298’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_298;
                        ^
Smt2Lexer.c:31194:24: warning: variable ‘LA15_541’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_541;
                        ^
Smt2Lexer.c:31230:24: warning: variable ‘LA15_542’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_542;
                        ^
Smt2Lexer.c:31266:24: warning: variable ‘LA15_747’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_747;
                        ^
Smt2Lexer.c:31302:24: warning: variable ‘LA15_748’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_748;
                        ^
Smt2Lexer.c:31338:24: warning: variable ‘LA15_493’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_493;
                        ^
Smt2Lexer.c:31374:24: warning: variable ‘LA15_257’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_257;
                        ^
Smt2Lexer.c:31456:24: warning: variable ‘LA15_190’ set but not used [-Wunused-but-set-variable]
          ANTLR3_UINT32 LA15_190;
                        ^
At global scope:
cc1plus: warning: unrecognized command line option ‘-Wno-tautological-compare’
ar: `u' modifier ignored since `D' is the default (see `U')
ar: `u' modifier ignored since `D' is the default (see `U')
ar: `u' modifier ignored since `D' is the default (see `U')
../../../../../src/bindings/../bindings/swig.h:29: Warning 204: CPP #warning, ""Working around a SWIG segfault in C++ template parsing."".
../../../../../src/bindings/../bindings/swig.h:29: Warning 204: CPP #warning, ""Working around a SWIG segfault in C++ template parsing."".
libtool: [31mwarning (B [m: [1mrelinking 'libcvc4parser.la' (B [m
libtool: [31mwarning (B [m: [1mrelinking 'libcvc4compat.la' (B [m
../../../../../src/bindings/../bindings/swig.h:29: Warning 204: CPP #warning, ""Working around a SWIG segfault in C++ template parsing."".
../../../../../src/bindings/../bindings/swig.h:29: Warning 204: CPP #warning, ""Working around a SWIG segfault in C++ template parsing."".
../../../../../src/bindings/../bindings/swig.h:29: Warning 204: CPP #warning, ""Working around a SWIG segfault in C++ template parsing."".
libtool: [31mwarning (B [m: [1mrelinking 'python/CVC4.la' (B [m

Traceback (most recent call last):
  File "/usr/local/bin/pysmt-install", line 11, in <module>
    sys.exit(main())
  File "/usr/local/lib/python3.5/dist-packages/pysmt/cmd/install.py", line 240, in main
    installer.install(force_redo=options.force_redo)
  File "/usr/local/lib/python3.5/dist-packages/pysmt/cmd/installers/base.py", line 144, in install
    self.move()
  File "/usr/local/lib/python3.5/dist-packages/pysmt/cmd/installers/cvc4.py", line 43, in move
    self.bindings_dir)
  File "/usr/local/lib/python3.5/dist-packages/pysmt/cmd/installers/base.py", line 243, in mv
    shutil.copy(source, dest)
  File "/usr/lib/python3.5/shutil.py", line 235, in copy
    copyfile(src, dst, follow_symlinks=follow_symlinks)
  File "/usr/lib/python3.5/shutil.py", line 114, in copyfile
    with open(src, 'rb') as fsrc:
FileNotFoundError: [Errno 2] No such file or directory: '/home/averma/.smt_solvers/python-bindings-3.5/CVC4_bin/lib/pyshared/_CVC4.so'

-----------------------------------------------------------------------------------------

[Marco Gario]

Hi,

The following line looks suspicious:

"configure: WARNING: could not figure out which toolset name to use for g++"

This is part of CVC4 ./configure and seems to be related to your C++ compiler. Or maybe it is related to lib boost (see [2]). 

Are you on Ubuntu? If so, which version? You can find in [1] the list of packages that we install on Ubuntu to get all solvers to compile. If this does not help, I would suggest that you try to manually build CVC4 outside pysmt.This will make it easier to understand what dependencies you are missing.

Hope this helps,

Marco

[1] https://github.com/pysmt/pysmt/blob/master/.travis.yml#L21 the

[2] http://comments.gmane.org/gmane.comp.gnome.love/3396