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 \
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 \
+++ /dev/null
-/********************* */
-/*! \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_iter<d_term_iter_limit ){
- Node n = d_qe->getTermDatabase()->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<bool>(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();
-}
+++ /dev/null
-/********************* */
-/*! \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 */
--- /dev/null
+/********************* */
+/*! \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_iter<d_term_iter_limit ){
+ Node n = d_qe->getTermDatabase()->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<bool>(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();
+}
--- /dev/null
+/********************* */
+/*! \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 */
#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;
}
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())
{
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()));
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).
#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"
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;
}
}
-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<BitVector>().toInteger()==1 &&
- n[2].getConst<BitVector>().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;
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
projects / cvc5.git / commitdiff