Add `ArithProof::{printInteger,getLfscFunction}` (#3716)

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 9ee5f2143f1e1ff8a5b0955e9f271c7407d41935..3ff0ff53942233ce1e44b18974959576162e3415 100644 (file)
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -870,6 +870,56 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
   }
 }
 
+std::string LFSCArithProof::getLfscFunction(const Node & n) {
+  Assert(n.getType().isInteger() || n.getType().isReal() || n.getType().isBoolean());
+  std::string opString;
+  switch (n.getKind()) {
+    case kind::UMINUS:
+      opString = "u-_";
+      break;
+    case kind::PLUS:
+      opString = "+_";
+      break;
+    case kind::MINUS:
+      opString = "-_";
+      break;
+    case kind::MULT:
+      opString = "*_";
+      break;
+    case kind::DIVISION:
+    case kind::DIVISION_TOTAL:
+      opString = "/_";
+      break;
+    case kind::GT:
+      opString = ">_";
+      break;
+    case kind::GEQ:
+      opString = ">=_";
+      break;
+    case kind::LT:
+      opString = "<_";
+      break;
+    case kind::LEQ:
+      opString = "<=_";
+      break;
+    default:
+      Unreachable() << "Tried to get the operator for a non-operator kind: " << n.getKind();
+  }
+  std::string typeString;
+  if (n.getType().isInteger()) {
+    typeString = "Int";
+  } else if (n.getType().isReal()) {
+    typeString = "Real";
+  } else { // Boolean
+    if (n[0].getType().isInteger()) {
+      typeString = "IntReal";
+    } else {
+      typeString = "Real";
+    }
+  }
+  return opString + typeString;
+}
+
 void LFSCArithProof::printRational(std::ostream& o, const Rational& r)
 {
   if (r.sgn() < 0)
@@ -883,6 +933,18 @@ void LFSCArithProof::printRational(std::ostream& o, const Rational& r)
   }
 }
 
+void LFSCArithProof::printInteger(std::ostream& o, const Integer& i)
+{
+  if (i.sgn() < 0)
+  {
+    o << "(~ " << i.abs() << ")";
+  }
+  else
+  {
+    o << i;
+  }
+}
+
 void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o,
                                                      const Node& n)
 {

diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index ac96ad1f337d5e6afb54fef754bc6679e5f70f5f..5522b4eb4c0d321d4c252ddedba144ceb8b905b3 100644 (file)
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -88,6 +88,19 @@ public:
                             TypeNode expectedType) override;
   void printOwnedSort(Type type, std::ostream& os) override;
 
+  /**
+   * Returns the LFSC identifier for the operator of this node.
+   *
+   * e.g. "+_Real".
+   *
+   * Does not include any parens.
+   *
+   * Even if the operator is a comparison (e.g. >=) on integers, will not
+   * return a purely `Int` predicate like ">=_Int". Instead this treats the
+   * right hand side as a real.
+   */
+  static std::string getLfscFunction(const Node& n);
+
   /**
    * Print a rational number in LFSC format.
    *        e.g. 5/8 or (~ 1/1)
@@ -97,6 +110,15 @@ public:
    */
   static void printRational(std::ostream& o, const Rational& r);
 
+  /**
+   * Print an integer in LFSC format.
+   *        e.g. 5 or (~ 1)
+   *
+   * @param o ostream to print to.
+   * @param i the integer to print
+   */
+  static void printInteger(std::ostream& o, const Integer& i);
+
   /**
    * Print a value of type poly_formula_norm
    *