Merge remote-tracking branch 'upstream/main'

Author: kondylidou

include/cvc5/cvc5_proof_rule.h

@@ -1685,6 +1685,16 @@ enum ENUM(ProofRule)
    * \endverbatim
    */
   EVALUE(RE_INTER),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Strings -- Regular expressions -- Concatenation**
+   *
+   * .. math::
+   *
+   *   \inferrule{t_1\in R_1,\,\ldots,\,t_n\in R_n\mid -}{\text{str.++}(t_1, \ldots, t_n)\in \text{re.++}(R_1, \ldots, R_n)}
+   * \endverbatim
+   */
+  EVALUE(RE_CONCAT),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Strings -- Regular expressions -- Positive Unfold**

proofs/eo/cpc/rules/Strings.eo

@@ -311,6 +311,8 @@
 
 ;;-------------------- Regular expressions
 
+;;;;; ProofRule::RE_INTER
+
 ; rule: re_inter
 ; implements: ProofRule::RE_INTER
 ; premises:
@@ -324,6 +326,38 @@
   :conclusion (str.in_re x (re.inter s t))
 )
 
+;;;;; ProofRule::RE_CONCAT
+
+; program: $mk_re_concat
+; args:
+; - E: A conjunction of regular expression memberships.
+; return: >
+;   The concatenation of the strings in E is in the concatenation of the regular
+;   expressions in E.
+(program $mk_re_concat ((Es Bool :list) (s String) (r RegLan))
+  (Bool) Bool
+  (
+  (($mk_re_concat (and (str.in_re s r) Es)) (eo::match ((s1 String) (r1 RegLan))
+                                              ($mk_re_concat Es)
+                                              (((str.in_re s1 r1) (str.in_re (eo::cons str.++ s s1) (eo::cons re.++ r r1))))))
+  (($mk_re_concat true)                     (str.in_re "" @re.empty))
+  )
+)
+
+; rule: re_concat
+; implements: ProofRule::RE_CONCAT
+; premises:
+; - E [:list]: A conjunction of regular expression memberships.
+; conclusion: >
+;   The concatenation of the strings in E is in the concatenation of the regular
+;   expressions in E.
+(declare-rule re_concat ((E Bool))
+  :premise-list E and
+  :conclusion ($mk_re_concat E)
+)
+
+;;;;; ProofRule::RE_UNFOLD_POS
+
 ; rule: re_unfold_pos
 ; implements: ProofRule::RE_UNFOLD_POS
 ; premises:
@@ -357,6 +391,8 @@
     ))
 )
 
+;;;;; ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED
+
 ; rule: re_unfold_neg_concat_fixed
 ; implements: ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED
 ; premises:
@@ -384,6 +420,8 @@
     ))
 )
 
+;;;;; ProofRule::RE_UNFOLD_NEG
+
 ; rule: re_unfold_neg
 ; implements: ProofRule::RE_UNFOLD_NEG
 ; premises:

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/api/cpp/cvc5_proof_rule_template.cpp

@@ -148,6 +148,7 @@ const char* toString(ProofRule rule)
     case ProofRule::STRING_REDUCTION: return "STRING_REDUCTION";
     case ProofRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION";
     case ProofRule::RE_INTER: return "RE_INTER";
+    case ProofRule::RE_CONCAT: return "RE_CONCAT";
     case ProofRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS";
     case ProofRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG";
     case ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED:

src/proof/alf/alf_printer.cpp

@@ -167,6 +167,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn)
     case ProofRule::STRING_LENGTH_POS:
     case ProofRule::STRING_LENGTH_NON_EMPTY:
     case ProofRule::RE_INTER:
+    case ProofRule::RE_CONCAT:
     case ProofRule::RE_UNFOLD_POS:
     case ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED:
     case ProofRule::RE_UNFOLD_NEG:

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)

src/theory/strings/proof_checker.cpp

@@ -55,6 +55,7 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(ProofRule::STRING_REDUCTION, this);
   pc->registerChecker(ProofRule::STRING_EAGER_REDUCTION, this);
   pc->registerChecker(ProofRule::RE_INTER, this);
+  pc->registerChecker(ProofRule::RE_CONCAT, this);
   pc->registerChecker(ProofRule::RE_UNFOLD_POS, this);
   pc->registerChecker(ProofRule::RE_UNFOLD_NEG, this);
   pc->registerChecker(ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED, this);
@@ -395,30 +396,45 @@ Node StringProofRuleChecker::checkInternal(ProofRule id,
     // memberships in the explanation
     for (const Node& c : children)
     {
-      bool polarity = c.getKind() != Kind::NOT;
-      Node catom = polarity ? c : c[0];
-      if (catom.getKind() != Kind::STRING_IN_REGEXP)
+      if (c.getKind() != Kind::STRING_IN_REGEXP)
       {
         return Node::null();
       }
       if (x.isNull())
       {
-        x = catom[0];
+        x = c[0];
       }
-      else if (x != catom[0])
+      else if (x != c[0])
       {
         // different LHS
         return Node::null();
       }
-      Node xcurr = catom[0];
-      Node rcurr =
-          polarity ? catom[1] : nm->mkNode(Kind::REGEXP_COMPLEMENT, catom[1]);
-      reis.push_back(rcurr);
+      reis.push_back(c[1]);
     }
     Node rei =
         reis.size() == 1 ? reis[0] : nm->mkNode(Kind::REGEXP_INTER, reis);
     return nm->mkNode(Kind::STRING_IN_REGEXP, x, rei);
   }
+  else if (id == ProofRule::RE_CONCAT)
+  {
+    Assert(children.size() >= 2);
+    Assert(args.empty());
+    std::vector<Node> ts;
+    std::vector<Node> rs;
+    // make the regular expression concatenation
+    for (const Node& c : children)
+    {
+      if (c.getKind() != Kind::STRING_IN_REGEXP)
+      {
+        return Node::null();
+      }
+      ts.push_back(c[0]);
+      rs.push_back(c[1]);
+    }
+    Node tc = nm->mkNode(Kind::STRING_CONCAT, ts);
+    Node rc = nm->mkNode(Kind::REGEXP_CONCAT, rs);
+    return nm->mkNode(Kind::STRING_IN_REGEXP, tc, rc);
+  }
   else if (id == ProofRule::RE_UNFOLD_POS || id == ProofRule::RE_UNFOLD_NEG
            || id == ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED)
   {