On a related note, I remember you wanted to have constraints print to another file that the user could then run. I didn't think that would be possible bc it would print it as a string but you'd need Z3 objects to run the file, but it seems it may be possible with the eval() and exec() methods—I used them in this code; you might want to play around with them if that's still an idea you're interested in
I have added a flag which generates a script, but right now it is of limited value since it just prints all the constraints in a list. The thought was to then call this list of constraints instead of generating constraints, allowing the user to make minor tweaks to test things. I haven't really needed to use this workflow but figured that it might be useful for troubleshooting semantic clauses (say during their design, or while comparing them to others). I'd be curious to know more about eval() and exec(). Is there some documentation that you could link?
This issue picks up a thread from #31:
I have added a flag which generates a script, but right now it is of limited value since it just prints all the constraints in a list. The thought was to then call this list of constraints instead of generating constraints, allowing the user to make minor tweaks to test things. I haven't really needed to use this workflow but figured that it might be useful for troubleshooting semantic clauses (say during their design, or while comparing them to others). I'd be curious to know more about
eval()
andexec()
. Is there some documentation that you could link?