From 06440f4ed1f4de8612740dc21b63ac6967404f31 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Jul 2018 19:53:14 +0200 Subject: [PATCH] Minor cleanup and fixes for conflict-based instantiation (#2123) --- src/options/options_handler.cpp | 8 - .../quantifiers/quant_conflict_find.cpp | 150 ++---------------- src/theory/quantifiers/quant_conflict_find.h | 5 - src/theory/quantifiers/term_database.h | 2 + 4 files changed, 15 insertions(+), 150 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 8f179531b..6f9d31024 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -331,12 +331,6 @@ prop-eq \n\ conflict \n\ + Apply QCF algorithm to find conflicts only.\n\ \n\ -partial \n\ -+ Apply QCF algorithm to instantiate heuristically as well. \n\ -\n\ -mc \n\ -+ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ -\n\ "; const std::string OptionsHandler::s_userPatModeHelp = "\ @@ -716,8 +710,6 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option, return theory::quantifiers::QCF_CONFLICT_ONLY; } else if(optarg == "default" || optarg == "prop-eq") { return theory::quantifiers::QCF_PROP_EQ; - } else if(optarg == "partial") { - return theory::quantifiers::QCF_PARTIAL; } else if(optarg == "help") { puts(s_qcfModeHelp.c_str()); exit(1); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index f7521ff4a..3b2a650ab 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -253,28 +253,6 @@ bool QuantInfo::reset_round( QuantConflictFind * p ) { d_curr_var_deq.clear(); d_tconstraints.clear(); - //add built-in variable constraints - for( unsigned r=0; r<2; r++ ){ - for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin(); - it != d_var_constraint[r].end(); ++it ){ - for( unsigned j=0; jsecond.size(); j++ ){ - Node rr = it->second[j]; - if( !isVar( rr ) ){ - rr = p->getRepresentative( rr ); - } - if( addConstraint( p, it->first, rr, r==0 )==-1 ){ - d_var_constraint[0].clear(); - d_var_constraint[1].clear(); - //quantified formula is actually equivalent to true - Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl; - d_mg->d_children.clear(); - d_mg->d_n = NodeManager::currentNM()->mkConst( true ); - d_mg->d_type = MatchGen::typ_ground; - return false; - } - } - } - } d_mg->reset_round( p ); for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){ it->second->reset_round( p ); @@ -664,24 +642,6 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { }else{ return chEnt; } -/* - if( chEnt ){ - //check if it is entailed - Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl; - std::pair et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew ); - ++(p->d_statistics.d_entailment_checks); - Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl; - if( !et.first ){ - Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl; - return false; - }else{ - return true; - } - }else{ - Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl; - return true; - } -*/ }else{ Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl; return true; @@ -1287,12 +1247,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { TNode f = getMatchOperator( p, d_n ); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f ); - if( qni!=NULL ){ - d_qn.push_back( qni ); - }else{ + if (qni == nullptr || qni->empty()) + { //inform irrelevant quantifiers p->setIrrelevantFunction( f ); } + else + { + d_qn.push_back(qni); + } d_matched_basis = false; }else if( d_type==typ_tsym || d_type==typ_tconstraint ){ for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){ @@ -1526,7 +1489,9 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl; d_wasSet = success; return success; - }else if( d_type==typ_formula || d_type==typ_ite_var ){ + } + else if (d_type == typ_formula) + { bool success = false; if( d_child_counter<0 ){ if( d_child_counter<-1 ){ @@ -1597,7 +1562,8 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_child_counter++; getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi ); }else{ - if( d_child_counter==4 || ( d_type==typ_ite_var && d_child_counter==2 ) ){ + if (d_child_counter == 4) + { d_child_counter = -1; }else{ d_child_counter +=2; @@ -1630,84 +1596,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { return false; } -bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) { - if( d_type==typ_eq ){ - Node n[2]; - for( unsigned i=0; i<2; i++ ){ - Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl; - n[i] = getExplanationTerm( p, qi, d_n[i], exp ); - } - Node eq = n[0].eqNode( n[1] ); - if( !d_tgt_orig ){ - eq = eq.negate(); - } - exp.push_back( eq ); - Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl; - return true; - }else if( d_type==typ_pred ){ - Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl; - Node n = getExplanationTerm( p, qi, d_n, exp ); - if( !d_tgt_orig ){ - n = n.negate(); - } - exp.push_back( n ); - Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl; - return true; - }else if( d_type==typ_formula ){ - Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl; - if( d_n.getKind()==OR || d_n.getKind()==AND ){ - if( (d_n.getKind()==AND)==d_tgt ){ - for( unsigned i=0; igetExplanation( p, qi, exp ) ){ - return false; - } - } - }else{ - return getChild( d_child_counter )->getExplanation( p, qi, exp ); - } - }else if( d_n.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( !getChild( i )->getExplanation( p, qi, exp ) ){ - return false; - } - } - }else if( d_n.getKind()==ITE ){ - for( unsigned i=0; i<3; i++ ){ - bool isActive = ( ( i==0 && d_child_counter!=5 ) || - ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) || - ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) ); - if( isActive ){ - if( !getChild( i )->getExplanation( p, qi, exp ) ){ - return false; - } - } - } - }else{ - return false; - } - return true; - }else{ - return false; - } -} - -Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) { - Node v = qi->getCurrentExpValue( t ); - if( isHandledUfTerm( t ) ){ - for( unsigned i=0; i& exp ); - Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ); bool isValid() { return d_type!=typ_invalid; } void setInvalid(); @@ -138,7 +135,6 @@ public: std::map< TNode, int > d_var_num; std::vector< int > d_tsym_vars; std::map< TNode, bool > d_inMatchConstraint; - std::map< int, std::vector< Node > > d_var_constraint[2]; int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; } bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); } int getNumVars() { return (int)d_vars.size(); } @@ -205,7 +201,6 @@ private: private: std::map< Node, Node > d_op_node; std::map< Node, int > d_fid; - Node mkEqNode( Node a, Node b ); public: //for ground terms Node d_true; Node d_false; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e9dd371df..7e3806e8c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -96,6 +96,8 @@ public: void debugPrint(const char* c, Node n, unsigned depth = 0); /** clear all data from this trie */ void clear() { d_data.clear(); } + /** is empty */ + bool empty() { return d_data.empty(); } };/* class TermArgTrie */ namespace fmcheck { -- 2.30.2