diff --git a/cmd/stages.go b/cmd/stages.go index 6cc4a8b..f5e4b72 100644 --- a/cmd/stages.go +++ b/cmd/stages.go @@ -2,9 +2,12 @@ package cmd import ( "fmt" - bule "github.com/vale1410/bule/grounder" + "log" "os" "strconv" + "time" + + bule "github.com/vale1410/bule/grounder" ) func stage0Prerequisites(p *bule.Program) { @@ -67,9 +70,10 @@ func stage1GeneratorsAndFacts(p *bule.Program) { runFixpoint(p.ExpandGroundRanges), "ExpandGroundRanges", "p[1..2]. and also X==1..2, but not Y==A..B.") + stage(p, &changed, p.ConstraintSimplification, - "Do Fixpoint of TransformConstraintsToInstantiation.", + "ConstraintSimplification.", "For each constraint (X==v) rewrite clause with (X<-v) and remove constraint.") stage(p, &changed, @@ -89,7 +93,7 @@ func stage1GeneratorsAndFacts(p *bule.Program) { stage(p, &changed, p.ConstraintSimplification, - "Do Fixpoint of TransformConstraintsToInstantiation.", + "ConstraintSimplification.", "For each constraint (X==v) rewrite clause with (X<-v) and remove constraint.") stage(p, &changed, @@ -111,7 +115,7 @@ func stage1GeneratorsAndFacts(p *bule.Program) { stage(p, &changed, p.RemoveRulesWithGenerators, "RemoveRulesWithGeneratorsBecauseTheyHaveEmptyDomains", - "Because they have empty domains, e.g. \n edge[_,_,V] => vertex[V]. %% there are no edges!") + "Because they have empty domains, e.g. \n edge[_,_,V] :: vertex[V]. %% there are no edges!") } // Unroll all iterators. @@ -240,6 +244,7 @@ func stage4Printing(p *bule.Program, args []string) { } func stage(p *bule.Program, change *bool, f func() (bool, error), stage string, info string) { + start := time.Now() stageInfo(p, stage, info) tmp, err := f() if err != nil { @@ -251,6 +256,9 @@ func stage(p *bule.Program, change *bool, f func() (bool, error), stage string, debug(2, "Stage changed Program!") } *change = *change || tmp + + elapsed := time.Since(start) + log.Printf("DEBUGTIME %6.2f %v %v", elapsed.Seconds(), stage, len(p.Rules)) } func runFixpoint(f func() (bool, error)) func() (bool, error) { diff --git a/grounder/ground.go b/grounder/ground.go index 1ea0f78..2218ba3 100644 --- a/grounder/ground.go +++ b/grounder/ground.go @@ -14,6 +14,7 @@ import ( func (p *Program) ConstraintSimplification() (bool, error) { finalChanged := true + //start := time.Now() i := 0 for { @@ -22,6 +23,9 @@ func (p *Program) ConstraintSimplification() (bool, error) { if err != nil { return true, fmt.Errorf("Constraint simplification, iteration %v. \n %w", i, err) } + //elapsed := time.Since(start) + //start = time.Now() + //log.Printf("X-DEBUGTIME %6.2f %v %v Constraints->Instantiation", elapsed.Seconds(), i, len(p.Rules)) if !changed { //Debug(2, "Remove clauses with contradictions, e.g. (1==2) or (1!=1), and remove true constraints, e.g. (1>2, 1==1).") finalChanged, err = p.CleanRulesFromGroundBoolExpression() @@ -30,6 +34,9 @@ func (p *Program) ConstraintSimplification() (bool, error) { } break } + //elapsed = time.Since(start) + //start = time.Now() + //log.Printf("X-DEBUGTIME %6.2f %v %v CleanRules", elapsed.Seconds(), i, len(p.Rules)) } return finalChanged || i > 1, nil } @@ -153,6 +160,7 @@ func (p *Program) findFilteredTuples(literal Literal) [][]string { filteredTuples = append(filteredTuples, tuple) } } + // fmt.Println("DEBUG", literal, filteredTuples) return filteredTuples } @@ -421,6 +429,11 @@ func (p *Program) CleanRulesFromGroundBoolExpression() (bool, error) { return true } } + for _, lit := range r.Generators { + if p.FinishCollectingFacts[lit.Name] && lit.IsGround() { + return true + } + } return false } @@ -437,6 +450,22 @@ func (p *Program) CleanRulesFromGroundBoolExpression() (bool, error) { newRule.Constraints = append(newRule.Constraints, cons) } } + newRule.Generators = []Literal{} + for _, lit := range rule.Generators { + if p.FinishCollectingFacts[lit.Name] && lit.IsGround() { + // fmt.Println("DEBUG", lit.IdString(), "\n", p.FinishCollectingFacts, "\n", p.PredicateTupleMap) + if lit.Neg && p.PredicateTupleMap[lit.createNegatedLiteral().IdString()] { + // fmt.Println("DEBUG REMOVE", rule.String()) + return []Rule{}, nil + } else if !lit.Neg && p.PredicateTupleMap[lit.IdString()] { + // fmt.Println("DEBUG DO NOT REMOVE", rule.String()) + } else { + newRule.Generators = append(newRule.Generators, lit) + } + } else { + newRule.Generators = append(newRule.Generators, lit) + } + } return []Rule{newRule}, nil } return p.RuleExpansion(check, transform) diff --git a/grounder/transformation.go b/grounder/transformation.go index ef25fc2..7dd05da 100644 --- a/grounder/transformation.go +++ b/grounder/transformation.go @@ -2,6 +2,7 @@ package grounder import ( "fmt" + "github.com/scylladb/go-set/strset" ) @@ -143,30 +144,6 @@ func TermTranslation(termIterator TermIterator, transform func(Term) (Term, bool return } -//func (iterator *Iterator) TermTranslation(transform func(Term) (Term, bool, error)) (changed bool, err error) { -// var ok bool -// for _, term := range iterator.AllTerms() { -// *term, ok, err = transform(*term) -// changed = ok || changed -// if err != nil { -// return changed, err -// } -// } -// return -//} -// -//func (rule *Rule) TermTranslation(transform func(Term) (Term, bool, error)) (changed bool, err error) { -// var ok bool -// for _, term := range rule.AllTerms() { -// *term, ok, err = transform(*term) -// changed = ok || changed -// if err != nil { -// return changed, err -// } -// } -// return -//} - func (iterator Iterator) AllTerms() (terms []*Term) { for i := range iterator.Head.Terms {