diff options
-rw-r--r-- | src/options/datatypes_options.toml | 9 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 29 |
2 files changed, 5 insertions, 33 deletions
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 82e833506..ac371efeb 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -32,15 +32,6 @@ header = "options/datatypes_options.h" help = "do binary splits for datatype constructor types" [[option]] - name = "dtRefIntro" - category = "regular" - long = "dt-ref-sk-intro" - type = "bool" - default = "false" - read_only = true - help = "introduce reference skolems for shorter explanations" - -[[option]] name = "cdtBisimilar" category = "regular" long = "cdt-bisimilar" diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index d202648f4..7fbe5bc68 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1306,15 +1306,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl; Node r; bool wrong = false; - Node use_s; - Node eq_exp; - if( options::dtRefIntro() ){ - eq_exp = d_true; - use_s = getTermSkolemFor( c ); - }else{ - eq_exp = c.eqNode( s[0] ); - use_s = s; - } + Node eq_exp = c.eqNode(s[0]); if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){ Node selector = s.getOperator(); size_t constructorIndex = utils::indexOf(c.getOperator()); @@ -1322,14 +1314,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { const DTypeConstructor& dtc = dt[constructorIndex]; int selectorIndex = dtc.getSelectorIndexInternal(selector); wrong = selectorIndex<0; - - //if( wrong ){ - // return; - //} r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); - if( options::dtRefIntro() ){ - use_s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), use_s ); - } } if( !r.isNull() ){ Node rr = Rewriter::rewrite( r ); @@ -1341,14 +1326,10 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { std::map< Node, Node > visited; rrs = removeUninterpretedConstants( rr, visited ); } - if( use_s!=rrs ){ - Node eq = use_s.eqNode( rrs ); - Node peq; - if( options::dtRefIntro() ){ - peq = d_true; - }else{ - peq = c.eqNode(s[0]); - } + if (s != rrs) + { + Node eq = s.eqNode(rrs); + Node peq = c.eqNode(s[0]); Trace("datatypes-infer") << "DtInfer : collapse sel"; //Trace("datatypes-infer") << ( wrong ? " wrong" : ""); Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl; |