search

purdue-cap / DryadSynth

A SyGuS Solver
MIT License
22 stars 7 forks source link

-E option #2

Open polgreen opened 3 years ago

polgreen commented 3 years ago

Hi!

This isn't an issue, just a request for more information. What does the exec.sh option -E do? It says "EUSolver entry point command, set to use EUSolver as CEGIS algorithm, set to empty string to disable. (default: )"

Does this mean it runs plain EUSolver instead of running any DryadSynth algorithm? Or does it run EUSolver as a subprocedure of DryadSynth? What does the string do?

Thanks

YanjunW commented 3 years ago

Hi @polgreen,

Sorry for the late reply.

Yes, -E can be used to run EUSolver as the enumerative synthesis component of DryadSynth, instead of our own height-based enumerative synthesizer. The string specified through -E should be the command that invokes EUSolver, though we do not include EUSolver in this repo.

Please let me know if you have any other questions, thanks!

polgreen commented 2 years ago

Ok, thanks. So what happens if I run it with an arbitrary string? It appears to run without throwing any errors. Does it just run EUSolver with it's own height based enumeration synthesizer?

YanjunW commented 2 years ago

If the string specified via -E is not a valid path to run EUSolver, DryadSynth will exit without throwing any errors. If you also enable the verbose output by -v, you may find "INFO: EUSolver failed to execute" in stdout.