From be316870ef337a435d65f46a26f40ef0eab97934 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 10 Nov 2014 15:53:51 +0100 Subject: [PATCH] Do not eliminate variables only occurring in patterns. Minor improvements to sort inference. Remove unused code. --- .../quantifiers/candidate_generator.cpp | 36 +------------------ .../quantifiers/quant_conflict_find.cpp | 3 +- .../quantifiers/quantifiers_rewriter.cpp | 14 +++++++- src/theory/quantifiers/quantifiers_rewriter.h | 1 + src/theory/quantifiers/term_database.cpp | 19 +--------- src/theory/quantifiers/term_database.h | 10 ------ src/theory/theory_engine.cpp | 11 +----- src/util/sort_inference.cpp | 19 ++++++++-- 8 files changed, 34 insertions(+), 79 deletions(-) diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 0f2adf3b4..29640e18f 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -101,6 +101,7 @@ Node CandidateGeneratorQE::getNextCandidate(){ //get next candidate term in the uf term database while( d_term_itergetTermDatabase()->d_op_map[d_op][d_term_iter]; + //Assert( d_qe->getEqualityQuery()->hasTerm( n ) ); d_term_iter++; if( isLegalCandidate( n ) ){ return n; @@ -126,41 +127,6 @@ Node CandidateGeneratorQE::getNextCandidate(){ return Node::null(); } -//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) : -// d_qe( qe ), d_eq_class( eqc ){ -// d_eci = NULL; -//} -//void CandidateGeneratorQEDisequal::resetInstantiationRound(){ -// -//} -////we will iterate over all terms that are disequal from eqc -//void CandidateGeneratorQEDisequal::reset( Node eqc ){ -// //Assert( !eqc.isNull() ); -// ////begin iterating over equivalence classes that are disequal from eqc -// //d_eci = d_ith->getEquivalenceClassInfo( eqc ); -// //if( d_eci ){ -// // d_eqci_iter = d_eci->d_disequal.begin(); -// //} -//} -//Node CandidateGeneratorQEDisequal::getNextCandidate(){ -// //if( d_eci ){ -// // while( d_eqci_iter != d_eci->d_disequal.end() ){ -// // if( (*d_eqci_iter).second ){ -// // //we have an equivalence class that is disequal from eqc -// // d_cg->reset( (*d_eqci_iter).first ); -// // Node n = d_cg->getNextCandidate(); -// // //if there is a candidate in this equivalence class, return it -// // if( !n.isNull() ){ -// // return n; -// // } -// // } -// // ++d_eqci_iter; -// // } -// //} -// return Node::null(); -//} - - CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : d_match_pattern( mpat ), d_qe( qe ){ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index d58ce14b1..768ba63de 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1886,8 +1886,7 @@ Node QuantConflictFind::evaluateTerm( Node n ) { /** new node */ void QuantConflictFind::newEqClass( Node n ) { - //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl; - //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl; + } /** merge */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index fb7ff679b..0d338f283 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -105,6 +105,7 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node } void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) { + Assert( activeArgs.empty() ); std::map< Node, bool > activeMap; computeArgs( args, activeMap, n ); for( unsigned i=0; i& args, std::vector< } } +void QuantifiersRewriter::computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ) { + Assert( activeArgs.empty() ); + std::map< Node, bool > activeMap; + computeArgs( args, activeMap, n ); + computeArgs( args, activeMap, ipl ); + for( unsigned i=0; i& args, Node n ){ if( std::find( args.begin(), args.end(), n )!=args.end() ){ @@ -728,7 +740,7 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ std::vector< Node > activeArgs; - computeArgVec( args, activeArgs, body ); + computeArgVec2( args, activeArgs, body, ipl ); if( activeArgs.empty() ){ return body; }else{ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index e2137b9f4..901a47f79 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -40,6 +40,7 @@ private: static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n ); static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); + static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); static bool hasArg( std::vector< Node >& args, Node n ); static void setNestedQuantifiers( Node n, Node q ); static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 392fc269a..c35adef6a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -329,6 +329,7 @@ void TermDb::reset( Theory::Effort effort ){ if( !it->second.empty() ){ for( unsigned i=0; isecond.size(); i++ ){ Node n = it->second[i]; + //Assert( d_quantEngine->getEqualityQuery()->hasTerm( n ) ); computeModelBasisArgAttribute( n ); if( !n.getAttribute(NoMatchAttribute()) ){ computeArgReps( n ); @@ -794,24 +795,6 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){ return d_free_vars[tn]; } -const std::vector & TermDb::getParents(TNode n, TNode f, int arg){ - std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >,NodeHashFunction >,NodeHashFunction >::const_iterator - rn = d_parents.find( n ); - if( rn !=d_parents.end() ){ - std::hash_map< Node, std::hash_map< int, std::vector< Node > > , NodeHashFunction > ::const_iterator - rf = rn->second.find(f); - if( rf != rn->second.end() ){ - std::hash_map< int, std::vector< Node > > ::const_iterator - ra = rf->second.find(arg); - if( ra != rf->second.end() ){ - return ra->second; - } - } - } - static std::vector empty; - return empty; -} - void TermDb::computeVarContains( Node n ) { if( d_var_contains.find( n )==d_var_contains.end() ){ d_var_contains[n].clear(); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e40635d4e..1d3757d65 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -170,16 +170,6 @@ public: TNode evaluateTerm( TNode n ); /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); -public: - /** parent structure (for efficient E-matching): - n -> op -> index -> L - map from node "n" to a list of nodes "L", where each node n' in L - has operator "op", and n'["index"] = n. - for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... } - */ - /* Todo replace int by size_t */ - std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents; - const std::vector & getParents(TNode n, TNode f, int arg); //for model basis private: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7fb989a5a..12a169e09 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -92,19 +92,10 @@ void TheoryEngine::finishInit() { void TheoryEngine::eqNotifyNewClass(TNode t){ d_quantEngine->addTermToDatabase( t ); - if( d_logicInfo.isQuantified() && options::quantConflictFind() ){ - d_quantEngine->getConflictFind()->newEqClass( t ); - } } void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){ - //TODO: add notification to efficient E-matching - if( d_logicInfo.isQuantified() ){ - //d_quantEngine->getEfficientEMatcher()->merge( t1, t2 ); - if( options::quantConflictFind() ){ - d_quantEngine->getConflictFind()->merge( t1, t2 ); - } - } + } void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){ diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index 066ba6103..dbd1dcd16 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -171,7 +171,9 @@ bool SortInference::simplify( std::vector< Node >& assertions ){ for( unsigned i=0; i var_bound; + Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl; assertions[i] = simplify( assertions[i], var_bound ); + Trace("sort-inference-debug") << "Done." << std::endl; if( prev!=assertions[i] ){ assertions[i] = theory::Rewriter::rewrite( assertions[i] ); rewritten = true; @@ -512,6 +514,7 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ } Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ + Trace("sort-inference-debug2") << "Simplify " << n << std::endl; std::vector< Node > children; if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ //recreate based on types of variables @@ -519,6 +522,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ for( size_t i=0; i& var_bound ){ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ children.push_back( n.getOperator() ); } + bool childChanged = false; for( size_t i=0; i=1; } if( processChild ){ - children.push_back( simplify( n[i], var_bound ) ); + Node nc = simplify( n[i], var_bound ); + Trace("sort-inference-debug2") << "Simplify " << i << " " << n[i] << " returned " << nc << std::endl; + children.push_back( nc ); + childChanged = childChanged || nc!=n[i]; } } @@ -543,6 +551,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ //erase from variable bound for( size_t i=0; imkNode( n.getKind(), children ); @@ -596,7 +605,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ if( n[i].isConst() ){ children[i+1] = getNewSymbol( n[i], tna ); }else{ - Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl; + Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl; Assert( false ); } } @@ -616,7 +625,11 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ //just return n, we will fix at higher scope return n; }else{ - return NodeManager::currentNM()->mkNode( n.getKind(), children ); + if( childChanged ){ + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } } } -- 2.30.2