From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2020 22:58:44 +0000 (-0500)
Subject: Fix sort inference for top-level Boolean variables (#4012)
X-Git-Tag: cvc5-1.0.0~3522
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d55bad95755c089adaac69bce106787425b56029;p=cvc5.git

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 07d156c98..9a90e591d 100644
--- 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 a9017ac20..1ca43b2fe 100644
--- 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
index 000000000..5b953e204
--- /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)