Merge pull request #50 from cvc5/rmDeclareFun

Demotes declare-fun, declare-sort, define-const, define-sort to smt2 commands only in reference.

src/cmd_parser.cpp

@@ -33,9 +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;
   d_table["pop"] = Token::POP;
@@ -54,6 +51,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["define-sort"] = Token::DEFINE_SORT;
     d_table["check-sat"] = Token::CHECK_SAT;
@@ -173,14 +173,15 @@ 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;
         d_eparser.parseAttributeList(t, attrs);
         // 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())
       {

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 <numeral> Int)
 (declare-consts <rational> Real)

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

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

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)
 

tests/arith-eval.smt3

@@ -1,5 +1,5 @@
-(declare-sort Int 0)
-(declare-sort Real 0)
+(declare-type Int ())
+(declare-type Real ())
 
 (declare-consts <numeral> Int)
 (declare-consts <rational> Real)

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

tests/arity-overload.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const - (-> Int Int))
 (declare-const - (-> Int Int Int))
 

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)
 
 

tests/binder-ex.smt3

@@ -1,8 +1,8 @@
-(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)
 
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-const P (-> Int Bool))
 (declare-const forall (-> @List Bool Bool) :binder @list.cons)

tests/binder-subterm-share.smt3

@@ -1,8 +1,8 @@
-(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)
 
-(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)

tests/bv-concat.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-type BitVec (Int)) 
@@ -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))
 

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

tests/bv-eval.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const = (-> (! Type :var T :implicit) T T Bool))

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

tests/bv-extract.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const BitVec (-> Int Type))
 

tests/bv-literals.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const = (-> (! Type :var T :implicit) T T Bool))

tests/bv-type-strict.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const = (-> (! Type :var T :implicit) T T Bool))

tests/constant-eval-args.smt3

@@ -1,5 +1,5 @@
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (program less-than ()

tests/constant-eval.smt3

@@ -1,6 +1,6 @@
 
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (program less-than ()

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

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

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 Array (Type Type))
+(declare-type Int ())
 (define IntArray ((T Type)) (Array Int T))
 (declare-const a (Array Int Bool))
 (declare-const b (IntArray Bool))

tests/distinct_value_testers.smt3

@@ -7,7 +7,7 @@
     :conclusion (not (= t s))
 )
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> 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 <rational> Real)
 
 (declare-rule disinct_value_real ((t Real) (s Real))
@@ -26,7 +26,7 @@
 )
 
 
-(declare-sort String 0)
+(declare-type String ())
 (declare-consts <string> 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 <binary> Bin)
 
 (declare-rule disinct_value_bin ((t Bin) (s Bin))

tests/eval-inc.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-consts <numeral> Int)
 

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

tests/evaluation.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-consts <numeral> Int)
 

tests/ff-nil.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const FiniteField (-> Int Type))
 
@@ -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))
 

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

tests/gt_eval.smt3

@@ -1,5 +1,5 @@
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const > (-> Int Int Bool))
 
@@ -9,7 +9,7 @@
     :conclusion (> t s)
 )
 
-(declare-sort Bin 0)
+(declare-type Bin ())
 (declare-consts <binary> Bin)
 (declare-const bvugt (-> Bin Bin Bool))
 

tests/ite-compile-test.smt3

@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const + (-> Int Int Int))
 (declare-const - (-> Int Int Int))
@@ -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)