Fix sort inference for top-level Boolean variables (#4012)

Fixes #4010.

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 07d156c98aaf64bbbcde2a061dc96119d9845080..9a90e591df94984f619fe1e4bd2fffb0d467c408 100644 (file)
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -119,11 +119,15 @@ void SortInference::initialize(const std::vector<Node>& assertions)
   Trace("sort-inference-proc") << "Calculating sort inference..." << std::endl;
   // process all assertions
   std::map<Node, int> visited;
+  NodeManager * nm = NodeManager::currentNM();
+  int btId = getIdForType( nm->booleanType() );
   for (const Node& a : assertions)
   {
     Trace("sort-inference-debug") << "Process " << a << std::endl;
     std::map<Node, Node> var_bound;
-    process(a, var_bound, visited);
+    int pid = process(a, var_bound, visited);
+    // the type of the topmost term must be Boolean
+    setEqual( pid, btId );
   }
   Trace("sort-inference-proc") << "...done" << std::endl;
   for (const std::pair<const Node, int>& rt : d_op_return_types)
@@ -471,7 +475,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map<
         Trace("sort-inference-debug") << n << " is a bound variable." << std::endl;
         //the return type was specified while binding
         retType = d_var_types[it->second][n];
-      }else if( n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM ){
+      }else if( n.isVar() ){
         Trace("sort-inference-debug") << n << " is a variable." << std::endl;
         if( d_op_return_types.find( n )==d_op_return_types.end() ){
           //assign arbitrary sort
@@ -694,7 +698,7 @@ Node SortInference::simplifyNode(
     }else if( n.getKind()==kind::EQUAL ){
       TypeNode tn1 = children[0].getType();
       TypeNode tn2 = children[1].getType();
-      if( !tn1.isSubtypeOf( tn2 ) && !tn2.isSubtypeOf( tn1 ) ){
+      if( !tn1.isComparableTo( tn2 ) ){
         Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl;
         Trace("sort-inference-warn") << "  Types : " << children[0].getType() << " " << children[1].getType() << std::endl;
         Assert(false);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a9017ac2005950f5accb592ca028b5cfc2b249f7..1ca43b2fe3533b1bffd2d3dbfcc24e40feef60e3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -546,6 +546,7 @@ set(regress_0_tests
   regress0/issue1063-overloading-dt-fun.smt2
   regress0/issue1063-overloading-dt-sel.smt2
   regress0/issue2832-qualId.smt2
+  regress0/issue4010-sort-inf-var.smt2
   regress0/ite.cvc
   regress0/ite2.smt2
   regress0/ite3.smt2

diff --git a/test/regress/regress0/issue4010-sort-inf-var.smt2 b/test/regress/regress0/issue4010-sort-inf-var.smt2
new file mode 100644 (file)
index 0000000..5b953e2
--- /dev/null
+++ b/test/regress/regress0/issue4010-sort-inf-var.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --sort-inference --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () Bool)
+(assert a)
+(check-sat)