Merge branch 'main' of https://github.com/cvc5/cvc5 into pfTrustId

proofs/eo/cpc/rules/Datatypes.eo

@@ -302,7 +302,7 @@
 ; args:
 ; - c U: The remaining term to process.
 ; - a T: The value to replace as an argument of t.
-; - n Int: The argument position (from the end) which a should be placed.
+; - n Int: The argument position (from the end) which a should replace.
 ; return: >
 ;   The result of updating the n^th argument from the end in t.
 (program $dt_collapse_updater_rhs ((U Type) (T Type) (f (-> T U)) (x T) (a T) (n Int))
@@ -317,7 +317,7 @@
 ; args:
 ; - c U: The remaining tuple term to process.
 ; - a T: The value to replace as an argument of t.
-; - n Int: The argument position which a should be placed.
+; - n Int: The argument position which a should replace.
 ; return: >
 ;   The result of updating the n^th argument in t.
 (program $tuple_collapse_updater_rhs ((U Type) (T Type) (W Type) (f (-> T U)) (x T) (a T) (b T) (n Int) (ts W :list))

proofs/eo/cpc/rules/Rewrites.eo

@@ -320,13 +320,13 @@
   :args (x1 y1 zs1)
   :conclusion (= (not (and x1 y1 zs1)) (or (not x1) (not ($singleton_elim (and y1 zs1)))))
 )
-(declare-rule bool-or-and-distrib ((y1 Bool) (y2 Bool) (y3 Bool :list) (zs1 Bool :list))
-  :args (y1 y2 y3 zs1)
-  :conclusion (= ($singleton_elim (or (and y1 y2 y3) zs1)) (and ($singleton_elim (or y1 zs1)) ($singleton_elim (or ($singleton_elim (and y2 y3)) zs1))))
+(declare-rule bool-or-and-distrib ((y1 Bool) (y2 Bool) (ys1 Bool :list) (zs1 Bool :list))
+  :args (y1 y2 ys1 zs1)
+  :conclusion (= ($singleton_elim (or (and y1 y2 ys1) zs1)) (and ($singleton_elim (or y1 zs1)) ($singleton_elim (or ($singleton_elim (and y2 ys1)) zs1))))
 )
-(declare-rule bool-implies-or-distrib ((y1 Bool) (y2 Bool) (y3 Bool :list) (zs1 Bool))
-  :args (y1 y2 y3 zs1)
-  :conclusion (= (=> (or y1 y2 y3) zs1) (and (=> y1 zs1) (=> ($singleton_elim (or y2 y3)) zs1)))
+(declare-rule bool-implies-or-distrib ((y1 Bool) (y2 Bool) (ys1 Bool :list) (z1 Bool))
+  :args (y1 y2 ys1 z1)
+  :conclusion (= (=> (or y1 y2 ys1) z1) (and (=> y1 z1) (=> ($singleton_elim (or y2 ys1)) z1)))
 )
 (declare-rule bool-xor-refl ((x1 Bool))
   :args (x1)

src/theory/booleans/rewrites

@@ -42,16 +42,16 @@
 
 ; We only permit distributing from the first child, or otherwise this rule
 ; could apply to fix point on all AND children of an OR at once.
-(define-rule* bool-or-and-distrib ((y1 Bool) (y2 Bool) (y3 Bool :list) (zs Bool :list))
-  (or (and y1 y2 y3) zs)
-  (or (and y2 y3) zs)
+(define-rule* bool-or-and-distrib ((y1 Bool) (y2 Bool) (ys Bool :list) (zs Bool :list))
+  (or (and y1 y2 ys) zs)
+  (or (and y2 ys) zs)
   (and (or y1 zs) _))
 
 ; Used for diamonds preprocessing
-(define-rule* bool-implies-or-distrib ((y1 Bool) (y2 Bool) (y3 Bool :list) (zs Bool))
-  (=> (or y1 y2 y3) zs)
-  (=> (or y2 y3) zs)
-  (and (=> y1 zs) _))
+(define-rule* bool-implies-or-distrib ((y1 Bool) (y2 Bool) (ys Bool :list) (z Bool))
+  (=> (or y1 y2 ys) z)
+  (=> (or y2 ys) z)
+  (and (=> y1 z) _))
 
 (define-rule bool-xor-refl ((x Bool)) (xor x x) false)
 (define-rule bool-xor-nrefl1 ((x Bool)) (xor x (not x)) true)

src/theory/quantifiers/conjecture_generator.cpp

@@ -380,53 +380,14 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
       d_hasAddedLemma = false;
       d_tge.d_cg = this;
       beginCallDebug();
-      eq::EqualityEngine* ee = getEqualityEngine();
       d_conj_count = 0;
       std::vector<TNode> eqcs;
       getEquivalenceClasses(eqcs);
       computeIrrelevantEqcs(eqcs);
-
       //debug printing
-      if( TraceIsOn("sg-gen-eqc") ){
-        for( unsigned i=0; i<eqcs.size(); i++ ){
-          TNode r = eqcs[i];
-          //print out members
-          bool firstTime = true;
-          bool isFalse = areEqual(r, d_false);
-          eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-          while( !eqc_i.isFinished() ){
-            TNode n = (*eqc_i);
-            if (getTermDatabase()->hasTermCurrent(n)
-                && getTermDatabase()->isTermActive(n)
-                && (n.getKind() != Kind::EQUAL || isFalse))
-            {
-              if( firstTime ){
-                Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
-                firstTime = false;
-              }
-              if( n.hasOperator() ){
-                Trace("sg-gen-eqc") << "   (" << n.getOperator();
-                for (const Node& nc : n)
-                {
-                  TNode ar = d_qstate.getRepresentative(nc);
-                  Trace("sg-gen-eqc") << " e" << d_em[ar];
-                }
-                Trace("sg-gen-eqc") << ") :: " << n << std::endl;
-              }else{
-                Trace("sg-gen-eqc") << "   " << n << std::endl;
-              }
-            }
-            ++eqc_i;
-          }
-          if( !firstTime ){
-            Trace("sg-gen-eqc") << "}" << std::endl;
-            //print out ground term
-            std::map< TNode, Node >::iterator it = d_ground_eqc_map.find( r );
-            if( it!=d_ground_eqc_map.end() ){
-              Trace("sg-gen-eqc") << "- Ground term : " << it->second << std::endl;
-            }
-          }
-        }
+      if( TraceIsOn("sg-gen-eqc") )
+      {
+        debugPrintIrrelevantEqcs(eqcs);
       }
 
       Trace("sg-proc") << "Compute relevant eqc..." << std::endl;
@@ -914,6 +875,59 @@ void ConjectureGenerator::computeIrrelevantEqcs(const std::vector<TNode>& eqcs)
   Trace("sg-proc") << "...done determine ground EQC" << std::endl;
 }
 
+void ConjectureGenerator::debugPrintIrrelevantEqcs(
+    const std::vector<TNode>& eqcs)
+{
+  eq::EqualityEngine* ee = getEqualityEngine();
+  for (unsigned i = 0; i < eqcs.size(); i++)
+  {
+    TNode r = eqcs[i];
+    // print out members
+    bool firstTime = true;
+    bool isFalse = areEqual(r, d_false);
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
+    while (!eqc_i.isFinished())
+    {
+      TNode n = (*eqc_i);
+      if (getTermDatabase()->hasTermCurrent(n)
+          && getTermDatabase()->isTermActive(n)
+          && (n.getKind() != Kind::EQUAL || isFalse))
+      {
+        if (firstTime)
+        {
+          Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
+          firstTime = false;
+        }
+        if (n.hasOperator())
+        {
+          Trace("sg-gen-eqc") << "   (" << n.getOperator();
+          for (const Node& nc : n)
+          {
+            TNode ar = d_qstate.getRepresentative(nc);
+            Trace("sg-gen-eqc") << " e" << d_em[ar];
+          }
+          Trace("sg-gen-eqc") << ") :: " << n << std::endl;
+        }
+        else
+        {
+          Trace("sg-gen-eqc") << "   " << n << std::endl;
+        }
+      }
+      ++eqc_i;
+    }
+    if (!firstTime)
+    {
+      Trace("sg-gen-eqc") << "}" << std::endl;
+      // print out ground term
+      std::map<TNode, Node>::iterator it = d_ground_eqc_map.find(r);
+      if (it != d_ground_eqc_map.end())
+      {
+        Trace("sg-gen-eqc") << "- Ground term : " << it->second << std::endl;
+      }
+    }
+  }
+}
+
 std::string ConjectureGenerator::identify() const { return "induction-cg"; }
 
 unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) {

src/theory/quantifiers/conjecture_generator.h

@@ -542,6 +542,20 @@ class ConjectureGenerator : public QuantifiersModule
    * when synthesizing conjectures.
    */
   void computeIrrelevantEqcs(const std::vector<TNode>& eqcs);
+  /** print information related to the computation of irrelevant equivalence
+   * classes
+   *
+   * This function requires that the contents of the input vector 'eqcs' are
+   * exactly the representatives of each equivalence class in the current model.
+   *
+   * For each element e of eqcs other than nodeManager()->mkConst(false), this
+   * function prints all terms t ~ e such that t is active (according to the
+   * term database) and t is not an equality.  If e is computed irrelevant (see
+   * computeIrrelevantEqcs) this function also prints a term that explains why e
+   * is irrelevant.
+   */
+  void debugPrintIrrelevantEqcs(const std::vector<TNode>& eqcs);
+
 public:  //for generalization
   //generalizations
   bool isGeneralization( TNode patg, TNode pat ) {

src/theory/quantifiers/ematching/trigger.cpp

@@ -160,7 +160,7 @@ uint64_t Trigger::addInstantiations()
     eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
     for (const Node& gt : d_groundTerms)
     {
-      if (!ee->hasTerm(gt))
+      if (!ee->hasTerm(gt) && !gt.getType().isBoolean())
       {
         Node k = SkolemManager::mkPurifySkolem(gt);
         Node eq = k.eqNode(gt);

test/regress/cli/CMakeLists.txt

@@ -1587,6 +1587,7 @@ set(regress_0_tests
   regress0/quantifiers/proj-issue152-2-non-std-nterm-ext-rew.smt2
   regress0/quantifiers/proj-issue512-has-skolem.smt2
   regress0/quantifiers/proj-issue608-mbqi-cegqi.smt2
+  regress0/quantifiers/proj-issue763-no-gt-purify-bool.smt2
   regress0/quantifiers/pure_dt_cbqi.smt2
   regress0/quantifiers/qarray-sel-over-store.smt2
   regress0/quantifiers/qbv-inequality2.smt2

test/regress/cli/regress0/quantifiers/proj-issue763-no-gt-purify-bool.smt2

@@ -0,0 +1,7 @@
+; COMMAND-LINE: --mbqi
+; EXPECT: sat
+(set-logic ALL)
+(declare-const x5 (Seq Bool))
+(declare-const x (Array Bool Bool))
+(assert (not (select x (exists ((_x (Seq Bool))) (forall ((x (Array Bool Bool))) (select x (seq.prefixof x5 _x)))))))
+(check-sat)