Fix subtype issue in cegqi arithmetic (#8440)

Fixes #8410.

Was not properly checking for cases where an Integer variable had a Real term as its solution.

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 8c10d49aaf7c945d1ee64457befe168fbb6dca13..0b94bdc37efe4b70fd5613951e558e1044336707 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -144,6 +144,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
                                          Node alit,
                                          CegInstEffort effort)
 {
+  Trace("cegqi-arith-debug") << "Process assertion " << lit << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   Node atom = lit.getKind() == NOT ? lit[0] : lit;
   bool pol = lit.getKind() != NOT;
@@ -828,9 +829,10 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
     return CEG_TT_INVALID;
   }
   // if its type is integer but the substitution is not integer
+  Node vval = mkVtsSum(val, vts_coeff[0], vts_coeff[1]);
   if (pvtn.isInteger()
       && ((!veq_c.isNull() && !veq_c.getType().isInteger())
-          || !val.getType().isInteger()))
+          || !vval.getType().isInteger()))
   {
     // redo, split integer/non-integer parts
     bool useCoeff = false;
@@ -985,20 +987,28 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
     val = rewrite(val);
     Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
   }
+  return mkVtsSum(val, inf_coeff, delta_coeff);
+}
+
+Node ArithInstantiator::mkVtsSum(const Node& val,
+                                 const Node& inf_coeff,
+                                 const Node& delta_coeff)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node vval = val;
   if (!inf_coeff.isNull())
   {
     Assert(!d_vts_sym[0].isNull());
-    val = nm->mkNode(ADD, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0]));
-    val = rewrite(val);
+    vval = nm->mkNode(ADD, vval, nm->mkNode(MULT, inf_coeff, d_vts_sym[0]));
   }
   if (!delta_coeff.isNull())
   {
     // create delta here if necessary
-    val = nm->mkNode(
-        ADD, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta()));
-    val = rewrite(val);
+    vval = nm->mkNode(
+        ADD, vval, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta()));
   }
-  return val;
+  vval = rewrite(vval);
+  return vval;
 }
 
 Node ArithInstantiator::negate(const Node& t) const

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
index fecb857226fa5f9be9faabad707234b1424cd841..cf75a3e45953153b97622e901a615179ca4ce66a 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
@@ -208,6 +208,12 @@ class ArithInstantiator : public Instantiator
                                     Node delta_coeff);
   /** Return the rewritten form of the negation of t */
   Node negate(const Node& t) const;
+  /**
+   * Make the node from base value, with infinity and delta coefficients.
+   */
+  Node mkVtsSum(const Node& val,
+                const Node& inf_coeff,
+                const Node& delta_coeff);
 };
 
 }  // namespace quantifiers

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 0be469ac7b6f0f51e2fb28aa5829fc6ef5db4c11..f10e59540cecd88de9f1f42c05f9657314de2db4 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -146,6 +146,7 @@ void TermProperties::composeProperty(TermProperties& p)
 // push the substitution pv_prop.getModifiedTerm(pv) -> n
 void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop)
 {
+  Assert(n.getType().isSubtypeOf(pv.getType()));
   d_vars.push_back(pv);
   d_subs.push_back(n);
   d_props.push_back(pv_prop);
@@ -938,6 +939,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
                                                 SolvedForm& sf,
                                                 bool revertOnSuccess)
 {
+  Assert(n.getType().isSubtypeOf(pv.getType()));
   Node cnode = pv_prop.getCacheNode();
   if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
     d_curr_subs_proc[pv][n][cnode] = true;

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index ac0ec5f052a752fd43efcac92cc2a429dcf3d9fb..4f37e2e2eb5e8825f600f2c3bd1209d7d6d7b777 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2213,6 +2213,7 @@ set(regress_1_tests
   regress1/quantifiers/issue7537-cegqi-comp-types.smt2
   regress1/quantifiers/issue8157-duplicate-conflicts.smt2
   regress1/quantifiers/issue8344-cegqi-string-witness.smt2
+  regress1/quantifiers/issue8410-vts-subtypes.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/issue8410-vts-subtypes.smt2 b/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2
new file mode 100644 (file)
index 0000000..3a2905f
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: -i
+; EXPECT: unsat
+(set-logic ALL)
+(push)
+(assert (or (forall ((v Real)) (or (exists ((V Real)) (or (exists ((V Real)) (= 0 (mod (to_int v) (to_int (- v)))))))))))
+(check-sat)