[proofs] [alethe] Improve error flagging to catch unsupported types

This allows cvc5 to realize it is an unsupported fragment in Alethe also when the problem contains only variables of unsupported theories.
HanielB · Sep 27, 2024 · e8c7f68 · e8c7f68
1 parent eae5e26
commit e8c7f68
Show file tree

Hide file tree

Showing 5 changed files with 72 additions and 10 deletions.
diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp
@@ -15,6 +15,7 @@
 
 #include "proof/alethe/alethe_node_converter.h"
 
+#include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "proof/proof_rule_checker.h"
@@ -229,8 +230,6 @@ Node AletheNodeConverter::postConvert(Node n)
     case Kind::BUILTIN:
     case Kind::EQUAL:
     case Kind::DISTINCT:
-    case Kind::VARIABLE:
-    case Kind::BOUND_VARIABLE:
     case Kind::SEXPR:
     case Kind::TYPE_CONSTANT:
     case Kind::RAW_SYMBOL:
@@ -404,6 +403,77 @@ Node AletheNodeConverter::postConvert(Node n)
     {
       return n;
     }
+    case Kind::BOUND_VARIABLE:
+    case Kind::VARIABLE:
+    {
+      // see if variable has a supported type. We need this check because in
+      // some problems involving unsupported theories there are no operators,
+      // just variables of unsupported type
+      TypeNode tn = n.getType();
+      Kind tnk = tn.getKind();
+      switch (tnk)
+      {
+        case Kind::SORT_TYPE:
+        case Kind::INSTANTIATED_SORT_TYPE:
+        case Kind::FUNCTION_TYPE:
+        case Kind::BITVECTOR_TYPE:
+        case Kind::ARRAY_TYPE:
+        case Kind::CONSTRUCTOR_TYPE:
+        case Kind::SELECTOR_TYPE:
+        case Kind::TESTER_TYPE:
+        case Kind::ASCRIPTION_TYPE:
+        {
+          return n;
+        }
+        default:
+        {
+          // The supported constant types
+          if (tnk == Kind::TYPE_CONSTANT)
+          {
+            switch (tn.getConst<TypeConstant>())
+            {
+              case TypeConstant::BUILTIN_OPERATOR_TYPE:
+              case TypeConstant::SEXPR_TYPE:
+              case TypeConstant::BOOLEAN_TYPE:
+              case TypeConstant::REAL_TYPE:
+              case TypeConstant::INTEGER_TYPE:
+              case TypeConstant::STRING_TYPE:
+              case TypeConstant::REGEXP_TYPE:
+              {
+                return n;
+              }
+              default:  // fallthrough to the error handling below
+                break;
+            }
+          }
+          // Only regular datatypes (parametric or not) are supported
+          else if (tn.isDatatype() && !tn.getDType().isCodatatype()
+                   && (tnk == Kind::DATATYPE_TYPE
+                       || tnk == Kind::PARAMETRIC_DATATYPE))
+          {
+            return n;
+          }
+          Trace("alethe-conv") << "AletheNodeConverter: ...unsupported type\n";
+          std::stringstream ss;
+          ss << "\"Proof unsupported by Alethe: contains ";
+          if (tnk == Kind::TYPE_CONSTANT)
+          {
+            ss << tn.getConst<TypeConstant>();
+          }
+          else if (tn.isDatatype())
+          {
+            ss << "non-standard datatype";
+          }
+          else
+          {
+            ss << tnk;
+          }
+          ss << "\"";
+          d_error = ss.str();
+          return Node::null();
+        }
+      }
+    }
     default:
     {
       Trace("alethe-conv") << "AletheNodeConverter: ...unsupported kind\n";

diff --git a/test/regress/cli/regress0/bv/issue9518.smt2 b/test/regress/cli/regress0/bv/issue9518.smt2
@@ -1,5 +1,3 @@
-;; FP is not supported in Alethe
-; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :bv-solver bitblast-internal)

diff --git a/test/regress/cli/regress0/datatypes/stream-singleton.smt2 b/test/regress/cli/regress0/datatypes/stream-singleton.smt2
@@ -1,5 +1,3 @@
-;; Codatatypes are not supported in Alethe
-; DISABLE-TESTER: alethe
 (set-logic QF_ALL)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 b/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2
@@ -1,7 +1,5 @@
 ; COMMAND-LINE: --full-saturate-quant
 ; EXPECT: unsat
-;; Logic not supported in Alethe
-; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-fun b () String)
 (assert (forall ((c (Seq Int))) (exists ((a String)) (and (= 1 (seq.len c)) (not (= b a))))))

diff --git a/test/regress/cli/regress1/sets/insert_invariant_37_2.smt2 b/test/regress/cli/regress1/sets/insert_invariant_37_2.smt2
@@ -1,5 +1,3 @@
-;; Logic not supported in Alethe
-; DISABLE-TESTER: alethe
 (set-option :print-success false)
 (set-logic AUFLIAFS)
 (set-info :status unsat)