Fix issue with free variables introduced by quantifier rewriter (#5602)

This was caused by the quantifiers rewriting eliminating extended arithmetic operators, which was required due to the way counterexample-guided quantifier instantiation used to work with preprocessing. The technique is now more robust and this option can be deleted.

This fixes a debug assertion failure from UFNIA SMT-LIB, a minimized benchmark is included as a regression.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index d29052042d0760e0a945234f2fd7aefcaa6fc8c8..57bf69162d477cdaf4439fd618b2acd78e25c96d 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -177,14 +177,6 @@ header = "options/quantifiers_options.h"
   read_only  = true
   help       = "eliminate tautological disjuncts of quantified formulas"
 
-[[option]]
-  name       = "elimExtArithQuant"
-  category   = "regular"
-  long       = "elim-ext-arith-quant"
-  type       = "bool"
-  default    = "true"
-  help       = "eliminate extended arithmetic symbols in quantified formulas"
-
 [[option]]
   name       = "extRewriteQuant"
   category   = "regular"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7e6bed464b0778f97ce5b4881ff7a9b53002c075..ca5a2773b5781023e6ccdd65c7217f024e884ab7 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -239,14 +239,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       options::fmfBound.set(true);
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
-    // Do not eliminate extended arithmetic symbols from quantified formulas,
-    // since some strategies, e.g. --re-elim-agg, introduce them.
-    if (!options::elimExtArithQuant.wasSetByUser())
-    {
-      options::elimExtArithQuant.set(false);
-      Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp"
-                   << std::endl;
-    }
     // Note we allow E-matching by default to support combinations of sequences
     // and quantifiers.
   }
@@ -935,11 +927,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT);
     }
-    // do not eliminate extended arithmetic symbols from quantified formulas
-    if (!options::elimExtArithQuant.wasSetByUser())
-    {
-      options::elimExtArithQuant.set(false);
-    }
     if (!options::eMatching.wasSetByUser())
     {
       options::eMatching.set(options::fmfInstEngine());

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index aa847d8ea3ff7fa3d3ec33109ac8ce3ee8742672..0a5deb4802ccd783af590c3dc8f4ea94284866b0 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -250,9 +250,10 @@ bool CegInstantiator::isEligible( Node n ) {
 CegHandledStatus CegInstantiator::isCbqiKind(Kind k)
 {
   if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ
-      || k == EQUAL
-      || k == MULT
-      || k == NONLINEAR_MULT)
+      || k == EQUAL || k == MULT || k == NONLINEAR_MULT || k == DIVISION
+      || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL
+      || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == TO_INTEGER
+      || k == IS_INTEGER)
   {
     return CEG_HANDLED;
   }

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 6d7275facbd8ccc964e661846b42dbb24cd4bbbe..20d80779387aea52b5d3c93d8f80899a183c20e6 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -401,11 +401,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
     Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
     if (!fbody.isNull())
     {
-      Node r = computeProcessTerms2(fbody,
-                                    cache,
-                                    new_vars,
-                                    new_conds,
-                                    false);
+      Node r = computeProcessTerms2(fbody, cache, new_vars, new_conds);
       Assert(new_vars.size() == h.getNumChildren());
       return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r));
     }
@@ -413,18 +409,13 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
     // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to
     // forall xy. false.
   }
-  return computeProcessTerms2(body,
-                              cache,
-                              new_vars,
-                              new_conds,
-                              options::elimExtArithQuant());
+  return computeProcessTerms2(body, cache, new_vars, new_conds);
 }
 
 Node QuantifiersRewriter::computeProcessTerms2(Node body,
                                                std::map<Node, Node>& cache,
                                                std::vector<Node>& new_vars,
-                                               std::vector<Node>& new_conds,
-                                               bool elimExtArith)
+                                               std::vector<Node>& new_conds)
 {
   NodeManager* nm = NodeManager::currentNM();
   Trace("quantifiers-rewrite-term-debug2")
@@ -438,8 +429,7 @@ Node QuantifiersRewriter::computeProcessTerms2(Node body,
   for (size_t i = 0; i < body.getNumChildren(); i++)
   {
     // do the recursive call on children
-    Node nn =
-        computeProcessTerms2(body[i], cache, new_vars, new_conds, elimExtArith);
+    Node nn = computeProcessTerms2(body[i], cache, new_vars, new_conds);
     children.push_back(nn);
     changed = changed || nn != body[i];
   }
@@ -515,82 +505,6 @@ Node QuantifiersRewriter::computeProcessTerms2(Node body,
       ret = nm->mkNode(ITE, iconds[i], elements[i], ret);
     }
   }
-  else if (elimExtArith)
-  {
-    if (ret.getKind() == INTS_DIVISION_TOTAL
-        || ret.getKind() == INTS_MODULUS_TOTAL)
-    {
-      Node num = ret[0];
-      Node den = ret[1];
-      if (den.isConst())
-      {
-        const Rational& rat = den.getConst<Rational>();
-        Assert(!num.isConst());
-        if (rat != 0)
-        {
-          Node intVar = nm->mkBoundVar(nm->integerType());
-          new_vars.push_back(intVar);
-          Node cond;
-          if (rat > 0)
-          {
-            cond = nm->mkNode(
-                AND,
-                nm->mkNode(LEQ, nm->mkNode(MULT, den, intVar), num),
-                nm->mkNode(
-                    LT,
-                    num,
-                    nm->mkNode(
-                        MULT,
-                        den,
-                        nm->mkNode(PLUS, intVar, nm->mkConst(Rational(1))))));
-          }
-          else
-          {
-            cond = nm->mkNode(
-                AND,
-                nm->mkNode(LEQ, nm->mkNode(MULT, den, intVar), num),
-                nm->mkNode(
-                    LT,
-                    num,
-                    nm->mkNode(
-                        MULT,
-                        den,
-                        nm->mkNode(PLUS, intVar, nm->mkConst(Rational(-1))))));
-          }
-          new_conds.push_back(cond.negate());
-          if (ret.getKind() == INTS_DIVISION_TOTAL)
-          {
-            ret = intVar;
-          }
-          else
-          {
-            ret = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
-          }
-        }
-      }
-    }
-    else if (ret.getKind() == TO_INTEGER || ret.getKind() == IS_INTEGER)
-    {
-      Node intVar = nm->mkBoundVar(nm->integerType());
-      new_vars.push_back(intVar);
-      new_conds.push_back(
-          nm->mkNode(
-                AND,
-                nm->mkNode(LT,
-                           nm->mkNode(MINUS, ret[0], nm->mkConst(Rational(1))),
-                           intVar),
-                nm->mkNode(LEQ, intVar, ret[0]))
-              .negate());
-      if (ret.getKind() == TO_INTEGER)
-      {
-        ret = intVar;
-      }
-      else
-      {
-        ret = ret[0].eqNode(intVar);
-      }
-    }
-  }
   cache[body] = ret;
   return ret;
 }
@@ -1865,9 +1779,7 @@ bool QuantifiersRewriter::doOperation(Node q,
   }
   else if (computeOption == COMPUTE_PROCESS_TERMS)
   {
-    return is_std
-           && (options::elimExtArithQuant()
-               || options::iteLiftQuant() != options::IteLiftQuantMode::NONE);
+    return is_std && options::iteLiftQuant() != options::IteLiftQuantMode::NONE;
   }
   else if (computeOption == COMPUTE_COND_SPLIT)
   {

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 550f5b1dc36a4f5801c0177bc688cca265b9ed87..78586fc87f4f987ff1485215d4ed44dd44736227 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -155,8 +155,7 @@ class QuantifiersRewriter : public TheoryRewriter
   static Node computeProcessTerms2(Node body,
                                    std::map<Node, Node>& cache,
                                    std::vector<Node>& new_vars,
-                                   std::vector<Node>& new_conds,
-                                   bool elimExtArith);
+                                   std::vector<Node>& new_conds);
   static void computeDtTesterIteSplit(
       Node n,
       std::map<Node, Node>& pcons,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5298a2ca972c4b961bae88f08abb52d959e5a3b5..d0e28f9e58133dab462644a584cc895cf6a2e51b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -820,6 +820,7 @@ set(regress_0_tests
   regress0/quantifiers/simp-typ-test.smt2
   regress0/quantifiers/sygus-inst-nia-psyco-060.smt2
   regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
+  regress0/quantifiers/ufnia-fv-delta.smt2
   regress0/rec-fun-const-parse-bug.smt2
   regress0/rels/addr_book_0.cvc
   regress0/rels/atom_univ2.cvc

diff --git a/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2 b/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2
new file mode 100644 (file)
index 0000000..dfb87a1
--- /dev/null
+++ b/test/regress/regress0/quantifiers/ufnia-fv-delta.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
+(set-logic UFNIA)
+(assert (exists ((k Int)) (not (=> (forall ((a Int) (b Int)) (! (= k (ite (= 0 (mod a 2)) 1 0)) :pattern (b))) false))))
+(check-sat)