Documentation
¶
Overview ¶
Package solver contains solving, constraints and context logic.
Index ¶
- Constants
- Variables
- func FindNextRule(st *State) (*State, Term)
- func FindVar(v Variable, t Term) (found bool)
- func FindVars(t Term) map[Variable]bool
- func Repl()
- func SameStructure(t1, t2 Term) bool
- func SortConstraintAscending(constraints []Constraint)
- func SortConstraintsDescending(constraints []Constraint)
- type Atom
- type CompoundTerm
- type Constraint
- type Number
- type Session
- type SolutionHandler
- type State
- type String
- type Term
- type Underscore
- type VarGTENum
- type VarGTNum
- type VarINT
- type VarIsAtom
- type VarIsCompoundTerm
- type VarIsNum
- type VarIsString
- type VarIsVar
- type VarLTENum
- type VarLTNum
- type Variable
Constants ¶
const ( RED = "\x1b[31m" GREEN = "\x1b[32m" BLUE = "\x1b[34m" YELLOW = "\x1b[33m" CYAN = "\x1b[36m" RESET = "\x1b[0m" )
const MAX_DEPTH = 300 // maximum depth control for state/uids
const MIN_DEPTH = 30 // minimum depth control for state/uids
const VERSION = "0.6.5"
Variables ¶
var ( ErrPred = fmt.Errorf("predicate cannot apply") ErrDiff = fmt.Errorf("diff predicate fails") )
Known atomic predicates.
var CompPredicateMap = map[string]int{
"rule": -1,
"query": -1,
"dot": -1,
"and": 2,
"or": 2,
"number": 1,
"integer": 1,
"load": -1,
"print": -1,
"eq": 2,
"diff": 2,
}
Known compound predicates with their imperative arity. A compund predicate MUST be a CompoundTerm. Arity set to -1 means it can vary. Assumes only canonical form. Constant values are eliminated (numbers, strings ...) as well as underscore.
var ErrDepthControl = fmt.Errorf("maximum allowed nesting depth reached - truncating search tree")
var ErrInvalidConstraintEmptyRange = fmt.Errorf("invalid constraint, specified range is empty")
var ErrInvalidConstraintNaN = fmt.Errorf("invalid constraint (NaN)")
var ErrInvalidConstraintSimplify = fmt.Errorf("incompatible constraints detected when simplifying")
var ErrNaN = fmt.Errorf("not a number (NaN)")
var ErrNotImplemented = fmt.Errorf(RED + "not implemented" + RESET) // should be removed later on //TODO
var ErrPositiveOccur = fmt.Errorf("positive occur check")
var ErrUnificationImpossible = fmt.Errorf("unification impossible")
var ZeroNumber, OneNumber = parser.ZeroNumber, parser.OneNumber
useful numbers
Functions ¶
func FindNextRule ¶
Find the next rule applicable in the current context. Returns an alpha-transformed rule. Only consider rules whose index is higher or equal to st.NextRule New State is created if a choice was made between multiple applicable rules. Return nil if no rule available. Will enforce the constraints of MAX_DEPTH when doing alpha-substitution.
func SameStructure ¶
Does the structure of both terms seem to match and should be considered, regardless of potential constraints . It may not be unifiable later. Do not check too deep into the structure, since predicates or expressions can be hidden inside that will disappear later. Float and Integer could unify if same float64 value. The goal is to eliminate early non match.
func SortConstraintAscending ¶
func SortConstraintAscending(constraints []Constraint)
compare constraints based on their variable. Panic if nil constraint.
func SortConstraintsDescending ¶
func SortConstraintsDescending(constraints []Constraint)
compare constraints based on their variable. Panic if nil constraint.
Types ¶
type CompoundTerm ¶
type CompoundTerm = parser.CompoundTerm
type Constraint ¶
type Constraint interface {
// deep copy
Clone() Constraint
// Check will check validity of constraint, clean it or simplify it.
// It will return the constraint itself, possibly modified, or nil if constraint should be ignored (
// CAUTION : return can be nil, despite a nil error !
// An error means the constraint is impossible to satisfy (e.g. positive occur check, empty number interval, ...)
Check() (Constraint, error)
// simplify c, taking into account the calling constraint (unchanged).
// if error, other results are not significant and should not be used.
// If changed, replace c by all of cc (possibly empty, to just suppress c).
// If changed is false, cc has no meaning.
// Input constraints MUST BE checked
// Output constraints are checkedutput.
Simplify(c Constraint) (cc []Constraint, changed bool, err error)
String() string
GetV() Variable // Get (a copy of) the main variable forthe constraint
}
a Constraint is immutable
func CheckAddConstraint ¶
func CheckAddConstraint(cc []Constraint, cl ...Constraint) ([]Constraint, error)
Check (individual), and Add a constraint to the list, return error for backtracking. Simplification not performed. Avoid later workload by notadding nil constraints.
func FilterSolutions ¶
func FilterSolutions(cc []Constraint) []Constraint
Filter constraints to display, keeping only 0 Nsp.
func SimplifyConstraints ¶
func SimplifyConstraints(constraints []Constraint) ([]Constraint, error)
Attempt to simplify constraint list. Return error if an incompatibility was detected. Constraints are supposed to have been checked before calling this function. Its is a garantee that returned constraints are checked.
func Unify ¶
func Unify(cList []Constraint, head Term, goal Term) ([]Constraint, error)
Unify recursively unifies rule head and goal. We avoid state directly, by just appending to a list of constraints. Simplification will occur later. No predicates are handled here. No backtracking is done.
type Session ¶
type Session struct {
// contains filtered or unexported fields
}
Set of rules that can be applied in a state
func NewSession ¶
func NewSession() *Session
func (*Session) AdjustDepthControl ¶
func (s *Session) AdjustDepthControl()
heuristic to adjust depth control called when adding new rules. multiple calls will increase the limit ...
func (*Session) ForceDepthControl ¶
Force the limit beyond which search trees will be truncated. Use at your own risks !
type SolutionHandler ¶
Handles a solution. A solution is assumed when goals are empty. Return value indicates what to do next. The state MAY be modified, typically by changing to parent state for backtracking. If returned state is nil, Solve exits.
type State ¶
type State struct {
Constraints []Constraint
Goals []Term // Goals we are trying to erase. They are ordered in the order they should be executed.
Parent *State // for backtracking
Uid int // Unique id for alpha-conversion of rules
NextRule int // index of the next rule to consider. It may not be applicable.
Session *Session // pointer to current session
}
State maintains the current state of the puzzle current state, and is used for backtracking. A new state is created if and only if we have to make a choice and backtracking may be necessary.
func ApplyRule ¶
Apply a rule to the state. No new state is created, no backtracking is performed here, an error is returned instead. Goals and constraints are potentially updated. Returns err!=nil if backtracking will be required.
func DoPredicate ¶
Execute predicates (recursively if needed) using the functor of the first goal. Includes removing underscore. Constant values (numbers, strings ...) are kept. State MAY change, if alternative must be considered (eg : 'or'), but only by forking. No backtracking is performed at this level, error is returned instead.
func NewState ¶
Creates a new state, using provided parent. Constraints and goals cloned from parent. Rules are copied but not cloned. Uid is copied verbatim. Next rule is set to 0.
func NewStateWithSession ¶
Create a new root state (ie, with nil parent) but with an existing session.
func Solve ¶
func Solve(st *State, sh SolutionHandler) *State
Solve for a given state. Backtracking is managed only in this function.
func (*State) RulesHistory ¶
a printable explanation of the rules applied to reach this state. rules are listed in the order they were applied.
type Underscore ¶
type Underscore = parser.Underscore
type VarGTENum ¶
Ensure V >= Value
func (VarGTENum) Check ¶
func (c VarGTENum) Check() (Constraint, error)
Check implements Constraint.
func (VarGTENum) Simplify ¶
func (c1 VarGTENum) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
Simplify implements Constraint.
type VarGTNum ¶
Ensure V > Value
func (VarGTNum) Simplify ¶
func (c1 VarGTNum) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
Simplify implements Constraint.
type VarINT ¶
type VarINT struct{ V Variable }
Force V to be any integer number NaN is not considered a valid number.
func (VarINT) Simplify ¶
func (c1 VarINT) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
Simplify implements Constraint.
type VarIsAtom ¶
func (VarIsAtom) Check ¶
func (c VarIsAtom) Check() (Constraint, error)
Check will check validity of constraint, clean it or simplify it. It will return the constraint itself, possibly modified, or nil if constraint should be ignored ( CAUTION : return can be nil, despite a nil error ! An error means the constraint is impossible to satisfy (e.g. positive occur check, empty number interval, ...)
func (VarIsAtom) Simplify ¶
func (c1 VarIsAtom) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
simplify c2, taking into account the calling constraint c1 (unchanged). if error, other results are not significant and should not be used. If changed, replace c by all of cc (possibly empty, to just suppress c). If changed is false, cc has no meaning. Input constraints MUST BE checked Output constraints are checked
type VarIsCompoundTerm ¶
Constraint for X = term
func (VarIsCompoundTerm) Check ¶
func (c VarIsCompoundTerm) Check() (Constraint, error)
Check will check validity of constraint, clean it or simplify it. It will return the constraint itself, possibly modified, or nil if constraint should be ignored ( CAUTION : return can be nil, despite a nil error ! An error means the constraint is impossible to satisfy (e.g. positive occur check, empty number interval, ...)
func (VarIsCompoundTerm) Clone ¶
func (c VarIsCompoundTerm) Clone() Constraint
Clone implements Constraint.
func (VarIsCompoundTerm) GetV ¶
func (c VarIsCompoundTerm) GetV() Variable
func (VarIsCompoundTerm) Simplify ¶
func (c1 VarIsCompoundTerm) Simplify(c Constraint) (cc []Constraint, changed bool, err error)
Simplify implements Constraint.
func (VarIsCompoundTerm) String ¶
func (v VarIsCompoundTerm) String() string
String implements Constraint.
type VarIsNum ¶
Ensure V = Number Value
func (VarIsNum) Simplify ¶
func (c1 VarIsNum) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
Simplify implements Constraint.
type VarIsString ¶
func (VarIsString) Check ¶
func (c VarIsString) Check() (Constraint, error)
Check will check validity of constraint, clean it or simplify it. It will return the constraint itself, possibly modified, or nil if constraint should be ignored ( CAUTION : return can be nil, despite a nil error ! An error means the constraint is impossible to satisfy (e.g. positive occur check, empty number interval, ...)
func (VarIsString) GetV ¶
func (c VarIsString) GetV() Variable
func (VarIsString) Simplify ¶
func (c1 VarIsString) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
simplify c2, taking into account the calling constraint c1 (unchanged). if error, other results are not significant and should not be used. If changed, replace c by all of cc (possibly empty, to just suppress c). If changed is false, cc has no meaning. Input constraints MUST BE checked Output constraints are checkedutput.
type VarIsVar ¶
func (VarIsVar) Check ¶
func (c VarIsVar) Check() (Constraint, error)
Check will check validity of constraint, clean it or simplify it. It will return the constraint itself, possibly modified, or nil if constraint should be ignored ( CAUTION : return can be nil, despite a nil error ! An error means the constraint is impossible to satisfy (e.g. positive occur check, empty number interval, ...) There is a cannonical order of variables, with Y = Y means Y is latest (highest Nsp)
func (VarIsVar) Simplify ¶
func (c1 VarIsVar) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
simplify c2, taking into account the calling constraint c1 (unchanged). if error, other results are not significant and should not be used. If changed, replace c by all of cc (possibly empty, to just suppress c). If changed is false, cc has no meaning. Input constraints MUST BE checked Output constraints are checked
type VarLTENum ¶
Ensure V <= Value
func (VarLTENum) Check ¶
func (c VarLTENum) Check() (Constraint, error)
Check implements Constraint.
func (VarLTENum) Simplify ¶
func (c1 VarLTENum) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
Simplify implements Constraint.
type VarLTNum ¶
Ensure V < Value
func (VarLTNum) Simplify ¶
func (c1 VarLTNum) Simplify(c2 Constraint) (cc []Constraint, changed bool, err error)
Simplify implements Constraint.
Source Files
¶
- consVarGTENum.go
- consVarGTNum.go
- consVarINT.go
- consVarIsAtom.go
- consVarIsCompoudTerm.go
- consVarIsNum.go
- consVarIsString.go
- consVarIsVar.go
- consVarLTENum.go
- consVarLTNum.go
- constraint.go
- depthControl.go
- predicates.go
- rules.go
- session.go
- session.repl.go.go
- solve.go
- state.go
- substitution.go
- unify.go
- utils.go
- version.go