Z3 works while Yices fails simple example

[matteocarde]

Z3 works while Yices fails simple example

[mikand]

@matteocarde I tried locally (same version of yices as yours) the following script, and it works. Can you check if it runs on your configuration (outside the testing environment you are using)?

from pysmt.shortcuts import *
from pysmt.logics import QF_UFLIRA

x, y = Symbol("x1"), Symbol("y1")
f = Implies(x, y)

solvers_set = ["yices"]
with Portfolio(solvers_set,
                logic=QF_UFLIRA,
                incremental=True,
                generate_models=True) as s:
    s.add_assertion(f)
    s.push()
    s.add_assertion(x)

    res = s.solve()
    v_y = s.get_value(y)
    assert v_y == TRUE()

    s.pop()
    s.add_assertion(Not(y))
    res = s.solve()
    v_x = s.get_value(x)
    assert v_x == FALSE()

[matteocarde]

Hi,
I get the same error

Traceback (most recent call last):
  File "/Users/carde/Desktop/test.py", line 20, in <module>
    assert v_y == TRUE()
AssertionError

To make it work I had to change the code to:

from pysmt.shortcuts import *
from pysmt.logics import QF_UFLIRA

if __name__ == '__main__':

    x, y = Symbol("x1"), Symbol("y1")
    f = Implies(x, y)

    solvers_set = ["yices"]
    with Portfolio(solvers_set,
                    logic=QF_UFLIRA,
                    incremental=True,
                    generate_models=True) as s:
        s.add_assertion(f)
        s.push()
        s.add_assertion(x)

        res = s.solve()
        v_y = s.get_value(y)
        assert v_y == TRUE()

        s.pop()
        s.add_assertion(Not(y))
        res = s.solve()
        v_x = s.get_value(x)
        assert v_x == FALSE()

Adding the if __name__ == '__main__': otherways I got the error An attempt has been made to start a new process before the current process has finished its bootstrapping phase

I'm using anaconda and this is my environment:

conda 4.14.0
Python 3.10.9

antlr-python-runtime      4.12.0             pyhd8ed1ab_0    conda-forge
antlr4-python3-runtime    4.12.0             pyh1a96a4e_0    conda-forge
bzip2                     1.0.8                h0d85af4_4    conda-forge
ca-certificates           2022.12.7            h033912b_0    conda-forge
libffi                    3.4.2                h0d85af4_5    conda-forge
libsqlite                 3.40.0               ha978bb4_0    conda-forge
libzlib                   1.2.13               hfd90126_4    conda-forge
ncurses                   6.3                  h96cf925_1    conda-forge
openssl                   3.0.8                hfd90126_0    conda-forge
pip                       23.0.1             pyhd8ed1ab_0    conda-forge
pysmt                     0.9.5              pyhd8ed1ab_0    conda-forge
python                    3.10.9          he7542f4_0_cpython    conda-forge
readline                  8.1.2                h3899abd_0    conda-forge
setuptools                67.5.1             pyhd8ed1ab_0    conda-forge
tk                        8.6.12               h5dbffcc_0    conda-forge
tzdata                    2022g                h191b570_0    conda-forge
wheel                     0.38.4             pyhd8ed1ab_0    conda-forge
xz                        5.2.6                h775f41a_0    conda-forge

[mikand]

mmmh, very strange...
Any chance you can try this on python 3.7?
Also, are you using windows, linux or macos?

[matteocarde]

Hi,
I can confirm it's Python 3.10 that causes problems. I've reinstalled everything with Python 3.7 and things seems to work very well

Maybe you can add this dependency in the README ?

[mikand]

Thanks for debugging this. I'll have a look at what causes this ASAP (if possible I would like to make this compatible with Python 3.10)

[Hook25]

I have recreated the environment (pysmt + installed solvers, same versions) but I can not trigger this bug at all. I have tested this on python 3.10.10, 3.11.1, 3.10.9 and 3.7.16 both with and without a virtualenv. I am running ArchLinux x86

[mikand]

Thanks a lot for the check @Hook25 !!
@matteocarde are you using windows, linux or macos?

[matteocarde]

Hi, I was on a MacBook with M1 Max Il giorno mar 28 mar 2023 alle 11:18 Massimiliano ***@***.***> ha scritto:

I have recreated the environment (pysmt + installed solvers, same versions) but I can not trigger this bug at all. I have tested this on python 3.10.10, 3.11.1, 3.10.9 and 3.7.16 both with and without a virtualenv. I am running ArchLinux x86 — Reply to this email directly, view it on GitHub <#753 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAPN2IYG6NPTIE2VRXD7RRTW6K3IZANCNFSM6AAAAAAWFBAC6Q> . You are receiving this because you were mentioned.Message ID: ***@***.***>

-- Matteo Cardellini

[mikand]

Unfortunately, we do not have any Apple silicon machines to test this on our end, and the support for M1 in Github actions is scheduled for Q4 2023: github/roadmap#528.

If someone can independently confirm the bug it would be helpful. @cristian-mattarei ?