Better support for HOL parsing and set up (#6697)

This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.

For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).

33 files changed, 33 insertions, 67 deletions

diff --git a/test/regress/regress0/ho/apply-collapse-sat.smt2 b/test/regress/regress0/ho/apply-collapse-sat.smt2
index 74a9df660..64aaa797d 100644
--- a/test/regress/regress0/ho/apply-collapse-sat.smt2
+++ b/test/regress/regress0/ho/apply-collapse-sat.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/apply-collapse-unsat.smt2 b/test/regress/regress0/ho/apply-collapse-unsat.smt2
index 101de9081..45eeb23a7 100644
--- a/test/regress/regress0/ho/apply-collapse-unsat.smt2
+++ b/test/regress/regress0/ho/apply-collapse-unsat.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
index 0ed7fe44b..c4b517e56 100644
--- a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
+++ b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
@@ -1,4 +1,3 @@
-% COMMAND-LINE:  --uf-ho
 % EXPECT: % SZS status Unsatisfiable for bug_nodbuilding_interpreted_SYO042^1
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress0/ho/cong-full-apply.smt2 b/test/regress/regress0/ho/cong-full-apply.smt2
index 0ff147b97..493bbf140 100644
--- a/test/regress/regress0/ho/cong-full-apply.smt2
+++ b/test/regress/regress0/ho/cong-full-apply.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status unsat)
 (declare-fun f (Int) Int)
 (declare-fun g (Int) Int)
diff --git a/test/regress/regress0/ho/cong.smt2 b/test/regress/regress0/ho/cong.smt2
index 531356568..b1feafe3e 100644
--- a/test/regress/regress0/ho/cong.smt2
+++ b/test/regress/regress0/ho/cong.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U) U)
diff --git a/test/regress/regress0/ho/declare-fun-variants.smt2 b/test/regress/regress0/ho/declare-fun-variants.smt2
index 990423fb3..de37f7044 100644
--- a/test/regress/regress0/ho/declare-fun-variants.smt2
+++ b/test/regress/regress0/ho/declare-fun-variants.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status sat)
 (declare-fun f (Int Int) Int)
 (declare-fun g (Int) (-> Int Int))
diff --git a/test/regress/regress0/ho/def-fun-flatten.smt2 b/test/regress/regress0/ho/def-fun-flatten.smt2
index af33098f5..81af169a7 100644
--- a/test/regress/regress0/ho/def-fun-flatten.smt2
+++ b/test/regress/regress0/ho/def-fun-flatten.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-fun f (Int Int) Int)
 (define-fun g ((x Int)) (-> Int Int) (f x))
diff --git a/test/regress/regress0/ho/ext-finite-unsat.smt2 b/test/regress/regress0/ho/ext-finite-unsat.smt2
index 1719d5ad1..282cc3bda 100644
--- a/test/regress/regress0/ho/ext-finite-unsat.smt2
+++ b/test/regress/regress0/ho/ext-finite-unsat.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U) U)
diff --git a/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 b/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2
index 7031829d4..175ced858 100644
--- a/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2
+++ b/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f ((-> U U)) U)
diff --git a/test/regress/regress0/ho/ext-ho.smt2 b/test/regress/regress0/ho/ext-ho.smt2
index 02e51654e..613533ebd 100644
--- a/test/regress/regress0/ho/ext-ho.smt2
+++ b/test/regress/regress0/ho/ext-ho.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f ((-> U U)) U)
diff --git a/test/regress/regress0/ho/ext-sat-partial-eval.smt2 b/test/regress/regress0/ho/ext-sat-partial-eval.smt2
index f3392f1ba..cc63c52ea 100644
--- a/test/regress/regress0/ho/ext-sat-partial-eval.smt2
+++ b/test/regress/regress0/ho/ext-sat-partial-eval.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/ext-sat.smt2 b/test/regress/regress0/ho/ext-sat.smt2
index 772b6eaa0..f91fb8240 100644
--- a/test/regress/regress0/ho/ext-sat.smt2
+++ b/test/regress/regress0/ho/ext-sat.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/finite-fun-ext.smt2 b/test/regress/regress0/ho/finite-fun-ext.smt2
index 005a2109a..63e25cb03 100644
--- a/test/regress/regress0/ho/finite-fun-ext.smt2
+++ b/test/regress/regress0/ho/finite-fun-ext.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 
 (declare-datatype Unit ((unit)))
 
diff --git a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 b/test/regress/regress0/ho/fta0144-alpha-eq.smt2
index 0fc536bd9..747bfd48e 100644
--- a/test/regress/regress0/ho/fta0144-alpha-eq.smt2
+++ b/test/regress/regress0/ho/fta0144-alpha-eq.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort Nat$ 0)
 (declare-sort Complex$ 0)
 (declare-sort Real_set$ 0)
diff --git a/test/regress/regress0/ho/fta0210.smt2 b/test/regress/regress0/ho/fta0210.smt2
index 9f0a39f25..864bb9859 100644
--- a/test/regress/regress0/ho/fta0210.smt2
+++ b/test/regress/regress0/ho/fta0210.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort A$ 0)
 (declare-sort Nat$ 0)
 (declare-sort A_poly$ 0)
diff --git a/test/regress/regress0/ho/fun-subtyping.smt2 b/test/regress/regress0/ho/fun-subtyping.smt2
index 8eae3d073..e7cc01772 100644
--- a/test/regress/regress0/ho/fun-subtyping.smt2
+++ b/test/regress/regress0/ho/fun-subtyping.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-fun g (Int) Real)
 (declare-fun h (Int) Real)
 (assert (not (= g h)))
diff --git a/test/regress/regress0/ho/ho-exponential-model.smt2 b/test/regress/regress0/ho/ho-exponential-model.smt2
index 3f0011828..964a45f77 100644
--- a/test/regress/regress0/ho/ho-exponential-model.smt2
+++ b/test/regress/regress0/ho/ho-exponential-model.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status sat)
 (declare-fun f1 (Int Int Int Int) Int)
 (declare-fun f2 (Int Int Int) Int)
diff --git a/test/regress/regress0/ho/ho-match-fun-suffix.smt2 b/test/regress/regress0/ho/ho-match-fun-suffix.smt2
index 1e4ad243c..4418b156f 100644
--- a/test/regress/regress0/ho/ho-match-fun-suffix.smt2
+++ b/test/regress/regress0/ho/ho-match-fun-suffix.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-fun f (Int Int) Int)
 (declare-fun a () Int)
diff --git a/test/regress/regress0/ho/ho-matching-enum-2.smt2 b/test/regress/regress0/ho/ho-matching-enum-2.smt2
index 9581e4c4f..e73afdce2 100644
--- a/test/regress/regress0/ho/ho-matching-enum-2.smt2
+++ b/test/regress/regress0/ho/ho-matching-enum-2.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 
 (declare-sort U 0)
diff --git a/test/regress/regress0/ho/ho-matching-enum.smt2 b/test/regress/regress0/ho/ho-matching-enum.smt2
index bd1d2837f..df3a920ec 100644
--- a/test/regress/regress0/ho/ho-matching-enum.smt2
+++ b/test/regress/regress0/ho/ho-matching-enum.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 
 (declare-sort U 0)
diff --git a/test/regress/regress0/ho/ho-matching-nested-app.smt2 b/test/regress/regress0/ho/ho-matching-nested-app.smt2
index d6de559e6..506cd55cf 100644
--- a/test/regress/regress0/ho/ho-matching-nested-app.smt2
+++ b/test/regress/regress0/ho/ho-matching-nested-app.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 
 (declare-sort U 0)
diff --git a/test/regress/regress0/ho/ho-std-fmf.smt2 b/test/regress/regress0/ho/ho-std-fmf.smt2
index 61d82d00c..1b23fdb6f 100644
--- a/test/regress/regress0/ho/ho-std-fmf.smt2
+++ b/test/regress/regress0/ho/ho-std-fmf.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --uf-ho --finite-model-find
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun P (U U) Bool)
diff --git a/test/regress/regress0/ho/hoa0008.smt2 b/test/regress/regress0/ho/hoa0008.smt2
index f4833aadf..b43920c21 100644
--- a/test/regress/regress0/ho/hoa0008.smt2
+++ b/test/regress/regress0/ho/hoa0008.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort A$ 0)
 (declare-sort Com$ 0)
 (declare-sort Loc$ 0)
diff --git a/test/regress/regress0/ho/issue4990-care-graph.smt2 b/test/regress/regress0/ho/issue4990-care-graph.smt2
index 6c44a94a8..93c87d3c9 100644
--- a/test/regress/regress0/ho/issue4990-care-graph.smt2
+++ b/test/regress/regress0/ho/issue4990-care-graph.smt2
@@ -1,7 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic QF_AUFBVLIA)
-(set-option :uf-ho true)
+(set-logic HO_QF_AUFBVLIA)
 (declare-fun a () Int)
 (declare-fun b () Int)
 (declare-fun c (Int) Int)
diff --git a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2
index e97b914a2..9091cf8bd 100644
--- a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2
+++ b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2
@@ -1,7 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic QF_AUFBVLIA)
-(set-option :uf-ho true)
+(set-logic HO_QF_AUFBVLIA)
 (declare-fun a (Int) Int)
 (declare-fun b (Int) Int)
 (assert (distinct a b))
diff --git a/test/regress/regress0/ho/ite-apply-eq.smt2 b/test/regress/regress0/ho/ite-apply-eq.smt2
index 474f6887e..2e21d3081 100644
--- a/test/regress/regress0/ho/ite-apply-eq.smt2
+++ b/test/regress/regress0/ho/ite-apply-eq.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status sat)
 (declare-fun x () Int)
 (declare-fun f (Int) Int)
diff --git a/test/regress/regress0/ho/lambda-equality-non-canon.smt2 b/test/regress/regress0/ho/lambda-equality-non-canon.smt2
index 80f3db417..61753d90a 100644
--- a/test/regress/regress0/ho/lambda-equality-non-canon.smt2
+++ b/test/regress/regress0/ho/lambda-equality-non-canon.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status sat)
 (declare-fun f (Int) Int)
 
diff --git a/test/regress/regress0/ho/match-middle.smt2 b/test/regress/regress0/ho/match-middle.smt2
index 0485f9a6f..225faa1a5 100644
--- a/test/regress/regress0/ho/match-middle.smt2
+++ b/test/regress/regress0/ho/match-middle.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status unsat)
 (declare-fun f (Int Int Int) Int)
 (declare-fun h (Int Int Int) Int)
diff --git a/test/regress/regress0/ho/modulo-func-equality.smt2 b/test/regress/regress0/ho/modulo-func-equality.smt2
index 8e300ac72..984835be7 100644
--- a/test/regress/regress0/ho/modulo-func-equality.smt2
+++ b/test/regress/regress0/ho/modulo-func-equality.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status unsat)
 (declare-fun P (Int) Bool)
 (declare-fun Q (Int) Bool)
diff --git a/test/regress/regress0/ho/shadowing-defs.smt2 b/test/regress/regress0/ho/shadowing-defs.smt2
index 722e970b6..fb5ac3ec6 100644
--- a/test/regress/regress0/ho/shadowing-defs.smt2
+++ b/test/regress/regress0/ho/shadowing-defs.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unknown
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort mu 0)
 
diff --git a/test/regress/regress0/ho/simple-matching-partial.smt2 b/test/regress/regress0/ho/simple-matching-partial.smt2
index 41b2a0bca..18c578367 100644
--- a/test/regress/regress0/ho/simple-matching-partial.smt2
+++ b/test/regress/regress0/ho/simple-matching-partial.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/simple-matching.smt2 b/test/regress/regress0/ho/simple-matching.smt2
index 8e2315b2f..cbd70f072 100644
--- a/test/regress/regress0/ho/simple-matching.smt2
+++ b/test/regress/regress0/ho/simple-matching.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U) U)
diff --git a/test/regress/regress0/ho/trans.smt2 b/test/regress/regress0/ho/trans.smt2
index 088abbab1..b33644db3 100644
--- a/test/regress/regress0/ho/trans.smt2
+++ b/test/regress/regress0/ho/trans.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U) U)