diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/bounded_integers.cpp')
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index c6800b092..cfff64f15 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -19,6 +19,7 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/term_enumeration.h" @@ -737,14 +738,17 @@ Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){ return Node::null(); } } - const Datatype& dt = Datatype::datatypeOf( t.getOperator().toExpr() ); - unsigned index = Datatype::indexOf( t.getOperator().toExpr() ); + NodeManager* nm = NodeManager::currentNM(); + const DType& dt = datatypes::utils::datatypeOf(t.getOperator()); + unsigned index = datatypes::utils::indexOf(t.getOperator()); for( unsigned i=0; i<t.getNumChildren(); i++ ){ Node u; if( e.getKind()==kind::APPLY_CONSTRUCTOR ){ u = matchBoundVar( v, t[i], e[i] ); }else{ - Node se = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index].getSelectorInternal( e.getType().toType(), i ) ), e ); + Node se = nm->mkNode(APPLY_SELECTOR_TOTAL, + dt[index].getSelectorInternal(e.getType(), i), + e); u = matchBoundVar( v, t[i], se ); } if( !u.isNull() ){ |