ada/cvc5
0
0
Fork 0
mirror of https://github.com/AdaCore/cvc5.git synced 2026-02-12 12:32:16 -08:00
Code Issues Packages Projects Releases Wiki Activity

Make cardinality constraint a nullary operator (#7333)

Browse Source 
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.
This commit is contained in:
Andrew Reynolds
2021-10-21 09:11:57 -05:00
committed by GitHub
parent 0291f941d4
commit eeb78c833a
18 changed files with 270 additions and 214 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
src/api/cpp/cvc5.cpp
View File

@@ -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 */
/* -------------------------------------------------------------------------- */

8
src/api/cpp/cvc5.h
View File

@@ -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 */
/* .................................................................... */

15
src/api/cpp/cvc5_kind.h
View File

@@ -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

7
src/expr/cardinality_constraint.cpp
View File

@@ -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)
{

8
src/expr/cardinality_constraint.h
View File

@@ -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

18
src/parser/smt2/smt2.cpp
View File

@@ -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;

12
src/printer/smt2/smt2_printer.cpp
View File

@@ -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:

32
src/theory/term_registration_visitor.cpp
View File

@@ -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)
{

16
src/theory/theory_model.cpp
View File

@@ -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

194
src/theory/uf/cardinality_extension.cpp
View File

@@ -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,30 +1592,51 @@ 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();
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 = 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();
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();
}
}

13
src/theory/uf/cardinality_extension.h
View File

@@ -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;

31
src/theory/uf/kinds
View File

@@ -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

7
src/theory/uf/symmetry_breaker.cpp
View File

@@ -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;

3
src/theory/uf/theory_uf.cpp
View File

@@ -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);
}

78
src/theory/uf/theory_uf_type_rules.cpp
View File

@@ -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())
const CardinalityConstraint& cc = n.getConst<CardinalityConstraint>();
if (!cc.getType().isSort())
{
throw TypeCheckingExceptionPrivate(
n, "cardinality constraint must be integer");
n, "cardinality constraint must apply to uninterpreted sort");
}
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)
{
throw TypeCheckingExceptionPrivate(
n, "Exceeded INT_MAX in cardinality constraint");
}
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)

10
src/theory/uf/theory_uf_type_rules.h
View File

@@ -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);

2
test/regress/regress1/fmf/issue5738-dt-interp-finite.smt2
View File

@@ -1,4 +1,4 @@
(set-logic UFLIA)
(set-logic UFDTLIA)
(set-info :status sat)
(set-option :finite-model-find true)
(declare-sort a 0)

11
test/unit/api/solver_black.cpp
View File

@@ -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;