Unknown predicates called in `smt_solvers_interface/solver_dispatcher.pl`

[pmoura]

*     Unknown predicate called but not defined: pretty_print_smt2/0
*       while compiling object solver_dispatcher
*       in file /Users/pmoura/ProB_src/src/smt_solvers_interface/solver_dispatcher.pl at or above line 33
*     
*     Unknown predicate called but not defined: pretty_print_smt2_for_id/2
*       while compiling object solver_dispatcher
*       in file /Users/pmoura/ProB_src/src/smt_solvers_interface/solver_dispatcher.pl at or above line 36

[dgelessus]

This seems to be a false positive. The predicates in question are exported from the z3interface module, which is imported in solver_dispatcher using:

:- use_module(extension('z3interface/z3interface')).

Perhaps Logtalk is confused because the predicates are implemented in C and only declared on the Prolog side using foreign:

foreign(pretty_print_smt2, c, pretty_print_smt2).
foreign(pretty_print_smt2_for_id, c, pretty_print_smt2_for_id(+atom, +integer)).

But shouldn't that cause an error in z3interface module itself, and not in the code that uses it?

[pmoura]

I get (on macOS 12.4):

$ sicstuslgt -l $PROB_SOURCE_DIR/prob_cli.pl --goal "go_cli." -a
...

| ?- current_module(z3interface).
yes
| ?- predicate_property(z3interface:pretty_print_smt2, P).
no
| ?- predicate_property(z3interface:Predicate, exported).
Predicate = reset_z3interface ? ;
Predicate = init_z3interface ? ;
Predicate = z3_interface_call(_A) ? ;
no

It seems the foreign resource is failing to load but I don't get any error loading the module. Looking into the extension directory, I noticed that it's not built. Oops! After gmake, I get:

$ ll
total 73736
-rw-rw-rw-@ 1 pmoura  staff      2019 Jul  8 22:34 Makefile
drwxrwxrwx@ 3 pmoura  staff        96 Jul  8 22:34 src
-rw-r--r--  1 pmoura  staff  35093632 Jul 12 10:09 z3-4.8.17-x64-osx-10.16.zip
drwxr-xr-x  3 pmoura  staff        96 Jul 12 10:10 z3dist
-rwxr-xr-x  1 pmoura  staff   1985216 Jul 12 10:10 z3interface.bundle
-rw-rw-rw-@ 1 pmoura  staff     10350 Jul  8 22:34 z3interface.pl
-rw-r--r--  1 pmoura  staff     44191 Jul 12 10:10 z3interface_glue.c
-rw-r--r--  1 pmoura  staff     13896 Jul 12 10:10 z3interface_glue.h
-rw-r--r--  1 pmoura  staff     38848 Jul 12 10:10 z3interface_glue.o

But I get the same results for the queries above. The README file says:

Note: before starting probcli or ProB Tcl/Tk from sources for the first time you need to build the extensions. Type "make" in the prob_prolog directory. In case this does not work, you can always try and download a ProB nightly build and copy the contents of the lib/ folder to prob_prolog/lib/. The lib/ folder should contain all relevant extensions (as .dll, .so or .bundle files depending on the platform) as well as some JAR files (e.g., the ProB parser).

I did that last week and I indeed have a ProB_src/lib/z3interface.bundle file. I assume that the prob_prolog directory mentioned in the README file is ProB_src.

[dgelessus]

It should be enough to run make in the top-level directory - that will build/download all the native extensions and place them in the lib folder as required by ProB. (The top-level directory is called ProB_src in the public source archive, but our internal repo is called prob_prolog - that's where the different name comes from.)

The foreign predicates are only defined when the foreign library is loaded. For z3interface, that is done with the init_z3interface predicate. I guess that needs to be called before compiling the module with Logtalk?

[pmoura]

I was indeed expecting that the call to the init_z3interface to be done automatically. Trying to do it manually, I get:

| ?- z3interface:init_z3interface.
*** LOADING Z3 library failed
*** Be sure to set Z3_HOME to the directory your z3 binary is located and have libz3.dylib/so/dll on your dynamic library path.
*** error(system_error,system_error(dlopen("/Users/pmoura/ProB_src/lib/z3interface.bundle") failed in load_foreign_resource/1: dlopen(/Users/pmoura/ProB_src/lib/z3interface.bundle, 0x0002): Library not loaded: libz3.dylib
  Referenced from: /Users/pmoura/ProB_src/lib/z3interface.bundle
  Reason: tried: 'libz3.dylib' (no such file), '/usr/local/lib/libz3.dylib' (no such file), '/usr/lib/libz3.dylib' (no such file), '/Users/pmoura/ProB_src/src/libz3.dylib' (no such file), '/usr/local/lib/libz3.dylib' (no such file), '/usr/lib/libz3.dylib' (no such file)))
no

Tried unsuccessfully setting both Z3_HOME and DYLD_LIBRARY_PATH. Solution: brew install z3. I no longer get the unknown predicate warnings.

P.S. Forgot to mention:

$ make
git rev-parse HEAD > src/revision
fatal: not a git repository (or any of the parent directories): .git
make: *** [src/revision] Error 128

[dgelessus]

Yes, that's the expected behavior - ProB doesn't ship a copy of Z3 itself, so Z3 has to be installed at the system level or you have to provide your own copy of libz3.

Normally, the Z3 integration is only loaded on-demand when using Z3-based features, so you can use most of ProB without needing to have Z3 installed. Plain SICStus doesn't care about undefined predicates until you call them, so this doesn't cause any problems. Is there any way to tell Logtalk that these foreign predicates exist, without having to actually load the foreign library?

P.S. Forgot to mention:

Thanks, this should be fixed in the next update of the sources.

[pmoura]

When Logtalk compiles modules as objects, it expands use_module/1-2 directives into Logtalk own use_module/2 directives (see https://logtalk.org/manuals/refman/directives/use_module_2.html). This is required to resolve implicitly-qualified references to module predicates at compile time. This is not essentially different from Prolog compilers loading modules when compiling use_module/1-2 directives. But the Logtalk compiler is more strict than Prolog compilers and checks at compile time for undefined predicates. The trouble in this particular case is that, although the module header is:

:- module(z3interface, [init_z3interface/0,
                        reset_z3interface/0, % TODO: make more lightweight once cvc 1.5 is out
                        pretty_print_smt1/0, % pretty print Z3's internal status and constraints
                        pretty_print_smt2/0, % pretty print Z3's internal status and constraints
                        pretty_print_smt2_for_id/2, % pretty print store + constraint pointed to by ID (previously created by z3_interface_call(s))
                        z3_interface_call/1]).

the pretty print predicates are only enumerated by SICStus predicate_property/2 after the foreign library is loaded. That was a surprise. Thanks for your help in sorting out this issue.