Improvements and fixes in cegqi arithmetic (#2247)

This includes several improvements for cegqi with arithmetic:
- Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV),
- Equalities are handled by processAssertions,
- Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV),
- cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic.

It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.:
`a+b*delta > c+d*delta if a>=c and b>=d`
Whereas the correct check is lexicographic:
`a+b*delta > c+d*delta if a>c or a=c and b>d`
This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred.

This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA.

4 files changed, 78 insertions, 12 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 5cd7a6892..f1235d185 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -20,6 +20,7 @@
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/quantifiers/term_util.h"
+#include "util/random.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -118,7 +119,7 @@ bool ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
                                             Node pv,
                                             CegInstEffort effort)
 {
-  return true;
+  return effort != CEG_INST_EFFORT_FULL;
 }
 
 Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
@@ -128,10 +129,9 @@ Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
                                             CegInstEffort effort)
 {
   Node atom = lit.getKind() == NOT ? lit[0] : lit;
-  bool pol = lit.getKind() != NOT;
   // arithmetic inequalities and disequalities
   if (atom.getKind() == GEQ
-      || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal()))
+      || (atom.getKind() == EQUAL && atom[0].getType().isReal()))
   {
     return lit;
   }
@@ -150,7 +150,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
   bool pol = lit.getKind() != NOT;
   // arithmetic inequalities and disequalities
   Assert(atom.getKind() == GEQ
-         || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal()));
+         || (atom.getKind() == EQUAL && atom[0].getType().isReal()));
   // get model value for pv
   Node pv_value = ci->getModelValue(pv);
   // cannot contain infinity?
@@ -165,8 +165,12 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
   {
     return false;
   }
-  // disequalities are either strict upper or lower bounds
-  unsigned rmax = (atom.getKind() == GEQ || options::cbqiModel()) ? 1 : 2;
+  // compute how many bounds we will consider
+  unsigned rmax = 1;
+  if (atom.getKind() == EQUAL && (pol || !options::cbqiModel()))
+  {
+    rmax = 2;
+  }
   for (unsigned r = 0; r < rmax; r++)
   {
     int uires = ires;
@@ -190,8 +194,14 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
         }
       }
     }
+    else if (pol)
+    {
+      // equalities are both non-strict upper and lower bounds
+      uires = r == 0 ? 1 : -1;
+    }
     else
     {
+      // disequalities are either strict upper or lower bounds
       bool is_upper;
       if (options::cbqiModel())
       {
@@ -226,11 +236,12 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
           Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value);
           cmp = Rewriter::rewrite(cmp);
           Assert(cmp.isConst());
-          is_upper = (cmp != ci->getQuantifiersEngine()->getTermUtil()->d_true);
+          is_upper = !cmp.isConst() || !cmp.getConst<bool>();
         }
       }
       else
       {
+        // since we are not using the model, we try both.
         is_upper = (r == 0);
       }
       Assert(atom.getKind() == EQUAL && !pol);
@@ -319,7 +330,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
   bool use_inf = ci->useVtsInfinity()
                  && (d_type.isInteger() ? options::cbqiUseInfInt()
                                         : options::cbqiUseInfReal());
-  bool upper_first = false;
+  bool upper_first = Random::getRandom().pickWithProb(0.5);
   if (options::cbqiMinBounds())
   {
     upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size();
@@ -353,6 +364,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         {
           return true;
         }
+        else if (!options::cbqiMultiInst())
+        {
+          return false;
+        }
       }
     }
     else
@@ -389,6 +404,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         t_values[rr].push_back(Node::null());
         // check if it is better than the current best bound : lexicographic
         // order infinite/finite/infinitesimal parts
+        bool new_best_set = false;
         bool new_best = true;
         for (unsigned t = 0; t < 3; t++)
         {
@@ -435,8 +451,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
                 value[t]);
             value[t] = Rewriter::rewrite(value[t]);
           }
-          // check if new best
-          if (best != -1)
+          // check if new best, if we have not already set it.
+          if (best != -1 && !new_best_set)
           {
             Assert(!value[t].isNull() && !best_bound_value[t].isNull());
             if (value[t] != best_bound_value[t])
@@ -444,12 +460,17 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
               Kind k = rr == 0 ? GEQ : LEQ;
               Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]);
               cmp_bound = Rewriter::rewrite(cmp_bound);
-              if (cmp_bound
-                  != ci->getQuantifiersEngine()->getTermUtil()->d_true)
+              // Should be comparing two constant values which should rewrite
+              // to a constant. If a step failed, we assume that this is not
+              // the new best bound.
+              Assert(cmp_bound.isConst());
+              if (!cmp_bound.isConst() || !cmp_bound.getConst<bool>())
               {
                 new_best = false;
                 break;
               }
+              // indicate that the value of new_best is now established.
+              new_best_set = true;
             }
           }
         }
@@ -504,6 +525,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
             {
               return true;
             }
+            else if (!options::cbqiMultiInst())
+            {
+              return false;
+            }
           }
         }
       }
@@ -531,6 +556,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       {
         return true;
       }
+      else if (!options::cbqiMultiInst())
+      {
+        return false;
+      }
     }
   }
   if (options::cbqiMidpoint() && !d_type.isInteger())
@@ -598,6 +627,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       {
         return true;
       }
+      else if (!options::cbqiMultiInst())
+      {
+        return false;
+      }
     }
   }
   // generally should not make it to this point, unless we are using a
@@ -637,6 +670,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
           {
             return true;
           }
+          else if (!options::cbqiMultiInst())
+          {
+            return false;
+          }
         }
       }
     }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 0b9e415fa..017e4f9bd 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1251,6 +1251,7 @@ REG1_TESTS = \
 	regress1/quantifiers/NUM878.smt2 \
 	regress1/quantifiers/RND-small.smt2 \
 	regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 \
+	regress1/quantifiers/RND_4_1-existing-inst.smt2 \
 	regress1/quantifiers/RND_4_16.smt2 \
 	regress1/quantifiers/anti-sk-simp.smt2 \
 	regress1/quantifiers/ari118-bv-2occ-x.smt2 \
@@ -1308,6 +1309,7 @@ REG1_TESTS = \
 	regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \
 	regress1/quantifiers/qcft-smtlib3dbc51.smt2 \
 	regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \
+	regress1/quantifiers/repair-const-nterm.smt2 \
 	regress1/quantifiers/recfact.cvc \
 	regress1/quantifiers/rew-to-0211-dd.smt2 \
 	regress1/quantifiers/ricart-agrawala6.smt2 \
diff --git a/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 b/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2
new file mode 100644
index 000000000..73c278522
--- /dev/null
+++ b/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2
@@ -0,0 +1,15 @@
+(set-logic LRA)
+(set-info :status unsat)
+(declare-fun a () Real)
+(assert 
+  (forall ((?y2 Real) (?y3 Real)) 
+    (or 
+        (= ?y3 1) 
+        (> ?y3 0)
+        (and 
+          (< ?y2 0) 
+          (< ?y3 49) 
+        )))
+)
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/quantifiers/repair-const-nterm.smt2 b/test/regress/regress1/quantifiers/repair-const-nterm.smt2
new file mode 100644
index 000000000..f9b1d6829
--- /dev/null
+++ b/test/regress/regress1/quantifiers/repair-const-nterm.smt2
@@ -0,0 +1,12 @@
+(set-logic LIA)
+(set-info :status unsat)
+
+(declare-fun k_20 () Int)
+(declare-fun k_72 () Int)
+(declare-fun k_73 () Int)
+
+(assert
+(forall ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) (not (>= (+ (* 3 x7) (* (- 1) (ite (= x7 k_20) k_72 k_73))) 1)) )
+)
+
+(check-sat)