feat: implementation of discrimination trees

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 = ""

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")

go.mod

@@ -0,0 +1,3 @@
+module github.com/GoelandProver/Goeland
+
+go 1.22.2

src/AST/tptp-native-types.go

@@ -60,8 +60,6 @@ func initTPTPNativeTypes() {
 
 	tIndividual = MkTyConst("$i")
 	tProp = MkTyConst("$o")
-
-	count_meta = 0
 }
 
 func TType() Ty {

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
 }

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,19 +74,23 @@ func (f FormListDS) Print() {
 	}
 }
 
-func (f FormListDS) Copy() Unif.DataStructure {
+func (f FormListDS) Copy() subst.DataStructure {
 	return FormListDS{Lib.ListCpy(f.GetFL())}
 }
 
 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{}
 }

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]

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 {

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{}

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 */

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 */

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
+}

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

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) {

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]()
 }

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"
 )
 
 // ----------------------------------------------------------------------------

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 {

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

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 {