Add Eunoia definitions of 3 datatype ad-hoc rewrites (cvc5#11443)

Does some minor reorg of signature files.

Also moves ARITH_POLY_NORM to fully supported, which was missed on a
previous PR.

proofs/eo/cpc/programs/Datatypes.eo

@@ -0,0 +1,75 @@
+(include "../theories/Datatypes.eo")
+
+; program: $dt_get_constructors
+; args:
+; - T Type: The datatype to get the constructors for.
+; return: The list of constructors of T, as a eo::List.
+; note: >
+;   (Unit) tuples are treated as a special case of datatypes with a single
+;   constructor. Parametric datatypes must reference the type constructor to
+;   extract their constructors.
+(program $dt_get_constructors ((D Type) (T Type) (c T) (T1 Type) (T2 Type :list) (DC (-> Type Type)))
+  (Type) eo::List
+  (
+    (($dt_get_constructors (Tuple T1 T2)) (eo::cons eo::List::cons tuple eo::List::nil))
+    (($dt_get_constructors UnitTuple)     (eo::cons eo::List::cons tuple.unit eo::List::nil))
+    (($dt_get_constructors (DC T))        ($dt_get_constructors DC))   ; user-defined parameteric datatypes, traverse
+    (($dt_get_constructors D)             (eo::dt_constructors D))     ; ordinary user-defined datatypes
+  )
+)
+
+; program: $tuple_get_selectors_rec
+; args:
+; - T Type: The tuple type to get the selectors for.
+; - n Int: The number of component types we have processed so far.
+; return: The list of selectors of T, as a eo::List.
+; note: >
+;   Tuples use a special selector tuple.select indexed by an integer, which is
+;   why they require a special method here.
+(program $tuple_get_selectors_rec ((D Type) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int))
+  (Type Int) Bool
+  (
+    (($tuple_get_selectors_rec UnitTuple n)     eo::List::nil)
+    (($tuple_get_selectors_rec (Tuple T1 T2) n) (eo::cons eo::List::cons (tuple.select n) ($tuple_get_selectors_rec T2 (eo::add n 1))))
+  )
+)
+
+; program: $dt_get_selectors
+; args:
+; - D Type: The type to get the selectors for.
+; - c T: The constructor of D.
+; return: The list of selectors of c, as a eo::List.
+; note: >
+;   (Unit) tuples are treated as a special case of datatypes whose selectors are
+;   tuple.select indexed by an integer, which requires the above method.
+(program $dt_get_selectors ((D Type) (T Type) (c Type) (T1 Type) (T2 Type :list))
+  (Type T) eo::List
+  (
+    (($dt_get_selectors (Tuple T1 T2) tuple)  ($tuple_get_selectors_rec (Tuple T1 T2) 0))
+    (($dt_get_selectors UnitTuple tuple.unit) eo::List::nil)
+    (($dt_get_selectors D c)                  (eo::dt_selectors c)) ; user-defined datatypes
+  )
+)
+
+; define: $dt_is_cons
+; args:
+; - t T: The term in question.
+; return: true iff t is a constructor symbol.
+(define $dt_is_cons ((T Type :implicit) (t T))
+  (eo::is_z (eo::list_len eo::List::cons (eo::dt_selectors t))))
+
+; define: $dt_arg_nth
+; args:
+; - t T: The term to inspect, expected to be a constructor application.
+; - n Int: The index of the argument to get.
+; return: >
+;   The nth argument of t.
+(program $dt_arg_nth ((T Type) (U Type) (V Type) (W Type) (t T) (n Int) (t1 V) (t2 W :list))
+  (T Int) U
+  (
+    ; for tuples, use nth on tuple as an n-ary constructor
+    (($dt_arg_nth (tuple t1 t2) n)  (eo::list_nth tuple (tuple t1 t2) n))
+    ; otherwise we get the argument list
+    (($dt_arg_nth t n)              (eo::list_nth @list ($get_arg_list t) n))
+  )
+)

proofs/eo/cpc/programs/Utils.eo

@@ -21,6 +21,19 @@
 (declare-const @list.nil @List)
 (declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
 
+; program: $get_fun
+; args:
+; - t S: The term to inspect.
+; return: >
+;   The function at the head of the application of t, or t itself if it is not
+;   an application.
+(program $get_fun ((T Type) (S Type) (U Type) (f (-> T S)) (x T) (y S))
+  (S) U
+  (
+    (($get_fun (f x))  ($get_fun f))
+    (($get_fun y)      y)
+  )
+)
 
 ; program: $get_arg_list_rec
 ; args:
@@ -45,8 +58,6 @@
 ;   list if t is not a function application.
 (define $get_arg_list ((T Type :implicit) (t T)) ($get_arg_list_rec t @list.nil))
 
-
-
 ; program: $is_app
 ; args:
 ; - f (-> T U): The function.

proofs/eo/cpc/rules/Datatypes.eo

@@ -1,56 +1,5 @@
 (include "../theories/Datatypes.eo")
-
-
-; program: $dt_get_constructors
-; args:
-; - T Type: The datatype to get the constructors for.
-; return: The list of constructors of T, as a eo::List.
-; note: >
-;   (Unit) tuples are treated as a special case of datatypes with a single
-;   constructor. Parametric datatypes must reference the type constructor to
-;   extract their constructors.
-(program $dt_get_constructors ((D Type) (T Type) (c T) (T1 Type) (T2 Type :list) (DC (-> Type Type)))
-  (Type) eo::List
-  (
-    (($dt_get_constructors (Tuple T1 T2)) (eo::cons eo::List::cons tuple eo::List::nil))
-    (($dt_get_constructors UnitTuple)     (eo::cons eo::List::cons tuple.unit eo::List::nil))
-    (($dt_get_constructors (DC T))        ($dt_get_constructors DC))   ; user-defined parameteric datatypes, traverse
-    (($dt_get_constructors D)             (eo::dt_constructors D))     ; ordinary user-defined datatypes
-  )
-)
-
-; program: $tuple_get_selectors_rec
-; args:
-; - T Type: The tuple type to get the selectors for.
-; - n Int: The number of component types we have processed so far.
-; return: The list of selectors of T, as a eo::List.
-; note: >
-;   Tuples use a special selector tuple.select indexed by an integer, which is
-;   why they require a special method here.
-(program $tuple_get_selectors_rec ((D Type) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int))
-  (Type Int) Bool
-  (
-    (($tuple_get_selectors_rec UnitTuple n)     eo::List::nil)
-    (($tuple_get_selectors_rec (Tuple T1 T2) n) (eo::cons eo::List::cons (tuple.select n) ($tuple_get_selectors_rec T2 (eo::add n 1))))
-  )
-)
-
-; program: $dt_get_selectors
-; args:
-; - D Type: The type to get the selectors for.
-; - c T: The constructor of D.
-; return: The list of selectors of c, as a eo::List.
-; note: >
-;   (Unit) tuples are treated as a special case of datatypes whose selectors are
-;   tuple.select indexed by an integer, which requires the above method.
-(program $dt_get_selectors ((D Type) (T Type) (c Type) (T1 Type) (T2 Type :list))
-  (Type T) eo::List
-  (
-    (($dt_get_selectors (Tuple T1 T2) tuple)  ($tuple_get_selectors_rec (Tuple T1 T2) 0))
-    (($dt_get_selectors UnitTuple tuple.unit) eo::List::nil)
-    (($dt_get_selectors D c)                  (eo::dt_selectors c)) ; user-defined datatypes
-  )
-)
+(include "../programs/Datatypes.eo")
 
 ;;;;; ProofRule::DT_SPLIT
 
@@ -144,3 +93,60 @@
   :requires ((($mk_dt_inst (eo::typeof x) c x) t))
   :conclusion (= (is c x) (= x t))
 )
+
+;;;;; ProofRewriteRule::DT_COLLAPSE_SELECTOR
+
+; rule: dt-collapse-selector
+; implements: ProofRewriteRule::DT_COLLAPSE_SELECTOR.
+; args:
+; - eq Bool: The equality to prove.
+; requires: >
+;   We require that the index^th argument of the term t we are selecting from
+;   is the right hand side of the equality, where index is the index of the
+;   selector in the constructor of t.
+; conclusion: The given equality.
+(declare-rule dt-collapse-selector ((D Type) (T Type) (s (-> D T)) (t D) (ti T))
+  :args ((= (s t) ti))
+  :requires (((eo::define ((c ($get_fun t)))
+              (eo::define ((ss ($dt_get_selectors (eo::typeof t) c)))
+              ; note that s must be a selector of the constructor of t, or else index will not evaluate
+              (eo::define ((index (eo::list_find eo::List::cons ss s)))
+                ($dt_arg_nth t index)))) ti))
+  :conclusion (= (s t) ti)
+)
+
+;;;;; ProofRewriteRule::DT_COLLAPSE_TESTER
+
+; rule: dt-collapse-tester
+; implements: ProofRewriteRule::DT_COLLAPSE_TESTER.
+; args:
+; - eq Bool: The equality to prove.
+; requires: >
+;   If the right hand side is true, then the function head of the term we are
+;   testing must be the constructor. If the right hand side is false, then the
+;   function head of the term we are testing must be the constructor that is
+;   not the constructor we are testing.
+; conclusion: The given equality.
+(declare-rule dt-collapse-tester ((D Type) (T Type) (c T) (t D) (b Bool))
+  :args ((= (is c t) b))
+  :requires (((eo::define ((f ($get_fun t)))
+              (eo::ite b
+                (eo::is_eq f c)
+                (eo::and ($dt_is_cons f) (eo::not (eo::is_eq f c))))) true))
+  :conclusion (= (is c t) b)
+)
+
+;;;;; ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON
+
+; rule: dt-collapse-tester-singleton
+; implements: ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON.
+; args:
+; - eq Bool: The equality to prove.
+; requires: >
+;   The number of constructors of the type of the term we are testing is one.
+; conclusion: The given equality.
+(declare-rule dt-collapse-tester-singleton ((D Type) (T Type) (c T) (t D))
+  :args ((= (is c t) true))
+  :requires (((eo::list_len eo::List::cons ($dt_get_constructors (eo::typeof t))) 1))
+  :conclusion (= (is c t) true)
+)

src/proof/alf/alf_printer.cpp

@@ -181,6 +181,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn)
     case ProofRule::ENCODE_EQ_INTRO:
     case ProofRule::HO_APP_ENCODE:
     case ProofRule::ACI_NORM:
+    case ProofRule::ARITH_POLY_NORM:
     case ProofRule::ARITH_POLY_NORM_REL:
     case ProofRule::DSL_REWRITE: return true;
     case ProofRule::BV_BITBLAST_STEP:
@@ -195,13 +196,6 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn)
       return isHandledTheoryRewrite(id, pfn->getArguments()[1]);
     }
     break;
-    case ProofRule::ARITH_POLY_NORM:
-    {
-      // we don't support bitvectors yet
-      Assert(pargs[0].getKind() == Kind::EQUAL);
-      return pargs[0][0].getType().isRealOrInt();
-    }
-    break;
     case ProofRule::ARITH_REDUCTION:
     {
       Kind k = pargs[0].getKind();
@@ -276,6 +270,9 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n)
     case ProofRewriteRule::QUANT_UNUSED_VARS:
     case ProofRewriteRule::ARRAYS_SELECT_CONST:
     case ProofRewriteRule::DT_INST:
+    case ProofRewriteRule::DT_COLLAPSE_SELECTOR:
+    case ProofRewriteRule::DT_COLLAPSE_TESTER:
+    case ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON:
     case ProofRewriteRule::QUANT_MERGE_PRENEX:
     case ProofRewriteRule::QUANT_MINISCOPE_AND:
     case ProofRewriteRule::QUANT_MINISCOPE_OR:

test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2

@@ -1,4 +1,5 @@
 ; EXPECT: unsat
+; DISABLE-TESTER: cpc
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort A$ 0)