Do not expand APPLY_SELECTOR (#8174)

Currently we expand (sel_C_n x) to (ite (is-C x) (sel_C_n_total x) (uf x)) during ppRewrite. This introduces ITEs very eagerly and moreover is not necessary since we do congruence over selectors.

This makes it so that we don't do this expansion. The code changes to use APPLY_SELECTOR everywhere instead of APPLY_SELECTOR_TOTAL, which can be deleted in a followup PR. It makes some of the datatype utilities more robust and independent of options.

This required changing one detail of the sygus solver to not do evaluation unfolding in cases where a selector chain was wrongly applied, as this now will not rewrite to a constant.

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index a054dffb890c2ff101f111e544e0ac48a97e020b..269f3ebca3b96bea43d58a2d65758b1841fa8a63 100644 (file)
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -260,26 +260,25 @@ Node DTypeConstructor::getSelectorInternal(TypeNode domainType,
 int DTypeConstructor::getSelectorIndexInternal(Node sel) const
 {
   Assert(isResolved());
-  if (options::dtSharedSelectors())
+  Assert(sel.getType().isSelector());
+  // might be a builtin selector
+  if (sel.hasAttribute(DTypeIndexAttr()))
   {
-    Assert(sel.getType().isSelector());
-    TypeNode domainType = sel.getType().getSelectorDomainType();
-    computeSharedSelectors(domainType);
-    std::map<Node, unsigned>::iterator its =
-        d_sharedSelectorIndex[domainType].find(sel);
-    if (its != d_sharedSelectorIndex[domainType].end())
-    {
-      return (int)its->second;
-    }
-  }
-  else
-  {
-    unsigned sindex = DType::indexOf(sel);
+    size_t sindex = DType::indexOf(sel);
     if (getNumArgs() > sindex && d_args[sindex]->getSelector() == sel)
     {
       return static_cast<int>(sindex);
     }
   }
+  // otherwise, check shared selector
+  TypeNode domainType = sel.getType().getSelectorDomainType();
+  computeSharedSelectors(domainType);
+  std::map<Node, unsigned>::iterator its =
+      d_sharedSelectorIndex[domainType].find(sel);
+  if (its != d_sharedSelectorIndex[domainType].end())
+  {
+    return (int)its->second;
+  }
   return -1;
 }
 

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 12acc1402005b2b7372552be1bd5de2042bb3013..a88421c7a8d48d8fcea63994053bc703c3cfefc2 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -395,29 +395,9 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
                                      << std::endl;
     // The argument that the selector extracts, or -1 if the selector is
     // is wrongly applied.
-    int selectorIndex = -1;
-    if (k == kind::APPLY_SELECTOR_TOTAL)
-    {
-      // The argument index of internal selectors is obtained by
-      // getSelectorIndexInternal.
-      selectorIndex = c.getSelectorIndexInternal(selector);
-    }
-    else
-    {
-      // The argument index of external selectors (applications of
-      // APPLY_SELECTOR) is given by an attribute and obtained via indexOf below
-      // The argument is only valid if it is the proper constructor.
-      selectorIndex = utils::indexOf(selector);
-      if (selectorIndex < 0
-          || selectorIndex >= static_cast<int>(c.getNumArgs()))
-      {
-        selectorIndex = -1;
-      }
-      else if (c[selectorIndex].getSelector() != selector)
-      {
-        selectorIndex = -1;
-      }
-    }
+    // The argument index of internal selectors is obtained by
+    // getSelectorIndexInternal.
+    int selectorIndex = c.getSelectorIndexInternal(selector);
     Trace("datatypes-rewrite-debug") << "Internal selector index is "
                                      << selectorIndex << std::endl;
     if (selectorIndex >= 0)
@@ -840,39 +820,24 @@ Node DatatypesRewriter::expandApplySelector(Node n)
 {
   Assert(n.getKind() == APPLY_SELECTOR);
   Node selector = n.getOperator();
+  if (!options::dtSharedSelectors()
+      || !selector.hasAttribute(DTypeConsIndexAttr()))
+  {
+    return n;
+  }
   // APPLY_SELECTOR always applies to an external selector, cindexOf is
   // legal here
   size_t cindex = utils::cindexOf(selector);
   const DType& dt = utils::datatypeOf(selector);
   const DTypeConstructor& c = dt[cindex];
-  Node selector_use;
   TypeNode ndt = n[0].getType();
-  if (options::dtSharedSelectors())
-  {
-    size_t selectorIndex = utils::indexOf(selector);
-    Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl;
-    Assert(selectorIndex < c.getNumArgs());
-    selector_use = c.getSelectorInternal(ndt, selectorIndex);
-  }
-  else
-  {
-    selector_use = selector;
-  }
+  size_t selectorIndex = utils::indexOf(selector);
+  Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl;
+  Assert(selectorIndex < c.getNumArgs());
+  Node selector_use = c.getSelectorInternal(ndt, selectorIndex);
   NodeManager* nm = NodeManager::currentNM();
-  Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
-  if (options::dtRewriteErrorSel())
-  {
-    return sel;
-  }
-  Node tester = c.getTester();
-  Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
-  SkolemManager* sm = nm->getSkolemManager();
-  TypeNode tnw = nm->mkFunctionType(ndt, n.getType());
-  Node f = sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector);
-  Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]);
-  Node ret = nm->mkNode(kind::ITE, tst, sel, sk);
-  Trace("dt-expand") << "Expand def : " << n << " to " << ret << std::endl;
-  return ret;
+  Node sel = nm->mkNode(kind::APPLY_SELECTOR, selector_use, n[0]);
+  return sel;
 }
 
 TrustNode DatatypesRewriter::expandDefinition(Node n)
@@ -916,8 +881,7 @@ TrustNode DatatypesRewriter::expandDefinition(Node n)
         }
         else
         {
-          b << nm->mkNode(
-              APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(tn, i), n[0]);
+          b << nm->mkNode(APPLY_SELECTOR, dc.getSelectorInternal(tn, i), n[0]);
         }
       }
       ret = b;

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 86ff493ea014bf476f0ff1567f42575cf2a580cb..5139d81b89368912fbcb86dfd3023232bd3b4cff 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -64,11 +64,12 @@ class DatatypesRewriter : public TheoryRewriter
    * Expand an APPLY_SELECTOR term n, return its expanded form. If n is
    *   (APPLY_SELECTOR selC x)
    * its expanded form is
-   *   (ITE (APPLY_TESTER is-C x)
-   *     (APPLY_SELECTOR_TOTAL selC' x)
-   *     (f x))
+   *   (APPLY_SELECTOR selC' x)
    * where f is a skolem function with id SELECTOR_WRONG, and selC' is the
    * internal selector function for selC (possibly a shared selector).
+   * Note that we do not introduce an uninterpreted function here, e.g. to
+   * handle when the selector is misapplied. This is because it suffices to
+   * reason about the original selector term e.g. via congruence.
    */
   static Node expandApplySelector(Node n);
   /**

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index e49d58f9162e67fb96d8dc1a3f90e991db80e53a..86386ab78876617d9314bdda079d9ed7b38cc6fe 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -169,7 +169,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
         Node concAtom = concPol ? conc : conc[0];
         concEq = concAtom.eqNode(nm->mkConst(concPol));
       }
-      if (concEq[0].getKind() != APPLY_SELECTOR_TOTAL)
+      if (concEq[0].getKind() != APPLY_SELECTOR)
       {
         // can happen for Boolean term variables, which are not currently
         // supported.
@@ -179,14 +179,14 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
       {
         Assert(exp[0].getType().isDatatype());
         Node sop = concEq[0].getOperator();
-        Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]);
-        Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]);
+        Node sl = nm->mkNode(APPLY_SELECTOR, sop, exp[0]);
+        Node sr = nm->mkNode(APPLY_SELECTOR, sop, exp[1]);
         // exp[0] = exp[1]
         // --------------------- CONG        ----------------- DT_COLLAPSE
         // s(exp[0]) = s(exp[1])             s(exp[1]) = r
         // --------------------------------------------------- TRANS
         // s(exp[0]) = r
-        Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL);
+        Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR);
         Node seq = sl.eqNode(sr);
         cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop});
         Node sceq = sr.eqNode(concEq[1]);

diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 69153ef005aa7300ce5891bbf391e0a605acd4d8..9384411510cc673372d2906d6b711f786a976038 100644 (file)
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -82,7 +82,7 @@ Node DatatypesProofRuleChecker::checkInternal(PfRule id,
     Assert(children.empty());
     Assert(args.size() == 1);
     Node t = args[0];
-    if (t.getKind() != kind::APPLY_SELECTOR_TOTAL
+    if (t.getKind() != kind::APPLY_SELECTOR
         || t[0].getKind() != kind::APPLY_CONSTRUCTOR)
     {
       return Node::null();

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 03c1fe9e0ed0ec8a739bbdeda34514b1588d08ce..d46e6e28d4ad300bc0fe90337941872cb15560b6 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -81,7 +81,8 @@ void SygusExtension::assertTester(int tindex, TNode n, Node exp)
       bool do_add = true;
       if (options().datatypes.sygusSymBreakLazy)
       {
-        if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+        if (n.getKind() == kind::APPLY_SELECTOR)
+        {
           NodeSet::const_iterator it = d_active_terms.find( n[0] );
           if( it==d_active_terms.end() ){
             do_add = false;
@@ -158,7 +159,8 @@ void SygusExtension::registerTerm(Node n)
     unsigned d = 0;
     bool is_top_level = false;
     bool success = false;
-    if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+    if (n.getKind() == kind::APPLY_SELECTOR)
+    {
       registerTerm(n[0]);
       std::unordered_map<Node, Node>::iterator it = d_term_to_anchor.find(n[0]);
       if( it!=d_term_to_anchor.end() ) {
@@ -169,7 +171,9 @@ void SygusExtension::registerTerm(Node n)
         is_top_level = computeTopLevel( tn, n[0] );
         success = true;
       }
-    }else if( n.isVar() ){
+    }
+    else if (n.isVar())
+    {
       registerSizeTerm(n);
       if( d_register_st[n] ){
         d_term_to_anchor[n] = n;
@@ -197,9 +201,13 @@ void SygusExtension::registerTerm(Node n)
 bool SygusExtension::computeTopLevel( TypeNode tn, Node n ){
   if( n.getType()==tn ){
     return false;
-  }else if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+  }
+  else if (n.getKind() == kind::APPLY_SELECTOR)
+  {
     return computeTopLevel( tn, n[0] );
-  }else{
+  }
+  else
+  {
     return true;
   }
 }
@@ -367,8 +375,8 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp)
   {
     Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
     for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
-      Node sel = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(ntn, j), n);
+      Node sel =
+          nm->mkNode(APPLY_SELECTOR, dt[tindex].getSelectorInternal(ntn, j), n);
       Trace("sygus-sb-debug2") << "  activate child sel : " << sel << std::endl;
       Assert(d_active_terms.find(sel) == d_active_terms.end());
       IntMap::const_iterator itt = d_testers.find( sel );
@@ -389,7 +397,7 @@ Node SygusExtension::getRelevancyCondition( Node n ) {
   std::map< Node, Node >::iterator itr = d_rlv_cond.find( n );
   if( itr==d_rlv_cond.end() ){
     Node cond;
-    if (n.getKind() == APPLY_SELECTOR_TOTAL)
+    if (n.getKind() == APPLY_SELECTOR)
     {
       TypeNode ntn = n[0].getType();
       const DType& dt = ntn.getDType();
@@ -476,7 +484,7 @@ Node SygusExtension::eliminateTraversalPredicates(Node n)
       {
         Assert(cur.getType().isBoolean());
         Assert(cur.getNumChildren() == 1
-               && (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR_TOTAL));
+               && (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR));
         ittb = d_traversal_bool.find(cur);
         Node ret;
         if (ittb == d_traversal_bool.end())
@@ -593,8 +601,8 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
   std::vector<Node> children;
   for (unsigned j = 0; j < dt_index_nargs; j++)
   {
-    Node sel = nm->mkNode(
-        APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, j), n);
+    Node sel =
+        nm->mkNode(APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, j), n);
     Assert(sel.getType().isDatatype());
     children.push_back(sel);
   }
@@ -919,9 +927,8 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
           && children[0].getType() == tn && children[1].getType() == tn)
       {
         // chainable
-        Node child11 = nm->mkNode(APPLY_SELECTOR_TOTAL,
-                                  dt[tindex].getSelectorInternal(tn, 1),
-                                  children[0]);
+        Node child11 = nm->mkNode(
+            APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, 1), children[0]);
         Assert(child11.getType() == children[1].getType());
         Node order_pred_trans =
             nm->mkNode(OR,
@@ -1007,8 +1014,8 @@ Node SygusExtension::registerSearchValue(Node a,
     bool childrenChanged = false;
     for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++)
     {
-      Node sel = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n);
+      Node sel =
+          nm->mkNode(APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), n);
       Node nvc = registerSearchValue(a,
                                      sel,
                                      nv[i],
@@ -1726,8 +1733,8 @@ bool SygusExtension::checkValue(Node n, TNode vn, int ind)
     }
   }
   for( unsigned i=0; i<vn.getNumChildren(); i++ ){
-    Node sel = nm->mkNode(
-        APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n);
+    Node sel =
+        nm->mkNode(APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), n);
     if (!checkValue(sel, vn[i], ind + 1))
     {
       return false;
@@ -1749,7 +1756,7 @@ Node SygusExtension::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_
     children.push_back(dt[tindex].getConstructor());
     for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
       Node sel = NodeManager::currentNM()->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, i), n);
+          APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, i), n);
       Node cc = getCurrentTemplate( sel, var_count );
       children.push_back( cc );
     }

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 555b35a36d5ed770bb756ed1e69278d0c6447d12..74228167ae5fa59cd6e6841042281bf42fca3431 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -104,7 +104,7 @@ void TheoryDatatypes::finishInit()
   Assert(d_equalityEngine != nullptr);
   // The kinds we are treating as function application in congruence
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
+  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   // We could but don't do congruence for DT_SIZE and DT_HEIGHT_BOUND here.
   // It also could make sense in practice to do congruence for APPLY_UF, but
@@ -445,8 +445,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n)
 {
   Trace("datatypes-prereg")
       << "TheoryDatatypes::preRegisterTerm() " << n << endl;
-  // external selectors should be preprocessed away by now
-  Assert(n.getKind() != APPLY_SELECTOR);
+  // should not use APPLY_SELECTOR_TOTAL
+  Assert(n.getKind() != APPLY_SELECTOR_TOTAL);
   // must ensure the type is well founded and has no nested recursion if
   // the option dtNestedRec is not set to true.
   TypeNode tn = n.getType();
@@ -992,30 +992,26 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   Node r;
   bool wrong = false;
   Node eq_exp = s[0].eqNode(c);
-  if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+  if (s.getKind() == kind::APPLY_SELECTOR)
+  {
     Node selector = s.getOperator();
     size_t constructorIndex = utils::indexOf(c.getOperator());
     const DType& dt = utils::datatypeOf(selector);
     const DTypeConstructor& dtc = dt[constructorIndex];
     int selectorIndex = dtc.getSelectorIndexInternal(selector);
+    Trace("dt-collapse-sel")
+        << "selector index is " << selectorIndex << std::endl;
     wrong = selectorIndex<0;
-    r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
+    r = NodeManager::currentNM()->mkNode(
+        kind::APPLY_SELECTOR, s.getOperator(), c);
   }
   if( !r.isNull() ){
     Node rrs;
     if (wrong)
     {
-      // Must use make ground term here instead of the rewriter, since we
-      // do not want to introduce arbitrary values. This is important so that
-      // we avoid constants for types that are not "closed enumerable", e.g.
-      // uninterpreted sorts and arrays, where the solver does not fully
-      // handle values of the sort. The call to mkGroundTerm does not introduce
-      // values for these sorts.
-      NodeManager* nm = NodeManager::currentNM();
-      rrs = nm->mkGroundTerm(r.getType());
-      Trace("datatypes-wrong-sel")
-          << "Bad apply " << r << " term = " << rrs
-          << ", value = " << nm->mkGroundValue(r.getType()) << std::endl;
+      // If the selector application was wrong, we do nothing. The selector
+      // term in this context will be unevaluated, and treated via congruence.
+      return;
     }
     else
     {
@@ -1387,7 +1383,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
     }
     return;
   }
-  if (nk == APPLY_SELECTOR_TOTAL || nk == DT_SIZE || nk == DT_HEIGHT_BOUND)
+  if (nk == APPLY_SELECTOR || nk == DT_SIZE || nk == DT_HEIGHT_BOUND)
   {
     d_functionTerms.push_back(n);
     // we must also record which selectors exist

diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index a429f83333349be26053a6dd1bd4be1708c2d749..d69ec9cd5786a2b30ba26dec2caf1cda00206041 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -36,8 +36,8 @@ Node getInstCons(Node n, const DType& dt, size_t index)
   TypeNode tn = n.getType();
   for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
   {
-    Node nc = nm->mkNode(
-        APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
+    Node nc =
+        nm->mkNode(APPLY_SELECTOR, dt[index].getSelectorInternal(tn, i), n);
     children.push_back(nc);
   }
   Node n_ic = mkApplyCons(tn, dt, index, children);
@@ -77,7 +77,7 @@ int isInstCons(Node t, Node n, const DType& dt)
     TypeNode tn = n.getType();
     for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
     {
-      if (n[i].getKind() != APPLY_SELECTOR_TOTAL
+      if (n[i].getKind() != APPLY_SELECTOR
           || n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t)
       {
         return -1;

diff --git a/src/theory/datatypes/tuple_utils.cpp b/src/theory/datatypes/tuple_utils.cpp
index d691b3831481074d88f221ff0a96bce25ab6c037..0a852c01e51971f3772071f38ee8e10d87a694dc 100644 (file)
--- a/src/theory/datatypes/tuple_utils.cpp
+++ b/src/theory/datatypes/tuple_utils.cpp
@@ -33,7 +33,7 @@ Node TupleUtils::nthElementOfTuple(Node tuple, int n_th)
   TypeNode tn = tuple.getType();
   const DType& dt = tn.getDType();
   return NodeManager::currentNM()->mkNode(
-      APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple);
+      APPLY_SELECTOR, dt[0].getSelectorInternal(tn, n_th), tuple);
 }
 
 std::vector<Node> TupleUtils::getTupleElements(Node tuple)

diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index b5ce012b7326f7e92dd027c6b119bf3877b7d178..0d8da809ea35875022dfcf01812070cc0a19d01f 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -66,9 +66,8 @@ bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
       // now must solve for selectors applied to pv
       for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
       {
-        Node c = nm->mkNode(APPLY_SELECTOR_TOTAL,
-                            dt[cindex].getSelectorInternal(d_type, j),
-                            pv);
+        Node c = nm->mkNode(
+            APPLY_SELECTOR, dt[cindex].getSelectorInternal(d_type, j), pv);
         ci->pushStackVariable(c);
         children.push_back(c);
       }
@@ -154,7 +153,7 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
       for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
       {
         Node nn = nm->mkNode(
-            APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), sb);
+            APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), sb);
         Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
         if (!s.isNull())
         {

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 414ff2e3bc0f5fc5098f11b960763afb77673e39..8d1f9f0074f94a7fb427e8c40675be9b9d5a7370 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -232,7 +232,7 @@ void CegInstantiator::computeProgVars( Node n ){
       d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end());
     }
     // selectors applied to program variables are also variables
-    if (n.getKind() == APPLY_SELECTOR_TOTAL
+    if (n.getKind() == APPLY_SELECTOR
         && d_prog_var[n].find(n[0]) != d_prog_var[n].end())
     {
       d_prog_var[n].insert(n);

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index db62da53b276087c04c4e662e5c3be756938941e..7f2ddd35db004e3eb6c206537d26b9b7174a9a27 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1844,7 +1844,9 @@ void TermGenEnv::collectSignatureInformation() {
     {
       Node nn = dbl->d_list[0];
       Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
-      if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
+      if (d_cg->isHandledTerm(nn) && nn.getKind() != APPLY_SELECTOR
+          && !nn.getType().isBoolean())
+      {
         bool do_enum = true;
         //check if we have enumerated ground terms
         if( nn.getKind()==APPLY_UF ){

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 57752d3752d6db8544a22980cbababacbbe3eaaa..f32655eb27b15a63ef14d91dc84bea68790c4b1e 100644 (file)
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -291,7 +291,7 @@ Node CandidateGeneratorConsExpand::getNextCandidate()
   for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
   {
     Node sel = nm->mkNode(
-        APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
+        APPLY_SELECTOR, dt[0].getSelectorInternal(d_mpat_type, i), curr);
     children.push_back(sel);
   }
   return nm->mkNode(APPLY_CONSTRUCTOR, children);
@@ -316,12 +316,12 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
   Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
   if (mpatExp.getKind() == ITE)
   {
-    Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
+    Assert(mpatExp[1].getKind() == APPLY_SELECTOR);
     Assert(mpatExp[2].getKind() == APPLY_UF);
     d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
     d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]);
   }
-  else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL)
+  else if (mpatExp.getKind() == APPLY_SELECTOR)
   {
     // corner case of datatype with one constructor
     d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 8392cd493d64c3b1f7467217607d291ae7b58cb4..516c9803cfe6210d8f8e4605669e035ea9d52b38 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -245,7 +245,7 @@ void InstMatchGenerator::initialize(Node q,
   }
   else if (mpk == INST_CONSTANT)
   {
-    if (d_pattern.getKind() == APPLY_SELECTOR_TOTAL)
+    if (d_pattern.getKind() == APPLY_SELECTOR)
     {
       Node selectorExpr = tdb->getMatchOperator(d_pattern);
       size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);

diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp
index 611f30ef05391edf232f82a300e1c5d6891d704d..0ba980d59e59196556b2b36a8c367871bba2d4a9 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger_term_info.cpp
+++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp
@@ -49,16 +49,12 @@ bool TriggerTermInfo::isAtomicTrigger(Node n)
 
 bool TriggerTermInfo::isAtomicTriggerKind(Kind k)
 {
-  // we use both APPLY_SELECTOR and APPLY_SELECTOR_TOTAL since this
-  // method is used both for trigger selection and for ground term registration,
-  // where these two things require those kinds respectively.
   return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
-         || k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL
-         || k == APPLY_TESTER || k == SET_UNION || k == SET_INTER
-         || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER
-         || k == SET_SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT
-         || k == INT_TO_BITVECTOR || k == HO_APPLY || k == STRING_LENGTH
-         || k == SEQ_NTH;
+         || k == APPLY_SELECTOR || k == APPLY_TESTER || k == SET_UNION
+         || k == SET_INTER || k == SET_SUBSET || k == SET_MINUS
+         || k == SET_MEMBER || k == SET_SINGLETON || k == SEP_PTO
+         || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY
+         || k == STRING_LENGTH || k == SEQ_NTH;
 }
 
 bool TriggerTermInfo::isRelationalTrigger(Node n)

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 2b44d240407b99dc131df3fbc7a6ad829fd8413a..33030894624183ffd032c546ad9d153979981500 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -787,9 +787,8 @@ Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
       if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
         u = matchBoundVar( v, t[i], e[i] );
       }else{
-        Node se = nm->mkNode(APPLY_SELECTOR_TOTAL,
-                             dt[index].getSelectorInternal(e.getType(), i),
-                             e);
+        Node se = nm->mkNode(
+            APPLY_SELECTOR, dt[index].getSelectorInternal(e.getType(), i), e);
         u = matchBoundVar( v, t[i], se );
       }
       if( !u.isNull() ){

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index fc292834397a3cef76d2d2ea83915bec2f5602ed..f24a1d6460a1bdfc8e60ca90a54126aeac2d2027 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2078,10 +2078,6 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
 }
 
 bool MatchGen::isHandledUfTerm( TNode n ) {
-  //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
-  //       n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
-  //TODO : treat APPLY_TESTER as a T-constraint instead of matching (currently leads to overabundance of instantiations)
-  //return inst::Trigger::isAtomicTriggerKind( n.getKind() ) && ( !options::qcfTConstraint() || n.getKind()!=APPLY_TESTER );
   return inst::TriggerTermInfo::isAtomicTriggerKind(n.getKind());
 }
 

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index fdd5fa0ac5d20e99d7a947975e7501669489af98..6d37fd75a553e718433d133d57a172c308302e3b 100644 (file)
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -168,8 +168,8 @@ void Skolemize::getSelfSel(const DType& dt,
     }
     for (unsigned k = 0; k < ssc.size(); k++)
     {
-      Node ss = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(n.getType(), j), n);
+      Node ss =
+          nm->mkNode(APPLY_SELECTOR, dc.getSelectorInternal(n.getType(), j), n);
       if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
       {
         selfSel.push_back(ss);

diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index b3c0522f93cb85aac6f2b75d550ea06ede68f81d..2e52f67d3ea328c26ded5d72e49013e8e911c8dd 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -100,6 +100,11 @@ void SygusEvalUnfold::registerModelValue(Node a,
       TNode vt = v;
       Node vn = n.substitute(at, vt);
       vn = rewrite(vn);
+      // it might be incorrectly applied
+      if (!vn.isConst())
+      {
+        continue;
+      }
       unsigned start = d_node_mv_args_proc[n][vn];
       // get explanation in terms of testers
       std::vector<Node> antec_exp;
@@ -275,7 +280,7 @@ Node SygusEvalUnfold::unfold(Node en,
     else
     {
       Node ret = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
+          APPLY_SELECTOR, dt[i].getSelectorInternal(headType, 0), en[0]);
       Trace("sygus-eval-unfold-debug")
           << "...return (from constructor) " << ret << std::endl;
       return ret;
@@ -298,7 +303,7 @@ Node SygusEvalUnfold::unfold(Node en,
     else
     {
       s = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, j), en[0]);
+          APPLY_SELECTOR, dt[i].getSelectorInternal(headType, j), en[0]);
     }
     cc.push_back(s);
     if (track_exp)

diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 23c315f425fe59808a3a6ee61d0aeebb0a28595c..dfbbc64b2cc0420f6a0abeb1154436b9a44308e8 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -153,7 +153,7 @@ void SygusExplain::getExplanationForEquality(Node n,
     if (cexc.find(j) == cexc.end())
     {
       Node sel = NodeManager::currentNM()->mkNode(
-          kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n);
+          kind::APPLY_SELECTOR, dt[i].getSelectorInternal(tn, j), n);
       getExplanationForEquality(sel, vn[j], exp);
     }
   }
@@ -249,7 +249,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
   for (unsigned i = 0; i < vn.getNumChildren(); i++)
   {
     Node sel = NodeManager::currentNM()->mkNode(
-        kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n);
+        kind::APPLY_SELECTOR, dt[cindex].getSelectorInternal(ntn, i), n);
     Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]);
     if (cexc.find(i) == cexc.end())
     {

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 622aa2a6a88b8a65627a25b93296861a4888d45d..4bea7b26bd0d22c49b9bf5cedd53c7d612a1ee0e 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -258,7 +258,7 @@ Node TermDbSygus::canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count)
   Trace("sygus-db-canon") << "  CanonizeBuiltin : compute for " << n << "\n";
   Node ret = n;
   // it is symbolic if it represents "any constant"
-  if (n.getKind() == APPLY_SELECTOR_TOTAL)
+  if (n.getKind() == APPLY_SELECTOR)
   {
     ret = getFreeVarInc(n[0].getType(), var_count, true);
   }
@@ -960,17 +960,23 @@ bool TermDbSygus::involvesDivByZero( Node n ) {
 }
 
 Node TermDbSygus::getAnchor( Node n ) {
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+  if (n.getKind() == APPLY_SELECTOR)
+  {
     return getAnchor( n[0] );
-  }else{
+  }
+  else
+  {
     return n;
   }
 }
 
 unsigned TermDbSygus::getAnchorDepth( Node n ) {
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+  if (n.getKind() == APPLY_SELECTOR)
+  {
     return 1+getAnchorDepth( n[0] );
-  }else{
+  }
+  else
+  {
     return 0;
   }
 }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9ff181b9ba1ae5c4e6b09e626ac53e3f1fad790b..b12acf9427b83f50647582fb27dd778cfa55e1bb 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -188,9 +188,8 @@ Node TermDb::getMatchOperator( Node n ) {
   //datatype operators may be parametric, always assume they are
   if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTER
       || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER
-      || k == SET_SINGLETON || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR
-      || k == APPLY_TESTER || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH
-      || k == STRING_LENGTH)
+      || k == SET_SINGLETON || k == APPLY_SELECTOR || k == APPLY_TESTER
+      || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH || k == STRING_LENGTH)
   {
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 69e205da10d6a331abb0dd8ddbc5a771a3b5f352..54dbcdd3cf26ff4f2b97fe44583b8dbd1970fca3 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -59,7 +59,7 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee)
   d_equalityEngine->addFunctionKind(kind::SELECT);
   // d_equalityEngine->addFunctionKind(kind::STORE);
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
+  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   d_equalityEngine->addFunctionKind(kind::SEQ_NTH);
   d_equalityEngine->addFunctionKind(kind::SEQ_NTH_TOTAL);

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 367bf557a501fa81d22cf11f47224d8c85cc8614..6b61ea1101fc4a876176427a6963862c82413eef 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -127,7 +127,7 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
 
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
-  if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL
+  if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR
       || n.getKind() == kind::SEQ_NTH_TOTAL || n.getKind() == kind::SEQ_NTH)
   {
     // selectors are always assignable (where we guarantee that they are not

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 604bb91dee34e0d943a048f0e6b505da7d0bf68c..6e8f5a774c7dab33d4ddf2e4cb27686ac8de115f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2856,7 +2856,6 @@ set(regress_2_tests
   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
   regress2/quantifiers/cee-event-wrong-sat.smt2
-  regress2/quantifiers/exp-trivially-dd3.smt2
   regress2/quantifiers/gn-wrong-091018.smt2
   regress2/quantifiers/issue3481-unsat1.smt2
   regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
@@ -3113,6 +3112,8 @@ set(regression_disabled_tests
   regress2/nl/nt-lemmas-bad.smt2
   # timeout after refactoring justification heuristic
   regress2/ho/SYO362^5.p
+  # timeout after refactoring selectors
+  regress2/quantifiers/exp-trivially-dd3.smt2
   # time out
   regress3/unifpi-solve-car_1.lus.sy
   # unknown (is sat)

diff --git a/test/regress/regress0/datatypes/data-nested-codata.smt2 b/test/regress/regress0/datatypes/data-nested-codata.smt2
index 6a571612358175d56a469b2a5b970a076f0ee9f1..d49f474273a367d84ee698717947817dbed42e88 100644 (file)
--- a/test/regress/regress0/datatypes/data-nested-codata.smt2
+++ b/test/regress/regress0/datatypes/data-nested-codata.smt2
@@ -1,4 +1,5 @@
-
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_DTLIA)
 (set-info :status sat)
 

diff --git a/test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2 b/test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2
index 2ea829b6ce402269b92d584f0cc433a463fc0642..a9694c6234b14baf384b8ebe22ea95208ade62aa 100644 (file)
--- a/test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2
+++ b/test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :incremental false)

diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
index 764c2dbedcf5cfeb3bf697a4d5739bb8a3fe5cbc..ece9532b41af01d89978c85ddc0034af9acb3ac9 100644 (file)
--- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
+++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress1/cee-bug0909-dd-scope.smt2 b/test/regress/regress1/cee-bug0909-dd-scope.smt2
index 6ce621a988d112b1eaae5f9d0fa45092c4aaab5a..5000dcb94700457f9afdf312199c0813572cfb51 100644 (file)
--- a/test/regress/regress1/cee-bug0909-dd-scope.smt2
+++ b/test/regress/regress1/cee-bug0909-dd-scope.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --ee-mode=distributed
-; COMMAND-LINE: --ee-mode=central
+; COMMAND-LINE: --ee-mode=distributed -q
+; COMMAND-LINE: --ee-mode=central -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress1/datatypes/non-simple-rec-param.smt2 b/test/regress/regress1/datatypes/non-simple-rec-param.smt2
index 8db92b0fdd16101d59c1c84ebb2d11bfd1b9e9c4..345a67d73dd48b177ef2d33c0b41df388bca1dcb 100644 (file)
--- a/test/regress/regress1/datatypes/non-simple-rec-param.smt2
+++ b/test/regress/regress1/datatypes/non-simple-rec-param.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dt-nested-rec
+; COMMAND-LINE: --dt-nested-rec -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress1/fmf/cons-sets-bounds.smt2 b/test/regress/regress1/fmf/cons-sets-bounds.smt2
index f0ff20de9804f5dfe118aab2023e99339e64f36e..c917d74d958575e938aedfa213911c218e0bd955 100644 (file)
--- a/test/regress/regress1/fmf/cons-sets-bounds.smt2
+++ b/test/regress/regress1/fmf/cons-sets-bounds.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-bound
+; COMMAND-LINE: --fmf-bound -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((list 0)) (((cons (head Int) (tail list)) (nil))))

diff --git a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
index 7241dab4b2b254e958b231fc626ed1bfab108483..9cafbfc6b646af2040806f8e9725c14b83aa8a2e 100644 (file)
--- a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
+++ b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress1/fmf/loopy_coda.smt2 b/test/regress/regress1/fmf/loopy_coda.smt2
index 2b91b8c7a24d21d97fbb076823839694320bf706..27323526114a8a54f2a38c90b01cb05202603fcc 100644 (file)
--- a/test/regress/regress1/fmf/loopy_coda.smt2
+++ b/test/regress/regress1/fmf/loopy_coda.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
index 2ed01adc619b125e1f20a52472e2b331b42cc6c4..432a3fdf641f308201801711608032e4473389be 100644 (file)
--- a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
+++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel
+; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil))))

diff --git a/test/regress/regress1/fmf/nun-0208-to.smt2 b/test/regress/regress1/fmf/nun-0208-to.smt2
index 32974ef41ecb2b04685c3ce2510b1d3fa7bbf7eb..f74b4b2430a05f9711e9cd5d7fee875a249efc4a 100644 (file)
--- a/test/regress/regress1/fmf/nun-0208-to.smt2
+++ b/test/regress/regress1/fmf/nun-0208-to.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-sort b__ 0)

diff --git a/test/regress/regress1/strings/issue1105.smt2 b/test/regress/regress1/strings/issue1105.smt2
index 59f6184035fecbfc2dce578d50d6c715e36dab9f..0a5513fec0a72d82bc9dc714dd7cdb431600973f 100644 (file)
--- a/test/regress/regress1/strings/issue1105.smt2
+++ b/test/regress/regress1/strings/issue1105.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)

diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
index 162ea0ad1f940720b242ecf45965b690dae6c076..b688d3fcf57e6bfa2940af596962ce3220b6a09e 100644 (file)
--- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2
+++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic UFDTLIRA)
 (set-option :fmf-bound true)

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 70ea318836f8987b99d626d7dd8e2cd1654dbc55..d057154fc165a16d13d134cfdf7cf079b67ba0c8 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3226,5 +3226,32 @@ TEST_F(TestApiBlackSolver, proj_issue422)
   slv.push(4);
 }
 
+TEST_F(TestApiBlackSolver, projIssue431)
+{
+  Solver slv;
+  slv.setOption("produce-abducts", "true");
+  Sort s2 = slv.mkBitVectorSort(22);
+  Sort s4 = slv.mkSetSort(s2);
+  Sort s5 = slv.getBooleanSort();
+  Sort s6 = slv.getRealSort();
+  Sort s7 = slv.mkFunctionSort({s6}, s5);
+  DatatypeDecl _dt46 = slv.mkDatatypeDecl("_dt46", {});
+  DatatypeConstructorDecl _cons64 = slv.mkDatatypeConstructorDecl("_cons64");
+  _cons64.addSelector("_sel62", s6);
+  _cons64.addSelector("_sel63", s4);
+  _dt46.addConstructor(_cons64);
+  Sort s14 = slv.mkDatatypeSorts({_dt46})[0];
+  Term t31 = slv.mkConst(s7, "_x100");
+  Term t47 = slv.mkConst(s14, "_x112");
+  Term sel =
+      t47.getSort().getDatatype().getConstructor("_cons64").getSelectorTerm(
+          "_sel62");
+  Term t274 = slv.mkTerm(APPLY_SELECTOR, sel, t47);
+  Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274});
+  slv.assertFormula({t488});
+  Term abduct;
+  slv.getAbduct(t488, abduct);
+}
+
 }  // namespace test
 }  // namespace cvc5