inter

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

• type Adder
• type Assumable
• type GoSolvable
• type Liter
• type MaxVar
• type Model
• type S
• type Sc
• type Solvable
• type Solve
• type Sv
• type Testable

Types

type Adder

type Adder interface {

	// add a literal to the clauses.  if m is z.LitNull,
	// signals end of clause.
	//
	// For performance reasons of reading big dimacs files,
	// Add should not be used unless no other goroutine
	// is accessing the object implementing adder.  Other
	// methods may provide safety in the presence of multiple
	// goroutines.  Add in general does not.
	Add(m z.Lit)
}

Adder encapsulates something to which clauses can be added by sequences of z.LitNull-terminated literals.

type Assumable

type Assumable interface {
	Assume(m ...z.Lit)
	Why(dst []z.Lit) []z.Lit
}

Assumable encapsulates a problem

type GoSolvable

type GoSolvable interface {
	GoSolve() Solve
}

Interface GoSolvable encapsulates a handle on a Solve running in its own goroutine.

type Liter

type Liter interface {
	Lit() z.Lit
}

Liter produces fresh variables and returns the corresponding positive literal.

type MaxVar

type MaxVar interface {
	MaxVar() z.Var
}

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 Model

type Model interface {
	Value(m z.Lit) bool
}

Model encapsulates something from which a model can be exracted.

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.
	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

type Solvable interface {
	Solve() int
}

Interface Solveable encapsulates a decision procedure which may run for a long time.

Solve returns

1  If the problem is SAT
0  If the problem is undetermined
-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:

1. Once a result from the underlying Solve() is obtained, Solve should no longer be used.
2. Every successful Pause() should be followed by Unpause before trying to obtain a result.
3. 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.
	// place the resulting propagated literals since the last
	// test in dst 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.