From eeb78c833af50c49fd581704b03fd3c500360c3d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 21 Oct 2021 09:11:57 -0500 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 19 +- src/api/cpp/cvc5.h | 8 + src/api/cpp/cvc5_kind.h | 15 -- src/expr/cardinality_constraint.cpp | 7 + src/expr/cardinality_constraint.h | 8 +- src/parser/smt2/smt2.cpp | 18 +- src/printer/smt2/smt2_printer.cpp | 12 +- src/theory/term_registration_visitor.cpp | 32 ++- src/theory/theory_model.cpp | 16 +- src/theory/uf/cardinality_extension.cpp | 196 ++++++++++-------- src/theory/uf/cardinality_extension.h | 13 +- src/theory/uf/kinds | 31 ++- src/theory/uf/symmetry_breaker.cpp | 7 +- src/theory/uf/theory_uf.cpp | 3 +- src/theory/uf/theory_uf_type_rules.cpp | 78 +++---- src/theory/uf/theory_uf_type_rules.h | 10 +- .../fmf/issue5738-dt-interp-finite.smt2 | 2 +- test/unit/api/solver_black.cpp | 11 + 18 files changed, 271 insertions(+), 215 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index bb39ae86d..280b07bb2 100644 --- 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 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 /* 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 3e8a57d3d..7375b16de 100644 --- 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 706dea944..a01f84c3f 100644 --- 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& 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& 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 3841228fb..695f5d4a3 100644 --- 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()(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 a51ba545c..b2bfa836f 100644 --- 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, - 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 be7bdcb0f..19c3527f7 100644 --- 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& 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& 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 1da2a3c7b..ccb2ed2c6 100644 --- 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().getType(); + out << " "; + out << n.getConst().getUpperBound(); + out << ")"; + break; case kind::EMPTYSET: out << "(as emptyset "; toStreamType(out, n.getConst().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 0ce07c867..27e75fd83 100644 --- 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 8c1a17fe1..a5ec0867a 100644 --- 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(); Debug("model-getvalue-debug") - << "get cardinality constraint " << ret[0].getType() << std::endl; - ret = nm->mkConst(getCardinality(ret[0].getType()).getFiniteCardinality() - <= ret[1].getConst().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 3c71cdbb9..650ef1d70 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -17,6 +17,7 @@ #include +#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(); + TypeNode tn = cc.getType(); Assert(tn.isSort()); Assert(d_rep_model[tn]); - uint32_t nCard = - lit[1].getConst().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::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().getNumerator().getUnsignedInt(); + const CombinedCardinalityConstraint& cc = + lit.getOperator().getConst(); + 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(); + tn = cc.getType(); + } + else + { + tn = n.getType(); + } + if (!tn.isSort()) + { + return; + } + std::map::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 10e9ceb44..4b989a166 100644 --- 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& clique); /** cardinality */ context::CDO d_cardinality; - /** cardinality lemma term */ - Node d_cardinality_term; /** cardinality literals */ std::map 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 d_c_dec_strat; diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index e4b946105..0faa5c672 100644 --- 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 aa5d9d953..da75d0eea 100644 --- 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 ca7dc6a73..a76591b6e 100644 --- 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 e95c8963e..5b132fc27 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -18,6 +18,7 @@ #include #include +#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() > r) + const CardinalityConstraint& cc = n.getConst(); + 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().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(); + 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() > r) - { - throw TypeCheckingExceptionPrivate( - n, "Exceeded INT_MAX in combined cardinality constraint"); - } - if (n[0].getConst().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 d786f5f24..b9451a500 100644 --- 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 50373fde4..6f0fb84f2 100644 --- 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 c9527c2d4..8dcb0fde6 100644 --- 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; -- 2.30.2