From 33c5eb093a7f032a7d9c9263da595eb53fdd223b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 9 Dec 2019 14:32:32 -0600 Subject: [PATCH] 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). --- .../quantifiers/fmf/full_model_check.cpp | 14 ++++----- src/theory/rep_set.cpp | 16 ++++++---- src/theory/rep_set.h | 10 ++++-- test/regress/CMakeLists.txt | 1 + .../regress1/quantifiers/issue3537.smt2 | 31 +++++++++++++++++++ 5 files changed, 57 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue3537.smt2 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) -- 2.30.2