From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 22 Mar 2020 14:23:57 +0000 (-0500)
Subject: Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)
X-Git-Tag: cvc5-1.0.0~3457
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c98ba7775ecb8a192e2a93735885163234546be3;p=cvc5.git

Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)

Fixes #4092 and fixes #4134.

Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.
---

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 9a90e591d..42364f080 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -29,6 +29,7 @@
 #include "theory/quantifiers/quant_util.h"
 
 using namespace CVC4;
+using namespace CVC4::kind;
 using namespace std;
 
 namespace CVC4 {
@@ -434,7 +435,9 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map<
       }
       d_equality_types[n] = child_types[0];
       retType = getIdForType( n.getType() );
-    }else if( n.getKind()==kind::APPLY_UF ){
+    }
+    else if (isHandledApplyUf(n.getKind()))
+    {
       Node op = n.getOperator();
       TypeNode tn_op = op.getType();
       if( d_op_return_types.find( op )==d_op_return_types.end() ){
@@ -663,7 +666,8 @@ Node SortInference::simplifyNode(
                 : i >= 1;
       }
       if( processChild ){
-        if( n.getKind()==kind::APPLY_UF ){
+        if (isHandledApplyUf(n.getKind()))
+        {
           Assert(d_op_arg_types.find(op) != d_op_arg_types.end());
           tnnc = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );
           Assert(!tnnc.isNull());
@@ -704,7 +708,9 @@ Node SortInference::simplifyNode(
         Assert(false);
       }
       ret = NodeManager::currentNM()->mkNode( kind::EQUAL, children );
-    }else if( n.getKind()==kind::APPLY_UF ){
+    }
+    else if (isHandledApplyUf(n.getKind()))
+    {
       if( d_symbol_map.find( op )==d_symbol_map.end() ){
         //make the new operator if necessary
         bool opChanged = false;
@@ -815,7 +821,8 @@ void SortInference::setSkolemVar( Node f, Node v, Node sk ){
 }
 
 bool SortInference::isWellSortedFormula( Node n ) {
-  if( n.getType().isBoolean() && n.getKind()!=kind::APPLY_UF ){
+  if (n.getType().isBoolean() && !isHandledApplyUf(n.getKind()))
+  {
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( !isWellSortedFormula( n[i] ) ){
         return false;
@@ -831,7 +838,8 @@ bool SortInference::isWellSorted( Node n ) {
   if( getSortId( n )==0 ){
     return false;
   }else{
-    if( n.getKind()==kind::APPLY_UF ){
+    if (isHandledApplyUf(n.getKind()))
+    {
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         int s1 = getSortId( n[i] );
         int s2 = d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] );
@@ -847,18 +855,14 @@ bool SortInference::isWellSorted( Node n ) {
   }
 }
 
-void SortInference::getSortConstraints( Node n, UnionFind& uf ) {
-  if( n.getKind()==kind::APPLY_UF ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      getSortConstraints( n[i], uf );
-      uf.setEqual( getSortId( n[i] ), d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ) );
-    }
-  }
-}
-
 bool SortInference::isMonotonic( TypeNode tn ) {
   Assert(tn.isSort());
   return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end();
 }
 
+bool SortInference::isHandledApplyUf(Kind k) const
+{
+  return k == APPLY_UF && !options::ufHo();
+}
+
 }/* CVC4 namespace */
diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index 5b28f669d..ecf86376c 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -154,11 +154,15 @@ public:
   //is well sorted
   bool isWellSortedFormula( Node n );
   bool isWellSorted( Node n );
-  //get constraints for being well-typed according to computed sub-types
-  void getSortConstraints( Node n, SortInference::UnionFind& uf );
 private:
   // store monotonicity for original sorts as well
  std::map<TypeNode, bool> d_non_monotonic_sorts_orig;
+ /**
+  * Returns true if k is the APPLY_UF kind and we are not using higher-order
+  * techniques. This is called in places where we want to know whether to
+  * treat a term as uninterpreted function.
+  */
+ bool isHandledApplyUf(Kind k) const;
 };
 
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a8ec4a665..cd83ef3d1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1302,6 +1302,8 @@ set(regress_1_tests
   regress1/ho/fta0328.lfho.p
   regress1/ho/issue3136-fconst-bool-bool.smt2
   regress1/ho/issue4065-no-rep.smt2
+  regress1/ho/issue4092-sinf.smt2
+  regress1/ho/issue4134-sinf.smt2
   regress1/ho/nested_lambdas-AGT034^2.smt2
   regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
   regress1/ho/NUM638^1.smt2
diff --git a/test/regress/regress1/ho/issue4092-sinf.smt2 b/test/regress/regress1/ho/issue4092-sinf.smt2
new file mode 100644
index 000000000..96f52fd39
--- /dev/null
+++ b/test/regress/regress1/ho/issue4092-sinf.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --uf-ho --sort-inference --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(set-option :sort-inference true)
+(set-option :uf-ho true)
+(set-info :status sat)
+(declare-fun a ( Int ) Int) 
+(declare-fun b ( Int ) Int)  
+(assert (and (distinct 0 (b 5)) (distinct a b ))) 
+(check-sat) 
diff --git a/test/regress/regress1/ho/issue4134-sinf.smt2 b/test/regress/regress1/ho/issue4134-sinf.smt2
new file mode 100644
index 000000000..e87845fab
--- /dev/null
+++ b/test/regress/regress1/ho/issue4134-sinf.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --uf-ho --sort-inference --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(set-option :uf-ho true)
+(set-option :sort-inference true)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b (Int) Int)
+(declare-fun c (Int) Int)
+(declare-fun d (Int) Int)
+(assert (distinct d (ite (= a 0) b c)))
+(assert (= (d 0) 0))
+(check-sat)