grounder

package
v0.0.0-...-c730170 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Oct 18, 2021 License: MIT Imports: 11 Imported by: 0

Documentation

Index

Constants

This section is empty.

Variables

View Source 
var (
	DebugLevel int
)

Functions

func ComparisonString 

func ComparisonString(tokenComparison tokenKind) (s string)

func Debug 

func Debug(level int, s ...interface{})

func Expansion 

func Expansion(func(Groundable) (changed bool, result []Groundable, err error)) (bool, error)

func IsMarkedAsFree 

func IsMarkedAsFree(v string) bool

func TermTranslation 

func TermTranslation(termIterator TermIterator, transform func(Term) (Term, bool, error)) (changed bool, err error)

Types

type Clause 

type Clause []Literal

type Constraint 

type Constraint struct {
	LeftTerm   Term
	Comparison tokenKind
	RightTerm  Term
}

is a math expression that evaluates to true or false Constraints can contain variables supported are <,>,<=,>=,== E.g..: A*3v<=v5-2*R/7#mod3.

func (Constraint) Copy 

func (constraint Constraint) Copy() (cons Constraint)

func (Constraint) FreeVars 

func (constraint Constraint) FreeVars() *strset.Set

func (*Constraint) GroundBoolExpression 

func (constraint *Constraint) GroundBoolExpression() (isGround bool, result bool)

func (Constraint) IsInstantiation 

func (constraint Constraint) IsInstantiation() (is bool, variable string, value string, err error)

Checks if constraint is of the form X==<math>, or <math>==X ( math is ground ) It also does very simple equation solving for equations with one variable, like X-3+1==<math> .

func (*Constraint) String 

func (constraint *Constraint) String() string

type Groundable 

type Groundable interface {
	Terms() []*Term
	Literals() *[]Literal
	Constraints() *[]Constraint
	Generators() *[]Literal
	Copy() Groundable
}

/ IDEA to unify treatment of Iterator and Rule

type Iterator 

type Iterator struct {
	Constraints  []Constraint
	Conditionals []Literal
	Head         Literal
}

func (Iterator) AllTerms 

func (iterator Iterator) AllTerms() (terms []*Term)

func (Iterator) Copy 

func (iterator Iterator) Copy() (newGen Iterator)

Deep Copy

func (*Iterator) Simplify 

func (iterator *Iterator) Simplify(assignment map[string]string) (bool, error)

func (Iterator) String 

func (iterator Iterator) String() string

type LineNumberInfo 

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

type Literal 

type Literal struct {
	Neg   bool
	Fact  bool // if true then search variable with parenthesis () otherwise a fact with brackets []
	Name  Predicate
	Terms []Term
}

func (Literal) Copy 

func (literal Literal) Copy() Literal

func (Literal) FreeVars 

func (literal Literal) FreeVars() *strset.Set

func (Literal) IdString 

func (literal Literal) IdString() string

func (*Literal) IsGround 

func (literal *Literal) IsGround() bool

type LiteralError 

type LiteralError struct {
	L       Literal
	R       Rule
	Message string
}

func (LiteralError) Error 

func (err LiteralError) Error() string

type Predicate 

type Predicate string

func (Predicate) String 

func (name Predicate) String() string

type Program 

type Program struct {
	Rules     []Rule
	Constants map[string]string

	// grounding stuff, backups, hashmaps
	PredicateToArity      map[Predicate]int        //
	PredicateExplicit     map[Predicate]bool       // If there is a explicit quantification for predicate
	FinishCollectingFacts map[Predicate]bool       // True if no more rules with that predicate in in the head.
	PredicateToTuples     map[Predicate][][]string // Contains a slice of all tuples
	PredicateTupleMap     map[string]bool          // hashmap that contains all positive and negative ground atoms in the program

	// handle string terms
	// String terms are replaced by integers.
	// These two mappings are the bijective mapping from integers to these strings:
	String2IntId map[string]int // StringReplacement
	IntId2String map[int]string // StringReplacement

	//Quantification
	Alternation [][]Literal
	// contains filtered or unexported fields
}

func ParseProgram 

func ParseProgram(fileNames []string) (Program, error)

func ParseProgramFromStrings 

func ParseProgramFromStrings(lines []string, where []LineNumberInfo) (p Program, err error)

func (*Program) CheckArityOfLiterals 

func (p *Program) CheckArityOfLiterals() error

func (*Program) CheckFactsInIterators 

func (p *Program) CheckFactsInIterators() error

func (*Program) CheckNoExplicitDeclarationAndNonGroundExplicit 

func (p *Program) CheckNoExplicitDeclarationAndNonGroundExplicit() error

func (*Program) CheckNoGeneratorsOrIterators 

func (p *Program) CheckNoGeneratorsOrIterators() error

func (*Program) CheckSearch 

func (p *Program) CheckSearch() error

func (*Program) CheckUnboundVariables 

func (p *Program) CheckUnboundVariables() error

Check that there are no unbound variables All variables that only occur in exactly one term are not bound by others and must be marked as free and unbound (i.e. starting with underscore _)

func (*Program) CleanIteratorFromGroundBoolExpressions 

func (p *Program) CleanIteratorFromGroundBoolExpressions() (bool, error)

Remove Iterator if with false constraint Remove true constraints from Iterator

func (*Program) CleanRulesFromGroundBoolExpression 

func (p *Program) CleanRulesFromGroundBoolExpression() (bool, error)

Remove Rules with false constraint Remove true constraints from Rule This is essentially Unit Propagation on Constraint Instantiation

func (*Program) CollectExplicitTupleDefinitions 

func (p *Program) CollectExplicitTupleDefinitions() (bool, error)

Check if rule contains #exist or #forall literal! At version 3.0 of BULE, a definition rule has to have exactly 1 literal in the generator, 1 literal be ground, and have question mark! Then take literal and add tuple and add to quantification level

func (*Program) CollectGroundFacts 

func (p *Program) CollectGroundFacts() (changed bool, err error)

func (*Program) CollectGroundTuples 

func (p *Program) CollectGroundTuples() (bool, error)

func (*Program) CollectStringTermsToIntegers 

func (p *Program) CollectStringTermsToIntegers() error

If a term matches Constant term expression (as a string) then replace it by a number and remember this in maps. Replace this everywhere ! Assumptions: Integers above 1*10^9 never used in the programs !

func (*Program) ConstraintSimplification 

func (p *Program) ConstraintSimplification() (bool, error)

func (*Program) ConvertHeadOnlyIteratorsToLiterals 

func (p *Program) ConvertHeadOnlyIteratorsToLiterals() (bool, error)

func (*Program) ExpandGroundRanges 

func (p *Program) ExpandGroundRanges() (changed bool, err error)

func (*Program) ExtractQuantors 

func (p *Program) ExtractQuantors()

func (*Program) FindFactsThatAreFullyCollected 

func (p *Program) FindFactsThatAreFullyCollected() (changed bool, err error)

A fact is fully collected if it does not occur as a head in any rule. Exception is #exist and #forall

func (*Program) InsertLiteralTuple 

func (p *Program) InsertLiteralTuple(lit Literal) error

func (*Program) InstantiateAndRemoveFactFromGenerator 

func (p *Program) InstantiateAndRemoveFactFromGenerator() (changed bool, err error)

This resolves facts with clauses.

func (*Program) InstantiateAndRemoveFactFromIterator 

func (p *Program) InstantiateAndRemoveFactFromIterator() (changed bool, err error)

This resolves facts with clauses.

func (*Program) InstantiateExplicitNonGroundLiterals 

func (p *Program) InstantiateExplicitNonGroundLiterals() (changed bool, err error)

This resolves facts with clauses.

func (*Program) InstantiateNonGroundLiterals 

func (p *Program) InstantiateNonGroundLiterals() (changed bool, err error)

This resolves facts with clauses.

func (*Program) IsSATProblem 

func (p *Program) IsSATProblem() bool

func (*Program) MergeConsecutiveQuantificationLevels 

func (p *Program) MergeConsecutiveQuantificationLevels()

Translates forallQ and existsQ into quantification

func (*Program) OutputRuleString 

func (p *Program) OutputRuleString(rule *Rule) string

func (*Program) OutputString 

func (p *Program) OutputString(literal Literal) string

This is equivalent to the String() method but maps onto the string terms, if term is string

func (*Program) OutputTermString 

func (p *Program) OutputTermString(term string) (s string)

func (*Program) Print 

func (p *Program) Print()

func (*Program) PrintDebug 

func (p *Program) PrintDebug(level int)

func (*Program) PrintFacts 

func (p *Program) PrintFacts()

func (*Program) PrintQuantification 

func (p *Program) PrintQuantification()

func (*Program) PrintRules 

func (p *Program) PrintRules()

func (*Program) PrintTuples 

func (p *Program) PrintTuples()

func (*Program) RemoveClausesWithExplicitLiteralAndTuplesThatDontExist 

func (p *Program) RemoveClausesWithExplicitLiteralAndTuplesThatDontExist() (bool, error)

func (*Program) RemoveClausesWithTuplesThatDontExist 

func (p *Program) RemoveClausesWithTuplesThatDontExist() (bool, error)

func (*Program) RemoveLiteralsWithEmptyIterators 

func (p *Program) RemoveLiteralsWithEmptyIterators() (bool, error)

func (*Program) RemoveNegatedGroundGenerator 

func (p *Program) RemoveNegatedGroundGenerator() (changed bool, err error)

func (*Program) RemoveRules 

func (p *Program) RemoveRules(ifTrueRemove func(r Rule) bool) (changed bool, err error)

Remove all rules where check is true.

func (*Program) RemoveRulesWithGenerators 

func (p *Program) RemoveRulesWithGenerators() (bool, error)

func (*Program) RemoveRulesWithNegatedGroundGenerator 

func (p *Program) RemoveRulesWithNegatedGroundGenerator() (changed bool, err error)

func (*Program) ReplaceConstantsAndMathFunctions 

func (p *Program) ReplaceConstantsAndMathFunctions()

func (*Program) RuleExpansion 

func (p *Program) RuleExpansion(check func(r Rule) bool, expand func(Rule) ([]Rule, error)) (changed bool, err error)

goes through all rules and expands expands if check is true. Note that this does not expand the generated rules. (i.e. it does not run until fixpoint)

func (*Program) RuleTransformation 

func (p *Program) RuleTransformation(check func(r Rule) bool,
	transformation func(Rule) (Rule, error)) (changed bool, err error)

goes through all rules and translates if check is true. Singleton version of RuleExpansion

func (*Program) TermExpansion 

func (p *Program) TermExpansion(check func(r Term) bool, expand func(Term) ([]Term, error)) (changed bool, err error)

Check terms in literals and expands the rules according to the *first* term found according to it's expansion.

func (*Program) TransformConstraintsToInstantiation 

func (p *Program) TransformConstraintsToInstantiation() (bool, error)

for each Constraint X==<Value> Rewrite all Terms with X <- <Value>

func (*Program) TransformConstraintsToInstantiationIterator 

func (p *Program) TransformConstraintsToInstantiationIterator() (bool, error)

for each Constraint X==<Value> Rewrite all Terms with X <- <Value> Only within Iterators

type Rule 

type Rule struct {
	LineNumber     LineNumberInfo
	Parent         *Rule
	Generators     []Literal
	Constraints    []Constraint
	Literals       []Literal
	Iterators      []Iterator
	IsQuestionMark bool // if final token is tokenQuestionMark then it generates, otherwise tokenDot
	// contains filtered or unexported fields
}

func (Rule) AllLiterals 

func (rule Rule) AllLiterals() (literals []*Literal)

func (Rule) AllTerms 

func (rule Rule) AllTerms() (terms []*Term)

func (Rule) Copy 

func (rule Rule) Copy() (newRule Rule)

Deep Copy

func (*Rule) Debug 

func (rule *Rule) Debug() string

func (*Rule) FreeVars 

func (rule *Rule) FreeVars() *strset.Set

only works on disjunctions

func (*Rule) IsFact 

func (rule *Rule) IsFact() bool

func (*Rule) IsGround 

func (rule *Rule) IsGround() bool

func (*Rule) Simplify 

func (rule *Rule) Simplify(assignment map[string]string) (bool, error)

func (*Rule) String 

func (rule *Rule) String() string

type RuleError 

type RuleError struct {
	R       Rule
	Message string
	Err     error
}

func (RuleError) Error 

func (err RuleError) Error() string

type SepToken 

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

type Term 

type Term string

func (Term) FreeVars 

func (term Term) FreeVars() *strset.Set

func (Term) Ground 

func (term Term) Ground() bool

is either a constant term or a number

func (Term) String 

func (term Term) String() string

type TermIterator 

type TermIterator interface {
	AllTerms() []*Term
}

type Token 

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

Token is accumulated while lexing the provided input, and emitted over a channel to the parser.

type Tokens 

type Tokens []Token

func (Tokens) Debug 

func (ts Tokens) Debug() string

func (Tokens) String 

func (ts Tokens) String() string

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.