Allow Int/Real subtyping in LFSC proofs

3 files changed, 25 insertions, 4 deletions

diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index ad3e81ac2..b0e2c7be3 100755
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -40,7 +40,7 @@ SIG_DIR="$BASE_DIR/lfsc-signatures"
 mkdir -p $SIG_DIR
 
 # download and unpack signatures
-sig_version="768cfda32847e7ba6b846d5e4e6e92e89b66aee1"
+sig_version="43b9b5939aac2939c9bd7d6240cb01172351a0e4"
 download "https://github.com/CVC4/signatures/archive/$sig_version.tar.gz" $BASE_DIR/tmp/signatures.tgz
 tar --strip 1 -xzf $BASE_DIR/tmp/signatures.tgz -C $SIG_DIR
 
diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index c536e8dea..e2af15fa2 100644
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -542,7 +542,8 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn,
     case PfRule::ARITH_MULT_POS:
     case PfRule::ARITH_MULT_NEG:
     {
-      pf << h << as[0] << as[1] << as[0].getType();
+      // do not pass type (as[0].getType())
+      pf << h << as[0] << as[1];
     }
       break;
     // strings
@@ -589,7 +590,8 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn,
         case LfscRule::NOT_AND_REV: pf << h << h << cs[0]; break;
         case LfscRule::PROCESS_SCOPE: pf << h << h << as[2] << cs[0]; break;
         case LfscRule::AND_INTRO2: pf << h << h << cs[0] << cs[1]; break;
-        case LfscRule::ARITH_SUM_UB: pf << h << h << h << cs[0]->getResult()[0].getType() << cs[0] << cs[1]; break;
+        // do not pass type (cs[0]->getResult()[0].getType())
+        case LfscRule::ARITH_SUM_UB: pf << h << h << h << cs[0] << cs[1]; break;
         default: return false; break;
       }
       break;
diff --git a/src/proof/lfsc/lfsc_term_process.cpp b/src/proof/lfsc/lfsc_term_process.cpp
index 0a27e1672..77c86413f 100644
--- a/src/proof/lfsc/lfsc_term_process.cpp
+++ b/src/proof/lfsc/lfsc_term_process.cpp
@@ -90,6 +90,7 @@ Node LfscTermProcessor::runConvert(Node n)
     // symbols
     if (tn.isConstructor() || tn.isSelector() || tn.isTester())
     {
+      // TODO: should be given user names
       return n;
     }
     // skolems v print as their witness forms
@@ -368,6 +369,9 @@ Node LfscTermProcessor::runConvert(Node n)
     if (k == PLUS || k == MULT || k == NONLINEAR_MULT)
     {
       std::stringstream opName;
+      // currently allow subtyping
+      opName << "a.";
+      /*
       if (n.getType().isInteger())
       {
         opName << "int.";
@@ -376,6 +380,7 @@ Node LfscTermProcessor::runConvert(Node n)
       {
         opName << "real.";
       }
+      */
       opName << printer::smt2::Smt2Printer::smtKindString(k);
       TypeNode ftype = nm->mkFunctionType({tn, tn}, tn);
       opc = getSymbolInternal(k, ftype, opName.str());
@@ -475,7 +480,17 @@ TypeNode LfscTermProcessor::runConvertType(TypeNode tn)
     {
       std::stringstream ss;
       tn.toStream(ss, language::output::LANG_SMTLIB_V2_6);
-      tnn = getSymbolInternal(k, d_sortType, ss.str());
+      if (false && (tn.isSort() || tn.isDatatype()))
+      {
+        std::stringstream sss;
+        sss << LfscTermProcessor::getNameForUserName(ss.str());
+        tnn = getSymbolInternal(k, d_sortType, sss.str());
+        cur = nm->mkSort(sss.str());
+      }
+      else
+      {
+        tnn = getSymbolInternal(k, d_sortType, ss.str());
+      }
     }
   }
   else
@@ -778,6 +793,9 @@ Node LfscTermProcessor::getOperatorOfTerm(Node n, bool macroApply)
       || k == DIVISION_TOTAL || k == INTS_DIVISION || k == INTS_DIVISION_TOTAL
       || k == INTS_MODULUS || k == INTS_MODULUS_TOTAL || k == UMINUS)
   {
+    // currently allow subtyping
+    opName << "a.";
+    /*
     if (n[0].getType().isInteger())
     {
       opName << "int.";
@@ -786,6 +804,7 @@ Node LfscTermProcessor::getOperatorOfTerm(Node n, bool macroApply)
     {
       opName << "real.";
     }
+    */
   }
   if (k == UMINUS)
   {