Boogie generates cvc5 incompatible smt2 syntax without monomorphize

[ChuyueSun]

After I modified this part of the dafny prelude to invoke the built-in sequence theory in cvc5. As a result, this dfy file will generate this bpl file. Unfortunately, boogie cannot directly monomorphize this program due to limitations created by the other parts of the prelude.

If I run boogie/Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver /proverOpt:PROVER_PATH="cvc5_path" /proverOpt:C:"--strings-exp" /proverLog:Test/mytest/seq_generated_smt_by_reference.smt2 Test/mytest/seq_generated_reference.bpl on the bpl file I mentioned above, then it will give

Test/mytest/seq_generated_reference.bpl(233,9): Warning: type parameter T is ambiguous, instantiating to int
Test/mytest/seq_generated_reference.bpl(233,35): Warning: type parameter T is ambiguous, instantiating to int
Advisory: m (correctness) SKIPPED due to I/O exception: Pipe is broken.
Test/mytest/seq_generated_reference.bpl(2592,49): Verification encountered solver exception (m (correctness))

Boogie program verifier finished with 0 verified, 0 errors, 1 solver exceptions

I should also note that the current boogie on master does not recognize my solver to be CVC5 when I use the PROVER_PATH option. I made manual changes on my local branch to fix it.

The generated Test/mytest/seq_generated_smt_by_reference.smt2 smt2 file is here.

If I run the following command on this bpl file which only contains sequences related parts, then it is able to verify only with \monomorphize.

boogie/Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver /proverOpt:PROVER_PATH="cvc5_path" /proverOpt:C:"--strings-exp" /proverLog:Test/mytest/seq_generated_mono.smt2 Test/mytest/seq_generated.bpl /monomorphize

And the generated smt2 file is here.

[shazqadeer]

I downloaded a CVC5 binary for MacOS on my machine and tried to run it on the smt2 file linked in the issue. I was not successful:

shazqadeer@Shazs-MacBook-Pro boogie % /Users/shazqadeer/Downloads/cvc5-macOS ~/Temp/livia.smt2                                                                            (error "Parse Error: /Users/shazqadeer/Temp/livia.smt2:31.38: Symbol 'RegEx' not declared as a type

  (declare-fun regex_2_U ((RegEx String)) T@U)
                           ^
")

I am wondering if I don't have the right cvc5.

shazqadeer@Shazs-MacBook-Pro boogie % /Users/shazqadeer/Downloads/cvc5-macOS --version
This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
compiled with GCC version Apple LLVM 13.0.0 (clang-1300.0.29.30)
on Aug 26 2022 17:16:04

[shazqadeer]

Regarding not being able to have Boogie recognize CVC5, try this:

shazqadeer@Shazs-MacBook-Pro boogie % boogie.sh /proverOpt:PROVER_PATH=/Users/shazqadeer/Downloads/cvc5-macOS ~/Temp/livia.bpl -monomorphize -proverOpt:SOLVER=CVC5 /proverOpt:C:"--strings-exp"

Boogie program verifier finished with 1 verified, 0 errors

[shazqadeer]

I am also not able to reproduce the behavior on the original bpl file you generated (I downloaded it and called it livia-big.bpl):

shazqadeer@Shazs-MacBook-Pro boogie % boogie.sh ~/Temp/livia-big.bpl -proverOpt:SOLVER=CVC5 /proverOpt:C:"--strings-exp" 
/Users/shazqadeer/Temp/livia-big.bpl(283,21): Error: undeclared type: t0
/Users/shazqadeer/Temp/livia-big.bpl(1137,32): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1139,29): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1141,20): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1145,20): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1149,20): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1153,20): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1153,28): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1158,20): Error: type constructor received wrong number of arguments: Seq

I am using the master version of Boogie. I have also installed the CVC5 binary as cvc5 somewhere in my path so I don't have to supply the binary path on the command line.

[ChuyueSun]

I am also not able to reproduce the behavior on the original bpl file you generated (I downloaded it and called it livia-big.bpl):

shazqadeer@Shazs-MacBook-Pro boogie % boogie.sh ~/Temp/livia-big.bpl -proverOpt:SOLVER=CVC5 /proverOpt:C:"--strings-exp" 
/Users/shazqadeer/Temp/livia-big.bpl(283,21): Error: undeclared type: t0
/Users/shazqadeer/Temp/livia-big.bpl(1137,32): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1139,29): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1141,20): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1145,20): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1149,20): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1153,20): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1153,28): Error: type constructor received wrong number of arguments: Seq
/Users/shazqadeer/Temp/livia-big.bpl(1158,20): Error: type constructor received wrong number of arguments: Seq

I am using the master version of Boogie. I have also installed the CVC5 binary as cvc5 somewhere in my path so I don't have to supply the binary path on the command line.

Sorry about the confusion. You are right that this should be the expected behavior. I have commented out all the axioms that caused the type constructor errors. The correct bpl I was referring to is here.

[shazqadeer]

The latest linked bpl file does not appear to work either. I am still getting the same type errors.

[ChuyueSun]

The latest linked bpl file does not appear to work either. I am still getting the same type errors.

This link should work now. Sorry I gave the wrong commit.

[shazqadeer]

Now I am able to reproduce the problem. I ran with increased verbosity:

shaz@shaz-mbp Temp % myboogie.sh livia-big.bpl -proverOpt:SOLVER=CVC5 /proverOpt:C:"--strings-exp" /proverOpt:"VERBOSITY:1"
livia-big.bpl(233,9): Warning: type parameter T is ambiguous, instantiating to int
livia-big.bpl(233,35): Warning: type parameter T is ambiguous, instantiating to int
[SMT-0] Starting cvc5 --strings-exp --lang=smt --no-strict-parsing --no-condense-function-values --incremental --produce-models
[SMT-OUT-0] (error "Parse Error: <stdin>:30.38: Symbol 'RegEx' not declared as a type
[SMT-OUT-0] 
[SMT-OUT-0]   (declare-fun regex_2_U ((RegEx String)) T@U)
[SMT-OUT-0]                            ^
[SMT-OUT-0] ")
Advisory: m (correctness) SKIPPED due to I/O exception: Pipe is broken.
livia-big.bpl(2592,49): Verification encountered solver exception (m (correctness))

Boogie program verifier finished with 0 verified, 0 errors, 1 solver exceptions

You can see how cvc5 is invoked by Boogie and the output produced. It looks like the Boogie file is using the RegEx type which is not understood by CVC5. I have not seen this type before but it looks like it is one of the primitive types supported in Boogie and Boogie assumes that a corresponding type is available in the SMT2 standard. Perhaps Z3 supports this type and Dafny has not been tried on CVC5?

I also generated the smt2 file and ran cvc5 directly on it after commenting out the two occurrences of RegEx. The file verified.

[ChuyueSun]

Thank you Shaz! Let me look into it.

[atomb]

I have some local changes that'll fix the RegEx issue. I haven't committed them yet because the current fix is a bit of a hack and I was planning to do a few other things to simplify the generated SMT-Lib along with it. I could commit my changes separately if it would be useful to have it available sooner.

[ChuyueSun]

That would be most helpful. Thank you!

[shazqadeer]

@ChuyueSun : I think this particular issue will be covered by the RegEx fix @atomb is planning. Do you see anything else raised by this issue that would not be covered?

I want to add that I am trying to extend monomorphization support in Boogie so that more programs generated by Dafny and other front-ends (such as Viper) would be handled. But it is going to take some time.

[ChuyueSun]

@shazqadeer Thank you Shaz for your experiments! I also tried to generate the smt2 file from the bpl with /proverLog then run cvc5 on it. But the smt2 I got does not have any (check-sat) at the end of the file. Does it mean that it is not checking the validity of the assertions? What does your generated smt2 look like?

[ChuyueSun]

@ChuyueSun : I think this particular issue will be covered by the RegEx fix @atomb is planning. Do you see anything else raised by this issue that would not be covered?

My main goal is to have dafny use the built-in seq datatype supported by cvc5. The current dafny/boogie cannot generate the smt2 with built-in seq without /monomorphize (as you can see in the example of the /proverlog generated by boogie) and the prelude is too long for the current monomorphization to work. But this is going to be a long-term effort. I have to think more about whether it is even possible to do it without monomorphization and how.

[shazqadeer]

I now have a PR up for the monomorphizing polymorphic features used by the Dafny encoding: https://github.com/boogie-org/boogie/pull/669.

[ChuyueSun]

Thank you for letting me know!

On Sat, Dec 24, 2022 at 07:38 Shaz Qadeer @.***> wrote:

I now have a PR up for the monomorphizing polymorphic features used by the Dafny encoding: #669 https://github.com/boogie-org/boogie/pull/669.

— Reply to this email directly, view it on GitHub https://github.com/boogie-org/boogie/issues/659#issuecomment-1364553488, or unsubscribe https://github.com/notifications/unsubscribe-auth/AIAF3WGU4KLQFWWKV6MBJWTWO4RJ7ANCNFSM6AAAAAASMDC6OQ . You are receiving this because you were mentioned.Message ID: @.***>

[shazqadeer]

@ChuyueSun : The monomorphization PR I mentioned in my last message has landed. The command-line flag /monomorphize continues to work but it should now work for a larger class of polymorphic programs. Please try it out and let us know if you run into problems. I will close this issue. Please create other issues if necessary.