[proofs] [alethe] Improve error flagging to catch unsupported types (c…

…vc5#11235) This allows cvc5 to realize it is in an unsupported fragment of Alethe also when the problem contains only variables of unsupported theories, which requires us to look at their type. As a consequence, we can re-enable a few regressions. This fixes the nightlies, where a build with Cocoa (which is not tested together with Alethe in CI) was generating proofs without FF operators but with FF variables.
ajreynol · Oct 14, 2024 · 7ec5106 · 7ec5106
1 parent 9ddaa54
commit 7ec5106
Show file tree

Hide file tree

Showing 5 changed files with 71 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,76 @@ 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::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)