pivc fails to compile .pi source code

[maranp]

Hi,
I am trying to setup pivc on my system as part of educating myself with "The Calculus of computation".

There are two issues

1. under src/ folder,
   make
   fails with the error
   Error: I/O error: ../../bin/test_parser: No such file or directory
   If make is invoked after manually creating bin folder under piVC and the make is invoked from src/, error is no more seen and make is successful. Executables pi_gui, servers are created in bin.
   Then I copied yices binary (obtained by following the steps under Aptitude section of https://github.com/SRI-CSL/yices2 to obtain pre-built binaries) in the bin/ folder.

2. When I tried to compile samples/feature_demonstrations/predicates.pi by the user interface provided by bin/pi_gui, I get the following exception.
   Exception

---

Verify.Dp_server_exception("Smt_solver.SolverError("yices: invalid option: -e")")

Earlier, I executed both_servers in a separate terminal and set server to 127.0.0.1 in settings menu in pi_gui window so that it connects to the server instantiated by both_servers.

Can you please help me with this?

[jgalenson]

Hi,

Thanks for pointing out the error in 1. I just added a commit that fixes this by ensuring that the makefiles create the bin/ directory if it doesn't exist. Tell me if you see any more problems with this.

For your second problem, it looks like you're using Yices 2. PiVC only supports Yices 1 (with experimental support for Z3 and I believe non-working support for Yices 2). See the top-level README.md for instructions on how to download Yices 1 or use Z3. Does that help?

[maranp]

Hi,
Thanks for the quick response and fixing 1.

Reg. 2., unfortunately http://yices.csl.sri.com is not reachable. So, I could not download yices 1.
However, by configuring to use z3, I could manage to get pivc working. Thanks for the help.