summaryrefslogtreecommitdiff
path: root/test/golden/formula
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/formula')
-rw-r--r--test/golden/formula/encoding tasks.golden8
-rw-r--r--test/golden/formula/generating tasks.golden331
-rw-r--r--test/golden/formula/glossing.golden189
-rw-r--r--test/golden/formula/verification.golden11
4 files changed, 0 insertions, 539 deletions
diff --git a/test/golden/formula/encoding tasks.golden b/test/golden/formula/encoding tasks.golden
deleted file mode 100644
index cb7505e..0000000
--- a/test/golden/formula/encoding tasks.golden
+++ /dev/null
@@ -1,8 +0,0 @@
-fof(zf_q0,conjecture,![V0,V1]:(V0=V0&V1=V1)).
-------------------
-fof(zf_q0,conjecture,?[V0,V1]:V0=V1).
-fof(zf_h0,axiom,![V2,V3]:(V2=V2&V3=V3)).
-------------------
-fof(zf_q0,conjecture,?[V0,V1]:V0=V1<=>~?[V2]:V2!=V2).
-fof(zf_h0,axiom,![V3,V4]:(V3=V3&V4=V4)).
-fof(zf_h1,axiom,?[V5,V6]:V5=V6). \ No newline at end of file
diff --git a/test/golden/formula/generating tasks.golden b/test/golden/formula/generating tasks.golden
deleted file mode 100644
index 54c2012..0000000
--- a/test/golden/formula/generating tasks.golden
+++ /dev/null
@@ -1,331 +0,0 @@
-[ Task
- { taskDirectness = Direct
- , taskHypotheses = []
- , taskConjectureLabel = Marker "formula_test_forall"
- , taskLocation = Location
- { locFile = "test/examples/formula.tex"
- , locLine = 1
- , locColumn = 1
- }
- , taskConjecture = Quantified Universally
- ( Scope
- ( Connected Conjunction
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 2
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 2
- , locColumn = 33
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "y" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- )
- }
-, Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "formula_test_forall" Quantified Universally
- ( Scope
- ( Connected Conjunction
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 2
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 2
- , locColumn = 33
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "y" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- )
- ]
- , taskConjectureLabel = Marker "formula_test_exists"
- , taskLocation = Location
- { locFile = "test/examples/formula.tex"
- , locLine = 5
- , locColumn = 1
- }
- , taskConjecture = Quantified Existentially
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 6
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- }
-, Task
- { taskDirectness = Direct
- , taskHypotheses =
- [ Hypothesis Marker "formula_test_exists" Quantified Existentially
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 6
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- , Hypothesis Marker "formula_test_forall" Quantified Universally
- ( Scope
- ( Connected Conjunction
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 2
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 2
- , locColumn = 33
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "y" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- )
- ]
- , taskConjectureLabel = Marker "formula_test_not_exists"
- , taskLocation = Location
- { locFile = "test/examples/formula.tex"
- , locLine = 9
- , locColumn = 1
- }
- , taskConjecture = Connected Equivalence
- ( Quantified Existentially
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 10
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- )
- ( Not
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 10
- , locColumn = 42
- }
- )
- ( Quantified Existentially
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 10
- , locColumn = 60
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "neq" )
- ( ParameterArity 0 )
- ( Marker "neq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- )
- )
- )
- }
-] \ No newline at end of file
diff --git a/test/golden/formula/glossing.golden b/test/golden/formula/glossing.golden
deleted file mode 100644
index b0eb10c..0000000
--- a/test/golden/formula/glossing.golden
+++ /dev/null
@@ -1,189 +0,0 @@
-[ BlockLemma
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 1
- , locColumn = 1
- }
- )
- ( Marker "formula_test_forall" )
- ( Lemma []
- ( Quantified Universally
- ( Scope
- ( Connected Conjunction
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 2
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 2
- , locColumn = 33
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "y" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- )
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 5
- , locColumn = 1
- }
- )
- ( Marker "formula_test_exists" )
- ( Lemma []
- ( Quantified Existentially
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 6
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 9
- , locColumn = 1
- }
- )
- ( Marker "formula_test_not_exists" )
- ( Lemma []
- ( Connected Equivalence
- ( Quantified Existentially
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 10
- , locColumn = 22
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "y" )
- )
- ]
- )
- )
- )
- ( Not
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 10
- , locColumn = 42
- }
- )
- ( Quantified Existentially
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/formula.tex"
- , locLine = 10
- , locColumn = 60
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "neq" )
- ( ParameterArity 0 )
- ( Marker "neq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- )
- )
- )
- )
- )
-] \ No newline at end of file
diff --git a/test/golden/formula/verification.golden b/test/golden/formula/verification.golden
deleted file mode 100644
index 3295320..0000000
--- a/test/golden/formula/verification.golden
+++ /dev/null
@@ -1,11 +0,0 @@
-VerifiedWithTrustedVampire
- ( VerificationReport
- { verificationRoute = LegacyVerificationRoute
- , verificationLegacyDeclaredAssumptionCount = 0
- , verificationTypedDeclaredAssumptionCount = 0
- , verificationTrustedVampireCount = 3
- , verificationExplicitGapLocations = []
- , verificationTrustedLegacyRuleCount = 0
- , verificationKernelProofCount = 0
- }
- ) \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-05 01:47:36 +0000