Documentation
¶
Overview ¶
Package ax supplies an "assumption eXchange".
An ax.T allows running solve requests for sets of assumptions all of which share a set of constraints in different goroutines.
The main object is an ax.T, which allows submitting and retrieving solve requests. Solve requests are requests to solve with a given set of assumptions, possibly with some options specified. Each request is related to the same fixed set of constraints, which are provided when the ax.T is constructed.
An ax.T is constructed with a single incremental solver, and a capacity C. The solver should have some constraints added. New solvers are created by copying an existing solver in the ax.T if a solve request is made and there is only 1 solver available and there are fewer than C solvers.
Solve responses are supplied via the ax.T interface. The user may request models or explanations, but must know if she wants this information when the request is submitted.
Index ¶
Examples ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
Types ¶
type ReqFlag ¶
type ReqFlag uint32
Type ReqFlag describes options for submitting requests to a parallel incremental solver.
type Request ¶
type Request struct {
Id int // An identifier for keeping track of requests.
Flag ReqFlag // Flags for the request.
Limit time.Duration // time limit (0 for no time limit)
Ms []z.Lit // Assumptions for solve.
}
Type Request is a request to solve under a given set of assumptions.
func NewRequest ¶
NewRequest creates a new request with the package default request generator.
type RequestGen ¶
type RequestGen struct {
// contains filtered or unexported fields
}
Type RequestGen encapsulates generating requests with the same flag.
func NewRequestGen ¶
func NewRequestGen() *RequestGen
NewRequestGen creates a new request generator.
func (*RequestGen) Flag ¶
func (g *RequestGen) Flag() ReqFlag
Flag returns the ReqFlag for subsequent generated requests.
func (*RequestGen) Limit ¶
func (g *RequestGen) Limit(d time.Duration)
Limit causes requests generated by g.New() to have time limit d.
func (*RequestGen) New ¶
func (g *RequestGen) New(ms ...z.Lit) *Request
New creates a new solve request over assumptions ms.
func (*RequestGen) SetFlag ¶
func (g *RequestGen) SetFlag(f ReqFlag)
SetFlag sets the flags for subsequent generated requests.
type Response ¶
type Response struct {
Req *Request // The request which was sent.
Who int // which pool processing unit processed the request
Res int // the result
Dur time.Duration // how long it took (wall clock time)
Pending int // how many solves were pending when this solve finished.
Ms []z.Lit // data in response
}
Type Response describes the result of an ax Request.
func (*Response) HasPending ¶
Pending returns whether the response is the last one of all requests sent so far to the ax. It is ok for r to be nil.
type T ¶
type T interface {
// Ex blocks until an exchange occurs
// If the request is accepted, ok is true, and false otherwise.
// If a response is ready, it is returned in resp, otherwise
// resp is nil.
//
// As a special case, if r is nil, then Ex blocks
// until a response is ready but does not try to submit the request.
Ex(r *Request) (resp *Response)
// TryEx tries to perform an exchange but does not block.
// It has the same semantics for Request and Response as
// Ex, but it can return a nil response and not process
// the supplied request. In this case, ok is false. Otherwise,
// ok is true.
TryEx(r *Request) (resp *Response, ok bool)
// Stop stops the ax.
Stop()
}
Interface T describes an assumptions exchanger (ax).
Objects implementing T process incremental solving requests and give solving responses. The fundamental operation supported is an exchange (Ex), in which exactly one of the following two events occur.
- A request is submitted to the system and an inter.S is guaranteed to process it unless T is Stop'd.
- A response to some previous request is returned.
Once the user is done with the object, it should be Stopped with Stop(). The number of pending requests is returned in each Response.
Objects implementing T must be safe for usage in mutlitple goroutines.
func NewT ¶
NewT creates a new ax.T from a prototype solver inter.S. NewT uses proto as the first solving unit and each time a request is received, if:
- there are less than cap copies; and
- all existing copies are busy.
then T will make another copy of proto.
If cap < 1, then NewT panics.
Example ¶
// create a random duration, random result solver.
// with 1024 max var.
d := 15 * time.Millisecond
randS := gen.RandSr(d, 0, rand.NewSource(44))
randS.Add(z.Var(1024).Pos())
// start the ax with randS as the prototype
ax := NewT(randS, 4)
defer ax.Stop()
// code for generating 128 random queries queries
N := 128
cubes := gen.NewRandCuber(32, z.Var(1024))
Limit(0)
var nGen int = 0
var genReq = func() *Request {
if nGen < N {
nGen++
return NewRequest(cubes.RandCube(nil)...)
}
return nil
}
// start the request/response loop.
var req *Request = genReq()
ttl := 0
ttlSat := 0
for ttl < N {
resp := ax.Ex(req)
if resp == nil { // request submitted.
req = genReq()
continue
}
// request not submitted, but we have a response.
ttl++
if resp.Res == 1 {
ttlSat++
}
}
fmt.Printf("solved %d\n", ttlSat)
Output: solved 67
Source Files