Split RARE rewrites for expert extensions to own files (cvc5#11619)

This is work towards decoupling expert/safe poritions of the proof
signature.

Author: ajreynol

src/CMakeLists.txt

@@ -1441,6 +1441,10 @@ set(REWRITES_FILES
   ${PROJECT_SOURCE_DIR}/src/theory/strings/rewrites
   ${PROJECT_SOURCE_DIR}/src/theory/strings/rewrites-regexp-membership
   ${PROJECT_SOURCE_DIR}/src/theory/uf/rewrites
+  # these files should only be enabled in expert builds and should
+  # be partitioned into their own proof signature
+  ${PROJECT_SOURCE_DIR}/src/theory/arith/rewrites-transcendentals
+  ${PROJECT_SOURCE_DIR}/src/theory/sets/rewrites-card
 )
 
 #-----------------------------------------------------------------------------#

src/theory/arith/rewrites

@@ -77,18 +77,6 @@
   (>= (to_real t) c)
   (>= t cc))
 
-; trancendentals
-
-(define-rule arith-sine-zero () (sin 0/1) 0/1)
-(define-rule arith-sine-pi2 () (sin (* 1/2 real.pi)) 1/1)
-(define-rule arith-cosine-elim ((x Real)) (cos x) (sin (- (* 1/2 real.pi) x)))
-(define-rule arith-tangent-elim ((x Real)) (tan x) (/ (sin x) (cos x)))
-(define-rule arith-secent-elim ((x Real)) (sec x) (/ 1/1 (sin x)))
-(define-rule arith-cosecent-elim ((x Real)) (csc x) (/ 1/1 (cos x)))
-(define-rule arith-cotangent-elim ((x Real)) (cot x) (/ (cos x) (sin x)))
-
-(define-rule arith-pi-not-int () (is_int real.pi) false)
-
 ; absolute value comparisons
 
 (define-rule arith-abs-eq ((x ?) (y ?))

src/theory/arith/rewrites-transcendentals

@@ -0,0 +1,12 @@
+; trancendentals
+
+(define-rule arith-sine-zero () (sin 0/1) 0/1)
+(define-rule arith-sine-pi2 () (sin (* 1/2 real.pi)) 1/1)
+(define-rule arith-cosine-elim ((x Real)) (cos x) (sin (- (* 1/2 real.pi) x)))
+(define-rule arith-tangent-elim ((x Real)) (tan x) (/ (sin x) (cos x)))
+(define-rule arith-secent-elim ((x Real)) (sec x) (/ 1/1 (sin x)))
+(define-rule arith-cosecent-elim ((x Real)) (csc x) (/ 1/1 (cos x)))
+(define-rule arith-cotangent-elim ((x Real)) (cot x) (/ (cos x) (sin x)))
+
+(define-rule arith-pi-not-int () (is_int real.pi) false)
+

src/theory/sets/rewrites

@@ -1,4 +1,4 @@
-; Equality
+; Theory of sets
 
 (define-cond-rule sets-eq-singleton-emp ((x ?Set) (y ?))
   (= x (@set.empty_of_type (@type_of x)))
@@ -64,29 +64,10 @@
   (set.choose (set.singleton x))
   x)
 
-(define-rule sets-card-singleton ((x ?))
-  (set.card (set.singleton x))
-  1)
-
-(define-rule sets-card-union ((s ?Set) (t ?Set))
-  (set.card (set.union s t))
-  (- (+ (set.card s) (set.card t)) (set.card (set.inter s t))))
-
-(define-rule sets-card-minus ((s ?Set) (t ?Set))
-  (set.card (set.minus s t))
-  (- (set.card s) (set.card (set.inter s t))))
-
-(define-cond-rule sets-card-emp ((x ?Set))
-  (= x (@set.empty_of_type (@type_of x)))
-  (set.card x)
-  0)
-
 (define-rule sets-minus-self ((x ?Set))
   (set.minus x x)
   (@set.empty_of_type (@type_of x)))
 
-; (set.complement S) ---> (set.minus (as set.universe (Set Int)) S)
-
 (define-rule sets-is-empty-elim ((x ?Set))
   (set.is_empty x)
   (= x (@set.empty_of_type (@type_of x))))

src/theory/sets/rewrites-card

@@ -0,0 +1,20 @@
+; Theory of sets with cardinality
+
+(define-rule sets-card-singleton ((x ?))
+  (set.card (set.singleton x))
+  1)
+
+(define-rule sets-card-union ((s ?Set) (t ?Set))
+  (set.card (set.union s t))
+  (- (+ (set.card s) (set.card t)) (set.card (set.inter s t))))
+
+(define-rule sets-card-minus ((s ?Set) (t ?Set))
+  (set.card (set.minus s t))
+  (- (set.card s) (set.card (set.inter s t))))
+
+(define-cond-rule sets-card-emp ((x ?Set))
+  (= x (@set.empty_of_type (@type_of x)))
+  (set.card x)
+  0)
+
+; (set.complement S) ---> (set.minus (as set.universe (Set Int)) S)