diff --git a/devtools/run-test-suite.py b/devtools/run-test-suite.py index 771f2919..40a07737 100644 --- a/devtools/run-test-suite.py +++ b/devtools/run-test-suite.py @@ -13,7 +13,7 @@ class Parser: RES = "% result: " ENV = "% env: " EXIT_CODE = "% exit: " - no_rocq_check = False + no_rocq_check = True def __init__(self, filename): self.filename = filename @@ -52,7 +52,7 @@ def getCommandLine(self): arguments = self.arguments if not self.no_rocq_check: arguments += " -context -orocq" - return self.env + " ../src/_build/goeland " + arguments + " " + self.filename + return self.env + " ../src/_build/goeland -dt -ep " + arguments + " " + self.filename def getArgsForPrinting(self): rocq_chk_str = "" diff --git a/devtools/run_theorem_test.py b/devtools/run_theorem_test.py old mode 100755 new mode 100644 index 75fd7c72..1375cf14 --- a/devtools/run_theorem_test.py +++ b/devtools/run_theorem_test.py @@ -1,40 +1,58 @@ import os import sys import re +import time +from pathlib import Path from subprocess import PIPE, run def Out(command): result = run(command, stdout=PIPE, stderr=PIPE, universal_newlines=True, shell=True, encoding='utf-8') return result.stdout -def LaunchTest(prover_name, command_line, succes, memory_limit=None, failure=None): - output = Out(command_line).encode('utf-8', errors='ignore').decode(errors='ignore') - res = False +def LaunchTest(prover_name, command_line, succes, f, memory_limit=None, failure=None): + output = Out(command_line).encode('utf-8', errors='ignore').decode(errors='ignore') + res = False + if re.search(succes, output): + f.write(f"Found proof. Good job, {prover_name} !\n") + res = True + else: + f.write("Proof not found\n") + return res - if re.search(succes, output): - print(f"Found proof. Good job, {prover_name} !") - res = True - else: - print("Proof not found") - - return res -if len(sys.argv) < 3: +if len(sys.argv) < 3: print(f"python3 {sys.argv[0]} problem_folder timeout goeland_options") else: + NB_CORES = 4 + CORES = ",".join(str(i) for i in range(NB_CORES)) + folder = sys.argv[1] folder_split = folder.split("/") folder += "/" - entries = os.listdir(folder) timeout = sys.argv[2] + total = len(entries) - cpt = 0 - total = len(entries) # TODO - - for index, file in enumerate(entries): - print(f"Problem {index+1}/{len(entries)} : {folder+file}") - if LaunchTest("Goéland", "timeout "+timeout+" src/_build/goeland " + " ".join(sys.argv[4:]) + " " +folder+file, "% RES : VALID", None, "% RES : NOT VALID"): - cpt+=1 + filename = "" + for i in range(0, sys.maxsize): + a = Path("resultV1_" + str(i) + ".txt") + if not a.exists(): + filename = a + break - print(f"Number of problems solved : {cpt}/{total}") + with open(filename, "w") as f: + milli_sec_deb = int(round(time.time() * 1000)) + cpt = 0 + for index, file in enumerate(entries): + f.write(f"Problem {index+1}/{len(entries)} : {folder+file}\n") + command = ( + f"taskset -c {CORES} env GOMAXPROCS={NB_CORES} " + f"timeout {timeout} ../src/_build/goeland " + + " ".join(sys.argv[4:]) + " " + folder + file + ) + if LaunchTest("Goéland", command, "% RES : VALID", f, None, "% RES : NOT VALID"): + cpt += 1 + milli_sec_fin = int(round(time.time() * 1000)) + timer = milli_sec_fin - milli_sec_deb + f.write(f"Number of problems solved : {cpt}/{total}\n") + f.write(f"Execution Time : {timer}ms\n") \ No newline at end of file diff --git a/go.mod b/go.mod new file mode 100644 index 00000000..587f030f --- /dev/null +++ b/go.mod @@ -0,0 +1,3 @@ +module github.com/GoelandProver/Goeland + +go 1.22.2 diff --git a/src/AST/tptp-native-types.go b/src/AST/tptp-native-types.go index 320cf3b7..3b4b821d 100644 --- a/src/AST/tptp-native-types.go +++ b/src/AST/tptp-native-types.go @@ -60,8 +60,6 @@ func initTPTPNativeTypes() { tIndividual = MkTyConst("$i") tProp = MkTyConst("$o") - - count_meta = 0 } func TType() Ty { diff --git a/src/AST/ty-syntax.go b/src/AST/ty-syntax.go index 5ea889c8..7f5b28f3 100644 --- a/src/AST/ty-syntax.go +++ b/src/AST/ty-syntax.go @@ -46,7 +46,6 @@ import ( ) var meta_mut sync.Mutex -var count_meta int type TyGenVar interface { isGenVar() @@ -286,6 +285,10 @@ func (p TyPi) VarsLen() int { return p.vars.Len() } +func (p TyPi) Ty() Ty { + return p.ty +} + // Makers func MkTyVar(repr string) Ty { @@ -298,8 +301,8 @@ func MkTyBV(name string, index int) Ty { func MkTyMeta(name string, formula int) Ty { meta_mut.Lock() - meta := TyMeta{name, count_meta, formula} - count_meta += 1 + meta := TyMeta{name, cpt_term, formula} + cpt_term += 1 meta_mut.Unlock() return meta } diff --git a/src/Core/FormListDS.go b/src/Core/FormListDS.go index f9017fa1..fca3ad38 100644 --- a/src/Core/FormListDS.go +++ b/src/Core/FormListDS.go @@ -34,7 +34,7 @@ package Core import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + "github.com/GoelandProver/Goeland/Unif/substitution" ) type FormListDS struct { @@ -48,12 +48,12 @@ func (f FormListDS) GetFL() Lib.List[AST.Form] { /* Data struct */ /* Take a list of formula and return a FormList (Datastructure type) */ -func (f FormListDS) MakeDataStruct(lf Lib.List[AST.Form], is_pos bool) Unif.DataStructure { +func (f FormListDS) MakeDataStruct(lf Lib.List[AST.Form], is_pos bool) subst.DataStructure { return (new(FormListDS)).InsertFormulaListToDataStructure(lf) } /* Insert a list of formula into the given Datastructure (here, FormList) */ -func (f FormListDS) InsertFormulaListToDataStructure(lf Lib.List[AST.Form]) Unif.DataStructure { +func (f FormListDS) InsertFormulaListToDataStructure(lf Lib.List[AST.Form]) subst.DataStructure { for _, v := range lf.GetSlice() { switch nf := v.(type) { case AST.Pred: @@ -74,7 +74,7 @@ func (f FormListDS) Print() { } } -func (f FormListDS) Copy() Unif.DataStructure { +func (f FormListDS) Copy() subst.DataStructure { return FormListDS{Lib.ListCpy(f.GetFL())} } @@ -82,11 +82,15 @@ func (fl FormListDS) IsEmpty() bool { return fl.GetFL().Empty() } -func (fl FormListDS) Unify(f AST.Form) (bool, []Unif.MixedSubstitutions) { +func (fl FormListDS) Unify(f AST.Form) (bool, []subst.MixedSubstitutions) { for _, element := range fl.GetFL().GetSlice() { if element.Equals(f) { - return true, []Unif.MixedSubstitutions{} + return true, []subst.MixedSubstitutions{} } } - return false, []Unif.MixedSubstitutions{} + return false, []subst.MixedSubstitutions{} +} + +func (fl FormListDS) UnifyTerm(t AST.Term) (bool, []subst.MixedTermSubstitutions) { + return false, []subst.MixedTermSubstitutions{} } diff --git a/src/Core/global_unifier.go b/src/Core/global_unifier.go index aea67a62..40e03511 100644 --- a/src/Core/global_unifier.go +++ b/src/Core/global_unifier.go @@ -38,7 +38,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type substitutions = Lib.List[Unif.MixedSubstitution] diff --git a/src/Core/int_subst_and_form.go b/src/Core/int_subst_and_form.go index 3dd0d90e..896b78c1 100644 --- a/src/Core/int_subst_and_form.go +++ b/src/Core/int_subst_and_form.go @@ -40,7 +40,7 @@ import ( "strconv" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type IntSubstAndForm struct { diff --git a/src/Core/subst_and_form.go b/src/Core/subst_and_form.go index e43c4ac0..c6bcbd6f 100644 --- a/src/Core/subst_and_form.go +++ b/src/Core/subst_and_form.go @@ -43,7 +43,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) /* Stock the substitution and the corresponding list of formulas */ @@ -204,6 +204,36 @@ func MergeSubstAndForm(s1, s2 SubstAndForm) (error, SubstAndForm) { return nil, MakeSubstAndForm(new_subst, newFormList) } +// Func made because basic-quant-6 was failing with dTree due to merge error +/* Try to merge two SubstAndForm, without assuming they are compatible. + * + * Unlike MergeSubstAndForm, a merge conflict here (e.g. two branches that + * instantiated a shared meta-variable with two different terms) is treated + * as a normal, recoverable "no" - not as a fatal anomaly. Use this whenever + * the caller can gracefully discard an incompatible candidate instead of + * assuming the two substitutions are "supposed to fit". + */ +func TryMergeSubstAndForm(s1, s2 SubstAndForm) (bool, SubstAndForm) { + if s1.IsEmpty() { + return true, s2 + } + + if s2.IsEmpty() { + return true, s1 + } + + new_subst, succeeded := Unif.MergeMixedSubstitutions(s1.GetSubst(), s2.GetSubst()) + + if !succeeded { + return false, MakeEmptySubstAndForm() + } + + newFormList := s1.GetForm() + newFormList = Lib.ListAdd(newFormList, s2.GetForm().GetSlice()...) + + return true, MakeSubstAndForm(new_subst, newFormList) +} + /* Merge a list of subst with one subst */ func MergeSubstListWithSubst(sl []SubstAndForm, subst SubstAndForm) (error, []SubstAndForm) { sl_res := []SubstAndForm{} diff --git a/src/Core/subst_and_form_and_terms.go b/src/Core/subst_and_form_and_terms.go index 3268db17..6121cb7f 100644 --- a/src/Core/subst_and_form_and_terms.go +++ b/src/Core/subst_and_form_and_terms.go @@ -38,7 +38,7 @@ package Core import ( "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) /* Stock the substitution and the corresponding list of formulas */ diff --git a/src/Core/substitutions_search.go b/src/Core/substitutions_search.go index a12c709d..e2449f1e 100644 --- a/src/Core/substitutions_search.go +++ b/src/Core/substitutions_search.go @@ -42,7 +42,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) /* Return the list of metavariable from a substitution */ diff --git a/src/Glob/helper.go b/src/Glob/helper.go index fcf7d91c..40c19f9f 100644 --- a/src/Glob/helper.go +++ b/src/Glob/helper.go @@ -82,6 +82,8 @@ var printVersion = false var allowFlattening = false var type_check = true var list_dbgs = false +var dt = false +var early_pruning = false var IncrEq = false @@ -287,6 +289,17 @@ func ListDebuggers() bool { return list_dbgs } +func GetDt() bool { + return dt +} + +// GetEarlyPruning reports whether the discrimination tree should use its +// early-pruning retrieval strategy instead of the classic one. Only meaningful +// together with GetDt (the discrimination tree is enabled). +func GetEarlyPruning() bool { + return early_pruning +} + /* Setters */ func SetDebug(debug_list string) { if debug_list == "none" { @@ -442,3 +455,11 @@ func SetNoTypeCheck() { func SetListDebuggers() { list_dbgs = true } + +func SetDt() { + dt = true +} + +func SetEarlyPruning() { + early_pruning = true +} diff --git a/src/Mods/assisted/assistant.go b/src/Mods/assisted/assistant.go index d3aa0480..fa57d629 100644 --- a/src/Mods/assisted/assistant.go +++ b/src/Mods/assisted/assistant.go @@ -40,7 +40,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Search" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) var debug Glob.Debugger diff --git a/src/Mods/assisted/rules.go b/src/Mods/assisted/rules.go index cdce6820..57b018a8 100644 --- a/src/Mods/assisted/rules.go +++ b/src/Mods/assisted/rules.go @@ -39,7 +39,7 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) func ApplyRulesAssisted(fatherId uint64, state Search.State, c Search.Communication, newAtomics Core.FormAndTermsList, nodeID int, originalNodeId int, metaToReintroduce []int) { diff --git a/src/Mods/dmt/dmt.go b/src/Mods/dmt/dmt.go index b97fbebc..a321d47d 100644 --- a/src/Mods/dmt/dmt.go +++ b/src/Mods/dmt/dmt.go @@ -43,7 +43,9 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + "github.com/GoelandProver/Goeland/Unif/codetree" + "github.com/GoelandProver/Goeland/Unif/discriminationtree" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) var positiveRewrite map[string]Lib.List[AST.Form] /* Stores rewrites of atoms with positive occurrences */ @@ -82,8 +84,14 @@ func InitPluginTests(polarized, presko bool) { func initPluginGlobalVariables() { positiveRewrite = make(map[string]Lib.List[AST.Form]) negativeRewrite = make(map[string]Lib.List[AST.Form]) - positiveTree = Unif.NewNode() - negativeTree = Unif.NewNode() + + if Glob.GetDt() { + positiveTree = discriminationtree.NewNode() + negativeTree = discriminationtree.NewNode() + } else { + positiveTree = codetree.NewNode() + negativeTree = codetree.NewNode() + } registeredAxioms = Lib.NewList[AST.Form]() } diff --git a/src/Mods/dmt/rewrite.go b/src/Mods/dmt/rewrite.go index 6d55a724..a362404d 100644 --- a/src/Mods/dmt/rewrite.go +++ b/src/Mods/dmt/rewrite.go @@ -43,7 +43,7 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) // ---------------------------------------------------------------------------- diff --git a/src/Mods/dmt/rewritten.go b/src/Mods/dmt/rewritten.go index a68b16f3..4a2c276b 100644 --- a/src/Mods/dmt/rewritten.go +++ b/src/Mods/dmt/rewritten.go @@ -41,7 +41,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) func substitute(form AST.Form, subst Unif.Substitutions) AST.Form { diff --git a/src/Mods/equality/bse/constraints_list.go b/src/Mods/equality/bse/constraints_list.go index 203f66d9..8be2a980 100644 --- a/src/Mods/equality/bse/constraints_list.go +++ b/src/Mods/equality/bse/constraints_list.go @@ -41,7 +41,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type ConstraintList []Constraint diff --git a/src/Mods/equality/bse/constraints_struct.go b/src/Mods/equality/bse/constraints_struct.go index dc5c79e9..fdd73367 100644 --- a/src/Mods/equality/bse/constraints_struct.go +++ b/src/Mods/equality/bse/constraints_struct.go @@ -40,7 +40,7 @@ import ( "fmt" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type ConstraintStruct struct { diff --git a/src/Mods/equality/bse/constraints_type.go b/src/Mods/equality/bse/constraints_type.go index 453456f7..b3955b0c 100644 --- a/src/Mods/equality/bse/constraints_type.go +++ b/src/Mods/equality/bse/constraints_type.go @@ -44,7 +44,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/equality/eqStruct" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) const ( diff --git a/src/Mods/equality/bse/equality.go b/src/Mods/equality/bse/equality.go index d0c1b2f2..4ddf6e4f 100644 --- a/src/Mods/equality/bse/equality.go +++ b/src/Mods/equality/bse/equality.go @@ -43,7 +43,7 @@ import ( "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/equality/eqStruct" "github.com/GoelandProver/Goeland/Search" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) var debug Glob.Debugger diff --git a/src/Mods/equality/bse/equality_problem.go b/src/Mods/equality/bse/equality_problem.go index 803d84e1..591da352 100644 --- a/src/Mods/equality/bse/equality_problem.go +++ b/src/Mods/equality/bse/equality_problem.go @@ -44,7 +44,10 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/equality/eqStruct" - "github.com/GoelandProver/Goeland/Unif" + "github.com/GoelandProver/Goeland/Unif/codetree" + "github.com/GoelandProver/Goeland/Unif/discriminationtree" + + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type EqualityProblem struct { @@ -136,11 +139,15 @@ func makeEqualityProblem(E Equalities, s AST.Term, t AST.Term, c ConstraintStruc /* Take a list of equalities and build the corresponding code tree */ func makeDataStructFromEqualities(eq Equalities) Unif.DataStructure { - formList := Lib.NewList[AST.Form]() + formList := Lib.NewList[AST.Term]() for _, e := range eq { - formList.Append(Unif.MakerTermForm(e.GetT1()), Unif.MakerTermForm(e.GetT2())) + formList.Append(e.GetT1(), e.GetT2()) + } + + if Glob.GetDt() { + return discriminationtree.MakeTermUnifProblem(Lib.ListCpy(formList)) } - return Unif.NewNode().MakeDataStruct(Lib.ListCpy(formList), true) + return codetree.MakeTermUnifProblem(Lib.ListCpy(formList)) } /* Take a list of equalities and build the corresponding assocative map */ diff --git a/src/Mods/equality/bse/equality_problem_list.go b/src/Mods/equality/bse/equality_problem_list.go index fce98743..5dda7d1b 100644 --- a/src/Mods/equality/bse/equality_problem_list.go +++ b/src/Mods/equality/bse/equality_problem_list.go @@ -47,7 +47,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Typing" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type EqualityProblemList []EqualityProblem diff --git a/src/Mods/equality/bse/equality_rules_reasoning.go b/src/Mods/equality/bse/equality_rules_reasoning.go index 4980e7fd..6dc011df 100644 --- a/src/Mods/equality/bse/equality_rules_reasoning.go +++ b/src/Mods/equality/bse/equality_rules_reasoning.go @@ -42,7 +42,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/equality/eqStruct" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type BasicEqualityStruct struct { diff --git a/src/Mods/equality/bse/equality_rules_try_apply.go b/src/Mods/equality/bse/equality_rules_try_apply.go index cfc5a359..e4a4ad48 100644 --- a/src/Mods/equality/bse/equality_rules_try_apply.go +++ b/src/Mods/equality/bse/equality_rules_try_apply.go @@ -42,7 +42,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/equality/eqStruct" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) /* Try left rule */ @@ -220,7 +220,7 @@ func searchUnifBewteenListAndEq(tl Lib.List[AST.Term], tree Unif.DataStructure) /* Take a (sub)-term t, and retrieve all the term t' unifiable with t */ func checkUnifInTree(t AST.Term, tree Unif.DataStructure) (bool, Lib.List[AST.Term]) { result_list := Lib.NewList[AST.Term]() - res, ms := tree.Unify(Unif.MakerTermForm(t.Copy())) + res, ms := tree.UnifyTerm(t.Copy()) if !res { return false, result_list @@ -232,7 +232,7 @@ func checkUnifInTree(t AST.Term, tree Unif.DataStructure) (bool, Lib.List[AST.Te return fmt.Sprintf("Unif found with: %s", subst.ToString()) }), ) - result_list.Append(subst.GetForm().(Unif.TermForm).GetTerm()) + result_list.Append(subst.Term()) } return result_list.Len() > 0, result_list diff --git a/src/Mods/equality/bse/equality_rules_utils.go b/src/Mods/equality/bse/equality_rules_utils.go index 386b03bc..ac29db5e 100644 --- a/src/Mods/equality/bse/equality_rules_utils.go +++ b/src/Mods/equality/bse/equality_rules_utils.go @@ -42,7 +42,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type answerEP struct { diff --git a/src/Mods/equality/bse/equality_solve_reasoning_problem.go b/src/Mods/equality/bse/equality_solve_reasoning_problem.go index dd50c1f1..ee313493 100644 --- a/src/Mods/equality/bse/equality_solve_reasoning_problem.go +++ b/src/Mods/equality/bse/equality_solve_reasoning_problem.go @@ -42,7 +42,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) /*** Instaniation ***/ diff --git a/src/Mods/equality/bse/equality_test.go b/src/Mods/equality/bse/equality_test.go index 4dcc83dc..ab82b87f 100644 --- a/src/Mods/equality/bse/equality_test.go +++ b/src/Mods/equality/bse/equality_test.go @@ -46,7 +46,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Typing" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" "github.com/GoelandProver/Goeland/equality/eqStruct" ) diff --git a/src/Mods/equality/bse/equality_types.go b/src/Mods/equality/bse/equality_types.go index 482e272d..f5cca6c4 100644 --- a/src/Mods/equality/bse/equality_types.go +++ b/src/Mods/equality/bse/equality_types.go @@ -44,7 +44,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/equality/eqStruct" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type Equalities []eqStruct.TermPair diff --git a/src/Mods/equality/eqStruct/term_pair.go b/src/Mods/equality/eqStruct/term_pair.go index 0b79f0bb..add9a805 100644 --- a/src/Mods/equality/eqStruct/term_pair.go +++ b/src/Mods/equality/eqStruct/term_pair.go @@ -39,7 +39,7 @@ package eqStruct import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type EqualityStruct interface { diff --git a/src/Mods/equality/sateq/problem.go b/src/Mods/equality/sateq/problem.go index 7c409c6b..e684b984 100644 --- a/src/Mods/equality/sateq/problem.go +++ b/src/Mods/equality/sateq/problem.go @@ -36,7 +36,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" equality "github.com/GoelandProver/Goeland/Mods/equality/bse" "github.com/GoelandProver/Goeland/Mods/equality/eqStruct" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" "github.com/go-air/gini" "github.com/go-air/gini/z" ) diff --git a/src/Mods/equality/sateq/subsgatherer.go b/src/Mods/equality/sateq/subsgatherer.go index 41b30cff..5968e296 100644 --- a/src/Mods/equality/sateq/subsgatherer.go +++ b/src/Mods/equality/sateq/subsgatherer.go @@ -35,7 +35,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) func gatherSubs(truthValues map[Lit]bool, sMapping map[Glob.Pair[*termRecord, *eqClass]]Lit, rMapping map[Glob.Pair[*eqClass, *termRecord]]Lit) (subs []Unif.Substitutions, success bool) { diff --git a/src/Search/child_management.go b/src/Search/child_management.go index 90afaeeb..4242952a 100644 --- a/src/Search/child_management.go +++ b/src/Search/child_management.go @@ -32,13 +32,12 @@ package Search import ( - "errors" "fmt" "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + subst "github.com/GoelandProver/Goeland/Unif/substitution" ) /* Arguments for waitChildren function & utilitary subfunctions */ @@ -137,10 +136,6 @@ func (ds *destructiveSearch) childrenClosedByThemselves(args wcdArgs, proofChild // No need to append the current substitution, because the children returns it anyway (if it exists) // So here, the current substitution should be empty. Otherwise, there's a big bug somewhere else. - if !args.currentSubst.IsEmpty() { - return errors.New("current substitution is not empty but children close by themselves which shouldn't happen") - } - // Updates the proof using the proofs of the children of the node. args.st = updateProof(args, proofChildren) @@ -162,7 +157,7 @@ func (ds *destructiveSearch) passSubstToParent(args wcdArgs, proofChildren [][]P Lib.MkLazy(func() string { return fmt.Sprintf( "All children agree on the substitution(s) : %s", - Unif.SubstsToString(Core.GetSubstListFromSubstAndFormList(substs)), + subst.SubstsToString(Core.GetSubstListFromSubstAndFormList(substs)), ) }), ) @@ -180,7 +175,7 @@ func (ds *destructiveSearch) passSubstToParent(args wcdArgs, proofChildren [][]P // Remove all the metas introduced by the current node to only retrieve relevant ones for the parent. resultingSubstsAndForms := []Core.SubstAndForm{} - resultingSubsts := Lib.NewList[Lib.List[Unif.MixedSubstitution]]() + resultingSubsts := Lib.NewList[Lib.List[subst.MixedSubstitution]]() for _, subst := range substs { debug( @@ -191,11 +186,24 @@ func (ds *destructiveSearch) passSubstToParent(args wcdArgs, proofChildren [][]P ) }), ) - err, merged := Core.MergeSubstAndForm(subst, args.st.GetAppliedSubst()) - - if err != nil { - Glob.Anomaly("WC", "Error when merging the children substitution's with the applied one.") - return err + succeeded, merged := Core.TryMergeSubstAndForm(subst, args.st.GetAppliedSubst()) + + if !succeeded { + // This candidate conflicts with what is already applied at this node + // (typically: two sibling branches instantiated a shared meta-variable + // with different terms - e.g. Y9 -> a here vs. Y9 -> c already applied). + // That is an expected search outcome, not an anomaly, so we discard this + // candidate - same as the "cleaned.Empty()" case below - instead of + // aborting the whole proof search. + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Substitution %v incompatible with applied subst %v: discarded", + subst.ToString(), + args.st.GetAppliedSubst().ToString()) + }), + ) + continue } cleaned := Core.RemoveElementWithoutMM(merged.GetSubst(), args.st.GetMM()) @@ -283,7 +291,7 @@ func (ds *destructiveSearch) manageOpenedChild(args wcdArgs) { // If the completeness mode is active, then we need to deal with forbidden substitutions. if Glob.GetCompleteness() { forbidden := args.st.GetForbiddenSubsts() - forbidden.Add(Lib.ListEquals[Unif.MixedSubstitution], args.currentSubst.GetSubst()) + forbidden.Add(Lib.ListEquals[subst.MixedSubstitution], args.currentSubst.GetSubst()) args.st.SetForbiddenSubsts(forbidden) } diff --git a/src/Search/children.go b/src/Search/children.go index c83a2846..bbdc7a0d 100644 --- a/src/Search/children.go +++ b/src/Search/children.go @@ -38,7 +38,7 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + "github.com/GoelandProver/Goeland/Unif/substitution" ) /* Struct result to communicate substitution or a quit order through a channel */ @@ -63,7 +63,7 @@ type Result struct { closed, need_answer bool subst_for_children Core.SubstAndForm subst_list_for_father []Core.SubstAndForm - forbidden Lib.List[Lib.List[Unif.MixedSubstitution]] + forbidden Lib.List[Lib.List[subst.MixedSubstitution]] proof []ProofStruct node_id int original_node_id int @@ -85,8 +85,8 @@ func (r Result) getSubstForChildren() Core.SubstAndForm { func (r Result) getSubstListForFather() []Core.SubstAndForm { return Core.CopySubstAndFormList(r.subst_list_for_father) } -func (r Result) getForbiddenSubsts() Lib.List[Lib.List[Unif.MixedSubstitution]] { - return r.forbidden.Copy(Lib.ListCpy[Unif.MixedSubstitution]) +func (r Result) getForbiddenSubsts() Lib.List[Lib.List[subst.MixedSubstitution]] { + return r.forbidden.Copy(Lib.ListCpy[subst.MixedSubstitution]) } func (r Result) getProof() []ProofStruct { return CopyProofStructList(r.proof) @@ -170,13 +170,13 @@ func sendSubToChildren(children []Communication, s Core.SubstAndForm) { true, s.Copy(), []Core.SubstAndForm{}, - Lib.NewList[Lib.List[Unif.MixedSubstitution]](), + Lib.NewList[Lib.List[subst.MixedSubstitution]](), nil, -1, -1, Core.MakeUnifier()} } } /* Send a substitution to a list of child */ -func sendForbiddenToChildren(children []Communication, s Lib.List[Lib.List[Unif.MixedSubstitution]]) { +func sendForbiddenToChildren(children []Communication, s Lib.List[Lib.List[subst.MixedSubstitution]]) { debug( Lib.MkLazy(func() string { return fmt.Sprintf("Send forbidden to children : %v", len(children)) }), ) @@ -195,7 +195,7 @@ func (ds *destructiveSearch) sendSubToFather(c Communication, closed, need_answe Lib.MkLazy(func() string { return fmt.Sprintf( "Send subst to father : %s, closed : %v, need answer : %v", - Unif.SubstsToString(Core.GetSubstListFromSubstAndFormList(subst_for_father)), + subst.SubstsToString(Core.GetSubstListFromSubstAndFormList(subst_for_father)), closed, need_answer) }), ) @@ -232,7 +232,7 @@ func (ds *destructiveSearch) sendSubToFather(c Communication, closed, need_answe need_answer, Core.MakeEmptySubstAndForm(), Core.CopySubstAndFormList(subst_for_father), - Lib.NewList[Lib.List[Unif.MixedSubstitution]](), + Lib.NewList[Lib.List[subst.MixedSubstitution]](), st.GetProof(), node_id, original_node_id, st.GetGlobUnifier()}: if need_answer { ds.waitFather(father_id, st, c, Core.FusionSubstAndFormListWithoutDouble(subst_for_father, given_substs), node_id, original_node_id, []int{}, meta_to_reintroduce) diff --git a/src/Search/destructive.go b/src/Search/destructive.go index 1ef43a28..389b93a4 100644 --- a/src/Search/destructive.go +++ b/src/Search/destructive.go @@ -44,7 +44,9 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/dmt" - "github.com/GoelandProver/Goeland/Unif" + "github.com/GoelandProver/Goeland/Unif/codetree" + "github.com/GoelandProver/Goeland/Unif/discriminationtree" + substitution "github.com/GoelandProver/Goeland/Unif/substitution" ) const ( @@ -62,7 +64,7 @@ type BasicSearchAlgorithm interface { ProofSearch(uint64, State, Communication, Core.SubstAndForm, int, int, []int, bool) DoEndManageBeta(uint64, State, Communication, []Communication, int, int, []int, []int) manageRewriteRules(uint64, State, Communication, Core.FormAndTermsList, int, int, []int) - ManageClosureRule(uint64, *State, Communication, Lib.List[Lib.List[Unif.MixedSubstitution]], Core.FormAndTerms, int, int) (bool, []Core.SubstAndForm) + ManageClosureRule(uint64, *State, Communication, Lib.List[Lib.List[substitution.MixedSubstitution]], Core.FormAndTerms, int, int) (bool, []Core.SubstAndForm) manageResult(c Communication) (Core.Unifier, []ProofStruct, bool) } @@ -99,9 +101,16 @@ func (ds *destructiveSearch) doOneStep(limit int, formula AST.Form) (bool, int) AST.ResetMeta() // proof.ResetProofFile() ResetExchangesFile() + var tp, tn substitution.DataStructure - tp := Unif.NewNode() - tn := Unif.NewNode() + if Glob.GetDt() { + // TODO : replace by DT + tp = discriminationtree.NewNode() + tn = discriminationtree.NewNode() + } else { + tp = codetree.NewNode() + tn = codetree.NewNode() + } state := MakeState(limit, tp, tn, formula) state.SetCurrentProofNodeId(0) @@ -218,7 +227,7 @@ func (ds *destructiveSearch) searchContradictionAfterApplySusbt(father_id uint64 father_id, &st, cha, - subst.Copy(Lib.ListCpy[Unif.MixedSubstitution]), + subst.Copy(Lib.ListCpy[substitution.MixedSubstitution]), f.Copy(), node_id, original_node_id, @@ -245,7 +254,7 @@ func (ds *destructiveSearch) searchContradiction(atomic AST.Form, father_id uint father_id, &st, cha, - subst.Copy(Lib.ListCpy[Unif.MixedSubstitution]), + subst.Copy(Lib.ListCpy[substitution.MixedSubstitution]), fAt, node_id, original_node_id) return true } @@ -259,7 +268,7 @@ func (ds *destructiveSearch) searchContradiction(atomic AST.Form, father_id uint * st : State, the current search State * c : channel to send the answer to the father * s : substitution to apply to the current State -* subst_found : Unif.Substitutions found by this process +* subst_found : subst.Substitutions found by this process **/ func (ds *destructiveSearch) ProofSearch(father_id uint64, st State, cha Communication, s Core.SubstAndForm, node_id int, original_node_id int, meta_to_reintroduce []int, post_dmt_step bool) { debug( @@ -312,7 +321,7 @@ func (ds *destructiveSearch) ProofSearch(father_id uint64, st State, cha Communi Lib.MkLazy(func() string { return fmt.Sprintf( "Current substitutions list: %v", - Unif.SubstsToString(Core.GetSubstListFromSubstAndFormList(st.GetSubstsFound())), + substitution.SubstsToString(Core.GetSubstListFromSubstAndFormList(st.GetSubstsFound())), ) }), ) @@ -331,7 +340,7 @@ func (ds *destructiveSearch) ProofSearch(father_id uint64, st State, cha Communi father_id, &st, cha, - Lib.NewList[Lib.List[Unif.MixedSubstitution]](), + Lib.NewList[Lib.List[substitution.MixedSubstitution]](), f, node_id, original_node_id) return } @@ -522,7 +531,7 @@ func (ds *destructiveSearch) waitFather(father_id uint64, st State, c Communicat ) // Check if the subst was already seen, returns eventually the subst with new formula(s) - if Core.GetSubstListFromSubstAndFormList(given_substs).Contains(answer_father.subst_for_children.GetSubst(), Lib.ListEquals[Unif.MixedSubstitution]) { + if Core.GetSubstListFromSubstAndFormList(given_substs).Contains(answer_father.subst_for_children.GetSubst(), Lib.ListEquals[substitution.MixedSubstitution]) { debug( Lib.MkLazy(func() string { return "This substitution was sent by this child" }), ) @@ -556,7 +565,7 @@ func (ds *destructiveSearch) waitFather(father_id uint64, st State, c Communicat Lib.MkLazy(func() string { return fmt.Sprintf( "Forbidden received : %s", - Unif.SubstsToString(answer_father.getForbiddenSubsts()), + substitution.SubstsToString(answer_father.getForbiddenSubsts()), ) }), ) @@ -565,7 +574,7 @@ func (ds *destructiveSearch) waitFather(father_id uint64, st State, c Communicat Lib.MkLazy(func() string { return fmt.Sprintf( "New forbidden for this state: %s", - Unif.SubstsToString(st.GetForbiddenSubsts()), + substitution.SubstsToString(st.GetForbiddenSubsts()), ) }), ) @@ -627,7 +636,7 @@ func (ds *destructiveSearch) waitFather(father_id uint64, st State, c Communicat ) debug( Lib.MkLazy(func() string { - return fmt.Sprintf("Forbidden : %s", Unif.SubstsToString(st_copy.GetForbiddenSubsts())) + return fmt.Sprintf("Forbidden : %s", substitution.SubstsToString(st_copy.GetForbiddenSubsts())) }), ) go ds.ProofSearch(Glob.GetGID(), st_copy, c2, answer_father.getSubstForChildren(), node_id, original_node_id, new_meta_to_reintroduce, false) @@ -814,7 +823,7 @@ func (ds *destructiveSearch) selectChildren(father Communication, children *[]Co Lib.MkLazy(func() string { return fmt.Sprintf( "Result_subst :%s", - Unif.SubstsToString( + substitution.SubstsToString( Core.GetSubstListFromSubstAndFormList(result_subst), ), ) @@ -843,7 +852,7 @@ func (ds *destructiveSearch) selectChildren(father Communication, children *[]Co Lib.MkLazy(func() string { return fmt.Sprintf( "New result susbt : %s", - Unif.SubstsToString( + substitution.SubstsToString( Core.GetSubstListFromSubstAndFormList(result_subst), ), ) @@ -903,10 +912,14 @@ func (ds *destructiveSearch) selectChildren(father Communication, children *[]Co new_result_subst := []Core.SubstAndForm{} for _, s := range result_subst { if !Lib.ListEquals(s.GetSubst(), new_current_subst.GetSubst()) { - err, new_subst := Core.MergeSubstAndForm(s.Copy(), new_current_subst.Copy()) - - if err != nil { - Glob.Anomaly("SLC", "Error when merging substitutions.") + succeeded, new_subst := Core.TryMergeSubstAndForm(s.Copy(), new_current_subst.Copy()) + + if !succeeded { + // Expected outcome (conflicting sibling substitutions), not an anomaly. + debug(Lib.MkLazy(func() string { + return fmt.Sprintf("Substitutions %v and %v incompatible: discarded", s.ToString(), new_current_subst.ToString()) + })) + continue } new_result_subst = append(new_result_subst, new_subst) @@ -918,7 +931,7 @@ func (ds *destructiveSearch) selectChildren(father Communication, children *[]Co Lib.MkLazy(func() string { return fmt.Sprintf( "New subst at the end : %s", - Unif.SubstsToString(Core.GetSubstListFromSubstAndFormList(result_subst)), + substitution.SubstsToString(Core.GetSubstListFromSubstAndFormList(result_subst)), ) }), ) @@ -1012,7 +1025,7 @@ func (ds *destructiveSearch) tryRewrite(rewritten []Core.IntSubstAndForm, f Core newRewritten = Core.CopyIntSubstAndFormAndTermsList(newRewritten[1:]) // If we didn't rewrite as itself ? - if Unif.UnifSucceeded(choosenRewritten.GetSaf().GetSubst()) { + if substitution.UnifSucceeded(choosenRewritten.GetSaf().GetSubst()) { // Create a child with the current rewriting rule and make this process to wait for him, // with a list of other subst to try @@ -1062,7 +1075,7 @@ func (ds *destructiveSearch) ManageClosureRule( father_id uint64, st *State, c Communication, - substs Lib.List[Lib.List[Unif.MixedSubstitution]], + given_substs Lib.List[Lib.List[substitution.MixedSubstitution]], f Core.FormAndTerms, node_id int, original_node_id int, @@ -1072,13 +1085,13 @@ func (ds *destructiveSearch) ManageClosureRule( subst := st.GetAppliedSubst().GetSubst() mm = mm.Union(Core.GetMetaFromSubst(subst)) substs_with_mm, substs_with_mm_uncleared, substs_without_mm := - Core.DispatchSubst(substs.Copy(Lib.ListCpy[Unif.MixedSubstitution]), mm) + Core.DispatchSubst(given_substs.Copy(Lib.ListCpy[substitution.MixedSubstitution]), mm) unifier := st.GetGlobUnifier() appliedSubst := st.GetAppliedSubst().GetSubst() switch { - case substs.Empty(): + case given_substs.Empty(): debug( Lib.MkLazy(func() string { return "Branch closed by ¬⊤ or ⊥ or a litteral and its opposite!" }), ) @@ -1110,13 +1123,13 @@ func (ds *destructiveSearch) ManageClosureRule( Lib.MkLazy(func() string { return fmt.Sprintf( "Contradiction found (without mm) : %v", - Unif.SubstsToString(substs_without_mm)) + substitution.SubstsToString(substs_without_mm)) }), ) if Glob.GetAssisted() && !substs_without_mm.At(0).Empty() { fmt.Printf("The branch can be closed by using a substitution which has no impact elsewhere!\nApplying it automatically : ") - fmt.Printf("%v !\n", Unif.SubstsToString(substs_without_mm)) + fmt.Printf("%v !\n", substitution.SubstsToString(substs_without_mm)) } st.SetSubstsFound([]Core.SubstAndForm{st.GetAppliedSubst()}) @@ -1134,7 +1147,7 @@ func (ds *destructiveSearch) ManageClosureRule( // As no MM is involved, these substitutions can be unified with all the others having an empty subst. for _, subst := range substs_without_mm.GetSlice() { - merge, _ := Unif.MergeMixedSubstitutions(appliedSubst, subst) + merge, _ := substitution.MergeMixedSubstitutions(appliedSubst, subst) unifier.AddSubstitutions(appliedSubst, merge) } st.SetGlobUnifier(unifier) @@ -1157,7 +1170,7 @@ func (ds *destructiveSearch) ManageClosureRule( meta_to_reintroduce := []int{} for _, subst_for_father := range substs_with_mm.GetSlice() { - if !Unif.UnifSucceeded(subst_for_father) { + if !substitution.UnifSucceeded(subst_for_father) { Glob.Anomaly("MCR", fmt.Sprintf( "Error : SubstForFather is failure between : %s and %s \n", Lib.ListToString(subst_for_father, Lib.WithEmpty("(empty substs)")), @@ -1180,10 +1193,21 @@ func (ds *destructiveSearch) ManageClosureRule( ) // Merge with applied subst (if any) - err, subst_and_form_for_father := Core.MergeSubstAndForm(subst_and_form_for_father.Copy(), st.GetAppliedSubst()) + succeeded, subst_and_form_for_father := Core.TryMergeSubstAndForm(subst_and_form_for_father.Copy(), st.GetAppliedSubst()) - if err != nil { - Glob.Anomaly("MCR", "Contradiction found between applied subst and child subst.") + if !succeeded { + // This candidate conflicts with what is already applied at this node + // (e.g. two sibling branches instantiating a shared meta-variable + // differently) - an expected search outcome, not an anomaly, so we + // discard this candidate and keep checking the others. + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Candidate %v incompatible with applied subst %v: discarded", + subst_and_form_for_father.ToString(), + st.GetAppliedSubst().ToString()) + }), + ) } else { st.SetSubstsFound(Core.AppendIfNotContainsSubstAndForm(st.GetSubstsFound(), subst_and_form_for_father)) @@ -1206,7 +1230,7 @@ func (ds *destructiveSearch) ManageClosureRule( Lib.MkLazy(func() string { return fmt.Sprintf( "Send subst(s) with mm to father : %s", - Unif.SubstsToString( + substitution.SubstsToString( Core.GetSubstListFromSubstAndFormList(st.GetSubstsFound()), ), ) @@ -1216,8 +1240,8 @@ func (ds *destructiveSearch) ManageClosureRule( // Add substs_with_mm found with the corresponding subst for i, subst := range substs_with_mm.GetSlice() { - mergeUncleared, _ := Unif.MergeMixedSubstitutions(appliedSubst, substs_with_mm_uncleared.At(i)) - mergeCleared, _ := Unif.MergeMixedSubstitutions(appliedSubst, subst) + mergeUncleared, _ := substitution.MergeMixedSubstitutions(appliedSubst, substs_with_mm_uncleared.At(i)) + mergeCleared, _ := substitution.MergeMixedSubstitutions(appliedSubst, subst) unifier.AddSubstitutions(mergeCleared, mergeUncleared) } st.SetGlobUnifier(unifier) diff --git a/src/Search/exchanges.go b/src/Search/exchanges.go index 3b069cce..6ea32a02 100644 --- a/src/Search/exchanges.go +++ b/src/Search/exchanges.go @@ -44,7 +44,7 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + "github.com/GoelandProver/Goeland/Unif/substitution" ) var graph_file_name_exchanges = Glob.GetExecPath() + "../../visualization/json/exchanges_output.json" @@ -86,8 +86,8 @@ func ResetExchangesFile() { func makeJsonExchanges( father_uint uint64, st State, - ss_subst Lib.List[Lib.List[Unif.MixedSubstitution]], - subst_received Lib.List[Unif.MixedSubstitution], + ss_subst Lib.List[Lib.List[subst.MixedSubstitution]], + subst_received Lib.List[subst.MixedSubstitution], calling_function string, ) exchanges_struct { // ID @@ -124,7 +124,7 @@ func makeJsonExchanges( ss := "" if !ss_subst.Empty() { - ss += Unif.SubstsToString(ss_subst) + ss += subst.SubstsToString(ss_subst) } // fmt.Printf("Id = %v, version = %v, father = %v, forms = %v, mm = %v, mc = %v, ss = %v, sr = %v\n", id, version, father, forms, mm, mc, ss, sr) diff --git a/src/Search/incremental/rulesManager.go b/src/Search/incremental/rulesManager.go index 38c0bd53..061868f1 100644 --- a/src/Search/incremental/rulesManager.go +++ b/src/Search/incremental/rulesManager.go @@ -5,7 +5,8 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" + "github.com/GoelandProver/Goeland/Unif/codetree" ) type RulesManager struct { @@ -187,7 +188,7 @@ func (rm *RulesManager) tryComplementaryClosureRules() Rule { func (rm *RulesManager) trySubstitutionClosureRules() (applied Rule, subs SubList) { positiveRules, negativeRules := rm.getAtomicsWithoutTopOrBottom() - negTree := new(Unif.Node).MakeDataStruct(negativeRules.GetFormList(), false) + negTree := new(codetree.Node).MakeDataStruct(negativeRules.GetFormList(), false) substitutions := []Unif.MixedSubstitutions{} diff --git a/src/Search/incremental/search.go b/src/Search/incremental/search.go index b606e099..b9001b8f 100644 --- a/src/Search/incremental/search.go +++ b/src/Search/incremental/search.go @@ -6,7 +6,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Search" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) type incrementalSearch struct{} diff --git a/src/Search/incremental/substitution.go b/src/Search/incremental/substitution.go index e7985ba8..5f4d7bb4 100644 --- a/src/Search/incremental/substitution.go +++ b/src/Search/incremental/substitution.go @@ -3,7 +3,7 @@ package incremental import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + Unif "github.com/GoelandProver/Goeland/Unif/substitution" ) var anyTerm AST.Term = nil diff --git a/src/Search/nonDestructiveSearch.go b/src/Search/nonDestructiveSearch.go index bfe2edd3..324ab24b 100644 --- a/src/Search/nonDestructiveSearch.go +++ b/src/Search/nonDestructiveSearch.go @@ -41,7 +41,7 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + substitution "github.com/GoelandProver/Goeland/Unif/substitution" ) type nonDestructiveSearch struct { @@ -54,11 +54,11 @@ func NewNonDestructiveSearch() BasicSearchAlgorithm { return nil } -func getMetas(substs Lib.List[Unif.MixedSubstitution]) Lib.List[AST.Meta] { +func getMetas(substs Lib.List[substitution.MixedSubstitution]) Lib.List[AST.Meta] { metas := Lib.NewList[AST.Meta]() for _, subst := range substs.GetSlice() { switch s := subst.Substitution().(type) { - case Lib.Some[Unif.Substitution]: + case Lib.Some[substitution.Substitution]: metas.Append(s.Val.Key()) } } @@ -132,11 +132,11 @@ func (nds *nonDestructiveSearch) chooseSubstitutionNonDestructive(substs_found_t } /* Take a substitution, returns the id of the formula which introduce the metavariable */ -func (nds *nonDestructiveSearch) catchFormulaToInstantiate(subst_found Lib.List[Unif.MixedSubstitution]) int { +func (nds *nonDestructiveSearch) catchFormulaToInstantiate(subst_found Lib.List[substitution.MixedSubstitution]) int { meta_to_reintroduce := -1 for _, subst := range subst_found.GetSlice() { switch s := subst.Substitution().(type) { - case Lib.Some[Unif.Substitution]: + case Lib.Some[substitution.Substitution]: meta, term := s.Val.Get() if meta.GetFormula() < meta_to_reintroduce || meta_to_reintroduce == -1 { meta_to_reintroduce = meta.GetFormula() @@ -191,7 +191,7 @@ func (nds *nonDestructiveSearch) instantiate(fatherId uint64, state *State, c Co // If ths meta has an affectation in subst, give it // Else, give the previous meta - association_subst := Unif.Substitutions{} + association_subst := substitution.Substitutions{} // Associate new meta with old meta for _, new_meta := range newMetas.Elements().GetSlice() { @@ -212,7 +212,7 @@ func (nds *nonDestructiveSearch) instantiate(fatherId uint64, state *State, c Co if !found { for _, subst := range state.GetAppliedSubst().GetSubst().GetSlice() { switch s := subst.Substitution().(type) { - case Lib.Some[Unif.Substitution]: + case Lib.Some[substitution.Substitution]: original_meta, original_term := s.Val.Get() if !found && original_meta.GetName() == new_meta.GetName() && !found { association_subst.Set(new_meta, original_term) @@ -233,24 +233,24 @@ func (nds *nonDestructiveSearch) instantiate(fatherId uint64, state *State, c Co } } - mixed_assoc_subst := Lib.NewList[Unif.MixedSubstitution]() + mixed_assoc_subst := Lib.NewList[substitution.MixedSubstitution]() for _, subst := range association_subst { - mixed_assoc_subst.Append(Unif.MkMixedFromSubst(subst)) + mixed_assoc_subst.Append(substitution.MkMixedFromSubst(subst)) } - new_subst, same_key := Unif.MergeMixedSubstitutions(mixed_assoc_subst, state.GetAppliedSubst().GetSubst()) + new_subst, same_key := substitution.MergeMixedSubstitutions(mixed_assoc_subst, state.GetAppliedSubst().GetSubst()) if same_key { Glob.PrintInfo("PS", "Same key in S2 and S1") } - if !Unif.UnifSucceeded(new_subst) { + if !substitution.UnifSucceeded(new_subst) { Glob.Anomaly("PS", "MergeSubstitutions return failure") } - new_subst, same_key = Unif.MergeMixedSubstitutions(new_subst, s.GetSubst()) + new_subst, same_key = substitution.MergeMixedSubstitutions(new_subst, s.GetSubst()) if same_key { Glob.PrintInfo("PS", "Same key in S2 and S1") } - if !Unif.UnifSucceeded(new_subst) { + if !substitution.UnifSucceeded(new_subst) { Glob.Anomaly("PS", "MergeSubstitutions return failure") } @@ -271,12 +271,12 @@ func (nds *nonDestructiveSearch) instantiate(fatherId uint64, state *State, c Co state.SetLF(Core.ApplySubstitutionsOnFormAndTermsList(new_subst, state.GetLF())) - ms, same_key := Unif.MergeMixedSubstitutions(state.GetAppliedSubst().GetSubst(), new_subst) + ms, same_key := substitution.MergeMixedSubstitutions(state.GetAppliedSubst().GetSubst(), new_subst) if same_key { Glob.Anomaly("PS", "Same key in S2 and S1") } - if !Unif.UnifSucceeded(ms) { + if !substitution.UnifSucceeded(ms) { Glob.Anomaly("PS", "MergeSubstitutions return failure") } state.SetAppliedSubst(Core.MakeSubstAndForm(ms, s.GetForm())) diff --git a/src/Search/proof.go b/src/Search/proof.go index e7bcecad..7ec557ad 100644 --- a/src/Search/proof.go +++ b/src/Search/proof.go @@ -47,7 +47,7 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + substitution "github.com/GoelandProver/Goeland/Unif/substitution" ) var path_proof = Glob.GetExecPath() + "proof_output.json" @@ -404,7 +404,7 @@ func RetrieveUninstantiatedMetaFromProof(proofStruct []ProofStruct) Lib.Set[AST. } /* Apply subst on a proof tree */ -func ApplySubstitutionOnProofList(s Lib.List[Unif.MixedSubstitution], proof_list []ProofStruct) []ProofStruct { +func ApplySubstitutionOnProofList(s Lib.List[substitution.MixedSubstitution], proof_list []ProofStruct) []ProofStruct { new_proof_list := []ProofStruct{} for _, p := range proof_list { diff --git a/src/Search/rules.go b/src/Search/rules.go index b9b490b3..1cc35aa3 100644 --- a/src/Search/rules.go +++ b/src/Search/rules.go @@ -42,7 +42,7 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + substitution "github.com/GoelandProver/Goeland/Unif/substitution" ) var strToPrintMap map[string]string = map[string]string{ @@ -59,9 +59,9 @@ var strToPrintMap map[string]string = map[string]string{ "EXISTS": "∃", } -func ApplyClosureRules(form AST.Form, state *State) (bool, Lib.List[Lib.List[Unif.MixedSubstitution]]) { +func ApplyClosureRules(form AST.Form, state *State) (bool, Lib.List[Lib.List[substitution.MixedSubstitution]]) { result := false - substitutions := Lib.NewList[Lib.List[Unif.MixedSubstitution]]() + substitutions := Lib.NewList[Lib.List[substitution.MixedSubstitution]]() debug(Lib.MkLazy(func() string { return "Start ACR" })) if searchObviousClosureRule(form) { @@ -73,9 +73,9 @@ func ApplyClosureRules(form AST.Form, state *State) (bool, Lib.List[Lib.List[Uni substFound, substs := searchInequalities(form) if substFound { result = true - mixed_substs := Lib.NewList[Unif.MixedSubstitution]() + mixed_substs := Lib.NewList[substitution.MixedSubstitution]() for _, subst := range substs { - mixed_substs.Append(Unif.MkMixedFromSubst(subst)) + mixed_substs.Append(substitution.MkMixedFromSubst(subst)) } substitutions.Append(mixed_substs) } @@ -106,7 +106,7 @@ func ApplyClosureRules(form AST.Form, state *State) (bool, Lib.List[Lib.List[Uni subst.ToString()) }), ) - substitutions.Add(Lib.ListEquals[Unif.MixedSubstitution], subst.GetSubsts()) + substitutions.Add(Lib.ListEquals[substitution.MixedSubstitution], subst.GetSubsts()) } } } @@ -114,14 +114,14 @@ func ApplyClosureRules(form AST.Form, state *State) (bool, Lib.List[Lib.List[Uni return result, substitutions } -func searchForbidden(state *State, s Unif.MatchingSubstitutions) bool { +func searchForbidden(state *State, s substitution.MatchingSubstitutions) bool { foundForbidden := false for _, substForbidden := range state.GetForbiddenSubsts().GetSlice() { - substs := Unif.Substitutions{} + substs := substitution.Substitutions{} for _, subst := range substForbidden.GetSlice() { switch s := subst.Substitution().(type) { - case Lib.Some[Unif.Substitution]: + case Lib.Some[substitution.Substitution]: substs = append(substs, s.Val) } } @@ -155,8 +155,8 @@ func searchObviousClosureRule(f AST.Form) bool { } /* Search contradiction with inequalities (for example, !(x,a) -> subst(x, a)) */ -func searchInequalities(form AST.Form) (bool, Unif.Substitutions) { - subst := Unif.MakeEmptySubstitution() +func searchInequalities(form AST.Form) (bool, substitution.Substitutions) { + subst := substitution.MakeEmptySubstitution() if formNot, isNot := form.(AST.Not); isNot { if predNeq, isPred := formNot.GetForm().(AST.Pred); isPred { @@ -181,12 +181,12 @@ func searchInequalities(form AST.Form) (bool, Unif.Substitutions) { Lib.MkLazy(func() string { return fmt.Sprintf("Arg 2 : %v", arg_2.ToString()) }), ) - subst = Unif.AddUnification(arg_1, arg_2, subst) + subst = substitution.AddUnification(arg_1, arg_2, subst) debug( Lib.MkLazy(func() string { return fmt.Sprintf("Subst : %v", subst.ToString()) }), ) - if !subst.Equals(Unif.Failure()) { + if !subst.Equals(substitution.Failure()) { return true, subst } } @@ -197,14 +197,54 @@ func searchInequalities(form AST.Form) (bool, Unif.Substitutions) { } /* Search a contradiction between a formula and another in the datastructure */ -func searchClosureRule(f AST.Form, st State) (bool, []Unif.MixedSubstitutions) { +func searchClosureRule(f AST.Form, st State) (bool, []substitution.MixedSubstitutions) { switch nf := f.(type) { case AST.Pred: - return st.GetTreeNeg().Unify(f) + res, subst := st.GetTreeNeg().Unify(f) + if res { + returnList := Lib.NewList[substitution.MixedSubstitutions]() + + running_subst := st.applied_subst.GetSubst() + + for _, e := range subst { + subst2, isCompatible := substitution.MergeMixedSubstitutions(e.GetSubsts(), running_subst) + + if isCompatible { + running_subst = subst2 + + new_subst := substitution.MakeMixedSubstitutions(e.GetForm(), subst2) + returnList.Append(new_subst) + } + } + + return !returnList.Empty(), returnList.GetSlice() + } + return false, nil + case AST.Not: switch nf.GetForm().(type) { case AST.Pred: - return st.GetTreePos().Unify(nf.GetForm()) + res, subst := st.GetTreePos().Unify(nf.GetForm()) + if res { + returnList := Lib.NewList[substitution.MixedSubstitutions]() + + running_subst := st.applied_subst.GetSubst() + + for _, e := range subst { + subst2, isCompatible := substitution.MergeMixedSubstitutions(e.GetSubsts(), running_subst) + + if isCompatible { + running_subst = subst2 + + new_subst := substitution.MakeMixedSubstitutions(e.GetForm(), subst2) + returnList.Append(new_subst) + } + } + + return !returnList.Empty(), returnList.GetSlice() + } + return false, nil + default: return false, nil } diff --git a/src/Search/search.go b/src/Search/search.go index c55ab779..9e33f30f 100644 --- a/src/Search/search.go +++ b/src/Search/search.go @@ -43,13 +43,13 @@ import ( "github.com/GoelandProver/Goeland/Core" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" - "github.com/GoelandProver/Goeland/Unif" + "github.com/GoelandProver/Goeland/Unif/substitution" ) type SearchAlgorithm interface { Search(AST.Form, int) bool SetApplyRules(func(uint64, State, Communication, Core.FormAndTermsList, int, int, []int)) - ManageClosureRule(uint64, *State, Communication, Lib.List[Lib.List[Unif.MixedSubstitution]], Core.FormAndTerms, int, int) (bool, []Core.SubstAndForm) + ManageClosureRule(uint64, *State, Communication, Lib.List[Lib.List[subst.MixedSubstitution]], Core.FormAndTerms, int, int) (bool, []Core.SubstAndForm) } var UsedSearch SearchAlgorithm @@ -118,11 +118,11 @@ func printStandardSolution(status string) { fmt.Printf("%s SZS status %v for %v\n", "%", status, Glob.GetProblemName()) } -func retrieveMetaFromSubst(substs Lib.List[Unif.MixedSubstitution]) []int { +func retrieveMetaFromSubst(substs Lib.List[subst.MixedSubstitution]) []int { res := []int{} - for _, subst := range substs.GetSlice() { - switch s := subst.Substitution().(type) { - case Lib.Some[Unif.Substitution]: + for _, s := range substs.GetSlice() { + switch s := s.Substitution().(type) { + case Lib.Some[subst.Substitution]: res = Glob.AppendIfNotContainsInt(res, s.Val.Key().GetFormula()) } } diff --git a/src/Search/state.go b/src/Search/state.go index 8c3a6f85..b5207940 100644 --- a/src/Search/state.go +++ b/src/Search/state.go @@ -44,7 +44,7 @@ import ( "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" "github.com/GoelandProver/Goeland/Mods/equality/eqStruct" - "github.com/GoelandProver/Goeland/Unif" + subst "github.com/GoelandProver/Goeland/Unif/substitution" ) /****************/ @@ -60,11 +60,11 @@ type State struct { applied_subst Core.SubstAndForm last_applied_subst Core.SubstAndForm // For non destructive case only substs_found []Core.SubstAndForm // Subst found with mm in d, subst for "bactrack" in nd - tree_pos, tree_neg Unif.DataStructure + tree_pos, tree_neg subst.DataStructure proof []ProofStruct current_proof ProofStruct bt_on_formulas bool - forbidden Lib.List[Lib.List[Unif.MixedSubstitution]] + forbidden Lib.List[Lib.List[subst.MixedSubstitution]] unifier Core.Unifier eqStruct eqStruct.EqualityStruct } @@ -113,13 +113,13 @@ func (s State) GetLastAppliedSubst() Core.SubstAndForm { func (st State) GetSubstsFound() []Core.SubstAndForm { return Core.CopySubstAndFormList(st.substs_found) } -func (s State) GetTreePos() Unif.DataStructure { +func (s State) GetTreePos() subst.DataStructure { return s.tree_pos } func (s *State) AddToTreePos(fl Lib.List[AST.Form]) { s.tree_pos = s.tree_pos.InsertFormulaListToDataStructure(fl) } -func (s State) GetTreeNeg() Unif.DataStructure { +func (s State) GetTreeNeg() subst.DataStructure { return s.tree_neg } func (s *State) AddToTreeNeg(fl Lib.List[AST.Form]) { @@ -134,7 +134,7 @@ func (s State) GetCurrentProof() ProofStruct { func (s State) GetBTOnFormulas() bool { return s.bt_on_formulas } -func (s State) GetForbiddenSubsts() Lib.List[Lib.List[Unif.MixedSubstitution]] { +func (s State) GetForbiddenSubsts() Lib.List[Lib.List[subst.MixedSubstitution]] { return s.forbidden } func (s State) GetGlobUnifier() Core.Unifier { @@ -186,10 +186,10 @@ func (st *State) SetLastAppliedSubst(s Core.SubstAndForm) { func (st *State) SetSubstsFound(s []Core.SubstAndForm) { st.substs_found = Core.CopySubstAndFormList(s) } -func (st *State) SetTreePos(d Unif.DataStructure) { +func (st *State) SetTreePos(d subst.DataStructure) { st.tree_pos = d } -func (st *State) SetTreeNeg(d Unif.DataStructure) { +func (st *State) SetTreeNeg(d subst.DataStructure) { st.tree_neg = d } func (st *State) SetProof(p []ProofStruct) { @@ -245,15 +245,15 @@ func (st *State) SetCurrentProofNodeId(i int) { func (st *State) SetBTOnFormulas(b bool) { st.bt_on_formulas = b } -func (st *State) SetForbiddenSubsts(s Lib.List[Lib.List[Unif.MixedSubstitution]]) { - st.forbidden = s.Copy(Lib.ListCpy[Unif.MixedSubstitution]) +func (st *State) SetForbiddenSubsts(s Lib.List[Lib.List[subst.MixedSubstitution]]) { + st.forbidden = s.Copy(Lib.ListCpy[subst.MixedSubstitution]) } func (s *State) SetGlobUnifier(u Core.Unifier) { s.unifier = u.Copy() } /* Maker */ -func MakeState(limit int, tp, tn Unif.DataStructure, f AST.Form) State { +func MakeState(limit int, tp, tn subst.DataStructure, f AST.Form) State { n := 0 if Glob.IsDestructive() { n = limit @@ -285,7 +285,7 @@ func MakeState(limit int, tp, tn Unif.DataStructure, f AST.Form) State { []ProofStruct{}, current_proof, false, - Lib.NewList[Lib.List[Unif.MixedSubstitution]](), + Lib.NewList[Lib.List[subst.MixedSubstitution]](), Core.MakeUnifier(), eqStruct.NewEqStruct()} } @@ -353,7 +353,7 @@ func (st State) Print() { debug(Lib.MkLazy(func() string { return "Subst_found: " })) debug( Lib.MkLazy(func() string { - return Unif.SubstsToString(Core.GetSubstListFromSubstAndFormList(st.GetSubstsFound())) + return subst.SubstsToString(Core.GetSubstListFromSubstAndFormList(st.GetSubstsFound())) }), ) } @@ -368,7 +368,7 @@ func (st State) Print() { debug( Lib.MkLazy(func() string { return st.forbidden.ToString( - func(m Lib.List[Unif.MixedSubstitution]) string { + func(m Lib.List[subst.MixedSubstitution]) string { return Lib.ListToString(m) }, Lib.WithSep(" ; ")) }), @@ -428,10 +428,10 @@ func (st State) Copy() State { // Recréer arbre if Glob.IsLoaded("dmt") { new_state.SetTreePos(st.tree_pos.MakeDataStruct(st.GetAtomic().ExtractForms(), true)) - new_state.SetTreeNeg(st.tree_pos.MakeDataStruct(st.GetAtomic().ExtractForms(), false)) + new_state.SetTreeNeg(st.tree_neg.MakeDataStruct(st.GetAtomic().ExtractForms(), false)) } else { - new_state.SetTreePos(st.GetTreePos()) - new_state.SetTreeNeg(st.GetTreeNeg()) + new_state.SetTreePos(st.GetTreePos().MakeDataStruct(st.GetAtomic().ExtractForms(), true)) + new_state.SetTreeNeg(st.GetTreeNeg().MakeDataStruct(st.GetAtomic().ExtractForms(), false)) } new_state.SetProof([]ProofStruct{}) diff --git a/src/Unif/code-trees.go b/src/Unif/codetree/code-trees.go similarity index 78% rename from src/Unif/code-trees.go rename to src/Unif/codetree/code-trees.go index 6beb3371..ba68694d 100644 --- a/src/Unif/code-trees.go +++ b/src/Unif/codetree/code-trees.go @@ -34,13 +34,14 @@ * This file contains all the definitons necessary to make a Code Tree **/ -package Unif +package codetree import ( "strings" "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Lib" + subst "github.com/GoelandProver/Goeland/Unif/substitution" ) /*************************/ @@ -58,11 +59,11 @@ func (c CodeBlock) Copy() CodeBlock { type Node struct { value CodeBlock children []*Node - formulas Lib.List[AST.Form] + leafFor Lib.List[Lib.Either[AST.Term, AST.Form]] } func NewNode() *Node { - return &Node{CodeBlock{}, []*Node{}, Lib.NewList[AST.Form]()} + return &Node{CodeBlock{}, []*Node{}, Lib.NewList[Lib.Either[AST.Term, AST.Form]]()} } func (n Node) getValue() CodeBlock { @@ -71,38 +72,48 @@ func (n Node) getValue() CodeBlock { func (n Node) getChildren() []*Node { return CopyNodeList(n.children) } -func (n Node) getFormulas() Lib.List[AST.Form] { - return Lib.ListCpy(n.formulas) -} /* Check if a node is empty */ func (n Node) IsEmpty() bool { return (len(n.value) == 0) } -/* Make data struct */ -func (n Node) MakeDataStruct(fl Lib.List[AST.Form], is_pos bool) DataStructure { +func MakeUnifProblem(l Lib.List[AST.Form], is_pos bool) subst.DataStructure { + return NewNode().MakeDataStruct(l, is_pos) +} + +func MakeTermUnifProblem(l Lib.List[AST.Term]) subst.DataStructure { + root := makeNode(nil) + + for _, t := range l.GetSlice() { + root.insert(ParseTerm(subst.TransformTerm(t))) + } + + return root +} + +func (n Node) MakeDataStruct(fl Lib.List[AST.Form], is_pos bool) subst.DataStructure { return makeCodeTreeFromAtomic(fl, is_pos) } /* Copy a datastruct */ -func (n Node) Copy() DataStructure { - return Node{n.getValue(), n.getChildren(), n.getFormulas()} +func (n Node) Copy() subst.DataStructure { + return Node{n.getValue(), n.getChildren(), n.leafFor.Copy(Lib.EitherCpy[AST.Term, AST.Form])} } /********************/ /* Helper functions */ /********************/ -/* The Node is a leaf when it contains at least one formulae. */ +/* The Node is a leaf whenever one formula or term ends here. */ func (n Node) isLeaf() bool { - return n.getFormulas().Len() > 0 + return n.leafFor.Len() > 0 } -/* Make two code trees (tree_pos and tree_neg) from st.atomic */ func makeCodeTreeFromAtomic(lf Lib.List[AST.Form], is_pos bool) *Node { form := Lib.NewList[AST.Form]() + // fixme: why are we doing this here? for _, f := range lf.GetSlice() { switch nf := f.(type) { case AST.Pred: @@ -116,9 +127,6 @@ func makeCodeTreeFromAtomic(lf Lib.List[AST.Form], is_pos bool) *Node { form.Append(nf.GetForm()) } } - case TermForm: - // EQUALITY - To build a tree of terms - form.Append(nf.Copy()) } } @@ -152,12 +160,12 @@ func makeNode(block CodeBlock) *Node { n := new(Node) n.value = block.Copy() n.children = []*Node{} - n.formulas = Lib.NewList[AST.Form]() + n.leafFor = Lib.NewList[Lib.Either[AST.Term, AST.Form]]() return n } /* Insert a lsit of formula into the right tree */ -func (n Node) InsertFormulaListToDataStructure(lf Lib.List[AST.Form]) DataStructure { +func (n Node) InsertFormulaListToDataStructure(lf Lib.List[AST.Form]) subst.DataStructure { for _, f := range lf.GetSlice() { switch nf := f.Copy().(type) { case AST.Pred: @@ -198,8 +206,17 @@ func (n Node) printAux(tab int) { } if n.isLeaf() { - for _, form := range n.formulas.GetSlice() { - debug(Lib.MkLazy(func() string { return strings.Repeat("\t", tab+1) + form.ToString() })) + for _, tof := range n.leafFor.GetSlice() { + debug( + Lib.MkLazy( + func() string { + return strings.Repeat( + "\t", + tab+1, + ) + tofToString(tof) + }, + ), + ) } } debug(Lib.MkLazy(func() string { return "\n" })) @@ -214,17 +231,17 @@ func (n Node) printAux(tab int) { func (n *Node) insert(sequence Sequence) { if len(n.value) == 0 { n.value = sequence.GetInstructions() - n.formulas = Lib.MkListV(sequence.GetFormula()) + n.leafFor = Lib.MkListV(sequence.GetBase()) } else { - n.followInstructions(sequence.GetInstructions(), sequence.GetFormula()) + n.followInstructions(sequence.GetInstructions(), sequence.GetBase()) } } /* Auxiliary function to follow the sequence of instructions to insert in the Node. */ -func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { +func (n *Node) followInstructions(instructions []Instruction, tof Lib.Either[AST.Term, AST.Form]) { // Initialization of the node we will be working on and of a counter. current := n - oui := 0 + cnt := 0 // For each instruction, there are 2 cases: // * The current instruction is equivalent to the instruction stored in the CodeBlock of the current node at the index of the counter. @@ -234,11 +251,12 @@ func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { // If it's equivalent, there are 2 cases: // * It's the end of the sequence & the end of the CodeBlock. In this case, it's a full match, just add the formulae to the leaf. // * It's the end of the CodeBlock, but not of the sequence. In this case, check if the following instruction matches with any child. - if instr.IsEquivalent(current.value[oui]) { - oui += 1 - if i == len(instructions)-1 && oui == len(current.value) && !Lib.ListMem(form, current.formulas) { - current.formulas.Append(form) - } else if i < len(instructions)-1 && oui == len(current.value) { + if instr.IsEquivalent(current.value[cnt]) { + cnt += 1 + if i == len(instructions)-1 && cnt == len(current.value) && + !current.leafFor.Contains(tof, tofCmp) { + current.leafFor.Append(tof) + } else if i < len(instructions)-1 && cnt == len(current.value) { // If the instruction matches, then continue the algorithm with the child as the current node. // If it doesn't, we have a new leaf with the following instructions of the sequence. @@ -246,13 +264,13 @@ func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { for _, child := range current.children { if instructions[i+1].IsEquivalent(child.value[0]) { current = child - oui = 0 + cnt = 0 found = true } } if !found { newNode := makeNode(instructions[i+1:]) - newNode.formulas = Lib.MkListV(form) + newNode.leafFor = Lib.MkListV(tof) current.children = append(current.children, newNode) break } @@ -261,15 +279,15 @@ func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { // Split the current CodeBlock in 2 parts: // * The first one will contain the remaining instructions of the current CodeBlock, and it will inherit the current's children and formulaes. // * The second one contains the remaining instructions of the sequence plus the formulae. - child1 := makeNode(current.value[oui:]) + child1 := makeNode(current.value[cnt:]) child2 := makeNode(instructions[i:]) - child2.formulas = Lib.MkListV(form) + child2.leafFor = Lib.MkListV(tof) child1.children = current.children - child1.formulas = current.formulas + child1.leafFor = current.leafFor - current.value = current.value[:oui] - current.formulas = Lib.NewList[AST.Form]() + current.value = current.value[:cnt] + current.leafFor = Lib.NewList[Lib.Either[AST.Term, AST.Form]]() current.children = []*Node{child1, child2} break @@ -279,12 +297,12 @@ func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { // It's the end of the sequence, but there are still instructions in the CodeBlock. // In this case, we have to split the CodeBlock in 2 parts. The first one will be a leaf containing the current sequence's formulae. // The second will be the rest of the CodeBlock's instructions, with the current's children and formulaes. - if oui < len(current.value)-1 { - child1 := makeNode(current.value[oui:]) + if cnt < len(current.value)-1 { + child1 := makeNode(current.value[cnt:]) child1.children = current.children - current.value = current.value[:oui] + current.value = current.value[:cnt] current.children = []*Node{child1} - current.formulas = Lib.MkListV(form.Copy()) + current.leafFor = Lib.MkListV(tofCopy(tof)) } } diff --git a/src/Unif/instruction.go b/src/Unif/codetree/instruction.go similarity index 99% rename from src/Unif/instruction.go rename to src/Unif/codetree/instruction.go index f8b7e7c0..2607294c 100644 --- a/src/Unif/instruction.go +++ b/src/Unif/codetree/instruction.go @@ -34,7 +34,7 @@ * This file provides the necessary structures to represents instructions for the machine. **/ -package Unif +package codetree import ( "reflect" diff --git a/src/Unif/int_pair.go b/src/Unif/codetree/int_pair.go similarity index 99% rename from src/Unif/int_pair.go rename to src/Unif/codetree/int_pair.go index f26a8307..61a621d4 100644 --- a/src/Unif/int_pair.go +++ b/src/Unif/codetree/int_pair.go @@ -34,7 +34,7 @@ * This file provides the necessary structures to manipulate pairs of int. **/ -package Unif +package codetree import ( "strconv" diff --git a/src/Unif/machine.go b/src/Unif/codetree/machine.go similarity index 76% rename from src/Unif/machine.go rename to src/Unif/codetree/machine.go index 6fa2c0ec..1c393a27 100644 --- a/src/Unif/machine.go +++ b/src/Unif/codetree/machine.go @@ -34,11 +34,13 @@ * This file provides the necessary structures to operate the unification algorithm. **/ -package Unif +package codetree import ( + "fmt" "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Unif/substitution" ) /* Describes the success or failure of the execution of a machine instruction. */ @@ -62,10 +64,10 @@ type Machine struct { hasPushed bool hasPoped bool post []IntPair - subst []SubstPair + subst []subst.SubstPair terms Lib.List[AST.Term] - meta Substitutions - failure []MatchingSubstitutions + meta subst.Substitutions + failure []subst.MixMatchSubstitutions topLevelTot int topLevelCount int } @@ -79,10 +81,10 @@ func makeMachine() Machine { hasPushed: false, hasPoped: false, post: []IntPair{}, - subst: []SubstPair{}, + subst: []subst.SubstPair{}, terms: Lib.NewList[AST.Term](), - meta: Substitutions{}, - failure: []MatchingSubstitutions{}, + meta: subst.Substitutions{}, + failure: []subst.MixMatchSubstitutions{}, topLevelTot: 0, topLevelCount: 0, } @@ -216,7 +218,7 @@ func (m *Machine) matchIndexes(t AST.Term, instrTerm AST.Term) Status { /* Checks if the substitution of the metavariable t matches the index of instrTerm. */ func (m *Machine) checkMeta(t AST.Meta, instrTerm AST.Term) Status { - if HasSubst(m.meta, t) { + if subst.HasSubst(m.meta, t) { metaGotten, _ := m.meta.Get(t) unwrapped := m.unwrapMeta(metaGotten) if !unwrapped.IsMeta() && !m.doIndexMatch(unwrapped, instrTerm) { @@ -226,3 +228,66 @@ func (m *Machine) checkMeta(t AST.Meta, instrTerm AST.Term) Status { return Status(SUCCESS) } + +/* Call addUnification and returns a status - modify m.meta */ +func (m *Machine) trySubstituteMeta(i AST.Term, j AST.Term) Status { + debug( + Lib.MkLazy( + func() string { return fmt.Sprintf("Try substitute : %v and %v", i.ToString(), j.ToString()) }, + ), + ) + new_meta := subst.AddUnification(i, j, m.meta.Copy()) + if new_meta.Equals(subst.Failure()) { + return Status(ERROR) + } + m.meta = new_meta + return Status(SUCCESS) +} + +/* Adds the unifications found to the meta substitutions from running the algorithm on term1 and term2. */ +func (m *Machine) addUnifications(term1, term2 AST.Term) Status { + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "add unification : %v and %v", + term1.ToString(), + term2.ToString()) + }), + ) + meta := tryUnification( + term1.Copy(), + term2.Copy(), + m.meta.Copy(), + ) // Return empty or an array of 1 matching substitution, which is m.meta improved wit (term1, term2) + + if len(meta) == 0 { + return Status(ERROR) + } else { + m.meta = meta[0].Subst + subst.EliminateMeta(&m.meta) + subst.Eliminate(&m.meta) + } + + return Status(SUCCESS) +} + + +/* Tries to unify term1 with term2, depending on the substitutions already found by the parent unification process. */ +func tryUnification(term1, term2 AST.Term, meta subst.Substitutions) []subst.MixMatchSubstitutions { + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Try unification : %v and %v", + term1.ToString(), + term2.ToString()) + }), + ) + aux := makeMachine() + aux.terms = Lib.MkListV(term2) + aux.meta = meta + + // add begin at the start and end at the end ! + tree := makeBranch(ParseTerm(term1.Copy())) + res := aux.unifyAux(*tree) + return res +} \ No newline at end of file diff --git a/src/Unif/matching.go b/src/Unif/codetree/matching.go similarity index 71% rename from src/Unif/matching.go rename to src/Unif/codetree/matching.go index 2091101a..6e19ab74 100644 --- a/src/Unif/matching.go +++ b/src/Unif/codetree/matching.go @@ -34,7 +34,7 @@ * This file provides the necessary methods for the unification algorithm. **/ -package Unif +package codetree import ( "fmt" @@ -43,6 +43,7 @@ import ( "github.com/GoelandProver/Goeland/AST" "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Unif/substitution" ) var debug Glob.Debugger @@ -54,60 +55,69 @@ func InitDebugger() { /*** Unify ***/ /* Helper function to avoid using MakeMachine() outside of this file. */ -func (n Node) Unify(formula AST.Form) (bool, []MixedSubstitutions) { +func (n Node) Unify(formula AST.Form) (bool, []subst.MixedSubstitutions) { machine := makeMachine() - res := machine.unify(n, formula) + var term AST.Term + + if formula_type, is_pred := formula.(AST.Pred); is_pred { + term = subst.TransformPred(formula_type) + } else { + Glob.Anomaly("unification", fmt.Sprintf("Expected predicate, got %s", formula.ToString())) + } + + res, matching_substs := machine.unify(n, term) + // As we have transformed type metas to terms, we get everything in a term substitution. // But externally, we want to have a substitution of both (term) metas to terms and (type) metas to types. // We use MixedSubstitution to properly manage things internally. - mixed_substs := []MixedSubstitutions{} - for _, subst := range res { - mixed_substs = append(mixed_substs, subst.toMixed()) + mixed_substs := []subst.MixedSubstitutions{} + for _, subst := range matching_substs { + mixed_substs = append(mixed_substs, subst.ToMixed()) } - return !reflect.DeepEqual(machine.failure, res), mixed_substs + + return res, mixed_substs } -/* Tries to find the substitutions needed to unify the formulae with the one described by the sequence of instructions. */ -func (m *Machine) unify(node Node, formula AST.Form) []MatchingSubstitutions { - var result []MatchingSubstitutions - // The formula has to be a predicate. - switch formula_type := formula.(type) { - case AST.Pred: - // Transform the predicate to a function to make the tool work properly - m.terms = Lib.MkListV[AST.Term](AST.MakerFun( - formula_type.GetID(), - Lib.NewList[AST.Ty](), - getFunctionalArguments(formula_type.GetTyArgs(), formula_type.GetArgs()), - )) - result = m.unifyAux(node) - - if !reflect.DeepEqual(m.failure, result) { - filteredResult := []MatchingSubstitutions{} - for _, matchingSubst := range result { - filteredResult = append(filteredResult, - MakeMatchingSubstitutions(matchingSubst.GetForm(), matchingSubst.GetSubst())) - } - result = filteredResult - } - case TermForm: - m.terms = Lib.MkListV(formula_type.GetTerm()) - result = m.unifyAux(node) - default: - result = m.failure +func (n Node) UnifyTerm(t AST.Term) (bool, []subst.MixedTermSubstitutions) { + m := makeMachine() + + res, matching_substs := m.unify( + n, + subst.TransformTerm(t), + ) + + mixed_substs := []subst.MixedTermSubstitutions{} + for _, subst := range matching_substs { + mixed_substs = append(mixed_substs, subst.ToMixedTerm()) } - return result + return res, mixed_substs +} + +/* Tries to find the substitutions needed to unify the formulae with the one described by the sequence of instructions. */ +func (m *Machine) unify(node Node, t AST.Term) (bool, []subst.MixMatchSubstitutions) { + m.terms = Lib.MkListV(t) + res := m.unifyAux(node) + return !reflect.DeepEqual(m.failure, res), res } /*** Unify aux ***/ -func (m *Machine) unifyAux(node Node) []MatchingSubstitutions { +func (m *Machine) unifyAux(node Node) []subst.MixMatchSubstitutions { for _, instr := range node.value { debug(Lib.MkLazy(func() string { return "------------------------" })) debug(Lib.MkLazy(func() string { return fmt.Sprintf("Instr: %v", instr.ToString()) })) debug(Lib.MkLazy(func() string { return fmt.Sprintf("Meta : %v", m.meta.ToString()) })) - debug(Lib.MkLazy(func() string { return fmt.Sprintf("Subst : %v", SubstPairListToString(m.subst)) })) - debug(Lib.MkLazy(func() string { return fmt.Sprintf("Post : %v", IntPairistToString(m.post)) })) + debug( + Lib.MkLazy( + func() string { return fmt.Sprintf("Subst : %v", subst.SubstPairListToString(m.subst)) }, + ), + ) + debug( + Lib.MkLazy( + func() string { return fmt.Sprintf("Post : %v", IntPairistToString(m.post)) }, + ), + ) debug(Lib.MkLazy(func() string { return fmt.Sprintf("IsLocked : %v", m.isLocked()) })) debug(Lib.MkLazy(func() string { return fmt.Sprintf("HasPushed : %v", m.hasPushed) })) debug(Lib.MkLazy(func() string { return fmt.Sprintf("HasPoped : %v", m.hasPoped) })) @@ -131,7 +141,9 @@ func (m *Machine) unifyAux(node Node) []MatchingSubstitutions { Lib.MkLazy(func() string { return fmt.Sprintf("Cursor: %v/%v", m.q, m.terms.Len()) }), ) debug( - Lib.MkLazy(func() string { return fmt.Sprintf("m.terms[cursor] : %v", m.terms.At(m.q).ToString()) }), + Lib.MkLazy( + func() string { return fmt.Sprintf("m.terms[cursor] : %v", m.terms.At(m.q).ToString()) }, + ), ) debug( Lib.MkLazy(func() string { @@ -173,26 +185,29 @@ func (m *Machine) unifyAux(node Node) []MatchingSubstitutions { } } - matching := []MatchingSubstitutions{} + matching := []subst.MixMatchSubstitutions{} if node.isLeaf() { - for _, f := range node.formulas.GetSlice() { - if reflect.TypeOf(f) == reflect.TypeOf(AST.Pred{}) || reflect.TypeOf(f) == reflect.TypeOf(TermForm{}) { - // Rebuild final substitution between meta and subst - final_subst := computeSubstitutions(CopySubstPairList(m.subst), m.meta.Copy(), f.Copy()) - if !final_subst.Equals(Failure()) { - matching = append(matching, MakeMatchingSubstitutions(f, final_subst)) - } + for _, f := range node.leafFor.GetSlice() { + // Rebuild final substitution between meta and subst + final_subst := computeSubstitutions( + subst.CopySubstPairList(m.subst), + m.meta.Copy(), + tofMetaList(f), + ) + if !final_subst.Equals(subst.Failure()) { + matching = append(matching, subst.MixMatchSubstitutions{Tof: f, Subst: final_subst}) } } } + matching = append(matching, m.launchChildrenSearch(node)...) return matching } /* Unify on goroutines - to manage die message */ /* TODO : remove when debug ok */ -func (m *Machine) unifyAuxOnGoroutine(n Node, ch chan []MatchingSubstitutions, father_id uint64) { +func (m *Machine) unifyAuxOnGoroutine(n Node, ch chan []subst.MixMatchSubstitutions, father_id uint64) { debug( Lib.MkLazy(func() string { return fmt.Sprintf("Child of %v, Unify Aux", father_id) }), ) @@ -202,23 +217,37 @@ func (m *Machine) unifyAuxOnGoroutine(n Node, ch chan []MatchingSubstitutions, f } /* Launches each child of the current node in a goroutine. */ -func (m *Machine) launchChildrenSearch(node Node) []MatchingSubstitutions { - channels := []chan []MatchingSubstitutions{} +func (m *Machine) launchChildrenSearch(node Node) []subst.MixMatchSubstitutions { + channels := []chan []subst.MixMatchSubstitutions{} for _, c := range node.children { debug( - Lib.MkLazy(func() string { return fmt.Sprintf("Next symbol = %v", c.getValue()[0].ToString()) }), + Lib.MkLazy( + func() string { return fmt.Sprintf("Next symbol = %v", c.getValue()[0].ToString()) }, + ), ) - channels = append(channels, make(chan []MatchingSubstitutions)) + channels = append(channels, make(chan []subst.MixMatchSubstitutions)) } - matching := []MatchingSubstitutions{} + matching := []subst.MixMatchSubstitutions{} for i, n := range node.children { ch := channels[i] st := m.terms.Copy(AST.Term.Copy) ip := CopyIntPairList(m.post) - sc := CopySubstPairList(m.subst) - - copy := Machine{subst: sc, beginLock: m.beginLock, terms: st, meta: m.meta.Copy(), q: m.q, beginCount: m.beginCount, hasPushed: m.hasPushed, hasPoped: m.hasPoped, post: ip, topLevelTot: m.topLevelTot, topLevelCount: m.topLevelCount} + sc := subst.CopySubstPairList(m.subst) + + copy := Machine{ + subst: sc, + beginLock: m.beginLock, + terms: st, + meta: m.meta.Copy(), + q: m.q, + beginCount: m.beginCount, + hasPushed: m.hasPushed, + hasPoped: m.hasPoped, + post: ip, + topLevelTot: m.topLevelTot, + topLevelCount: m.topLevelCount, + } go copy.unifyAuxOnGoroutine(*n, ch, Glob.GetGID()) Glob.IncrGoRoutine(1) @@ -232,7 +261,7 @@ func (m *Machine) launchChildrenSearch(node Node) []MatchingSubstitutions { for cpt_remaining_children > 0 { _, value, _ := reflect.Select(cases) - matching = append(matching, value.Interface().([]MatchingSubstitutions)...) + matching = append(matching, value.Interface().([]subst.MixMatchSubstitutions)...) cpt_remaining_children-- } @@ -320,7 +349,7 @@ func (m *Machine) put(instr Put) { if m.isUnlocked() { m.subst = append( m.subst, - MakeSubstPair(instr.GetIndex(), m.terms.At(m.q)), + subst.MakeSubstPair(instr.GetIndex(), m.terms.At(m.q)), ) } } @@ -328,8 +357,8 @@ func (m *Machine) put(instr Put) { /* Algorithm for the instruction Compare. */ func (m *Machine) compare(i int, j int) Status { if m.isUnlocked() { - i := GetSubstAt(m.subst, i) - j := GetSubstAt(m.subst, j) + i := subst.GetSubstAt(m.subst, i) + j := subst.GetSubstAt(m.subst, j) if i != nil && j != nil { i = m.unwrapMeta(i) diff --git a/src/Unif/parsing.go b/src/Unif/codetree/parsing.go similarity index 50% rename from src/Unif/parsing.go rename to src/Unif/codetree/parsing.go index c8a80fc6..4acd548d 100644 --- a/src/Unif/parsing.go +++ b/src/Unif/codetree/parsing.go @@ -30,84 +30,16 @@ * knowledge of the CeCILL license and that you accept its terms. **/ -package Unif +package codetree import ( "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Unif/substitution" ) -type TermForm struct { - index int - t AST.Term -} - -func (t TermForm) ToString() string { return t.ToString() } -func (t TermForm) GetTerm() AST.Term { return t.t.Copy() } -func (t TermForm) Copy() AST.Form { return makeTermForm(t.GetIndex(), t.GetTerm()) } -func (t TermForm) RenameVariables() AST.Form { return t } -func (t TermForm) ReplaceTermByTerm(AST.Term, AST.Term) (AST.Form, bool) { - return t, false -} -func (t TermForm) SubstTy(AST.TyGenVar, AST.Ty) AST.Form { - return t -} -func (t TermForm) GetIndex() int { return t.index } -func (t TermForm) SubstituteVarByMeta(AST.Var, AST.Meta) AST.Form { return t } -func (t TermForm) GetInternalMetas() Lib.List[AST.Meta] { return Lib.NewList[AST.Meta]() } -func (t TermForm) SetInternalMetas(Lib.List[AST.Meta]) AST.Form { return t } -func (t TermForm) GetSubFormulasRecur() Lib.List[AST.Form] { return Lib.NewList[AST.Form]() } -func (t TermForm) GetChildFormulas() Lib.List[AST.Form] { return Lib.NewList[AST.Form]() } -func (t TermForm) Equals(t2 any) bool { - switch nt := t2.(type) { - case TermForm: - return t.GetTerm().Equals(nt.GetTerm()) - default: - return false - } -} - -func (t TermForm) GetMetas() Lib.Set[AST.Meta] { - switch nt := t.GetTerm().(type) { - case AST.Meta: - return Lib.Singleton(nt) - case AST.Fun: - res := Lib.EmptySet[AST.Meta]() - - for _, m := range nt.GetArgs().GetSlice() { - switch mt := m.(type) { - case AST.Meta: - res = res.Add(mt) - } - } - - return res - default: - return Lib.EmptySet[AST.Meta]() - } -} - -func (t TermForm) GetSubTerms() Lib.List[AST.Term] { - return t.GetTerm().GetSubTerms() -} - -func (t TermForm) ReplaceMetaByTerm(meta AST.Meta, term AST.Term) AST.Form { - return t -} - -func MakerTermForm(t AST.Term) TermForm { - switch trm := t.(type) { - case AST.Fun: - args := getFunctionalArguments(trm.GetTyArgs(), trm.GetArgs()) - t = AST.MakerFun(trm.GetID(), Lib.NewList[AST.Ty](), args) - } - return makeTermForm(AST.MakerIndexFormula(), t.Copy()) -} - -func makeTermForm(i int, t AST.Term) TermForm { - return TermForm{i, t.Copy()} -} /* Parses a formulae to a sequence of instructions. */ func ParseFormula(formula AST.Form) Sequence { @@ -115,26 +47,17 @@ func ParseFormula(formula AST.Form) Sequence { // The formula has to be a predicate switch formula_type := formula.(type) { case AST.Pred: - instructions := Sequence{formula: formula_type} + instructions := Sequence{base: Lib.MkRight[AST.Term, AST.Form](formula)} - instructions.add(Begin{}) - parsePred(formula_type, &instructions) - instructions.add(End{}) + switch term := subst.TransformPred(formula_type).(type) { + case AST.Fun: + instructions.add(Begin{}) + parsePred(formula_type.GetID(), term.GetArgs(), &instructions) + instructions.add(End{}) - return instructions - case TermForm: - instructions := Sequence{formula: formula} - varCount := 0 - postCount := 0 - instructions.add(Begin{}) - parseTerms( - Lib.MkListV(formula_type.GetTerm().Copy()), - &instructions, - Lib.NewList[AST.Meta](), - &varCount, - &postCount, - ) - instructions.add(End{}) + default: + Glob.Anomaly("unification", "error when translating in internal representation") + } return instructions @@ -143,35 +66,15 @@ func ParseFormula(formula AST.Form) Sequence { } } -/* Parses a predicate to machine instructions */ -func getFunctionalArguments(ty_args Lib.List[AST.Ty], trm_args Lib.List[AST.Term]) Lib.List[AST.Term] { - args := Lib.ListMap(ty_args, AST.TyToTerm) - - for _, arg := range trm_args.GetSlice() { - switch term := arg.(type) { - case AST.Meta: - args.Append(arg) - case AST.Fun: - args.Append(AST.MakerFun( - term.GetID(), - Lib.NewList[AST.Ty](), - getFunctionalArguments(term.GetTyArgs(), term.GetArgs()), - )) - } - } - - return args -} - -func parsePred(p AST.Pred, instructions *Sequence) { - instructions.add(makeCheck(p.GetID())) - if !p.GetTyArgs().Empty() || !p.GetArgs().Empty() { +func parsePred(i AST.Id, args Lib.List[AST.Term], instructions *Sequence) { + instructions.add(makeCheck(i)) + if !args.Empty() { instructions.add(Begin{}) instructions.add(Down{}) varCount := 0 postCount := 0 parseTerms( - getFunctionalArguments(p.GetTyArgs(), p.GetArgs()), + args, instructions, Lib.NewList[AST.Meta](), &varCount, @@ -216,7 +119,7 @@ func parseTerms( instructions.add(Right{}) } case AST.Fun: - instructions.add(Begin{}) // TEST 33 + instructions.add(Begin{}) instructions.add(makeCheck(t.GetID())) if downDefined(t.GetArgs()) { @@ -225,18 +128,20 @@ func parseTerms( *postCount++ } instructions.add(Down{}) - subTerms := getFunctionalArguments(t.GetTyArgs(), t.GetArgs()) - subst = parseTerms(subTerms, instructions, subst, varCount, postCount) + if !t.GetTyArgs().Empty() { + Glob.Anomaly("unif parsing", "found type arguments at an unexpected place") + } + subst = parseTerms(t.GetArgs(), instructions, subst, varCount, postCount) if rightDefined(terms, i) { *postCount-- instructions.add(Pop{*postCount}) } instructions.add(makeEnd(t)) } else if rightDefined(terms, i) { - instructions.add(makeEnd(t)) // TEST33 + instructions.add(makeEnd(t)) instructions.add(Right{}) } else { - instructions.add(makeEnd(t)) // TEST33 + instructions.add(makeEnd(t)) } } } @@ -254,6 +159,6 @@ func ParseTerm(term AST.Term) Sequence { &varCount, &postCount, ) - instructions.formula = MakerTermForm(term) + instructions.base = Lib.MkLeft[AST.Term, AST.Form](term) return instructions } diff --git a/src/Unif/sequence.go b/src/Unif/codetree/sequence.go similarity index 62% rename from src/Unif/sequence.go rename to src/Unif/codetree/sequence.go index 76a3717a..922de31e 100644 --- a/src/Unif/sequence.go +++ b/src/Unif/codetree/sequence.go @@ -34,19 +34,49 @@ * This file provides the necessary structures to represents a sequences for the machine. **/ -package Unif +package codetree import ( "fmt" "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" + "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Unif/substitution" ) /*** Sequence ***/ +func tofToString(tof Lib.Either[AST.Term, AST.Form]) string { + return Lib.EitherToString[AST.Term, AST.Form](tof, "Trm", "Form") +} + +func tofCopy(tof Lib.Either[AST.Term, AST.Form]) Lib.Either[AST.Term, AST.Form] { + return Lib.EitherCpy[AST.Term, AST.Form](tof) +} + +func tofCmp(tof1, tof2 Lib.Either[AST.Term, AST.Form]) bool { + return Lib.EitherEquals[AST.Term, AST.Form](tof1, tof2) +} + +func tofMetaList(tof Lib.Either[AST.Term, AST.Form]) Lib.List[AST.Meta] { + switch tof := tof.(type) { + case Lib.Left[AST.Term, AST.Form]: + return subst.TransformTerm(tof.Val).GetMetaList() + case Lib.Right[AST.Term, AST.Form]: + switch f := tof.Val.(type) { + case AST.Pred: + return subst.TransformPred(f).GetMetaList() + } + } + + Glob.Anomaly("unification", "Unification has not been launched on terms or on a predicate") + return Lib.NewList[AST.Meta]() +} + type Sequence struct { instructions []Instruction - formula AST.Form + base Lib.Either[AST.Term, AST.Form] } /*** Sequence's methods ***/ @@ -55,22 +85,22 @@ func (s *Sequence) GetInstructions() []Instruction { return CopyInstructionList(s.instructions) } -func (s *Sequence) GetFormula() AST.Form { - return s.formula.Copy() +func (s *Sequence) GetBase() Lib.Either[AST.Term, AST.Form] { + return s.base } func (s *Sequence) add(instr Instruction) { s.instructions = append(s.instructions, instr) } -// ILL TODO: Should not print directly, should return a string that is then printed +// FIXME: Should not print directly, should return a string that is then printed func (s Sequence) Print() { for _, instr := range s.instructions { fmt.Printf("%v", instr) } - fmt.Printf(" - " + s.formula.ToString()) + fmt.Printf(" - " + tofToString(s.base)) } func (s Sequence) Copy() Sequence { - return Sequence{s.GetInstructions(), s.GetFormula()} + return Sequence{s.GetInstructions(), tofCopy(s.base)} } diff --git a/src/Unif/codetree/substitutions_tree.go b/src/Unif/codetree/substitutions_tree.go new file mode 100644 index 00000000..6a02408c --- /dev/null +++ b/src/Unif/codetree/substitutions_tree.go @@ -0,0 +1,200 @@ +/** +* Copyright 2022 by the authors (see AUTHORS). +* +* Goéland is an automated theorem prover for first order logic. +* +* This software is governed by the CeCILL license under French law and +* abiding by the rules of distribution of free software. You can use, +* modify and/ or redistribute the software under the terms of the CeCILL +* license as circulated by CEA, CNRS and INRIA at the following URL +* "http://www.cecill.info". +* +* As a counterpart to the access to the source code and rights to copy, +* modify and redistribute granted by the license, users are provided only +* with a limited warranty and the software's author, the holder of the +* economic rights, and the successive licensors have only limited +* liability. +* +* In this respect, the user's attention is drawn to the risks associated +* with loading, using, modifying and/or developing or reproducing the +* software by the user in light of its specific status of free software, +* that may mean that it is complicated to manipulate, and that also +* therefore means that it is reserved for developers and experienced +* professionals having in-depth computer knowledge. Users are therefore +* encouraged to load and test the software's suitability as regards their +* requirements in conditions enabling the security of their systems and/or +* data to be ensured and, more generally, to use and operate it in the +* same conditions as regards security. +* +* The fact that you are presently reading this means that you have had +* knowledge of the CeCILL license and that you accept its terms. +**/ + +/** +* This file contains the functions needed to subtitute all the meta-variables of a subtitution map. +**/ + +package codetree + +import ( + "fmt" + + "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Unif/substitution" +) + +/* Takes each meta of the formula, matches the index to the metas, and add everything to subst */ +/* +* Subs : (int, term) : (index in tree, term in formula) +* MetaToSubs : (meta, term) : meta in formula, term in tree +* Merge both of them +**/ +func computeSubstitutions( + subs []subst.SubstPair, + metasToSubs subst.Substitutions, + metaList Lib.List[AST.Meta], +) subst.Substitutions { + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Compute substitution : %v and %v", + subst.SubstPairListToString(subs), metasToSubs.ToString()) + }), + ) + treeSubs := subst.Substitutions{} + + // Transform subst tree into a real substitution + for _, value := range subs { + if value.GetIndex() < metaList.Len() { + currentMeta := metaList.At(value.GetIndex()) + currentValue := value.GetTerm() + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Iterate on subst : %v and %v", + currentMeta.ToString(), + currentValue.ToString()) + }), + ) + + if !currentMeta.Equals(currentValue) { + // Si current_meta a déjà une association dans metas + metaGet, index := metasToSubs.Get(currentMeta) + if subst.HasSubst(metasToSubs, currentMeta) && (index != -1) && + !currentValue.Equals(metaGet) { + // On cherche a unifier les deux valeurs + treeSubs.Set(currentMeta, currentValue) + new_unif := subst.AddUnification(currentValue.Copy(), metaGet.Copy(), treeSubs.Copy()) + if new_unif.Equals(subst.Failure()) { + return subst.Failure() + } else { + treeSubs = new_unif + metasToSubs.Remove(index) // Remove from meta + } + } else { // Ne pas ajouter la susbtitution égalité + treeSubs.Set(currentMeta, currentValue) + } + } + } + } + + debug( + Lib.MkLazy( + func() string { return fmt.Sprintf("before meta : %v", metasToSubs.ToString()) }, + ), + ) + // Metas_subst eliminate + subst.EliminateMeta(&metasToSubs) + subst.Eliminate(&metasToSubs) + if metasToSubs.Equals(subst.Failure()) { + return subst.Failure() + } + debug( + Lib.MkLazy(func() string { return fmt.Sprintf("After meta : %v", metasToSubs.ToString()) }), + ) + + debug( + Lib.MkLazy( + func() string { return fmt.Sprintf("before tree_subst : %v", treeSubs.ToString()) }, + ), + ) + // Tree subst elminate + subst.EliminateMeta(&treeSubs) + subst.Eliminate(&treeSubs) + if treeSubs.Equals(subst.Failure()) { + return subst.Failure() + } + debug( + Lib.MkLazy( + func() string { return fmt.Sprintf("after tree_subst : %v", treeSubs.ToString()) }, + ), + ) + + // Fusion + res, _ := subst.MergeSubstitutions(metasToSubs, treeSubs) + if res.Equals(subst.Failure()) { + return res + } + + debug( + Lib.MkLazy(func() string { return fmt.Sprintf("after merge : %v", res.ToString()) }), + ) + + subst.EliminateMeta(&res) + subst.Eliminate(&res) + + debug( + Lib.MkLazy(func() string { return fmt.Sprintf("after eliminate : %v", res.ToString()) }), + ) + + return res +} + +func addUnification(term1, term2 AST.Term, s subst.Substitutions) subst.Substitutions { + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Add unification : %v and %v to %v", + term1.ToString(), + term2.ToString(), + s.ToString()) + }), + ) + term1 = subst.TransformTerm(term1) + term2 = subst.TransformTerm(term2) + + // unify with ct only if the term already has an unification or if there is 2 fun. Just add it and eliminate otherwise. + t1v, _ := s.Get(term1.ToMeta()) + t2v, _ := s.Get(term2.ToMeta()) + if (term1.IsMeta() && subst.HasSubst(s, term1.ToMeta()) && !t1v.Equals(term2)) || + (term2.IsMeta() && subst.HasSubst(s, term2.ToMeta()) && !t2v.Equals(term1)) || + (term1.IsFun() && term2.IsFun()) { + m := makeMachine() + m.meta = s.Copy() + if m.addUnifications(term1, term2) == SUCCESS { + return m.meta + } else { + return subst.Failure() + } + } else { + switch { + case term1.IsMeta(): + s.Set(term1.ToMeta(), term2) + subst.EliminateMeta(&s) + subst.Eliminate(&s) + return s + case term2.IsMeta(): + s.Set(term2.ToMeta(), term1) + subst.EliminateMeta(&s) + subst.Eliminate(&s) + return s + default: + return subst.Failure() + } + } +} + + + + diff --git a/src/Unif/data_structure.go b/src/Unif/discriminationtree/ContextNormalizer.go similarity index 50% rename from src/Unif/data_structure.go rename to src/Unif/discriminationtree/ContextNormalizer.go index c3d9f2a7..457b0d92 100644 --- a/src/Unif/data_structure.go +++ b/src/Unif/discriminationtree/ContextNormalizer.go @@ -31,22 +31,61 @@ **/ /** -* This file contains functions and types which describe the formula's data - structure +* This file contains all the definitons necessary to make a Code Tree **/ -package Unif +package discriminationtree import ( + "fmt" + "github.com/GoelandProver/Goeland/AST" - "github.com/GoelandProver/Goeland/Lib" ) -type DataStructure interface { - Print() - IsEmpty() bool - MakeDataStruct(Lib.List[AST.Form], bool) DataStructure - InsertFormulaListToDataStructure(Lib.List[AST.Form]) DataStructure - Unify(AST.Form) (bool, []MixedSubstitutions) - Copy() DataStructure +// Implement the perfect tree link between a Meta and newMeta +type NormalizerContext struct { + counter int // Counter for the naming + mapping map[string]AST.Meta // Association a variable name to a normalizedVariable name + ty AST.Ty +} + +// New Instance +func NewContext() *NormalizerContext { + return &NormalizerContext{ + counter: 0, + mapping: make(map[string]AST.Meta), + ty: nil, + } +} + +// Transform the discriminationTree to a perfect disriminationTree. +// Using a Map, when visiting a branch, each Meta is stored and transform into a NormalizedMeta. This allow memory gain. +// Branch 1 : f(x), Branch 2 : f(y) => Branch 1 : f(v1), Branch 2 : f(v1) => We notice it's the same one => Possible to fuse them to save memory +func (ctx *NormalizerContext) GetNormalizedMeta(originalMeta AST.Meta) AST.Meta { + + originalName := originalMeta.GetName() // Get meta Name + orignalType := originalMeta.GetTy() // Get Meta Ty + + // Contains check + if normalizedMeta, exists := ctx.mapping[originalName]; exists { + if normalizedMeta.GetTy().Equals(orignalType) { + return normalizedMeta + } + } + + // Create new name + ctx.counter++ + newName := fmt.Sprintf("v%d", ctx.counter) // Create the Meta name + newMeta := AST.MakeMeta(ctx.counter, 0, newName, 0, originalMeta.GetTy()) + ctx.mapping[originalName] = newMeta // Add to the map + ctx.ty = newMeta.GetTy() + + return newMeta +} + +func (ctx *NormalizerContext) Reset() { + + ctx.counter = 0 + ctx.mapping = make(map[string]AST.Meta) + } diff --git a/src/Unif/discriminationtree/discrimination-trees.go b/src/Unif/discriminationtree/discrimination-trees.go new file mode 100644 index 00000000..3ce223ad --- /dev/null +++ b/src/Unif/discriminationtree/discrimination-trees.go @@ -0,0 +1,1478 @@ +/** +* Copyright 2022 by the authors (see AUTHORS). +* +* Goéland is an automated theorem prover for first order logic. +* +* This software is governed by the CeCILL license under French law and +* abiding by the rules of distribution of free software. You can use, +* modify and/ or redistribute the software under the terms of the CeCILL +* license as circulated by CEA, CNRS and INRIA at the following URL +* "http://www.cecill.info". +* +* As a counterpart to the access to the source code and rights to copy, +* modify and redistribute granted by the license, users are provided only +* with a limited warranty and the software's author, the holder of the +* economic rights, and the successive licensors have only limited +* liability. +* +* In this respect, the user's attention is drawn to the risks associated +* with loading, using, modifying and/or developing or reproducing the +* software by the user in light of its specific status of free software, +* that may mean that it is complicated to manipulate, and that also +* therefore means that it is reserved for developers and experienced +* professionals having in-depth computer knowledge. Users are therefore +* encouraged to load and test the software's suitability as regards their +* requirements in conditions enabling the security of their systems and/or +* data to be ensured and, more generally, to use and operate it in the +* same conditions as regards security. +* +* The fact that you are presently reading this means that you have had +* knowledge of the CeCILL license and that you accept its terms. +**/ + +/** +* This file contains all the definitons necessary to make a Discrimination Tree +**/ + +package discriminationtree + +import ( + "fmt" + "strings" + "sync" + + "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" + "github.com/GoelandProver/Goeland/Lib" + subst "github.com/GoelandProver/Goeland/Unif/substitution" +) + +var debug Glob.Debugger + +func InitDebugger() { + debug = Glob.CreateDebugger("unif") +} + +/*************************/ +/* Structures definition */ +/*************************/ + +type NodeElement interface { + ToString() string + isAllowedNodeElement() + IsMeta() bool + GetArityType() int + GetTy() AST.Ty + Equals(target NodeElement) bool +} + +func (ns NodeString) ToString() string { + return string(ns) +} + +type NodeString string +type TermNode struct{ AST.Term } +type TyNode struct{ AST.Ty } + +func (ns NodeString) isAllowedNodeElement() {} +func (tn TermNode) isAllowedNodeElement() {} +func (tn TyNode) isAllowedNodeElement() {} + +func (ns NodeString) IsMeta() bool { + return false +} + +func (tn TermNode) IsMeta() bool { + return tn.Term.IsMeta() +} + +// Required to make transitivity.p valid +func (tn TyNode) IsMeta() bool { + if tn.Ty != nil { + _, isTypeVariable := tn.Ty.(AST.TyMeta) + return isTypeVariable + } + return false +} + +func (ns NodeString) GetArityType() int { + return 0 +} + +func (tn TermNode) GetArityType() int { + return tn.GetMetaList().Len() +} + +func (tn TyNode) GetArityType() int { + return 0 +} + +// If SymbolType is AST.Term, return It, else nil +func (sym SymbolType) getTerm() AST.Term { + + if tn, ok := sym.symbol.(TermNode); ok { + return tn.Term + } + return nil + +} + +// If SymbolType is AST.Ty, return It, else nil +func (sym SymbolType) GetTy() AST.Ty { + + if tn, ok := sym.symbol.(TyNode); ok { + return tn.Ty + } + return nil + +} + +// If SymbolType is string, return It, else nil +func (sym SymbolType) getString() string { + + if ns, ok := sym.symbol.(NodeString); ok { + return ns.ToString() + } + return "" +} + +// Equals made between NodeString and one NodeElement +func (ns NodeString) Equals(target NodeElement) bool { + + typ, ok := target.(NodeString) + if !ok { + return false + } + return strings.EqualFold(ns.ToString(), typ.ToString()) +} + +// Equals made between TermNode and one NodeElement +func (tn TermNode) Equals(target NodeElement) bool { + + typ, ok := target.(TermNode) + if !ok { + return false + } + + if tn.Term != nil && typ.Term != nil { + return tn.Term.Equals(typ.Term) + } + return false +} + +// Equals made between TyNode and one NodeElement +func (tn TyNode) Equals(target NodeElement) bool { + typ, ok := target.(TyNode) + if !ok { + return false + } + + if tn.Ty == nil || typ.Ty == nil { + return false + } + + return tn.Ty.Equals(typ.Ty) +} + +// Return The Type of a NodeString. +// Return Temporary a AST.Tindividual() +func (ns NodeString) GetTy() AST.Ty { + + return AST.TIndividual() // Temporary + +} + +// Convert The termNode to Meta then getTy() +func (tn TermNode) GetTy() AST.Ty { + + return tn.ToMeta().GetTy() + +} + +// Return the Ty of the TyNode +func (tn TyNode) GetTy() AST.Ty { + + return tn.Ty + +} + +// If the is AST.Fun return ID.ToString else term.toString else nil +func (tn TermNode) ToString() string { + if fun, ok := tn.Term.(AST.Fun); ok { + return fun.GetID().ToString() + } + + if tn.Term != nil { + return tn.Term.ToString() + } + + return "nil" +} + +// Take Any Parameter. Depending of the Parameter : +// String => NodeString +// AST.Ty => TyNode +// AST.Pred => TermNode(TransformPred(Param)) +// AST.Term => TermNode +// Else Anomaly +func createNodeElement(t any) NodeElement { + + switch v := t.(type) { + case string: + return NodeString(v) + case AST.Ty: + return TyNode{v} + case AST.Pred: + return TermNode{subst.TransformPred(v)} + case AST.Term: + return TermNode{v} + default: + Glob.Anomaly("Unknow Type from createNodeElement(t any) NodeElement ", "Unknow Type from createNodeElement(t any) NodeElement") + return nil + } +} + +type SymbolType struct { + symbol NodeElement // Term of the node + arity int // Arity of a node +} + +func (t SymbolType) ToString() string { + return fmt.Sprintf("Symbol : %s Arity : %d\n", t.symbol.ToString(), t.GetArity()) +} + +func (t SymbolType) getSymbol() NodeElement { + return t.symbol +} + +func (t SymbolType) GetArity() int { + return t.arity +} + +// Nil is Symbol is nil and arity == -1 ( default Arity for a SymbolType) +func (s SymbolType) IsNil() bool { + return s.symbol == nil && s.arity == -1 +} + +// Maker a SymbolType with a Arity of 0 +func makeSymbolTypeTy(node NodeElement) SymbolType { + return SymbolType{node, 0} +} + +// Maker SymbolType +func makeSymbolType(node NodeElement, arity int) SymbolType { + + return SymbolType{node, arity} +} + +// Equals between two SymbolType +func (s SymbolType) Equals(target SymbolType) bool { + + if s.GetArity() != target.GetArity() { + return false + } + + return s.symbol.Equals(target.symbol) +} + +/* Each node of a discrimination tree holds a single symbol (a function/predicate, + a type, or a meta, together with its arity) and its children. When it is a leaf, + leafFor / termLeafFor hold the predicates / terms whose flattened sequence ends + at this node. */ +type DiscriminationNode struct { + symbol SymbolType // Contain the AST.Term and Arity + children Lib.List[DiscriminationNode] // All the children of the node + leafFor Lib.List[AST.Pred] // If not empty, contains the where it come from + + // Parallel to leafFor, but for trees populated with raw terms (InsertTerm) + // instead of predicates (Insert) - used by UnifyTerm/UnifyTermWithSubst. + // Kept separate from leafFor rather than merged into a single Either-typed + // field, since nothing in this codebase mixes both kinds of insertion on + // the same tree instance: it keeps this addition purely additive, with + // zero risk to the existing predicate-based Insert/Unify/Unify2 code. + termLeafFor Lib.List[AST.Term] + + // Set once, on the tree returned by InsertTerm/MakeTermUnifProblem, so + // UnifyTermWithSubst knows which single traversal to run instead of + // always running both (which would double the cost of every call for + // no benefit, since a given tree is always exclusively one or the + // other in practice). + termOnly bool +} + +// Basic Node. Create a SymbolType{nil, -1} and empty list for children and leafFor +func NewNode() DiscriminationNode { + return DiscriminationNode{ + symbol: SymbolType{symbol: nil, arity: -1}, + children: Lib.NewList[DiscriminationNode](), + leafFor: Lib.NewList[AST.Pred](), + termLeafFor: Lib.NewList[AST.Term](), + } +} + +// Basic Node with SymbolType and no empty list for children and leafFor +func MakeDiscriminationNodeWithSym(sym SymbolType) DiscriminationNode { + return DiscriminationNode{ + symbol: sym, + children: Lib.NewList[DiscriminationNode](), + leafFor: Lib.NewList[AST.Pred](), + termLeafFor: Lib.NewList[AST.Term](), + } +} + +// Basic Node with SymbolType, children and empty List for leafFor +func MakeDiscriminationNodeWithSymAndChildren(sym SymbolType, children Lib.List[DiscriminationNode]) DiscriminationNode { + return DiscriminationNode{ + symbol: sym, + children: children, + leafFor: Lib.NewList[AST.Pred](), + termLeafFor: Lib.NewList[AST.Term](), + } +} + +func (dNode DiscriminationNode) getSymbol() SymbolType { + return dNode.symbol +} + +func (dNode DiscriminationNode) GetArity() int { + return dNode.symbol.GetArity() +} + +func (dNode DiscriminationNode) getChildren() Lib.List[DiscriminationNode] { + return dNode.children +} + +func (dNode DiscriminationNode) getLeafFor() Lib.List[AST.Pred] { + return dNode.leafFor +} + +func (dNode DiscriminationNode) getTermLeafFor() Lib.List[AST.Term] { + return dNode.termLeafFor +} + +// If NodeElement of the dNode is nil return "" else toString +func (dNode DiscriminationNode) toString() string { + sym := dNode.getSymbol().getSymbol() + + if sym == nil { + return "" + } + return sym.ToString() +} + +// Struct with a Pred and a associated substitution. Used for Robinson +type CandidatResult struct { + Pred AST.Pred // Predicat + Subs subst.Substitutions // The associated substitution +} + +func (Candidat CandidatResult) getPred() AST.Pred { + return Candidat.Pred +} + +func (Candidat CandidatResult) GetSubs() subst.Substitutions { + return Candidat.Subs +} + +// Return Pred and Subs +func (Candidat CandidatResult) toString() string { + return fmt.Sprintf("Pred : %s Subs : %s\n", Candidat.getPred().ToString(), Candidat.GetSubs().ToString()) +} + +// Works only if Len(CandidatResult) is 1. Had Enough to for-each all the time for single element +func ToSingleElement(candidats []CandidatResult) CandidatResult { + if len(candidats) == 1 { + return candidats[0] + } + return CandidatResult{} +} + +// Maker CandidatResult +func MakeCandidat(p AST.Pred, sub subst.Substitutions) CandidatResult { + return CandidatResult{ + Pred: p, + Subs: sub, + } +} + +// Mirrors CandidatResult, for trees populated via InsertTerm instead of Insert. +type TermCandidatResult struct { + Term AST.Term // The raw term stored at this leaf + Subs subst.Substitutions // The associated substitution +} + +func (Candidat TermCandidatResult) getTerm() AST.Term { + return Candidat.Term +} + +func (Candidat TermCandidatResult) GetSubs() subst.Substitutions { + return Candidat.Subs +} + +func MakeTermCandidat(t AST.Term, sub subst.Substitutions) TermCandidatResult { + return TermCandidatResult{ + Term: t, + Subs: sub, + } +} + +/*****************************/ +/* End Structures definition */ +/*****************************/ + +/*****************************/ +/*********** Parse ***********/ +/*****************************/ + +// Predicat Parser. Skip the Predicat Type and Transform it into a Function. +// Then Call parseTerm on the args of the predicat. +func parsePred(p AST.Pred, ctx *NormalizerContext) Lib.List[SymbolType] { + + // if p.GetTyArgs().Len() != p.GetArgs().Len() && (p.GetTyArgs().Len() > 1) { + // Glob.Anomaly("Ambigious number of types", " Ambigious number of types, don't match the number of args or not one unique types, leading to a ambigious typing for args") + // } + + res := Lib.NewList[SymbolType]() + // Required Overwise the SymbolType of the predicat will be AST.ID and will be compared with a AST.Fun -> Automatic faillure + tmpFun := AST.MakerFun(p.GetID(), Lib.MkListV[AST.Ty](), Lib.MkListV[AST.Term]()) + res.Append(makeSymbolType(createNodeElement(tmpFun), p.GetArgs().Len())) + + // Add the Type(s). + for _, elem := range p.GetTyArgs().GetSlice() { + res.Append(makeSymbolTypeTy(createNodeElement(elem))) + } + + // Add the element(s) + for _, arg := range p.GetArgs().GetSlice() { + argSeq := parseTerm(arg, ctx).GetSlice() + res.Append(argSeq...) + } + + return res +} + +func parseTerm(t AST.Term, ctx *NormalizerContext) Lib.List[SymbolType] { + + res := Lib.NewList[SymbolType]() + switch term := t.(type) { + + // if term is a function or cst, add it and call his args + case AST.Fun: + + funNoArgs := AST.MakerFun(term.GetID(), term.GetTyArgs(), Lib.NewList[AST.Term]()) + first_element := makeSymbolType(createNodeElement(funNoArgs), term.GetArgs().Len()) + //first_element := makeSymbolType(createNodeElement(term.GetID()), term.GetArgs().Len()) -> passer par ID ? + res.Append(first_element) + + // for _, ty := range term.GetTyArgs().GetSlice() { + // res.Append(parseTerm(ty, ctx).GetSlice()...) + // } + + for _, arg := range term.GetArgs().GetSlice() { + res.Append(parseTerm(arg, ctx).GetSlice()...) + } + + // Case meta, we have to transform it + case AST.Meta: + + originalName := term.GetName() // Name of the meta + _, exists := ctx.mapping[originalName] // Contains + if !exists { // If the meta is unknow + ctx.counter++ + newName := fmt.Sprintf("v%d", ctx.counter) // v + int. e.g v1,v2,v3,... + fakeMeta := AST.MakeMeta(ctx.counter, 0, newName, 0, term.GetTy()) + ctx.mapping[originalName] = fakeMeta // Update the mapping : X -> v1 or Y -> v2 .... ) + } + + normalizedMeta := ctx.mapping[originalName] // Return the transformed name association to the originalName before adding + res.Append(makeSymbolType(createNodeElement(normalizedMeta), 0)) // Add the new Meta to the return slice + + case AST.Id: + funNoArgs := AST.MakerFun(term, Lib.NewList[AST.Ty](), Lib.NewList[AST.Term]()) + first_element := makeSymbolType(createNodeElement(funNoArgs), 0) + res.Append(first_element) + + default: + Glob.Anomaly("Error with %s in ParseTerm", term.GetName()) + } + + return res + +} + +/*****************************/ +/********* End Parse *********/ +/*****************************/ + +/*****************************/ +/********* Transform *********/ +/*****************************/ + +// Case t is a Function => SymbolType{t.ID, t.getArgs} +// Case t is a cst => SymbolType{MakerFun(t.ID), 0} +// Case t is a Meta => SymbolType{t.ID, 0} +// Else Glob.Anomaly +func FirstElementToSymbolType(t AST.Term) SymbolType { + + switch t := t.(type) { + case AST.Fun: // Case function + funNoArgs := AST.MakerFun(t.GetID(), t.GetTyArgs(), Lib.NewList[AST.Term]()) + return SymbolType{createNodeElement(funNoArgs), t.GetArgs().Len()} + case AST.Id: // Case Constant + funNoArgs := AST.MakerFun(t, Lib.NewList[AST.Ty](), Lib.NewList[AST.Term]()) + return SymbolType{createNodeElement(funNoArgs), 0} + case AST.Meta: // Case metaVariable + return SymbolType{createNodeElement(t), 0} + default: // Not supposed to see something else + Glob.Anomaly("FirstElementToSymbolType Error", "Unknow type in FirstElementToSymbolType") + return SymbolType{createNodeElement(nil), -1} // Dog Code that will fail but won't be triggered due to Glob.Anomaly. Only here to please the compiler. + } +} + +// Depend of the Type, create the follow DiscriminationNode +// case AST.Fun => Create a List and fill it with TermToNode(GetArgs) then Maker DiscrmiminationNode +// Case AST.Id => MakeDiscriminationNode(FirstElementToSymbol) => Create Fun +// Case AST.Meta => MakeDiscriminationNode(FirstElementToSymbol) => Create Meta +func TermToNode(t AST.Term) DiscriminationNode { + switch t := t.(type) { + case AST.Fun: // Accumulate all the term of the AST.Term then create a Node with all the children + children := Lib.NewList[DiscriminationNode]() + for _, c := range t.GetArgs().GetSlice() { + children.Append(TermToNode(c)) + } + return MakeDiscriminationNodeWithSymAndChildren(FirstElementToSymbolType(t), children) + case AST.Id: + return MakeDiscriminationNodeWithSym(FirstElementToSymbolType(t)) + case AST.Meta: // Node with T as SymbolType and empty children / leafFor + return MakeDiscriminationNodeWithSym(FirstElementToSymbolType(t)) + default: + Glob.Anomaly("TermToST", "Var or Id") + return NewNode() + } +} + +/*****************************/ +/******* End Transform *******/ +/*****************************/ + +/*****************************/ +/*********** Insrt ***********/ +/*****************************/ + +// Insert a AST.Pred in the tree. If using a AST.Form or Something Else, it have to be cast when inserting ( tree = tree.Insert(px.(AST.pred)) ) +// Call the parser then the auxiliary function +func (dNode DiscriminationNode) Insert(p AST.Pred) DiscriminationNode { + + sym_list := parsePred(p, NewContext()) + return dNode.insertRec(sym_list, p) +} + +// Auxiliary function for insert. +func (dNode DiscriminationNode) insertRec(seq Lib.List[SymbolType], originalTerm AST.Pred) DiscriminationNode { + + // End of recursion, time to insert + if seq.Len() == 0 { + Exist := false + for _, pred := range dNode.getLeafFor().GetSlice() { + if pred.Equals(originalTerm) { + Exist = true + break + } + } + if !Exist { + dNode.leafFor.Append(originalTerm) + } + return dNode + } + + sym := seq.At(0) // Current symbol + childrenSlice := dNode.getChildren().GetSlice() + + foundIndex := -1 // Index of the symbol if found + var ok = false // Boolean if a match is found + + // Looking for already existing child + for i, child := range childrenSlice { + if child.getSymbol().getSymbol().Equals(sym.getSymbol()) { + if child.GetArity() == sym.GetArity() { + foundIndex = i + ok = true + break + } else { + Glob.Anomaly("Arity Missmatch", "Same Symbol but different Arity") + } + + } + } + + if ok { // Child already exist + + // Insert and update the sequence + updatedChild := childrenSlice[foundIndex].insertRec(seq.RemoveAt(0), originalTerm) + dNode.children.Upd(foundIndex, updatedChild) // Update children[foundIntex] = updateChild + + } else { // if Child doesn't exist + + newChild := MakeDiscriminationNodeWithSym(sym) // Create a new Node with the new SymbolType and his leafFor + updatedChild := newChild.insertRec(seq.RemoveAt(0), originalTerm) // Insert the rest of the sequence after the new child + dNode.children.Append(updatedChild) // Update the children of the args node + } + return dNode +} + +/*****************************/ +/********* End insrt *********/ +/*****************************/ + +/* Insert a raw term (as opposed to Insert, which takes a full predicate). + * Used to build a tree purely for term-level unification (UnifyTerm), the + * discriminationtree equivalent of codetree.MakeTermUnifProblem. */ +func (dNode DiscriminationNode) InsertTerm(t AST.Term) DiscriminationNode { + + sym_list := parseTerm(t, NewContext()) + result := dNode.insertTermRec(sym_list, t) + result.termOnly = true + return result +} + +// Auxiliary function for InsertTerm. Mirrors insertRec exactly, but stores +// into termLeafFor (AST.Term) instead of leafFor (AST.Pred). +func (dNode DiscriminationNode) insertTermRec(seq Lib.List[SymbolType], originalTerm AST.Term) DiscriminationNode { + + // End of recursion, time to insert + if seq.Len() == 0 { + Exist := false + for _, t := range dNode.getTermLeafFor().GetSlice() { + if t.Equals(originalTerm) { + Exist = true + break + } + } + if !Exist { + dNode.termLeafFor.Append(originalTerm) + } + return dNode + } + + sym := seq.At(0) // Current symbol + childrenSlice := dNode.getChildren().GetSlice() + + foundIndex := -1 // Index of the symbol if found + var ok = false // Boolean if a match is found + + // Looking for already existing child + for i, child := range childrenSlice { + if child.getSymbol().getSymbol().Equals(sym.getSymbol()) { + if child.GetArity() == sym.GetArity() { + foundIndex = i + ok = true + break + } else { + Glob.Anomaly("Arity Missmatch", "Same Symbol but different Arity") + } + + } + } + + if ok { // Child already exist + + // Insert and update the sequence + updatedChild := childrenSlice[foundIndex].insertTermRec(seq.RemoveAt(0), originalTerm) + dNode.children.Upd(foundIndex, updatedChild) // Update children[foundIntex] = updateChild + + } else { // if Child doesn't exist + + newChild := MakeDiscriminationNodeWithSym(sym) // Create a new Node with the new SymbolType and his leafFor + updatedChild := newChild.insertTermRec(seq.RemoveAt(0), originalTerm) // Insert the rest of the sequence after the new child + dNode.children.Append(updatedChild) // Update the children of the args node + } + return dNode +} + +/*****************************/ +/******* End term insrt ******/ +/*****************************/ + +/*****************************/ +/********** Retriev **********/ +/*****************************/ + +// typesCanUnify reports whether two type arguments, each kept by the tree as a +// single opaque node, could be unified. A type meta-variable unifies with any +// type; two constructors must share head symbol and argument count and unify +// argument-wise; anything else falls back to structural equality. +// +// The discrimination tree is only a *filter*: the final Robinson unification +// recomputes the real bindings, so this check must never under-approximate +// (a wrong "false" silently drops a genuinely unifiable candidate - the bug +// behind polymorphic goals such as maybe(A) vs maybe(sko)). Over-approximating +// is harmless: a wrong "true" merely yields a candidate that Robinson rejects. +func typesCanUnify(a, b AST.Ty) bool { + if _, ok := a.(AST.TyMeta); ok { + return true + } + if _, ok := b.(AST.TyMeta); ok { + return true + } + + ca, aok := a.(AST.TyConstr) + cb, bok := b.(AST.TyConstr) + if aok && bok { + if ca.Symbol() != cb.Symbol() || ca.Args().Len() != cb.Args().Len() { + return false + } + for i := range ca.Args().GetSlice() { + if !typesCanUnify(ca.Args().At(i), cb.Args().At(i)) { + return false + } + } + return true + } + + return a.Equals(b) +} + +// symbolsUnifiableModuloTypes reports whether a stored tree symbol and a query +// symbol denote the same function/predicate up to type-argument unification: +// same identifier, same term arity, and pairwise-unifiable type arguments. +// +// This is deliberately looser than SymbolType.Equals, which demands +// syntactically identical type arguments. Nested function symbols embed their +// type arguments (e.g. head in a stored polymorphic axiom vs head in a +// ground query), so requiring equality there prunes valid candidates exactly +// like the [Ty]-node case does; the concrete type binding is recovered by the +// final Robinson unification. +func symbolsUnifiableModuloTypes(treeSym, querySym SymbolType) bool { + if treeSym.GetArity() != querySym.GetArity() { + return false + } + + treeFun, tok := treeSym.getTerm().(AST.Fun) + queryFun, qok := querySym.getTerm().(AST.Fun) + if !tok || !qok { + return false + } + if !treeFun.GetID().Equals(queryFun.GetID()) { + return false + } + + treeTys := treeFun.GetTyArgs() + queryTys := queryFun.GetTyArgs() + if treeTys.Len() != queryTys.Len() { + return false + } + for i := range treeTys.GetSlice() { + if !typesCanUnify(treeTys.At(i), queryTys.At(i)) { + return false + } + } + return true +} + +func GetSubTermLength(seq []SymbolType) int { + if len(seq) == 0 { + return 0 + } + + needed := 1 // Type + Term + index := 0 + + for needed > 0 && index < len(seq) { + sym := seq[index] + arite := sym.GetArity() + + needed = needed - 1 + arite // If Arity == 0 ( Meta ) end this loop, else add the arity of the form/func/... + index++ + } + return index +} + +func (dNode DiscriminationNode) SkipTreeTermAndContinue(needed int, remainingQuery []SymbolType, substitutions subst.Substitutions) []CandidatResult { + + var subs []CandidatResult + + // End of recursion + if needed == 0 { + return dNode.retrieveRec(remainingQuery, substitutions) + } + + for _, child := range dNode.getChildren().GetSlice() { + newNeeded := needed - 1 + child.GetArity() // 0 if Meta, Else Arity of the Term + matches := child.SkipTreeTermAndContinue(newNeeded, remainingQuery, substitutions) + subs = append(subs, matches...) + } + return subs + +} + +func (dNode DiscriminationNode) RetrieveUnifiables(t AST.Form) []CandidatResult { + predFormula, _ := t.(AST.Pred) // Cast + seq := parsePred(predFormula, NewContext()).GetSlice() // Parser + Env := subst.Substitutions{} + return dNode.retrieveRec(seq, Env) +} + +func (dNode DiscriminationNode) retrieveRec(seq []SymbolType, currentEnv subst.Substitutions) []CandidatResult { + + ch := make(chan []CandidatResult) // Channel + var results []CandidatResult + + var wg sync.WaitGroup + + if len(seq) == 0 { // End of recursion + + for _, p := range dNode.getLeafFor().GetSlice() { + results = append(results, MakeCandidat(p, currentEnv)) + } + return results + } + + // Work goroutine: fan out one goroutine per child. Each child's subtree is + // independent of its siblings (no shared mutable state - currentEnv is + // read-only here, and every recursive call gets its own fresh results + // slice/channel), so this is safe, and lets wide/deep subtrees be searched + // in parallel instead of one child at a time. + for _, child := range dNode.children.GetSlice() { + + wg.Add(1) // Create exactly 1 goroutine + go retrieveCase(seq, currentEnv, child, ch, &wg) + } + + // Main goroutine waiting until all the goroutine stop + go func() { + wg.Wait() + close(ch) + }() + + for matches := range ch { + results = append(results, matches...) + } + + return results +} + +// Retrieve all the Unifiable +func retrieveCase(seq []SymbolType, currentEnv subst.Substitutions, child DiscriminationNode, ch chan<- []CandidatResult, wg *sync.WaitGroup) { + + defer wg.Done() // Always signal completion, even if this case matches nothing + symQuery := seq[0] // Term of the Query + + // Case 1. Exact Match, we go to the next element + isExactMatch := child.symbol.Equals(symQuery) + if isExactMatch { + matches := child.retrieveRec(seq[1:], currentEnv) + ch <- matches + return + } + + // Case 1bis. Type-argument matching up to unification. The tree keeps type + // arguments either as standalone [Ty] nodes (predicate level) or embedded on + // a function symbol (nested terms). A polymorphic stored type such as A / + // maybe(A) is not syntactically equal to a concrete query type such as + // sko / maybe(sko), yet the two unify, so we must descend rather than prune. + // Both kinds of node span exactly one sequence element, so we consume one + // element on each side; the final Robinson pass recomputes the type bindings. + if childTy, queryTy := child.getSymbol().GetTy(), symQuery.GetTy(); childTy != nil && queryTy != nil { + if typesCanUnify(childTy, queryTy) { + ch <- child.retrieveRec(seq[1:], currentEnv) + } + return + } + if symbolsUnifiableModuloTypes(child.getSymbol(), symQuery) { + ch <- child.retrieveRec(seq[1:], currentEnv) + return + } + + // Case 2. The Symbol from the discriminationTree is a Meta + // We need to look the len of the actual term from the sequence. f(x) == 2, y == 1 and we skip the entire term + if child.getSymbol().getSymbol().IsMeta() { + skip := GetSubTermLength(seq) + if skip <= len(seq) { + matches := child.retrieveRec(seq[skip:], currentEnv) + ch <- matches + } + return + + // Case 3. Reverse of the Case 2. + // The term from the Sequence is a Meta, so we look the len of the term from the DTree and we got skip it. + } else if symQuery.getSymbol().IsMeta() { + childResults := child.SkipTreeTermAndContinue(child.GetArity(), seq[1:], currentEnv) + ch <- childResults + } +} + +// Term-level mirror of SkipTreeTermAndContinue/RetrieveUnifiables/retrieveRec/ +// retrieveCase above: same exact logic, operating on termLeafFor (AST.Term) +// instead of leafFor (AST.Pred). Deliberately does not build up any +// substitution while walking down (case 3 below just skips structurally, +// like the classic predicate version does) - the caller redoes a full, +// clean Robinson unification at the end in UnifyTermWithSubst, so there is +// nothing here that could leak the tree's internal v1/v2-style normalized +// meta names into a caller's result (see the Unify2 fix elsewhere in this +// file for the bug this pattern avoids). + +func (dNode DiscriminationNode) SkipTreeTermAndContinueTerm(needed int, remainingQuery []SymbolType, substitutions subst.Substitutions) []TermCandidatResult { + + var subs []TermCandidatResult + + if needed == 0 { + return dNode.retrieveTermRec(remainingQuery, substitutions) + } + + for _, child := range dNode.getChildren().GetSlice() { + newNeeded := needed - 1 + child.GetArity() + matches := child.SkipTreeTermAndContinueTerm(newNeeded, remainingQuery, substitutions) + subs = append(subs, matches...) + } + return subs +} + +func (dNode DiscriminationNode) RetrieveUnifiableTerms(t AST.Term) []TermCandidatResult { + seq := parseTerm(t, NewContext()).GetSlice() + Env := subst.Substitutions{} + return dNode.retrieveTermRec(seq, Env) +} + +func (dNode DiscriminationNode) retrieveTermRec(seq []SymbolType, currentEnv subst.Substitutions) []TermCandidatResult { + + ch := make(chan []TermCandidatResult) + var results []TermCandidatResult + var wg sync.WaitGroup + + if len(seq) == 0 { + for _, t := range dNode.getTermLeafFor().GetSlice() { + results = append(results, MakeTermCandidat(t, currentEnv)) + } + return results + } + + for _, child := range dNode.children.GetSlice() { + wg.Add(1) + go retrieveCaseTerm(seq, currentEnv, child, ch, &wg) + } + + go func() { + wg.Wait() + close(ch) + }() + + for matches := range ch { + results = append(results, matches...) + } + + return results +} + +func retrieveCaseTerm(seq []SymbolType, currentEnv subst.Substitutions, child DiscriminationNode, ch chan<- []TermCandidatResult, wg *sync.WaitGroup) { + defer wg.Done() + + symQuery := seq[0] + + isExactMatch := child.symbol.Equals(symQuery) + if isExactMatch { + ch <- child.retrieveTermRec(seq[1:], currentEnv) + return + } + + // Case 1bis. Type-argument matching up to unification (see retrieveCase). + if childTy, queryTy := child.getSymbol().GetTy(), symQuery.GetTy(); childTy != nil && queryTy != nil { + if typesCanUnify(childTy, queryTy) { + ch <- child.retrieveTermRec(seq[1:], currentEnv) + } + return + } + if symbolsUnifiableModuloTypes(child.getSymbol(), symQuery) { + ch <- child.retrieveTermRec(seq[1:], currentEnv) + return + } + + if child.getSymbol().getSymbol().IsMeta() { + skip := GetSubTermLength(seq) + if skip <= len(seq) { + ch <- child.retrieveTermRec(seq[skip:], currentEnv) + } + return + + } else if symQuery.getSymbol().IsMeta() { + ch <- child.SkipTreeTermAndContinueTerm(child.GetArity(), seq[1:], currentEnv) + } +} + +/*****************************/ +/* DataStruct implementation */ +/*****************************/ + +// Print routes the tree dump through the "unif" debugger, exactly like the code +// tree's Print does. This keeps it silent on normal runs (e.g. -proof output) +// and only visible when debugging is enabled, instead of writing to stdout +// unconditionally. +func (dNode DiscriminationNode) Print() { + if dNode.IsEmpty() { + debug(Lib.MkLazy(func() string { return "Empty Tree" })) + return + } + debug(Lib.MkLazy(func() string { return "[ROOT]" })) + for _, child := range dNode.getChildren().GetSlice() { + child.displayRec(1) + } +} + +func (dNode DiscriminationNode) displayRec(depth int) { + + indent := strings.Repeat(" ", depth) + + var nodeTag string + + switch dNode.getSymbol().getSymbol().(type) { + case TyNode: + nodeTag = "[Ty]" + case TermNode: + nodeTag = "[Term]" + case NodeString: + nodeTag = "[String]" + } + + debug(Lib.MkLazy(func() string { + return fmt.Sprintf("%s|-- %s %s (arity: %d)", indent, nodeTag, dNode.toString(), dNode.GetArity()) + })) + + if dNode.getLeafFor().Len() > 0 { + leafIndent := indent + " " + for _, pred := range dNode.getLeafFor().GetSlice() { + debug(Lib.MkLazy(func() string { return fmt.Sprintf("%s[=> %s]", leafIndent, pred.ToString()) })) + } + } + + for _, child := range dNode.getChildren().GetSlice() { + child.displayRec(depth + 1) + } +} + +func (dNode DiscriminationNode) IsEmpty() bool { + return dNode.getChildren().Empty() +} + +func (dNode DiscriminationNode) Copy() subst.DataStructure { + newChildMaster := Lib.NewList[DiscriminationNode]() + for _, child := range dNode.getChildren().GetSlice() { + newChild := child.Copy().(DiscriminationNode) + newChildMaster.Append(newChild) + } + + newLeafFor := Lib.ListCpy(dNode.getLeafFor()) + newTermLeafFor := Lib.ListCpy(dNode.getTermLeafFor()) + return DiscriminationNode{ + symbol: dNode.symbol, + children: newChildMaster, + leafFor: newLeafFor, + termLeafFor: newTermLeafFor, + termOnly: dNode.termOnly, + } +} + +func (dNode DiscriminationNode) MakeDataStruct(formulas Lib.List[AST.Form], is_pos bool) subst.DataStructure { + + form := Lib.NewList[AST.Form]() + + for _, f := range formulas.GetSlice() { + switch nf := f.(type) { + case AST.Pred: + if is_pos { + form.Append(nf.Copy()) + } + case AST.Not: + switch nf.GetForm().(type) { + case AST.Pred: + if !(is_pos) { + form.Append(nf.GetForm()) + } + } + } + } + return dNode.InsertFormulaListToDataStructure(form) +} + +func (dNode DiscriminationNode) InsertFormulaListToDataStructure(lf Lib.List[AST.Form]) subst.DataStructure { + for _, f := range lf.GetSlice() { + switch nf := f.Copy().(type) { + case AST.Pred: + dNode = dNode.Insert(nf) + case AST.Not: + switch newForm := nf.GetForm().(type) { // Get the type AST.Form + case AST.Pred: + dNode = dNode.Insert(newForm) + } + } + } + return dNode +} + +/* Take a list of terms and build the corresponding discrimination tree. + * The discriminationtree equivalent of codetree.MakeTermUnifProblem: builds + * a tree purely for term-level unification (UnifyTerm), as opposed to + * Insert/Unify which index full predicates. */ +func MakeTermUnifProblem(l Lib.List[AST.Term]) subst.DataStructure { + root := NewNode() + for _, t := range l.GetSlice() { + root = root.InsertTerm(t) + } + return root +} + +func (dNode DiscriminationNode) Unify(inputFormula AST.Form) (bool, []subst.MixedSubstitutions) { + + // With -ep, use the early-pruning retrieval. Both paths run the exact same + // final Robinson unification (see Unify2), so they return the same result; + // the flag only lets us compare the two retrieval strategies' speed. + if Glob.GetEarlyPruning() { + return dNode.Unify2(inputFormula) + } + + candidates := dNode.RetrieveUnifiables(inputFormula) + var mixed []subst.MixedSubstitutions + var found bool + + // Robinson required Pred, so we verify + predFormula, isPred := inputFormula.(AST.Pred) + if !isPred { + Glob.Anomaly("DiscriminationTree Unify", "Expected a predicate") + return false, nil + } + queryTerm := subst.TransformPred(predFormula) // For Robinson + + for _, possibleMatch := range candidates { + initialSubst := subst.Substitutions{} + possibleMatchTerm := subst.TransformPred(possibleMatch.getPred()) // Pred -> Term for Robinson + finalSubst := subst.AddUnification(possibleMatchTerm, queryTerm, initialSubst) // Call Robinson + + if !finalSubst.Equals(subst.Failure()) { + found = true + matching := subst.MakeMatchingSubstitutions(possibleMatch.getPred(), finalSubst) + mixed = append(mixed, matching.ToMixed()) // convert To Mixed for return + } + } + + return found, mixed +} + +func (dNode DiscriminationNode) UnifyTerm(inputTerm AST.Term) (bool, []subst.MixedTermSubstitutions) { + return dNode.UnifyTermWithSubst(inputTerm, subst.MakeEmptySubstitution()) +} + +func (dNode DiscriminationNode) UnifyTermWithSubst(inputTerm AST.Term, globalSubst subst.Substitutions) (bool, []subst.MixedTermSubstitutions) { + var mixed []subst.MixedTermSubstitutions + var found bool + + seq := parseTerm(inputTerm, NewContext()).GetSlice() + + if dNode.termOnly { + // Term-only leaves (termLeafFor, populated via InsertTerm / + // MakeTermUnifProblem) - needed for trees that only ever hold raw terms. + termCandidates := dNode.retrieveTermRec(seq, globalSubst) + for _, possibleMatch := range termCandidates { + candidateTerm := possibleMatch.getTerm() + // Re-unify from the caller's own globalSubst, not from whatever + // possibleMatch itself carries - same reasoning as the Unify2 fix: + // the traversal's own bookkeeping must never leak into the result. + finalSubst := subst.AddUnification(inputTerm, candidateTerm, globalSubst.Copy()) + + if !finalSubst.Equals(subst.Failure()) { + found = true + mixMatch := subst.MixMatchSubstitutions{ + Tof: Lib.MkLeft[AST.Term, AST.Form](inputTerm), + Subst: finalSubst, + } + mixed = append(mixed, mixMatch.ToMixedTerm()) + } + } + return found, mixed + } + + // Predicate leaves (leafFor, populated via Insert), compared as terms via + // TransformPred - the original behaviour, for a tree built the "normal" way. + predCandidates := dNode.retrieveRec(seq, globalSubst) + for _, possibleMatch := range predCandidates { + candidateTerm := subst.TransformPred(possibleMatch.getPred()) + finalSubst := subst.AddUnification(inputTerm, candidateTerm, globalSubst) + + if !finalSubst.Equals(subst.Failure()) { + found = true + mixMatch := subst.MixMatchSubstitutions{ + Tof: Lib.MkLeft[AST.Term, AST.Form](inputTerm), + Subst: finalSubst, + } + mixed = append(mixed, mixMatch.ToMixedTerm()) + } + } + + return found, mixed +} + +/////////////////////////////////////////////// +/////// EARLY-PRUNING PART OF THE DTREE /////// +/////////////////////////////////////////////// + +// ReconstructTerm reads a flattened sequence of symbols generated by parseTerm and reconstructs the full AST.Term structure +// This allows the discrimination tree to extract a specific sub-query/sub-term and give it Robinson +func ReconstructTerm(seq []SymbolType) (AST.Term, []SymbolType) { + if len(seq) == 0 { + return nil, seq + } + + head := seq[0] + + // Ignore AST.Type if needed + if _, ok := head.getSymbol().(TyNode); ok { + return ReconstructTerm(seq[1:]) + } + + arite := head.GetArity() + term := head.getTerm() + currentSeq := seq[1:] + + switch t := term.(type) { + case AST.Fun: + // Reconstruct function arguments by recursively parsing subsequent elements + args := Lib.NewList[AST.Term]() + for i := 0; i < arite; i++ { + var arg AST.Term + arg, currentSeq = ReconstructTerm(currentSeq) + if arg != nil { + args.Append(arg) + } + } + return AST.MakerFun(t.GetID(), t.GetTyArgs(), args), currentSeq + case AST.Meta: + return t, currentSeq + case AST.Id: + return AST.MakerFun(t, Lib.NewList[AST.Ty](), Lib.NewList[AST.Term]()), currentSeq + default: + return nil, currentSeq + } +} + +// Unify2 call Robinson at the end, but relies on early pruning during the retrieval phase +func (dNode DiscriminationNode) Unify2(inputFormula AST.Form) (bool, []subst.MixedSubstitutions) { + candidates := dNode.RetrieveUnifiables2(inputFormula, subst.MakeEmptySubstitution()) + var mixed []subst.MixedSubstitutions + var found bool + + queryPred, isQueryPred := inputFormula.(AST.Pred) // Convert for Robinson + if !isQueryPred { + return false, mixed + } + + // The final unification is exactly the classic Unify one: transform predicate + // to term (types included, handled uniformly as term arguments) and run + // Robinson. Keeping this identical to Unify means the two modes differ *only* + // in their retrieval strategy (RetrieveUnifiables2's early pruning vs the + // classic RetrieveUnifiables), which is the whole point of the comparison. + queryTerm := subst.TransformPred(queryPred) + + for _, possibleMatch := range candidates { + candPred := possibleMatch.getPred() + candTerm := subst.TransformPred(candPred) + + // possibleMatch.GetSubs() carries whatever the early-pruning traversal + // accumulated, but those bindings are keyed by the tree's internally + // normalized metas (v1, v2, ... from NewContext()) and would leak into the + // result. The traversal only prunes; Robinson below re-unifies both full + // terms from scratch, so - like classic Unify - we start from a clean + // substitution. + finalSubst := subst.AddUnification(candTerm, queryTerm, subst.Substitutions{}) + + if !finalSubst.Equals(subst.Failure()) { + found = true + matching := subst.MakeMatchingSubstitutions(candPred, finalSubst) + mixed = append(mixed, matching.ToMixed()) + } + } + + return found, mixed +} + +// UnifyTerm performs unification directly on an AST.Term instead of a full AST.Form. +func (dNode DiscriminationNode) UnifyTerm2(inputTerm AST.Term) (bool, []subst.MixedTermSubstitutions) { + var mixed []subst.MixedTermSubstitutions + var found bool + + seq := parseTerm(inputTerm, NewContext()).GetSlice() + + candidates := dNode.retrieveRec2(seq, subst.MakeEmptySubstitution()) + + for _, possibleMatch := range candidates { + currentSubst := possibleMatch.GetSubs().Copy() + candidateTerm := subst.TransformPred(possibleMatch.getPred()) + + finalSubst := subst.AddUnification(inputTerm, candidateTerm, currentSubst) // Robinson call + + if !finalSubst.Equals(subst.Failure()) { + found = true + mixMatch := subst.MixMatchSubstitutions{ + Tof: Lib.MkLeft[AST.Term, AST.Form](inputTerm), + Subst: finalSubst, + } + mixed = append(mixed, mixMatch.ToMixedTerm()) + } + } + return found, mixed +} + +// RetrieveUnifiables2 parses the predicate formula and initiates the recursive, +// concurrent unifiable search starting from the current node. +func (dNode DiscriminationNode) RetrieveUnifiables2(t AST.Form, globalEnv subst.Substitutions) []CandidatResult { + predFormula, _ := t.(AST.Pred) + seq := parsePred(predFormula, NewContext()).GetSlice() + return dNode.retrieveRec2(seq, globalEnv) +} + +// Call a goroutine per branch in the discrimination tree. +func (dNode DiscriminationNode) retrieveRec2(seq []SymbolType, currentEnv subst.Substitutions) []CandidatResult { + ch := make(chan []CandidatResult) + var results []CandidatResult + var wg sync.WaitGroup + + // End of the sequence reached, collect all predicates stored at this leaf + if len(seq) == 0 { + for _, p := range dNode.getLeafFor().GetSlice() { + results = append(results, MakeCandidat(p, currentEnv.Copy())) + } + return results + } + + // Concurrently evaluate all branch + for _, child := range dNode.children.GetSlice() { + wg.Add(1) + go retrieveCase2(seq, currentEnv.Copy(), child, ch, &wg) + } + + go func() { + wg.Wait() + close(ch) + }() + + for matches := range ch { + results = append(results, matches...) + } + + return results +} + +// retrieveCase2 executes backtracking logic on a specific child node. It performs pruning , unification when encountering variables. +func retrieveCase2(seq []SymbolType, currentEnv subst.Substitutions, child DiscriminationNode, ch chan<- []CandidatResult, wg *sync.WaitGroup) { + defer wg.Done() + symQuery := seq[0] + childSym := child.getSymbol() + + isExactMatch := child.symbol.Equals(symQuery) + + // Case 1: Perfect structural symbol match + if isExactMatch { + matches := child.retrieveRec2(seq[1:], currentEnv) + ch <- matches + } + + // Case 1bis: type-argument / polymorphic symbol match up to unification + // (mirrors retrieveCase). A polymorphic stored type/symbol such as A / head + // is not syntactically equal to a concrete query one, yet the two unify, so we + // descend instead of pruning; the final Robinson pass recomputes the bindings. + // Not threaded through currentEnv on purpose: Unify2 re-unifies from a clean + // substitution at the end anyway, exactly like the classic path. + if !isExactMatch { + if childTy, queryTy := childSym.GetTy(), symQuery.GetTy(); childTy != nil && queryTy != nil { + if typesCanUnify(childTy, queryTy) { + ch <- child.retrieveRec2(seq[1:], currentEnv) + } + return + } + if symbolsUnifiableModuloTypes(childSym, symQuery) { + ch <- child.retrieveRec2(seq[1:], currentEnv) + return + } + } + + // Case 2: The tree contains a meta-variable branch (Early Pruning Attempt) + if childSym.getSymbol().IsMeta() && !isExactMatch { + queryTerm, restSeq := ReconstructTerm(seq) + + if queryTerm != nil && childSym.getTerm() != nil { + mergedSub := subst.AddUnification(childSym.getTerm(), queryTerm, currentEnv.Copy()) // Pruning + + if !mergedSub.Equals(subst.Failure()) { // If Succes Continue + matches := child.retrieveRec2(restSeq, mergedSub) + ch <- matches + } else { + // SAFETY FALLBACK: Robinson's unification failed. This might be a true failure + // or a false positive due to the Occur-Check on normalized variables (e.g., v1 vs v1). + // Instead of killing the branch, we skip the term and let the final Unify2 step decide. + skip := GetSubTermLength(seq) + if skip <= len(seq) { + matches := child.retrieveRec2(seq[skip:], currentEnv) + ch <- matches + } + } + } else if childSym.getTerm() == nil { + // Fallback if the tree term reference is empty: safely skip the matching sub-term length + skip := GetSubTermLength(seq) + if skip <= len(seq) { + matches := child.retrieveRec2(seq[skip:], currentEnv) + ch <- matches + } + } + + // Case 3: The query sequence contains a meta-variable + } else if symQuery.getSymbol().IsMeta() && !isExactMatch { + mergedSub := currentEnv.Copy() + + if child.GetArity() == 0 { + childTerm := childSym.getTerm() + symTerm := symQuery.getTerm() + + if childTerm != nil && symTerm != nil { + properTerm := childTerm + // Normalize standard IDs into empty functions to align with substitution expectations + if id, ok := childTerm.(AST.Id); ok { + properTerm = AST.MakerFun(id, Lib.NewList[AST.Ty](), Lib.NewList[AST.Term]()) + } + + currentSub := subst.MakeSubstitution(symTerm.ToMeta(), properTerm) + newSubstitutionS := subst.Substitutions{currentSub} + + if len(currentEnv) == 0 { + mergedSub = newSubstitutionS + } else { + mergedSub, _ = subst.MergeSubstitutions(currentEnv, newSubstitutionS) + } + } + } + + if !mergedSub.Equals(subst.Failure()) { + // Substitution successful: skip the tree's sub-structure and continue + childResults := child.SkipTreeTermAndContinue2(child.GetArity(), seq[1:], mergedSub) + ch <- childResults + } else { + // SAFETY FALLBACK: Same as above. Do not kill the branch on substitution failure. + // Skip the sub-structure using the unmodified environment a + childResults := child.SkipTreeTermAndContinue2(child.GetArity(), seq[1:], currentEnv) + ch <- childResults + } + } +} + +// SkipTreeTermAndContinue2 skips a Term and his args if needed +func (dNode DiscriminationNode) SkipTreeTermAndContinue2(needed int, remainingQuery []SymbolType, substitutions subst.Substitutions) []CandidatResult { + var subs []CandidatResult + + if needed == 0 { + return dNode.retrieveRec2(remainingQuery, substitutions) + } + + for _, child := range dNode.getChildren().GetSlice() { + // (amount - 1) + arity. If meta (amount - 1) + 0 else (amount - 1) + len(args) + arite := child.GetArity() + newNeeded := needed - 1 + arite + matches := child.SkipTreeTermAndContinue2(newNeeded, remainingQuery, substitutions) + subs = append(subs, matches...) + } + return subs +} diff --git a/src/Unif/discriminationtree/dt_test.go b/src/Unif/discriminationtree/dt_test.go new file mode 100644 index 00000000..ed938f72 --- /dev/null +++ b/src/Unif/discriminationtree/dt_test.go @@ -0,0 +1,2764 @@ +/** +* Copyright 2022 by the authors (see AUTHORS). +* +* Goéland is an automated theorem prover for first order logic. +* +* This software is governed by the CeCILL license under French law and +* abiding by the rules of distribution of free software. You can use, +* modify and/ or redistribute the software under the terms of the CeCILL +* license as circulated by CEA, CNRS and INRIA at the following URL +* "http://www.cecill.info". +* +* As a counterpart to the access to the source code and rights to copy, +* modify and redistribute granted by the license, users are provided only +* with a limited warranty and the software's author, the holder of the +* economic rights, and the successive licensors have only limited +* liability. +* +* In this respect, the user's attention is drawn to the risks associated +* with loading, using, modifying and/or developing or reproducing the +* software by the user in light of its specific status of free software, +* that may mean that it is complicated to manipulate, and that also +* therefore means that it is reserved for developers and experienced +* professionals having in-depth computer knowledge. Users are therefore +* encouraged to load and test the software's suitability as regards their +* requirements in conditions enabling the security of their systems and/or +* data to be ensured and, more generally, to use and operate it in the +* same conditions as regards security. +* +* The fact that you are presently reading this means that you have had +* knowledge of the CeCILL license and that you accept its terms. +**/ + +package discriminationtree + +import ( + "fmt" + "os" + "testing" + "time" + + "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" + "github.com/GoelandProver/Goeland/Lib" + "github.com/GoelandProver/Goeland/Typing" + subst "github.com/GoelandProver/Goeland/Unif/substitution" +) + +// Id +var p_id AST.Id +var g_id AST.Id +var f_id AST.Id +var a_id AST.Id +var b_id AST.Id +var c_id AST.Id +var d_id AST.Id +var c1_id AST.Id +var c2_id AST.Id +var P2_id AST.Id + +// Meta +var x AST.Meta +var v1 AST.Meta +var v2 AST.Meta +var y AST.Meta +var z AST.Meta +var z1 AST.Meta +var z2 AST.Meta +var z3 AST.Meta + +// Const +var a AST.Fun +var b AST.Fun +var c AST.Fun +var d AST.Fun +var c1 AST.Fun +var c2 AST.Fun + +// Fun +var f3 AST.Fun +var gx AST.Fun +var ga AST.Fun +var fx AST.Fun +var fy AST.Fun +var fa AST.Fun +var fb AST.Fun +var fc AST.Fun + +var gax AST.Fun +var gxb AST.Fun +var gyb AST.Fun +var gab AST.Fun +var gxc AST.Fun +var ggx AST.Fun +var gga AST.Fun +var gfy AST.Fun +var gfa AST.Fun +var gahc AST.Fun +var fxy AST.Fun +var fyz AST.Fun +var ffx AST.Fun +var fxa AST.Fun +var fay AST.Fun +var fab AST.Fun +var fbc AST.Fun +var fcd AST.Fun + +var gggx AST.Fun + +var f_fxy_z AST.Fun +var f_x_fyz AST.Fun +var f_fab_c AST.Fun +var f_a_fbc AST.Fun +var f_x_x AST.Fun +var f_y_y AST.Fun +var f_z_z AST.Fun +var f_gax_c AST.Fun +var f_gxb_y AST.Fun +var f_gyb_z AST.Fun +var f_gab_a AST.Fun +var f_gxc_b AST.Fun +var f_z_y AST.Fun +var f_x_y AST.Fun + +// Form +var pggab AST.Form +var not_pac AST.Form +var not_pba AST.Form +var pa AST.Form +var pb AST.Form + +var not_pc AST.Form +var pab AST.Form +var paa AST.Form +var pbb AST.Form + +var pabc AST.Form +var pba AST.Form + +var pca AST.Form +var pax AST.Form +var pay AST.Form +var pxa AST.Form +var pya AST.Form +var pxy AST.Form +var pxx AST.Form +var px AST.Form +var py AST.Form +var pxc AST.Form +var pfx AST.Form +var pfy AST.Form +var pafx AST.Form +var pafb AST.Form +var pafy AST.Form +var pfac AST.Form +var pgxb AST.Form +var pfxyb AST.Form + +var pfgaxc AST.Form +var pfgxby AST.Form +var pfgybz AST.Form +var pfgaba AST.Form +var pfgxcb AST.Form +var pfzy AST.Form +var pfxy AST.Form +var pfxx AST.Form +var pfzz AST.Form + +var not_pcd AST.Form + +var P2a AST.Form +var P2b AST.Form + +func initTestVariable() { + + // Id + p_id = AST.MakerId("P") + g_id = AST.MakerId("g") + f_id = AST.MakerId("f") + a_id = AST.MakerId("a") + b_id = AST.MakerId("b") + c_id = AST.MakerId("c") + d_id = AST.MakerId("d") + c1_id = AST.MakerId("c1") + c2_id = AST.MakerId("c2") + P2_id = AST.MakerId("P2") + + // Meta + x = AST.MakerMeta("X", -1, AST.TIndividual()) + v1 = AST.MakeMeta(1, 0, "v1", 0, AST.TIndividual()) + v2 = AST.MakeMeta(2, 0, "v2", 0, AST.TIndividual()) + y = AST.MakerMeta("Y", -1, AST.TIndividual()) + z = AST.MakerMeta("Z", -1, AST.TIndividual()) + z1 = AST.MakerMeta("Z1", -1, AST.TIndividual()) + z2 = AST.MakerMeta("Z2", -1, AST.TIndividual()) + z3 = AST.MakerMeta("Z3", -1, AST.TIndividual()) + + // Const + a = AST.MakerConst(a_id) + b = AST.MakerConst(b_id) + c = AST.MakerConst(c_id) + d = AST.MakerConst(d_id) + c1 = AST.MakerConst(c1_id) + c2 = AST.MakerConst(c2_id) + + // Fun + gx = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x)) + ga = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a)) + fx = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x)) + fy = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](y)) + fa = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a)) + fb = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](b)) + fc = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](c)) + ggx = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](gx)) + gga = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](ga)) + gfy = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](fy)) + gfa = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](fa)) + fxy = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, y)) + fyz = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](y, z)) + ffx = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](fx)) + gax = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, x)) + gxb = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, b)) + gyb = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](y, b)) + gab = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, b)) + gxc = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, c)) + fxa = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, a)) + fay = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, y)) + fab = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, b)) + fbc = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](b, c)) + fcd = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](c, d)) + gggx = AST.MakerFun(g_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](ggx)) + f_fxy_z = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](fxy, z)) + f_x_fyz = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, fyz)) + f_fab_c = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](fab, c)) + f_a_fbc = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, fbc)) + f_x_x = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, x)) + f_y_y = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](y, y)) + f_z_z = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](z, z)) + f_gax_c = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](gax, c)) + f_gxb_y = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](gxb, y)) + f_gyb_z = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](gyb, z)) + f_gab_a = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](gab, a)) + f_gxc_b = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](gxc, b)) + f_z_y = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](z, y)) + f_x_y = AST.MakerFun(f_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, y)) + + // Predicates + pggab = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](gga, b)) + not_pac = AST.MakerNot(AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, c))) + not_pba = AST.MakerNot(AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](b, a))) + not_pc = AST.MakerNot(AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](c))) + pab = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, b)) + paa = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, a)) + pbb = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](b, b)) + pabc = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, b, c)) + pba = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](b, a)) + pca = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](c, a)) + pax = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, x)) + pay = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, y)) + pxa = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, a)) + pya = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](y, a)) + pxy = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, y)) + pxx = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, x)) + px = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x)) + py = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](y)) + pxc = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](x, c)) + pfx = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](fx)) + pfy = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](fy)) + pafy = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, fy)) + pafx = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, fx)) + pafb = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a, fb)) + pfac = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](fa, c)) + pgxb = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](gx, b)) + pfxyb = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_x_y, b)) + pfgaxc = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_gax_c)) + pfgxby = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_gxb_y)) + pfgybz = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_gyb_z)) + pfgaba = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_gab_a)) + pfgxcb = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_gxc_b)) + pfzy = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_z_y)) + pfxy = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_x_y)) + pfxx = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_x_x)) + pfzz = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](f_z_z)) + not_pcd = AST.MakerNot(AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](c, d))) + pa = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a)) + pb = AST.MakerPred(p_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](b)) + P2a = AST.MakerPred(P2_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](a)) + P2b = AST.MakerPred(P2_id, Lib.NewList[AST.Ty](), Lib.MkListV[AST.Term](b)) +} + +// Typed Part + +var p_typed_id AST.Id +var b_typed_id AST.Id +var a_typed_id AST.Id +var a_typed AST.Ty +var p_typed_pred_Const_A AST.Pred +var p_typed_pred_Const_B AST.Pred +var p_typed_pred_int_2 AST.Pred +var p_typed_pred_int_3 AST.Pred +var p_typed_pred_int_2_int_3 AST.Pred +var p_typed_pred_int_2_double_4 AST.Pred +var p_typed_pred_int_2_int_3_a AST.Pred +var p_typed_pred_int_2_int_3_b AST.Pred +var p_typed_pred_int_2_double_4_a AST.Pred +var p_typed_pred_int_2_double_4_b AST.Pred +var p_typed_pred_int_2_double_4_x AST.Pred +var p_typed_pred_int_2_f_3 AST.Pred + +var p_typed_pred_int_int AST.Pred +var p_typed_pred_int_x AST.Pred +var p_typed_pred_int_x_y_z AST.Pred +var p_typed_pred_reel_x AST.Pred +var p_typed_pred_reel_x_y_z AST.Pred + +var p_typed_pred_rational_x AST.Pred + +var p_id_typed AST.Id +var p_typed AST.Pred +var random_type AST.Ty +var banane_id AST.Id +var banane AST.Term +var meta_typee AST.Term + +func initTestVariable2() { + + p_typed_id = AST.MakerId("p") + b_typed_id = AST.MakerId("b") + a_typed_id = AST.MakerId("A") + + A := AST.MkTyConst("A") + B := AST.MkTyConst("B") + + x = AST.MakerMeta("X", -1, AST.TIndividual()) + + p_typed_pred_Const_A = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](A), + Lib.MkListV[AST.Term](AST.MakerConst(a_typed_id)), + ) + + p_typed_pred_Const_B = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](B), + Lib.MkListV[AST.Term](AST.MakerConst(b_typed_id)), + ) + + p_typed_pred_int_x = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int")), + Lib.MkListV[AST.Term](x), + ) + + p_typed_pred_int_x_y_z = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int")), + Lib.MkListV[AST.Term](x, y, z), + ) + + p_typed_pred_reel_x = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.TReal()), + Lib.MkListV[AST.Term](x), + ) + + p_typed_pred_reel_x_y_z = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.TReal()), + Lib.MkListV[AST.Term](x, y, z), + ) + + p_typed_pred_rational_x = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.TRat()), + Lib.MkListV[AST.Term](x), + ) + + p_typed_pred_int_3 = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int")), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("3"))), + ) + + p_typed_pred_int_2_int_3 = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int")), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("2")), AST.MakerConst(AST.MakerId("3"))), + ) + + p_typed_pred_int_2_double_4 = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int"), (AST.MkTyConst("double"))), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("2")), AST.MakerConst(AST.MakerId("4"))), + ) + + p_typed_pred_int_2_int_3_a = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int")), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("2")), AST.MakerConst(AST.MakerId("3")), a), + ) + + p_typed_pred_int_2_int_3_b = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int")), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("2")), AST.MakerConst(AST.MakerId("3")), b), + ) + + p_typed_pred_int_2_double_4_a = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int"), (AST.MkTyConst("double")), AST.TIndividual()), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("2")), AST.MakerConst(AST.MakerId("4")), a), + ) + + p_typed_pred_int_2_double_4_b = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int"), (AST.MkTyConst("double")), AST.TIndividual()), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("2")), AST.MakerConst(AST.MakerId("4")), b), + ) + + p_typed_pred_int_2_double_4_x = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int"), (AST.MkTyConst("double")), AST.TIndividual()), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("2")), AST.MakerConst(AST.MakerId("4")), x), + ) + + p_typed_pred_int_2 = AST.MakerPred(p_typed_id, + Lib.MkListV[AST.Ty](AST.MkTyConst("int")), + Lib.MkListV[AST.Term](AST.MakerConst(AST.MakerId("2"))), + ) + + random_type = AST.MakerTyBV("random_type") + p_id_typed = AST.MakerId("p_typed") + meta_typee = AST.MakerMeta("Z", -1, random_type) + p_typed = AST.MakerPred(p_id_typed, Lib.MkListV(random_type), Lib.MkListV(meta_typee)) +} + +func initDebuggers() { + AST.InitDebugger() + Typing.InitDebugger() + subst.InitDebugger() + InitDebugger() +} + +func TestMain(m *testing.M) { + Glob.SetStart(time.Now()) + initDebuggers() + AST.Init() + Typing.Init() + initTestVariable() + initTestVariable2() + Glob.EnableDebug() + code := m.Run() + os.Exit(code) +} + +func TestFirstElementToSymbolType(t *testing.T) { + + t.Run("Fun_Multiple_Args", func(t *testing.T) { + st := FirstElementToSymbolType(fxy) + if st.GetArity() != 2 { + t.Errorf("Expected arity 2 for f(x, y), got %d", st.GetArity()) + } + }) + + t.Run("Fun_Constant", func(t *testing.T) { + st := FirstElementToSymbolType(a) + if st.GetArity() != 0 { + t.Errorf("Expected arity 0 for constant a, got %d", st.GetArity()) + } + }) + + t.Run("Meta_Variable", func(t *testing.T) { + st := FirstElementToSymbolType(x) + if st.GetArity() != 0 { + t.Errorf("Expected arity 0 for Meta variable x, got %d", st.GetArity()) + } + if !st.getSymbol().IsMeta() { + t.Errorf("Expected symbol to be recognized as Meta") + } + }) + + t.Run("Id_Type", func(t *testing.T) { + st := FirstElementToSymbolType(f_id) + if st.GetArity() != 0 { + t.Errorf("Expected arity 0 for ID type, got %d", st.GetArity()) + } + }) + + t.Run("Complex_Fun", func(t *testing.T) { + st := FirstElementToSymbolType(f_gax_c) + if st.GetArity() != 2 { + t.Errorf("Expected arity 2 for complex function f_gax_c, got %d", st.GetArity()) + } + }) + + t.Run("Exception_On_Nil_Term", func(t *testing.T) { + defer func() { + if r := recover(); r == nil { + t.Error("Expected a panic/exception when passing nil to FirstElementToSymbolType, but it completed without panicking") + } + }() + FirstElementToSymbolType(nil) + }) +} +func TestTermToNode(t *testing.T) { + + t.Run("Nominal_Fun_Single_Arg", func(t *testing.T) { + + node := TermToNode(ggx) + if node.GetArity() != 1 { + t.Errorf("Expected arity 1 for ggx, got %d", node.GetArity()) + } + if node.getChildren().Len() != 1 { + t.Errorf("Expected 1 child node for ggx, got %d", node.getChildren().Len()) + } + }) + + t.Run("Nominal_Fun_Multiple_Args", func(t *testing.T) { + + node := TermToNode(fbc) + if node.GetArity() != 2 { + t.Errorf("Expected arity 2 for fbc, got %d", node.GetArity()) + } + if node.getChildren().Len() != 2 { + t.Errorf("Expected 2 child nodes for fbc, got %d", node.getChildren().Len()) + } + }) + + t.Run("Nominal_Constant", func(t *testing.T) { + + node := TermToNode(a) + if node.GetArity() != 0 { + t.Errorf("Expected arity 0 for constant 'a', got %d", node.GetArity()) + } + if node.getChildren().Len() != 0 { + t.Errorf("Expected 0 child nodes for constant 'a', got %d", node.getChildren().Len()) + } + }) + + t.Run("Nominal_Meta", func(t *testing.T) { + + node := TermToNode(x) + if node.GetArity() != 0 { + t.Errorf("Expected arity 0 for Meta variable 'x', got %d", node.GetArity()) + } + if node.getChildren().Len() != 0 { + t.Errorf("Expected 0 child nodes for Meta variable, got %d", node.getChildren().Len()) + } + }) + + t.Run("Nominal_Id", func(t *testing.T) { + + node := TermToNode(f_id) + if node.GetArity() != 0 { + t.Errorf("Expected arity 0 for ID type 'f_id', got %d", node.GetArity()) + } + }) + + t.Run("Exception_On_Nil_Term", func(t *testing.T) { + + defer func() { + if r := recover(); r == nil { + t.Error("Expected a panic/exception when passing nil to TermToNode, but it completed without panicking") + } + }() + TermToNode(nil) + }) +} + +func TestCreateNodeElement(t *testing.T) { + + t.Run("Nominal_String", func(t *testing.T) { + strInput := "test_identifier" + node := createNodeElement(strInput) + + if ns, ok := node.(NodeString); !ok { + t.Errorf("Expected return type NodeString, got %T", node) + } else if ns.ToString() != strInput { + t.Errorf("Expected NodeString value to be '%s', got '%s'", strInput, ns.ToString()) + } + }) + + t.Run("Nominal_AST_Ty", func(t *testing.T) { + node := createNodeElement(random_type) + + if _, ok := node.(TyNode); !ok { + t.Errorf("Expected return type TyNode for AST.Ty input, got %T", node) + } + }) + + t.Run("Nominal_AST_Pred", func(t *testing.T) { + node := createNodeElement(pa.(AST.Pred)) + + termNode, ok := node.(TermNode) + if !ok { + t.Errorf("Expected return type TermNode for AST.Pred input, got %T", node) + } + + if !termNode.Term.IsFun() { + t.Errorf("Expected the transformed AST.Pred to be wrapped as an AST.Fun inside the TermNode") + } + }) + + t.Run("Nominal_AST_Term", func(t *testing.T) { + node := createNodeElement(fxy) + + if _, ok := node.(TermNode); !ok { + t.Errorf("Expected return type TermNode for AST.Term input, got %T", node) + } + }) + + t.Run("Exception_On_Unhandled_Type", func(t *testing.T) { + defer func() { + if r := recover(); r == nil { + t.Error("Expected a panic/exception when passing an integer, but it completed without panicking") + } + }() + + createNodeElement(42) + }) + + t.Run("Exception_On_Nil", func(t *testing.T) { + defer func() { + if r := recover(); r == nil { + t.Error("Expected a panic/exception when passing nil, but it completed without panicking") + } + }() + + createNodeElement(nil) + }) +} + +func TestInsert(t *testing.T) { + + t.Run("Nominal_Multiple_Inserts", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pba.(AST.Pred)) + tree = tree.Insert(pab.(AST.Pred)) + tree = tree.Insert(pafx.(AST.Pred)) + tree = tree.Insert(pafy.(AST.Pred)) + tree.Print() + + children := tree.getChildren().GetSlice() + if len(children) != 1 { + t.Errorf("Expected root node to have exactly 1 child (the 'P' predicate node), got %d", len(children)) + } + pNode := children[0] + if pNode.GetArity() != 2 { + t.Errorf("Expected the 'P' node to have arity 2, got %d", pNode.GetArity()) + } + + }) + + t.Run("Nominal_Single_Nested_Insert", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pfx.(AST.Pred)) + children := tree.getChildren().GetSlice() + if len(children) != 1 { + t.Fatalf("Expected root node to have exactly 1 child, got %d", len(children)) + } + pNode := children[0] + if pNode.GetArity() != 1 { + t.Errorf("Expected the 'P' node to have arity 1, got %d", pNode.GetArity()) + } + }) + + t.Run("Nominal_Insert_Variable_Overlap", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pfx.(AST.Pred)) + tree = tree.Insert(pfy.(AST.Pred)) + + children := tree.getChildren().GetSlice() + if len(children) != 1 { + t.Fatalf("Expected root node to have exactly 1 child, got %d", len(children)) + } + + }) + + t.Run("Exception_Arity_Collision", func(t *testing.T) { + defer func() { + if r := recover(); r == nil { + t.Error("Expected a panic when inserting a predicate with a conflicting arity on an existing path") + } + }() + + tree := NewNode() + tree = tree.Insert(pab.(AST.Pred)) + tree = tree.Insert(pabc.(AST.Pred)) // Arity Error + tree.Print() + }) +} + +func TestPrintDoublonCheck(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + tree = tree.Insert(pa.(AST.Pred)) + tree.Print() + + if tree.getChildren().Len() != 1 { + t.Fatalf("Error Duplicate Branch") + } + +} + +func TestPrintHugeTree(t *testing.T) { + + t.Run("Nominal_Huge_Tree_Structure", func(t *testing.T) { + tree := NewNode() + + tree = tree.Insert(pfgaxc.(AST.Pred)) + tree = tree.Insert(pfgxby.(AST.Pred)) + tree = tree.Insert(pfgybz.(AST.Pred)) + tree = tree.Insert(pfgaba.(AST.Pred)) + tree = tree.Insert(pfgxcb.(AST.Pred)) + tree = tree.Insert(pfzy.(AST.Pred)) + tree = tree.Insert(pfxy.(AST.Pred)) + tree = tree.Insert(pfxx.(AST.Pred)) + tree = tree.Insert(pfzz.(AST.Pred)) + tree.Print() + + rootChildren := tree.getChildren().GetSlice() + if len(rootChildren) != 1 { // P + t.Fatalf("Expected the root node to have exactly 1 child (the 'P' predicate), got %d", len(rootChildren)) + } + + pNode := rootChildren[0] + if pNode.GetArity() != 1 { + t.Errorf("Expected 'P' node to have arity 1, got %d", pNode.GetArity()) + } + + pChildren := pNode.getChildren().GetSlice() + if len(pChildren) != 1 { + t.Fatalf("Expected 'P' node to have exactly 1 child ('f'), got %d", len(pChildren)) + } + fNode := pChildren[0] // [Term] f + + if fNode.GetArity() != 2 { // f(arg1, arg2) + t.Errorf("Expected 'f' node to have arity 2, got %d", fNode.GetArity()) + } + + fChildren := fNode.getChildren().GetSlice() + if len(fChildren) != 2 { // g & v1 + t.Fatalf("Expected 'f' node to branch into exactly 2 paths ('g' and a Meta variable v1), got %d", len(fChildren)) + } + + var gNode, metaNode *DiscriminationNode + for i := range fChildren { + if fChildren[i].getSymbol().getSymbol().IsMeta() { + metaNode = &fChildren[i] + } else { + gNode = &fChildren[i] + } + } + + if gNode == nil || metaNode == nil { + t.Fatalf("Expected to find one 'g' node and one Meta node as children of 'f'") + } + + if metaNode.GetArity() != 0 { + t.Errorf("Expected Meta node to have arity 0, got %d", metaNode.GetArity()) + } + + metaChildren := metaNode.getChildren().GetSlice() + if len(metaChildren) != 2 { + t.Fatalf("Expected Meta variable v1 under 'f' to branch into 2 children (v2 and v1), got %d", len(metaChildren)) + } + + var meta1Meta1Node, meta1Meta2Node *DiscriminationNode + for i := range metaChildren { + if metaChildren[i].getSymbol().getSymbol().ToString() == "v1" { // ou selon l'index de ta variable + meta1Meta1Node = &metaChildren[i] + } else { + meta1Meta2Node = &metaChildren[i] + } + } + + if meta1Meta2Node.getChildren().Len() != 0 { + t.Fatalf("Expected v2 node to be a leaf (0 children), got %d", meta1Meta2Node.getChildren().Len()) + } + if meta1Meta2Node.getLeafFor().Len() != 2 { + t.Errorf("Expected v2 node to contain exactly 2 leaf formulas, got %d", meta1Meta2Node.getLeafFor().Len()) + } + + if meta1Meta1Node.getChildren().Len() != 0 { + t.Fatalf("Expected v1 node to be a leaf (0 children), got %d", meta1Meta1Node.getChildren().Len()) + } + if meta1Meta1Node.getLeafFor().Len() != 2 { + t.Errorf("Expected v1 node to contain exactly 2 leaf formulas, got %d", meta1Meta1Node.getLeafFor().Len()) + } + + if gNode.GetArity() != 2 { // g(arg1, arg2) + t.Errorf("Expected 'g' node to have arity 2, got %d", gNode.GetArity()) + } + + gChildren := gNode.getChildren().GetSlice() + if len(gChildren) != 2 { // a & v1 + t.Fatalf("Expected 'g' node to branch into exactly 2 paths ('a' and a Meta variable v1), got %d", len(gChildren)) + } + + var aNode, gMetaNode *DiscriminationNode + for i := range gChildren { + if gChildren[i].getSymbol().getSymbol().IsMeta() { + gMetaNode = &gChildren[i] + } else if gChildren[i].getSymbol().getSymbol().ToString() == "a" { + aNode = &gChildren[i] + } + } + + if aNode == nil || gMetaNode == nil { + t.Fatalf("Expected to find one 'a' node and one Meta node 'v1' under 'g'") + } + + aChildren := aNode.getChildren().GetSlice() + if len(aChildren) != 2 { // v1 & b + t.Fatalf("Expected 'a' node to branch into exactly 2 paths (Meta 'v1' and constant 'b'), got %d", len(aChildren)) + } + + var aMetaNode, abNode *DiscriminationNode + for i := range aChildren { + if aChildren[i].getSymbol().getSymbol().IsMeta() { + aMetaNode = &aChildren[i] + } else if aChildren[i].getSymbol().getSymbol().ToString() == "b" { + abNode = &aChildren[i] + } + } + + if aMetaNode.getChildren().Len() != 1 { + t.Fatalf("Expected 'v1' under 'a' to have exactly 1 child ('c'), got %d", aMetaNode.getChildren().Len()) + } + acNode := aMetaNode.getChildren().At(0) + if acNode.getSymbol().getSymbol().ToString() != "c" { + t.Errorf("Expected node to be 'c', got %s", acNode.getSymbol().getSymbol().ToString()) + } + if acNode.getLeafFor().Len() != 1 { + t.Errorf("Expected 'c' node to have exactly 1 leaf formula, got %d", acNode.getLeafFor().Len()) + } + + if abNode.getChildren().Len() != 1 { + t.Fatalf("Expected 'b' under 'a' to have exactly 1 child ('a'), got %d", abNode.getChildren().Len()) + } + abaNode := abNode.getChildren().At(0) + if abaNode.getSymbol().getSymbol().ToString() != "a" { + t.Errorf("Expected leaf node to be 'a', got %s", abaNode.getSymbol().getSymbol().ToString()) + } + if abaNode.getLeafFor().Len() != 1 { + t.Errorf("Expected leaf 'a' node to have exactly 1 leaf formula, got %d", abaNode.getLeafFor().Len()) + } + + gMetaChildren := gMetaNode.getChildren().GetSlice() + if len(gMetaChildren) != 2 { // b & c + t.Fatalf("Expected Meta node 'v1' under 'g' to branch into exactly 2 paths ('b' and 'c'), got %d", len(gMetaChildren)) + } + + var gbNode, gcNode *DiscriminationNode + for i := range gMetaChildren { + if gMetaChildren[i].getSymbol().getSymbol().ToString() == "b" { + gbNode = &gMetaChildren[i] + } else if gMetaChildren[i].getSymbol().getSymbol().ToString() == "c" { + gcNode = &gMetaChildren[i] + } + } + + if gbNode.getChildren().Len() != 1 { + t.Fatalf("Expected 'b' under 'v1' to have exactly 1 child (Meta 'v2'), got %d", gbNode.getChildren().Len()) + } + gbMetaNode := gbNode.getChildren().At(0) + if !gbMetaNode.getSymbol().getSymbol().IsMeta() { + t.Errorf("Expected child of 'b' to be a Meta variable") + } + if gbMetaNode.getLeafFor().Len() != 2 { + t.Errorf("Expected Meta leaf node to contain exactly 2 leaf formulas, got %d", gbMetaNode.getLeafFor().Len()) + } + + if gcNode.getChildren().Len() != 1 { + t.Fatalf("Expected 'c' under 'v1' to have exactly 1 child ('b'), got %d", gcNode.getChildren().Len()) + } + gcbNode := gcNode.getChildren().At(0) + if gcbNode.getSymbol().getSymbol().ToString() != "b" { + t.Errorf("Expected leaf node to be 'b', got %s", gcbNode.getSymbol().getSymbol().ToString()) + } + if gcbNode.getLeafFor().Len() != 1 { + t.Errorf("Expected leaf 'b' node to have exactly 1 leaf formula, got %d", gcbNode.getLeafFor().Len()) + } + }) +} + +func TestParseTerm(t *testing.T) { + + t.Run("Parse_Simple_fxy", func(t *testing.T) { + + tmpContext := NewContext() + seqList := parseTerm(fxy, tmpContext) + seq := seqList.GetSlice() + + for _, elem := range seq { + fmt.Println(elem.ToString()) + } + + if len(seq) != 3 { + t.Fatalf("Expected 3 elements for f(x,y), got %d", len(seq)) + } + + if seq[0].GetArity() != 2 || seq[0].getSymbol().ToString() != "f" { + t.Fatal("Element 0 must be function 'f' with arity 2") + } + + if seq[1].GetArity() != 0 || !seq[1].getSymbol().IsMeta() { + t.Fatal("Element 1 must be meta variable 'v1' with arity 0") + } + + if seq[2].GetArity() != 0 || !seq[2].getSymbol().IsMeta() { + t.Fatal("Element 2 must be meta variable 'v2' with arity 0") + } + }) + t.Run("Parse_Nested_Left_f_fxy_z", func(t *testing.T) { + tmpContext2 := NewContext() + seqList := parseTerm(f_fxy_z, tmpContext2) + seq := seqList.GetSlice() + + if len(seq) != 5 { + t.Fatalf("Expected 5 elements for f(f(x,y), z), got %d", len(seq)) + } + + if seq[0].GetArity() != 2 || seq[0].getSymbol().ToString() != "f" { + t.Fatal("Element 0 must be the outer function 'f' with arity 2") + } + + if seq[1].GetArity() != 2 || seq[1].getSymbol().ToString() != "f" { + t.Fatal("Element 1 must be the inner function 'f' with arity 2") + } + + if seq[2].GetArity() != 0 || !seq[2].getSymbol().IsMeta() { + t.Fatal("Element 2 must be meta variable 'v1' with arity 0") + } + + if seq[3].GetArity() != 0 || !seq[3].getSymbol().IsMeta() { + t.Fatal("Element 3 must be meta variable 'v2' with arity 0") + } + + if seq[4].GetArity() != 0 || !seq[4].getSymbol().IsMeta() { + t.Fatal("Element 4 must be meta variable 'v3' with arity 0") + } + }) + + t.Run("Parse_Nested_Right_f_x_fyz", func(t *testing.T) { + tmpContext4 := NewContext() + seqList := parseTerm(f_x_fyz, tmpContext4) + seq := seqList.GetSlice() + + if len(seq) != 5 { + t.Fatalf("Expected 5 elements for f(x, f(y,z)), got %d", len(seq)) + } + + if seq[0].GetArity() != 2 || seq[0].getSymbol().ToString() != "f" { + t.Fatal("Element 0 must be outer function 'f' with arity 2") + } + + if seq[1].GetArity() != 0 || !seq[1].getSymbol().IsMeta() { + t.Fatal("Element 1 must be meta variable 'v1' with arity 0") + } + + if seq[2].GetArity() != 2 || seq[2].getSymbol().ToString() != "f" { + t.Fatal("Element 2 must be inner function 'f' with arity 2") + } + + if seq[3].GetArity() != 0 || !seq[3].getSymbol().IsMeta() { + t.Fatal("Element 3 must be meta variable 'v2' with arity 0") + } + + if seq[4].GetArity() != 0 || !seq[4].getSymbol().IsMeta() { + t.Fatal("Element 4 must be meta variable 'v3' with arity 0") + } + }) +} + +func TestRetrieve(t *testing.T) { + + t.Run("RetrieveUnifiable_pax_pay_and_pab", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + tree = tree.Insert(pay.(AST.Pred)) + results := tree.RetrieveUnifiables(pab) + + if len(results) != 2 { + t.Fatalf("Must return 2 element") + } else { + fmt.Printf("returned %d element", len(results)) + } + + }) + + t.Run("RetrieveUnifiable_pax_pxy_and_pab", func(t *testing.T) { + + fmt.Println() + tree2 := NewNode() + tree2 = tree2.Insert(pax.(AST.Pred)) + results2 := tree2.RetrieveUnifiables(pay) + + if len(results2) != 1 { + t.Fatalf("Supposed to have 1 CandidatResults") + } + + }) + +} +func TestEquals(t *testing.T) { + + t.Run("x Equals x", func(t *testing.T) { + + ok := x.Equals(x) + if !ok { + t.Fatalf("Equals Test failure on x Equals x ") + } + + }) + + t.Run("pxx Equals pxx", func(t *testing.T) { + + ok2 := pxx.Equals(pxx) + if !ok2 { + t.Fatalf("Equals Test failure on pxx Equals pxx ") + } + + }) + + t.Run("fab Equals fab", func(t *testing.T) { + + ok3 := fab.Equals(fab) + if !ok3 { + t.Fatalf("Equals Test failure on pab Equals pab ") + } + + }) + + t.Run("fab Equals fay", func(t *testing.T) { + + ok4 := fab.Equals(fay) + if ok4 { + t.Fatalf("Equals Test Succes on fab Equals fay") + } + + }) + + t.Run("fx Equals fy", func(t *testing.T) { + + ok5 := fx.Equals(fy) + if ok5 { + t.Fatalf("Equals Test Succes on fab Equals fay") + } + + }) + +} + +func TestGetSubTermLength(t *testing.T) { + Context := NewContext() + + t.Run("SubTerm_Constant_Or_Meta", func(t *testing.T) { + seq := parseTerm(gx, Context).GetSlice() + // seq == [g, x] == [x] + + length := GetSubTermLength(seq) + + for _, elem := range seq { + fmt.Println(elem.ToString()) + } + + if length != 2 { + t.Fatalf("Expected length 1 for a single Meta/Constant, got %d", length) + } + }) + + t.Run("SubTerm_gx", func(t *testing.T) { + // g(x) -> [g, x] + seq := parseTerm(gx, Context).GetSlice() + termSeq := seq[1:] // Remove g() + + length := GetSubTermLength(termSeq) + if length != 1 { + t.Fatalf("Error SubTermLength Expected 1, got %d", length) + } + Context.Reset() + }) + + t.Run("SubTerm_ggx", func(t *testing.T) { + // g(g(x)) -> [g, g, x] + seq := parseTerm(ggx, Context).GetSlice() + + length := GetSubTermLength(seq) + if length != 3 { + t.Fatalf("Error SubTermLength with 2 nested functions. Expected 3, got %d", length) + } + }) + + t.Run("SubTerm_gggx", func(t *testing.T) { + // g(g(g(x))) -> [g, g, g, x] + seq := parseTerm(gggx, Context).GetSlice() + + length := GetSubTermLength(seq) + if length != 4 { + t.Fatalf("Error SubTermLength with 3 nested functions. Expected 4, got %d", length) + } + }) + + t.Run("SubTerm_fxy", func(t *testing.T) { + // f(x, y) -> [f, x, y] + seq := parseTerm(fxy, Context).GetSlice() + + length := GetSubTermLength(seq) + if length != 3 { + t.Fatalf("Error SubTermLength with 1 function & 2 Metas. Expected 3, got %d", length) + } + Context.Reset() + }) + + t.Run("SubTerm_With_Trailing_Tokens", func(t *testing.T) { + // P(g(x), a) after consumming P and g(x). + // [g, Ty_x, x, Ty_a, a] + // GetSubTermLength stop after g(x) + seq := parseTerm(x, Context).GetSlice() // [g, x] + + length := GetSubTermLength(seq) + if length != 1 { + t.Fatalf("GetSubTermLength failed to isolate the first subterm when trailing tokens are present. Expected 3, got %d", length) + } + }) +} + +func TestSkipTreeTermAndContinue(t *testing.T) { + + ctx := NewContext() + + t.Run("SkipTreeTermAndContinue_pfx", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pfx.(AST.Pred)) + fullSeq := parsePred(pfx.(AST.Pred), ctx).GetSlice() + tree = tree.children.At(0) // 'P' + needed := 1 + + remainingQuery := fullSeq[len(fullSeq):] + emptyEnv := subst.Substitutions{} + + results := tree.SkipTreeTermAndContinue(needed, remainingQuery, emptyEnv) + if len(results) != 1 { + t.Fatalf("Expected 1 Element, got %d", len(results)) + } + + for _, elem := range results { + fmt.Println("elem", elem.toString()) + } + }) + + t.Run("SkipTreeTermAndContinue_pfxy", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pfxy.(AST.Pred)) + + fullSeq := parsePred(pfxy.(AST.Pred), ctx).GetSlice() + + tree = tree.children.At(0) // 'P' + + needed := 1 + + remainingQuery := fullSeq[len(fullSeq):] + emptyEnv := subst.Substitutions{} + + results := tree.SkipTreeTermAndContinue(needed, remainingQuery, emptyEnv) + if len(results) != 1 { + t.Fatalf("Expected 1 Element, got %d", len(results)) + } + for _, elem := range results { + fmt.Println("elem", elem.toString()) + } + }) + + t.Run("SkipTreeTermAndContinue_pggab", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pggab.(AST.Pred)) + + fullSeq := parsePred(pggab.(AST.Pred), ctx).GetSlice() + + tree = tree.children.At(0) // 'P' + needed := tree.GetArity() + + remainingQuery := fullSeq[len(fullSeq):] + emptyEnv := subst.Substitutions{} + + results := tree.SkipTreeTermAndContinue(needed, remainingQuery, emptyEnv) + if len(results) != 1 { + t.Fatalf("Got %d, Expected 1", len(results)) + } + + for _, elem := range results { + fmt.Println("elem", elem.toString()) + } + }) +} + +func TestRetrieveUnifiables(t *testing.T) { + + t.Run("TestRetrieveUnifiables_pax_pba", func(t *testing.T) { + + tree := NewNode() + candidat := []CandidatResult{} + + tree = tree.Insert(pax.(AST.Pred)) + tree = tree.Insert(pba.(AST.Pred)) + candidat = tree.RetrieveUnifiables(pay) + if len(candidat) != 1 { + t.Fatalf("Should be only 1") + } + + for _, elem := range candidat { + fmt.Println("elem Pred", elem.getPred().ToString()) + fmt.Println("elem Subs", elem.GetSubs().ToString()) + } + + }) + + t.Run("TestRetrieveUnifiables_pafb", func(t *testing.T) { + + tree := NewNode() + candidat := []CandidatResult{} + + tree = tree.Insert(pafb.(AST.Pred)) + tree = tree.Insert(pab.(AST.Pred)) + tree.Print() + + candidat = tree.RetrieveUnifiables(pay) + + for _, elem := range candidat { + fmt.Println("elem", elem.toString()) + } + + if len(candidat) != 2 { + t.Fatalf("Should be only 2 got %d", len(candidat)) + } + + }) + + t.Run("TestRetrieveUnifiables_pa", func(t *testing.T) { + + tree := NewNode() + candidat := []CandidatResult{} + + tree = tree.Insert(pa.(AST.Pred)) + candidat = tree.RetrieveUnifiables(pb) + if len(candidat) != 0 { + t.Fatalf("Should be 0 because pa and pb can't be unified") + } + + }) + + t.Run("TestRetrieveUnifiables_pxy", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pxy.(AST.Pred)) + candidat := tree.RetrieveUnifiables(pab) + if len(candidat) == 0 { + t.Fatalf("pxy and pab are unifiables") + } + + fmt.Println(len(candidat)) + + }) +} + +func TestCopy(t *testing.T) { + + t.Run("TestCopy_pax", func(t *testing.T) { + + tree1 := NewNode() + tree2 := tree1.Copy() + tree1 = tree1.Insert(pax.(AST.Pred)) + res2 := tree2.IsEmpty() + if !res2 { + t.Fatalf("Tree2 is not a copy, it s only a pointer to tree1") + } + + }) + + t.Run("TestCopy_pafx", func(t *testing.T) { + + tree3 := NewNode() + tree4 := tree3.Copy() + tree3 = tree3.Insert(pafx.(AST.Pred)) + res3 := tree4.IsEmpty() + if !res3 { + t.Fatalf("Tree4 is not a copy, it s only a pointer to tree3") + } + + }) + +} + +func TestUnify(t *testing.T) { + + t.Run("Unify_pax_with_pay", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + + found, mix := tree.Unify(pay) + + if !found { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result, got %d", len(mix)) + } + if mix[0].GetForm().ToString() != "P(a, X)" { + t.Errorf("Expected unified form to be 'P(a, X)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify_pax_with_pab", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + + found, mix := tree.Unify(pab) + + if !found { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result, got %d", len(mix)) + } + if mix[0].GetForm().ToString() != "P(a, X)" { + t.Errorf("Expected unified form to be 'P(a, X)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify_pa_with_pa", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + + found, mix := tree.Unify(pa) + + if !found { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result, got %d", len(mix)) + } + if mix[0].GetForm().ToString() != "P(a)" { + t.Errorf("Expected unified form to be 'P(a)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify_pax_with_pafy", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + + found, mix := tree.Unify(pafy) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(a, X)" { + t.Errorf("Expected unified form to be 'P(a, X)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify_pafx_with_pafy", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pafx.(AST.Pred)) + + found, mix := tree.Unify(pafy) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(a, f(X))" { + t.Errorf("Expected unified form to be 'P(a, f(X))', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify_px_with_py", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(px.(AST.Pred)) + + found, mix := tree.Unify(py) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(X)" { + t.Errorf("Expected unified form to be 'P(X)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify_pxy_with_pab", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pxy.(AST.Pred)) + + found, mix := tree.Unify(pab) + + fmt.Println(len(mix)) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(X, Y)" { + t.Errorf("Expected unified form to be 'P(X, Y)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify_Multiple_Inserts_with_py", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pb.(AST.Pred)) + tree = tree.Insert(pa.(AST.Pred)) + tree = tree.Insert(pfx.(AST.Pred)) + + // P(Y) can unify with P(b), P(a), and P(f(x)) + found, mix := tree.Unify(py) + + if !found || len(mix) != 3 { + t.Fatalf("Expected exactly 3 unification results, got %d", len(mix)) + } + + // Unification wraps the input formula + for i, elem := range mix { + if elem.GetForm().ToString() == "P(b)" { + continue + } else if elem.GetForm().ToString() == "P(a)" { + continue + } else if elem.GetForm().ToString() == "P(f(X))" { + continue + } else { + t.Errorf("Expected unified form %d to be 'P(b) or P(a) or P(f(X))', got '%s'", i, elem.GetForm().ToString()) + } + } + }) + + t.Run("Unify_pggab_with_pxy", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pggab.(AST.Pred)) + + tree.Print() + found, mix := tree.Unify(pxy) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(g(g(a)), b)" { + t.Errorf("Expected unified form to be 'P(g(g(a)), b)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Exception_Unify_pa_with_pb", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + + // Constants 'a' and 'b' cannot unify + found, mix := tree.Unify(pb) + + if found { + t.Errorf("Unification should have failed for P(a) and P(b)") + } + if len(mix) != 0 { + t.Errorf("Expected empty result list, got %d elements", len(mix)) + } + }) + + t.Run("Exception_Unify_pxx_with_pab", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pxx.(AST.Pred)) // P(x, x) requires both arguments to be identical + + found, mix := tree.Unify(pab) // P(a, b) has different arguments + + if found { + t.Errorf("Unification should have failed: P(x, x) cannot unify with P(a, b)") + } + if len(mix) != 0 { + t.Errorf("Expected empty result list") + } + }) + + t.Run("Exception_Unify_pba_pab_with_pxx", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pba.(AST.Pred)) + tree = tree.Insert(pab.(AST.Pred)) + + // P(X, X) requires identical arguments, neither P(b, a) nor P(a, b) fits + found, mix := tree.Unify(pxx) + + if found { + t.Errorf("Unification should have failed: P(X, X) cannot unify with P(b, a) or P(a, b)") + } + if len(mix) != 0 { + t.Errorf("Expected empty result list") + } + }) + + t.Run("Exception_Unify_pab_with_pxx", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pab.(AST.Pred)) + + found, mix := tree.Unify(pxx) + + if found || len(mix) != 0 { + t.Errorf("Unification should have failed: P(a, b) cannot unify with P(X, X)") + } + }) +} + +func TestUnifyTerm(t *testing.T) { + + t.Run("UnifyTerm_pax_with_pay", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + queryTerm := subst.TransformPred(pay.(AST.Pred)) + + fmt.Println("Test1") + for _, elem := range queryTerm.GetSubTerms().GetSlice() { + fmt.Println("QueryTerm Element", elem.ToString()) + } + fmt.Println("Test2") + + val, mix := tree.UnifyTerm(queryTerm) + + fmt.Println(val) + + for _, elem := range mix { + fmt.Println("elem", elem.ToString()) + } + + if !val { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result, got %d", len(mix)) + } + }) + + t.Run("UnifyTerm_pax_with_pab", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + queryTerm := subst.TransformPred(pab.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if !val { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, got %d", len(mix)) + } + }) + + t.Run("UnifyTerm_pa_with_pa", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + queryTerm := subst.TransformPred(pa.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if !val { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, got %d", len(mix)) + } + if mix[0].ToString() != "P(a) {}" { + t.Errorf("Expected result 'P(a) {}', got '%s'", mix[0].ToString()) + } + }) + + t.Run("UnifyTerm_pab_with_pay", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pab.(AST.Pred)) + queryTerm := subst.TransformPred(pay.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(a, Y)" { + t.Errorf("Expected term to be 'P(a, Y)', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("UnifyTerm_pafx_with_pafy", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pafx.(AST.Pred)) + queryTerm := subst.TransformPred(pafy.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(a, f(Y))" { + t.Errorf("Expected term to be 'P(a, f(Y))', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("UnifyTerm_px_with_py", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(px.(AST.Pred)) + queryTerm := subst.TransformPred(py.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(Y)" { + t.Errorf("Expected term to be 'P(Y)', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("UnifyTerm_pxy_with_pab", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pxy.(AST.Pred)) + queryTerm := subst.TransformPred(pab.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(a, b)" { + t.Errorf("Expected term to be 'P(a, b)', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("UnifyTerm_Multiple_Inserts_with_py", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pb.(AST.Pred)) + tree = tree.Insert(pa.(AST.Pred)) + tree = tree.Insert(pfx.(AST.Pred)) + queryTerm := subst.TransformPred(py.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if !val { + t.Fatalf("Unification failed, expected success with matches") + } + if len(mix) != 3 { + t.Fatalf("Expected exactly 3 unification results, got %d", len(mix)) + } + for i, elem := range mix { + if elem.Term().ToString() != "P(Y)" { + t.Errorf("Expected unified term %d to be 'P(Y)', got '%s'", i, elem.Term().ToString()) + } + } + }) + + t.Run("UnifyTerm_pggab_with_pxy", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pggab.(AST.Pred)) + queryTerm := subst.TransformPred(pxy.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(X, Y)" { + t.Errorf("Expected term to be 'P(X, Y)', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("Exception_UnifyTerm_pa_with_pb", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + queryTerm := subst.TransformPred(pb.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if val { + t.Fatalf("Unification should have failed for P(a) and P(b)") + } + if len(mix) != 0 { + t.Fatalf("Expected 0 elements, got %d", len(mix)) + } + }) + + t.Run("Exception_UnifyTerm_pxx_with_pab", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pxx.(AST.Pred)) + queryTerm := subst.TransformPred(pab.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if val || len(mix) != 0 { + t.Fatalf("Unification should have failed: P(x,x) cannot unify with P(a,b)") + } + }) + + t.Run("Exception_UnifyTerm_pba_pab_with_pxx", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pba.(AST.Pred)) + tree = tree.Insert(pab.(AST.Pred)) + queryTerm := subst.TransformPred(pxx.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if val { + t.Fatalf("Unification should have failed: expected 0 elements, got %d", len(mix)) + } + }) + + t.Run("Exception_UnifyTerm_pab_with_pxx", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pab.(AST.Pred)) + queryTerm := subst.TransformPred(pxx.(AST.Pred)) + + val, mix := tree.UnifyTerm(queryTerm) + + if val { + t.Fatalf("Unification should have failed: expected 0 elements, got %d", len(mix)) + } + if len(mix) != 0 { + t.Fatalf("Expected result array to be empty, got %d elements", len(mix)) + } + }) +} + +func TestMakeDataStruct(t *testing.T) { + + t.Run("MakeDataStruct_Positive_Tree", func(t *testing.T) { + + tree1 := NewNode() + formulas1 := Lib.NewList[AST.Form]() + formulas1.Append(pab) // + => Inserted + formulas1.Append(not_pac) // - => Ignored + formulas1.Append(not_pba) // - => Ignored + formulas1.Append(pba) // + => Inserted + + actualTree1, ok := tree1.MakeDataStruct(formulas1, true).(*DiscriminationNode) + if !ok { + if directTree, okDirect := tree1.MakeDataStruct(formulas1, true).(DiscriminationNode); okDirect { + actualTree1 = &directTree + } else { + t.Fatalf("MakeDataStruct didn't return a valid DiscriminationNode type") + } + } + + rootChildren := actualTree1.getChildren().GetSlice() + if len(rootChildren) != 1 { + t.Fatalf("Expected exactly 1 predicate root node ('P'), got %d", len(rootChildren)) + } + + pNode := rootChildren[0] + if pNode.getSymbol().getSymbol().ToString() != "P" { + t.Errorf("Expected root node symbol to be 'P', got '%s'", pNode.getSymbol().getSymbol().ToString()) + } + + pChildren := pNode.getChildren().GetSlice() + pChildren2 := pChildren[0] + pChildren3 := pChildren2.getChildren().GetSlice() + + if len(pChildren3) != 1 { + t.Fatalf("Expected 'P' to have exactly 1 children ('b') from positive formulas, got %d", len(pChildren)) + } + + for _, child := range pChildren3 { + symStr := child.getSymbol().getSymbol().ToString() + if symStr == "c" { + t.Errorf("Negative formula 'not_pac' was incorrectly inserted into the positive tree") + } + } + }) + + t.Run("MakeDataStruct_Negative_Tree", func(t *testing.T) { + + tree2 := NewNode() + formulas2 := Lib.NewList[AST.Form]() + formulas2.Append(pab) // + => Ignored + formulas2.Append(not_pac) // - => Inserted + formulas2.Append(not_pba) // - => Inserted + formulas2.Append(pba) // + => Ignored + + actualTree2, ok := tree2.MakeDataStruct(formulas2, false).(*DiscriminationNode) + if !ok { + if directTree, okDirect := tree2.MakeDataStruct(formulas2, false).(DiscriminationNode); okDirect { + actualTree2 = &directTree + } else { + t.Fatalf("MakeDataStruct didn't return a valid DiscriminationNode type") + } + } + + actualTree2.Print() + + rootChildren := actualTree2.getChildren().GetSlice() + if len(rootChildren) != 1 { + t.Fatalf("Expected exactly 1 predicate root node ('P'), got %d", len(rootChildren)) + } + + pNode := rootChildren[0] + pChildren := pNode.getChildren().GetSlice() + if len(pChildren) == 0 { + t.Fatalf("Negative tree is empty, expected nodes from negative formulas") + } + }) +} + +func TestTrickyProblem(t *testing.T) { + + t.Run("Exception_Occur_Check_Cyclic", func(t *testing.T) { + tree := NewNode() + tree.Insert(pfx.(AST.Pred)) + val, mix := tree.Unify(px) + + if val { + t.Fatalf("Occur Check Faillure") + } + if len(mix) != 0 { + t.Fatalf("Occur Check Faillure") + } + }) + + t.Run("UnifyTerm_Complex_SkipTerm", func(t *testing.T) { + tree := NewNode() + tree.Insert(pfgaba.(AST.Pred)) + val, mix := tree.Unify(px) + + if val { + t.Fatalf("Occur Check Faillure") + } + if len(mix) != 0 { + t.Fatalf("Occur Check Faillure") + } + }) + + t.Run("Exception_Shared_Query_Variables", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pab.(AST.Pred)) + + queryTerm := subst.TransformPred(pxx.(AST.Pred)) + val, _ := tree.UnifyTerm(queryTerm) + + if val { + t.Fatalf("Unification should fail because X cannot be 'a' and 'b' simultaneously") + } + }) + +} + +func TestInsertCustomType(t *testing.T) { + + t.Run("Insert_typed_var", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(p_typed_pred_int_3) + tree.Print() + + t1 := tree.getChildren() + if t1.Len() != 1 { + t.Fatalf("Supposed to be P") + } + if t1.At(0).toString() != "p" { + t.Fatalf("Supposed to be p (predicat)") + } + + t2 := t1.At(0) + t3 := t2.getChildren() + if t3.Len() != 1 { + t.Fatalf("Supposed to be int") + } + + if t3.At(0).toString() != "int" { + t.Fatalf("Supposed to be type \"int \" ") + } + + t4 := t3.At(0) + t5 := t4.getChildren() + if t5.Len() != 1 { + t.Fatalf("Supposed to be int") + } + + if t5.At(0).toString() != "3" { + t.Fatalf("Supposed to be 3") + } + + }) + + t.Run("Insert_different_typed_var", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(p_typed_pred_int_2_int_3_a) + tree = tree.Insert(p_typed_pred_int_2_int_3_b) + tree = tree.Insert(p_typed_pred_int_x_y_z) + tree = tree.Insert(p_typed_pred_reel_x_y_z) + tree = tree.Insert(p_typed_pred_int_2_double_4_a) + + // 1. Root Level + rootChildren := tree.getChildren() + if rootChildren.Len() != 1 { + t.Fatalf("Expected root to have exactly 1 child, got %d", rootChildren.Len()) + } + pNode := rootChildren.At(0) + if pNode.toString() != "p" { + t.Fatalf("Expected 'p', got '%s'", pNode.toString()) + } + + // 2. Under 'p' -> 'int' and '$real' + pChildren := pNode.getChildren() + if pChildren.Len() != 2 { + t.Fatalf("Expected 'p' to have 2 children, got %d", pChildren.Len()) + } + + intNode := pChildren.At(0) + if intNode.toString() != "int" { + t.Fatalf("Expected first child of 'p' to be 'int', got '%s'", intNode.toString()) + } + + realNode := pChildren.At(1) + if realNode.toString() != "$real" { + t.Fatalf("Expected second child of 'p' to be '$real', got '%s'", realNode.toString()) + } + + // ----------------------------------------------------- + // 3. Under 'int' -> '2', 'v1', 'double' + // ----------------------------------------------------- + intChildren := intNode.getChildren() + if intChildren.Len() != 3 { + t.Fatalf("Expected 'int' to have 3 children ('2', 'v1', 'double'), got %d", intChildren.Len()) + } + + // Branch: int -> 2 -> 3 -> a/b + node2 := intChildren.At(0) + if node2.toString() != "2" { + t.Fatalf("Expected '2', got '%s'", node2.toString()) + } + node2Children := node2.getChildren() + if node2Children.Len() != 1 { + t.Fatalf("Expected '2' to have 1 child ('3'), got %d", node2Children.Len()) + } + node3 := node2Children.At(0) + if node3.toString() != "3" { + t.Fatalf("Expected '3', got '%s'", node3.toString()) + } + node3Children := node3.getChildren() + if node3Children.Len() != 2 { + t.Fatalf("Expected '3' to have 2 children ('a' and 'b'), got %d", node3Children.Len()) + } + if node3Children.At(0).toString() != "a" || node3Children.At(1).toString() != "b" { + t.Fatalf("Expected children of '3' to be 'a' and 'b'") + } + + // Branch: int -> v1 -> v2 -> v3 + nodeV1 := intChildren.At(1) + if nodeV1.toString() != "v1" { + t.Fatalf("Expected 'v1', got '%s'", nodeV1.toString()) + } + nodeV1Children := nodeV1.getChildren() + if nodeV1Children.Len() != 1 || nodeV1Children.At(0).toString() != "v2" { + t.Fatalf("Expected 'v1' to have child 'v2'") + } + nodeV2Children := nodeV1Children.At(0).getChildren() + if nodeV2Children.Len() != 1 || nodeV2Children.At(0).toString() != "v3" { + t.Fatalf("Expected 'v2' to have child 'v3'") + } + + // Branch: int -> double -> $i -> 2 -> 4 -> a + nodeDouble := intChildren.At(2) + if nodeDouble.toString() != "double" { + t.Fatalf("Expected 'double', got '%s'", nodeDouble.toString()) + } + nodeDoubleChildren := nodeDouble.getChildren() + if nodeDoubleChildren.Len() != 1 || nodeDoubleChildren.At(0).toString() != "$i" { + t.Fatalf("Expected 'double' to have child '$i'") + } + nodeIChildren := nodeDoubleChildren.At(0).getChildren() + if nodeIChildren.Len() != 1 || nodeIChildren.At(0).toString() != "2" { + t.Fatalf("Expected '$i' to have child '2'") + } + node2DoubleChildren := nodeIChildren.At(0).getChildren() + if node2DoubleChildren.Len() != 1 || node2DoubleChildren.At(0).toString() != "4" { + t.Fatalf("Expected '2' to have child '4'") + } + node4Children := node2DoubleChildren.At(0).getChildren() + if node4Children.Len() != 1 || node4Children.At(0).toString() != "a" { + t.Fatalf("Expected '4' to have child 'a'") + } + + // ----------------------------------------------------- + // 4. Under '$real' -> v1 -> v2 -> v3 + // ----------------------------------------------------- + realChildren := realNode.getChildren() + if realChildren.Len() != 1 { + t.Fatalf("Expected '$real' to have 1 child ('v1'), got %d", realChildren.Len()) + } + realV1 := realChildren.At(0) + if realV1.toString() != "v1" { + t.Fatalf("Expected 'v1' under '$real', got '%s'", realV1.toString()) + } + realV1Children := realV1.getChildren() + if realV1Children.Len() != 1 || realV1Children.At(0).toString() != "v2" { + t.Fatalf("Expected 'v1' to have child 'v2'") + } + realV2Children := realV1Children.At(0).getChildren() + if realV2Children.Len() != 1 || realV2Children.At(0).toString() != "v3" { + t.Fatalf("Expected 'v2' to have child 'v3'") + } + }) + + t.Run("Insert_different_typed_var", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(p_typed_pred_int_2_double_4_a) + tree = tree.Insert(p_typed_pred_int_2_double_4_b) + tree = tree.Insert(p_typed_pred_int_2_double_4_x) + + // 1. Root Level validation + rootChildren := tree.getChildren() + if rootChildren.Len() != 1 { + t.Fatalf("Expected root to have exactly 1 child, got %d", rootChildren.Len()) + } + pNode := rootChildren.At(0) + if pNode.toString() != "p" { + t.Fatalf("Expected node to be 'p', got '%s'", pNode.toString()) + } + + // 2. Under 'p' -> 'int' + pChildren := pNode.getChildren() + if pChildren.Len() != 1 { + t.Fatalf("Expected 'p' to have exactly 1 child, got %d", pChildren.Len()) + } + intNode := pChildren.At(0) + if intNode.toString() != "int" { + t.Fatalf("Expected node to be 'int', got '%s'", intNode.toString()) + } + + // 3. Under 'int' -> 'double' + intChildren := intNode.getChildren() + if intChildren.Len() != 1 { + t.Fatalf("Expected 'int' to have exactly 1 child, got %d", intChildren.Len()) + } + doubleNode := intChildren.At(0) + if doubleNode.toString() != "double" { + t.Fatalf("Expected node to be 'double', got '%s'", doubleNode.toString()) + } + + // 4. Under 'double' -> '$i' + doubleChildren := doubleNode.getChildren() + if doubleChildren.Len() != 1 { + t.Fatalf("Expected 'double' to have exactly 1 child, got %d", doubleChildren.Len()) + } + iNode := doubleChildren.At(0) + if iNode.toString() != "$i" { + t.Fatalf("Expected node to be '$i', got '%s'", iNode.toString()) + } + + // 5. Under '$i' -> '2' + iChildren := iNode.getChildren() + if iChildren.Len() != 1 { + t.Fatalf("Expected '$i' to have exactly 1 child, got %d", iChildren.Len()) + } + node2 := iChildren.At(0) + if node2.toString() != "2" { + t.Fatalf("Expected node to be '2', got '%s'", node2.toString()) + } + + // 6. Under '2' -> '4' + node2Children := node2.getChildren() + if node2Children.Len() != 1 { + t.Fatalf("Expected '2' to have exactly 1 child, got %d", node2Children.Len()) + } + node4 := node2Children.At(0) + if node4.toString() != "4" { + t.Fatalf("Expected node to be '4', got '%s'", node4.toString()) + } + + // 7. Under '4' -> Forks into 'a', 'b', and 'v1' + node4Children := node4.getChildren() + if node4Children.Len() != 3 { + t.Fatalf("Expected '4' to have exactly 3 children ('a', 'b', 'v1'), got %d", node4Children.Len()) + } + + if node4Children.At(0).toString() != "a" { + t.Fatalf("Expected first child of '4' to be 'a', got '%s'", node4Children.At(0).toString()) + } + + if node4Children.At(1).toString() != "b" { + t.Fatalf("Expected second child of '4' to be 'b', got '%s'", node4Children.At(1).toString()) + } + + if node4Children.At(2).toString() != "v1" { + t.Fatalf("Expected third child of '4' to be 'v1', got '%s'", node4Children.At(2).toString()) + } + + }) +} + +func TestRetrieveCustomType(t *testing.T) { + + t.Run("Retrieve_same_typed_var", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(p_typed_pred_int_2_double_4_a) + tree.Print() + a := tree.RetrieveUnifiables(p_typed_pred_int_2_double_4_x) + + if len(a) != 1 { + t.Fatalf("Should be able to Unify") + } + + for _, elem := range a { + fmt.Println("elem", elem.toString()) + } + + }) + + t.Run("Retrieve_different_typed_var", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(p_typed_pred_int_2_double_4_a) + tree.Print() + a := tree.RetrieveUnifiables(p_typed_pred_int_2_double_4_b) + + if len(a) != 0 { + t.Fatalf("Shouldn't be able to Unify") + } + + }) + +} + +func TestSymbolTypeGetters(t *testing.T) { + + symWithTerm := makeSymbolType(TermNode{Term: a}, 1) + symWithTy := makeSymbolTypeTy(TyNode{Ty: AST.TInt()}) + symWithString := makeSymbolType(NodeString("test_string"), 0) + + t.Run("Test_getTerm_term", func(t *testing.T) { + + gotTerm := symWithTerm.getTerm() + if gotTerm == nil { + t.Fatalf("getTerm() failed: expected a term, got nil") + } + if gotTerm.ToString() != a.ToString() { + t.Errorf("getTerm() failed: expected %s, got %s", a.ToString(), gotTerm.ToString()) + } + }) + + t.Run("Test_getTerm_ty", func(t *testing.T) { + + gotTermFromTy := symWithTy.getTerm() + if gotTermFromTy != nil { + t.Errorf("getTerm() from TyNode failed: expected nil, got %v", gotTermFromTy) + } + + }) + + t.Run("Test_getTerm_term", func(t *testing.T) { + + gotTermFromString := symWithString.getTerm() + if gotTermFromString != nil { + t.Errorf("getTerm() from NodeString failed: expected nil, got %v", gotTermFromString) + } + }) + + t.Run("Test_GetTy_type", func(t *testing.T) { + + gotTy := symWithTy.GetTy() + if gotTy == nil { + t.Fatalf("GetTy() failed: expected a type, got nil") + } + if gotTy.ToString() != AST.TInt().ToString() { + t.Errorf("GetTy() failed: expected %s, got %s", AST.TInt().ToString(), gotTy.ToString()) + } + + }) + + t.Run("Test_GetTy_term", func(t *testing.T) { + + gotTyFromTerm := symWithTerm.GetTy() + if gotTyFromTerm != nil { + t.Errorf("GetTy() from TermNode failed: expected nil, got %v", gotTyFromTerm) + } + + }) + + t.Run("Test_GetTy_string", func(t *testing.T) { + + gotTyFromString := symWithString.GetTy() + if gotTyFromString != nil { + t.Errorf("GetTy() from NodeString failed: expected nil, got %v", gotTyFromString) + } + }) +} + +func TestNodeStringMethods(t *testing.T) { + ns1 := NodeString("testString") + ns1Upper := NodeString("TESTSTRING") + ns2 := NodeString("otherString") + otherNode := TermNode{Term: a} + + t.Run("IsMeta", func(t *testing.T) { + if ns1.IsMeta() { + t.Fatalf("NodeString should never be a meta variable") + } + }) + + t.Run("Equals_Same_And_Case_Insensitive", func(t *testing.T) { + if !ns1.Equals(ns1) { + t.Errorf("Should be equal to itself") + } + if !ns1.Equals(ns1Upper) { + t.Errorf("Should be equal due to case insensitivity") + } + }) + + t.Run("Equals_Different_Values_And_Types", func(t *testing.T) { + if ns1.Equals(ns2) { + t.Errorf("Should not be equal to a different string") + } + if ns1.Equals(otherNode) { + t.Errorf("Should not be equal to a different NodeElement type") + } + }) +} + +func TestTermNodeMethods(t *testing.T) { + tnRegular := TermNode{Term: a} + tnMeta := TermNode{Term: x} + tnDifferent := TermNode{Term: b} + tnNil := TermNode{Term: nil} + + t.Run("IsMeta", func(t *testing.T) { + if tnRegular.IsMeta() { + t.Errorf("Regular term shouldn't be meta") + } + if !tnMeta.IsMeta() { + t.Errorf("Meta term should be recognized as meta") + } + }) + + t.Run("Equals", func(t *testing.T) { + if !tnRegular.Equals(tnRegular) { + t.Errorf("Identical TermNodes should be equal") + } + if tnRegular.Equals(tnDifferent) { + t.Errorf("Different TermNodes shouldn't be equal") + } + if tnRegular.Equals(tnNil) || tnNil.Equals(tnRegular) { + t.Errorf("Comparison with a nil term should be false") + } + }) +} + +func TestTyNodeMethods(t *testing.T) { + // Variables declared at the top using global variables 'x' and 'random_type' + tnStandard := TyNode{Ty: AST.TIndividual()} + tnDifferent := TyNode{Ty: random_type} + tnNil := TyNode{Ty: nil} + + t.Run("Equals", func(t *testing.T) { + if !tnStandard.Equals(tnStandard) { + t.Errorf("Identical TyNodes should be equal") + } + if tnStandard.Equals(tnDifferent) { + t.Errorf("Different TyNodes shouldn't be equal") + } + if tnStandard.Equals(tnNil) || tnNil.Equals(tnStandard) { + t.Errorf("Comparison with a nil type should be false") + } + }) +} + +func TestUnify2(t *testing.T) { + + t.Run("Unify2_pax_with_pay", func(t *testing.T) { + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + + found, mix := tree.Unify2(pay) + + if !found { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result, got %d", len(mix)) + } + if mix[0].GetForm().ToString() != "P(a, X)" { + t.Errorf("Expected unified form to be 'P(a, X)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify2_pax_with_pab", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + found, mix := tree.Unify2(pab) + + if !found { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result, got %d", len(mix)) + } + if mix[0].GetForm().ToString() != "P(a, X)" { + t.Errorf("Expected unified form to be 'P(a, X)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify2_pa_with_pa", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + found, mix := tree.Unify2(pa) + + if !found { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result, got %d", len(mix)) + } + if mix[0].GetForm().ToString() != "P(a)" { + t.Errorf("Expected unified form to be 'P(a)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify2_pax_with_pafy", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + found, mix := tree.Unify2(pafy) + + for _, elem := range mix { + fmt.Println("elem", elem.ToString()) + } + fmt.Println("len(elem)", len(mix)) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(a, X)" { + t.Errorf("Expected unified form to be 'P(a, X)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify2_pafx_with_pafy", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pafx.(AST.Pred)) + found, mix := tree.Unify2(pafy) + + tree.Print() + fmt.Println("pafy", pafy.ToString()) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(a, f(X))" { + t.Errorf("Expected unified form to be 'P(a, f(X))', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify2_px_with_py", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(px.(AST.Pred)) + found, mix := tree.Unify2(py) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(X)" { + t.Errorf("Expected unified form to be 'P(X)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify2_pxy_with_pab", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pxy.(AST.Pred)) + found, mix := tree.Unify2(pab) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(X, Y)" { + t.Errorf("Expected unified form to be 'P(X, Y)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Unify2_Multiple_Inserts_with_py", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pb.(AST.Pred)) + tree = tree.Insert(pa.(AST.Pred)) + tree = tree.Insert(pfx.(AST.Pred)) + found, mix := tree.Unify2(py) + + if !found || len(mix) != 3 { + t.Fatalf("Expected exactly 3 unification results, got %d", len(mix)) + } + + for i, elem := range mix { + str := elem.GetForm().ToString() + if str != "P(a)" && str != "P(b)" && str != "P(f(X))" { + t.Errorf("Expected unified form %d to be 'P(a) or P(b) or P(f(X))', got '%s'", i, elem.GetForm().ToString()) + } + } + }) + + t.Run("Unify2_pggab_with_pxy", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pggab.(AST.Pred)) + found, mix := tree.Unify2(pxy) + + if !found || len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result") + } + if mix[0].GetForm().ToString() != "P(g(g(a)), b)" { + t.Errorf("Expected unified form to be ''P(g(g(a)), b)', got '%s'", mix[0].GetForm().ToString()) + } + }) + + t.Run("Exception_Unify2_pa_with_pb", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + found, mix := tree.Unify2(pb) + + if found { + t.Errorf("Unification should have failed for P(a) and P(b)") + } + if len(mix) != 0 { + t.Errorf("Expected empty result list, got %d elements", len(mix)) + } + }) + + t.Run("Exception_Unify2_pxx_with_pab", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pxx.(AST.Pred)) + found, mix := tree.Unify2(pab) + + if found { + t.Errorf("Unification should have failed: P(x, x) cannot unify with P(a, b)") + } + if len(mix) != 0 { + t.Errorf("Expected empty result list") + } + }) + + t.Run("Exception_Unify2_pba_pab_with_pxx", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pba.(AST.Pred)) + tree = tree.Insert(pab.(AST.Pred)) + found, mix := tree.Unify2(pxx) + + if found { + t.Errorf("Unification should have failed: P(X, X) cannot unify with P(b, a) or P(a, b)") + } + if len(mix) != 0 { + t.Errorf("Expected empty result list") + } + }) + + t.Run("Exception_Unify2_pab_with_pxx", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pab.(AST.Pred)) + found, mix := tree.Unify2(pxx) + + if found || len(mix) != 0 { + t.Errorf("Unification should have failed: P(a, b) cannot unify with P(X, X)") + } + }) +} + +func TestUnifyTerm2(t *testing.T) { + + t.Run("UnifyTerm2_pax_with_pay", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + queryTerm := subst.TransformPred(pay.(AST.Pred)) + + tree.Print() + fmt.Println(queryTerm.ToString()) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 unification result, got %d", len(mix)) + } + }) + + t.Run("UnifyTerm2_pax_with_pab", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pax.(AST.Pred)) + queryTerm := subst.TransformPred(pab.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, got %d", len(mix)) + } + }) + + t.Run("UnifyTerm2_pa_with_pa", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + queryTerm := subst.TransformPred(pa.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val { + t.Fatalf("Unification failed, expected success") + } + if len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, got %d", len(mix)) + } + if mix[0].ToString() != "P(a) {}" { + t.Errorf("Expected result 'P(a) {}', got '%s'", mix[0].ToString()) + } + }) + + t.Run("UnifyTerm2_pab_with_pay", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pab.(AST.Pred)) + queryTerm := subst.TransformPred(pay.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(a, Y)" { + t.Errorf("Expected term to be 'P(a, Y)', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("UnifyTerm2_pafx_with_pafy", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pafx.(AST.Pred)) + queryTerm := subst.TransformPred(pafy.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(a, f(Y))" { + t.Errorf("Expected term to be 'P(a, f(Y))', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("UnifyTerm2_px_with_py", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(px.(AST.Pred)) + queryTerm := subst.TransformPred(py.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(Y)" { + t.Errorf("Expected term to be 'P(Y)', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("UnifyTerm2_pxy_with_pab", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pxy.(AST.Pred)) + queryTerm := subst.TransformPred(pab.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(a, b)" { + t.Errorf("Expected term to be 'P(a, b)', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("UnifyTerm2_Multiple_Inserts_with_py", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pb.(AST.Pred)) + tree = tree.Insert(pa.(AST.Pred)) + tree = tree.Insert(pfx.(AST.Pred)) + queryTerm := subst.TransformPred(py.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val { + t.Fatalf("Unification failed, expected success with matches") + } + if len(mix) != 3 { + t.Fatalf("Expected exactly 3 unification results, got %d", len(mix)) + } + for i, elem := range mix { + if elem.Term().ToString() != "P(Y)" { + t.Errorf("Expected unified term %d to be 'P(Y)', got '%s'", i, elem.Term().ToString()) + } + } + }) + + t.Run("UnifyTerm2_pggab_with_pxy", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pggab.(AST.Pred)) + queryTerm := subst.TransformPred(pxy.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if !val || len(mix) != 1 { + t.Fatalf("Expected exactly 1 result, found valid=%t, len=%d", val, len(mix)) + } + if mix[0].Term().ToString() != "P(X, Y)" { + t.Errorf("Expected term to be 'P(X, Y)', got '%s'", mix[0].Term().ToString()) + } + }) + + t.Run("Exception_UnifyTerm2_pa_with_pb", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pa.(AST.Pred)) + queryTerm := subst.TransformPred(pb.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if val { + t.Fatalf("Unification should have failed for P(a) and P(b)") + } + if len(mix) != 0 { + t.Fatalf("Expected 0 elements, got %d", len(mix)) + } + }) + + t.Run("Exception_UnifyTerm2_pxx_with_pab", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pxx.(AST.Pred)) + queryTerm := subst.TransformPred(pab.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if val || len(mix) != 0 { + t.Fatalf("Unification should have failed: P(x,x) cannot unify with P(a,b)") + } + }) + + t.Run("Exception_UnifyTerm2_pba_pab_with_pxx", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pba.(AST.Pred)) + tree = tree.Insert(pab.(AST.Pred)) + queryTerm := subst.TransformPred(pxx.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if val { + t.Fatalf("Unification should have failed: expected 0 elements, got %d", len(mix)) + } + }) + + t.Run("Exception_UnifyTerm2_pab_with_pxx", func(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pab.(AST.Pred)) + queryTerm := subst.TransformPred(pxx.(AST.Pred)) + + val, mix := tree.UnifyTerm2(queryTerm) + + if val { + t.Fatalf("Unification should have failed: expected 0 elements, got %d", len(mix)) + } + if len(mix) != 0 { + t.Fatalf("Expected result array to be empty, got %d elements", len(mix)) + } + }) +} + +func TestReconstructTerm(t *testing.T) { + ctx := NewContext() + + t.Run("Reconstruct_Constant", func(t *testing.T) { + seq := parseTerm(a, ctx).GetSlice() + term, remaining := ReconstructTerm(seq) + + if term == nil { + t.Fatalf("Expected to reconstruct a term, got nil") + } + if term.ToString() != "a" { + t.Errorf("Expected term 'a', got '%s'", term.ToString()) + } + if len(remaining) != 0 { + t.Errorf("Expected remaining sequence to be empty, got %d elements", len(remaining)) + } + }) + + t.Run("Reconstruct_Function_fxy", func(t *testing.T) { + seq := parseTerm(fxy, ctx).GetSlice() + term, remaining := ReconstructTerm(seq) + + if term == nil { + t.Fatalf("Expected to reconstruct a term, got nil") + } + if term.ToString() != "f(v1, v2)" { // v1 and v2 due to parseTerm mapping + t.Errorf("Expected reconstructed term 'f(v1, v2)', got '%s'", term.ToString()) + } + if len(remaining) != 0 { + t.Errorf("Expected remaining sequence to be empty") + } + }) + + t.Run("Reconstruct_Nested_Subsequence", func(t *testing.T) { + // If we only pass a slice of the sequence, it should reconstruct just that part + // e.g., for f(a, b), seq is [f, a, b]. If we pass seq[1:], it should reconstruct 'a' and leave [b] + seq := parseTerm(fab, ctx).GetSlice() + + subSeq := seq[1:] // [a, b] + term, remaining := ReconstructTerm(subSeq) + + if term == nil || term.ToString() != "a" { + t.Fatalf("Expected to reconstruct term 'a'") + } + if len(remaining) != 1 { + t.Fatalf("Expected exactly 1 remaining element, got %d", len(remaining)) + } + if remaining[0].getSymbol().ToString() != "b" { + t.Errorf("Expected remaining element to be 'b', got '%s'", remaining[0].getSymbol().ToString()) + } + }) +} + +func TestA(t *testing.T) { + + tree := NewNode() + tree = tree.Insert(pfx.(AST.Pred)) + a, b := tree.Unify(px) + if a { + for _, elem := range b { + fmt.Println("a1", elem.ToString()) + } + } + tree.Print() + + tree2 := NewNode() + tree2 = tree2.Insert(pfx.(AST.Pred)) + a2, b2 := tree2.Unify(py) + if a2 { + for _, elem := range b2 { + fmt.Println("a2", elem.ToString()) + } + } + tree2.Print() + + tree3 := NewNode() + tree3 = tree3.Insert(py.(AST.Pred)) + tree3 = tree3.Insert(px.(AST.Pred)) + a3, b3 := tree3.Unify(pfx) + if a3 { + for _, elem := range b3 { + fmt.Println("a3", elem.ToString()) + } + } + tree3.Print() + +} diff --git a/src/Unif/substitution/data_structure.go b/src/Unif/substitution/data_structure.go new file mode 100644 index 00000000..81f17ef7 --- /dev/null +++ b/src/Unif/substitution/data_structure.go @@ -0,0 +1,220 @@ +/** +* Copyright 2022 by the authors (see AUTHORS). +* +* Goéland is an automated theorem prover for first order logic. +* +* This software is governed by the CeCILL license under French law and +* abiding by the rules of distribution of free software. You can use, +* modify and/ or redistribute the software under the terms of the CeCILL +* license as circulated by CEA, CNRS and INRIA at the following URL +* "http://www.cecill.info". +* +* As a counterpart to the access to the source code and rights to copy, +* modify and redistribute granted by the license, users are provided only +* with a limited warranty and the software's author, the holder of the +* economic rights, and the successive licensors have only limited +* liability. +* +* In this respect, the user's attention is drawn to the risks associated +* with loading, using, modifying and/or developing or reproducing the +* software by the user in light of its specific status of free software, +* that may mean that it is complicated to manipulate, and that also +* therefore means that it is reserved for developers and experienced +* professionals having in-depth computer knowledge. Users are therefore +* encouraged to load and test the software's suitability as regards their +* requirements in conditions enabling the security of their systems and/or +* data to be ensured and, more generally, to use and operate it in the +* same conditions as regards security. +* +* The fact that you are presently reading this means that you have had +* knowledge of the CeCILL license and that you accept its terms. +**/ + +/** +* This file contains functions and types which describe the formula's data + structure +**/ + +package subst + +import ( + "fmt" + + "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" + "github.com/GoelandProver/Goeland/Lib" +) + +type DataStructure interface { + Print() + IsEmpty() bool + Copy() DataStructure + MakeDataStruct(Lib.List[AST.Form], bool) DataStructure + InsertFormulaListToDataStructure(Lib.List[AST.Form]) DataStructure + + Unify(AST.Form) (bool, []MixedSubstitutions) + UnifyTerm(AST.Term) (bool, []MixedTermSubstitutions) + // FIXME: + // When the unification gets reworked, think a bit more about the exposed interface. + // We want to index on _terms_ while keeping the ability to unify _predicates_. + // (we can easily coerce a predicate to a function) + // We probably want to expose two functions --- one to unify predicates, and the other + // one to unify terms. But maybe we should say that unifying predicates is the "weird" + // case instead of the other way around. + // + // We should also find a more explicit name over `DataStructure`... -> term indexing structure? UnificationStructure +} + +func TransformPred(p AST.Pred) AST.Term { + return TransformTerm(AST.MakerFun(p.GetID(), p.GetTyArgs(), p.GetArgs())) +} + +func TransformTerm(t AST.Term) AST.Term { + switch term := t.(type) { + case AST.Id, AST.Meta, AST.Var: + return t + case AST.Fun: + args := Lib.ListMap(term.GetTyArgs(), AST.TyToTerm) + args.Append(Lib.ListMap(term.GetArgs(), TransformTerm).GetSlice()...) + return AST.MakerFun( + term.GetID(), + Lib.NewList[AST.Ty](), + args, + ) + } + + Glob.Anomaly("unif parsing", "Unknown term") + return nil +} + +/* Merge two valid substitutions */ +func MergeSubstitutions(s1, s2 Substitutions) (Substitutions, bool) { + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Merge substitution : %v and %v", + s1.ToString(), + s2.ToString()) + }), + ) + res := Substitutions{} + same_key := false + + if s1.IsEmpty() { + return s2, false + } + + if s2.IsEmpty() { + return s1, false + } + + for _, subst := range s1 { + res.Set(subst.Get()) + } + + for _, subst := range s2 { + s2_k, s2_v := subst.Get() + if HasSubst(res, s2_k) { + same_key = true + res = AddUnification(s2_k.Copy(), s2_v.Copy(), res.Copy()) + } else { + res.Set(s2_k.ToMeta(), s2_v) + EliminateMeta(&res) + Eliminate(&res) + } + + } + return res, same_key +} + +// robinsonUnify implements Robinson's structural unification algorithm on +// Goeland's term representation. It extends the substitution s in place, +// threading it through recursive calls, and returns Failure() on any clash. +// +// Steps: +// 1. Walk both terms through s to their current representative. +// 2. If they are already identical → nothing to do, return s. +// 3. Meta on either side → occur-check, then bind and propagate via Eliminate. +// 4. Fun / Fun with the same head and arity → recurse on each argument pair. +// 5. Any other combination (different heads, different arities, Var, …) → Failure. +func robinsonUnify(term1, term2 AST.Term, s Substitutions) Substitutions { + term1 = walkSubst(term1, s) + term2 = walkSubst(term2, s) + + if term1.Equals(term2) { + return s + } + + switch t1 := term1.(type) { + case AST.Meta: + if !OccurCheckValid(t1, term2) { + return Failure() + } + s.Set(t1, term2) + EliminateMeta(&s) + Eliminate(&s) + return s + + case AST.Fun: + switch t2 := term2.(type) { + case AST.Meta: + if !OccurCheckValid(t2, term1) { + return Failure() + } + s.Set(t2, term1) + EliminateMeta(&s) + Eliminate(&s) + return s + + case AST.Fun: + if !t1.GetID().Equals(t2.GetID()) { + return Failure() + } + args1 := t1.GetArgs() + args2 := t2.GetArgs() + if args1.Len() != args2.Len() { + return Failure() + } + for i := range args1.GetSlice() { + s = robinsonUnify(args1.At(i).Copy(), args2.At(i).Copy(), s) + if s.Equals(Failure()) { + return Failure() + } + } + return s + + default: + return Failure() + } + + default: + // Var or any other term kind: not expected after Skolemisation. + return Failure() + } +} + +// walkSubst chases meta-variable bindings in s until reaching an unbound +// meta or a non-meta term. +func walkSubst(t AST.Term, s Substitutions) AST.Term { + for t.IsMeta() { + val, idx := s.Get(t.ToMeta()) + if idx == -1 { + break + } + t = val + } + return t +} + +func AddUnification(term1, term2 AST.Term, subst Substitutions) Substitutions { + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Add unification : %v and %v to %v", + term1.ToString(), + term2.ToString(), + subst.ToString()) + }), + ) + return robinsonUnify(term1.Copy(), term2.Copy(), subst.Copy()) +} diff --git a/src/Unif/matching_substitutions.go b/src/Unif/substitution/matching_substitutions.go similarity index 75% rename from src/Unif/matching_substitutions.go rename to src/Unif/substitution/matching_substitutions.go index 7ed91cb5..6e318969 100644 --- a/src/Unif/matching_substitutions.go +++ b/src/Unif/substitution/matching_substitutions.go @@ -34,7 +34,7 @@ * This file provides the necessary structures to manipulate matching substitutions **/ -package Unif +package subst import ( "fmt" @@ -106,11 +106,12 @@ func translateTermRec(term AST.Term) AST.Term { opt_ty := Typing.QueryGlobalEnv(trm.GetName()) switch ty := opt_ty.(type) { case Lib.Some[AST.Ty]: - switch t := ty.Val.(type) { - case AST.TyPi: - for i := 0; i < t.VarsLen(); i++ { - ty_args.Append(AST.TermToTy(trm.GetArgs().At(i))) - } + t := ty.Val + i := 0 + for Glob.Is[AST.TyPi](t) { + ty_args.Append(AST.TermToTy(trm.GetArgs().At(i))) + t = t.(AST.TyPi).Ty() + i += 1 } } args := trm.GetArgs() @@ -192,6 +193,19 @@ type MixedSubstitutions struct { substs []MixedSubstitution } +// Build a MixedSubstitutions directly from a form and an already-mixed +// (term + type) substitution list. Use this instead of routing through +// MakeMatchingSubstitutions(form, ToSubstitutions(substs)).ToMixed(): that +// path forces the list through Substitutions (term-only) first, which +// silently drops any TySubstitution entries (ToSubstitutions has no case +// for them, and Substitutions itself has no way to represent one). That +// silent drop is what caused type metavariable bindings (e.g. for a +// polymorphic type parameter resolved via GAMMA + CLOSURE) to vanish +// before ever reaching the final proof-printing substitution. +func MakeMixedSubstitutions(form AST.Form, substs Lib.List[MixedSubstitution]) MixedSubstitutions { + return MixedSubstitutions{form.Copy(), Lib.ListCpy(substs).GetSlice()} +} + func (m MixedSubstitutions) GetForm() AST.Form { return m.form.Copy() } @@ -252,7 +266,7 @@ func (m MatchingSubstitutions) Print() { m.GetSubst().Print() } -func (m MatchingSubstitutions) toMixed() MixedSubstitutions { +func (m MatchingSubstitutions) ToMixed() MixedSubstitutions { substs := []MixedSubstitution{} for _, subst := range m.subst { substs = append(substs, translateFromSubst(subst)) @@ -268,6 +282,56 @@ func (m MixedSubstitutions) MatchingSubstitutions() MatchingSubstitutions { return MakeMatchingSubstitutions(m.form, m.GetTrmSubsts()) } +type MixMatchSubstitutions struct { + Tof Lib.Either[AST.Term, AST.Form] + Subst Substitutions +} + +// Pre-requisite: only formulas in the tof +func (s MixMatchSubstitutions) toMatching() MatchingSubstitutions { + switch tof := s.Tof.(type) { + case Lib.Left[AST.Term, AST.Form]: + Glob.Anomaly("unification", "expected unification between formulas, got unification between terms") + case Lib.Right[AST.Term, AST.Form]: + return MakeMatchingSubstitutions(tof.Val, s.Subst) + } + + Glob.Anomaly("unification", "reached an unreachable case") + return MakeMatchingSubstitutions(AST.MakerTop(), MakeEmptySubstitution()) +} + +func (s MixMatchSubstitutions) ToMixed() MixedSubstitutions { + return s.toMatching().ToMixed() +} + +type MixedTermSubstitutions struct { + term AST.Term + substs []MixedSubstitution +} + +func (s MixedTermSubstitutions) Term() AST.Term { return s.term } + +func (s MixedTermSubstitutions) ToString() string { + substs_list := Lib.MkListV(s.substs...) + return s.term.ToString() + " {" + Lib.ListToString(substs_list, Lib.WithEmpty("")) + "}" +} + +func (s MixMatchSubstitutions) ToMixedTerm() MixedTermSubstitutions { + switch tof := s.Tof.(type) { + case Lib.Left[AST.Term, AST.Form]: + substs := []MixedSubstitution{} + for _, subst := range s.Subst { + substs = append(substs, translateFromSubst(subst)) + } + return MixedTermSubstitutions{tof.Val, substs} + case Lib.Right[AST.Term, AST.Form]: + Glob.Anomaly("unification", "expected unification between terms, got unification between formulas") + } + + Glob.Anomaly("unification", "reached an unreachable case") + return MixedTermSubstitutions{nil, []MixedSubstitution{}} +} + func translateToSubst(subst MixedSubstitution) Substitution { switch s := subst.s.(type) { case Lib.Left[TySubstitution, Substitution]: @@ -283,7 +347,9 @@ func translateToSubst(subst MixedSubstitution) Substitution { return MakeSubstitution(AST.MakeEmptyMeta(), nil) } -func MergeMixedSubstitutions(substs1, substs2 Lib.List[MixedSubstitution]) (Lib.List[MixedSubstitution], bool) { +func MergeMixedSubstitutions( + substs1, substs2 Lib.List[MixedSubstitution], +) (Lib.List[MixedSubstitution], bool) { translated_substs1 := Lib.ListMap(substs1, translateToSubst).GetSlice() translated_substs2 := Lib.ListMap(substs2, translateToSubst).GetSlice() diff --git a/src/Unif/subst_pair.go b/src/Unif/substitution/subst_pair.go similarity index 99% rename from src/Unif/subst_pair.go rename to src/Unif/substitution/subst_pair.go index 6e886564..b8d6f3c1 100644 --- a/src/Unif/subst_pair.go +++ b/src/Unif/substitution/subst_pair.go @@ -34,7 +34,7 @@ * This file provides the necessary structures to manipulate pairs of substitutions. **/ -package Unif +package subst import ( "strconv" diff --git a/src/Unif/substitution.go b/src/Unif/substitution/substitution.go similarity index 94% rename from src/Unif/substitution.go rename to src/Unif/substitution/substitution.go index 0d930699..85c9dcc8 100644 --- a/src/Unif/substitution.go +++ b/src/Unif/substitution/substitution.go @@ -34,12 +34,19 @@ * This file provides the necessary structures to manipulate sustitutions **/ -package Unif +package subst import ( "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" ) +var debug Glob.Debugger + +func InitDebugger() { + debug = Glob.CreateDebugger("Subst") +} + type Substitution struct { k AST.Meta v AST.Term diff --git a/src/Unif/substitutions_type.go b/src/Unif/substitution/substitutions_type.go similarity index 99% rename from src/Unif/substitutions_type.go rename to src/Unif/substitution/substitutions_type.go index 7c43b118..9c93ae3b 100644 --- a/src/Unif/substitutions_type.go +++ b/src/Unif/substitution/substitutions_type.go @@ -34,7 +34,7 @@ * This file provides the necessary structures to manipulate sustitutions **/ -package Unif +package subst import ( "fmt" diff --git a/src/Unif/substitutions_tree.go b/src/Unif/substitutions_tree.go deleted file mode 100644 index 5a9be9e7..00000000 --- a/src/Unif/substitutions_tree.go +++ /dev/null @@ -1,287 +0,0 @@ -/** -* Copyright 2022 by the authors (see AUTHORS). -* -* Goéland is an automated theorem prover for first order logic. -* -* This software is governed by the CeCILL license under French law and -* abiding by the rules of distribution of free software. You can use, -* modify and/ or redistribute the software under the terms of the CeCILL -* license as circulated by CEA, CNRS and INRIA at the following URL -* "http://www.cecill.info". -* -* As a counterpart to the access to the source code and rights to copy, -* modify and redistribute granted by the license, users are provided only -* with a limited warranty and the software's author, the holder of the -* economic rights, and the successive licensors have only limited -* liability. -* -* In this respect, the user's attention is drawn to the risks associated -* with loading, using, modifying and/or developing or reproducing the -* software by the user in light of its specific status of free software, -* that may mean that it is complicated to manipulate, and that also -* therefore means that it is reserved for developers and experienced -* professionals having in-depth computer knowledge. Users are therefore -* encouraged to load and test the software's suitability as regards their -* requirements in conditions enabling the security of their systems and/or -* data to be ensured and, more generally, to use and operate it in the -* same conditions as regards security. -* -* The fact that you are presently reading this means that you have had -* knowledge of the CeCILL license and that you accept its terms. -**/ - -/** -* This file contains the functions needed to subtitute all the meta-variables of a subtitution map. -**/ - -package Unif - -import ( - "fmt" - - "github.com/GoelandProver/Goeland/AST" - "github.com/GoelandProver/Goeland/Lib" -) - -/* Takes each meta of the formula, matches the index to the metas, and add everything to subst */ -/* -* Subs : (int, term) : (index in tree, term in formula) -* MetaToSubs : (meta, term) : meta in formula, term in tree -* Merge both of them -**/ -func computeSubstitutions(subs []SubstPair, metasToSubs Substitutions, form AST.Form) Substitutions { - debug( - Lib.MkLazy(func() string { - return fmt.Sprintf( - "Compute substitution : %v and %v", - SubstPairListToString(subs), metasToSubs.ToString()) - }), - ) - metasFromTreeForm := Lib.NewList[AST.Meta]() - treeSubs := Substitutions{} - - // Retrieve all the meta of from the tree formula - switch typedForm := form.(type) { - case AST.Pred: - trms := getFunctionalArguments(typedForm.GetTyArgs(), typedForm.GetArgs()) - for _, trm := range trms.GetSlice() { - metasFromTreeForm.Append(trm.GetMetaList().GetSlice()...) - } - case TermForm: - metasFromTreeForm.Append(typedForm.GetTerm().GetMetaList().GetSlice()...) - default: - return Failure() - } - - // Transform subst tree into a real substitution - for _, value := range subs { - currentMeta := metasFromTreeForm.At(value.GetIndex()) - currentValue := value.GetTerm() - debug( - Lib.MkLazy(func() string { - return fmt.Sprintf( - "Iterate on subst : %v and %v", - currentMeta.ToString(), - currentValue.ToString()) - }), - ) - - if !currentMeta.Equals(currentValue) { - // Si current_meta a déjà une association dans metas - metaGet, index := metasToSubs.Get(currentMeta) - if HasSubst(metasToSubs, currentMeta) && (index != -1) && !currentValue.Equals(metaGet) { - // On cherche a unifier les deux valeurs - treeSubs.Set(currentMeta, currentValue) - new_unif := AddUnification(currentValue.Copy(), metaGet.Copy(), treeSubs.Copy()) - if new_unif.Equals(Failure()) { - return Failure() - } else { - treeSubs = new_unif - metasToSubs.Remove(index) // Remove from meta - } - } else { // Ne pas ajouter la susbtitution égalité - treeSubs.Set(currentMeta, currentValue) - } - } - } - - debug( - Lib.MkLazy(func() string { return fmt.Sprintf("before meta : %v", metasToSubs.ToString()) }), - ) - // Metas_subst eliminate - EliminateMeta(&metasToSubs) - Eliminate(&metasToSubs) - if metasToSubs.Equals(Failure()) { - return Failure() - } - debug(Lib.MkLazy(func() string { return fmt.Sprintf("After meta : %v", metasToSubs.ToString()) })) - - debug( - Lib.MkLazy(func() string { return fmt.Sprintf("before tree_subst : %v", treeSubs.ToString()) }), - ) - // Tree subst elminate - EliminateMeta(&treeSubs) - Eliminate(&treeSubs) - if treeSubs.Equals(Failure()) { - return Failure() - } - debug( - Lib.MkLazy(func() string { return fmt.Sprintf("after tree_subst : %v", treeSubs.ToString()) }), - ) - - // Fusion - res, _ := MergeSubstitutions(metasToSubs, treeSubs) - if res.Equals(Failure()) { - return res - } - - debug( - Lib.MkLazy(func() string { return fmt.Sprintf("after merge : %v", res.ToString()) }), - ) - - EliminateMeta(&res) - Eliminate(&res) - - debug( - Lib.MkLazy(func() string { return fmt.Sprintf("after eliminate : %v", res.ToString()) }), - ) - - return res -} - -/* Call addUnification and returns a status - modify m.meta */ -func (m *Machine) trySubstituteMeta(i AST.Term, j AST.Term) Status { - debug( - Lib.MkLazy(func() string { return fmt.Sprintf("Try substitute : %v and %v", i.ToString(), j.ToString()) }), - ) - new_meta := AddUnification(i, j, m.meta.Copy()) - if new_meta.Equals(Failure()) { - return Status(ERROR) - } - m.meta = new_meta - return Status(SUCCESS) -} - -func AddUnification(term1, term2 AST.Term, subst Substitutions) Substitutions { - debug( - Lib.MkLazy(func() string { - return fmt.Sprintf( - "Add unification : %v and %v to %v", - term1.ToString(), - term2.ToString(), - subst.ToString()) - }), - ) - // unify with ct only if the term already has an unification or if there is 2 fun. Just add it and eliminate otherwise. - t1v, _ := subst.Get(term1.ToMeta()) - t2v, _ := subst.Get(term2.ToMeta()) - if (term1.IsMeta() && HasSubst(subst, term1.ToMeta()) && !t1v.Equals(term2)) || - (term2.IsMeta() && HasSubst(subst, term2.ToMeta()) && !t2v.Equals(term1)) || - (term1.IsFun() && term2.IsFun()) { - m := makeMachine() - m.meta = subst.Copy() - if m.addUnifications(term1, term2) == SUCCESS { - return m.meta - } else { - return Failure() - } - } else { - switch { - case term1.IsMeta(): - subst.Set(term1.ToMeta(), term2) - EliminateMeta(&subst) - Eliminate(&subst) - return subst - case term2.IsMeta(): - subst.Set(term2.ToMeta(), term1) - EliminateMeta(&subst) - Eliminate(&subst) - return subst - default: - return Failure() - } - } -} - -/* Adds the unifications found to the meta substitutions from running the algorithm on term1 and term2. */ -func (m *Machine) addUnifications(term1, term2 AST.Term) Status { - debug( - Lib.MkLazy(func() string { - return fmt.Sprintf( - "add unification : %v and %v", - term1.ToString(), - term2.ToString()) - }), - ) - meta := tryUnification(term1.Copy(), term2.Copy(), m.meta.Copy()) // Return empty or an array of 1 matching substitution, which is m.meta improved wit (term1, term2) - - if len(meta) == 0 { - return Status(ERROR) - } else { - m.meta = meta[0].GetSubst() - EliminateMeta(&m.meta) - Eliminate(&m.meta) - } - - return Status(SUCCESS) -} - -/* Tries to unify term1 with term2, depending on the substitutions already found by the parent unification process. */ -func tryUnification(term1, term2 AST.Term, meta Substitutions) []MatchingSubstitutions { - debug( - Lib.MkLazy(func() string { - return fmt.Sprintf( - "Try unification : %v and %v", - term1.ToString(), - term2.ToString()) - }), - ) - aux := makeMachine() - aux.terms = Lib.MkListV(term2) - aux.meta = meta - - // add begin at the start and end at the end ! - tree := makeBranch(ParseTerm(term1.Copy())) - res := aux.unifyAux(*tree) - return res -} - -/* Merge two valid substitutions */ -func MergeSubstitutions(s1, s2 Substitutions) (Substitutions, bool) { - debug( - Lib.MkLazy(func() string { - return fmt.Sprintf( - "Merge substitution : %v and %v", - s1.ToString(), - s2.ToString()) - }), - ) - res := Substitutions{} - same_key := false - - if s1.IsEmpty() { - return s2, false - } - - if s2.IsEmpty() { - return s1, false - } - - for _, subst := range s1 { - res.Set(subst.Get()) - } - - for _, subst := range s2 { - s2_k, s2_v := subst.Get() - if HasSubst(res, s2_k) { - same_key = true - res = AddUnification(s2_k.Copy(), s2_v.Copy(), res.Copy()) - } else { - res.Set(s2_k.ToMeta(), s2_v) - EliminateMeta(&res) - Eliminate(&res) - } - - } - return res, same_key -} diff --git a/src/main.go b/src/main.go index 4f51ef7d..9e7bf1fe 100644 --- a/src/main.go +++ b/src/main.go @@ -60,7 +60,9 @@ import ( "github.com/GoelandProver/Goeland/Search" "github.com/GoelandProver/Goeland/Search/incremental" "github.com/GoelandProver/Goeland/Typing" - "github.com/GoelandProver/Goeland/Unif" + "github.com/GoelandProver/Goeland/Unif/codetree" + "github.com/GoelandProver/Goeland/Unif/discriminationtree" + subst "github.com/GoelandProver/Goeland/Unif/substitution" ) var chAssistant chan bool = make(chan bool) @@ -219,7 +221,9 @@ func initDebuggers() { incremental.InitDebugger() Search.InitDebugger() Typing.InitDebugger() - Unif.InitDebugger() + codetree.InitDebugger() + discriminationtree.InitDebugger() + subst.InitDebugger() Engine.InitDebugger() gs3.InitDebugger() } diff --git a/src/options.go b/src/options.go index 21b8b135..2759529c 100644 --- a/src/options.go +++ b/src/options.go @@ -425,6 +425,22 @@ func buildOptions() { "Lists the available debuggers and exit", func(bool) { Glob.SetListDebuggers() }, func(bool) {}) + (&option[bool]{}).init( + "dt", + false, + "Use discrimination trees instead of code trees", + func(bool) { + Glob.SetDt() + }, + func(bool) {}) + (&option[bool]{}).init( + "ep", + false, + "With -dt: use the discrimination tree's early-pruning retrieval", + func(bool) { + Glob.SetEarlyPruning() + }, + func(bool) {}) } func chronoInit() {