Parsing THF and adding several regressions (#3131)

7 files changed, 284 insertions, 0 deletions

diff --git a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
new file mode 100644
index 000000000..0ed7fe44b
--- /dev/null
+++ b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
@@ -0,0 +1,56 @@
+% COMMAND-LINE:  --uf-ho
+% EXPECT: % SZS status Unsatisfiable for bug_nodbuilding_interpreted_SYO042^1
+
+%------------------------------------------------------------------------------
+% File     : SYO042^1 : TPTP v7.2.0. Released v4.0.0.
+% Domain   : Syntactic
+% Problem  : Unsatisfiable basic formula 4
+% Version  : Especial.
+% English  :
+
+% Refs     : [BS09a] Brown E. & Smolka (2009), Terminating Tableaux for the
+%          : [BS09b] Brown E. & Smolka (2009), Extended First-Order Logic
+% Source   : [BS09a]
+% Names    :
+
+% Status   : Unsatisfiable
+% Rating   : 0.00 v5.4.0, 0.33 v5.3.0, 0.67 v5.0.0, 0.33 v4.1.0, 0.67 v4.0.1, 1.00 v4.0.0
+% Syntax   : Number of formulae    :    5 (   0 unit;   4 type;   0 defn)
+%            Number of atoms       :   15 (   3 equality;   0 variable)
+%            Maximal formula depth :    7 (   4 average)
+%            Number of connectives :   10 (   2   ~;   0   |;   4   &;   4   @)
+%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :    3 (   3   >;   0   *;   0   +;   0  <<)
+%            Number of symbols     :    6 (   4   :;   0   =)
+%            Number of variables   :    0 (   0 sgn;   0   !;   0   ?;   0   ^)
+%                                         (   0   :;   0  !>;   0  ?*)
+%                                         (   0  @-;   0  @+)
+% SPC      : TH0_UNS_EQU_NAR
+
+% Comments : The fragment of simple type theory that restricts equations to
+%            base types and disallows lambda abstraction and quantification is
+%            decidable. This is an example.
+%------------------------------------------------------------------------------
+thf(g,type,(
+    g: $o > $o )).
+
+thf(p,type,(
+    p: ( $o > $o ) > $o )).
+
+thf(x,type,(
+    x: $o )).
+
+thf(y,type,(
+    y: $o )).
+
+thf(4,axiom,
+    ( ( x != y )
+    & ( ( g @ x )
+      = y )
+    & ( ( g @ y )
+      = x )
+    & ( p @ g )
+    & ~ ( p @ (~) ) )).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/ho/fta0210.smt2 b/test/regress/regress0/ho/fta0210.smt2
new file mode 100644
index 000000000..9f0a39f25
--- /dev/null
+++ b/test/regress/regress0/ho/fta0210.smt2
@@ -0,0 +1,64 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort A$ 0)
+(declare-sort Nat$ 0)
+(declare-sort A_poly$ 0)
+(declare-sort Nat_poly$ 0)
+(declare-sort A_poly_poly$ 0)
+(declare-fun p$ () A_poly$)
+(declare-fun uu$ (A_poly$ (-> A_poly$ A_poly$) A_poly$) A_poly$)
+(declare-fun one$ () Nat$)
+(declare-fun suc$ (Nat$) Nat$)
+(declare-fun uua$ (A_poly$) A_poly$)
+(declare-fun uub$ (A$ (-> A$ A$) A$) A$)
+(declare-fun uuc$ (A$) A$)
+(declare-fun uud$ (Nat$ (-> Nat$ Nat$) Nat$) Nat$)
+(declare-fun uue$ (Nat$) Nat$)
+(declare-fun one$a () Nat_poly$)
+(declare-fun one$b () A$)
+(declare-fun one$c () A_poly$)
+(declare-fun plus$ (A_poly$ A_poly$) A_poly$)
+(declare-fun poly$ (A_poly$ A$) A$)
+(declare-fun zero$ () A_poly$)
+(declare-fun pCons$ (A$ A_poly$) A_poly$)
+(declare-fun plus$a (Nat$ Nat$) Nat$)
+(declare-fun plus$b (A$ A$) A$)
+(declare-fun plus$c (Nat_poly$ Nat_poly$) Nat_poly$)
+(declare-fun poly$a (Nat_poly$ Nat$) Nat$)
+(declare-fun poly$b (A_poly_poly$ A_poly$) A_poly$)
+(declare-fun power$ (A$ Nat$) A$)
+(declare-fun psize$ (A_poly$) Nat$)
+(declare-fun times$ (A_poly$ A_poly$) A_poly$)
+(declare-fun zero$a () Nat$)
+(declare-fun zero$b () A$)
+(declare-fun zero$c () Nat_poly$)
+(declare-fun zero$d () A_poly_poly$)
+(declare-fun pCons$a (Nat$ Nat_poly$) Nat_poly$)
+(declare-fun pCons$b (A_poly$ A_poly_poly$) A_poly_poly$)
+(declare-fun power$a (A_poly$ Nat$) A_poly$)
+(declare-fun power$b (Nat_poly$ Nat$) Nat_poly$)
+(declare-fun power$c (Nat$ Nat$) Nat$)
+(declare-fun psize$a (A_poly_poly$) Nat$)
+(declare-fun times$a (Nat$ Nat$) Nat$)
+(declare-fun times$b (A$ A$) A$)
+(declare-fun times$c (Nat_poly$ Nat_poly$) Nat_poly$)
+(declare-fun times$d (A_poly_poly$ A_poly_poly$) A_poly_poly$)
+(declare-fun uminus$ (A_poly$) A_poly$)
+(declare-fun uminus$a (A$) A$)
+(declare-fun constant$ ((-> A$ A$)) Bool)
+(declare-fun pcompose$ (A_poly$ A_poly$) A_poly$)
+(declare-fun pcompose$a (Nat_poly$ Nat_poly$) Nat_poly$)
+(declare-fun pcompose$b (A_poly_poly$ A_poly_poly$) A_poly_poly$)
+(declare-fun poly_shift$ (Nat$ A_poly$) A_poly$)
+(declare-fun fold_coeffs$ ((-> A_poly$ (-> (-> A_poly$ A_poly$) (-> A_poly$ A_poly$))) A_poly_poly$ (-> A_poly$ A_poly$)) (-> A_poly$ A_poly$))
+(declare-fun poly_cutoff$ (Nat$ A_poly$) A_poly$)
+(declare-fun fold_coeffs$a ((-> A$ (-> (-> A$ A$) (-> A$ A$))) A_poly$ (-> A$ A$)) (-> A$ A$))
+(declare-fun fold_coeffs$b ((-> Nat$ (-> (-> Nat$ Nat$) (-> Nat$ Nat$))) Nat_poly$ (-> Nat$ Nat$)) (-> Nat$ Nat$))
+
+(assert (! (forall ((?v0 A$)) (= (poly$ zero$ ?v0) zero$b)) :named a14))
+(assert (! (forall ((?v0 (-> A$ A$))) (= (constant$ ?v0) (forall ((?v1 A$) (?v2 A$)) (= (?v0 ?v1) (?v0 ?v2))))) :named a69))
+(assert (! (not (constant$ (poly$ zero$))) :named a206))
+
+(check-sat)
+;(get-proof)
diff --git a/test/regress/regress0/ho/ho-exponential-model.smt2 b/test/regress/regress0/ho/ho-exponential-model.smt2
new file mode 100644
index 000000000..3f0011828
--- /dev/null
+++ b/test/regress/regress0/ho/ho-exponential-model.smt2
@@ -0,0 +1,40 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun f1 (Int Int Int Int) Int)
+(declare-fun f2 (Int Int Int) Int)
+(declare-fun f3 (Int Int) Int)
+(declare-fun f4 (Int) Int)
+(declare-fun f5 (Int Int Int) Int)
+(declare-fun f6 (Int Int) Int)
+(declare-fun f7 (Int) Int)
+
+
+(assert (= (f1 0) (f1 1)))
+(assert (= (f1 1) f2))
+
+(assert (= (f2 0) (f2 1)))
+(assert (= (f2 1) f3))
+
+(assert (= (f3 0) (f3 1)))
+(assert (= (f3 1) f4))
+
+(assert (= (f4 0) (f4 1)))
+(assert (= (f4 1) 2))
+
+
+(assert (= (f1 3) (f1 4)))
+(assert (= (f1 4) f5))
+
+(assert (= (f5 3) (f5 4)))
+(assert (= (f5 4) f6))
+
+(assert (= (f6 3) (f6 4)))
+(assert (= (f6 4) f7))
+
+(assert (= (f7 3) (f7 4)))
+(assert (= (f7 4) 5))
+
+; this benchmark has a concise model representation for f1 if we use curried (tree-like) models for UF
+(check-sat)
diff --git a/test/regress/regress0/ho/ho-matching-enum-2.smt2 b/test/regress/regress0/ho/ho-matching-enum-2.smt2
new file mode 100644
index 000000000..9581e4c4f
--- /dev/null
+++ b/test/regress/regress0/ho/ho-matching-enum-2.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun p (Int) Bool)
+(declare-fun q (Int) Bool)
+(declare-fun k (Int Int) Int)
+
+(assert (q (k 0 1)))
+(assert (not (p (k 0 0))))
+
+(assert (forall ((f (-> Int Int Int)) (y Int) (z Int)) (or (p (f y z)) (not (q (f z y))))))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/ho/ho-std-fmf.smt2 b/test/regress/regress0/ho/ho-std-fmf.smt2
new file mode 100644
index 000000000..61d82d00c
--- /dev/null
+++ b/test/regress/regress0/ho/ho-std-fmf.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --uf-ho --finite-model-find
+; EXPECT: sat
+(set-logic UF)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun P (U U) Bool)
+(declare-fun Q (U U) Bool)
+(declare-fun R (U U) Bool)
+(declare-fun a () U)
+(declare-fun b () U)
+
+; can solve this using standard MBQI model for P = \ xy true
+(assert (forall ((x U) (y U)) (or (P x y) (Q x y))))
+(assert (forall ((x U) (y U)) (or (P x y) (R x y))))
+
+(assert (not (= a b)))
+(assert (= (Q a) (R b)))
+(check-sat)
diff --git a/test/regress/regress0/ho/hoa0008.smt2 b/test/regress/regress0/ho/hoa0008.smt2
new file mode 100644
index 000000000..f4833aadf
--- /dev/null
+++ b/test/regress/regress0/ho/hoa0008.smt2
@@ -0,0 +1,68 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort A$ 0)
+(declare-sort Com$ 0)
+(declare-sort Loc$ 0)
+(declare-sort Nat$ 0)
+(declare-sort Pname$ 0)
+(declare-sort State$ 0)
+(declare-sort Vname$ 0)
+(declare-sort Literal$ 0)
+(declare-sort Natural$ 0)
+(declare-sort Typerep$ 0)
+(declare-sort A_triple$ 0)
+(declare-sort Com_option$ 0)
+(declare-fun p$ () (-> A$ (-> State$ Bool)))
+(declare-fun q$ () (-> A$ (-> State$ Bool)))
+(declare-fun pn$ () Pname$)
+(declare-fun wt$ (Com$) Bool)
+(declare-fun ass$ (Vname$ (-> State$ Nat$)) Com$)
+(declare-fun suc$ (Nat$) Nat$)
+(declare-fun the$ (Com_option$) Com$)
+(declare-fun body$ (Pname$) Com$)
+(declare-fun call$ (Vname$ Pname$ (-> State$ Nat$)) Com$)
+(declare-fun cond$ ((-> State$ Bool) Com$ Com$) Com$)
+(declare-fun none$ () Com_option$)
+(declare-fun plus$ (Nat$ Nat$) Nat$)
+(declare-fun semi$ (Com$ Com$) Com$)
+(declare-fun size$ (A_triple$) Nat$)
+(declare-fun skip$ () Com$)
+(declare-fun some$ (Com$) Com_option$)
+(declare-fun suc$a (Natural$) Natural$)
+(declare-fun zero$ () Nat$)
+(declare-fun body$a (Pname$) Com_option$)
+(declare-fun evalc$ (Com$ State$ State$) Bool)
+(declare-fun evaln$ (Com$ State$ Nat$ State$) Bool)
+(declare-fun local$ (Loc$ (-> State$ Nat$) Com$) Com$)
+(declare-fun plus$a (Natural$ Natural$) Natural$)
+(declare-fun size$a (Com$) Nat$)
+(declare-fun size$b (Natural$) Nat$)
+(declare-fun size$c (Bool) Nat$)
+(declare-fun size$d (Com_option$) Nat$)
+(declare-fun size$e (Typerep$) Nat$)
+(declare-fun size$f (Literal$) Nat$)
+(declare-fun while$ ((-> State$ Bool) Com$) Com$)
+(declare-fun zero$a () Natural$)
+(declare-fun triple$ ((-> A$ (-> State$ Bool)) Com$ (-> A$ (-> State$ Bool))) A_triple$)
+(declare-fun rec_bool$ (Nat$ Nat$) (-> Bool Nat$))
+(declare-fun size_com$ (Com$) Nat$)
+(declare-fun size_bool$ (Bool) Nat$)
+(declare-fun wT_bodies$ () Bool)
+(declare-fun size_option$ ((-> Com$ Nat$)) (-> Com_option$ Nat$))
+(declare-fun size_triple$ ((-> A$ Nat$) A_triple$) Nat$)
+(declare-fun size_natural$ (Natural$) Nat$)
+(declare-fun triple_valid$ (Nat$ A_triple$) Bool)
+(assert (! (not (triple_valid$ zero$ (triple$ p$ (body$ pn$) q$))) :named a0))
+
+(assert (! (forall ((?v0 Nat$) (?v1 (-> A$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> A$ (-> State$ Bool)))) (= (triple_valid$ ?v0 (triple$ ?v1 ?v2 ?v3)) (forall ((?v4 A$) (?v5 State$)) (=> (?v1 ?v4 ?v5) (forall ((?v6 State$)) (=> (evaln$ ?v2 ?v5 ?v0 ?v6) (?v3 ?v4 ?v6))))))) :named a6))
+
+(assert (! (= (size_bool$ true) zero$) :named a13))
+(assert (! (= size_bool$ (rec_bool$ zero$ zero$)) :named a14))
+
+(assert (! (forall ((?v0 Nat$)) (not (= zero$ (suc$ ?v0)))) :named a37))
+
+(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (and (evaln$ (body$ ?v0) ?v1 ?v2 ?v3) (forall ((?v4 Nat$)) (=> (and (= ?v2 (suc$ ?v4)) (evaln$ (the$ (body$a ?v0)) ?v1 ?v4 ?v3)) false))) false)) :named a204))
+
+(check-sat)
+;(get-proof)
diff --git a/test/regress/regress0/ho/match-middle.smt2 b/test/regress/regress0/ho/match-middle.smt2
new file mode 100644
index 000000000..0485f9a6f
--- /dev/null
+++ b/test/regress/regress0/ho/match-middle.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun f (Int Int Int) Int)
+(declare-fun h (Int Int Int) Int)
+(declare-fun g (Int Int) Int)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+
+(assert (or (= (f a) g) (= (h a) g)))
+
+(assert (= (f a b d) c))
+(assert (= (h a b d) c))
+
+(assert (forall ((x Int) (y Int)) (not (= (g x y) c))))
+
+(check-sat)