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.

2 files changed, 27 insertions, 0 deletions

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)