Make cardinality constraint a nullary operator (#7333)

This makes cardinality constraints nullary operators. This eliminates hacks for supporting these previously.

It also removes an unimplemented kind CARDINALITY_VALUE.

Notice that the parser and printer now do not use a common syntax for cardinality constraints, this will be resolved on followup PRs.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index bb39ae86d48f6dba9df5a0a9bf7f6790aedf5115..280b07bb2dafe14feab22b3e9036419776c6f826 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -41,6 +41,7 @@
 #include "base/modal_exception.h"
 #include "expr/array_store_all.h"
 #include "expr/ascription_type.h"
+#include "expr/cardinality_constraint.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/dtype_selector.h"
@@ -131,7 +132,6 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     /* UF ------------------------------------------------------------------ */
     {APPLY_UF, cvc5::Kind::APPLY_UF},
     {CARDINALITY_CONSTRAINT, cvc5::Kind::CARDINALITY_CONSTRAINT},
-    {CARDINALITY_VALUE, cvc5::Kind::CARDINALITY_VALUE},
     {HO_APPLY, cvc5::Kind::HO_APPLY},
     /* Arithmetic ---------------------------------------------------------- */
     {PLUS, cvc5::Kind::PLUS},
@@ -410,7 +410,6 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         /* UF -------------------------------------------------------------- */
         {cvc5::Kind::APPLY_UF, APPLY_UF},
         {cvc5::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT},
-        {cvc5::Kind::CARDINALITY_VALUE, CARDINALITY_VALUE},
         {cvc5::Kind::HO_APPLY, HO_APPLY},
         /* Arithmetic ------------------------------------------------------ */
         {cvc5::Kind::PLUS, PLUS},
@@ -6055,6 +6054,22 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC5_API_TRY_CATCH_END;
 }
 
+Term Solver::mkCardinalityConstraint(const Sort& sort, uint32_t ubound) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_SOLVER_CHECK_SORT(sort);
+  CVC5_API_ARG_CHECK_EXPECTED(sort.isUninterpretedSort(), sort)
+      << "an uninterpreted sort";
+  CVC5_API_ARG_CHECK_EXPECTED(ubound > 0, ubound) << "a value > 0";
+  //////// all checks before this line
+  Node cco =
+      d_nodeMgr->mkConst(cvc5::CardinalityConstraint(*sort.d_type, ubound));
+  Node cc = d_nodeMgr->mkNode(cvc5::Kind::CARDINALITY_CONSTRAINT, cco);
+  return Term(this, cc);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 /* Create constants                                                           */
 /* -------------------------------------------------------------------------- */
 

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 3e8a57d3d6877ba37a162584b99b203b420116f0..7375b16de1d635e168c9877380138f4d1da99e8d 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3597,6 +3597,14 @@ class CVC5_EXPORT Solver
    */
   Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const;
 
+  /**
+   * Create a cardinality constraint for an uninterpreted sort.
+   * @param sort the sort the cardinality constraint is for
+   * @param val the upper bound on the cardinality of the sort
+   * @return the cardinality constraint
+   */
+  Term mkCardinalityConstraint(const Sort& sort, uint32_t ubound) const;
+
   /* .................................................................... */
   /* Create Variables                                                     */
   /* .................................................................... */

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 706dea944b385c4c46e535f0a624f9ecde71b54b..a01f84c3fef0f29b23bc1ca6e0467ef0a4bbf34d 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -331,22 +331,7 @@ enum Kind : int32_t
    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
    */
   CARDINALITY_CONSTRAINT,
-  /**
-   * Cardinality value for uninterpreted sort S.
-   * An operator that returns an integer indicating the value of the cardinality
-   * of sort S.
-   *
-   * Parameters:
-   *   - 1: Term of sort S
-   *
-   * Create with:
-   *   - `Solver::mkTerm(Kind kind, const Term& child1) const`
-   *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
-   */
-  CARDINALITY_VALUE,
 #if 0
-  /* Combined cardinality constraint.  */
-  COMBINED_CARDINALITY_CONSTRAINT,
   /* Partial uninterpreted function application.  */
   PARTIAL_APPLY_UF,
 #endif

diff --git a/src/expr/cardinality_constraint.cpp b/src/expr/cardinality_constraint.cpp
index 3841228fb5dd55421888b207eef10cfd29365ddb..695f5d4a3bd1a9035a0dace515b68e38e5d1f545 100644 (file)
--- a/src/expr/cardinality_constraint.cpp
+++ b/src/expr/cardinality_constraint.cpp
@@ -56,6 +56,13 @@ std::ostream& operator<<(std::ostream& out, const CardinalityConstraint& cc)
              << ')';
 }
 
+size_t CardinalityConstraintHashFunction::operator()(
+    const CardinalityConstraint& cc) const
+{
+  return std::hash<TypeNode>()(cc.getType())
+         * IntegerHashFunction()(cc.getUpperBound());
+}
+
 CombinedCardinalityConstraint::CombinedCardinalityConstraint(const Integer& ub)
     : d_ubound(ub)
 {

diff --git a/src/expr/cardinality_constraint.h b/src/expr/cardinality_constraint.h
index a51ba545ca5289475008c8799ddd1a618b35bb3c..b2bfa836f18ad5938f295a8c1c86c2ef28a2adce 100644 (file)
--- a/src/expr/cardinality_constraint.h
+++ b/src/expr/cardinality_constraint.h
@@ -60,10 +60,10 @@ class CardinalityConstraint
 
 std::ostream& operator<<(std::ostream& out, const CardinalityConstraint& cc);
 
-using CardinalityConstraintHashFunction = PairHashFunction<TypeNode,
-                                                           Integer,
-                                                           std::hash<TypeNode>,
-                                                           IntegerHashFunction>;
+struct CardinalityConstraintHashFunction
+{
+  size_t operator()(const CardinalityConstraint& cc) const;
+};
 
 /**
  * A combined cardinality constraint, handled in the cardinality extension of

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index be7bdcb0fa409dde8d773c666235026e75b8c40f..19c3527f77c8cc61ddbaba75acda49a13b635f34 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -516,7 +516,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
     {
       addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card");
-      addOperator(api::CARDINALITY_VALUE, "fmf.card.val");
     }
   }
 
@@ -956,6 +955,8 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     {
       // a builtin operator, convert to kind
       kind = getOperatorKind(p.d_name);
+      Debug("parser") << "Got builtin kind " << kind << " for name"
+                      << std::endl;
     }
     else
     {
@@ -1128,6 +1129,21 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       Debug("parser") << "applyParseOp: return singleton " << ret << std::endl;
       return ret;
     }
+    else if (kind == api::CARDINALITY_CONSTRAINT)
+    {
+      if (args.size() != 2)
+      {
+        parseError("Incorrect arguments for cardinality constraint");
+      }
+      api::Sort sort = args[0].getSort();
+      if (!sort.isUninterpretedSort())
+      {
+        parseError("Expected uninterpreted sort for cardinality constraint");
+      }
+      uint64_t ubound = args[1].getUInt32Value();
+      api::Term ret = d_solver->mkCardinalityConstraint(sort, ubound);
+      return ret;
+    }
     api::Term ret = d_solver->mkTerm(kind, args);
     Debug("parser") << "applyParseOp: return default builtin " << ret
                     << std::endl;

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1da2a3c7be9262bf79f8d03b3db760405ccc6b2b..ccb2ed2c6a737a631399d44634e79edcdfb4a86d 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -24,6 +24,7 @@
 #include "api/cpp/cvc5.h"
 #include "expr/array_store_all.h"
 #include "expr/ascription_type.h"
+#include "expr/cardinality_constraint.h"
 #include "expr/datatype_index.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
@@ -331,7 +332,13 @@ void Smt2Printer::toStream(std::ostream& out,
       out << ss.str();
       break;
     }
-
+    case kind::CARDINALITY_CONSTRAINT:
+      out << "(_ fmf.card ";
+      out << n.getConst<CardinalityConstraint>().getType();
+      out << " ";
+      out << n.getConst<CardinalityConstraint>().getUpperBound();
+      out << ")";
+      break;
     case kind::EMPTYSET:
       out << "(as emptyset ";
       toStreamType(out, n.getConst<EmptySet>().getType());
@@ -659,9 +666,6 @@ void Smt2Printer::toStream(std::ostream& out,
     break;
   }
 
-  case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
-  case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
-
     // bv theory
   case kind::BITVECTOR_CONCAT:
   case kind::BITVECTOR_AND:

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 0ce07c867ee3491239956588ff88eaa13a2a4cee..27e75fd83bd637aef9c2fca84f4f9093f6ccf1a6 100644 (file)
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -92,7 +92,6 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
        || parent.getKind() == kind::SEP_STAR
        || parent.getKind() == kind::SEP_WAND
        || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
-       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
        )
       && current != parent)
   {
@@ -193,25 +192,19 @@ void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
         << "): adding " << id << std::endl;
     // This should never throw an exception, since theories should be
     // guaranteed to be initialized.
-    // These checks don't work with finite model finding, because it
-    // uses Rational constants to represent cardinality constraints,
-    // even though arithmetic isn't actually involved.
-    if (!options::finiteModelFind())
+    if (!te->isTheoryEnabled(id))
     {
-      if (!te->isTheoryEnabled(id))
-      {
-        const LogicInfo& l = te->getLogicInfo();
-        LogicInfo newLogicInfo = l.getUnlockedCopy();
-        newLogicInfo.enableTheory(id);
-        newLogicInfo.lock();
-        std::stringstream ss;
-        ss << "The logic was specified as " << l.getLogicString()
-           << ", which doesn't include " << id
-           << ", but found a term in that theory." << std::endl
-           << "You might want to extend your logic to "
-           << newLogicInfo.getLogicString() << std::endl;
-        throw LogicException(ss.str());
-      }
+      const LogicInfo& l = te->getLogicInfo();
+      LogicInfo newLogicInfo = l.getUnlockedCopy();
+      newLogicInfo.enableTheory(id);
+      newLogicInfo.lock();
+      std::stringstream ss;
+      ss << "The logic was specified as " << l.getLogicString()
+         << ", which doesn't include " << id
+         << ", but found a term in that theory." << std::endl
+         << "You might want to extend your logic to "
+         << newLogicInfo.getLogicString() << std::endl;
+      throw LogicException(ss.str());
     }
   }
   // call the theory's preRegisterTerm method
@@ -249,7 +242,6 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
        || parent.getKind() == kind::SEP_STAR
        || parent.getKind() == kind::SEP_WAND
        || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
-       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
        )
       && current != parent)
   {

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 8c1a17fe1acba20fa70615824f249824ed506083..a5ec0867ad7647b4f03b3df8b324e3bb3c2e0ea5 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -14,6 +14,7 @@
  */
 #include "theory/theory_model.h"
 
+#include "expr/cardinality_constraint.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
@@ -253,17 +254,12 @@ Node TheoryModel::getModelValue(TNode n) const
     // special cases
     if (ret.getKind() == kind::CARDINALITY_CONSTRAINT)
     {
+      const CardinalityConstraint& cc =
+          ret.getOperator().getConst<CardinalityConstraint>();
       Debug("model-getvalue-debug")
-          << "get cardinality constraint " << ret[0].getType() << std::endl;
-      ret = nm->mkConst(getCardinality(ret[0].getType()).getFiniteCardinality()
-                        <= ret[1].getConst<Rational>().getNumerator());
-    }
-    else if (ret.getKind() == kind::CARDINALITY_VALUE)
-    {
-      Debug("model-getvalue-debug")
-          << "get cardinality value " << ret[0].getType() << std::endl;
-      ret = nm->mkConst(
-          Rational(getCardinality(ret[0].getType()).getFiniteCardinality()));
+          << "get cardinality constraint " << cc.getType() << std::endl;
+      ret = nm->mkConst(getCardinality(cc.getType()).getFiniteCardinality()
+                        <= cc.getUpperBound());
     }
     // if the value was constant, we return it. If it was non-constant,
     // we only return it if we an evaluated kind. This can occur if the

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 3c71cdbb9bcb37b5913669c7b33b80af463b51d8..650ef1d70cd5b3234d699aeae13787c5ee47dc4f 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -17,6 +17,7 @@
 
 #include <sstream>
 
+#include "expr/cardinality_constraint.h"
 #include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
@@ -447,26 +448,28 @@ void Region::debugPrint( const char* c, bool incClique ) {
 }
 
 SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy(
-    Env& env, Node t, Valuation valuation)
-    : DecisionStrategyFmf(env, valuation), d_cardinality_term(t)
+    Env& env, TypeNode type, Valuation valuation)
+    : DecisionStrategyFmf(env, valuation), d_type(type)
 {
 }
+
 Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i)
 {
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(
-      CARDINALITY_CONSTRAINT, d_cardinality_term, nm->mkConst(Rational(i + 1)));
+  Node cco = nm->mkConst(CardinalityConstraint(d_type, Integer(i + 1)));
+  return nm->mkNode(CARDINALITY_CONSTRAINT, cco);
 }
+
 std::string SortModel::CardinalityDecisionStrategy::identify() const
 {
   return std::string("uf_card");
 }
 
-SortModel::SortModel(Node n,
+SortModel::SortModel(TypeNode tn,
                      TheoryState& state,
                      TheoryInferenceManager& im,
                      CardinalityExtension* thss)
-    : d_type(n.getType()),
+    : d_type(tn),
       d_state(state),
       d_im(im),
       d_thss(thss),
@@ -481,7 +484,6 @@ SortModel::SortModel(Node n,
       d_initialized(thss->userContext(), false),
       d_c_dec_strat(nullptr)
 {
-  d_cardinality_term = n;
 
   if (options::ufssMode() == options::UfssMode::FULL)
   {
@@ -489,7 +491,7 @@ SortModel::SortModel(Node n,
     // We are guaranteed that the decision manager is ready since we
     // construct this module during TheoryUF::finishInit.
     d_c_dec_strat.reset(new CardinalityDecisionStrategy(
-        thss->d_env, n, thss->getTheory()->getValuation()));
+        thss->d_env, d_type, thss->getTheory()->getValuation()));
   }
 }
 
@@ -1342,72 +1344,80 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
   if (options::ufssMode() == options::UfssMode::FULL)
   {
     if( lit.getKind()==CARDINALITY_CONSTRAINT ){
-      TypeNode tn = lit[0].getType();
+      const CardinalityConstraint& cc =
+          lit.getOperator().getConst<CardinalityConstraint>();
+      TypeNode tn = cc.getType();
       Assert(tn.isSort());
       Assert(d_rep_model[tn]);
-      uint32_t nCard =
-          lit[1].getConst<Rational>().getNumerator().getUnsignedInt();
-      Node ct = d_rep_model[tn]->getCardinalityTerm();
-      Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
-      if( lit[0]==ct ){
-        if( options::ufssFairnessMonotone() ){
-          SortInference* si = d_state.getSortInference();
-          Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
-          if( tn!=d_tn_mono_master ){
-            std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
-            if( it==d_tn_mono_slave.end() ){
-              bool isMonotonic;
-              if (si != nullptr)
+      uint32_t nCard = cc.getUpperBound().getUnsignedInt();
+      Trace("uf-ss-debug") << "...check cardinality constraint : " << tn
+                           << std::endl;
+      if (options::ufssFairnessMonotone())
+      {
+        SortInference* si = d_state.getSortInference();
+        Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
+        if (tn != d_tn_mono_master)
+        {
+          std::map<TypeNode, bool>::iterator it = d_tn_mono_slave.find(tn);
+          if (it == d_tn_mono_slave.end())
+          {
+            bool isMonotonic;
+            if (si != nullptr)
+            {
+              isMonotonic = si->isMonotonic(tn);
+            }
+            else
+            {
+              // if ground, everything is monotonic
+              isMonotonic = true;
+            }
+            if (isMonotonic)
+            {
+              if (d_tn_mono_master.isNull())
               {
-                isMonotonic = si->isMonotonic(tn);
-              }else{
-                //if ground, everything is monotonic
-                isMonotonic = true;
+                Trace("uf-ss-com-card-debug")
+                    << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
+                d_tn_mono_master = tn;
               }
-              if( isMonotonic ){
-                if( d_tn_mono_master.isNull() ){
-                  Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
-                  d_tn_mono_master = tn;
-                }else{
-                  Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
-                  d_tn_mono_slave[tn] = true;
-                }
-              }else{
-                Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl;
-                d_tn_mono_slave[tn] = false;
+              else
+              {
+                Trace("uf-ss-com-card-debug")
+                    << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
+                d_tn_mono_slave[tn] = true;
               }
             }
-          }
-          //set the minimum positive cardinality for master if necessary
-          if( polarity && tn==d_tn_mono_master ){
-            Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl;
-            if (!d_min_pos_tn_master_card_set.get()
-                || nCard < d_min_pos_tn_master_card.get())
+            else
             {
-              d_min_pos_tn_master_card_set.set(true);
-              d_min_pos_tn_master_card.set( nCard );
+              Trace("uf-ss-com-card-debug")
+                  << "uf-ss-fair-monotone: Set non-monotonic : " << tn
+                  << std::endl;
+              d_tn_mono_slave[tn] = false;
             }
           }
         }
-        Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
-        d_rep_model[tn]->assertCardinality(nCard, polarity);
-        //check if combined cardinality is violated
-        checkCombinedCardinality();
-      }else{
-        //otherwise, make equal via lemma
-        if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
-          Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
-          eqv_lit = lit.eqNode( eqv_lit );
-          Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
-          d_im.lemma(eqv_lit, InferenceId::UF_CARD_EQUIV);
-          d_card_assertions_eqv_lemma[lit] = true;
+        // set the minimum positive cardinality for master if necessary
+        if (polarity && tn == d_tn_mono_master)
+        {
+          Trace("uf-ss-com-card-debug")
+              << "...set min positive cardinality" << std::endl;
+          if (!d_min_pos_tn_master_card_set.get()
+              || nCard < d_min_pos_tn_master_card.get())
+          {
+            d_min_pos_tn_master_card_set.set(true);
+            d_min_pos_tn_master_card.set(nCard);
+          }
         }
       }
+      Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
+      d_rep_model[tn]->assertCardinality(nCard, polarity);
+      // check if combined cardinality is violated
+      checkCombinedCardinality();
     }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
       if( polarity ){
         //safe to assume int here
-        uint32_t nCard =
-            lit[0].getConst<Rational>().getNumerator().getUnsignedInt();
+        const CombinedCardinalityConstraint& cc =
+            lit.getOperator().getConst<CombinedCardinalityConstraint>();
+        uint32_t nCard = cc.getUpperBound().getUnsignedInt();
         if (!d_min_pos_com_card_set.get() || nCard < d_min_pos_com_card.get())
         {
           d_min_pos_com_card_set.set(true);
@@ -1570,7 +1580,8 @@ Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
     unsigned i)
 {
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(COMBINED_CARDINALITY_CONSTRAINT, nm->mkConst(Rational(i)));
+  Node cco = nm->mkConst(CombinedCardinalityConstraint(Integer(i)));
+  return nm->mkNode(COMBINED_CARDINALITY_CONSTRAINT, cco);
 }
 
 std::string
@@ -1581,31 +1592,52 @@ CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
 
 void CardinalityExtension::preRegisterTerm(TNode n)
 {
-  if (options::ufssMode() == options::UfssMode::FULL)
+  if (options::ufssMode() != options::UfssMode::FULL)
   {
-    //initialize combined cardinality
-    initializeCombinedCardinality();
-
-    Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
-    //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
-    TypeNode tn = n.getType();
-    std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
-    if( it==d_rep_model.end() ){
-      SortModel* rm = NULL;
-      if( tn.isSort() ){
-        Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
-        rm = new SortModel(n, d_state, d_im, this);
-      }
-      if( rm ){
-        rm->initialize();
-        d_rep_model[tn] = rm;
-        //d_rep_model_init[tn] = true;
-      }
-    }else{
-      //ensure sort model is initialized
-      it->second->initialize();
+    return;
+  }
+  // initialize combined cardinality
+  initializeCombinedCardinality();
+
+  Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
+  // shouldn't have to preregister this type (it may be that there are no
+  // quantifiers over tn)
+  TypeNode tn;
+  if (n.getKind() == CARDINALITY_CONSTRAINT)
+  {
+    const CardinalityConstraint& cc =
+        n.getOperator().getConst<CardinalityConstraint>();
+    tn = cc.getType();
+  }
+  else
+  {
+    tn = n.getType();
+  }
+  if (!tn.isSort())
+  {
+    return;
+  }
+  std::map<TypeNode, SortModel*>::iterator it = d_rep_model.find(tn);
+  if (it == d_rep_model.end())
+  {
+    SortModel* rm = nullptr;
+    if (tn.isSort())
+    {
+      Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
+      rm = new SortModel(tn, d_state, d_im, this);
+    }
+    if (rm)
+    {
+      rm->initialize();
+      d_rep_model[tn] = rm;
+      // d_rep_model_init[tn] = true;
     }
   }
+  else
+  {
+    // ensure sort model is initialized
+    it->second->initialize();
+  }
 }
 
 SortModel* CardinalityExtension::getSortModel(Node n)

diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 10e9ceb4496df2c067ab4d62d32c7723f5c3c936..4b989a1669df0279840dfa33253b4d9c36646d72 100644 (file)
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -265,8 +265,6 @@ class CardinalityExtension : protected EnvObj
     void addCliqueLemma(std::vector<Node>& clique);
     /** cardinality */
     context::CDO<uint32_t> d_cardinality;
-    /** cardinality lemma term */
-    Node d_cardinality_term;
     /** cardinality literals */
     std::map<uint32_t, Node> d_cardinality_literal;
     /** whether a positive cardinality constraint has been asserted */
@@ -283,7 +281,7 @@ class CardinalityExtension : protected EnvObj
     void simpleCheckCardinality();
 
    public:
-    SortModel(Node n,
+    SortModel(TypeNode tn,
               TheoryState& state,
               TheoryInferenceManager& im,
               CardinalityExtension* thss);
@@ -309,7 +307,7 @@ class CardinalityExtension : protected EnvObj
     /** has cardinality */
     bool hasCardinalityAsserted() const { return d_hasCard; }
     /** get cardinality term */
-    Node getCardinalityTerm() const { return d_cardinality_term; }
+    TypeNode getType() const { return d_type; }
     /** get cardinality literal */
     Node getCardinalityLiteral(uint32_t c);
     /** get maximum negative cardinality */
@@ -341,15 +339,14 @@ class CardinalityExtension : protected EnvObj
     class CardinalityDecisionStrategy : public DecisionStrategyFmf
     {
      public:
-      CardinalityDecisionStrategy(Env& env, Node t, Valuation valuation);
+      CardinalityDecisionStrategy(Env& env, TypeNode type, Valuation valuation);
       /** make literal (the i^th combined cardinality literal) */
       Node mkLiteral(unsigned i) override;
       /** identify */
       std::string identify() const override;
-
      private:
-      /** the cardinality term */
-      Node d_cardinality_term;
+      /** The type we are considering cardinality constraints for */
+      TypeNode d_type;
     };
     /** cardinality decision strategy */
     std::unique_ptr<CardinalityDecisionStrategy> d_c_dec_strat;

diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index e4b946105eaa1efc70df97f828d4f26aee87a474..0faa5c67203bd02aedde9033d659bc43e8e14989 100644 (file)
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -17,19 +17,32 @@ typerule APPLY_UF ::cvc5::theory::uf::UfTypeRule
 
 variable BOOLEAN_TERM_VARIABLE "Boolean term variable"
 
-operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S"
-typerule CARDINALITY_CONSTRAINT ::cvc5::theory::uf::CardinalityConstraintTypeRule
-
-operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature"
-typerule COMBINED_CARDINALITY_CONSTRAINT ::cvc5::theory::uf::CombinedCardinalityConstraintTypeRule
-
 parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application"
 typerule PARTIAL_APPLY_UF ::cvc5::theory::uf::PartialTypeRule
 
-operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
-typerule CARDINALITY_VALUE ::cvc5::theory::uf::CardinalityValueTypeRule
-
 operator HO_APPLY 2 "higher-order (partial) function application"
 typerule HO_APPLY ::cvc5::theory::uf::HoApplyTypeRule
 
+constant CARDINALITY_CONSTRAINT_OP \
+  class \
+  CardinalityConstraint \
+  ::cvc5::CardinalityConstraintHashFunction \
+  "expr/cardinality_constraint.h" \
+  "the empty set constant; payload is an instance of the cvc5::CardinalityConstraint class"
+parameterized CARDINALITY_CONSTRAINT CARDINALITY_CONSTRAINT_OP 0 "a fixed upper bound on the cardinality of an uninterpreted sort"
+
+typerule CARDINALITY_CONSTRAINT_OP ::cvc5::theory::uf::CardinalityConstraintOpTypeRule
+typerule CARDINALITY_CONSTRAINT ::cvc5::theory::uf::CardinalityConstraintTypeRule
+
+constant COMBINED_CARDINALITY_CONSTRAINT_OP \
+  class \
+  CombinedCardinalityConstraint \
+  ::cvc5::CombinedCardinalityConstraintHashFunction \
+  "expr/cardinality_constraint.h" \
+  "the empty set constant; payload is an instance of the cvc5::CombinedCardinalityConstraint class"
+parameterized COMBINED_CARDINALITY_CONSTRAINT COMBINED_CARDINALITY_CONSTRAINT_OP 0 "a fixed upper bound on the sum of cardinalities of uninterpreted sorts"
+
+typerule COMBINED_CARDINALITY_CONSTRAINT_OP ::cvc5::theory::uf::CombinedCardinalityConstraintOpTypeRule
+typerule COMBINED_CARDINALITY_CONSTRAINT ::cvc5::theory::uf::CombinedCardinalityConstraintTypeRule
+
 endtheory

diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index aa5d9d953d430ae53b08905dcea2d6eb868852a2..da75d0eeaef9d08e62b64cc4a2d67a2ae9d603d6 100644 (file)
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -79,12 +79,11 @@ bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) {
   }
 
   if(t.getNumChildren() == 0) {
-    if(t.isConst()) {
-      Assert(n.isConst());
-      Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl;
+    if (!t.isVar())
+    {
+      Debug("ufsymm:match") << "UFSYMM non-variables, failing match" << endl;
       return false;
     }
-    Assert(t.isVar() && n.isVar());
     t = find(t);
     n = find(n);
     Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl;

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ca7dc6a73adc5e1ace1952d319a7ccf1b2a7f52a..a76591b6ed46c8e810d2c2f52dc83ebc063d991a 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -251,7 +251,8 @@ void TheoryUF::preRegisterTerm(TNode node)
 {
   Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
 
-  if (d_thss != NULL) {
+  if (d_thss != nullptr)
+  {
     d_thss->preRegisterTerm(node);
   }
 

diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp
index e95c8963e72c52ee37bd7cda38b7ea40e22b6c80..5b132fc2772bf221929eea5a4d69d2d17ab09673 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.cpp
+++ b/src/theory/uf/theory_uf_type_rules.cpp
@@ -18,6 +18,7 @@
 #include <climits>
 #include <sstream>
 
+#include "expr/cardinality_constraint.h"
 #include "util/rational.h"
 
 namespace cvc5 {
@@ -63,33 +64,19 @@ TypeNode UfTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check)
   return fType.getRangeType();
 }
 
-TypeNode CardinalityConstraintTypeRule::computeType(NodeManager* nodeManager,
-                                                    TNode n,
-                                                    bool check)
+TypeNode CardinalityConstraintOpTypeRule::computeType(NodeManager* nodeManager,
+                                                      TNode n,
+                                                      bool check)
 {
   if (check)
   {
-    // don't care what it is, but it should be well-typed
-    n[0].getType(check);
-
-    TypeNode valType = n[1].getType(check);
-    if (valType != nodeManager->integerType())
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "cardinality constraint must be integer");
-    }
-    if (n[1].getKind() != kind::CONST_RATIONAL)
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "cardinality constraint must be a constant");
-    }
-    cvc5::Rational r(INT_MAX);
-    if (n[1].getConst<Rational>() > r)
+    const CardinalityConstraint& cc = n.getConst<CardinalityConstraint>();
+    if (!cc.getType().isSort())
     {
       throw TypeCheckingExceptionPrivate(
-          n, "Exceeded INT_MAX in cardinality constraint");
+          n, "cardinality constraint must apply to uninterpreted sort");
     }
-    if (n[1].getConst<Rational>().getNumerator().sgn() != 1)
+    if (cc.getUpperBound().sgn() != 1)
     {
       throw TypeCheckingExceptionPrivate(
           n, "cardinality constraint must be positive");
@@ -98,37 +85,35 @@ TypeNode CardinalityConstraintTypeRule::computeType(NodeManager* nodeManager,
   return nodeManager->booleanType();
 }
 
-TypeNode CombinedCardinalityConstraintTypeRule::computeType(
+TypeNode CardinalityConstraintTypeRule::computeType(NodeManager* nodeManager,
+                                                    TNode n,
+                                                    bool check)
+{
+  return nodeManager->booleanType();
+}
+
+TypeNode CombinedCardinalityConstraintOpTypeRule::computeType(
     NodeManager* nodeManager, TNode n, bool check)
 {
   if (check)
   {
-    TypeNode valType = n[0].getType(check);
-    if (valType != nodeManager->integerType())
+    const CombinedCardinalityConstraint& cc =
+        n.getConst<CombinedCardinalityConstraint>();
+    if (cc.getUpperBound().sgn() != 1)
     {
       throw TypeCheckingExceptionPrivate(
-          n, "combined cardinality constraint must be integer");
-    }
-    if (n[0].getKind() != kind::CONST_RATIONAL)
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "combined cardinality constraint must be a constant");
-    }
-    cvc5::Rational r(INT_MAX);
-    if (n[0].getConst<Rational>() > r)
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "Exceeded INT_MAX in combined cardinality constraint");
-    }
-    if (n[0].getConst<Rational>().getNumerator().sgn() == -1)
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "combined cardinality constraint must be non-negative");
+          n, "combined cardinality constraint must be positive");
     }
   }
   return nodeManager->booleanType();
 }
 
+TypeNode CombinedCardinalityConstraintTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  return nodeManager->booleanType();
+}
+
 TypeNode PartialTypeRule::computeType(NodeManager* nodeManager,
                                       TNode n,
                                       bool check)
@@ -136,17 +121,6 @@ TypeNode PartialTypeRule::computeType(NodeManager* nodeManager,
   return n.getOperator().getType().getRangeType();
 }
 
-TypeNode CardinalityValueTypeRule::computeType(NodeManager* nodeManager,
-                                               TNode n,
-                                               bool check)
-{
-  if (check)
-  {
-    n[0].getType(check);
-  }
-  return nodeManager->integerType();
-}
-
 TypeNode HoApplyTypeRule::computeType(NodeManager* nodeManager,
                                       TNode n,
                                       bool check)

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index d786f5f24025dcc83e7fe9ec173c54817617bc02..b9451a50094bfc4dc4044f9773beaf9748b36b36 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -37,19 +37,25 @@ class CardinalityConstraintTypeRule
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+class CardinalityConstraintOpTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
+
 class CombinedCardinalityConstraintTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class PartialTypeRule
+class CombinedCardinalityConstraintOpTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class CardinalityValueTypeRule
+class PartialTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);

diff --git a/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2 b/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2
index 50373fde47df1d6acb9eca09215907b45608835d..6f0fb84f2b50bc0edd83558cb52e7e09d1309d09 100644 (file)
--- a/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2
+++ b/test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2
@@ -1,4 +1,4 @@
-(set-logic UFLIA)
+(set-logic UFDTLIA)
 (set-info :status sat)
 (set-option :finite-model-find true)
 (declare-sort a 0)

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index c9527c2d4dbd0908abddd9af2e9ca61f6270354e..8dcb0fde606743a838f8fd7fff38633633114984 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -410,6 +410,17 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint)
   ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, mkCardinalityConstraint)
+{
+  Sort su = d_solver.mkUninterpretedSort("u");
+  Sort si = d_solver.getIntegerSort();
+  ASSERT_NO_THROW(d_solver.mkCardinalityConstraint(su, 3));
+  ASSERT_THROW(d_solver.mkCardinalityConstraint(si, 3), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkCardinalityConstraint(su, 0), CVC5ApiException);
+  Solver slv;
+  ASSERT_THROW(slv.mkCardinalityConstraint(su, 3), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, mkEmptySet)
 {
   Solver slv;