Do not introduce mixed arithmetic in transcendental proof rules (cvc5#12101)

Also adds a regression for `ARITH_TRANS_SINE_APPROX_BELOW_NEG`, which
was missing.

---------

Co-authored-by: Haniel Barbosa <[email protected]>

Author: ajreynol

include/cvc5/cvc5_proof_rule.h

@@ -2208,7 +2208,7 @@ enum ENUM(ProofRule)
    *
    * .. math::
    *
-   *   \inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)}
+   *   \inferrule{- \mid t}{(t < 0.0) \leftrightarrow (\exp(t) < 1.0)}
    *
    * \endverbatim
    */
@@ -2219,7 +2219,7 @@ enum ENUM(ProofRule)
    *
    * .. math::
    *
-   *   \inferrule{- \mid t}{\exp(t) > 0}
+   *   \inferrule{- \mid t}{\exp(t) > 0.0}
    *
    * \endverbatim
    */
@@ -2231,7 +2231,7 @@ enum ENUM(ProofRule)
    *
    * .. math::
    *
-   *   \inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1}
+   *   \inferrule{- \mid t}{t \leq 0.0 \lor \exp(t) > t+1.0}
    *
    * \endverbatim
    */
@@ -2242,7 +2242,7 @@ enum ENUM(ProofRule)
    *
    * .. math::
    *
-   *   \inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)}
+   *   \inferrule{- \mid t}{(t=0.0) \leftrightarrow (\exp(t) = 1.0)}
    *
    * \endverbatim
    */
@@ -2336,7 +2336,7 @@ enum ENUM(ProofRule)
    *
    * .. math::
    *
-   *   \inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1}
+   *   \inferrule{- \mid t}{\sin(t) \leq 1.0 \land \sin(t) \geq -1.0}
    *
    * \endverbatim
    */
@@ -2368,7 +2368,7 @@ enum ENUM(ProofRule)
    *
    * .. math::
    *
-   *   \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0}
+   *   \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0.0}
    *
    * \endverbatim
    */
@@ -2379,7 +2379,7 @@ enum ENUM(ProofRule)
    *
    * .. math::
    *
-   *   \inferrule{- \mid t}{(t > 0 \rightarrow \sin(t) < t) \land (t < 0
+   *   \inferrule{- \mid t}{(t > 0.0 \rightarrow \sin(t) < t) \land (t < 0.0
    *   \rightarrow \sin(t) > t)}
    *
    * \endverbatim

proofs/eo/cpc/expert/rules/Transcendentals.eo

@@ -24,7 +24,7 @@
 (declare-rule arith_trans_exp_neg ((x Real))
   :premises ()
   :args (x)
-  :conclusion (= (< x 0) (< (exp x) 1))
+  :conclusion (= (< x 0/1) (< (exp x) 1/1))
 )
 
 ; rule: arith_trans_exp_positivity
@@ -35,7 +35,7 @@
 (declare-rule arith_trans_exp_positivity ((x Real))
   :premises ()
   :args (x)
-  :conclusion (> (exp x) 0)
+  :conclusion (> (exp x) 0/1)
 )
 
 ; rule: arith_trans_exp_super_lin
@@ -47,7 +47,7 @@
 ;   greater than its argument plus one.
 (declare-rule arith_trans_exp_super_lin ((x Real))
   :args (x)
-  :conclusion (or (<= x 0) (> (exp x) (+ x 1)))
+  :conclusion (or (<= x 0/1) (> (exp x) (+ x 1/1)))
 )
 
 ; rule: arith_trans_exp_zero
@@ -69,7 +69,7 @@
 ; conclusion: The sine is within positive and negative one.
 (declare-rule arith_trans_sine_bounds ((x Real))
   :args (x)
-  :conclusion (and (<= (sin x) 1) (>= (sin x) -1))
+  :conclusion (and (<= (sin x) 1/1) (>= (sin x) -1/1))
 )
 
 ; rule: arith_trans_sine_symmetry
@@ -81,7 +81,7 @@
 ;   sine is symmetric wrt the point 0.
 (declare-rule arith_trans_sine_symmetry ((x Real))
   :args (x)
-  :conclusion (= (+ (sin x) (sin (* -1 x))) 0)
+  :conclusion (= (+ (sin x) (sin (* -1/1 x))) 0/1)
 )
 
 ; rule: arith_trans_sine_tangent_zero
@@ -93,7 +93,7 @@
 ;   x is less than zero, sin is greater than x.
 (declare-rule arith_trans_sine_tangent_zero ((x Real))
   :args (x)
-  :conclusion (and (=> (> x 0) (< (sin x) x)) (=> (< x 0) (> (sin x) x)))
+  :conclusion (and (=> (> x 0/1) (< (sin x) x)) (=> (< x 0/1) (> (sin x) x)))
 )
 
 ; rule: arith_trans_sine_tangent_pi
@@ -105,5 +105,5 @@
 ;   x is less than pi, sin is less than pi minus x.
 (declare-rule arith_trans_sine_tangent_pi ((x Real))
   :args (x)
-  :conclusion (and (=> (> x (* -1 real.pi)) (> (sin x) (- (* -1 real.pi) x))) (=> (< x real.pi) (< (sin x) (- real.pi x))))
+  :conclusion (and (=> (> x (* -1/1 real.pi)) (> (sin x) (- (* -1/1 real.pi) x))) (=> (< x real.pi) (< (sin x) (- real.pi x))))
 )

src/theory/arith/nl/transcendental/exponential_solver.cpp

@@ -81,8 +81,8 @@ void ExponentialSolver::checkInitialRefine()
       // initial refinements
       if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end())
       {
-        Node zero = nm->mkConstInt(Rational(0));
-        Node one = nm->mkConstInt(Rational(1));
+        Node zero = nm->mkConstReal(Rational(0));
+        Node one = nm->mkConstReal(Rational(1));
         d_tf_initial_refine[t] = true;
         {
           // exp is always positive: exp(t) > 0

src/theory/arith/nl/transcendental/proof_checker.cpp

@@ -82,9 +82,9 @@ Node TranscendentalProofRuleChecker::checkInternal(
     const std::vector<Node>& args)
 {
   NodeManager* nm = nodeManager();
-  Node zero = nm->mkConstInt(Rational(0));
-  Node one = nm->mkConstInt(Rational(1));
-  Node mone = nm->mkConstInt(Rational(-1));
+  Node zero = nm->mkConstReal(Rational(0));
+  Node one = nm->mkConstReal(Rational(1));
+  Node mone = nm->mkConstReal(Rational(-1));
   Node pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
   Node mpi = nm->mkNode(Kind::MULT, mone, pi);
   Trace("nl-trans-checker") << "Checking " << id << std::endl;

src/theory/arith/nl/transcendental/sine_solver.cpp

@@ -226,15 +226,20 @@ void SineSolver::checkInitialRefine()
       // initial refinements
       if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end())
       {
+        NodeManager * nm = nodeManager();
+        Node zero = nm->mkConstReal(Rational(0));
+        Node one = nm->mkConstReal(Rational(1));
+        Node mone = nm->mkConstReal(Rational(-1));
+        Node mpi = nm->mkNode(Kind::MULT, mone, d_pi);
         Trace("nl-ext-debug") << "Process initial refine " << t << std::endl;
         d_tf_initial_refine[t] = true;
         Assert(d_data->isPurified(t));
         {
           // sine bounds: -1 <= sin(t) <= 1
           Node lem = NodeManager::mkNode(
               Kind::AND,
-              NodeManager::mkNode(Kind::LEQ, t, d_data->d_one),
-              NodeManager::mkNode(Kind::GEQ, t, d_data->d_neg_one));
+              NodeManager::mkNode(Kind::LEQ, t, one),
+              NodeManager::mkNode(Kind::GEQ, t, mone));
           CDProof* proof = nullptr;
           if (d_data->isProofEnabled())
           {
@@ -252,11 +257,11 @@ void SineSolver::checkInitialRefine()
               Kind::AND,
               NodeManager::mkNode(
                   Kind::IMPLIES,
-                  NodeManager::mkNode(Kind::GT, t[0], d_data->d_zero),
+                  NodeManager::mkNode(Kind::GT, t[0], zero),
                   NodeManager::mkNode(Kind::LT, t, t[0])),
               NodeManager::mkNode(
                   Kind::IMPLIES,
-                  NodeManager::mkNode(Kind::LT, t[0], d_data->d_zero),
+                  NodeManager::mkNode(Kind::LT, t[0], zero),
                   NodeManager::mkNode(Kind::GT, t, t[0])));
           CDProof* proof = nullptr;
           if (d_data->isProofEnabled())
@@ -276,11 +281,11 @@ void SineSolver::checkInitialRefine()
               Kind::AND,
               NodeManager::mkNode(
                   Kind::IMPLIES,
-                  NodeManager::mkNode(Kind::GT, t[0], d_neg_pi),
+                  NodeManager::mkNode(Kind::GT, t[0], mpi),
                   NodeManager::mkNode(
                       Kind::GT,
                       t,
-                      NodeManager::mkNode(Kind::SUB, d_neg_pi, t[0]))),
+                      NodeManager::mkNode(Kind::SUB, mpi, t[0]))),
               NodeManager::mkNode(
                   Kind::IMPLIES,
                   NodeManager::mkNode(Kind::LT, t[0], d_pi),

test/regress/cli/CMakeLists.txt

@@ -1153,6 +1153,7 @@ set(regress_0_tests
   regress0/nl/nia-wrong-tl.smt2
   regress0/nl/nlExtPurify-test.smt2
   regress0/nl/nta/cos-sig-value.smt2
+  regress0/nl/nta/dd.mirko_example_01.k5.bound300.smt2
   regress0/nl/nta/exp-n0.5-lb.smt2
   regress0/nl/nta/exp-n0.5-ub.smt2
   regress0/nl/nta/exp-neg2-unsat-unsound.smt2

test/regress/cli/regress0/nl/nta/dd.mirko_example_01.k5.bound300.smt2

@@ -0,0 +1,12 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const x774336__fresh Bool)
+(declare-const x957672__fresh Bool)
+(declare-fun y2@3 () Real)
+(declare-fun t@3 () Real)
+(declare-fun y1@5 () Real)
+(declare-fun y2@5 () Real)
+(declare-fun t@4 () Real)
+(declare-fun t@5 () Real)
+(assert (let ((.def_7 false)) (let ((.def_15 false)) (let ((.def_26 false)) (let ((.def_28 false)) (let ((.def_32 false)) (let ((.def_39 false)) (let ((.def_40 false)) (let ((.def_41 false)) (let ((.def_42 false)) (let ((.def_43 false)) (let ((cos 0.0)) (let ((.def_45 0)) (let ((sin 0.0)) (let ((.def_47 0.0)) (let ((.def_48 0.0)) (let ((.def_51 0)) (let ((.def_52 0.0)) (let ((.def_53 0.0)) (let ((.def_54 false)) (let ((.def_56 0.0)) (let ((.def_57 0.0)) (let ((.def_58 false)) (let ((.def_59 false)) (let ((.def_60 false)) (let ((.def_61 false)) (let ((cos 0.0)) (let ((.def_70 1)) (let ((.def_75 (* t@4 (- 1.0)))) (let ((.def_76 (+ t@3 .def_75))) (let ((.def_77 (= .def_76 (- (/ 1 2))))) (let ((.def_78 false)) (let ((.def_79 .def_77)) (let ((.def_80 false)) (let ((.def_81 0.0)) (let ((.def_83 0.0)) (let ((.def_87 0.0)) (let ((.def_94 (* t@3 (- 1.0)))) (let ((.def_95 (+ 1.0 .def_94))) (let ((.def_96 (= .def_95 (- (/ 1 2))))) (let ((.def_97 .def_96)) (let ((.def_98 .def_97)) (let ((.def_99 .def_98)) (let ((.def_103 0.0)) (let ((.def_107 false)) (let ((.def_115 false)) (let ((.def_117 true)) (let ((.def_118 false)) (let ((.def_119 0.0)) (let ((.def_121 0.0)) (let ((.def_129 0.0)) (let ((.def_131 false)) (let ((.def_133 0.0)) (let ((.def_137 true)) (let ((cos 0.0)) (let ((.def_150 false)) (let ((.def_151 false)) (let ((.def_152 false)) (let ((.def_153 (and true true true .def_99 .def_79 (> (- 3.0) y1@5) (= .def_76 (+ t@4 (* t@5 (- 1.0)))) (= 0.0 (+ y1@5 (* 2.0 (sin t@5)) (* (- 2.0) (cos t@5))))))) (let ((.def_154 .def_153)) (let ((.def_155 false)) (let ((.def_156 false)) (let ((.def_157 false)) (let ((.def_158 false)) (let ((.def_159 false)) (let ((.def_160 false)) (let ((.def_161 false)) (let ((.def_162 false)) (let ((.def_163 false)) (let ((.def_164 false)) (let ((.def_165 false)) (let ((.def_166 false)) (let ((.def_167 false)) (let ((.def_168 false)) (let ((.def_169 false)) (let ((.def_170 false)) (let ((.def_171 false)) (let ((.def_172 false)) (let ((.def_173 false)) (let ((.def_174 false)) (let ((.def_175 false)) (let ((.def_176 false)) (let ((.def_177 false)) (let ((.def_178 false)) (let ((.def_179 false)) (let ((.def_180 false)) (let ((.def_181 false)) (let ((.def_182 false)) (let ((.def_183 false)) (let ((.def_184 false)) (let ((.def_185 false)) (let ((.def_186 false)) (let ((.def_187 false)) (let ((.def_188 false)) (let ((.def_189 false)) .def_154)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)