Do not automatically parse rational constants from NEG and DIVISION (c…

…vc5#10472)

This eliminates an optimization in our parser where terms that specific rational or numeral values are automatically.

This increases our proof size by 0.1% (985k steps vs. 984k steps) and our number of trusted rewrite steps by 0.08% (135742 vs 135632).

This includes cvc5#10471, review that PR first.

Some benchmarks that used array constants required changing. In particular ((as const (Array Real Real)) (/ 1 4)) is no longer a valid term, since (/ 1 4) is the division of 1 and 4 and not a rational value. Due to our partial, experimental support of array constants that only accept values, the required syntax for this is now ((as const (Array Real Real)) 1/4).

FYI @barrettcw

This PR also introduces --print-arith-lit-token (disabled by default) which prints rational values and negative arithmetic values using the new syntax.

Based on these changes, it simplifies and improves the ALF printer.

proofs/alf/cvc5/Cvc5.smt3

@@ -21,25 +21,6 @@
 (declare-sort @ho-elim-sort 1)
 (declare-const @fmf-fun-sort (-> (! Type :var T :implicit) T Type))
 
-; side condition for normalizing inputs for the purposes of the reference command
-(program parse_normalize ((T Type) (U Type) (S Type) (x T) (y U) (f (-> T S)) (z S))
-  (S) S
-  (
-    ((parse_normalize (/ x y))  (let ((xn (parse_normalize x)) (yn (parse_normalize y)))
-                                (let ((xz (alf.to_z xn)) (yz (alf.to_z yn)))
-                                (alf.ite (alf.and (alf.is_eq xz xn) (alf.is_eq yz yn) (alf.not (alf.is_eq yz 0)))
-                                  (alf.qdiv xn yn)
-                                  (/ xn yn)))))
-    ((parse_normalize (- x))    (let ((xn (parse_normalize x)))
-                                (let ((xz (alf.to_z xn)) (xq (alf.to_q xn)))
-                                (alf.ite (alf.is_eq xn xz) (alf.neg xn)
-                                (alf.ite (alf.is_eq xn xq) (alf.neg xn)
-                                  (- xn))))))
-    ((parse_normalize (f x))    (_ (parse_normalize f) (parse_normalize x)))
-    ((parse_normalize z)        z)
-  )
-)
-
 ; Converts x to an equivalent form, for ProofRule::ENCODE_TRANSFORM.
 ; This side condition is used to convert between the native
 ; representation in cvc5 to the form expected by DSL rewrite rules.

src/options/printer_options.toml

@@ -63,3 +63,11 @@ name   = "Printing"
   type       = "bool"
   default    = "false"
   help       = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x"
+
+[[option]]
+  name       = "printArithLitToken"
+  category   = "expert"
+  long       = "print-arith-lit-token"
+  type       = "bool"
+  default    = "false"
+  help       = "print rationals and negative arithmetic literals as lexed tokens, e.g. 1/4, -1.5"

src/parser/smt2/smt2_state.cpp

@@ -1536,31 +1536,10 @@ Term Smt2State::applyParseOp(const ParseOp& p, std::vector<Term>& args)
     }
     else if (kind == Kind::SUB && args.size() == 1)
     {
-      if (isConstInt(args[0]) && args[0].getRealOrIntegerValueSign() > 0)
-      {
-        // (- n) denotes a negative value
-        std::stringstream suminus;
-        suminus << "-" << args[0].getIntegerValue();
-        Term ret = d_tm.mkInteger(suminus.str());
-        Trace("parser") << "applyParseOp: return negative constant " << ret
-                        << std::endl;
-        return ret;
-      }
       Term ret = d_tm.mkTerm(Kind::NEG, {args[0]});
       Trace("parser") << "applyParseOp: return uminus " << ret << std::endl;
       return ret;
     }
-    else if (kind == Kind::DIVISION && args.size() == 2 && isConstInt(args[0])
-             && isConstInt(args[1]) && args[1].getRealOrIntegerValueSign() > 0)
-    {
-      // (/ m n) or (/ (- m) n) denote values in reals
-      std::stringstream sdiv;
-      sdiv << args[0].getIntegerValue() << "/" << args[1].getIntegerValue();
-      Term ret = d_tm.mkReal(sdiv.str());
-      Trace("parser") << "applyParseOp: return rational constant " << ret
-                      << std::endl;
-      return ret;
-    }
     else if (kind == Kind::FLOATINGPOINT_FP)
     {
       // (fp #bX #bY #bZ) denotes a floating-point value

src/printer/smt2/smt2_printer.cpp

@@ -73,44 +73,76 @@ static void toStreamRational(std::ostream& out,
                              Variant v)
 {
   bool neg = r.sgn() < 0;
+  bool arithTokens = options::ioutils::getPrintArithLitToken(out);
   // Print the rational, possibly as a real.
   // Notice that we print (/ (- 5) 3) instead of (- (/ 5 3)),
   // the former is compliant with real values in the smt lib standard.
   if (r.isIntegral())
   {
-    if (neg)
+    if (arithTokens)
     {
-      out << "(- " << -r;
+      if (neg)
+      {
+        out << "-" << -r;
+      }
+      else
+      {
+        out << r;
+      }
+      if (isReal)
+      {
+        out << ".0";
+      }
     }
     else
     {
-      out << r;
-    }
-    if (isReal)
-    {
-      out << ".0";
-    }
-    if (neg)
-    {
-      out << ")";
+      if (neg)
+      {
+        out << "(- " << -r;
+      }
+      else
+      {
+        out << r;
+      }
+      if (isReal)
+      {
+        out << ".0";
+      }
+      if (neg)
+      {
+        out << ")";
+      }
     }
   }
   else
   {
     Assert(isReal);
-    out << "(/ ";
-    if (neg)
+    if (arithTokens)
     {
-      Rational abs_r = (-r);
-      out << "(- " << abs_r.getNumerator();
-      out << ") " << abs_r.getDenominator();
+      if (neg)
+      {
+        Rational abs_r = (-r);
+        out << '-' << abs_r.getNumerator() << '/' << abs_r.getDenominator();
+      }
+      else
+      {
+        out << r.getNumerator() << '/' << r.getDenominator();
+      }
     }
     else
     {
-      out << r.getNumerator();
-      out << ' ' << r.getDenominator();
+      out << "(/ ";
+      if (neg)
+      {
+        Rational abs_r = (-r);
+        out << "(- " << abs_r.getNumerator() << ") " << abs_r.getDenominator();
+      }
+      else
+      {
+        out << r.getNumerator() << ' ' << r.getDenominator();
+      }
+      out << ')';
     }
-    out << ')';
   }
 }
 

src/proof/alf/alf_node_converter.cpp

@@ -137,29 +137,6 @@ Node AlfNodeConverter::postConvert(Node n)
   {
     return mkInternalApp("_", {n[0], n[1]}, tn);
   }
-  else if (k == Kind::CONST_INTEGER)
-  {
-    Rational r = n.getConst<Rational>();
-    if (r.sgn() == -1)
-    {
-      // negative integers are printed as "-n"
-      std::stringstream ss;
-      ss << "-" << r.abs();
-      return mkInternalSymbol(ss.str(), tn);
-    }
-    return n;
-  }
-  else if (k == Kind::CONST_RATIONAL)
-  {
-    Rational r = n.getConst<Rational>();
-    // ensure rationals are printed properly here using alf syntax,
-    // which is "n/d" or "-n/d".
-    Integer num = r.getNumerator().abs();
-    Integer den = r.getDenominator();
-    std::stringstream ss;
-    ss << (r.sgn() == -1 ? "-" : "") << num << "/" << den;
-    return mkInternalSymbol(ss.str(), tn);
-  }
   else if (n.isClosure())
   {
     // e.g. (forall ((x1 T1) ... (xn Tk)) P) is

src/proof/alf/alf_print_channel.cpp

@@ -72,7 +72,8 @@ void AlfPrintChannelOut::printStepInternal(const std::string& rname,
   d_out << "(" << (isPop ? "step-pop" : "step") << " @p" << i;
   if (!n.isNull())
   {
-    printNode(n);
+    d_out << " ";
+    printNodeInternal(d_out, n);
   }
   d_out << " :rule " << rname;
   bool firstTime = true;
@@ -144,7 +145,6 @@ void AlfPrintChannelOut::printTrustStep(ProofRule r,
 
 void AlfPrintChannelOut::printNodeInternal(std::ostream& out, Node n)
 {
-  options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
   if (d_lbind)
   {
     // use the toStream with custom letification method
@@ -153,13 +153,12 @@ void AlfPrintChannelOut::printNodeInternal(std::ostream& out, Node n)
   else
   {
     // just use default print
-    out << n;
+    Printer::getPrinter(out)->toStream(out, n);
   }
 }
 
 void AlfPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn)
 {
-  options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
   tn.toStream(out);
 }
 

src/proof/alf/alf_printer.cpp

@@ -260,6 +260,9 @@ void AlfPrinter::printLetList(std::ostream& out, LetBinding& lbind)
 
 void AlfPrinter::print(std::ostream& out, std::shared_ptr<ProofNode> pfn)
 {
+  // ensures options are set once and for all
+  options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
+  options::ioutils::applyPrintArithLitToken(out, true);
   d_pfIdCounter = 0;
 
   // Get the definitions and assertions and print the declarations from them
@@ -305,10 +308,10 @@ void AlfPrinter::print(std::ostream& out, std::shared_ptr<ProofNode> pfn)
       }
       if (options().proof.alfPrintReference)
       {
-        // parse_normalize is used as the normalization function for the input
         // [1] print the reference
-        out << "(reference \"" << options().driver.filename
-            << "\" parse_normalize)" << std::endl;
+        // we currently do not need to provide a normalization routine.
+        out << "(reference \"" << options().driver.filename << "\")"
+            << std::endl;
         // [2] print the universal variables
         out << outVars.str();
       }

test/regress/cli/regress0/array-const-real-parse.smt2

@@ -1,7 +1,8 @@
+; COMMAND-LINE: --print-arith-lit-token
 (set-logic QF_AUFLIRA)
 (set-info :status sat)
 (declare-fun a () (Array Int Real))
 (assert (= a ((as const (Array Int Real)) 0.0)))
 (declare-fun b () (Array Int Real))
-(assert (= b ((as const (Array Int Real)) (/ 1 3))))
+(assert (= b ((as const (Array Int Real)) 1/3)))
 (check-sat)

test/regress/cli/regress0/arrays/issue7596-define-array-uminus.smt2

@@ -1,5 +1,6 @@
+; COMMAND-LINE: --print-arith-lit-token
 (set-logic ALL)
 (set-info :status sat)
-(define-fun foo () (Array Int Int) ((as const (Array Int Int)) (- 1)))
+(define-fun foo () (Array Int Int) ((as const (Array Int Int)) -1))
 (assert (= (select foo 0) (- 1)))
 (check-sat)