From 33c5eb093a7f032a7d9c9263da595eb53fdd223b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 Dec 2019 14:32:32 -0600
Subject: Fix case of uninterpreted constant instantiation in FMF (#3543)

Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).
---
 src/theory/quantifiers/fmf/full_model_check.cpp | 14 +++++++-------
 src/theory/rep_set.cpp                          | 16 ++++++++++------
 src/theory/rep_set.h                            | 10 ++++++++--
 3 files changed, 25 insertions(+), 15 deletions(-)

(limited to 'src')

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index f397b9a0a..d6c939e5d 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -793,13 +793,13 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       std::vector< Node > inst;
       for (unsigned i = 0; i < riter.getNumTerms(); i++)
       {
-        Node rr = riter.getCurrentTerm( i );
-        Node r = rr;
-        //if( r.getType().isSort() ){
-        r = fm->getRepresentative( r );
-        //}else{
-        //  r = fm->getCurrentModelValue( r );
-        //}
+        TypeNode tn = riter.getTypeOf(i);
+        // if the type is not closed enumerable (see
+        // TypeNode::isClosedEnumerable), then we must ensure that we are
+        // using a term and not a value. This ensures that e.g. uninterpreted
+        // constants do not appear in instantiations.
+        Node rr = riter.getCurrentTerm(i, !tn.isClosedEnumerable());
+        Node r = fm->getRepresentative(rr);
         debugPrint("fmc-exh-debug", r);
         Trace("fmc-exh-debug") << " (term : " << rr << ")";
         ev_inst.push_back( r );
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index ea462e55c..d293890bf 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -201,6 +201,8 @@ unsigned RepSetIterator::domainSize(unsigned i)
   return d_domain_elements[v].size();
 }
 
+TypeNode RepSetIterator::getTypeOf(unsigned i) const { return d_types[i]; }
+
 bool RepSetIterator::setQuantifier(Node q)
 {
   Trace("rsi") << "Make rsi for quantified formula " << q << std::endl;
@@ -403,14 +405,16 @@ int RepSetIterator::increment(){
 
 bool RepSetIterator::isFinished() const { return d_index.empty(); }
 
-Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm) const
+Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const
 {
-  unsigned ii = d_index_order[v];
+  unsigned ii = d_index_order[i];
   unsigned curr = d_index[ii];
-  Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
-  Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl;
-  Assert(0 <= curr && curr < d_domain_elements[v].size());
-  Node t = d_domain_elements[v][curr];
+  Trace("rsi-debug") << "rsi : get term " << i
+                     << ", index order = " << d_index_order[i] << std::endl;
+  Trace("rsi-debug") << "rsi : curr = " << curr << " / "
+                     << d_domain_elements[i].size() << std::endl;
+  Assert(0 <= curr && curr < d_domain_elements[i].size());
+  Node t = d_domain_elements[i][curr];
   if (valTerm)
   {
     Node tt = d_rs->getTermForRepresentative(t);
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 2ae5e1c4b..58f449202 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -175,8 +175,14 @@ public:
  bool isFinished() const;
  /** get domain size of the i^th field of this iterator */
  unsigned domainSize(unsigned i);
- /** get the i^th term in the tuple we are considering */
- Node getCurrentTerm(unsigned v, bool valTerm = false) const;
+ /** Get the type of terms in the i^th field of this iterator */
+ TypeNode getTypeOf(unsigned i) const;
+ /**
+  * Get the value for the i^th field in the tuple we are currently considering.
+  * If valTerm is true, we return a term instead of a value by calling
+  * RepSet::getTermForRepresentative on the value.
+  */
+ Node getCurrentTerm(unsigned i, bool valTerm = false) const;
  /** get the number of terms in the tuple we are considering */
  unsigned getNumTerms() const { return d_index_order.size(); }
  /** get current terms */
-- 
cgit v1.2.3