WIP: SyGuS PDR

[zhanghongce]

No description provided.

[zhanghongce]

Please let me know if it is okay to put partial model generation under modifiers. Thanks!

[makaimann]

Hey! Sorry, I responded just now on your closed PR. Copy-pasted that response here:

As for where to put partial model generation: that's a great question. I'm not sure it belongs in modifiers. Modifiers are supposed to be anything that changes the transition system, which static-coi does. I'd recommend either creating a new file in utils, or adding it to https://github.com/upscale-project/pono/blob/master/utils/ts_analysis.h. There's also term_analysis.* but I think that this type of partial model generation takes the specifics of the transition system into account, right?

What do you think about putting it in ts_analysis.*? That's supposed to be for any functions that do "analysis" loosely defined on a transition system but don't change the transition system. It also makes perfect sense to just create new files there, especially if it's a lot of code.

[zhanghongce]

No problem. Will move to ts_analysis.

Sorry, I was thinking maybe term_analysis?

[makaimann]

Cool, yeah I think term_analysis.* or new files makes sense! Whichever you prefer.

[zhanghongce]

Thanks!

[makaimann]

Actually just looking through the diff, it's a fair amount of code. term_analysis.* is more for small utility functions in my opinion. How about you just move partial_model.* to the utils directory and otherwise leave it the same?

[zhanghongce]

Actually just looking through the diff, it's a fair amount of code. term_analysis.* is more for small utility functions in my opinion. How about you just move partial_model.* to the utils directory and otherwise leave it the same?

No problem. Thanks!

[zhanghongce]

This update relies on the UNSAT core reduction function in this pull request: stanford-centaur/smt-switch#152

[makaimann]

Hi @zhanghongce, thanks for all your work on this -- it's much appreciated. I just made another pass and I think it looks awesome! It looks really clean.

[makaimann]

@zhanghongce let me know if you'd like to make any other changes, otherwise I think it looks great and I'm ready to merge it!

Also, please let me know if there's anything you're still waiting on me for and / or anything I can do to help.

p.s. I decided not to worry about the function case for now. It's not that important, and we can always change it later if at all.

[zhanghongce]

Hi Makai, I think code-wise it is okay. I have been running larger tests and working on locating and debugging some performance issues. The new commits solves those that I found, but I think there is still room for more.I can definitely improve more in the future. Thanks!

[makaimann]

Gotcha, that sounds great! Let's get this merged then and you can continue to work on it (but of course no pressure). Either way I think it's good to get this in and any improvements can be subsequent PRs. Thanks!

I'll wait for Travis and then merge.

[zhanghongce]

Thank you, Makai! And the updated usage is pono --promote-inputvars -e sygus-pdr <btor name>

[zhanghongce]

Hi Makai, I'm looking at the results from Travis and it shows segmentation faults on two existing tests:

The following tests FAILED:
	  7 - test_witness (SEGFAULT)
	 24 - test_btor2_ts_copy_equal (SEGFAULT)

However, I don't think I touch the base class and I'm not able to reproduce this segmentation fault by make test locally. If you have any clues that would be really helpful. Thanks!

[makaimann]

Interesting! I'll pull and see if I can reproduce locally.

[makaimann]

I'm not able to reproduce this segmentation fault by make test locally.

I'm not able to reproduce it locally either. I'll keep looking into it -- it's very strange.

[makaimann]

Actually, I have an idea what this could be -- I was updating CVC4 for smt-switch and it probably got pulled into this PR. Hopefully it's fixed now. I'll restart the Travis build.

[makaimann]

All right, looks like that was it. Going to merge now! Thanks again for all your work!!

[zhanghongce]

All right, looks like that was it. Going to merge now! Thanks again for all your work!!

Thank you very much!