iter

type BasicStrategy struct {
	SplitProvider SplitProvider
	MaxModels     int
}

type Collector[R any] interface {
	// AddModel adds a model to the iteration collector.  Returns true if the
	// model was added successfully.
	AddModel(modelFromSolver []bool, solver *sat.Solver, relevantAllIndices []int32, handler Handler) bool

	// Commit confirms all models found since the last commit.  These cannot be
	// rolled back anymore.  Also calls the Commit method of the handler.
	// Returns true if the iteration should continue after the commit.
	Commit(handler Handler) bool

	// Rollback discards all models since the last commit.  Also calls the
	// Rollback method of the handler.  Returns true if the iteration should
	// continue after the commit.
	Rollback(handler Handler) bool

	// RollbackAndReturnModels discards all models since the last commit and
	// returns them.  Also calls the Rollback method of the handler.
	RollbackAndReturnModels(solver *sat.Solver, handler Handler) []*model.Model

	// Result returns the committed state of the collector .
	Result() R
}

type Config struct {
	Handler  Handler
	Strategy Strategy
}

type FixedVarProvider struct {
	// contains filtered or unexported fields
}

type Handler interface {
	handler.Handler

	// SatHandler returns the embedded SAT handler.
	SatHandler() sat.Handler

	// FoundModels is called every time new models are found.  The found models
	// are in an uncommitted state until they are confirmed by calling Commit.
	// It is also possible to roll back the uncommitted models by calling
	// Rollback.  Returns true if the iteration should continue.
	FoundModels(numberOfModels int) bool

	// Commit is called every time the models are committed.  Returns true if
	// the iteration should continue.
	Commit() bool

	// Rollback is called everytime uncommitted models are rolled back.  Returns
	// true if the iteration should continue.
	Rollback() bool
}

type LeastCommonVarProvider struct {
	// contains filtered or unexported fields
}

type LimitHandler struct {
	handler.Computation
	// contains filtered or unexported fields
}

type ModelIterator[R any] struct {
	// contains filtered or unexported fields
}

type MostCommonVarProvider struct {
	// contains filtered or unexported fields
}

type NoSplitStrategy struct{}

type SplitProvider interface {
	Vars(solver *sat.Solver, variables *f.VarSet) *f.VarSet
}

type Strategy interface {
	// MaxModelsForIter returns the maximum number of models to be iterated
	// on the given recursion depth.
	//
	// If this number of models is exceeded, the algorithm will compute new
	// split assignments and proceed to the next recursion step.
	//
	// This number refers to actual iterations on the solver, not to the
	// expanded number of models in the presence of don't care variables.
	MaxModelsForIter(recursionDepth int) int

	// MaxModelsForSplitAssignments returns the maximum number of models to be
	// iterated for split variables on the given recursion depth.
	//
	// This method is used to determine how many split assignments should at
	// most be computed and used for the next recursion step. If this limit is
	// exceeded, the algorithm will reduce the number of split variables using
	// ReduceSplitVars and then try again.
	MaxModelsForSplitAssignments(recursionDepth int) int

	// SplitVarsForRecursionDepth selects the split variables for the given
	// recursion depth from the given variables.
	//
	// This method is called before the algorithm makes another recursive call
	// to determine the initial split variables for this call.
	SplitVarsForRecursionDepth(variables *f.VarSet, solver *sat.Solver, recursionDepth int) *f.VarSet

	// ReduceSplitVars reduces the split variables for the given recursion
	// depth in case of MaxModelsForSplitAssignments was exceeded.
	ReduceSplitVars(variables *f.VarSet, recursionDepth int) *f.VarSet
}

type TimeoutHandler struct {
	handler.Timeout
	// contains filtered or unexported fields
}