Properly implement function extensionality based on cardinality (#1765)

5 files changed, 196 insertions, 51 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 9e61e713b..e7775cf7f 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -82,6 +82,22 @@ bool TypeNode::isInterpretedFinite() const {
       }else if( isSet() ) {
         return getSetElementType().isInterpretedFinite();
       }
+      else if (isFunction())
+      {
+        if (!getRangeType().isInterpretedFinite())
+        {
+          return false;
+        }
+        std::vector<TypeNode> argTypes = getArgTypes();
+        for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+        {
+          if (!argTypes[i].isInterpretedFinite())
+          {
+            return false;
+          }
+        }
+        return true;
+      }
     }
     return false;
   }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index b3fb8e211..f5748549e 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -39,9 +39,12 @@ namespace theory {
 namespace uf {
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
-                   OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, std::string instanceName)
+TheoryUF::TheoryUF(context::Context* c,
+                   context::UserContext* u,
+                   OutputChannel& out,
+                   Valuation valuation,
+                   const LogicInfo& logicInfo,
+                   std::string instanceName)
     : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName),
       d_notify(*this),
       /* The strong theory solver can be notified by EqualityEngine::init(),
@@ -49,7 +52,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
       d_thss(NULL),
       d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true),
       d_conflict(c, false),
-      d_extensionality_deq(u),
+      d_extensionality(u),
       d_uf_std_skolem(u),
       d_functionsTerms(c),
       d_symb(u, instanceName)
@@ -345,21 +348,38 @@ bool TheoryUF::collectModelInfo(TheoryModel* m)
   if( options::ufHo() ){
     for( std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it ){
       Node n = *it;
-      if( n.getKind()==kind::APPLY_UF ){
-        // for model-building with ufHo, we require that APPLY_UF is always expanded to HO_APPLY
-        Node hn = TheoryUfRewriter::getHoApplyForApplyUf( n );
-        if (!m->assertEquality(n, hn, true))
-        {
-          return false;
-        }
+      // for model-building with ufHo, we require that APPLY_UF is always
+      // expanded to HO_APPLY
+      if (!collectModelInfoHoTerm(n, m))
+      {
+        return false;
       }
     }
+    // must add extensionality disequalities for all pairs of (non-disequal)
+    // function equivalence classes.
+    if (checkExtensionality(m) != 0)
+    {
+      return false;
+    }
   }
 
   Debug("uf") << "UF : finish collectModelInfo " << std::endl;
   return true;
 }
 
+bool TheoryUF::collectModelInfoHoTerm(Node n, TheoryModel* m)
+{
+  if (n.getKind() == kind::APPLY_UF)
+  {
+    Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n);
+    if (!m->assertEquality(n, hn, true))
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
 void TheoryUF::presolve() {
   // TimerStat::CodeTimer codeTimer(d_presolveTimer);
 
@@ -670,20 +690,26 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
   }
 }
 
-unsigned TheoryUF::applyExtensionality(TNode deq) {
+Node TheoryUF::getExtensionalityDeq(TNode deq)
+{
   Assert( deq.getKind()==kind::NOT && deq[0].getKind()==kind::EQUAL );
   Assert( deq[0][0].getType().isFunction() );
-  // apply extensionality
-  if( d_extensionality_deq.find( deq )==d_extensionality_deq.end() ){
-    d_extensionality_deq.insert( deq );
+  std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
+  if (it == d_extensionality_deq.end())
+  {
     TypeNode tn = deq[0][0].getType();
+    std::vector<TypeNode> argTypes = tn.getArgTypes();
     std::vector< Node > skolems;
-    for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
-      Node k = NodeManager::currentNM()->mkSkolem( "k", tn[i], "skolem created for extensionality." );
+    NodeManager* nm = NodeManager::currentNM();
+    for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+    {
+      Node k =
+          nm->mkSkolem("k", argTypes[i], "skolem created for extensionality.");
       skolems.push_back( k );
     }
     Node t[2];
-    for( unsigned i=0; i<2; i++ ){
+    for (unsigned i = 0; i < 2; i++)
+    {
       std::vector< Node > children;
       Node curr = deq[0][i];
       while( curr.getKind()==kind::HO_APPLY ){
@@ -693,32 +719,52 @@ unsigned TheoryUF::applyExtensionality(TNode deq) {
       children.push_back( curr );
       std::reverse( children.begin(), children.end() );
       children.insert( children.end(), skolems.begin(), skolems.end() );
-      t[i] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
+      t[i] = nm->mkNode(kind::APPLY_UF, children);
     }
     Node conc = t[0].eqNode( t[1] ).negate();
+    d_extensionality_deq[deq] = conc;
+    return conc;
+  }
+  return it->second;
+}
+
+unsigned TheoryUF::applyExtensionality(TNode deq)
+{
+  Assert(deq.getKind() == kind::NOT && deq[0].getKind() == kind::EQUAL);
+  Assert(deq[0][0].getType().isFunction());
+  // apply extensionality
+  if (d_extensionality.find(deq) == d_extensionality.end())
+  {
+    d_extensionality.insert(deq);
+    Node conc = getExtensionalityDeq(deq);
     Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq[0], conc );
     Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem << std::endl;
     d_out->lemma( lem );
     return 1;
-  }else{
-    return 0;
   }
+  return 0;
 }
 
-unsigned TheoryUF::checkExtensionality() {
+unsigned TheoryUF::checkExtensionality(TheoryModel* m)
+{
   unsigned num_lemmas = 0;
-  Trace("uf-ho") << "TheoryUF::checkExtensionality..." << std::endl;
-  // This is bit eager: we should allow functions to be neither equal nor disequal during model construction
-  // However, doing so would require a function-type enumerator.
+  bool isCollectModel = (m != nullptr);
+  Trace("uf-ho") << "TheoryUF::checkExtensionality, collectModel="
+                 << isCollectModel << "..." << std::endl;
   std::map< TypeNode, std::vector< Node > > func_eqcs;
-
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
     TypeNode tn = eqc.getType();
     if( tn.isFunction() ){
-      func_eqcs[tn].push_back( eqc );
-      Trace("uf-ho-debug") << "  func eqc : " << tn << " : " << eqc << std::endl;
+      // if during collect model, must have an infinite type
+      // if not during collect model, must have a finite type
+      if (tn.isInterpretedFinite() != isCollectModel)
+      {
+        func_eqcs[tn].push_back(eqc);
+        Trace("uf-ho-debug")
+            << "  func eqc : " << tn << " : " << eqc << std::endl;
+      }
     }
     ++eqcs_i;
   }
@@ -728,9 +774,38 @@ unsigned TheoryUF::checkExtensionality() {
     for( unsigned j=0; j<itf->second.size(); j++ ){
       for( unsigned k=(j+1); k<itf->second.size(); k++ ){ 
         // if these equivalence classes are not explicitly disequal, do extensionality to ensure distinctness
-        if( !d_equalityEngine.areDisequal( itf->second[j], itf->second[k], false ) ){
+        if (!d_equalityEngine.areDisequal(
+                itf->second[j], itf->second[k], false))
+        {
           Node deq = Rewriter::rewrite( itf->second[j].eqNode( itf->second[k] ).negate() );
-          num_lemmas += applyExtensionality( deq );
+          // either add to model, or add lemma
+          if (isCollectModel)
+          {
+            // add extentionality disequality to the model
+            Node edeq = getExtensionalityDeq(deq);
+            Assert(edeq.getKind() == kind::NOT
+                   && edeq[0].getKind() == kind::EQUAL);
+            // introducing terms, must add required constraints, e.g. to
+            // force equalities between APPLY_UF and HO_APPLY terms
+            for (unsigned r = 0; r < 2; r++)
+            {
+              if (!collectModelInfoHoTerm(edeq[0][r], m))
+              {
+                return 1;
+              }
+            }
+            Trace("uf-ho-debug")
+                << "Add extensionality deq to model : " << edeq << std::endl;
+            if (!m->assertEquality(edeq[0][0], edeq[0][1], false))
+            {
+              return 1;
+            }
+          }
+          else
+          {
+            // apply extensionality lemma
+            num_lemmas += applyExtensionality(deq);
+          }
         }
       }   
     }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index bac03c34c..790968360 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -139,7 +139,10 @@ private:
   Node d_conflictNode;
 
   /** extensionality has been applied to these disequalities */
-  NodeSet d_extensionality_deq;
+  NodeSet d_extensionality;
+
+  /** cache of getExtensionalityDeq below */
+  std::map<Node, Node> d_extensionality_deq;
 
   /** map from non-standard operators to their skolems */
   NodeNodeMap d_uf_std_skolem;
@@ -185,31 +188,55 @@ private:
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 
-private: // for higher-order
-  /** applyExtensionality 
-   * Given disequality deq 
-   * If not already cached, this sends a lemma of the form 
+ private:  // for higher-order
+  /** get extensionality disequality
+   *
+   * Given disequality deq f != g, this returns the disequality:
+   *   (f k) != (g k) for fresh constant(s) k.
+   */
+  Node getExtensionalityDeq(TNode deq);
+
+  /** applyExtensionality
+   *
+   * Given disequality deq f != g, if not already cached, this sends a lemma of
+   * the form:
    *   f = g V (f k) != (g k) for fresh constant k.
-   * on the output channel.
-   * Return value is the number of lemmas sent.
+   * on the output channel. This is an "extensionality lemma".
+   * Return value is the number of lemmas of this form sent on the output
+   * channel.
    */
   unsigned applyExtensionality(TNode deq);
 
-  /** check whether extensionality should be applied for any
-   * pair of terms in the equality engine.
+  /**
+   * Check whether extensionality should be applied for any pair of terms in the
+   * equality engine.
+   *
+   * If we pass a null model m to this function, then we add extensionality
+   * lemmas to the output channel and return the total number of lemmas added.
+   * We only add lemmas for functions whose type is finite, since pairs of
+   * functions whose types are infinite can be made disequal in a model by
+   * witnessing a point they are disequal.
+   *
+   * If we pass a non-null model m to this function, then we add disequalities
+   * that correspond to the conclusion of extensionality lemmas to the model's
+   * equality engine. We return 0 if the equality engine of m is consistent
+   * after this call, and 1 otherwise. We only add disequalities for functions
+   * whose type is infinite, since our decision procedure guarantees that
+   * extensionality lemmas are added for all pairs of functions whose types are
+   * finite.
    */
-  unsigned checkExtensionality();
-  
+  unsigned checkExtensionality(TheoryModel* m = nullptr);
+
   /** applyAppCompletion
-   * This infers a correspondence between APPLY_UF and HO_APPLY 
+   * This infers a correspondence between APPLY_UF and HO_APPLY
    * versions of terms for higher-order.
-   * Given APPLY_UF node e.g. (f a b c), this adds the equality to its 
+   * Given APPLY_UF node e.g. (f a b c), this adds the equality to its
    * HO_APPLY equivalent:
    *   (f a b c) == (@ (@ (@ f a) b) c)
    * to equality engine, if not already equal.
    * Return value is the number of equalities added.
    */
-  unsigned applyAppCompletion( TNode n );
+  unsigned applyAppCompletion(TNode n);
 
   /** check whether app-completion should be applied for any
    * pair of terms in the equality engine.
@@ -224,19 +251,31 @@ private: // for higher-order
   */
   unsigned checkHigherOrder();
 
-  /** get apply uf for ho apply 
+  /** collect model info for higher-order term
+   *
+   * This adds required constraints to m for term n. In particular, if n is
+   * an APPLY_UF term, we add its HO_APPLY equivalent in this call. We return
+   * true if the model m is consistent after this call.
+   */
+  bool collectModelInfoHoTerm(Node n, TheoryModel* m);
+
+  /** get apply uf for ho apply
    * This returns the APPLY_UF equivalent for the HO_APPLY term node, where
    * node has non-functional return type (that is, it corresponds to a fully
    * applied function term).
    * This call may introduce a skolem for the head operator and send out a lemma
    * specifying the definition.
   */
-  Node getApplyUfForHoApply( Node node );
-  /** get the operator for this node (node should be either APPLY_UF or HO_APPLY) */
-  Node getOperatorForApplyTerm( TNode node );
-  /** get the starting index of the arguments for node (node should be either APPLY_UF or HO_APPLY) */
-  unsigned getArgumentStartIndexForApplyTerm( TNode node );
-public:
+  Node getApplyUfForHoApply(Node node);
+  /** get the operator for this node (node should be either APPLY_UF or
+   * HO_APPLY)
+   */
+  Node getOperatorForApplyTerm(TNode node);
+  /** get the starting index of the arguments for node (node should be either
+   * APPLY_UF or HO_APPLY) */
+  unsigned getArgumentStartIndexForApplyTerm(TNode node);
+
+ public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
   TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 46d856156..3899ff367 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -443,6 +443,7 @@ REG0_TESTS = \
 	regress0/ho/ext-ho.smt2 \
 	regress0/ho/ext-sat-partial-eval.smt2 \
 	regress0/ho/ext-sat.smt2 \
+	regress0/ho/finite-fun-ext.smt2 \
 	regress0/ho/ho-match-fun-suffix.smt2 \
 	regress0/ho/ho-matching-enum.smt2 \
 	regress0/ho/ho-matching-nested-app.smt2 \
diff --git a/test/regress/regress0/ho/finite-fun-ext.smt2 b/test/regress/regress0/ho/finite-fun-ext.smt2
new file mode 100644
index 000000000..005a2109a
--- /dev/null
+++ b/test/regress/regress0/ho/finite-fun-ext.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+
+(declare-datatype Unit ((unit)))
+
+(declare-fun f (Int) Unit)
+(declare-fun g (Int) Unit)
+(declare-fun P ((-> Int Unit)) Bool)
+
+(assert (P f))
+(assert (not (P g)))
+
+(check-sat)