From: Andrew Reynolds Date: Tue, 21 Aug 2018 00:22:21 +0000 (-0500) Subject: More unused code elimination (#2339) X-Git-Tag: cvc5-1.0.0~4754 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03abb94451a8bc2fb59b5b2fc95c931715575dc0;p=cvc5.git More unused code elimination (#2339) --- diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 2394a1b5d..67829e033 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -40,15 +40,6 @@ header = "options/datatypes_options.h" read_only = true help = "introduce reference skolems for shorter explanations" -[[option]] - name = "dtUseTesters" - category = "regular" - long = "dt-use-testers" - type = "bool" - default = "true" - read_only = true - help = "do not preprocess away tester predicates" - [[option]] name = "cdtBisimilar" category = "regular" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 5f6638dce..6e1c7f6b6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -224,15 +224,6 @@ header = "options/quantifiers_options.h" read_only = true help = "infer equalities for trigger terms based on solving arithmetic equalities" -[[option]] - name = "inferArithTriggerEqExp" - category = "regular" - long = "infer-arith-trigger-eq-exp" - type = "bool" - default = "false" - read_only = true - help = "record explanations for inferArithTriggerEq" - [[option]] name = "strictTriggers" category = "regular" diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index a8e5d74b6..fe6764297 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -432,18 +432,6 @@ RewriteResponse DatatypesRewriter::rewriteTester(TNode in) NodeManager::currentNM()->mkConst(true)); } // could try dt.getNumConstructors()==2 && indexOf(in.getOperator())==1 ? - else if (!options::dtUseTesters()) - { - unsigned tindex = indexOf(in.getOperator()); - Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality " - << in[0] << " " << tindex << std::endl; - Node neq = mkTester(in[0], tindex, dt); - Assert(neq != in); - Trace("datatypes-rewrite") - << "DatatypesRewriter::postRewrite: Rewrite tester " << in << " to " - << neq << std::endl; - return RewriteResponse(REWRITE_AGAIN_FULL, neq); - } return RewriteResponse(REWRITE_DONE, in); } @@ -552,64 +540,19 @@ int DatatypesRewriter::isInstCons(Node t, Node n, const Datatype& dt) int DatatypesRewriter::isTester(Node n, Node& a) { - if (options::dtUseTesters()) - { - if (n.getKind() == kind::APPLY_TESTER) - { - a = n[0]; - return indexOf(n.getOperator()); - } - } - else + if (n.getKind() == kind::APPLY_TESTER) { - if (n.getKind() == kind::EQUAL) - { - for (int i = 1; i >= 0; i--) - { - if (n[i].getKind() == kind::APPLY_CONSTRUCTOR) - { - const Datatype& dt = - Datatype::datatypeOf(n[i].getOperator().toExpr()); - int ic = isInstCons(n[1 - i], n[i], dt); - if (ic != -1) - { - a = n[1 - i]; - return ic; - } - } - } - } + a = n[0]; + return indexOf(n.getOperator()); } return -1; } int DatatypesRewriter::isTester(Node n) { - if (options::dtUseTesters()) + if (n.getKind() == kind::APPLY_TESTER) { - if (n.getKind() == kind::APPLY_TESTER) - { - return indexOf(n.getOperator().toExpr()); - } - } - else - { - if (n.getKind() == kind::EQUAL) - { - for (int i = 1; i >= 0; i--) - { - if (n[i].getKind() == kind::APPLY_CONSTRUCTOR) - { - const Datatype& dt = - Datatype::datatypeOf(n[i].getOperator().toExpr()); - int ic = isInstCons(n[1 - i], n[i], dt); - if (ic != -1) - { - return ic; - } - } - } - } + return indexOf(n.getOperator().toExpr()); } return -1; } @@ -634,21 +577,8 @@ unsigned DatatypesRewriter::indexOf(Node n) Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt) { - if (options::dtUseTesters()) - { - return NodeManager::currentNM()->mkNode( - kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n); - } -#ifdef CVC4_ASSERTIONS - Node ret = n.eqNode(DatatypesRewriter::getInstCons(n, dt, i)); - Node a; - int ii = isTester(ret, a); - Assert(ii == i); - Assert(a == n); - return ret; -#else - return n.eqNode(DatatypesRewriter::getInstCons(n, dt, i)); -#endif + return NodeManager::currentNM()->mkNode( + kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n); } Node DatatypesRewriter::mkSplit(Node n, const Datatype& dt) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f886c6d3f..65df3a642 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -824,24 +824,6 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( !cons1.isNull() && !cons2.isNull() ){ Trace("datatypes-debug") << " constructors : " << cons1 << " " << cons2 << std::endl; Node unifEq = cons1.eqNode( cons2 ); - /* - std::vector< Node > exp; - std::vector< std::pair< TNode, TNode > > deq_cand; - bool conf = checkClashModEq( cons1, cons2, exp, deq_cand ); - if( !conf ){ - for( unsigned i=0; imkNode( kind::EQUAL, deq_cand[i].first, deq_cand[i].second ); - exp.push_back( eq.negate() ); - } - } - } - if( conf ){ - exp.push_back( unifEq ); - d_conflictNode = explain( exp ); - } - */ std::vector< Node > rew; if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){ d_conflictNode = explain( unifEq ); @@ -1747,41 +1729,41 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ //add constructor to equivalence class if not done so already int index = getLabelIndex( eqc, n ); - if( index!=-1 && !eqc->d_inst ){ - if( options::dtUseTesters() ){ - Node exp; - Node tt; - if( !eqc->d_constructor.get().isNull() ){ - exp = d_true; - tt = eqc->d_constructor; - }else{ - exp = getLabel( n ); - tt = exp[0]; - } - const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); - //instantiate this equivalence class - eqc->d_inst = true; - Node tt_cons = getInstantiateCons( tt, dt, index ); - Node eq; - if( tt!=tt_cons ){ - eq = tt.eqNode( tt_cons ); - Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; - d_pending.push_back( eq ); - d_pending_exp[ eq ] = exp; - Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl; - Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl; - //eqc->d_inst.set( eq ); - d_infer.push_back( eq ); - d_infer_exp.push_back( exp ); - } - }else{ - eqc->d_inst = true; - } - //} - //else{ - // Debug("datatypes-inst") << "Do not instantiate" << std::endl; - //} + if (index == -1 || eqc->d_inst) + { + return; + } + Node exp; + Node tt; + if (!eqc->d_constructor.get().isNull()) + { + exp = d_true; + tt = eqc->d_constructor; + } + else + { + exp = getLabel(n); + tt = exp[0]; + } + const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); + // instantiate this equivalence class + eqc->d_inst = true; + Node tt_cons = getInstantiateCons(tt, dt, index); + Node eq; + if (tt == tt_cons) + { + return; } + eq = tt.eqNode(tt_cons); + Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq + << std::endl; + d_pending.push_back(eq); + d_pending_exp[eq] = exp; + Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl; + Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp + << std::endl; + d_infer.push_back(eq); + d_infer_exp.push_back(exp); } void TheoryDatatypes::checkCycles() { @@ -2197,38 +2179,6 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { } } -bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) { - if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { - if( n1.getOperator() != n2.getOperator() ) { - return true; - } else { - Assert( n1.getNumChildren() == n2.getNumChildren() ); - for( int i=0; i<(int)n1.getNumChildren(); i++ ) { - TNode nc1 = getEqcConstructor( n1[i] ); - TNode nc2 = getEqcConstructor( n2[i] ); - if( checkClashModEq( nc1, nc2, exp, deq_cand ) ) { - if( nc1!=n1[i] ){ - exp.push_back( nc1.eqNode( n1[i] ) ); - } - if( nc2!=n2[i] ){ - exp.push_back( nc2.eqNode( n2[i] ) ); - } - return true; - } - } - } - }else if( n1!=n2 ){ - if( n1.isConst() && n2.isConst() ){ - return true; - }else{ - if( !areEqual( n1, n2 ) ){ - deq_cand.push_back( std::pair< TNode, TNode >( n1, n2 ) ); - } - } - } - return false; -} - void TheoryDatatypes::getRelevantTerms( std::set& termSet ) { // Compute terms appearing in assertions and shared terms std::set irr_kinds; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index e3a375b87..e06bb7408 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -330,8 +330,6 @@ private: void instantiate( EqcInfo* eqc, Node n ); /** must communicate fact */ bool mustCommunicateFact( Node n, Node exp ); - /** check clash mod eq */ - bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ); /** get relevant terms */ void getRelevantTerms( std::set& termSet ); private: diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index b3dc9965b..a8079f775 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -24,8 +24,6 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#define USE_INDEX_ORDERING - using namespace std; using namespace CVC4::kind; using namespace CVC4::context; @@ -770,7 +768,7 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri } } Trace("fmf-eval-debug") << "Evaluate term " << n << " = "; - printRepresentativeDebug( "fmf-eval-debug", val ); + Trace("fmf-eval-debug") << getRepresentative(val); Trace("fmf-eval-debug") << " (term " << val << "), depIndex = " << depIndex << std::endl; } } @@ -859,7 +857,6 @@ struct sortGetMaxVariableNum { void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){ if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ -#ifdef USE_INDEX_ORDERING //sort arguments in order of least significant vs. most significant variable in default ordering std::map< Node, std::vector< int > > argIndex; std::vector< Node > args; @@ -889,30 +886,8 @@ void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){ Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " "; } Debug("fmf-index-order") << std::endl; -#else - d_eval_uf_use_default[n] = true; -#endif - } -} - -/* -Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { - std::vector< Node > children; - children.push_back(n.getOperator()); - children.insert(children.end(), args.begin(), args.end()); - Node nv = NodeManager::currentNM()->mkNode(APPLY_UF, children); - //make the term model specifically for nv - makeEvalUfModel( nv ); - int argDepIndex; - if( d_eval_uf_use_default[nv] ){ - return d_uf_model_tree[ n.getOperator() ].getValue( this, nv, argDepIndex ); - }else{ - return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex ); } } -*/ - - FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : FirstOrderModel(qe, c, name){ @@ -926,17 +901,6 @@ FirstOrderModelFmc::~FirstOrderModelFmc() } } -/* -Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { - Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl; - for(unsigned i=0; ievaluate(this, args); -} -*/ - void FirstOrderModelFmc::processInitialize( bool ispre ) { if( ispre ){ for( std::map::iterator it = d_models.begin(); it != d_models.end(); ++it ){ @@ -1111,21 +1075,6 @@ Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) { return Node::null(); } -/* -Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { - Debug("qint-debug") << "get curr uf value " << n << std::endl; - if( d_models_valid[n] ){ - TypeNode tn = n.getType(); - if( tn.getNumChildren()>0 ){ - tn = tn[tn.getNumChildren()-1]; - } - return d_models[n]->evaluate( this, tn, args ); - }else{ - return Node::null(); - } -} -*/ - void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) { if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ Node op = n.getKind()==APPLY_UF ? n.getOperator() : n; diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index fcc9cd060..d1b7eebb8 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -194,7 +194,7 @@ Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue( double score = (1.0 + static_cast(d_value_pro_con[0][v].size())) / (1.0 + static_cast(d_value_pro_con[1][v].size())); Debug("fmf-model-cons-debug") << " - score( "; - m->printRepresentativeDebug("fmf-model-cons-debug", v); + Debug("fmf-model-cons-debug") << m->getRepresentative(v); Debug("fmf-model-cons-debug") << " ) = " << score << std::endl; if (score > maxScore) { @@ -213,7 +213,7 @@ Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue( { defaultVal = newDefaultVal; Debug("fmf-model-cons-debug") << "-> Change default value to "; - m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal); + Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal); Debug("fmf-model-cons-debug") << std::endl; } else @@ -227,7 +227,7 @@ Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue( } // get the default term (this term must be defined non-ground in model) Debug("fmf-model-cons-debug") << " Choose "; - m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal); + Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal); Debug("fmf-model-cons-debug") << " as default value (" << defaultTerm << ")" << std::endl; Debug("fmf-model-cons-debug") @@ -437,7 +437,7 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); fmig->d_uf_model_gen[op].makeModel( fmig, it->second ); Debug("fmf-model-cons") << "Function " << op << " is the constant function "; - fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val ); + Debug("fmf-model-cons") << d_uf_prefs[op].d_const_val; Debug("fmf-model-cons") << std::endl; d_uf_model_constructed[op] = true; }else{ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 73d2de401..8c43e98ff 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -116,7 +116,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, } if( options::inferArithTriggerEq() ){ - d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() ); + d_eq_inference = new quantifiers::EqualityInference(c, false); }else{ d_eq_inference = NULL; } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 42818d581..34e1d455b 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -542,36 +542,6 @@ bool TheoryModel::areDisequal(TNode a, TNode b) } } -//for debugging -void TheoryModel::printRepresentativeDebug( const char* c, Node r ){ - if( r.isNull() ){ - Trace( c ) << "null"; - }else if( r.getType().isBoolean() ){ - if( areEqual( r, d_true ) ){ - Trace( c ) << "true"; - }else{ - Trace( c ) << "false"; - } - }else{ - Trace( c ) << getRepresentative( r ); - } -} - -void TheoryModel::printRepresentative( std::ostream& out, Node r ){ - Assert( !r.isNull() ); - if( r.isNull() ){ - out << "null"; - }else if( r.getType().isBoolean() ){ - if( areEqual( r, d_true ) ){ - out << "true"; - }else{ - out << "false"; - } - }else{ - out << getRepresentative( r ); - } -} - bool TheoryModel::areFunctionValuesEnabled() const { return d_enableFuncModels; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index ac0d686de..47d68a365 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -251,10 +251,6 @@ public: Expr getValue(Expr expr) const override; /** get cardinality for sort */ Cardinality getCardinality(Type t) const override; - /** print representative debug function */ - void printRepresentativeDebug( const char* c, Node r ); - /** print representative function */ - void printRepresentative( std::ostream& out, Node r ); //---------------------------- function values /** a map from functions f to a list of all APPLY_UF terms with operator f */ diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 3d656cf24..a3e058569 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -289,7 +289,7 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector }else{ indent( out, ind ); out << "return "; - m->printRepresentative( out, d_value ); + out << m->getRepresentative(d_value); out << std::endl; } }