search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
449 stars 149 forks source link

flag for ignoring z3 symbols #108

Closed mhhf closed 3 years ago

mhhf commented 6 years ago

when supplying a custom z3 prelude file, axioms have to be stated about "known" symbols, so they have to be defined in the prelude file as well. However, currently there is no way to prevent them here to be exported a second time, which leads to a crash. I currently modify the file myself and recompile k in order to prevent a crash due tue a z3 prelude file. It would be great to have a flag which i can pass the symbols i customely defined in the prelude.

ehildenb commented 6 years ago

Hmmm, I suppose the "correct" way to do this would be to make more structured queries to Z3, then scan through and make sure there aren't duplicate symbol declarations or something.

I guess as a heuristic we could search the query string we pass to Z3 and see if a symbol is already declared before re-declaring it. Have you tried this with both the --z3-executable flag and not?

mhhf commented 6 years ago

Tried it without the --z3-executable flag, but z3 fails to prove almost anything without it. I like your approach of scanning the document, since it would remove the users responsibility to specify those flags explicitly. Another way of doing it is inserting the prelude file after all things have been defined, this would remove the users need to define those tags in de prelude file in the first place.

ehildenb commented 6 years ago

Sorry I don't understand your second comment about inserting the prelude after things have been defined. Do you mean just appending instead of prepending the prelude file to the built query? I'm not sure that would work.

mhhf commented 6 years ago

why not? I'm suggesting inserting it in the middle after the type signatures have been defined.

ehildenb commented 3 years ago

Closing this due to age, and because many improvements to how you can declare SMT symbols have been made since.

Note that you can use the smtlib attribute, the smt-hook attribute (to say that you're going to declare the symbol yourself and axiomatize it in an smt-prelude, which can be supplied by --smt-prelude). Note that the Haskell backend is also much smarter about sending things to Z3, so if you were having these problems on the Java backend, then try it out with the Haskell backend and you may be pleasantly surprised.