diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-21 09:11:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-21 14:11:57 +0000 |
| commit | eeb78c833af50c49fd581704b03fd3c500360c3d (patch) | |
| tree | 4e546205fb5d7495fd45c6fa5e76adc279abaecd /src/theory/theory_model.cpp | |
| parent | 0291f941d4a2bae49a80c3db4afe626b55636fdf (diff) | |
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.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 16 |
1 files changed, 6 insertions, 10 deletions
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<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 |