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

16 files changed, 28 insertions, 33 deletions

diff --git a/test/regress/regress1/ho/NUM638^1.smt2 b/test/regress/regress1/ho/NUM638^1.smt2
index 59391ce8c..11683b1a7 100644
--- a/test/regress/regress1/ho/NUM638^1.smt2
+++ b/test/regress/regress1/ho/NUM638^1.smt2
@@ -1,8 +1,8 @@
-; COMMAND-LINE: --uf-ho --finite-model-find
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: unsat
 
 (set-option :incremental false)
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort nat 0)
 (declare-fun x () nat)
diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p
index e162a63a4..e07ad784f 100644
--- a/test/regress/regress1/ho/NUM925^1.p
+++ b/test/regress/regress1/ho/NUM925^1.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --ho-elim
+% COMMAND-LINE:  --ho-elim
 % EXPECT: % SZS status Theorem for NUM925^1
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress1/ho/SYO056^1.p b/test/regress/regress1/ho/SYO056^1.p
index a8a6bafca..deda234da 100644
--- a/test/regress/regress1/ho/SYO056^1.p
+++ b/test/regress/regress1/ho/SYO056^1.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --finite-model-find
+% COMMAND-LINE:  --finite-model-find
 % EXPECT: % SZS status CounterSatisfiable for SYO056^1
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress1/ho/bound_var_bug.p b/test/regress/regress1/ho/bound_var_bug.p
index 0dc946d6a..23bda7fb2 100644
--- a/test/regress/regress1/ho/bound_var_bug.p
+++ b/test/regress/regress1/ho/bound_var_bug.p
@@ -1,4 +1,3 @@
-% COMMAND-LINE: --uf-ho
 % EXPECT: % SZS status GaveUp for bound_var_bug
 
 % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/misc/leo --foatp e --atp e="$E_HOME"/eprover --atp epclextract="$E_HOME"/epclextract --proofoutput 1 --timeout 30 /Users/blanchette/hgs/afp_mining/tools/judgment_day_2017/data_afp/leo2-mepo/Call_Arity_SestoftGC_data/prob_308__3244432_1 ) ; }
diff --git a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p
index 6c35270fd..22c1d1dd1 100644
--- a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p
+++ b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --uf-ho --finite-model-find
+% COMMAND-LINE: --finite-model-find
 % EXPECT: % SZS status Satisfiable for bug_freeVar_BDD_General_data_270
 
 thf(ty_n_t__Nat__Onat, type,
diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
index 21405dfdb..7c9de4c49 100644
--- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
+++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --uf-ho --finite-model-find -q --decision=justification-old
+; COMMAND-LINE: --finite-model-find -q --decision=justification-old
 ; EXPECT: sat
 
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort qML_mu 0)
 (declare-sort qML_i 0)
diff --git a/test/regress/regress1/ho/fta0328.lfho.p b/test/regress/regress1/ho/fta0328.lfho.p
index c33b43ca5..f67c6db58 100644
--- a/test/regress/regress1/ho/fta0328.lfho.p
+++ b/test/regress/regress1/ho/fta0328.lfho.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --uf-ho --finite-model-find
+% COMMAND-LINE:  --finite-model-find
 % EXPECT: % SZS status CounterSatisfiable for fta0328.lfho
 
 % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/.isabelle/contrib/e-2.0-2/x86_64-darwin/eprover --auto-schedule --tstp-in --tstp-out --silent --cpu-limit=2 --proof-object=1 /Users/blanchette/hgs/matryoshka/papers/2019-TACAS-ehoh/eval/judgment_day/judgment_day_lifting_32/fta/prob_804__4064966_1 ) ; }
diff --git a/test/regress/regress1/ho/hoa0102.smt2 b/test/regress/regress1/ho/hoa0102.smt2
index 6be063783..c5840e6a9 100644
--- a/test/regress/regress1/ho/hoa0102.smt2
+++ b/test/regress/regress1/ho/hoa0102.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --uf-ho --full-saturate-quant
+; COMMAND-LINE:  --full-saturate-quant
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort Com$ 0)
 (declare-sort Glb$ 0)
diff --git a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2
index d536e51a1..d15095123 100644
--- a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2
+++ b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE:  --uf-ho --ho-elim
+; COMMAND-LINE:  --ho-elim
 ; EXPECT: unsat
 
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort num 0)
 (declare-fun agent_THFTYPE_i () $$unsorted)
diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2
index 9852150d9..a13aa2bae 100644
--- a/test/regress/regress1/ho/issue4065-no-rep.smt2
+++ b/test/regress/regress1/ho/issue4065-no-rep.smt2
@@ -1,7 +1,6 @@
-(set-logic AUFBV)
+(set-logic HO_AUFBV)
 (set-info :status unsat)
 (set-option :fmf-bound-int true)
-(set-option :uf-ho true)
 (declare-fun _substvar_20_ () Bool)
 (declare-sort S4 0)
 (assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true)))
diff --git a/test/regress/regress1/ho/issue4092-sinf.smt2 b/test/regress/regress1/ho/issue4092-sinf.smt2
index d3066c282..83a3e08b9 100644
--- a/test/regress/regress1/ho/issue4092-sinf.smt2
+++ b/test/regress/regress1/ho/issue4092-sinf.smt2
@@ -1,10 +1,9 @@
-; COMMAND-LINE: --uf-ho --sort-inference
+; COMMAND-LINE: --sort-inference
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-option :sort-inference true)
-(set-option :uf-ho true)
 (set-info :status sat)
-(declare-fun a ( Int ) Int) 
-(declare-fun b ( Int ) Int)  
-(assert (and (distinct 0 (b 5)) (distinct a b ))) 
-(check-sat) 
+(declare-fun a ( Int ) Int)
+(declare-fun b ( Int ) Int)
+(assert (and (distinct 0 (b 5)) (distinct a b )))
+(check-sat)
diff --git a/test/regress/regress1/ho/issue4134-sinf.smt2 b/test/regress/regress1/ho/issue4134-sinf.smt2
index 60a754aad..0003bc91e 100644
--- a/test/regress/regress1/ho/issue4134-sinf.smt2
+++ b/test/regress/regress1/ho/issue4134-sinf.smt2
@@ -1,7 +1,6 @@
-; COMMAND-LINE: --uf-ho --sort-inference
+; COMMAND-LINE: --sort-inference
 ; EXPECT: sat
-(set-logic ALL)
-(set-option :uf-ho true)
+(set-logic HO_ALL)
 (set-option :sort-inference true)
 (set-info :status sat)
 (declare-fun a () Int)
diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
index 313ff68a1..6a8feba5c 100644
--- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
+++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models --ho-elim
+; COMMAND-LINE: --no-check-unsat-cores --no-produce-models --ho-elim
 ; EXPECT: unsat
 
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort mu 0)
 (declare-fun meq_ind (mu mu $$unsorted) Bool)
diff --git a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
index 6743e00d4..3f02e56fd 100644
--- a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
+++ b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
@@ -1,8 +1,7 @@
-; COMMAND-LINE:  --uf-ho --finite-model-find --no-check-models
+; COMMAND-LINE:  --finite-model-find --no-check-models
 ; EXPECT: sat
 
-
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 
 (declare-fun mvalid ((-> $$unsorted Bool)) Bool)
diff --git a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p
index baabd675a..4068cc42e 100644
--- a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p
+++ b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --finite-model-find
+% COMMAND-LINE:   --finite-model-find
 % EXPECT: % SZS status GaveUp for soundness_fmf_SYO362^5-delta
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress1/ho/store-ax-min.p b/test/regress/regress1/ho/store-ax-min.p
index d67eb8dad..d000a17d0 100644
--- a/test/regress/regress1/ho/store-ax-min.p
+++ b/test/regress/regress1/ho/store-ax-min.p
@@ -1,5 +1,5 @@
-% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim-store-ax
-% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim
+% COMMAND-LINE: --full-saturate-quant --ho-elim-store-ax
+% COMMAND-LINE: --full-saturate-quant --ho-elim
 % EXPECT: % SZS status Theorem for store-ax-min
 
 thf(a, type, (a: $i)).