Documentation ¶
Overview ¶
Package inter contains common gini interfaces and functions to map between them.
The inter package is designed with facets of solving interfaces. Facets for solve processes, models, assumptions, scoping, and asynchronous solves are provided.
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type Activatable ¶
type Activatable interface { // Activate should be called in place of Add(0) to activate a // clause. Activate returns the activation literal, which, if assigned // activates the last added clause. // // If the last clause is empty, then Activate panics. The caller // should only activate non-empty clauses. Note that in incremental // settings, one may have to verify whether or not a clause is // empty. // // like `Add()`, Activate should only be called at decision level 0. Activate() z.Lit // ActivateWith is like Activate but it allows the caller to specify // the activation literal `act`. The activation literal should // be `pure`, meaning that `act.Not()` does not appear anywhere in // any clause added. Note that deactivation of literals passed to // ActivateWith causes them to be recycled. ActivateWith(act z.Lit) // ActivationLit returns a literal to be used with ActivateWith. // As all other Activation related methods, ActivationLit is // not supported under test scopes. ActivationLit() z.Lit // Deactivate deactivates an activation literal as returned by // Activate. // // like `Add()`, Deactivate should only be called at decision level 0. Deactivate(m z.Lit) }
Activatable provides support for recyclable activation literals
Caveats: activation clauses must not be empty under unit propagtion at level 0. The caller should ensure this by construction.
type Adder ¶
type Adder interface { // add a literal to the clauses. if m is z.LitNull, // signals end of clause. // // If the implemation of Add is a solver under a test scope // then Add undoes the test. // Add(m z.Lit) }
Adder encapsulates something to which clauses can be added by sequences of z.LitNull-terminated literals.
type GoSolvable ¶
type GoSolvable interface {
GoSolve() Solve
}
Interface GoSolvable encapsulates a handle on a Solve running in its own goroutine.
type MaxVar ¶
Interface MaxVar is something which records the maximum variable from a stream of inputs (such as Adds/Assumes) and can return the maximum of all such variables.
type S ¶
type S interface { MaxVar // Although an S can generate literals via Liter, it // doesn't have to. One can just send arbitrary variables // via Adder, Assume, etc. Liter is useful for applications // which need a way to know how to generate new variables/literals. Liter Adder Solvable GoSolvable Model Testable // Can create a copy. A copy copies everything in the S interface // and nothing more (such as simplifiers). SCopy() S }
Interface S encapsulates something capable of a complete incremental SAT interface enabling composing solvable, assumable, model, testable, and GoSolveable.
type Sc ¶
type Sc interface { S // Stop stops the Sc and should be called once. Once stop // is called all behavior of Sc is undefined. Stop() }
Interface Sc is an interface for a concurrent solver which must be stopped in order to free goroutines.
type Solvable ¶
Interface Solveable encapsulates a decision procedure which may run for a long time.
Solve/Try returns
1 If the problem is SAT 0 If the problem is undetermined (Try only) -1 If the problem is UNSAT
These error codes are used throughout gini.
type Solve ¶
type Solve interface { // Stop stops the Solve() call and returns the result, defaulting to // 0 if the answer is unknown. Stop() int // Try lets Solve() run for at most d time and then returns the result. Try(d time.Duration) int // Test checks whether or not a result is ready, and if so returns it // together with true. If not, it returns (0, false). Test() (int, bool) // Pause tries to pause the Solve(), returning the result of solve if any // and whether the Pause succeeded (ok). If the pause did not succeed, it // is because the underlying Solve() returned a result. Pause() (res int, ok bool) // Unpause unpauses the Solve(). Should only be called if Pause succeeded. Unpause() // Wait blocks until there is a result. Wait() int }
Interface Solve represents a connection to a call to (S).Solve().
Solve may be constructed by a call to (S).GoSolve().
Since solves can take almost arbitrary time, we provide an asynchronous interface via Solve. This interface is safe only in the sense that the solver will not go out of wack with multiple Solve calls in the face of asynchronous cancelation.
This interface is NOT safe for usage in multiple goroutines and several caveats must be respected:
- Once a result from the underlying Solve() is obtained, Solve should no longer be used.
- Every successful Pause() should be followed by Unpause before trying to obtain a result.
- Every unsucessful Pause should not be followed by a corresponding Pause, as a result is obtained.
type Sv ¶
type Sv interface { S // Inner returns the positive literal of a new inner variable. Inner() z.Lit // FreeInner frees the previously inner-allocated variable // associated with m. If m's variables was not previously // allocated with Inner, then FreeInner and all subsequent // usage of Sv is undefined. FreeInner(m z.Lit) }
Interface Sv encapsulates an S which has the need or capacity to use inner variables which are hidden from the user.
type Testable ¶
type Testable interface { Assumable // Test the current assumptions under unit propagation. // append the resulting propagated literals since the last // test in dst, if dst is not nil, and return // // result: -1 for UNSAT, 1 for SAT, 0 for UNKNOWN // out: the propagated literals since last Test, // stored in dst if possible, or nil if out is nil. // // Once Test is called on a set of assumptions, all // future calls to Solve do not consume and forget // assumptions prior to test. Test(dst []z.Lit) (result int, out []z.Lit) // Untest removes the assumptions from the last test. // Untest returns -1 if the result is UNSAT, and // 0 (indicating unknown) otherwise. If the result is // -1, then Test should not be called. Untest() int // Reasons returns the reasons for implied, storing // the result in rs if possible. Reasons(rs []z.Lit, implied z.Lit) []z.Lit }
Interface Testable provides an interface for scoped assumptions.
Testable provides scoped light weight Solving and tracking of implications.
A Solvable and Assumable which also implements Testable has the following semantics w.r.t. Assumptions. All calls to Assume which are subsequently Tested before calling Solve() remain until a corresponding call to Untest.
Put another way, Solve() consumes and forgets any untested assumptions for a given Solve process. To forget tested assumptions, the user must call Untest(). Tests and Untests may be nested.