diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-15 00:18:49 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-15 00:18:49 +0100 |
commit | 081351e87edeb52facba0d0abc2e933433480444 (patch) | |
tree | 8d0192c895c4103877e12673c0927d25e53a3db3 /src/theory/theory_model.h | |
parent | 94fe6a0d525bff3cdd4450b2abd04eb2cb044308 (diff) |
Ensure model construction for parametric sorts involving uninterpreted sorts respect cardinality bounds on when finite model finding is enabled.
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index fb2c3cd01..8ee4e843d 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -260,6 +260,9 @@ protected: /** is v an excluded codatatype value */ bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ); bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ); + /** involves usort */ + bool involvesUSort( TypeNode tn ); + bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ); public: TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} |