From: Andrew Reynolds Date: Fri, 23 Mar 2018 18:33:12 +0000 (-0500) Subject: Minor reorganization for ematching (#1701) X-Git-Tag: cvc5-1.0.0~5218 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f506ac50e43a71a92094a478deeaa2c2cd1df4a;p=cvc5.git Minor reorganization for ematching (#1701) --- diff --git a/src/Makefile.am b/src/Makefile.am index c6f8a7ad1..6395a70bc 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -366,8 +366,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/anti_skolem.h \ theory/quantifiers/bv_inverter.cpp \ theory/quantifiers/bv_inverter.h \ - theory/quantifiers/candidate_generator.cpp \ - theory/quantifiers/candidate_generator.h \ theory/quantifiers/cegqi/ceg_instantiator.cpp \ theory/quantifiers/cegqi/ceg_instantiator.h \ theory/quantifiers/cegqi/ceg_t_instantiator.cpp \ @@ -378,6 +376,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/conjecture_generator.h \ theory/quantifiers/dynamic_rewrite.cpp \ theory/quantifiers/dynamic_rewrite.h \ + theory/quantifiers/ematching/candidate_generator.cpp \ + theory/quantifiers/ematching/candidate_generator.h \ theory/quantifiers/ematching/ho_trigger.cpp \ theory/quantifiers/ematching/ho_trigger.h \ theory/quantifiers/ematching/inst_match_generator.cpp \ diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp deleted file mode 100644 index 699a93286..000000000 --- a/src/theory/quantifiers/candidate_generator.cpp +++ /dev/null @@ -1,309 +0,0 @@ -/********************* */ -/*! \file candidate_generator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of theory uf candidate generator class - **/ - -#include "theory/quantifiers/candidate_generator.h" -#include "options/quantifiers_options.h" -#include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::inst; - -bool CandidateGenerator::isLegalCandidate( Node n ){ - return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); -} - -void CandidateGeneratorQueue::addCandidate( Node n ) { - if( isLegalCandidate( n ) ){ - d_candidates.push_back( n ); - } -} - -void CandidateGeneratorQueue::reset( Node eqc ){ - if( d_candidate_index>0 ){ - d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index ); - d_candidate_index = 0; - } - if( !eqc.isNull() ){ - d_candidates.push_back( eqc ); - } -} -Node CandidateGeneratorQueue::getNextCandidate(){ - if( d_candidate_index<(int)d_candidates.size() ){ - Node n = d_candidates[d_candidate_index]; - d_candidate_index++; - return n; - }else{ - d_candidate_index = 0; - d_candidates.clear(); - return Node::null(); - } -} - -CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) : -CandidateGenerator( qe ), d_term_iter( -1 ){ - d_op = qe->getTermDatabase()->getMatchOperator( pat ); - Assert( !d_op.isNull() ); - d_op_arity = pat.getNumChildren(); -} - -void CandidateGeneratorQE::resetInstantiationRound(){ - d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op ); -} - -void CandidateGeneratorQE::reset( Node eqc ){ - d_term_iter = 0; - if( eqc.isNull() ){ - d_mode = cand_term_db; - }else{ - if( isExcludedEqc( eqc ) ){ - d_mode = cand_term_none; - }else{ - eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); - if( ee->hasTerm( eqc ) ){ - quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op ); - if( tat ){ -#if 1 - //create an equivalence class iterator in eq class eqc - Node rep = ee->getRepresentative( eqc ); - d_eqc_iter = eq::EqClassIterator( rep, ee ); - d_mode = cand_term_eqc; -#else - d_tindex.push_back( tat ); - d_tindex_iter.push_back( tat->d_data.begin() ); - d_mode = cand_term_tindex; -#endif - }else{ - d_mode = cand_term_none; - } - }else{ - //the only match is this term itself - d_n = eqc; - d_mode = cand_term_ident; - } - } - } -} -bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { - if( n.hasOperator() ){ - if( isLegalCandidate( n ) ){ - return d_qe->getTermDatabase()->getMatchOperator( n )==d_op; - } - } - return false; -} - -Node CandidateGeneratorQE::getNextCandidate(){ - if( d_mode==cand_term_db ){ - Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; - //get next candidate term in the uf term database - while( d_term_itergetTermDatabase()->getGroundTerm( d_op, d_term_iter ); - d_term_iter++; - if( isLegalCandidate( n ) ){ - if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ - if( d_exclude_eqc.empty() ){ - return n; - }else{ - Node r = d_qe->getEqualityQuery()->getRepresentative( n ); - if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){ - Debug("cand-gen-qe") << "...returning " << n << std::endl; - return n; - } - } - } - } - } - }else if( d_mode==cand_term_eqc ){ - Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl; - while( !d_eqc_iter.isFinished() ){ - Node n = *d_eqc_iter; - ++d_eqc_iter; - if( isLegalOpCandidate( n ) ){ - Debug("cand-gen-qe") << "...returning " << n << std::endl; - return n; - } - } - }else if( d_mode==cand_term_tindex ){ - Debug("cand-gen-qe") << "...get next candidate in tindex " << d_op << " " << d_op_arity << std::endl; - //increment the term index iterator - if( !d_tindex.empty() ){ - //populate the vector - while( d_tindex_iter.size()<=d_op_arity ){ - Assert( !d_tindex_iter.empty() ); - Assert( !d_tindex_iter.back()->second.d_data.empty() ); - d_tindex.push_back( &(d_tindex_iter.back()->second) ); - d_tindex_iter.push_back( d_tindex_iter.back()->second.d_data.begin() ); - } - //get the current node - Assert( d_tindex_iter.back()->second.hasNodeData() ); - Node n = d_tindex_iter.back()->second.getNodeData(); - Debug("cand-gen-qe") << "...returning " << n << std::endl; - Assert( !n.isNull() ); - Assert( isLegalOpCandidate( n ) ); - //increment - bool success = false; - do{ - ++d_tindex_iter.back(); - if( d_tindex_iter.back()==d_tindex.back()->d_data.end() ){ - d_tindex.pop_back(); - d_tindex_iter.pop_back(); - }else{ - success = true; - } - }while( !success && !d_tindex.empty() ); - return n; - } - }else if( d_mode==cand_term_ident ){ - Debug("cand-gen-qe") << "...get next candidate identity" << std::endl; - if( !d_n.isNull() ){ - Node n = d_n; - d_n = Node::null(); - if( isLegalOpCandidate( n ) ){ - return n; - } - } - } - return Node::null(); -} - -CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : - CandidateGenerator( qe ), d_match_pattern( mpat ){ - Assert( mpat.getKind()==EQUAL ); - for( unsigned i=0; i<2; i++ ){ - if( !quantifiers::TermUtil::hasInstConstAttr(mpat[i]) ){ - d_match_gterm = mpat[i]; - } - } -} -void CandidateGeneratorQELitEq::resetInstantiationRound(){ - -} -void CandidateGeneratorQELitEq::reset( Node eqc ){ - if( d_match_gterm.isNull() ){ - d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); - }else{ - d_do_mgt = true; - } -} -Node CandidateGeneratorQELitEq::getNextCandidate(){ - if( d_match_gterm.isNull() ){ - while( !d_eq.isFinished() ){ - Node n = (*d_eq); - ++d_eq; - if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){ - //an equivalence class with the same type as the pattern, return reflexive equality - return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); - } - } - }else{ - if( d_do_mgt ){ - d_do_mgt = false; - return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm ); - } - } - return Node::null(); -} - - -CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : -CandidateGenerator( qe ), d_match_pattern( mpat ){ - - Assert( d_match_pattern.getKind()==EQUAL ); - d_match_pattern_type = d_match_pattern[0].getType(); -} - -void CandidateGeneratorQELitDeq::resetInstantiationRound(){ - -} - -void CandidateGeneratorQELitDeq::reset( Node eqc ){ - Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst(false) ); - d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); -} - -Node CandidateGeneratorQELitDeq::getNextCandidate(){ - //get next candidate term in equivalence class - while( !d_eqc_false.isFinished() ){ - Node n = (*d_eqc_false); - ++d_eqc_false; - if( n.getKind()==d_match_pattern.getKind() ){ - if( n[0].getType().isComparableTo( d_match_pattern_type ) ){ - //found an iff or equality, try to match it - //DO_THIS: cache to avoid redundancies? - //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? - return n; - } - } - } - return Node::null(); -} - - -CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : - CandidateGenerator( qe ), d_match_pattern( mpat ){ - d_match_pattern_type = mpat.getType(); - Assert( mpat.getKind()==INST_CONSTANT ); - d_f = quantifiers::TermUtil::getInstConstAttr( mpat ); - d_index = mpat.getAttribute(InstVarNumAttribute()); - d_firstTime = false; -} - -void CandidateGeneratorQEAll::resetInstantiationRound() { - -} - -void CandidateGeneratorQEAll::reset( Node eqc ) { - d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); - d_firstTime = true; -} - -Node CandidateGeneratorQEAll::getNextCandidate() { - while( !d_eq.isFinished() ){ - TNode n = (*d_eq); - ++d_eq; - if( n.getType().isComparableTo( d_match_pattern_type ) ){ - TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); - if( !nh.isNull() ){ - if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ - nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); - //don't consider this if already the instantiation is ineligible - if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){ - nh = Node::null(); - } - } - if( !nh.isNull() ){ - d_firstTime = false; - //an equivalence class with the same type as the pattern, return it - return nh; - } - } - } - } - if( d_firstTime ){ - //must return something - d_firstTime = false; - return d_qe->getInstantiate()->getTermForType(d_match_pattern_type); - } - return Node::null(); -} diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h deleted file mode 100644 index 4662d7c4c..000000000 --- a/src/theory/quantifiers/candidate_generator.h +++ /dev/null @@ -1,179 +0,0 @@ -/********************* */ -/*! \file candidate_generator.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Theory uf candidate generator - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H -#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H - -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" - -namespace CVC4 { -namespace theory { - -namespace quantifiers { - class TermArgTrie; -} - -class QuantifiersEngine; - -namespace inst { - -/** base class for generating candidates for matching */ -class CandidateGenerator { -protected: - QuantifiersEngine* d_qe; -public: - CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){} - virtual ~CandidateGenerator(){} - - /** Get candidates functions. These set up a context to get all match candidates. - cg->reset( eqc ); - do{ - Node cand = cg->getNextCandidate(); - //....... - }while( !cand.isNull() ); - - eqc is the equivalence class you are searching in - */ - virtual void reset( Node eqc ) = 0; - virtual Node getNextCandidate() = 0; - /** add candidate to list of nodes returned by this generator */ - virtual void addCandidate( Node n ) {} - /** call this at the beginning of each instantiation round */ - virtual void resetInstantiationRound() = 0; -public: - /** legal candidate */ - bool isLegalCandidate( Node n ); -};/* class CandidateGenerator */ - -/** candidate generator queue (for manual candidate generation) */ -class CandidateGeneratorQueue : public CandidateGenerator { - private: - std::vector< Node > d_candidates; - int d_candidate_index; - - public: - CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){} - - void addCandidate(Node n) override; - - void resetInstantiationRound() override {} - void reset(Node eqc) override; - Node getNextCandidate() override; -};/* class CandidateGeneratorQueue */ - -//the default generator -class CandidateGeneratorQE : public CandidateGenerator -{ - friend class CandidateGeneratorQEDisequal; - - private: - //operator you are looking for - Node d_op; - //the equality class iterator - unsigned d_op_arity; - std::vector< quantifiers::TermArgTrie* > d_tindex; - std::vector< std::map< TNode, quantifiers::TermArgTrie >::iterator > d_tindex_iter; - eq::EqClassIterator d_eqc_iter; - //std::vector< Node > d_eqc; - int d_term_iter; - int d_term_iter_limit; - bool d_using_term_db; - enum { - cand_term_db, - cand_term_ident, - cand_term_eqc, - cand_term_tindex, - cand_term_none, - }; - short d_mode; - bool isLegalOpCandidate( Node n ); - Node d_n; - std::map< Node, bool > d_exclude_eqc; - - public: - CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ); - - void resetInstantiationRound() override; - void reset(Node eqc) override; - Node getNextCandidate() override; - void excludeEqc( Node r ) { d_exclude_eqc[r] = true; } - bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); } -}; - -class CandidateGeneratorQELitEq : public CandidateGenerator -{ - private: - //the equality classes iterator - eq::EqClassesIterator d_eq; - //equality you are trying to match equalities for - Node d_match_pattern; - Node d_match_gterm; - bool d_do_mgt; - - public: - CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); - - void resetInstantiationRound() override; - void reset(Node eqc) override; - Node getNextCandidate() override; -}; - -class CandidateGeneratorQELitDeq : public CandidateGenerator -{ - private: - //the equality class iterator for false - eq::EqClassIterator d_eqc_false; - //equality you are trying to match disequalities for - Node d_match_pattern; - //type of disequality - TypeNode d_match_pattern_type; - - public: - CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); - - void resetInstantiationRound() override; - void reset(Node eqc) override; - Node getNextCandidate() override; -}; - -class CandidateGeneratorQEAll : public CandidateGenerator -{ - private: - //the equality classes iterator - eq::EqClassesIterator d_eq; - //equality you are trying to match equalities for - Node d_match_pattern; - TypeNode d_match_pattern_type; - // quantifier/index for the variable we are matching - Node d_f; - unsigned d_index; - //first time - bool d_firstTime; - - public: - CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); - - void resetInstantiationRound() override; - void reset(Node eqc) override; - Node getNextCandidate() override; -}; - -}/* CVC4::theory::inst namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp new file mode 100644 index 000000000..ea5e8592d --- /dev/null +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -0,0 +1,309 @@ +/********************* */ +/*! \file candidate_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of theory uf candidate generator class + **/ + +#include "theory/quantifiers/ematching/candidate_generator.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::inst; + +bool CandidateGenerator::isLegalCandidate( Node n ){ + return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); +} + +void CandidateGeneratorQueue::addCandidate( Node n ) { + if( isLegalCandidate( n ) ){ + d_candidates.push_back( n ); + } +} + +void CandidateGeneratorQueue::reset( Node eqc ){ + if( d_candidate_index>0 ){ + d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index ); + d_candidate_index = 0; + } + if( !eqc.isNull() ){ + d_candidates.push_back( eqc ); + } +} +Node CandidateGeneratorQueue::getNextCandidate(){ + if( d_candidate_index<(int)d_candidates.size() ){ + Node n = d_candidates[d_candidate_index]; + d_candidate_index++; + return n; + }else{ + d_candidate_index = 0; + d_candidates.clear(); + return Node::null(); + } +} + +CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) : +CandidateGenerator( qe ), d_term_iter( -1 ){ + d_op = qe->getTermDatabase()->getMatchOperator( pat ); + Assert( !d_op.isNull() ); + d_op_arity = pat.getNumChildren(); +} + +void CandidateGeneratorQE::resetInstantiationRound(){ + d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op ); +} + +void CandidateGeneratorQE::reset( Node eqc ){ + d_term_iter = 0; + if( eqc.isNull() ){ + d_mode = cand_term_db; + }else{ + if( isExcludedEqc( eqc ) ){ + d_mode = cand_term_none; + }else{ + eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); + if( ee->hasTerm( eqc ) ){ + quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op ); + if( tat ){ +#if 1 + //create an equivalence class iterator in eq class eqc + Node rep = ee->getRepresentative( eqc ); + d_eqc_iter = eq::EqClassIterator( rep, ee ); + d_mode = cand_term_eqc; +#else + d_tindex.push_back( tat ); + d_tindex_iter.push_back( tat->d_data.begin() ); + d_mode = cand_term_tindex; +#endif + }else{ + d_mode = cand_term_none; + } + }else{ + //the only match is this term itself + d_n = eqc; + d_mode = cand_term_ident; + } + } + } +} +bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { + if( n.hasOperator() ){ + if( isLegalCandidate( n ) ){ + return d_qe->getTermDatabase()->getMatchOperator( n )==d_op; + } + } + return false; +} + +Node CandidateGeneratorQE::getNextCandidate(){ + if( d_mode==cand_term_db ){ + Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; + //get next candidate term in the uf term database + while( d_term_itergetTermDatabase()->getGroundTerm( d_op, d_term_iter ); + d_term_iter++; + if( isLegalCandidate( n ) ){ + if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ + if( d_exclude_eqc.empty() ){ + return n; + }else{ + Node r = d_qe->getEqualityQuery()->getRepresentative( n ); + if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){ + Debug("cand-gen-qe") << "...returning " << n << std::endl; + return n; + } + } + } + } + } + }else if( d_mode==cand_term_eqc ){ + Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl; + while( !d_eqc_iter.isFinished() ){ + Node n = *d_eqc_iter; + ++d_eqc_iter; + if( isLegalOpCandidate( n ) ){ + Debug("cand-gen-qe") << "...returning " << n << std::endl; + return n; + } + } + }else if( d_mode==cand_term_tindex ){ + Debug("cand-gen-qe") << "...get next candidate in tindex " << d_op << " " << d_op_arity << std::endl; + //increment the term index iterator + if( !d_tindex.empty() ){ + //populate the vector + while( d_tindex_iter.size()<=d_op_arity ){ + Assert( !d_tindex_iter.empty() ); + Assert( !d_tindex_iter.back()->second.d_data.empty() ); + d_tindex.push_back( &(d_tindex_iter.back()->second) ); + d_tindex_iter.push_back( d_tindex_iter.back()->second.d_data.begin() ); + } + //get the current node + Assert( d_tindex_iter.back()->second.hasNodeData() ); + Node n = d_tindex_iter.back()->second.getNodeData(); + Debug("cand-gen-qe") << "...returning " << n << std::endl; + Assert( !n.isNull() ); + Assert( isLegalOpCandidate( n ) ); + //increment + bool success = false; + do{ + ++d_tindex_iter.back(); + if( d_tindex_iter.back()==d_tindex.back()->d_data.end() ){ + d_tindex.pop_back(); + d_tindex_iter.pop_back(); + }else{ + success = true; + } + }while( !success && !d_tindex.empty() ); + return n; + } + }else if( d_mode==cand_term_ident ){ + Debug("cand-gen-qe") << "...get next candidate identity" << std::endl; + if( !d_n.isNull() ){ + Node n = d_n; + d_n = Node::null(); + if( isLegalOpCandidate( n ) ){ + return n; + } + } + } + return Node::null(); +} + +CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : + CandidateGenerator( qe ), d_match_pattern( mpat ){ + Assert( mpat.getKind()==EQUAL ); + for( unsigned i=0; i<2; i++ ){ + if( !quantifiers::TermUtil::hasInstConstAttr(mpat[i]) ){ + d_match_gterm = mpat[i]; + } + } +} +void CandidateGeneratorQELitEq::resetInstantiationRound(){ + +} +void CandidateGeneratorQELitEq::reset( Node eqc ){ + if( d_match_gterm.isNull() ){ + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + }else{ + d_do_mgt = true; + } +} +Node CandidateGeneratorQELitEq::getNextCandidate(){ + if( d_match_gterm.isNull() ){ + while( !d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){ + //an equivalence class with the same type as the pattern, return reflexive equality + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); + } + } + }else{ + if( d_do_mgt ){ + d_do_mgt = false; + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm ); + } + } + return Node::null(); +} + + +CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : +CandidateGenerator( qe ), d_match_pattern( mpat ){ + + Assert( d_match_pattern.getKind()==EQUAL ); + d_match_pattern_type = d_match_pattern[0].getType(); +} + +void CandidateGeneratorQELitDeq::resetInstantiationRound(){ + +} + +void CandidateGeneratorQELitDeq::reset( Node eqc ){ + Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst(false) ); + d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); +} + +Node CandidateGeneratorQELitDeq::getNextCandidate(){ + //get next candidate term in equivalence class + while( !d_eqc_false.isFinished() ){ + Node n = (*d_eqc_false); + ++d_eqc_false; + if( n.getKind()==d_match_pattern.getKind() ){ + if( n[0].getType().isComparableTo( d_match_pattern_type ) ){ + //found an iff or equality, try to match it + //DO_THIS: cache to avoid redundancies? + //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? + return n; + } + } + } + return Node::null(); +} + + +CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : + CandidateGenerator( qe ), d_match_pattern( mpat ){ + d_match_pattern_type = mpat.getType(); + Assert( mpat.getKind()==INST_CONSTANT ); + d_f = quantifiers::TermUtil::getInstConstAttr( mpat ); + d_index = mpat.getAttribute(InstVarNumAttribute()); + d_firstTime = false; +} + +void CandidateGeneratorQEAll::resetInstantiationRound() { + +} + +void CandidateGeneratorQEAll::reset( Node eqc ) { + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); + d_firstTime = true; +} + +Node CandidateGeneratorQEAll::getNextCandidate() { + while( !d_eq.isFinished() ){ + TNode n = (*d_eq); + ++d_eq; + if( n.getType().isComparableTo( d_match_pattern_type ) ){ + TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); + if( !nh.isNull() ){ + if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ + nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); + //don't consider this if already the instantiation is ineligible + if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){ + nh = Node::null(); + } + } + if( !nh.isNull() ){ + d_firstTime = false; + //an equivalence class with the same type as the pattern, return it + return nh; + } + } + } + } + if( d_firstTime ){ + //must return something + d_firstTime = false; + return d_qe->getInstantiate()->getTermForType(d_match_pattern_type); + } + return Node::null(); +} diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h new file mode 100644 index 000000000..4662d7c4c --- /dev/null +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -0,0 +1,179 @@ +/********************* */ +/*! \file candidate_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Clark Barrett + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Theory uf candidate generator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +namespace quantifiers { + class TermArgTrie; +} + +class QuantifiersEngine; + +namespace inst { + +/** base class for generating candidates for matching */ +class CandidateGenerator { +protected: + QuantifiersEngine* d_qe; +public: + CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){} + virtual ~CandidateGenerator(){} + + /** Get candidates functions. These set up a context to get all match candidates. + cg->reset( eqc ); + do{ + Node cand = cg->getNextCandidate(); + //....... + }while( !cand.isNull() ); + + eqc is the equivalence class you are searching in + */ + virtual void reset( Node eqc ) = 0; + virtual Node getNextCandidate() = 0; + /** add candidate to list of nodes returned by this generator */ + virtual void addCandidate( Node n ) {} + /** call this at the beginning of each instantiation round */ + virtual void resetInstantiationRound() = 0; +public: + /** legal candidate */ + bool isLegalCandidate( Node n ); +};/* class CandidateGenerator */ + +/** candidate generator queue (for manual candidate generation) */ +class CandidateGeneratorQueue : public CandidateGenerator { + private: + std::vector< Node > d_candidates; + int d_candidate_index; + + public: + CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){} + + void addCandidate(Node n) override; + + void resetInstantiationRound() override {} + void reset(Node eqc) override; + Node getNextCandidate() override; +};/* class CandidateGeneratorQueue */ + +//the default generator +class CandidateGeneratorQE : public CandidateGenerator +{ + friend class CandidateGeneratorQEDisequal; + + private: + //operator you are looking for + Node d_op; + //the equality class iterator + unsigned d_op_arity; + std::vector< quantifiers::TermArgTrie* > d_tindex; + std::vector< std::map< TNode, quantifiers::TermArgTrie >::iterator > d_tindex_iter; + eq::EqClassIterator d_eqc_iter; + //std::vector< Node > d_eqc; + int d_term_iter; + int d_term_iter_limit; + bool d_using_term_db; + enum { + cand_term_db, + cand_term_ident, + cand_term_eqc, + cand_term_tindex, + cand_term_none, + }; + short d_mode; + bool isLegalOpCandidate( Node n ); + Node d_n; + std::map< Node, bool > d_exclude_eqc; + + public: + CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ); + + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; + void excludeEqc( Node r ) { d_exclude_eqc[r] = true; } + bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); } +}; + +class CandidateGeneratorQELitEq : public CandidateGenerator +{ + private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + Node d_match_gterm; + bool d_do_mgt; + + public: + CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); + + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; +}; + +class CandidateGeneratorQELitDeq : public CandidateGenerator +{ + private: + //the equality class iterator for false + eq::EqClassIterator d_eqc_false; + //equality you are trying to match disequalities for + Node d_match_pattern; + //type of disequality + TypeNode d_match_pattern_type; + + public: + CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); + + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; +}; + +class CandidateGeneratorQEAll : public CandidateGenerator +{ + private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + TypeNode d_match_pattern_type; + // quantifier/index for the variable we are matching + Node d_f; + unsigned d_index; + //first time + bool d_firstTime; + + public: + CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); + + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; +}; + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index c36597e3e..ec0a4039a 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -17,11 +17,11 @@ #include "expr/datatype.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/ematching/candidate_generator.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -541,14 +541,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) } Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" << std::endl; - if (Trigger::isBooleanTermTrigger(n)) - { - VarMatchGeneratorBooleanTerm* vmg = - new VarMatchGeneratorBooleanTerm(n[0], n[1]); - Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0] - << std::endl; - return vmg; - } Node x; if (options::purifyTriggers()) { @@ -565,38 +557,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n) return new InstMatchGenerator(n); } -VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) : - InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) { - d_children_types.push_back(var.getAttribute(InstVarNumAttribute())); -} - -int VarMatchGeneratorBooleanTerm::getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) -{ - int ret_val = -1; - if( !d_eq_class.isNull() ){ - Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern )); - d_eq_class = Node::null(); - d_rm_prev = m.get(d_children_types[0]).isNull(); - if (!m.set(qe->getEqualityQuery(), d_children_types[0], s)) - { - return -1; - }else{ - ret_val = continueNextMatch(q, m, qe, tparent); - if( ret_val>0 ){ - return ret_val; - } - } - } - if( d_rm_prev ){ - m.d_vals[d_children_types[0]] = Node::null(); - d_rm_prev = false; - } - return ret_val; -} - VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) : InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){ d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute())); diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 6c38db13b..cbd5702a0 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -418,32 +418,6 @@ class InstMatchGenerator : public IMGenerator { static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); };/* class InstMatchGenerator */ -/** match generator for Boolean term ITEs -* This handles the special case of triggers that look like ite( x, BV1, BV0 ). -*/ -class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { -public: - VarMatchGeneratorBooleanTerm( Node var, Node comp ); - - /** Reset */ - bool reset(Node eqc, QuantifiersEngine* qe) override - { - d_eq_class = eqc; - return true; - } - /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; - - private: - /** stores the true branch of the Boolean ITE */ - Node d_comp; - /** stores whether we have written a value for var in the current match. */ - bool d_rm_prev; -}; - /** match generator for purified terms * This handles the special case of invertible terms like x+1 (see * Trigger::getTermInversionVariable). diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 430d261a1..4039c632f 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -15,7 +15,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/ematching/candidate_generator.h" #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/instantiate.h" @@ -262,9 +262,8 @@ bool Trigger::isUsable( Node n, Node q ){ return true; }else{ std::map< Node, Node > coeffs; - if( isBooleanTermTrigger( n ) ){ - return true; - }else if( options::purifyTriggers() ){ + if (options::purifyTriggers()) + { Node x = getInversionVariable( n ); if( !x.isNull() ){ return true; @@ -522,22 +521,6 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod } } -bool Trigger::isBooleanTermTrigger( Node n ) { - if( n.getKind()==ITE ){ - //check for boolean term converted to ITE - if( n[0].getKind()==INST_CONSTANT && - n[1].getKind()==CONST_BITVECTOR && - n[2].getKind()==CONST_BITVECTOR ){ - if( ((BitVectorType)n[1].getType().toType()).getSize()==1 && - n[1].getConst().toInteger()==1 && - n[2].getConst().toInteger()==0 ){ - return true; - } - } - } - return false; -} - bool Trigger::isPureTheoryTrigger( Node n ) { if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){ return false; diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index cd10e4f8a..28d227bf7 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -315,8 +315,6 @@ class Trigger { static bool isRelationalTriggerKind( Kind k ); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger( Node n ); - /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */ - static bool isBooleanTermTrigger( Node n ); /** is n a pure theory trigger, e.g. head( x )? */ static bool isPureTheoryTrigger( Node n ); /** get trigger weight