From 58cfaff9571f9d83a0ab9e264a995194efaec9fe Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 15:47:03 -0500 Subject: [PATCH 1/9] Towards demoting declare-fun --- src/cmd_parser.cpp | 4 ++-- tests/arith-rules-test.smt3 | 8 ++++---- tests/bv-concat.smt3 | 4 ++-- tests/datatype-simple.smt3 | 6 +++--- tests/ff-nil.smt3 | 2 +- tests/ite-compile-test.smt3 | 4 ++-- tests/literals.smt3 | 4 ++-- tests/mutual-rec.smt3 | 4 ++-- tests/nat-type.smt3 | 2 +- tests/pf-haniel.smt3 | 16 ++++++++-------- tests/premise-list-cong-2.smt3 | 2 +- tests/premise-list-cong.smt3 | 2 +- tests/quant-sk-small.alfc.smt3 | 2 +- tests/quoted.smt3 | 6 +++--- tests/requires.smt3 | 4 ++-- tests/simple-pf.smt3 | 6 +++--- tests/simple-pf2.smt3 | 6 +++--- tests/simple.smt3 | 2 +- tests/strings-rules-test.smt3 | 8 ++++---- tests/use-match.smt3 | 2 +- user_manual.md | 12 ++++++------ 21 files changed, 53 insertions(+), 53 deletions(-) diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index ab37650f..cce7648c 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -33,8 +33,6 @@ CmdParser::CmdParser(Lexer& lex, d_table["declare-const"] = Token::DECLARE_CONST; d_table["declare-datatype"] = Token::DECLARE_DATATYPE; d_table["declare-datatypes"] = Token::DECLARE_DATATYPES; - d_table["declare-fun"] = Token::DECLARE_FUN; - d_table["declare-sort"] = Token::DECLARE_SORT; d_table["define-const"] = Token::DEFINE_CONST; d_table["echo"] = Token::ECHO; d_table["exit"] = Token::EXIT; @@ -54,7 +52,9 @@ CmdParser::CmdParser(Lexer& lex, { // only used in smt2 queries d_table["assert"] = Token::ASSERT; + d_table["declare-fun"] = Token::DECLARE_FUN; d_table["define-fun"] = Token::DEFINE_FUN; + d_table["declare-sort"] = Token::DECLARE_SORT; d_table["define-sort"] = Token::DEFINE_SORT; d_table["check-sat"] = Token::CHECK_SAT; d_table["check-sat-assuming"] = Token::CHECK_SAT_ASSUMING; diff --git a/tests/arith-rules-test.smt3 b/tests/arith-rules-test.smt3 index 99a29b7e..2ba86921 100644 --- a/tests/arith-rules-test.smt3 +++ b/tests/arith-rules-test.smt3 @@ -1,9 +1,9 @@ (include "Arith-rules.smt3") -(declare-fun x () Int) -(declare-fun y () Int) -(declare-fun z () Int) -(declare-fun w () Int) +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) +(declare-const w Int) (assume @p0 (< x (* 2 y))) (assume @p1 (< y z)) diff --git a/tests/bv-concat.smt3 b/tests/bv-concat.smt3 index 1b4e2a81..8f2aa741 100644 --- a/tests/bv-concat.smt3 +++ b/tests/bv-concat.smt3 @@ -18,7 +18,7 @@ (BitVec (alf.add n m)))) -(declare-fun x () (BitVec 2)) -(declare-fun y () (BitVec 3)) +(declare-const x (BitVec 2)) +(declare-const y (BitVec 3)) (define z () (bvconcat x y) :type (BitVec 5)) diff --git a/tests/datatype-simple.smt3 b/tests/datatype-simple.smt3 index 7d2eb549..762b32fd 100644 --- a/tests/datatype-simple.smt3 +++ b/tests/datatype-simple.smt3 @@ -3,7 +3,7 @@ (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (data nat) (children list)) (leaf)))) -(declare-fun x () nat) -(declare-fun y () list) -(declare-fun z () tree) +(declare-const x nat) +(declare-const y list) +(declare-const z tree) (assume a1 (= x (succ zero))) diff --git a/tests/ff-nil.smt3 b/tests/ff-nil.smt3 index 759903d6..af059d7f 100644 --- a/tests/ff-nil.smt3 +++ b/tests/ff-nil.smt3 @@ -10,7 +10,7 @@ :right-assoc-nil (ff.value p 0) ) -(declare-fun c () (_ FiniteField 17)) +(declare-const c (_ FiniteField 17)) (declare-const eq (-> (! Type :var T :implicit) T T Bool)) diff --git a/tests/ite-compile-test.smt3 b/tests/ite-compile-test.smt3 index aa8692ca..b7263492 100644 --- a/tests/ite-compile-test.smt3 +++ b/tests/ite-compile-test.smt3 @@ -25,7 +25,7 @@ ) ) -(declare-fun f (Int) Int) +(declare-const f (-> Int Int)) (declare-rule eval_factorial ((x Int)) @@ -35,7 +35,7 @@ (step @p0 (= (f 4) 24) :rule eval_factorial :args (4)) -(declare-fun e (Int) Int) +(declare-const e (-> Int Int)) (declare-rule eval_check_sign ((x Int)) :args (x) diff --git a/tests/literals.smt3 b/tests/literals.smt3 index 39ded750..a56551ff 100644 --- a/tests/literals.smt3 +++ b/tests/literals.smt3 @@ -29,8 +29,8 @@ :conclusion (select i (and f g)) ) -(declare-fun P () Bool) -(declare-fun Q () Bool) +(declare-const P Bool) +(declare-const Q Bool) (assume a0 (and P Q)) (step a1 Q :rule and_elim :premises (a0) :args (1)) diff --git a/tests/mutual-rec.smt3 b/tests/mutual-rec.smt3 index 187512a9..8a5c6dbc 100644 --- a/tests/mutual-rec.smt3 +++ b/tests/mutual-rec.smt3 @@ -24,8 +24,8 @@ ) ) -(declare-fun not (Bool) Bool) -(declare-fun pred_is_even (Int) Bool) +(declare-const not (-> Bool Bool)) +(declare-const pred_is_even (-> Int Bool)) (declare-rule find_is_even ((n Int)) :args (n) diff --git a/tests/nat-type.smt3 b/tests/nat-type.smt3 index 742175d3..d651fa56 100644 --- a/tests/nat-type.smt3 +++ b/tests/nat-type.smt3 @@ -2,7 +2,7 @@ (declare-consts (! Nat :requires ((alf.is_neg alf.self) false))) -(declare-fun f (Nat) Bool) +(declare-const f (-> Nat Bool)) (assume @p0 (f 0)) ;(assume @p0 (f (alf.neg 1))) diff --git a/tests/pf-haniel.smt3 b/tests/pf-haniel.smt3 index 51fa5602..c48eb494 100644 --- a/tests/pf-haniel.smt3 +++ b/tests/pf-haniel.smt3 @@ -2,14 +2,14 @@ (include "Builtin-rules.smt3") (include "Booleans-rules.smt3") (declare-sort U 0) -(declare-fun f (U U) U) -(declare-fun p2 () Bool) -(declare-fun p3 () Bool) -(declare-fun p1 () Bool) -(declare-fun c () U) -(declare-fun d () U) -(declare-fun a () U) -(declare-fun b () U) +(declare-const f (-> U U U)) +(declare-const p2 Bool) +(declare-const p3 Bool) +(declare-const p1 Bool) +(declare-const c U) +(declare-const d U) +(declare-const a U) +(declare-const b U) (define @t1 () (= a b)) (define @t2 () (= c d)) (define @t3 () (and p1 true)) diff --git a/tests/premise-list-cong-2.smt3 b/tests/premise-list-cong-2.smt3 index f58c1e26..3a4f5816 100644 --- a/tests/premise-list-cong-2.smt3 +++ b/tests/premise-list-cong-2.smt3 @@ -29,7 +29,7 @@ (declare-const b U) (declare-const c U) (declare-const d U) -(declare-fun f (U U) U) +(declare-const f (-> U U U)) (assume @p0 (= a b)) (assume @p1 (= c d)) diff --git a/tests/premise-list-cong.smt3 b/tests/premise-list-cong.smt3 index cd489c08..7b6383cb 100644 --- a/tests/premise-list-cong.smt3 +++ b/tests/premise-list-cong.smt3 @@ -21,7 +21,7 @@ (declare-const b U) (declare-const c U) (declare-const d U) -(declare-fun f (U U) U) +(declare-const f (-> U U U)) (assume @p0 (= a b)) (assume @p1 (= c d)) diff --git a/tests/quant-sk-small.alfc.smt3 b/tests/quant-sk-small.alfc.smt3 index 5d9860ea..792d430c 100644 --- a/tests/quant-sk-small.alfc.smt3 +++ b/tests/quant-sk-small.alfc.smt3 @@ -5,7 +5,7 @@ (define alf.1.x () (alf.var "alf.1.x" Int)) (define x () (alf.var "x" Int)) (define y () (alf.var "y" Int)) -(declare-fun P (Int Int) Bool) +(declare-const P (-> Int Int Bool)) (define @t1 () (forall (@list x y) (P x y))) (define @t2 () (P alf.1.x 5)) (define @t3 () (exists (@list alf.1.x @list.nil) (not @t2))) diff --git a/tests/quoted.smt3 b/tests/quoted.smt3 index 28c1c205..b85e2050 100644 --- a/tests/quoted.smt3 +++ b/tests/quoted.smt3 @@ -12,9 +12,9 @@ (declare-sort Int 0) -(declare-fun x () Int) -(declare-fun y () Int) -(declare-fun c () Bool) +(declare-const x Int) +(declare-const y Int) +(declare-const c Bool) (step a5 (= Bool (= Int x y) (= Int y x)) :rule eq-symm-taut :premises () :args ((= Int x y))) ;(step a6 (= Bool (= Int x y) (= Int y x)) :rule eq-symm-taut :premises () :args (x)) diff --git a/tests/requires.smt3 b/tests/requires.smt3 index fcf3d5bd..7250d30a 100644 --- a/tests/requires.smt3 +++ b/tests/requires.smt3 @@ -22,8 +22,8 @@ ) -(declare-fun P () Bool) -(declare-fun Q () Bool) +(declare-const P Bool) +(declare-const Q Bool) (assume a0 (and P Q)) (step a1 P :rule and_elim :premises (a0) :args (i0)) diff --git a/tests/simple-pf.smt3 b/tests/simple-pf.smt3 index af0a9338..e5a028c6 100644 --- a/tests/simple-pf.smt3 +++ b/tests/simple-pf.smt3 @@ -9,9 +9,9 @@ (declare-sort Int 0) -(declare-fun a () Int) -(declare-fun b () Int) -(declare-fun c () Bool) +(declare-const a Int) +(declare-const b Int) +(declare-const c Bool) (assume a1 (= Int a b)) (step a2 (= Int b a) :rule eq-symm :premises (a1) :args ()) diff --git a/tests/simple-pf2.smt3 b/tests/simple-pf2.smt3 index 92edbedf..6139ff80 100644 --- a/tests/simple-pf2.smt3 +++ b/tests/simple-pf2.smt3 @@ -15,9 +15,9 @@ ) (declare-sort Int 0) -(declare-fun x () Int) -(declare-fun y () Int) -(declare-fun c () Bool) +(declare-const x Int) +(declare-const y Int) +(declare-const c Bool) (assume a1 (= Int x y)) (assume a2 (not (= Int y x))) (step a3 (= Int y x) :rule eq-symm :premises (a1) :args ()) diff --git a/tests/simple.smt3 b/tests/simple.smt3 index 2c35f61a..103ab34d 100644 --- a/tests/simple.smt3 +++ b/tests/simple.smt3 @@ -1,3 +1,3 @@ (declare-sort Int 0) -(declare-fun x () Int) +(declare-const x Int) (define y () x :type Int) diff --git a/tests/strings-rules-test.smt3 b/tests/strings-rules-test.smt3 index 003f4e64..e0a1295b 100644 --- a/tests/strings-rules-test.smt3 +++ b/tests/strings-rules-test.smt3 @@ -15,10 +15,10 @@ (string_from_flat_form U ts rev))))) ) -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) -(declare-fun w () String) +(declare-const x String) +(declare-const y String) +(declare-const z String) +(declare-const w String) (assume @p0 (= (str.++ x y) (str.++ x z))) (step @q0 (= y z) :rule concat_eq :premises (@p0) :args (String false)) diff --git a/tests/use-match.smt3 b/tests/use-match.smt3 index ef857514..93be533c 100644 --- a/tests/use-match.smt3 +++ b/tests/use-match.smt3 @@ -65,5 +65,5 @@ ) ) -(declare-fun x () String) +(declare-const x String) (step @p0 (= (str.++ "A" "B" x) (str.++ "AB" x)) :rule collect_acc :args ((str.++ "A" "B" x))) diff --git a/user_manual.md b/user_manual.md index 8b2b93a7..ddda510d 100644 --- a/user_manual.md +++ b/user_manual.md @@ -404,7 +404,7 @@ where the type of its pairwise operator is `(-> S S S)`, and that operator has b (declare-const @nil @List) (declare-const @cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @nil) (declare-const forall (-> @List Bool Bool) :binder @cons) -(declare-fun P (Int) Bool) +(declare-const P (-> Int Bool)) (define Q1 () (forall ((x Int)) (P x))) (define Q2 () (forall ((x Int)) (P x))) @@ -463,7 +463,7 @@ The following gives an example of how to define the class of numeral constants. ``` (declare-sort Int 0) (declare-consts Int) -(declare-fun P ((x Int)) Bool (> x 7)) +(define P ((x Int)) (> x 7)) ``` In the above example, the `declare-consts` command specifies that numerals (`1`, `2`, `3`, and so on) are constants of type `Int`. @@ -788,8 +788,8 @@ for the term `or` applied to arguments `a,b`. (BitVec m) (BitVec (alf.add n m)))) -(declare-fun x () (BitVec 2)) -(declare-fun y () (BitVec 3)) +(declare-const x (BitVec 2)) +(declare-const y (BitVec 3)) (define z () (concat x y) :type (BitVec 5)) ``` @@ -802,8 +802,8 @@ If on the other hand we defined: ... (declare-const a Int) (declare-const b Int) -(declare-fun x2 () (BitVec a)) -(declare-fun y2 () (BitVec b)) +(declare-const x2 (BitVec a)) +(declare-const y2 (BitVec b)) (define z2 () (concat x2 y2)) ``` The type `z2` in the above example is `(BitVec (alf.add a b))`, where the application of `alf.add` does not evaluate. From 0f8ad118fa8985aea360259d4bbde2ecac8ed566 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 15:51:59 -0500 Subject: [PATCH 2/9] More towards --- tests/Arith-theory.smt3 | 4 ++-- tests/arith-eval.smt3 | 4 ++-- tests/arity-overload.smt3 | 2 +- tests/beta-reduce-define-fun.smt3 | 2 +- tests/binder-ex.smt3 | 2 +- tests/binder-subterm-share.smt3 | 2 +- tests/bv-concat.smt3 | 2 +- tests/bv-dep-type.smt3 | 10 +++++----- tests/bv-eval.smt3 | 2 +- tests/bv-extract-smt3.smt3 | 2 +- tests/bv-extract.smt3 | 2 +- tests/bv-literals.smt3 | 2 +- tests/bv-type-strict.smt3 | 2 +- tests/constant-eval-args.smt3 | 2 +- tests/constant-eval.smt3 | 2 +- tests/define-sort-iarray.smt3 | 2 +- tests/distinct_value_testers.smt3 | 4 ++-- tests/eval-inc.smt3 | 2 +- tests/evaluate.smt3 | 6 +++--- tests/evaluation.smt3 | 2 +- tests/ff-nil.smt3 | 2 +- tests/generic-swap.smt3 | 2 +- tests/gt_eval.smt3 | 2 +- tests/ite-compile-test.smt3 | 2 +- tests/literals.smt3 | 2 +- tests/match-simple.smt3 | 2 +- tests/match-variants.smt3 | 2 +- tests/mixed-arith.smt3 | 4 ++-- tests/mutual-rec.smt3 | 2 +- tests/nground-nil-v3.smt3 | 2 +- tests/opaque-inst.smt3 | 2 +- tests/opaque-inst2.smt3 | 2 +- tests/oracle-ex.smt3 | 2 +- tests/oracle-ex2.smt3 | 2 +- tests/overloading-as.smt3 | 2 +- tests/overloading.smt3 | 4 ++-- tests/pairwise.smt3 | 2 +- tests/par-dt.smt3 | 2 +- tests/pf-haniel.smt3 | 2 +- tests/pf-quant.smt3 | 2 +- tests/pf-simple-sig-2.smt3 | 6 +++--- tests/pf-simple-sig.smt3 | 8 ++++---- tests/premise-list-cong-2.smt3 | 2 +- tests/premise-list-cong.smt3 | 2 +- tests/push-pop.smt3 | 2 +- tests/quoted.smt3 | 2 +- tests/requires.smt3 | 2 +- tests/right-assoc-variants.smt3 | 4 ++-- tests/simple-pf-implicit.smt3 | 8 ++++---- tests/simple-pf.smt3 | 2 +- tests/simple-pf2.smt3 | 2 +- tests/simple-program.smt3 | 2 +- tests/simple.smt3 | 2 +- tests/str-eval.smt3 | 2 +- tests/substitution-opaque.smt3 | 2 +- tests/tiny_oracle.smt3 | 2 +- tests/to_string.smt3 | 2 +- tests/typeof.smt3 | 4 ++-- 58 files changed, 79 insertions(+), 79 deletions(-) diff --git a/tests/Arith-theory.smt3 b/tests/Arith-theory.smt3 index 09c1d93c..2912324d 100644 --- a/tests/Arith-theory.smt3 +++ b/tests/Arith-theory.smt3 @@ -1,7 +1,7 @@ (include "Builtin-theory.smt3") -(declare-sort Int 0) -(declare-sort Real 0) +(declare-type Int ()) +(declare-type Real ()) (declare-consts Int) (declare-consts Real) diff --git a/tests/arith-eval.smt3 b/tests/arith-eval.smt3 index 9f86a7c8..61c15ecd 100644 --- a/tests/arith-eval.smt3 +++ b/tests/arith-eval.smt3 @@ -1,5 +1,5 @@ -(declare-sort Int 0) -(declare-sort Real 0) +(declare-type Int ()) +(declare-type Real ()) (declare-consts Int) (declare-consts Real) diff --git a/tests/arity-overload.smt3 b/tests/arity-overload.smt3 index 14837a77..d6167bcd 100644 --- a/tests/arity-overload.smt3 +++ b/tests/arity-overload.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-const - (-> Int Int)) (declare-const - (-> Int Int Int)) diff --git a/tests/beta-reduce-define-fun.smt3 b/tests/beta-reduce-define-fun.smt3 index 3d1ddcdd..73cb724d 100644 --- a/tests/beta-reduce-define-fun.smt3 +++ b/tests/beta-reduce-define-fun.smt3 @@ -4,7 +4,7 @@ (declare-const not (-> Bool Bool)) -(declare-sort U 0) +(declare-type U ()) (define f_true ((x U)) true) diff --git a/tests/binder-ex.smt3 b/tests/binder-ex.smt3 index 684ede18..7c0e8c89 100644 --- a/tests/binder-ex.smt3 +++ b/tests/binder-ex.smt3 @@ -2,7 +2,7 @@ (declare-const @list.nil @List) (declare-const @list.cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil) -(declare-sort Int 0) +(declare-type Int ()) (declare-const P (-> Int Bool)) (declare-const forall (-> @List Bool Bool) :binder @list.cons) diff --git a/tests/binder-subterm-share.smt3 b/tests/binder-subterm-share.smt3 index 37f429e5..c223c634 100644 --- a/tests/binder-subterm-share.smt3 +++ b/tests/binder-subterm-share.smt3 @@ -2,7 +2,7 @@ (declare-const @list.nil @List) (declare-const @list.cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil) -(declare-sort Int 0) +(declare-type Int ()) (declare-const P (-> Int Bool)) (declare-const forall (-> @List Bool Bool) :binder @list.cons) (declare-rule id ((y Bool)) :premises (y) :conclusion y) diff --git a/tests/bv-concat.smt3 b/tests/bv-concat.smt3 index 8f2aa741..1f08833d 100644 --- a/tests/bv-concat.smt3 +++ b/tests/bv-concat.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-type BitVec (Int)) diff --git a/tests/bv-dep-type.smt3 b/tests/bv-dep-type.smt3 index 53bd0708..5837d5a8 100644 --- a/tests/bv-dep-type.smt3 +++ b/tests/bv-dep-type.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-type BitVec (Int)) @@ -8,9 +8,9 @@ (BitVec n) (BitVec n))) -(declare-fun m () Int) -(declare-fun dummy () Int) +(declare-const m Int) +(declare-const dummy Int) -(declare-fun x () (BitVec m)) -(declare-fun y () (BitVec m)) +(declare-const x (BitVec m)) +(declare-const y (BitVec m)) (define z () (bvadd m x y) :type (BitVec m)) diff --git a/tests/bv-eval.smt3 b/tests/bv-eval.smt3 index 245dec23..85f0faa2 100644 --- a/tests/bv-eval.smt3 +++ b/tests/bv-eval.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const = (-> (! Type :var T :implicit) T T Bool)) diff --git a/tests/bv-extract-smt3.smt3 b/tests/bv-extract-smt3.smt3 index f29909db..2c8e80de 100644 --- a/tests/bv-extract-smt3.smt3 +++ b/tests/bv-extract-smt3.smt3 @@ -1,7 +1,7 @@ (declare-const = (-> (! Type :var A :implicit) A A Bool)) (declare-const and (-> Bool Bool Bool) :left-assoc) -(declare-sort Int 0) +(declare-type Int ()) (declare-const < (-> Int Int Bool)) (declare-const <= (-> Int Int Bool) :chainable and) (declare-const - (-> Int Int Int)) diff --git a/tests/bv-extract.smt3 b/tests/bv-extract.smt3 index 34e4092e..17fc85a4 100644 --- a/tests/bv-extract.smt3 +++ b/tests/bv-extract.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const BitVec (-> Int Type)) diff --git a/tests/bv-literals.smt3 b/tests/bv-literals.smt3 index 879bb859..b8004fa7 100644 --- a/tests/bv-literals.smt3 +++ b/tests/bv-literals.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const = (-> (! Type :var T :implicit) T T Bool)) diff --git a/tests/bv-type-strict.smt3 b/tests/bv-type-strict.smt3 index 3ba2beb3..609e39e7 100644 --- a/tests/bv-type-strict.smt3 +++ b/tests/bv-type-strict.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const = (-> (! Type :var T :implicit) T T Bool)) diff --git a/tests/constant-eval-args.smt3 b/tests/constant-eval-args.smt3 index 9cadfaca..7724c405 100644 --- a/tests/constant-eval-args.smt3 +++ b/tests/constant-eval-args.smt3 @@ -1,5 +1,5 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (program less-than () diff --git a/tests/constant-eval.smt3 b/tests/constant-eval.smt3 index c3027c7d..2263b4d9 100644 --- a/tests/constant-eval.smt3 +++ b/tests/constant-eval.smt3 @@ -1,6 +1,6 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (program less-than () diff --git a/tests/define-sort-iarray.smt3 b/tests/define-sort-iarray.smt3 index 0eb698ee..2b822321 100644 --- a/tests/define-sort-iarray.smt3 +++ b/tests/define-sort-iarray.smt3 @@ -1,7 +1,7 @@ (declare-const = (-> (! Type :var T :implicit) T T Bool)) (declare-sort Array 2) -(declare-sort Int 0) +(declare-type Int ()) (define IntArray ((T Type)) (Array Int T)) (declare-const a (Array Int Bool)) (declare-const b (IntArray Bool)) diff --git a/tests/distinct_value_testers.smt3 b/tests/distinct_value_testers.smt3 index 9ba4d2ec..18ca344a 100644 --- a/tests/distinct_value_testers.smt3 +++ b/tests/distinct_value_testers.smt3 @@ -7,7 +7,7 @@ :conclusion (not (= t s)) ) -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-rule disinct_value_int ((t Int) (s Int)) @@ -16,7 +16,7 @@ :conclusion (not (= t s)) ) -(declare-sort Real 0) +(declare-type Real ()) (declare-consts Real) (declare-rule disinct_value_real ((t Real) (s Real)) diff --git a/tests/eval-inc.smt3 b/tests/eval-inc.smt3 index f1e0141f..cbe17b4a 100644 --- a/tests/eval-inc.smt3 +++ b/tests/eval-inc.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) diff --git a/tests/evaluate.smt3 b/tests/evaluate.smt3 index ee01dbcc..87f31be3 100644 --- a/tests/evaluate.smt3 +++ b/tests/evaluate.smt3 @@ -1,5 +1,5 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-const and (-> Bool Bool Bool)) (declare-const i0 Int) @@ -21,7 +21,7 @@ ) -(declare-fun P () Bool) -(declare-fun Q () Bool) +(declare-const P Bool) +(declare-const Q Bool) (assume a0 (and P Q)) (step a1 P :rule and_elim :premises (a0) :args (i0)) diff --git a/tests/evaluation.smt3 b/tests/evaluation.smt3 index 696bbc92..d15b7279 100644 --- a/tests/evaluation.smt3 +++ b/tests/evaluation.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) diff --git a/tests/ff-nil.smt3 b/tests/ff-nil.smt3 index af059d7f..06f7bc17 100644 --- a/tests/ff-nil.smt3 +++ b/tests/ff-nil.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const FiniteField (-> Int Type)) diff --git a/tests/generic-swap.smt3 b/tests/generic-swap.smt3 index b10f06c8..17e006c2 100644 --- a/tests/generic-swap.smt3 +++ b/tests/generic-swap.smt3 @@ -19,7 +19,7 @@ :conclusion (is_swap t (swap t)) ) -(declare-sort Int 0) +(declare-type Int ()) (declare-const a Int) (declare-const b Int) diff --git a/tests/gt_eval.smt3 b/tests/gt_eval.smt3 index f6a4643c..9893f4a5 100644 --- a/tests/gt_eval.smt3 +++ b/tests/gt_eval.smt3 @@ -1,5 +1,5 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const > (-> Int Int Bool)) diff --git a/tests/ite-compile-test.smt3 b/tests/ite-compile-test.smt3 index b7263492..edba9525 100644 --- a/tests/ite-compile-test.smt3 +++ b/tests/ite-compile-test.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const + (-> Int Int Int)) (declare-const - (-> Int Int Int)) diff --git a/tests/literals.smt3 b/tests/literals.smt3 index a56551ff..46df88a5 100644 --- a/tests/literals.smt3 +++ b/tests/literals.smt3 @@ -1,6 +1,6 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const and (-> Bool Bool Bool)) diff --git a/tests/match-simple.smt3 b/tests/match-simple.smt3 index 49124005..6c9ae0ab 100644 --- a/tests/match-simple.smt3 +++ b/tests/match-simple.smt3 @@ -1,7 +1,7 @@ (declare-const => (-> Bool Bool Bool)) -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-type Pair (Type Type)) diff --git a/tests/match-variants.smt3 b/tests/match-variants.smt3 index f2c2e0e5..59d546ba 100644 --- a/tests/match-variants.smt3 +++ b/tests/match-variants.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-const a Int) (declare-const b Int) (declare-const P (-> Int Bool)) diff --git a/tests/mixed-arith.smt3 b/tests/mixed-arith.smt3 index 4c26f359..d09f0518 100644 --- a/tests/mixed-arith.smt3 +++ b/tests/mixed-arith.smt3 @@ -1,5 +1,5 @@ -(declare-sort Int 0) -(declare-sort Real 0) +(declare-type Int ()) +(declare-type Real ()) (declare-consts Int) (declare-consts Real) diff --git a/tests/mutual-rec.smt3 b/tests/mutual-rec.smt3 index 8a5c6dbc..42230df9 100644 --- a/tests/mutual-rec.smt3 +++ b/tests/mutual-rec.smt3 @@ -1,6 +1,6 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) ; forward declaration diff --git a/tests/nground-nil-v3.smt3 b/tests/nground-nil-v3.smt3 index 9a72cff5..214fff1e 100644 --- a/tests/nground-nil-v3.smt3 +++ b/tests/nground-nil-v3.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const BitVec (-> Int Type)) diff --git a/tests/opaque-inst.smt3 b/tests/opaque-inst.smt3 index 3d77d216..2036394e 100644 --- a/tests/opaque-inst.smt3 +++ b/tests/opaque-inst.smt3 @@ -8,7 +8,7 @@ (declare-const not (-> Bool Bool)) (declare-sort Array 2) -(declare-sort Int 0) +(declare-type Int ()) (declare-const select (-> (Array Int Int) Int Int)) diff --git a/tests/opaque-inst2.smt3 b/tests/opaque-inst2.smt3 index f84c2797..0b28075c 100644 --- a/tests/opaque-inst2.smt3 +++ b/tests/opaque-inst2.smt3 @@ -8,7 +8,7 @@ (declare-const not (-> Bool Bool)) (declare-sort Array 2) -(declare-sort Int 0) +(declare-type Int ()) (declare-const select (-> (Array Int Int) Int Int)) diff --git a/tests/oracle-ex.smt3 b/tests/oracle-ex.smt3 index 1417c4a3..ac6d5b4a 100644 --- a/tests/oracle-ex.smt3 +++ b/tests/oracle-ex.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-sort String 0) (declare-consts String) diff --git a/tests/oracle-ex2.smt3 b/tests/oracle-ex2.smt3 index e4992dcd..9b433c95 100644 --- a/tests/oracle-ex2.smt3 +++ b/tests/oracle-ex2.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-sort String 0) (declare-consts String) diff --git a/tests/overloading-as.smt3 b/tests/overloading-as.smt3 index 3ef1b075..0efdc1f3 100644 --- a/tests/overloading-as.smt3 +++ b/tests/overloading-as.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-const - (-> Int Int Int)) (declare-const - (-> Int Int)) diff --git a/tests/overloading.smt3 b/tests/overloading.smt3 index dd6a0d85..2a0e1bb3 100644 --- a/tests/overloading.smt3 +++ b/tests/overloading.smt3 @@ -1,5 +1,5 @@ -(declare-sort Int 0) -(declare-sort Real 0) +(declare-type Int ()) +(declare-type Real ()) (program a.typeunion () (Type Type) Type diff --git a/tests/pairwise.smt3 b/tests/pairwise.smt3 index 5d4d8d5f..d919ed00 100644 --- a/tests/pairwise.smt3 +++ b/tests/pairwise.smt3 @@ -11,7 +11,7 @@ :conclusion a ) -(declare-sort U 0) +(declare-type U ()) (declare-const a U) (declare-const b U) diff --git a/tests/par-dt.smt3 b/tests/par-dt.smt3 index 6c3b5b51..dbcbd803 100644 --- a/tests/par-dt.smt3 +++ b/tests/par-dt.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-datatypes ((List 1)) ((par (T) ((nil) (cons (head T) (tail (List T))))))) (define y () (alf.var "y" (List Int))) (define @t1 () (tail y) :type (List Int)) diff --git a/tests/pf-haniel.smt3 b/tests/pf-haniel.smt3 index c48eb494..d51f7c05 100644 --- a/tests/pf-haniel.smt3 +++ b/tests/pf-haniel.smt3 @@ -1,7 +1,7 @@ (include "Uf-rules.smt3") (include "Builtin-rules.smt3") (include "Booleans-rules.smt3") -(declare-sort U 0) +(declare-type U ()) (declare-const f (-> U U U)) (declare-const p2 Bool) (declare-const p3 Bool) diff --git a/tests/pf-quant.smt3 b/tests/pf-quant.smt3 index c198f2a3..3fb56e1f 100644 --- a/tests/pf-quant.smt3 +++ b/tests/pf-quant.smt3 @@ -1,6 +1,6 @@ (include "./quant.smt3") -(declare-sort Int 0) +(declare-type Int ()) (define x1 () (alf.var "x1" Int)) (declare-const a Int) diff --git a/tests/pf-simple-sig-2.smt3 b/tests/pf-simple-sig-2.smt3 index 0c32afcd..f525ec63 100644 --- a/tests/pf-simple-sig-2.smt3 +++ b/tests/pf-simple-sig-2.smt3 @@ -1,8 +1,8 @@ (include "./simple-sig-2.smt3") -(declare-sort Int 0) -(declare-fun a () Int) -(declare-fun b () Int) +(declare-type Int ()) +(declare-const a Int) +(declare-const b Int) (assume a1 (= a b)) (step a2 (= b a) :rule eq-symm-flip :premises (a1)) diff --git a/tests/pf-simple-sig.smt3 b/tests/pf-simple-sig.smt3 index 2409d3a4..aa3d48a6 100644 --- a/tests/pf-simple-sig.smt3 +++ b/tests/pf-simple-sig.smt3 @@ -1,10 +1,10 @@ (include "./simple-sig.smt3") -(declare-sort Int 0) -(declare-fun a () Int) -(declare-fun b () Int) -(declare-fun c () Bool) +(declare-type Int ()) +(declare-const a Int) +(declare-const b Int) +(declare-const c Bool) (assume a1 (= a b)) (assume a2 (not (= b a))) (step a3 (= b a) :rule eq-symm :premises (a1) :args ()) diff --git a/tests/premise-list-cong-2.smt3 b/tests/premise-list-cong-2.smt3 index 3a4f5816..290dd01c 100644 --- a/tests/premise-list-cong-2.smt3 +++ b/tests/premise-list-cong-2.smt3 @@ -24,7 +24,7 @@ ) -(declare-sort U 0) +(declare-type U ()) (declare-const a U) (declare-const b U) (declare-const c U) diff --git a/tests/premise-list-cong.smt3 b/tests/premise-list-cong.smt3 index 7b6383cb..2b0ccf9b 100644 --- a/tests/premise-list-cong.smt3 +++ b/tests/premise-list-cong.smt3 @@ -16,7 +16,7 @@ :conclusion (mk_cong_eq (= f f) E) ) -(declare-sort U 0) +(declare-type U ()) (declare-const a U) (declare-const b U) (declare-const c U) diff --git a/tests/push-pop.smt3 b/tests/push-pop.smt3 index 76ee0717..3124599a 100644 --- a/tests/push-pop.smt3 +++ b/tests/push-pop.smt3 @@ -7,7 +7,7 @@ :conclusion (= t t) ) -(declare-sort Int 0) +(declare-type Int ()) (declare-const b Int) (push) diff --git a/tests/quoted.smt3 b/tests/quoted.smt3 index b85e2050..2f717946 100644 --- a/tests/quoted.smt3 +++ b/tests/quoted.smt3 @@ -11,7 +11,7 @@ :conclusion (= Bool (= T x y) (= T y x))) -(declare-sort Int 0) +(declare-type Int ()) (declare-const x Int) (declare-const y Int) (declare-const c Bool) diff --git a/tests/requires.smt3 b/tests/requires.smt3 index 7250d30a..8f21b487 100644 --- a/tests/requires.smt3 +++ b/tests/requires.smt3 @@ -1,5 +1,5 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-const and (-> Bool Bool Bool)) (declare-const i0 Int) diff --git a/tests/right-assoc-variants.smt3 b/tests/right-assoc-variants.smt3 index 12291482..10ab4d80 100644 --- a/tests/right-assoc-variants.smt3 +++ b/tests/right-assoc-variants.smt3 @@ -1,6 +1,6 @@ -(declare-sort Int 0) -(declare-sort Real 0) +(declare-type Int ()) +(declare-type Real ()) (declare-const BitVec (-> Int Type)) (declare-sort String 0) (declare-type Seq (Type)) diff --git a/tests/simple-pf-implicit.smt3 b/tests/simple-pf-implicit.smt3 index 810437ec..426371f4 100644 --- a/tests/simple-pf-implicit.smt3 +++ b/tests/simple-pf-implicit.smt3 @@ -8,9 +8,9 @@ :conclusion (= y x)) -(declare-sort Int 0) -(declare-fun a () Int) -(declare-fun b () Int) -(declare-fun c () Bool) +(declare-type Int ()) +(declare-const a Int) +(declare-const b Int) +(declare-const c Bool) (assume a1 (= a b)) (step a2 (= b a) :rule eq-symm :premises (a1) :args ()) diff --git a/tests/simple-pf.smt3 b/tests/simple-pf.smt3 index e5a028c6..4ae418a6 100644 --- a/tests/simple-pf.smt3 +++ b/tests/simple-pf.smt3 @@ -8,7 +8,7 @@ :conclusion (= T y x)) -(declare-sort Int 0) +(declare-type Int ()) (declare-const a Int) (declare-const b Int) (declare-const c Bool) diff --git a/tests/simple-pf2.smt3 b/tests/simple-pf2.smt3 index 6139ff80..7fbe6619 100644 --- a/tests/simple-pf2.smt3 +++ b/tests/simple-pf2.smt3 @@ -14,7 +14,7 @@ :conclusion false ) -(declare-sort Int 0) +(declare-type Int ()) (declare-const x Int) (declare-const y Int) (declare-const c Bool) diff --git a/tests/simple-program.smt3 b/tests/simple-program.smt3 index 73f00d1b..5af795e8 100644 --- a/tests/simple-program.smt3 +++ b/tests/simple-program.smt3 @@ -1,5 +1,5 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-const and (-> Bool Bool Bool)) (declare-const i0 Int) diff --git a/tests/simple.smt3 b/tests/simple.smt3 index 103ab34d..6734c8b4 100644 --- a/tests/simple.smt3 +++ b/tests/simple.smt3 @@ -1,3 +1,3 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-const x Int) (define y () x :type Int) diff --git a/tests/str-eval.smt3 b/tests/str-eval.smt3 index bd964b9c..0df8f467 100644 --- a/tests/str-eval.smt3 +++ b/tests/str-eval.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const = (-> (! Type :var T :implicit) T T Bool)) diff --git a/tests/substitution-opaque.smt3 b/tests/substitution-opaque.smt3 index 09e88b3c..7e18d247 100644 --- a/tests/substitution-opaque.smt3 +++ b/tests/substitution-opaque.smt3 @@ -27,7 +27,7 @@ (declare-const not (-> Bool Bool)) (declare-sort Array 2) -(declare-sort Int 0) +(declare-type Int ()) (declare-const @array_deq_diff (-> diff --git a/tests/tiny_oracle.smt3 b/tests/tiny_oracle.smt3 index b8e637aa..4d60eebd 100644 --- a/tests/tiny_oracle.smt3 +++ b/tests/tiny_oracle.smt3 @@ -1,4 +1,4 @@ -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-oracle-fun test_oracle (Int) Bool ./tiny_oracle.sh) diff --git a/tests/to_string.smt3 b/tests/to_string.smt3 index 7f534093..aaec3af9 100644 --- a/tests/to_string.smt3 +++ b/tests/to_string.smt3 @@ -2,7 +2,7 @@ ; we can't do options in regression tests, these pass with: ; `--no-normalize-dec --no-normalize-hex` -(declare-sort Real 0) +(declare-type Real ()) (declare-consts Real) ;(declare-consts Real) (declare-sort BitVec 0) diff --git a/tests/typeof.smt3 b/tests/typeof.smt3 index 3002c193..2073e499 100644 --- a/tests/typeof.smt3 +++ b/tests/typeof.smt3 @@ -1,9 +1,9 @@ (declare-const = (-> (! Type :var A :implicit) A A Bool)) -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) -(declare-sort Real 0) +(declare-type Real ()) (declare-consts Real) (declare-const to_real (-> Int Real)) From 862f3fc6e84f1b5f917d1a5bd06769c15c45b86f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 16:01:20 -0500 Subject: [PATCH 3/9] Finish updates to tests --- tests/Sets-theory.smt3 | 2 +- tests/Strings-theory.smt3 | 4 ++-- tests/Utils.smt3 | 2 +- tests/binder-ex.smt3 | 2 +- tests/binder-subterm-share.smt3 | 2 +- tests/define-sort-iarray.smt3 | 2 +- tests/distinct_value_testers.smt3 | 4 ++-- tests/generic-swap.smt3 | 2 +- tests/gt_eval.smt3 | 2 +- tests/nat-type.smt3 | 2 +- tests/opaque-inst.smt3 | 2 +- tests/opaque-inst2.smt3 | 2 +- tests/oracle-ex.smt3 | 2 +- tests/oracle-ex2.smt3 | 2 +- tests/right-assoc-variants.smt3 | 2 +- tests/self-requires.smt3 | 2 +- tests/str-eval.smt3 | 2 +- tests/substitution-opaque.smt3 | 2 +- tests/to_string.smt3 | 4 ++-- tests/use-match.smt3 | 2 +- tests/var-binders-syntax.smt3 | 2 +- 21 files changed, 24 insertions(+), 24 deletions(-) diff --git a/tests/Sets-theory.smt3 b/tests/Sets-theory.smt3 index b13e4bad..ebb38747 100644 --- a/tests/Sets-theory.smt3 +++ b/tests/Sets-theory.smt3 @@ -2,7 +2,7 @@ (include "Arith-theory.smt3") (include "Datatypes-theory.smt3") -(declare-sort Set 1) +(declare-type Set (Type)) ; NOTE: permits non-set types (declare-const set.empty (-> (! Type :var T) T)) diff --git a/tests/Strings-theory.smt3 b/tests/Strings-theory.smt3 index 0beedb51..b196c362 100644 --- a/tests/Strings-theory.smt3 +++ b/tests/Strings-theory.smt3 @@ -1,9 +1,9 @@ (include "Builtin-theory.smt3") (include "Arith-theory.smt3") -(declare-sort RegLan 0) +(declare-type RegLan ()) (declare-type Seq (Type)) -(declare-sort Char 0) +(declare-type Char ()) (define String () (Seq Char)) (declare-consts String) diff --git a/tests/Utils.smt3 b/tests/Utils.smt3 index 7848c3e3..2a2eb8e8 100644 --- a/tests/Utils.smt3 +++ b/tests/Utils.smt3 @@ -26,7 +26,7 @@ ) ; untyped list -(declare-sort @List 0) +(declare-type @List ()) (declare-const @list.nil @List) (declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil) diff --git a/tests/binder-ex.smt3 b/tests/binder-ex.smt3 index 7c0e8c89..faa79c31 100644 --- a/tests/binder-ex.smt3 +++ b/tests/binder-ex.smt3 @@ -1,4 +1,4 @@ -(declare-sort @List 0) +(declare-type @List ()) (declare-const @list.nil @List) (declare-const @list.cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil) diff --git a/tests/binder-subterm-share.smt3 b/tests/binder-subterm-share.smt3 index c223c634..981f7912 100644 --- a/tests/binder-subterm-share.smt3 +++ b/tests/binder-subterm-share.smt3 @@ -1,4 +1,4 @@ -(declare-sort @List 0) +(declare-type @List ()) (declare-const @list.nil @List) (declare-const @list.cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil) diff --git a/tests/define-sort-iarray.smt3 b/tests/define-sort-iarray.smt3 index 2b822321..e59403c0 100644 --- a/tests/define-sort-iarray.smt3 +++ b/tests/define-sort-iarray.smt3 @@ -1,6 +1,6 @@ (declare-const = (-> (! Type :var T :implicit) T T Bool)) -(declare-sort Array 2) +(declare-type Array (Type Type)) (declare-type Int ()) (define IntArray ((T Type)) (Array Int T)) (declare-const a (Array Int Bool)) diff --git a/tests/distinct_value_testers.smt3 b/tests/distinct_value_testers.smt3 index 18ca344a..b5398d2b 100644 --- a/tests/distinct_value_testers.smt3 +++ b/tests/distinct_value_testers.smt3 @@ -26,7 +26,7 @@ ) -(declare-sort String 0) +(declare-type String ()) (declare-consts String) (declare-rule disinct_value_str ((t String) (s String)) @@ -35,7 +35,7 @@ :conclusion (not (= t s)) ) -(declare-sort Bin 0) +(declare-type Bin ()) (declare-consts Bin) (declare-rule disinct_value_bin ((t Bin) (s Bin)) diff --git a/tests/generic-swap.smt3 b/tests/generic-swap.smt3 index 17e006c2..1f2bb521 100644 --- a/tests/generic-swap.smt3 +++ b/tests/generic-swap.smt3 @@ -1,4 +1,4 @@ -(declare-sort Pair 1) +(declare-type Pair (Type)) (declare-const pair (-> (! Type :var T :implicit) T T (Pair T))) diff --git a/tests/gt_eval.smt3 b/tests/gt_eval.smt3 index 9893f4a5..623148c2 100644 --- a/tests/gt_eval.smt3 +++ b/tests/gt_eval.smt3 @@ -9,7 +9,7 @@ :conclusion (> t s) ) -(declare-sort Bin 0) +(declare-type Bin ()) (declare-consts Bin) (declare-const bvugt (-> Bin Bin Bool)) diff --git a/tests/nat-type.smt3 b/tests/nat-type.smt3 index d651fa56..e7759d68 100644 --- a/tests/nat-type.smt3 +++ b/tests/nat-type.smt3 @@ -1,4 +1,4 @@ -(declare-sort Nat 0) +(declare-type Nat ()) (declare-consts (! Nat :requires ((alf.is_neg alf.self) false))) diff --git a/tests/opaque-inst.smt3 b/tests/opaque-inst.smt3 index 2036394e..1a5b0d72 100644 --- a/tests/opaque-inst.smt3 +++ b/tests/opaque-inst.smt3 @@ -7,7 +7,7 @@ (declare-const and (-> Bool Bool Bool) :right-assoc-nil true) (declare-const not (-> Bool Bool)) -(declare-sort Array 2) +(declare-type Array (Type Type)) (declare-type Int ()) (declare-const select (-> (Array Int Int) Int Int)) diff --git a/tests/opaque-inst2.smt3 b/tests/opaque-inst2.smt3 index 0b28075c..9181f381 100644 --- a/tests/opaque-inst2.smt3 +++ b/tests/opaque-inst2.smt3 @@ -7,7 +7,7 @@ (declare-const and (-> Bool Bool Bool) :right-assoc-nil true) (declare-const not (-> Bool Bool)) -(declare-sort Array 2) +(declare-type Array (Type Type)) (declare-type Int ()) (declare-const select (-> (Array Int Int) Int Int)) diff --git a/tests/oracle-ex.smt3 b/tests/oracle-ex.smt3 index ac6d5b4a..f4db66f3 100644 --- a/tests/oracle-ex.smt3 +++ b/tests/oracle-ex.smt3 @@ -1,6 +1,6 @@ (declare-type Int ()) (declare-consts Int) -(declare-sort String 0) +(declare-type String ()) (declare-consts String) (declare-const or (-> Bool Bool Bool) :right-assoc-nil false) (declare-const and (-> Bool Bool Bool) :right-assoc-nil true) diff --git a/tests/oracle-ex2.smt3 b/tests/oracle-ex2.smt3 index 9b433c95..98860d45 100644 --- a/tests/oracle-ex2.smt3 +++ b/tests/oracle-ex2.smt3 @@ -1,6 +1,6 @@ (declare-type Int ()) (declare-consts Int) -(declare-sort String 0) +(declare-type String ()) (declare-consts String) (declare-const or (-> Bool Bool Bool) :right-assoc-nil false) (declare-const and (-> Bool Bool Bool) :right-assoc-nil true) diff --git a/tests/right-assoc-variants.smt3 b/tests/right-assoc-variants.smt3 index 10ab4d80..3ae9ab2c 100644 --- a/tests/right-assoc-variants.smt3 +++ b/tests/right-assoc-variants.smt3 @@ -2,7 +2,7 @@ (declare-type Int ()) (declare-type Real ()) (declare-const BitVec (-> Int Type)) -(declare-sort String 0) +(declare-type String ()) (declare-type Seq (Type)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/tests/self-requires.smt3 b/tests/self-requires.smt3 index 428a883c..58a7395b 100644 --- a/tests/self-requires.smt3 +++ b/tests/self-requires.smt3 @@ -1,3 +1,3 @@ -(declare-sort Nat 0) +(declare-type Nat ()) (declare-consts (! Nat :requires ((alf.is_neg alf.self) false))) diff --git a/tests/str-eval.smt3 b/tests/str-eval.smt3 index 0df8f467..4bad17b4 100644 --- a/tests/str-eval.smt3 +++ b/tests/str-eval.smt3 @@ -15,7 +15,7 @@ ) ) -(declare-sort String 0) +(declare-type String ()) (declare-consts String) (declare-const str.++ (-> String String String)) diff --git a/tests/substitution-opaque.smt3 b/tests/substitution-opaque.smt3 index 7e18d247..5691ab35 100644 --- a/tests/substitution-opaque.smt3 +++ b/tests/substitution-opaque.smt3 @@ -26,7 +26,7 @@ (declare-const and (-> Bool Bool Bool) :right-assoc-nil true) (declare-const not (-> Bool Bool)) -(declare-sort Array 2) +(declare-type Array (Type Type)) (declare-type Int ()) (declare-const @array_deq_diff diff --git a/tests/to_string.smt3 b/tests/to_string.smt3 index aaec3af9..375f0e59 100644 --- a/tests/to_string.smt3 +++ b/tests/to_string.smt3 @@ -5,10 +5,10 @@ (declare-type Real ()) (declare-consts Real) ;(declare-consts Real) -(declare-sort BitVec 0) +(declare-type BitVec ()) (declare-consts BitVec) ;(declare-consts BitVec) -(declare-sort String 0) +(declare-type String ()) (declare-consts String) (declare-const ok (-> (! Type :var T :implicit) T Bool)) diff --git a/tests/use-match.smt3 b/tests/use-match.smt3 index 93be533c..055b67e2 100644 --- a/tests/use-match.smt3 +++ b/tests/use-match.smt3 @@ -20,7 +20,7 @@ ) ) -(declare-sort String 0) +(declare-type String ()) (declare-consts String) (declare-const str.++ (-> String String String) :right-assoc-nil "") diff --git a/tests/var-binders-syntax.smt3 b/tests/var-binders-syntax.smt3 index 357023d5..737ef7f8 100644 --- a/tests/var-binders-syntax.smt3 +++ b/tests/var-binders-syntax.smt3 @@ -1,5 +1,5 @@ -(declare-sort @List 0) +(declare-type @List ()) (declare-const @list.nil @List) (declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil) From bfa2de8b9979a3c8ca9df9a1bacdfee9ea4c530f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 16:10:32 -0500 Subject: [PATCH 4/9] More --- src/cmd_parser.cpp | 13 ----- tests/define-const-simple.smt3 | 2 +- user_manual.md | 89 ++++++++++++++++------------------ 3 files changed, 43 insertions(+), 61 deletions(-) diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index cce7648c..10dd533a 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -33,7 +33,6 @@ CmdParser::CmdParser(Lexer& lex, d_table["declare-const"] = Token::DECLARE_CONST; d_table["declare-datatype"] = Token::DECLARE_DATATYPE; d_table["declare-datatypes"] = Token::DECLARE_DATATYPES; - d_table["define-const"] = Token::DEFINE_CONST; d_table["echo"] = Token::ECHO; d_table["exit"] = Token::EXIT; d_table["pop"] = Token::POP; @@ -462,18 +461,6 @@ bool CmdParser::parseNextCommand() d_eparser.bind(name, decType); } break; - // (define-const ) - case Token::DEFINE_CONST: - { - //d_state.checkThatLogicIsSet(); - std::string name = d_eparser.parseSymbol(); - //d_state.checkUserSymbol(name); - Expr ret = d_eparser.parseType(); - Expr e = d_eparser.parseExpr(); - d_eparser.typeCheck(e, ret); - d_eparser.bind(name, e); - } - break; // (define-fun (*) ) // (define-type (*) ) // (define (*) *) diff --git a/tests/define-const-simple.smt3 b/tests/define-const-simple.smt3 index 86fd6cee..80265630 100644 --- a/tests/define-const-simple.smt3 +++ b/tests/define-const-simple.smt3 @@ -1,7 +1,7 @@ (declare-const not (-> Bool Bool)) -(define-const f_true Bool true) +(define f_true true) (declare-rule trust ((f Bool)) diff --git a/user_manual.md b/user_manual.md index ddda510d..029e18a9 100644 --- a/user_manual.md +++ b/user_manual.md @@ -90,12 +90,8 @@ In the following, we informally write BNF categories `` to denote an SMT The following commands are supported for declaring and defining types and terms. The first set of commands are identical to those in SMT-LIB version 3.0: - `(declare-const *)` declares a constant named `` whose type is ``. Can be given an optional list of attributes (see [attributes](#attributes)). -- `(declare-fun (*) *)` declares a constant named `` whose type is given by the argument types and return type. Can be given an optional list of attributes. -- `(declare-sort )` declares a new type named `` whose kind is `(-> Type^n Type)` if `n>0` or `Type` for the provided numeral `n`. - `(declare-type (*))` declares a new type named `` whose kind is given by the argument types and return type `Type`. -- `(define-const )` defines `` to be the given term. -- `(define-sort (*) )` defines `` to be a lambda term whose arguments are given by variables of kind `Type` and whose body is given by the return type, or the return type if the argument is empty. -- `(define-type (*) )` defines `` to be a lambda term whose kind is given +- `(define-type (*) )` defines `` to be a lambda term whose type is given by the argument and return types. - `(declare-datatype )` defines a datatype ``, along with its associated constructors, selectors, discriminators and updaters. - `(declare-datatypes (^n) (^n))` defines a list of `n` datatypes for some `n>0`. - `(exit)` causes the checker to immediately terminate. @@ -113,11 +109,11 @@ The ALF language contains further commands for declaring symbols that are not st ### Example: Basic Declarations ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const c Int) (declare-const f (-> Int Int Int)) -(declare-fun g (Int Int) Int) -(declare-fun P (Int) Bool) +(declare-const g (-> Int (-> Int Int))) +(declare-const P (-> Int Bool)) ``` Since alfc does not assume any builtin definitions of SMT-LIB theories, definitions of standard symbols (such as `Int`) may be provided in ALF signatures. In the above example, `c` is declared to be a constant (0-ary) symbol of type `Int`. The symbol `f` is a function taking two integers and returning an integer. @@ -148,20 +144,19 @@ In other words, the following file is equivalent to the one above after parsing: ### Example: Polymorphic types ``` -(declare-sort Int 0) -(declare-sort Array 2) +(declare-type Int ()) +(declare-type Array (Type Type)) (declare-const a (Array Int Bool)) -(define-sort IntArray (T) (Array Int T)) +(define IntArray ((T Type)) (Array Int T)) (declare-const b (IntArray Bool)) ``` In the above example, we define the integer sort and the array sort, whose kind is `(-> Type Type Type)`. -Note the following declarations all generate terms of the same type: +Note the following declarations generate terms of the same type: ``` -(declare-sort Array_v1 2) (declare-type Array_v2 (Type Type)) (declare-const Array_v3 (-> Type Type Type)) ``` @@ -182,7 +177,7 @@ If this is not the specified type (in this case `Bool`), an error will be thrown The ALF language uses the SMT-LIB version 3.0 attributes `:var ` and `:implicit` in term annotations for naming arguments of functions and specifying they are implicit. ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const eq (-> (! Type :var T) T T Bool)) (define P ((x Int) (y Int)) (eq Int x y)) ``` @@ -190,7 +185,7 @@ The ALF language uses the SMT-LIB version 3.0 attributes `:var ` and `:i The above example declares a predicate `eq` whose first argument is a type, that is given a name `T`. It then expects two terms of type `T` and returns a `Bool`. In the definition of `P`, this predicate is applied to two variables, where the type `Int` must be explicitly provided. ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const = (-> (! Type :var T :implicit) T T Bool)) (define P ((x Int) (y Int)) (= x y)) ``` @@ -201,7 +196,7 @@ We call `T` in the above definitions a *parameter*. The free parameters of the r ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const f (-> (! Type :var T :implicit) Int T)) ``` @@ -214,7 +209,7 @@ We call `T` in the above definitions a *parameter*. The free parameters of the r Arguments to functions can also be annotated with the attribute `:requires ( )` to denote a equality condition that is required for applications of the term to type check. ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const BitVec (-> (! Int :var w :requires ((alf.is_neg w) false)) Type)) ``` The above declares the integer sort and the bitvector sort that expects a non-negative integer `w`. @@ -294,7 +289,7 @@ The nil terminator of a right associative operator may involve previously declar For example: ``` -(declare-sort RegLan 0) +(declare-type RegLan ()) (declare-const re.all RegLan) (declare-const re.inter (-> RegLan RegLan RegLan) :right-assoc-nil re.all) ``` @@ -327,8 +322,8 @@ This annotation marks that the term should be treated as a list of arguments whe (define Q ((x Bool) (y Bool :list)) (or x y)) (declare-const a Bool) (declare-const b Bool) -(define-const Paab Bool (P a (or a b))) -(define-const Qaab Bool (Q a (or a b))) +(define Paab () (P a (or a b))) +(define Qaab () (Q a (or a b))) ``` In the above example, note that `or` has been marked `:right-assoc-nil false`. @@ -371,7 +366,7 @@ In contrast, `(or x)` denotes the `or` whose children are `x` and `false`. ### Chainable ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const and (-> Bool Bool Bool) :right-assoc) (declare-const >= (-> Int Int Bool) :chainable) (define ((x Int) (y Int) (z Int)) (>= x y z)) @@ -387,7 +382,7 @@ where the type of its chaining operator is `(-> S S S)`, and that operator has b ### Pairwise ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const and (-> Bool Bool Bool) :right-assoc) (declare-const distinct (-> (! Type :var T :implicit) T T Bool) :pairwise and) (define P ((x Int) (y Int) (z Int)) (distinct x y z)) @@ -399,8 +394,8 @@ where the type of its pairwise operator is `(-> S S S)`, and that operator has b ### Binder ``` -(declare-sort Int 0) -(declare-sort @List 0) +(declare-type Int ()) +(declare-type @List ()) (declare-const @nil @List) (declare-const @cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @nil) (declare-const forall (-> @List Bool Bool) :binder @cons) @@ -461,7 +456,7 @@ String values are implemented as a vector of unsigned integers whose maximum val The following gives an example of how to define the class of numeral constants. ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (define P ((x Int)) (> x 7)) ``` @@ -675,7 +670,7 @@ The ALF checker supports extensions of `alf.and, alf.or, alf.xor, alf.add, alf.m Note the following examples of core operators for the given signature ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const x Int) (declare-const y Int) (declare-const a Bool) @@ -777,7 +772,7 @@ for the term `or` applied to arguments `a,b`. ### Example: Type rule for BitVector concatentation ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-type BitVec (Int)) @@ -813,7 +808,7 @@ For example, given a function `f` of type `(-> (BitVec (alf.add b a)) T)`, the t ### Example: Type rule for BitVector constants ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-type BitVec (Int)) @@ -837,7 +832,7 @@ Its syntax is: In the following example, we declare bitvector-or (`bvor` in SMT-LIB) where its nil terminator is bitvector zero for the given bitwidth. ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) ; numeral literals denote Int constants (declare-type BitVec (Int)) (declare-consts @@ -1030,7 +1025,7 @@ In detail, an application of this proof rule for premise proof `(= a b)` for con A list of requirements can be given to a proof rule. ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-fun >= (Int Int) Bool) (declare-rule leq-contra ((x Int)) @@ -1077,7 +1072,7 @@ where :premises ((= t s)) :conclusion (= s t) ) -(declare-sort Int 0) +(declare-type Int ()) (declare-const a Int) (declare-const b Int) (assume @p0 (= a b)) @@ -1249,7 +1244,7 @@ Thus, the side condition is written in three cases: either `t` is `x` in which c ### Example: Term evaluator ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const = (-> (! Type :var T :implicit) T T Bool)) (declare-const + (-> Int Int Int)) @@ -1275,8 +1270,8 @@ The above example recursively evaluates arithmetic terms and predicates accordin ### Example: A computational type rule ``` -(declare-sort Int 0) -(declare-sort Real 0) +(declare-type Int ()) +(declare-type Real ()) (program arith.typeunion () (Type Type) Type ( @@ -1298,7 +1293,7 @@ The return type of `+` invokes this side condition, which conceptually is implem ### Example: Conversion to DIMACS ``` -(declare-sort String 0) +(declare-type String ()) (declare-consts String) (declare-const not (-> Bool Bool)) (declare-const or (-> Bool Bool Bool) :right-assoc-nil false) @@ -1346,7 +1341,7 @@ Also, similar to programs, the free parameters of `ri` that occur in the paramet ### Examples of legal and illegal match terms ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const F Bool) (declare-const a Int) (declare-const P (-> Int Bool)) @@ -1387,7 +1382,7 @@ Also, similar to programs, the free parameters of `ri` that occur in the paramet ### Example: Proof rule for symmetry of (dis)equality ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const = (-> (! Type :var T :implicit) T T Bool)) (declare-const not (-> Bool Bool)) (declare-rule symm ((F Bool)) @@ -1406,7 +1401,7 @@ It matches the given premise `F` with either `(= t1 t2)` or `(not (= t1 t2))` an Internally, the semantics of `alf.match` can be seen as an (inlined) program applied to its head, such that the above example is equivalent to: ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const = (-> (! Type :var T :implicit) T T Bool)) (declare-const not (-> Bool Bool)) (program matchF ((t1 Int) (t2 Int)) @@ -1429,7 +1424,7 @@ In more general cases, if the body of the match term contains free variables, th ### Example: Proof rule for transitivity of equality with a premise list ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-const = (-> (! Type :var T :implicit) T T Bool)) (declare-const and (-> Bool Bool Bool) :left-assoc) @@ -1485,8 +1480,8 @@ For this reason, alfc additionally supports providing an optional normalization For example: ``` -(declare-sort Int 0) -(declare-sort Real 0) +(declare-type Int ()) +(declare-type Real ()) (declare-const / (-> Int Int Real)) (program normalize ((T Type) (S Type) (f (-> S T)) (x S) (a Int) (b Int)) (T) T @@ -1512,14 +1507,14 @@ In particular, the ALF checker supports the command: ``` (declare-oracle-fun (*) ) ``` -Like `declare-fun`, this command declares a constant named `` whose type is given by the argument types and return type. +Like the `declare-fun` command from SMT-LIB, this command declares a constant named `` whose type is given by the argument types and return type. In addition, a symbol is provided at the end of the command which specifies the name of executable command to run. Ground applications of oracle functions are eagerly evaluated by invoking the binary and parsing its result, which we describe in more detail in the following. ### Example: Oracle isPrime ``` -(declare-sort Int 0) +(declare-type Int ()) (declare-consts Int) (declare-const = (-> (! Type :var T :implicit) T T Bool)) (declare-const >= (-> Int Int Bool)) @@ -1593,10 +1588,6 @@ Valid inputs to the ALF checker are `*`, where: (declare-const *) (declare-datatype ) | (declare-datatypes (^n) (^n)) | - (declare-fun (*) *) | - (declare-sort ) | - (define-const ) | - (define-sort (*) ) | (echo ?) | (exit) | (reset) @@ -1606,7 +1597,11 @@ Valid inputs to the ALF checker are `*`, where: (assert ) | (check-sat) | (check-sat-assuming (*)) | + (declare-fun (*) *) | + (declare-sort ) | + (define-const ) | (define-fun (*) ) | + (define-sort (*) ) | (set-info ) | (set-logic ) | (set-option ) | From 811463116694e2b69a3541711b933607dbefc90e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 16:11:02 -0500 Subject: [PATCH 5/9] Fix --- tests/define-const-simple.smt3 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/define-const-simple.smt3 b/tests/define-const-simple.smt3 index 80265630..c527fd1c 100644 --- a/tests/define-const-simple.smt3 +++ b/tests/define-const-simple.smt3 @@ -1,7 +1,7 @@ (declare-const not (-> Bool Bool)) -(define f_true true) +(define f_true () true) (declare-rule trust ((f Bool)) From 02c662e61870b06b17674facac9719b5cfee87a6 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 16:13:24 -0500 Subject: [PATCH 6/9] Revert --- src/cmd_parser.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index 10dd533a..faf1b1e9 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -52,6 +52,7 @@ CmdParser::CmdParser(Lexer& lex, // only used in smt2 queries d_table["assert"] = Token::ASSERT; d_table["declare-fun"] = Token::DECLARE_FUN; + d_table["define-const"] = Token::DEFINE_CONST; d_table["define-fun"] = Token::DEFINE_FUN; d_table["declare-sort"] = Token::DECLARE_SORT; d_table["define-sort"] = Token::DEFINE_SORT; @@ -461,6 +462,18 @@ bool CmdParser::parseNextCommand() d_eparser.bind(name, decType); } break; + // (define-const ) + case Token::DEFINE_CONST: + { + //d_state.checkThatLogicIsSet(); + std::string name = d_eparser.parseSymbol(); + //d_state.checkUserSymbol(name); + Expr ret = d_eparser.parseType(); + Expr e = d_eparser.parseExpr(); + d_eparser.typeCheck(e, ret); + d_eparser.bind(name, e); + } + break; // (define-fun (*) ) // (define-type (*) ) // (define (*) *) From 2f6dfbcf9cb2a056c1ceeb810d65dfefabb39433 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 16:18:23 -0500 Subject: [PATCH 7/9] Minor --- src/cmd_parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index faf1b1e9..fbb42dd3 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -52,9 +52,9 @@ CmdParser::CmdParser(Lexer& lex, // only used in smt2 queries d_table["assert"] = Token::ASSERT; d_table["declare-fun"] = Token::DECLARE_FUN; + d_table["declare-sort"] = Token::DECLARE_SORT; d_table["define-const"] = Token::DEFINE_CONST; d_table["define-fun"] = Token::DEFINE_FUN; - d_table["declare-sort"] = Token::DECLARE_SORT; d_table["define-sort"] = Token::DEFINE_SORT; d_table["check-sat"] = Token::CHECK_SAT; d_table["check-sat-assuming"] = Token::CHECK_SAT_ASSUMING; From 85e879ce475f35f7ecff1c02d51c868a161d5d18 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 16:24:04 -0500 Subject: [PATCH 8/9] More fixes to manual --- user_manual.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/user_manual.md b/user_manual.md index 029e18a9..7582e1e3 100644 --- a/user_manual.md +++ b/user_manual.md @@ -814,7 +814,7 @@ For example, given a function `f` of type `(-> (BitVec (alf.add b a)) T)`, the t (declare-consts (BitVec (alf.len alf.self))) -(define-const x (BitVec 3) #b000) +(define x () #b000 :type (BitVec 3)) ``` To define the class of binary values, whose type depends on the number of bits they contain, the ALF checker provides support for a distinguished parameter `alf.self`. The type checker for values applies the substitution mapping `alf.self` to the term being type checked. @@ -1027,7 +1027,7 @@ A list of requirements can be given to a proof rule. ``` (declare-type Int ()) (declare-consts Int) -(declare-fun >= (Int Int) Bool) +(declare-const >= (-> Int Int Bool)) (declare-rule leq-contra ((x Int)) :premise ((>= x 0)) :requires (((alf.is_neg x) true)) @@ -1042,7 +1042,7 @@ It requires that the left hand side of this inequality `x` is a negative numeral A rule can take an arbitrary number of premises via the syntax `:premise-list `. For example: ``` -(declare-fun and (-> Bool Bool Bool) :right-assoc-nil true) +(declare-const and (-> Bool Bool Bool) :right-assoc-nil true) (declare-rule and-intro ((F Bool)) :premise-list F and :conclusion F) From 9cfec269b2faad8d607f29c0d4382eba3adef2d2 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 23 Jun 2024 16:26:12 -0500 Subject: [PATCH 9/9] Minor --- src/cmd_parser.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index fbb42dd3..d7faa839 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -173,7 +173,7 @@ bool CmdParser::parseNextCommand() cons = d_state.mkLiteral(Kind::STRING, oname); // don't permit attributes for oracle functions } - else if (tok==Token::DECLARE_CONST || tok==Token::DECLARE_FUN || tok==Token::DECLARE_PARAMETERIZED_CONST) + else if (tok==Token::DECLARE_CONST || tok==Token::DECLARE_PARAMETERIZED_CONST) { // possible attribute list AttrMap attrs; @@ -181,6 +181,7 @@ bool CmdParser::parseNextCommand() // determine if an attribute specified a constructor kind d_eparser.processAttributeMap(attrs, ck, cons, params); } + // declare-fun does not parse attribute list, as it is only in smt2 t = ret; if (!sorts.empty()) {