Added Assume() + companion methods

[justinfx]

I've added the Assume() method, along with the checks for failed assumptions, and the max subsets of satisfiable assumptions.

[wkschwartz]

Thanks! If it's a little while before I merge this, it's not because I've forgotten about it. It's just that my next few weeks are pretty busy. I'll definitely get to it though.

[justinfx]

That's alright. I have 1 or 2 more merge requests to put together anyways,
based on the features from my fork.

On Mon, 23 Feb 2015 6:13 PM William Schwartz notifications@github.com
wrote:

Thanks! If it's a little while before I merge this, it's not because I've
forgotten about it. It's just that my next few weeks are pretty busy. I'll
definitely get to it though.

—
Reply to this email directly or view it on GitHub
#12 (comment).

[wkschwartz]

FYI, I'm working on a pull request for your branch (i.e., merge from my assumptions branch into yours, which would then merge into my master). So far it's mostly readability stuff (the biggest change is moving the assume-related methods into a separate file). I want to see if there's a better way to loop over C arrays too. Will send pull request soon.

[justinfx]

Awesome. Glad to see this is still being considered.

On Wed, Apr 15, 2015 at 8:46 AM William Schwartz notifications@github.com
wrote:

FYI, I'm working on a pull request for your branch (i.e., merge from my
assumptions branch into yours, which would then merge into my master). So
far it's mostly readability stuff (the biggest change is moving the
assume-related methods into a separate file). I want to see if there's a
better way to loop over C arrays too. Will send pull request soon.

—
Reply to this email directly or view it on GitHub
#12 (comment).

[justinfx]

Curious if this will ever get merged. I was thinking of open sourcing some old package resolving code, which would be making use of this.

[wkschwartz]

Yes, I'm sorry for the delay, but it will be merged. Thanks for the
reminder. I'm swamped at work until mid September but will turn back to
this then. Same goes for your other pull request.

Thanks for your patience and sorry I've neglected this package all year.

[wkschwartz]

Still haven't forgotten about this! I've cleared my schedule for tomorrow to work on this and your other PR.

[wkschwartz]

(Moving discussion of your comment to here to keep the whole PR together.)

The reason why we should lock before checking the last result is to prevent the race condition in which one thread calls FailedAssumption while another thread kicks off a new Solve. The reason calling Res from inside FailedAssumption doesn't deadlock is that they both acquire a read lock and neither acquires a write lock. There is not limit on the number of threads holding a read lock.

The only advantage I can see to avoiding calling a public (i.e., read-lock-acquiring) method such as Res here is speed, or avoiding a situation where in the future we want to switch Res to acquire a write lock (not sure why we would want to do the latter). In that case, I think it's fine to create an internal method res and have all the public methods, including Res and FailedAssumption call res. That change would be cheap, at least, because it's just a couple lines of code.

[wkschwartz]

Incidentally, in a number of places in #13 such as this, we call picosat_res directly. Maybe we not worry about Res/res/picosat_res at all for now and harmonize the convention after merging these PRs?

[justinfx]

Sorry if my lack of a reply was holding this up at all. Yea I agree that we shouldn't hold up this ticket with out-of-scope improvements. I do feel that exported methods that lock should not call other exported methods that lock, and that there would be unexported methods which do not lock. Because if that method that is being called decides to change the way it locks it could then cause bugs/deadlocking in the callers which anticipated the implementation. But all good. I would much prefer we get this merged over anything else.

[wkschwartz]

I think we're on the same page. Would you mind pushing a commit that replaces the internal calls to Res with direct calls to C? Once we get this commit merged, we'll fix it with #20.

[justinfx]

Sure. I can do that.

[wkschwartz]

Proposal to make the signature like the following so litArrayToSlice is a function instead of a method. Instead of looping over the litPtr array using a Go slice, what if we did this:

func litArrayToSlice(litPtr *C.int) []Literal {
  if litPtr == nil {
    return nil
  }

  lits := []Literal{}
  for *litPtr != 0 {
    lits = append(lits, Literal(*litPtr))
  }
  return lits
}

Is there any risk that we'll never get to *litPtr != 0?

[justinfx]

In this example, how do you advance the litPtr? The previous approach wraps the *C.int in a slice to be able to range over it. Would we have to do some unsafe pointer arith?

[wkschwartz]

Omitting the pointer arithmetic was a typo on my part, but I did forget about using unsafe (got my C/Go cross-combobulated). I guess it would look like this?

  for *litPtr != 0 {
    lits = append(lits, Literal(*litPtr))
    litPtr += unsafe.Sizeof(C.int)
  }

What's the "recommended" way of dealing with this in Cgo? No doubt there's a convention or semiofficial FAQ or something. Have a link or seen this done in the wild?

[justinfx]

That would be the cgo way, since cgo is unsafe by nature. I suppose the only danger is if the literal was not 0-terminated and we loop forever. Whereas the other approach is limiting it to a max size when wrapping it in a slice header

[wkschwartz]

We could pass in a maxLen int argument and bail or panic (I think I prefer panic) if we don't hit *litPtr == 0 before len(lits) >= maxLen. Or we could keep calling picosat_variables from within the function.

[justinfx]

I prefer panic as well, as it would be a library error for the private method to iterate beyond an expected max

[wkschwartz]

If litPtr == nil why should we return a non-nil result here?

[justinfx]

We could return nil but we would need to update the docstrings on the exported functions that return the result of litArrayToSlice. They should say a nil slice could be returned. I assume in actual practice (the usage in the exported functions) that we just want to return valid empty Literals, for consistency? But I know they can be treated the same with len() and append() operations, so maybe it doesn't matter.

[wkschwartz]

From the way I read the documentation for picosat_failed_assumptions:

/* Returns a zero terminated list of failed assumption in the last call to
 * 'picosat_sat'.  The pointer is valid until the next call to
 * 'picosat_sat' or 'picosat_failed_assumptions'.  It only makes sense if the
 * last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'.
 */

I think it would take an internal picosat error for picosat_failed_assumptions to return a NULL pointer. Perhaps it makes more sense to panic when litPtr == nil?

[wkschwartz]

And, like I said in the other thread, I have no problem changing the API since the last stable release of Pigosat was version <1. After merging this and #15, the API will be pretty different anyway.

[wkschwartz]

Does this mean we should implement blocksol differently, or not automatically call blocksol from Solve? (Disclaimer: I have not used the assumption interface before.)

[justinfx]

TBH I didn't look to much into the blocksol stuff too closely. I see now that its a Pigosat addition that implicitly blocks on Solves. But if I understand this correctly, this shouldn't impact what we have done in our go Solve() method, right? This will call into C, which will use the C solve and then block the solution. That would mean the only custom logic that has been layered in Pigosat is the blocking being done from our own Solve

[wkschwartz]

Correct. Pigosat.Solve calls blocksol before returning, and blocksol just adds a clause to the formula that negates the solution just found. This way subsequent calls to solve can return any solution except the ones already returned. Based off Pycosat.

I wonder if this messes up the use of Assume(), et al. Do changes to the formula make Picosat forget about the last set of assumptions? If this is the case, perhaps we should make blocksol a public method that users have to call themselves if they intend to find more than one solution. (I have no problem with changing the API if it makes sense. I had put Pigosat at version <1 for a reason.)

[justinfx]

According to the docs, the blocksol would invalidate any current assumptions, since it would be adding more literals:

• More precisely, assumptions actually remain valid even after the next
• call to 'picosat_sat' has returned. Valid means they remain 'assumed'
• internally until a call to 'picosat_add', 'picosat_assume', or a second
• 'picosat_sat', following the first 'picosat_sat'. The reason for keeping
• them valid is to allow 'picosat_failed_assumption' to return correct
• values.

I think I see what you mean, and I was too focused on the location of this comment in the source. Because we are doing a block solution at the end of OUR solve, we are breaking the ability to check for failed assumptions afterwards. Yea we should probably remove the super secret blocking operations and make it user-explicit.

[wkschwartz]

Whoops, both of us forgot about Pigosat.BlockSolution already being a public method. This is good. We just need to update the documentation about using Solve like an iterator and remove the call to blocksol. I think it'll break some tests though, so I'm not going to try to do this tonight.

[justinfx]

Sounds good

[wkschwartz]

I can't get any tests to fail to demonstrate this problem. I think the reason why we don't need to worry about the call to blocksol is because all the assumption-related Picosat functions look at failed literals after Picosat derives UNSAT. PiGosat only calls blocksol upon SAT. Anyway, it's probably best not to do anything that seems "super secret" as you put it, so I've made #22, which I'll do after merging this PR.

[wkschwartz]

Just a heads up: It's going to be the end of the month before I can turn back to this. Swamped at work.

[justinfx]

I've pushed up my work to github today, since it didn't end up becoming a project, internally at my company.

https://github.com/justinfx/pakr

Its still pointing at my fork of pigosat because it is dependent on this branch getting merged.

[wkschwartz]

The last ten commits reduce the length of the assumption tests by a third. This is entirely for readability. The only reason for the separate commits was because that's how I tested the changes.

[wkschwartz]

Definitely need to resolve crash in TestAssumptionsNoCrash (see 483bdf6) before merging this. I think we'll have to keep track of when the assumptions are valid on the Go side to avoid this crash.

[wkschwartz]

I think all that remains at this point is fixing #22, and doing a final go test -v -coverprofile=cover.out && go tool cover -html=cover.out to make sure all the tests are running (I noticed two tests weren't running this way; I do wish go test would just print a test count every time like Python does).

[justinfx]

Why would it be considered "not zero-terminated" if there are more elements in lits than maxLen? Does maxLen imply that you know the length up front, and if so, does being 0-terminated even matter at that point?

[wkschwartz]

"Array not zero-terminated" isn't the best error message there. My idea is this, keeping in mind that litArrayToSlice is an internal utility function. We only use litArrayToSlice on zero-terminated arrays coming from PicoSAT. In general, these arrays are zero-terminated. In case for whatever reason they are not, we can pass in maxLen, which we known in general is equal to p.Variables(), so that we don't loop forever here. In other words, maxLen is purely a safety control and we don't know how long the array actually is until we hit the zero terminator.

Thoughts on a better error message?

[wkschwartz]

I think this is ready. Will require a version bump once merged into master because of #22.

[wkschwartz]

@justinfx Thanks again for your work on this PR. I merged it without giving you a chance to review it one last time, but as always, feel free to leave a note here or open a new issue or PR if you notice anything amiss. I'm hoping to finish the other PRs and issues to get PiGoSAT to version 1.0.