diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-26 14:08:33 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-26 14:08:33 +0100 |
| commit | 365d6022b5742fc6910363e04e873b26e221bb05 (patch) | |
| tree | 0c4111ffbaa325646610bb598886216938ff10e4 /src/theory/theory_model.cpp | |
| parent | 7f43bd304b3d6bede36a777ee85ab68fab35d742 (diff) | |
Front-end support for get-value of sort cardinality, minor fixes for sygus solution reconstruction.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index c62a0dd4a..44e4193eb 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -88,11 +88,14 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ //for now, we only handle cardinalities for uninterpreted sorts if( tn.isSort() ){ if( d_rep_set.hasType( tn ) ){ + Debug("model-getvalue-debug") << "Get cardinality sort, #rep : " << d_rep_set.getNumRepresentatives( tn ) << std::endl; return Cardinality( d_rep_set.getNumRepresentatives( tn ) ); }else{ - return Cardinality( CardinalityUnknown() ); + Debug("model-getvalue-debug") << "Get cardinality sort, unconstrained, return 1." << std::endl; + return Cardinality( 1 ); } }else{ + Debug("model-getvalue-debug") << "Get cardinality other sort, unknown." << std::endl; return Cardinality( CardinalityUnknown() ); } } @@ -191,7 +194,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const ret = Rewriter::rewrite(ret); Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl; if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) { + Debug("model-getvalue-debug") << "get cardinality constraint " << ret[0].getType() << std::endl; ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).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 = NodeManager::currentNM()->mkConst(Rational(getCardinality(ret[0].getType().toType()).getFiniteCardinality())); } d_modelCache[n] = ret; return ret; |