diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2c9430876..bfeacf044 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1481,6 +1481,19 @@ bool TermDb::containsVtsInfinity( Node n, bool isFree ) { return containsTerms( n, t ); } +Node TermDb::mkNodeType( Node n, TypeNode tn ) { + TypeNode ntn = n.getType(); + Assert( ntn.isComparableTo( tn ) ); + if( ntn.isSubtypeOf( tn ) ){ + return n; + }else{ + if( tn.isInteger() ){ + return NodeManager::currentNM()->mkNode( TO_INTEGER, n ); + } + return Node::null(); + } +} + bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) { if( n==t ){ return true; |