Fix issues with mixed types in relevant domain (#8901)

Fixes #8881.

Indentation changed, leading to the large diff. The code change is only to ensure the type of the term to add to the relevant domain matches the type of the variable.

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index dca27c38a118ccc38ce20b6cd693f4ee5d114b27..6801dd2ddf9cb3380d21fda2cdffa96e15cb4cac 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -294,14 +294,15 @@ class Instantiate : public QuantifiersUtil
   }; /* class Instantiate::Statistics */
   Statistics d_statistics;
 
- private:
-  /** record instantiation, return true if it was not a duplicate */
-  bool recordInstantiationInternal(Node q, const std::vector<Node>& terms);
   /**
    * Ensure that n has type tn, return a term equivalent to it for that type
    * if possible.
    */
   static Node ensureType(Node n, TypeNode tn);
+
+ private:
+  /** record instantiation, return true if it was not a duplicate */
+  bool recordInstantiationInternal(Node q, const std::vector<Node>& terms);
   /** Get or make the instantiation list for quantified formula q */
   InstLemmaList* getOrMkInstLemmaList(TNode q);
 

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 0f103ec43dc5992b45bb3ae899685b2bab8371bd..e1849d9362dc908f840b7bb115c39e14baa248b8 100644 (file)
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "util/rational.h"
@@ -309,128 +310,168 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
 }
 
 void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) {
-  if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){
-    NodeManager* nm = NodeManager::currentNM();
-    RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n];
-    rdl.d_merge = false;
-    int varCount = 0;
-    int varCh = -1;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( n[i].getKind()==INST_CONSTANT ){
-        // must get the quantified formula this belongs to, which may be
-        // different from q
-        Node qi = TermUtil::getInstConstAttr(n[i]);
-        unsigned id = n[i].getAttribute(InstVarNumAttribute());
-        rdl.d_rd[i] = getRDomain(qi, id, false);
-        varCount++;
-        varCh = i;
-      }else{
-        rdl.d_rd[i] = nullptr;
-      }
+  if (d_rel_dom_lit[hasPol][pol].find(n) != d_rel_dom_lit[hasPol][pol].end())
+  {
+    return;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  RDomainLit& rdl = d_rel_dom_lit[hasPol][pol][n];
+  rdl.d_merge = false;
+  size_t varCount = 0;
+  size_t varCh = 0;
+  Assert(n.getNumChildren() == 2);
+  for (size_t i = 0; i < 2; i++)
+  {
+    if (n[i].getKind() == INST_CONSTANT)
+    {
+      // must get the quantified formula this belongs to, which may be
+      // different from q
+      Node qi = TermUtil::getInstConstAttr(n[i]);
+      unsigned id = n[i].getAttribute(InstVarNumAttribute());
+      rdl.d_rd[i] = getRDomain(qi, id, false);
+      varCount++;
+      varCh = i;
     }
-    
-    Node r_add;
-    bool varLhs = true;
-    if( varCount==2 ){
-      rdl.d_merge = true;
-    }else{
-      if( varCount==1 ){
-        r_add = n[1-varCh];
-        varLhs = (varCh==0);
-        rdl.d_rd[0] = rdl.d_rd[varCh];
-        rdl.d_rd[1] = nullptr;
-      }else{
-        //solve the inequality for one/two variables, if possible
-        if (n[0].getType().isRealOrInt())
+    else
+    {
+      rdl.d_rd[i] = nullptr;
+    }
+  }
+
+  Node rAdd;
+  Node rVar;
+  bool varLhs = true;
+  if (varCount == 2)
+  {
+    // don't merge Int and Real
+    rdl.d_merge = (n[0].getType() == n[1].getType());
+  }
+  else if (varCount == 1)
+  {
+    rVar = n[varCh];
+    rAdd = n[1 - varCh];
+    varLhs = (varCh == 0);
+    rdl.d_rd[0] = rdl.d_rd[varCh];
+    rdl.d_rd[1] = nullptr;
+  }
+  else if (n[0].getType().isRealOrInt())
+  {
+    // solve the inequality for one/two variables, if possible
+    std::map<Node, Node> msum;
+    if (ArithMSum::getMonomialSumLit(n, msum))
+    {
+      Node var;
+      Node var2;
+      bool hasNonVar = false;
+      for (std::pair<const Node, Node>& m : msum)
+      {
+        if (!m.first.isNull() && m.first.getKind() == INST_CONSTANT
+            && TermUtil::getInstConstAttr(m.first) == q)
         {
-          std::map< Node, Node > msum;
-          if (ArithMSum::getMonomialSumLit(n, msum))
+          if (var.isNull())
           {
-            Node var;
-            Node var2;
-            bool hasNonVar = false;
-            for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-              if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
-                  && TermUtil::getInstConstAttr(it->first) == q)
-              {
-                if( var.isNull() ){
-                  var = it->first;
-                }else if( var2.isNull() ){
-                  var2 = it->first;
-                }else{
-                  hasNonVar = true;
-                }
-              }else{
-                hasNonVar = true;
-              }
-            }
-            Trace("rel-dom") << "Process lit " << n << ", var/var2=" << var
-                             << "/" << var2 << std::endl;
-            if( !var.isNull() ){
-              Assert(var.hasAttribute(InstVarNumAttribute()));
-              if( var2.isNull() ){
-                //single variable solve
-                Node veq_c;
-                Node val;
-                int ires =
-                    ArithMSum::isolate(var, msum, veq_c, val, n.getKind());
-                if( ires!=0 ){
-                  if( veq_c.isNull() ){
-                    r_add = val;
-                    varLhs = (ires==1);
-                    rdl.d_rd[0] = getRDomain(
-                        q, var.getAttribute(InstVarNumAttribute()), false);
-                    rdl.d_rd[1] = nullptr;
-                  }
-                }
-              }else if( !hasNonVar ){
-                Assert(var2.hasAttribute(InstVarNumAttribute()));
-                //merge the domains
-                rdl.d_rd[0] = getRDomain(
-                    q, var.getAttribute(InstVarNumAttribute()), false);
-                rdl.d_rd[1] = getRDomain(
-                    q, var2.getAttribute(InstVarNumAttribute()), false);
-                rdl.d_merge = true;
-              }
+            var = m.first;
+          }
+          else if (var2.isNull())
+          {
+            var2 = m.first;
+          }
+          else
+          {
+            hasNonVar = true;
+          }
+        }
+        else
+        {
+          hasNonVar = true;
+        }
+      }
+      Trace("rel-dom") << "Process lit " << n << ", var/var2=" << var << "/"
+                       << var2 << std::endl;
+      if (!var.isNull())
+      {
+        Assert(var.hasAttribute(InstVarNumAttribute()));
+        if (var2.isNull())
+        {
+          // single variable solve
+          Node veq_c;
+          Node val;
+          int ires = ArithMSum::isolate(var, msum, veq_c, val, n.getKind());
+          if (ires != 0)
+          {
+            if (veq_c.isNull())
+            {
+              rVar = var;
+              rAdd = val;
+              varLhs = (ires == 1);
+              rdl.d_rd[0] =
+                  getRDomain(q, var.getAttribute(InstVarNumAttribute()), false);
+              rdl.d_rd[1] = nullptr;
             }
           }
         }
+        else if (!hasNonVar)
+        {
+          Assert(var2.hasAttribute(InstVarNumAttribute()));
+          // merge the domains
+          rdl.d_rd[0] =
+              getRDomain(q, var.getAttribute(InstVarNumAttribute()), false);
+          rdl.d_rd[1] =
+              getRDomain(q, var2.getAttribute(InstVarNumAttribute()), false);
+          rdl.d_merge = true;
+        }
       }
     }
-    if (rdl.d_merge)
+  }
+  if (rdl.d_merge)
+  {
+    // do not merge if constant negative polarity
+    if (hasPol && !pol)
     {
-      //do not merge if constant negative polarity
-      if( hasPol && !pol ){
-        rdl.d_merge = false;
-      }
+      rdl.d_merge = false;
+    }
+    return;
+  }
+  if (!rAdd.isNull())
+  {
+    // Ensure that rAdd has the same type as the variable. This is necessary
+    // since GEQ may mix Int and Real, as well as the equality solving above
+    // may introduce mixed Int and Real.
+    rAdd = Instantiate::ensureType(rAdd, rVar.getType());
+  }
+  if (!rAdd.isNull() && !TermUtil::hasInstConstAttr(rAdd))
+  {
+    Trace("rel-dom-debug") << "...add term " << rAdd << ", pol = " << pol
+                           << ", kind = " << n.getKind() << std::endl;
+    // the negative occurrence adds the term to the domain
+    if (!hasPol || !pol)
+    {
+      rdl.d_val.push_back(rAdd);
     }
-    else if (!r_add.isNull() && !TermUtil::hasInstConstAttr(r_add))
+    // the positive occurence adds other terms
+    if ((!hasPol || pol) && n[0].getType().isInteger())
     {
-      Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl;
-      //the negative occurrence adds the term to the domain
-      if( !hasPol || !pol ){
-        rdl.d_val.push_back(r_add);
-      }
-      //the positive occurence adds other terms
-      if( ( !hasPol || pol ) && n[0].getType().isInteger() ){
-        if( n.getKind()==EQUAL ){
-          for( unsigned i=0; i<2; i++ ){
-            Node roff = nm->mkNode(
-                ADD, r_add, nm->mkConstInt(Rational(i == 0 ? 1 : -1)));
-            rdl.d_val.push_back(roff);
-          }
-        }else if( n.getKind()==GEQ ){
+      if (n.getKind() == EQUAL)
+      {
+        for (size_t i = 0; i < 2; i++)
+        {
           Node roff =
-              nm->mkNode(ADD, r_add, nm->mkConstInt(Rational(varLhs ? 1 : -1)));
+              nm->mkNode(ADD, rAdd, nm->mkConstInt(Rational(i == 0 ? 1 : -1)));
           rdl.d_val.push_back(roff);
         }
       }
+      else if (n.getKind() == GEQ)
+      {
+        Node roff =
+            nm->mkNode(ADD, rAdd, nm->mkConstInt(Rational(varLhs ? 1 : -1)));
+        rdl.d_val.push_back(roff);
+      }
     }
-    else
-    {
-      rdl.d_rd[0] = nullptr;
-      rdl.d_rd[1] = nullptr;
-    }
+  }
+  else
+  {
+    rdl.d_rd[0] = nullptr;
+    rdl.d_rd[1] = nullptr;
   }
 }
 

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index aa500578889de0f62d1d641e73933b9dc041a0f7..c7ee7ca1d337982469834026b9e4e3711f746e82 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2297,6 +2297,7 @@ set(regress_1_tests
   regress1/quantifiers/issue8517-exp-exp.smt2
   regress1/quantifiers/issue8520-cegqi-nl-cov.smt2
   regress1/quantifiers/issue8572-sygus-inst-ic-purify.smt2
+  regress1/quantifiers/issue8881-rd-types.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2

diff --git a/test/regress/cli/regress1/quantifiers/issue8881-rd-types.smt2 b/test/regress/cli/regress1/quantifiers/issue8881-rd-types.smt2
new file mode 100644 (file)
index 0000000..218dbd4
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/issue8881-rd-types.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unknown
+(set-logic ALL)
+(set-option :full-saturate-quant true)
+(declare-fun q2 (Real Real) Bool)
+(assert (forall ((x2 Real)) (q2 x2 (ite (< x2 1.0) x2 1.0))))
+(check-sat)