search

fvutils / pyvsc

Python packages providing a library for Verification Stimulus and Coverage
https://fvutils.github.io/pyvsc
Apache License 2.0
113 stars 26 forks source link

Cannot retrieve model if input formula is not SAT #98

Closed aneels3 closed 3 years ago

aneels3 commented 3 years ago

Hi @mballance I am getting this error in a random fashion. image The same error that I was discussing with you in #59 .

I am not getting the exact cause of this. Can you give me some pointers like why this error generally pops up?

In the meantime, I will try to create a test case for this.

Thanks, Anil

mballance commented 3 years ago

Hi @aneels3, The Boolector SAT() method evaluates the constraint system and determines a value for each variable. This method must be called after changing the constraints (via addAssume/addAssert) and before getting the value of a variable. Since this can be a fairly time-consuming method, we only want to call it when necessary.

Looks like there's a path through the diagnostics code that allows us to begin querying values from fields without ensuring the constraint system is SAT. I'll have a closer look at this and let you know about any improvements I make.

aneels3 commented 3 years ago

@mballance Thanks for the update!

aneels3 commented 3 years ago

Hi @mballance Any further update on this?

mballance commented 3 years ago

Hi @aneels3, for some reason I thought we had resolved this. Are you still seeing these issues? If so, having a stack trace showing the issue would help me focus on the right area of code.

aneels3 commented 3 years ago

Hi @mballance I haven't encountered this error recently. I was hoping to keep this on track to understand more about the issue. I am closing this for now and will re-open it if required.

Thanks, Anil