Statistics on instantiations per quantified formula. (#4719)

This adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).

It also simplifies and improves printing of Instantiation Tries.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2fb5dd0babcbe8ce1d3084485b7688f8d9e2465d..227f43c46b9edbb6337d03997e0a3022757f18f8 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1962,6 +1962,30 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"
 
+### Output options
+
+[[option]]
+  name       = "printInstMode"
+  category   = "regular"
+  long       = "print-inst=MODE"
+  type       = "PrintInstMode"
+  default    = "LIST"
+  help       = "print format for printing instantiations"
+  help_mode  = "Print format for printing instantiations."
+[[option.mode.LIST]]
+  name = "list"
+  help = "Print the list of instantiations per quantified formula, when non-empty."
+[[option.mode.NUM]]
+  name = "num"
+  help = "Print the total number of instantiations per quantified formula, when non-zero."
+
+[[option]]
+  name       = "printInstFull"
+  category   = "regular"
+  long       = "print-inst-full"
+  type       = "bool"
+  default    = "true"
+  help       = "print instantiations for formulas that do not have given identifiers"
 
 ### SyGuS instantiation options
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index cc87306e38c6e669d3c427819fbc3d375400fbcb..62ea4e4fa2a8516733972a64c67896c401b577e7 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1898,6 +1898,16 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }
+  | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr]
+    {
+      api::Sort boolType = SOLVER->getBooleanSort();
+      api::Term avar = SOLVER->mkVar(boolType, sexpr.toString());
+      attr = std::string(":qid");
+      retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
+      Command* c = new SetUserAttributeCommand("qid", avar.getExpr());
+      c->setMuted(true);
+      PARSER_STATE->preemptCommand(c);
+    }
   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
     {
       attr = std::string(":named");
@@ -2351,6 +2361,7 @@ ATTRIBUTE_PATTERN_TOK : ':pattern';
 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
 ATTRIBUTE_NAMED_TOK : ':named';
 ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
+ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid';
 
 // operators (NOTE: theory symbols go here)
 EXISTS_TOK        : 'exists';

diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index 0993edbae7baf7b7f7400d692c00a43defa257ca..e5ab440321db916825815a74c70079a015ce7b74 100644 (file)
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -131,7 +131,6 @@ bool InstMatchTrie::recordInstLemma(Node q,
 void InstMatchTrie::print(std::ostream& out,
                           Node q,
                           std::vector<TNode>& terms,
-                          bool& firstTime,
                           bool useActive,
                           std::vector<Node>& active) const
 {
@@ -156,11 +155,6 @@ void InstMatchTrie::print(std::ostream& out,
     }
     if (print)
     {
-      if (firstTime)
-      {
-        out << "(instantiation " << q << std::endl;
-        firstTime = false;
-      }
       out << "  ( ";
       for (unsigned i = 0, size = terms.size(); i < size; i++)
       {
@@ -178,7 +172,7 @@ void InstMatchTrie::print(std::ostream& out,
     for (const std::pair<const Node, InstMatchTrie>& d : d_data)
     {
       terms.push_back(d.first);
-      d.second.print(out, q, terms, firstTime, useActive, active);
+      d.second.print(out, q, terms, useActive, active);
       terms.pop_back();
     }
   }
@@ -392,7 +386,6 @@ bool CDInstMatchTrie::recordInstLemma(Node q,
 void CDInstMatchTrie::print(std::ostream& out,
                             Node q,
                             std::vector<TNode>& terms,
-                            bool& firstTime,
                             bool useActive,
                             std::vector<Node>& active) const
 {
@@ -419,11 +412,6 @@ void CDInstMatchTrie::print(std::ostream& out,
       }
       if (print)
       {
-        if (firstTime)
-        {
-          out << "(instantiation " << q << std::endl;
-          firstTime = false;
-        }
         out << "  ( ";
         for (unsigned i = 0; i < terms.size(); i++)
         {
@@ -438,7 +426,7 @@ void CDInstMatchTrie::print(std::ostream& out,
       for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
       {
         terms.push_back(d.first);
-        d.second->print(out, q, terms, firstTime, useActive, active);
+        d.second->print(out, q, terms, useActive, active);
         terms.pop_back();
       }
     }

diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index a827ff6975012945c0731ae0bca3d92604b1c1f2..961d1608c5a0033fe7bab52ce7fa139ea17954a7 100644 (file)
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -164,12 +164,11 @@ class InstMatchTrie
   /** print this class */
   void print(std::ostream& out,
              Node q,
-             bool& firstTime,
              bool useActive,
              std::vector<Node>& active) const
   {
     std::vector<TNode> terms;
-    print(out, q, terms, firstTime, useActive, active);
+    print(out, q, terms, useActive, active);
   }
   /** the data */
   std::map<Node, InstMatchTrie> d_data;
@@ -181,7 +180,6 @@ class InstMatchTrie
   void print(std::ostream& out,
              Node q,
              std::vector<TNode>& terms,
-             bool& firstTime,
              bool useActive,
              std::vector<Node>& active) const;
   /** helper for get instantiations
@@ -332,12 +330,11 @@ class CDInstMatchTrie
   /** print this class */
   void print(std::ostream& out,
              Node q,
-             bool& firstTime,
              bool useActive,
              std::vector<Node>& active) const
   {
     std::vector<TNode> terms;
-    print(out, q, terms, firstTime, useActive, active);
+    print(out, q, terms, useActive, active);
   }
 
  private:
@@ -351,7 +348,6 @@ class CDInstMatchTrie
   void print(std::ostream& out,
              Node q,
              std::vector<TNode>& terms,
-             bool& firstTime,
              bool useActive,
              std::vector<Node>& active) const;
   /** helper for get instantiations

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 53e9c68324c5fa09655c7a99ab239a4c82e9680a..d40a2c13d02537f120736256c8c5d9da59b6e46d 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -37,7 +37,7 @@ Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u)
     : d_qe(qe),
       d_term_db(nullptr),
       d_term_util(nullptr),
-      d_total_inst_count_debug(0),
+      d_total_inst_debug(u),
       d_c_inst_match_trie_dom(u)
 {
 }
@@ -264,9 +264,8 @@ bool Instantiate::addInstantiation(
     return false;
   }
 
-  d_total_inst_debug[q]++;
+  d_total_inst_debug[q] = d_total_inst_debug[q] + 1;
   d_temp_inst_debug[q]++;
-  d_total_inst_count_debug++;
   if (Trace.isOn("inst"))
   {
     Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
@@ -465,6 +464,16 @@ Node Instantiate::getTermForType(TypeNode tn)
 }
 
 bool Instantiate::printInstantiations(std::ostream& out)
+{
+  if (options::printInstMode() == options::PrintInstMode::NUM)
+  {
+    return printInstantiationsNum(out);
+  }
+  Assert(options::printInstMode() == options::PrintInstMode::LIST);
+  return printInstantiationsList(out);
+}
+
+bool Instantiate::printInstantiationsList(std::ostream& out)
 {
   bool useUnsatCore = false;
   std::vector<Node> active_lemmas;
@@ -473,35 +482,89 @@ bool Instantiate::printInstantiations(std::ostream& out)
     useUnsatCore = true;
   }
   bool printed = false;
+  bool isFull = options::printInstFull();
   if (options::incrementalSolving())
   {
     for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
     {
-      bool firstTime = true;
-      t.second->print(out, t.first, firstTime, useUnsatCore, active_lemmas);
-      if (!firstTime)
+      std::stringstream qout;
+      if (!printQuant(t.first, qout, isFull))
+      {
+        continue;
+      }
+      std::stringstream sout;
+      t.second->print(sout, t.first, useUnsatCore, active_lemmas);
+      if (!sout.str().empty())
       {
+        out << "(instantiations " << qout.str() << std::endl;
+        out << sout.str();
         out << ")" << std::endl;
+        printed = true;
       }
-      printed = printed || !firstTime;
     }
   }
   else
   {
     for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
     {
-      bool firstTime = true;
-      t.second.print(out, t.first, firstTime, useUnsatCore, active_lemmas);
-      if (!firstTime)
+      std::stringstream qout;
+      if (!printQuant(t.first, qout, isFull))
+      {
+        continue;
+      }
+      std::stringstream sout;
+      t.second.print(sout, t.first, useUnsatCore, active_lemmas);
+      if (!sout.str().empty())
       {
+        out << "(instantiations " << qout.str() << std::endl;
+        out << sout.str();
         out << ")" << std::endl;
+        printed = true;
       }
-      printed = printed || !firstTime;
     }
   }
+  out << std::endl;
   return printed;
 }
 
+bool Instantiate::printInstantiationsNum(std::ostream& out)
+{
+  if (d_total_inst_debug.empty())
+  {
+    return false;
+  }
+  bool isFull = options::printInstFull();
+  for (NodeUIntMap::iterator it = d_total_inst_debug.begin();
+       it != d_total_inst_debug.end();
+       ++it)
+  {
+    std::stringstream ss;
+    if (printQuant((*it).first, ss, isFull))
+    {
+      out << "(num-instantiations " << ss.str() << " " << (*it).second << ")"
+          << std::endl;
+    }
+  }
+  return true;
+}
+
+bool Instantiate::printQuant(Node q, std::ostream& out, bool isFull)
+{
+  if (isFull)
+  {
+    out << q;
+    return true;
+  }
+  quantifiers::QuantAttributes* qa = d_qe->getQuantAttributes();
+  Node name = qa->getQuantName(q);
+  if (name.isNull())
+  {
+    return false;
+  }
+  out << name;
+  return true;
+}
+
 void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 {
   if (options::incrementalSolving())
@@ -726,7 +789,7 @@ void Instantiate::debugPrint()
   // debug information
   if (Trace.isOn("inst-per-quant-round"))
   {
-    for (std::pair<const Node, int>& i : d_temp_inst_debug)
+    for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
     {
       Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first
                                     << std::endl;
@@ -739,10 +802,12 @@ void Instantiate::debugPrintModel()
 {
   if (Trace.isOn("inst-per-quant"))
   {
-    for (std::pair<const Node, int>& i : d_total_inst_debug)
+    for (NodeUIntMap::iterator it = d_total_inst_debug.begin();
+         it != d_total_inst_debug.end();
+         ++it)
     {
-      Trace("inst-per-quant") << " * " << i.second << " for " << i.first
-                              << std::endl;
+      Trace("inst-per-quant")
+          << " * " << (*it).second << " for " << (*it).first << std::endl;
     }
   }
 }

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index aa4f85cdca5e9f16d725f1c37a2e1e0889c8207c..630efe72ca11d534c05bf5ee7f7794d0a69947ca 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -81,6 +81,8 @@ class InstantiationRewriter
  */
 class Instantiate : public QuantifiersUtil
 {
+  typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap;
+
  public:
   Instantiate(QuantifiersEngine* qe, context::UserContext* u);
   ~Instantiate();
@@ -209,7 +211,8 @@ class Instantiate : public QuantifiersUtil
   /** print instantiations
    *
    * Print all instantiations for all quantified formulas on out,
-   * returns true if at least one instantiation was printed.
+   * returns true if at least one instantiation was printed. The type of output
+   * (list, num, etc.) is determined by printInstMode.
    */
   bool printInstantiations(std::ostream& out);
   /** get instantiated quantified formulas
@@ -323,6 +326,16 @@ class Instantiate : public QuantifiersUtil
    * if possible.
    */
   static Node ensureType(Node n, TypeNode tn);
+  /** print instantiations in list format */
+  bool printInstantiationsList(std::ostream& out);
+  /** print instantiations in num format */
+  bool printInstantiationsNum(std::ostream& out);
+  /**
+   * Print quantified formula q on output out. If isFull is false, then we print
+   * the identifier of the quantified formula if it has one, or print
+   * nothing and return false otherwise.
+   */
+  bool printQuant(Node q, std::ostream& out, bool isFull);
 
   /** pointer to the quantifiers engine */
   QuantifiersEngine* d_qe;
@@ -333,12 +346,10 @@ class Instantiate : public QuantifiersUtil
   /** instantiation rewriter classes */
   std::vector<InstantiationRewriter*> d_instRewrite;
 
-  /** statistics for debugging total instantiation */
-  int d_total_inst_count_debug;
   /** statistics for debugging total instantiations per quantifier */
-  std::map<Node, int> d_total_inst_debug;
+  NodeUIntMap d_total_inst_debug;
   /** statistics for debugging total instantiations per quantifier per round */
-  std::map<Node, int> d_temp_inst_debug;
+  std::map<Node, uint32_t> d_temp_inst_debug;
 
   /** list of all instantiations produced for each quantifier
    *

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 17c6256529b6a1f99af3f23180723bf85879f6d5..c00d3c5791a7d930693aae87123cb1e941e5d030 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -50,8 +50,9 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     SygusAttribute ca;
     n.setAttribute( ca, true );
   }
-  else if (attr == "quant-name")
+  else if (attr == "qid")
   {
+    // using z3 syntax "qid"
     Trace("quant-attr-debug") << "Set quant-name " << n << std::endl;
     QuantNameAttribute qna;
     n.setAttribute(qna, true);
@@ -303,6 +304,16 @@ bool QuantAttributes::isQuantElimPartial( Node q ) {
   }
 }
 
+Node QuantAttributes::getQuantName(Node q) const
+{
+  std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
+  if (it != d_qattr.end())
+  {
+    return it->second.d_name;
+  }
+  return Node::null();
+}
+
 int QuantAttributes::getQuantIdNum( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it!=d_qattr.end() ){

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 189c7947013822d4373bc6c588ec4244d786708c..cadf0b0d603243c519553209f503c5679dc5f6d7 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -126,9 +126,9 @@ struct QAttributes
   /** the instantiation pattern list for this quantified formula (its 3rd child)
    */
   Node d_ipl;
-  /** the name of this quantified formula */
+  /** The name of this quantified formula, used for :qid */
   Node d_name;
-  /** the quantifier id associated with this formula */
+  /** The (internal) quantifier id associated with this formula */
   Node d_qid_num;
   /** is this quantified formula a function definition? */
   bool isFunDef() const { return !d_fundef_f.isNull(); }
@@ -198,9 +198,11 @@ public:
   bool isQuantElim( Node q );
   /** is quant elim partial */
   bool isQuantElimPartial( Node q );
-  /** get quant id num */
+  /** get quant name, which is used for :qid */
+  Node getQuantName(Node q) const;
+  /** get (internal) quant id num */
   int getQuantIdNum( Node q );
-  /** get quant id num */
+  /** get (internal)quant id num */
   Node getQuantIdNumNode( Node q );
 
   /** set instantiation level attr */

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index e7d5d36a37805b7f9f25c6ba1c0b737f844cbbe1..7365960e9e95b6a290c00e72834fa2d685aeea41 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -46,7 +46,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
 {
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute( "sygus", this );
-  out.handleUserAttribute("quant-name", this);
+  out.handleUserAttribute("qid", this);
   out.handleUserAttribute("sygus-synth-grammar", this);
   out.handleUserAttribute( "sygus-synth-fun-var-list", this );
   out.handleUserAttribute( "quant-inst-max-level", this );

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 6dce6ce1e5eb091c7e2db459aedb2b6b66246440..534d92c92393a13aeb9f19bc42e3db16b4cb1dd0 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1153,9 +1153,12 @@ void QuantifiersEngine::getExplanationForInstLemmas(
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
   bool printed = false;
   // print the skolemizations
-  if (d_skolemize->printSkolemization(out))
+  if (options::printInstMode() == options::PrintInstMode::LIST)
   {
-    printed = true;
+    if (d_skolemize->printSkolemization(out))
+    {
+      printed = true;
+    }
   }
   // print the instantiations
   if (d_instantiate->printInstantiations(out))

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c5048ae63583f89d34611db9b1ead8f48def58ba..0449107af4f842389ab59be1c7d57f18aaa27744 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1603,6 +1603,7 @@ set(regress_1_tests
   regress1/quantifiers/qcft-smtlib3dbc51.smt2
   regress1/quantifiers/qe-partial.smt2
   regress1/quantifiers/qe.smt2
+  regress1/quantifiers/qid.smt2
   regress1/quantifiers/quant-wf-int-ind.smt2
   regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
   regress1/quantifiers/recfact.cvc

diff --git a/test/regress/regress1/quantifiers/dump-inst-i.smt2 b/test/regress/regress1/quantifiers/dump-inst-i.smt2
index 9221a2abcd1cf86e93e42b27da28615d6977b694..94dbe9f88fa98c7a0a0a16e411873a93440435c0 100644 (file)
--- a/test/regress/regress1/quantifiers/dump-inst-i.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-i.smt2
@@ -4,14 +4,14 @@
 ; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
-; EXPECT: (instantiation (forall ((x Int)) (P x) )
+; EXPECT: (instantiations (forall ((x Int)) (P x) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
 ; EXPECT: unsat
 ; EXPECT: (skolem (forall ((x Int)) (or (P x) (R x)) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
-; EXPECT: (instantiation (forall ((x Int)) (P x) )
+; EXPECT: (instantiations (forall ((x Int)) (P x) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
 (set-logic UFLIA)

diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index 674950c34414e69f1ff3242ad2b98faa1bdb742d..2995f768249fc01f3c9f90e4d6cc70da5ad880b6 100644 (file)
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,10 +1,10 @@
 ; REQUIRES: proof
 ; COMMAND-LINE: --dump-instantiations --proof
 ; EXPECT: unsat
-; EXPECT: (instantiation (forall ((x Int)) (or (P x) (Q x)) )
+; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( 2 )
 ; EXPECT: )
-; EXPECT: (instantiation (forall ((x Int)) (or (not (S x)) (not (Q x))) )
+; EXPECT: (instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))) )
 ; EXPECT:   ( 2 )
 ; EXPECT: )
 (set-logic UFLIA)

diff --git a/test/regress/regress1/quantifiers/dump-inst.smt2 b/test/regress/regress1/quantifiers/dump-inst.smt2
index 38e60d4db36501c1912a31d3eca00e7f836267e3..3a8bc4b9c77c214b18ac7c34d85657516edf4037 100644 (file)
--- a/test/regress/regress1/quantifiers/dump-inst.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst.smt2
@@ -4,7 +4,7 @@
 ; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
-; EXPECT: (instantiation (forall ((x Int)) (P x) )
+; EXPECT: (instantiations (forall ((x Int)) (P x) )
 ; EXPECT:   ( skv_TERM )
 ; EXPECT: )
 (set-logic UFLIA)

diff --git a/test/regress/regress1/quantifiers/qid.smt2 b/test/regress/regress1/quantifiers/qid.smt2
new file mode 100644 (file)
index 0000000..0563933
--- /dev/null
+++ b/test/regress/regress1/quantifiers/qid.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --dump-instantiations --print-inst=num --no-print-inst-full
+; EXPECT: unsat
+; EXPECT: (num-instantiations myQuantP 1)
+; EXPECT: (num-instantiations myQuantQ 7)
+
+(set-logic UFLIA)
+(declare-fun P (Int) Bool)
+(declare-fun Q (Int) Bool)
+(assert (forall ((x Int)) (! (P x) :qid |myQuantP|)))
+(assert (forall ((x Int)) (! (=> (Q x) (Q (+ x 1))) :qid |myQuantQ|)))
+(assert (Q 0))
+(assert (or (not (P 5)) (not (Q 7))))
+(check-sat)