search

wkschwartz / pigosat

Go (golang) bindings for Picosat, the satisfiability solver
Other
15 stars 4 forks source link

Flatten and simplify the picosat C lib (make go-gettable) #4

Closed wkschwartz closed 9 years ago

wkschwartz commented 9 years ago

@justinfx,

Thank you for your pull request #2, which this replaces (and sorry it took me so long to get into this!). Your approach works great. I augmented it by removing version.c and config.h because their contents fit easily into pigosat.go. I also updated to PicoSAT 960 (was at 957 before).

If I don't hear from you soon I'll merge this but if you have a minute to look at 67a27e7, I'd be interested in your thoughts. (If you're wondering how I chose which CFLAGS to use, I came up with them by carefully reading PicoSAT's configure script.) Also take a look at 01ec477 and let me know if I'm forgetting anything.

justinfx commented 9 years ago

That's a cool idea, to make things more compact. Since you were asking about the CGO flags, maybe you want to see what I was doing in my fork so far?

https://github.com/justinfx/pigosat/blob/master/pigosat.go#L12

I haven't done any merge requests for this yet, but I was making use of the clausal cores and traces, which needed extra compile flags. I worked them in as build tags.

wkschwartz commented 9 years ago

Sounds like you think everything in this branch is good to go then. I'm going to merge it now.

I'd like to add a number of the features you've got in your branch eventually, including trace and stats support, but I don't want to add anything without tests, so I'd like to give each feature its proper due in its own pull request so I can figure out how to test the feature.

justinfx commented 9 years ago

Thanks. Yea I don't have test cases yet for those features, as I have just been exposing them as needed to research and test approaches on a certain project.

On Tue, 10 Feb 2015 3:12 AM William Schwartz notifications@github.com wrote:

Merged #4 https://github.com/wkschwartz/pigosat/pull/4.

— Reply to this email directly or view it on GitHub https://github.com/wkschwartz/pigosat/pull/4#event-232474007.

wkschwartz commented 9 years ago

What have been the most useful features that you've exposed so far? Does the project you're working on give you any hints about how to test the new features? I'm happy to write them -- I just don't have any experience with most of the features you've got there.

justinfx commented 9 years ago

Well the core trace stuff allows me to interrogate the exact logic that led to a conflict. I'm using pigosat as part of an internal package version dependency system (environment management). So if there is a conflict in the solution, I can report what happened. I haven't been back to the project in a little bit since its on the shelf, but if I did get back to it, I could also try to work on tests. Basically for a given conflicting solver it will give you back a format that shows you which clauses conflict.

On Tue, 10 Feb 2015 11:35 AM William Schwartz notifications@github.com wrote:

What have been the most useful features that you've exposed so far? Does the project you're working on give you any hints about how to test the new features? I'm happy to write them -- I just don't have any experience with most of the features you've got there.

— Reply to this email directly or view it on GitHub https://github.com/wkschwartz/pigosat/pull/4#issuecomment-73605621.