inter

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)
}

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)
}

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

type GoSolvable interface {
	GoSolve() Solve
}

type Liter interface {
	Lit() z.Lit
}

type MaxVar interface {
	MaxVar() z.Var
}

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

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
}

type Sc interface {
	S

	// Stop stops the Sc and should be called once.  Once stop
	// is called all behavior of Sc is undefined.
	Stop()
}

type Solvable interface {
	Solve() int
	Try(dur time.Duration) int
}

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
}

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)
}

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
}