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).

5 files changed, 57 insertions, 15 deletions

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 */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 787633178..edc44c3d2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1412,6 +1412,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3316.smt2
   regress1/quantifiers/issue3317.smt2
   regress1/quantifiers/issue3481.smt2
+  regress1/quantifiers/issue3537.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2
diff --git a/test/regress/regress1/quantifiers/issue3537.smt2 b/test/regress/regress1/quantifiers/issue3537.smt2
new file mode 100644
index 000000000..0a2f3feaa
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3537.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-datatypes ((UNIT 0)) (((Unit))
+))
+(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))
+))
+(declare-sort node$type 0)
+(declare-sort data$type 0)
+(declare-datatypes ((cache_state$type 0)) (((invalid) (shared) (exclusive))
+))
+(declare-datatypes ((cache$type 0)) (((c_cache$type (c_state cache_state$type) (c_data data$type)))
+))
+(declare-datatypes ((msg_cmd$type 0)) (((empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte))
+))
+(declare-datatypes ((msg$type 0)) (((c_msg$type (m_cmd msg_cmd$type) (m_data data$type)))
+))
+(declare-fun dummy () data$type)
+(declare-fun memdata$1 () data$type)
+(declare-fun shrset$1 () (Array node$type BOOL))
+(declare-fun recv_invack$i () node$type)
+(declare-fun exgntd () BOOL)
+(declare-fun chan3$1 () (Array node$type msg$type))
+(declare-fun shrset () (Array node$type BOOL))
+(declare-fun exgntd$1 () BOOL)
+(declare-fun chan2 () (Array node$type msg$type))
+(declare-fun chan3 () (Array node$type msg$type))
+(declare-fun curcmd () msg_cmd$type)
+(assert (distinct true (distinct true (forall ((n node$type)) (distinct false (not (= (select shrset n) Truth)) (and (= (m_cmd (select chan2 n)) empty) (= (m_cmd (select chan3 n)) empty))) ) (distinct false (= (m_cmd (select chan3 recv_invack$i)) invack) (=> (not (= curcmd empty)) (=> (= chan3$1 (store chan3 recv_invack$i (c_msg$type empty (m_data (select chan3 recv_invack$i))))) (distinct true (= shrset$1 (store shrset recv_invack$i Falsity)) (= (ite (= exgntd Truth) (ite (= false (= exgntd$1 Falsity) (=> (= memdata$1 (m_data (select chan3$1 recv_invack$i))) (exists ((n node$type)) (=> (not (= (select shrset$1 n) Truth)) (and (= (m_cmd (select chan2 n)) empty) (= (m_cmd (select chan3$1 n)) empty))) ))) Truth Falsity) (ite (forall ((n node$type)) (distinct true (not (= (select shrset$1 n) Truth)) (= true (= (m_cmd (select chan2 n)) empty) (= (m_cmd (select chan3$1 n)) empty))) ) Truth Falsity)) Truth))))))))
+(check-sat)
+(exit)