Fixes, improvements

ajreynol · Jan 23, 2025 · 91a46a2 · 91a46a2
1 parent ecd2183
commit 91a46a2
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 5 deletions.
diff --git a/proofs/eo/cpc/theories/Datatypes.eo b/proofs/eo/cpc/theories/Datatypes.eo
@@ -36,10 +36,7 @@
 ; disclaimer: >
 ;   This sort is not in the SMT-LIB standard. All further function
 ;   symbols over this sort are also not part of the SMT-LIB standard.
-(declare-const Nullable (-> Type Type))
-(declare-const nullable.null (-> (! Type :var T) (Nullable T)))
-(declare-const nullable.some (-> (! Type :var T :implicit) T (Nullable T)))
-(declare-const nullable.val (-> (! Type :var T :implicit) (Nullable T) T))
+(declare-datatypes ((Nullable 1)) ((par (T) ((nullable.some (nullable.val T)) (nullable.null)))))
 
 ; program: $get_type_nullable_lift
 ; args:

diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp
@@ -231,9 +231,22 @@ Node AlfNodeConverter::postConvert(Node n)
     Assert(!lam.isNull());
     return convert(lam);
   }
+  else if (k == Kind::APPLY_CONSTRUCTOR)
+  {
+    Node opc = getOperatorOfTerm(n);
+    if (n.getNumChildren() == 0)
+    {
+      return opc;
+    }
+    std::vector<Node> newArgs;
+    newArgs.push_back(opc);
+    newArgs.insert(newArgs.end(), n.begin(), n.end());
+    Node ret = d_nm->mkNode(Kind::APPLY_UF, newArgs);
+    return convert(ret);
+  }
   else if (k == Kind::APPLY_TESTER || k == Kind::APPLY_UPDATER || k == Kind::NEG
            || k == Kind::DIVISION_TOTAL || k == Kind::INTS_DIVISION_TOTAL
-           || k == Kind::INTS_MODULUS_TOTAL || k == Kind::APPLY_CONSTRUCTOR
+           || k == Kind::INTS_MODULUS_TOTAL
            || k == Kind::APPLY_SELECTOR
            || k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
   {