diff options
Diffstat (limited to 'src/theory/quantifiers')
-rwxr-xr-x | src/theory/quantifiers/inst_gen.cpp | 596 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_gen.h | 122 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_match_generator.cpp | 1328 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_match_generator.h | 384 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_cbqi.cpp | 806 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_cbqi.h | 218 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_e_matching.cpp | 758 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_e_matching.h | 270 | ||||
-rwxr-xr-x | src/theory/quantifiers/macros.cpp | 750 | ||||
-rwxr-xr-x | src/theory/quantifiers/macros.h | 124 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_util.cpp | 290 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_util.h | 198 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 60 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 80 |
14 files changed, 2992 insertions, 2992 deletions
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index d3bd6ad03..b5f92c5f8 100755 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -1,298 +1,298 @@ -/********************* */
-/*! \file inst_gen.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of inst gen classes
- **/
-
-#include "theory/quantifiers/inst_gen.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/model_builder.h"
-#include "theory/quantifiers/first_order_model.h"
-
-//#define CHILD_USE_CONSIDER
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-
-
-InstGenProcess::InstGenProcess( Node n ) : d_node( n ){
- Assert( n.hasAttribute(InstConstantAttribute()) );
- int count = 0;
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){
- d_children.push_back( InstGenProcess( n[i] ) );
- d_children_index.push_back( i );
- d_children_map[ i ] = count;
- count++;
- }
- }
-}
-
-void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){
- if( !qe->existsInstantiation( f, m, true ) ){
- //make sure no duplicates are produced
- if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){
- d_match_values.push_back( val );
- d_matches.push_back( InstMatch( &m ) );
- qe->getModelEngine()->getModelBuilder()->d_instGenMatches++;
- }
- }
-}
-
-void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){
- Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;
- //whether we are doing a product or sum or matches
- bool doProduct = true;
- //get the model
- FirstOrderModel* fm = qe->getModel();
-
- //calculate terms we will consider
- std::vector< Node > considerTerms;
- std::vector< std::vector< Node > > newConsiderVal;
- std::vector< bool > newUseConsider;
- std::map< Node, InstMatch > considerTermsMatch[2];
- std::map< Node, bool > considerTermsSuccess[2];
- newConsiderVal.resize( d_children.size() );
- newUseConsider.resize( d_children.size(), useConsider );
- if( d_node.getKind()==APPLY_UF ){
- Node op = d_node.getOperator();
- if( useConsider ){
-#ifndef CHILD_USE_CONSIDER
- for( size_t i=0; i<newUseConsider.size(); i++ ){
- newUseConsider[i] = false;
- }
-#endif
- for( size_t i=0; i<considerVal.size(); i++ ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ),
- qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en.getKind()==APPLY_UF && en.getOperator()==op ){
- considerTerms.push_back( en );
- }
- ++eqc;
- }
- }
- }else{
- considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() );
- }
- //for each term we consider, calculate a current match
- for( size_t i=0; i<considerTerms.size(); i++ ){
- Node n = considerTerms[i];
- bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
- bool hadSuccess CVC4_UNUSED = false;
- for( int t=(isSelected ? 0 : 1); t<2; t++ ){
- if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
- considerTermsMatch[t][n] = InstMatch();
- considerTermsSuccess[t][n] = true;
- for( size_t j=0; j<d_node.getNumChildren(); j++ ){
- if( d_children_map.find( j )==d_children_map.end() ){
- if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
- if( d_node[j].getKind()==INST_CONSTANT ){
- if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){
- Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";
- Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl;
- considerTermsSuccess[t][n] = false;
- break;
- }
- }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){
- Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;
- considerTermsSuccess[t][n] = false;
- break;
- }
- }
- }
- }
- //if successful, store it
- if( considerTermsSuccess[t][n] ){
-#ifdef CHILD_USE_CONSIDER
- if( !hadSuccess ){
- hadSuccess = true;
- for( size_t k=0; k<d_children.size(); k++ ){
- if( newUseConsider[k] ){
- int childIndex = d_children_index[k];
- //determine if we are restricted or not
- if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){
- Node r = qe->getModel()->getRepresentative( n[childIndex] );
- if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){
- newConsiderVal[k].push_back( r );
- //check if we now need to consider the entire domain
- TypeNode tn = r.getType();
- if( qe->getModel()->d_rep_set.hasType( tn ) ){
- if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){
- newConsiderVal[k].clear();
- newUseConsider[k] = false;
- }
- }
- }
- }else{
- //matching against selected term, will need to consider all values
- newConsiderVal[k].clear();
- newUseConsider[k] = false;
- }
- }
- }
- }
-#endif
- }
- }
- }
- }
- }else{
- //the interpretted case
- if( d_node.getType().isBoolean() ){
- if( useConsider ){
- //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; }
- Assert( considerVal.size()==1 );
- bool reqPol = considerVal[0]==fm->d_true;
- Node ncv = considerVal[0];
- if( d_node.getKind()==NOT ){
- ncv = reqPol ? fm->d_false : fm->d_true;
- }
- if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){
- for( size_t i=0; i<newConsiderVal.size(); i++ ){
- newConsiderVal[i].push_back( ncv );
- }
- //instead we will do a sum
- if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol ) ){
- doProduct = false;
- }
- }else{
- //do not use consider
- for( size_t i=0; i<newUseConsider.size(); i++ ){
- newUseConsider[i] = false;
- }
- }
- }
- }
- }
-
- //calculate all matches for children
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i].calculateMatches( qe, f, newConsiderVal[i], newUseConsider[i] );
- if( doProduct && d_children[i].getNumMatches()==0 ){
- return;
- }
- }
- if( d_node.getKind()==APPLY_UF ){
- //if this is an uninterpreted function
- Node op = d_node.getOperator();
- //process all values
- for( size_t i=0; i<considerTerms.size(); i++ ){
- Node n = considerTerms[i];
- bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
- for( int t=(isSelected ? 0 : 1); t<2; t++ ){
- //do not consider ground case if it is already congruent to another ground term
- if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
- Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;
- if( considerTermsSuccess[t][n] ){
- //try to find unifier for d_node = n
- calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 );
- }
- }
- }
- }
- }else{
- //if this is an interpreted function
- if( doProduct ){
- //combining children matches
- InstMatch curr;
- std::vector< Node > terms;
- calculateMatchesInterpreted( qe, f, curr, terms, 0 );
- }else{
- //summing children matches
- Assert( considerVal.size()==1 );
- for( int i=0; i<(int)d_children.size(); i++ ){
- for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){
- InstMatch m;
- if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){
- addMatchValue( qe, f, considerVal[0], m );
- }
- }
- }
- }
- }
- Trace("inst-gen-cm") << "done calculate matches" << std::endl;
- //can clear information used for finding duplicates
- d_inst_trie.clear();
-}
-
-bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){
- //FIXME: is this correct? (query may not be accurate)
- return m.merge( q, d_matches[i] );
-}
-
-void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){
- if( childIndex==(int)d_children.size() ){
- Node val = qe->getModel()->getRepresentative( n ); //FIXME: is this correct?
- Trace("inst-gen-cm") << " - u-match : " << val << std::endl;
- Trace("inst-gen-cm") << " : " << curr << std::endl;
- addMatchValue( qe, f, val, curr );
- }else{
- Trace("inst-gen-cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl;
- bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) );
- for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){
- //FIXME: is this correct?
- if( sel || qe->getEqualityQuery()->areEqual( d_children[ childIndex ].getMatchValue( i ), n[d_children_index[childIndex]] ) ){
- InstMatch next( &curr );
- if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){
- calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected );
- }else{
- Trace("inst-gen-cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl;
- Trace("inst-gen-cm") << childIndex << " match " << i << " not equal subs." << std::endl;
- }
- }else{
- Trace("inst-gen-cm") << childIndex << " match " << i << " not equal value." << std::endl;
- }
- }
- }
-}
-
-void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ){
- FirstOrderModel* fm = qe->getModel();
- if( argIndex==(int)d_node.getNumChildren() ){
- Node val;
- if( d_node.getNumChildren()==0 ){
- val = d_node;
- }else if( d_node.getKind()==EQUAL ){
- val = qe->getEqualityQuery()->areEqual( terms[0], terms[1] ) ? fm->d_true : fm->d_false;
- }else{
- val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms );
- val = Rewriter::rewrite( val );
- }
- Trace("inst-gen-cm") << " - i-match : " << d_node << std::endl;
- Trace("inst-gen-cm") << " : " << val << std::endl;
- Trace("inst-gen-cm") << " : " << curr << std::endl;
- addMatchValue( qe, f, val, curr );
- }else{
- if( d_children_map.find( argIndex )==d_children_map.end() ){
- terms.push_back( fm->getRepresentative( d_node[argIndex] ) );
- calculateMatchesInterpreted( qe, f, curr, terms, argIndex+1 );
- terms.pop_back();
- }else{
- for( int i=0; i<(int)d_children[ d_children_map[argIndex] ].getNumMatches(); i++ ){
- InstMatch next( &curr );
- if( d_children[ d_children_map[argIndex] ].getMatch( qe->getEqualityQuery(), i, next ) ){
- terms.push_back( d_children[ d_children_map[argIndex] ].getMatchValue( i ) );
- calculateMatchesInterpreted( qe, f, next, terms, argIndex+1 );
- terms.pop_back();
- }
- }
- }
- }
-}
+/********************* */ +/*! \file inst_gen.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of inst gen classes + **/ + +#include "theory/quantifiers/inst_gen.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/first_order_model.h" + +//#define CHILD_USE_CONSIDER + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + + + +InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ + Assert( n.hasAttribute(InstConstantAttribute()) ); + int count = 0; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){ + d_children.push_back( InstGenProcess( n[i] ) ); + d_children_index.push_back( i ); + d_children_map[ i ] = count; + count++; + } + } +} + +void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){ + if( !qe->existsInstantiation( f, m, true ) ){ + //make sure no duplicates are produced + if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ + d_match_values.push_back( val ); + d_matches.push_back( InstMatch( &m ) ); + qe->getModelEngine()->getModelBuilder()->d_instGenMatches++; + } + } +} + +void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){ + Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl; + //whether we are doing a product or sum or matches + bool doProduct = true; + //get the model + FirstOrderModel* fm = qe->getModel(); + + //calculate terms we will consider + std::vector< Node > considerTerms; + std::vector< std::vector< Node > > newConsiderVal; + std::vector< bool > newUseConsider; + std::map< Node, InstMatch > considerTermsMatch[2]; + std::map< Node, bool > considerTermsSuccess[2]; + newConsiderVal.resize( d_children.size() ); + newUseConsider.resize( d_children.size(), useConsider ); + if( d_node.getKind()==APPLY_UF ){ + Node op = d_node.getOperator(); + if( useConsider ){ +#ifndef CHILD_USE_CONSIDER + for( size_t i=0; i<newUseConsider.size(); i++ ){ + newUseConsider[i] = false; + } +#endif + for( size_t i=0; i<considerVal.size(); i++ ){ + eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ), + qe->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + if( en.getKind()==APPLY_UF && en.getOperator()==op ){ + considerTerms.push_back( en ); + } + ++eqc; + } + } + }else{ + considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() ); + } + //for each term we consider, calculate a current match + for( size_t i=0; i<considerTerms.size(); i++ ){ + Node n = considerTerms[i]; + bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + bool hadSuccess CVC4_UNUSED = false; + for( int t=(isSelected ? 0 : 1); t<2; t++ ){ + if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ + considerTermsMatch[t][n] = InstMatch(); + considerTermsSuccess[t][n] = true; + for( size_t j=0; j<d_node.getNumChildren(); j++ ){ + if( d_children_map.find( j )==d_children_map.end() ){ + if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){ + if( d_node[j].getKind()==INST_CONSTANT ){ + if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){ + Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to "; + Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl; + considerTermsSuccess[t][n] = false; + break; + } + }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){ + Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl; + considerTermsSuccess[t][n] = false; + break; + } + } + } + } + //if successful, store it + if( considerTermsSuccess[t][n] ){ +#ifdef CHILD_USE_CONSIDER + if( !hadSuccess ){ + hadSuccess = true; + for( size_t k=0; k<d_children.size(); k++ ){ + if( newUseConsider[k] ){ + int childIndex = d_children_index[k]; + //determine if we are restricted or not + if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){ + Node r = qe->getModel()->getRepresentative( n[childIndex] ); + if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){ + newConsiderVal[k].push_back( r ); + //check if we now need to consider the entire domain + TypeNode tn = r.getType(); + if( qe->getModel()->d_rep_set.hasType( tn ) ){ + if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){ + newConsiderVal[k].clear(); + newUseConsider[k] = false; + } + } + } + }else{ + //matching against selected term, will need to consider all values + newConsiderVal[k].clear(); + newUseConsider[k] = false; + } + } + } + } +#endif + } + } + } + } + }else{ + //the interpretted case + if( d_node.getType().isBoolean() ){ + if( useConsider ){ + //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; } + Assert( considerVal.size()==1 ); + bool reqPol = considerVal[0]==fm->d_true; + Node ncv = considerVal[0]; + if( d_node.getKind()==NOT ){ + ncv = reqPol ? fm->d_false : fm->d_true; + } + if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){ + for( size_t i=0; i<newConsiderVal.size(); i++ ){ + newConsiderVal[i].push_back( ncv ); + } + //instead we will do a sum + if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol ) ){ + doProduct = false; + } + }else{ + //do not use consider + for( size_t i=0; i<newUseConsider.size(); i++ ){ + newUseConsider[i] = false; + } + } + } + } + } + + //calculate all matches for children + for( int i=0; i<(int)d_children.size(); i++ ){ + d_children[i].calculateMatches( qe, f, newConsiderVal[i], newUseConsider[i] ); + if( doProduct && d_children[i].getNumMatches()==0 ){ + return; + } + } + if( d_node.getKind()==APPLY_UF ){ + //if this is an uninterpreted function + Node op = d_node.getOperator(); + //process all values + for( size_t i=0; i<considerTerms.size(); i++ ){ + Node n = considerTerms[i]; + bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + for( int t=(isSelected ? 0 : 1); t<2; t++ ){ + //do not consider ground case if it is already congruent to another ground term + if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ + Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl; + if( considerTermsSuccess[t][n] ){ + //try to find unifier for d_node = n + calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 ); + } + } + } + } + }else{ + //if this is an interpreted function + if( doProduct ){ + //combining children matches + InstMatch curr; + std::vector< Node > terms; + calculateMatchesInterpreted( qe, f, curr, terms, 0 ); + }else{ + //summing children matches + Assert( considerVal.size()==1 ); + for( int i=0; i<(int)d_children.size(); i++ ){ + for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){ + InstMatch m; + if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){ + addMatchValue( qe, f, considerVal[0], m ); + } + } + } + } + } + Trace("inst-gen-cm") << "done calculate matches" << std::endl; + //can clear information used for finding duplicates + d_inst_trie.clear(); +} + +bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){ + //FIXME: is this correct? (query may not be accurate) + return m.merge( q, d_matches[i] ); +} + +void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){ + if( childIndex==(int)d_children.size() ){ + Node val = qe->getModel()->getRepresentative( n ); //FIXME: is this correct? + Trace("inst-gen-cm") << " - u-match : " << val << std::endl; + Trace("inst-gen-cm") << " : " << curr << std::endl; + addMatchValue( qe, f, val, curr ); + }else{ + Trace("inst-gen-cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl; + bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) ); + for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){ + //FIXME: is this correct? + if( sel || qe->getEqualityQuery()->areEqual( d_children[ childIndex ].getMatchValue( i ), n[d_children_index[childIndex]] ) ){ + InstMatch next( &curr ); + if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){ + calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected ); + }else{ + Trace("inst-gen-cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl; + Trace("inst-gen-cm") << childIndex << " match " << i << " not equal subs." << std::endl; + } + }else{ + Trace("inst-gen-cm") << childIndex << " match " << i << " not equal value." << std::endl; + } + } + } +} + +void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ){ + FirstOrderModel* fm = qe->getModel(); + if( argIndex==(int)d_node.getNumChildren() ){ + Node val; + if( d_node.getNumChildren()==0 ){ + val = d_node; + }else if( d_node.getKind()==EQUAL ){ + val = qe->getEqualityQuery()->areEqual( terms[0], terms[1] ) ? fm->d_true : fm->d_false; + }else{ + val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms ); + val = Rewriter::rewrite( val ); + } + Trace("inst-gen-cm") << " - i-match : " << d_node << std::endl; + Trace("inst-gen-cm") << " : " << val << std::endl; + Trace("inst-gen-cm") << " : " << curr << std::endl; + addMatchValue( qe, f, val, curr ); + }else{ + if( d_children_map.find( argIndex )==d_children_map.end() ){ + terms.push_back( fm->getRepresentative( d_node[argIndex] ) ); + calculateMatchesInterpreted( qe, f, curr, terms, argIndex+1 ); + terms.pop_back(); + }else{ + for( int i=0; i<(int)d_children[ d_children_map[argIndex] ].getNumMatches(); i++ ){ + InstMatch next( &curr ); + if( d_children[ d_children_map[argIndex] ].getMatch( qe->getEqualityQuery(), i, next ) ){ + terms.push_back( d_children[ d_children_map[argIndex] ].getMatchValue( i ) ); + calculateMatchesInterpreted( qe, f, next, terms, argIndex+1 ); + terms.pop_back(); + } + } + } + } +} diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h index f6e6a372e..c8de2c642 100755 --- a/src/theory/quantifiers/inst_gen.h +++ b/src/theory/quantifiers/inst_gen.h @@ -1,61 +1,61 @@ -/********************* */
-/*! \file inst_gen.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Inst Gen classes
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_GEN_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_GEN_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/inst_match.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class InstGenProcess
-{
-private:
- //the node we are processing
- Node d_node;
- //the sub children for this node
- std::vector< InstGenProcess > d_children;
- std::vector< int > d_children_index;
- std::map< int, int > d_children_map;
- //the matches we have produced
- std::vector< InstMatch > d_matches;
- std::vector< Node > d_match_values;
- //add match value
- std::map< Node, inst::InstMatchTrie > d_inst_trie;
- void addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m );
-private:
- void calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected );
- void calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex );
-public:
- InstGenProcess( Node n );
- virtual ~InstGenProcess(){}
-
- void calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider );
- int getNumMatches() { return d_matches.size(); }
- bool getMatch( EqualityQuery* q, int i, InstMatch& m );
- Node getMatchValue( int i ) { return d_match_values[i]; }
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file inst_gen.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Inst Gen classes + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_GEN_H +#define __CVC4__THEORY__QUANTIFIERS__INST_GEN_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/inst_match.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class InstGenProcess +{ +private: + //the node we are processing + Node d_node; + //the sub children for this node + std::vector< InstGenProcess > d_children; + std::vector< int > d_children_index; + std::map< int, int > d_children_map; + //the matches we have produced + std::vector< InstMatch > d_matches; + std::vector< Node > d_match_values; + //add match value + std::map< Node, inst::InstMatchTrie > d_inst_trie; + void addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ); +private: + void calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ); + void calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ); +public: + InstGenProcess( Node n ); + virtual ~InstGenProcess(){} + + void calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ); + int getNumMatches() { return d_matches.size(); } + bool getMatch( EqualityQuery* q, int i, InstMatch& m ); + Node getMatchValue( int i ) { return d_match_values[i]; } +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 3b5e594fb..2822597e1 100755 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -1,664 +1,664 @@ -/********************* */
-/*! \file inst_match_generator.cpp
-** \verbatim
-** Original author: ajreynol
-** Major contributors: bobot
-** Minor contributors (to current version): barrett, mdeters
-** This file is part of the CVC4 prototype.
-** Copyright (c) 2009-2012 New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief Implementation of inst match generator class
-**/
-
-#include "theory/quantifiers/inst_match_generator.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/candidate_generator.h"
-#include "theory/quantifiers_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
-namespace CVC4 {
-namespace theory {
-namespace inst {
-
-
-InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
- initializePattern( pat, qe );
-}
-
-InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
- if( pats.size()==1 ){
- initializePattern( pats[0], qe );
- }else{
- initializePatterns( pats, qe );
- }
-}
-
-void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){
- int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;
- for( int i=0; i<(int)pats.size(); i++ ){
- d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) );
- }
- d_pattern = Node::null();
- d_match_pattern = Node::null();
- d_cg = NULL;
-}
-
-void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
- Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
- Assert( pat.hasAttribute(InstConstantAttribute()) );
- d_pattern = pat;
- d_match_pattern = pat;
- if( d_match_pattern.getKind()==NOT ){
- //we want to add the children of the NOT
- d_match_pattern = d_pattern[0];
- }
- if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){
- if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){
- Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
- //swap sides
- d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
- d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;
- if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
- d_match_pattern = d_match_pattern[1];
- }else{
- d_match_pattern = d_pattern[0][0];
- }
- }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){
- Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
- if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
- d_match_pattern = d_match_pattern[0];
- }
- }
- }
- int childMatchPolicy = MATCH_GEN_DEFAULT;
- for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
- if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
- if( d_match_pattern[i].getKind()!=INST_CONSTANT ){
- d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) );
- d_children_index.push_back( i );
- }
- }
- }
-
- Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
-
- //create candidate generator
- if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
- Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
- //we will be producing candidates via literal matching heuristics
- if( d_pattern.getKind()!=NOT ){
- //candidates will be all equalities
- d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );
- }else{
- //candidates will be all disequalities
- d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
- }
- }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){
- Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
- if( d_pattern.getKind()==NOT ){
- Unimplemented("Disequal generator unimplemented");
- }else{
- Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
- //we are matching only in a particular equivalence class
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
- //store the equivalence class that we will call d_cg->reset( ... ) on
- d_eq_class = d_pattern[1];
- }
- }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
- //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){
- //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
- //}
- //we will be scanning lists trying to find d_match_pattern.getOperator()
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
- }else{
- d_cg = new CandidateGeneratorQueue;
- if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
- Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
- //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
- d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
- }else{
- Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;
- for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
- Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl;
- }
- //we will treat this as match gen internal arithmetic
- d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC;
- }
- }
-}
-
-/** get match (not modulo equality) */
-bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){
- Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
- << m.size() << ")" << ", " << d_children.size() << std::endl;
- Assert( !d_match_pattern.isNull() );
- if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
- return true;
- }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){
- return getMatchArithmetic( t, m, qe );
- }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){
- return false;
- }else{
- EqualityQuery* q = qe->getEqualityQuery();
- //add m to partial match vector
- std::vector< InstMatch > partial;
- partial.push_back( InstMatch( &m ) );
- //if t is null
- Assert( !t.isNull() );
- Assert( !t.hasAttribute(InstConstantAttribute()) );
- Assert( t.getKind()==d_match_pattern.getKind() );
- Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
- //first, check if ground arguments are not equal, or a match is in conflict
- for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
- if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
- if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){
- //match is in conflict
- Debug("matching-debug") << "Match in conflict " << t[i] << " and "
- << d_match_pattern[i] << " because "
- << partial[0].get(d_match_pattern[i])
- << std::endl;
- Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl;
- return false;
- }
- }
- }else{
- if( !q->areEqual( d_match_pattern[i], t[i] ) ){
- Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
- //ground arguments are not equal
- return false;
- }
- }
- }
- //now, fit children into match
- //we will be requesting candidates for matching terms for each child
- std::vector< Node > reps;
- for( int i=0; i<(int)d_children.size(); i++ ){
- Node rep = q->getRepresentative( t[ d_children_index[i] ] );
- reps.push_back( rep );
- d_children[i]->d_cg->reset( rep );
- }
-
- //combine child matches
- int index = 0;
- while( index>=0 && index<(int)d_children.size() ){
- partial.push_back( InstMatch( &partial[index] ) );
- if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){
- index++;
- }else{
- d_children[index]->d_cg->reset( reps[index] );
- partial.pop_back();
- if( !partial.empty() ){
- partial.pop_back();
- }
- index--;
- }
- }
- if( index>=0 ){
- m = partial.back();
- return true;
- }else{
- return false;
- }
- }
-}
-
-bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){
- bool success = false;
- Node t;
- do{
- //get the next candidate term t
- t = d_cg->getNextCandidate();
- //if t not null, try to fit it into match m
- if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
- success = getMatch( t, m, qe );
- }
- }while( !success && !t.isNull() );
- if (saveMatched) m.d_matched = t;
- return success;
-}
-
-bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){
- Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl;
- if( !d_arith_coeffs.empty() ){
- NodeBuilder<> tb(kind::PLUS);
- Node ic = Node::null();
- for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
- Debug("matching-arith") << it->first << " -> " << it->second << std::endl;
- if( !it->first.isNull() ){
- if( m.find( it->first )==m.end() ){
- //see if we can choose this to set
- if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){
- ic = it->first;
- }
- }else{
- Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;
- Node tm = m.get( it->first );
- if( !it->second.isNull() ){
- tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );
- }
- tb << tm;
- }
- }else{
- tb << it->second;
- }
- }
- if( !ic.isNull() ){
- Node tm;
- if( tb.getNumChildren()==0 ){
- tm = t;
- }else{
- tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
- tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );
- }
- if( !d_arith_coeffs[ ic ].isNull() ){
- Assert( !ic.getType().isInteger() );
- Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );
- tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );
- }
- m.set( ic, Rewriter::rewrite( tm ));
- //set the rest to zeros
- for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
- if( !it->first.isNull() ){
- if( m.find( it->first )==m.end() ){
- m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) );
- }
- }
- }
- Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;
- return true;
- }else{
- return false;
- }
- }else{
- return false;
- }
-}
-
-
-/** reset instantiation round */
-void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
- if( d_match_pattern.isNull() ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->resetInstantiationRound( qe );
- }
- }else{
- if( d_cg ){
- d_cg->resetInstantiationRound();
- }
- }
-}
-
-void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
- if( d_match_pattern.isNull() ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->reset( eqc, qe );
- }
- d_partial.clear();
- }else{
- if( !d_eq_class.isNull() ){
- //we have a specific equivalence class in mind
- //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
- //just look in equivalence class of the RHS
- d_cg->reset( d_eq_class );
- }else{
- d_cg->reset( eqc );
- }
- }
-}
-
-bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
- m.d_matched = Node::null();
- if( d_match_pattern.isNull() ){
- int index = (int)d_partial.size();
- while( index>=0 && index<(int)d_children.size() ){
- if( index>0 ){
- d_partial.push_back( InstMatch( &d_partial[index-1] ) );
- }else{
- d_partial.push_back( InstMatch() );
- }
- if( d_children[index]->getNextMatch( d_partial[index], qe ) ){
- index++;
- }else{
- d_children[index]->reset( Node::null(), qe );
- d_partial.pop_back();
- if( !d_partial.empty() ){
- d_partial.pop_back();
- }
- index--;
- }
- }
- if( index>=0 ){
- m = d_partial.back();
- d_partial.pop_back();
- return true;
- }else{
- return false;
- }
- }else{
- bool res = getNextMatch2( m, qe, true );
- Assert(!res || !m.d_matched.isNull());
- return res;
- }
-}
-
-
-
-int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
- //now, try to add instantiation for each match produced
- int addedLemmas = 0;
- InstMatch m;
- while( getNextMatch( m, qe ) ){
- //m.makeInternal( d_quantEngine->getEqualityQuery() );
- m.add( baseMatch );
- if( qe->addInstantiation( f, m ) ){
- addedLemmas++;
- if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){
- return addedLemmas;
- }
- }
- m.clear();
- }
- //return number of lemmas added
- return addedLemmas;
-}
-
-int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
- Assert( options::eagerInstQuant() );
- if( !d_match_pattern.isNull() ){
- InstMatch m;
- if( getMatch( t, m, qe ) ){
- if( qe->addInstantiation( f, m ) ){
- return 1;
- }
- }
- }else{
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->addTerm( f, t, qe );
- }
- }
- return 0;
-}
-
-/** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :
-d_f( f ){
- Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
- std::map< Node, std::vector< Node > > var_contains;
- qe->getTermDatabase()->getVarContains( f, pats, var_contains );
- //convert to indicies
- for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
- Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
- for( int i=0; i<(int)it->second.size(); i++ ){
- Debug("smart-multi-trigger") << it->second[i] << " ";
- int index = it->second[i].getAttribute(InstVarNumAttribute());
- d_var_contains[ it->first ].push_back( index );
- d_var_to_node[ index ].push_back( it->first );
- }
- Debug("smart-multi-trigger") << std::endl;
- }
- for( int i=0; i<(int)pats.size(); i++ ){
- Node n = pats[i];
- //make the match generator
- d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) );
- //compute unique/shared variables
- std::vector< int > unique_vars;
- std::map< int, bool > shared_vars;
- int numSharedVars = 0;
- for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
- if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
- Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
- unique_vars.push_back( d_var_contains[n][j] );
- }else{
- shared_vars[ d_var_contains[n][j] ] = true;
- numSharedVars++;
- }
- }
- //we use the latest shared variables, then unique variables
- std::vector< int > vars;
- int index = i==0 ? (int)(pats.size()-1) : (i-1);
- while( numSharedVars>0 && index!=i ){
- for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
- if( it->second ){
- if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
- d_var_contains[ pats[index] ].end() ){
- vars.push_back( it->first );
- shared_vars[ it->first ] = false;
- numSharedVars--;
- }
- }
- }
- index = index==0 ? (int)(pats.size()-1) : (index-1);
- }
- vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
- Debug("smart-multi-trigger") << " Index[" << i << "]: ";
- for( int i=0; i<(int)vars.size(); i++ ){
- Debug("smart-multi-trigger") << vars[i] << " ";
- }
- Debug("smart-multi-trigger") << std::endl;
- //make ordered inst match trie
- InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;
- imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );
- d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );
- }
-
-}
-
-/** reset instantiation round (call this whenever equivalence classes have changed) */
-void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->resetInstantiationRound( qe );
- }
-}
-
-/** reset, eqc is the equivalence class to search in (any if eqc=null) */
-void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->reset( eqc, qe );
- }
-}
-
-int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
- int addedLemmas = 0;
- Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
- for( int i=0; i<(int)d_children.size(); i++ ){
- Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
- std::vector< InstMatch > newMatches;
- InstMatch m;
- while( d_children[i]->getNextMatch( m, qe ) ){
- m.makeRepresentative( qe );
- newMatches.push_back( InstMatch( &m ) );
- m.clear();
- }
- for( int j=0; j<(int)newMatches.size(); j++ ){
- processNewMatch( qe, newMatches[j], i, addedLemmas );
- }
- }
- return addedLemmas;
-}
-
-void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
- //see if these produce new matches
- d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );
- //possibly only do the following if we know that new matches will be produced?
- //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
- // we can safely skip the following lines, even when we have already produced this match.
- Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;
- //process new instantiations
- int childIndex = (fromChildIndex+1)%(int)d_children.size();
- std::vector< IndexedTrie > unique_var_tries;
- processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),
- unique_var_tries, 0, childIndex, fromChildIndex, true );
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
- std::vector< IndexedTrie >& unique_var_tries,
- int trieIndex, int childIndex, int endChildIndex, bool modEq ){
- if( childIndex==endChildIndex ){
- //now, process unique variables
- processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
- }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
- int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
- if( m.find( curr_ic )==m.end() ){
- //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME
- // //unique variable(s), defer calculation
- // unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
- // int newChildIndex = (childIndex+1)%(int)d_children.size();
- // processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
- // 0, newChildIndex, endChildIndex, modEq );
- //}else{
- //shared and non-set variable, add to InstMatch
- for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
- InstMatch mn( &m );
- mn.set( curr_ic, it->first);
- processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
- }
- //}
- }else{
- //shared and set variable, try to merge
- Node n = m.get( curr_ic );
- std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );
- if( it!=tr->d_data.end() ){
- processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
- }
- if( modEq ){
- //check modulo equality for other possible instantiations
- if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
- qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en!=n ){
- std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en );
- if( itc!=tr->d_data.end() ){
- processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
- }
- }
- ++eqc;
- }
- }
- }
- }
- }else{
- int newChildIndex = (childIndex+1)%(int)d_children.size();
- processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
- 0, newChildIndex, endChildIndex, modEq );
- }
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
- std::vector< IndexedTrie >& unique_var_tries,
- int uvtIndex, InstMatchTrie* tr, int trieIndex ){
- if( uvtIndex<(int)unique_var_tries.size() ){
- int childIndex = unique_var_tries[uvtIndex].first.first;
- if( !tr ){
- tr = unique_var_tries[uvtIndex].second;
- trieIndex = unique_var_tries[uvtIndex].first.second;
- }
- if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
- int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
- //unique non-set variable, add to InstMatch
- for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
- InstMatch mn( &m );
- mn.set( curr_ic, it->first);
- processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
- }
- }else{
- processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
- }
- }else{
- //m is an instantiation
- if( qe->addInstantiation( d_f, m ) ){
- addedLemmas++;
- Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
- }
- }
-}
-
-int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
- Assert( options::eagerInstQuant() );
- int addedLemmas = 0;
- for( int i=0; i<(int)d_children.size(); i++ ){
- if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){
- InstMatch m;
- //if it produces a match, then process it with the rest
- if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){
- processNewMatch( qe, m, i, addedLemmas );
- }
- }
- }
- return addedLemmas;
-}
-
-int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
- InstMatch m;
- m.add( baseMatch );
- int addedLemmas = 0;
- if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){
- for( int i=0; i<2; i++ ){
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) );
- }
- }else{
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );
- }
- return addedLemmas;
-}
-
-void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
- if( argIndex==(int)d_match_pattern.getNumChildren() ){
- //m is an instantiation
- if( qe->addInstantiation( d_f, m ) ){
- addedLemmas++;
- Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;
- }
- }else{
- if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
- Node ic = d_match_pattern[argIndex];
- for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
- Node t = it->first;
- if( ( m.get( ic ).isNull() || m.get( ic )==t ) && ic.getType()==t.getType() ){
- Node prev = m.get( ic );
- m.set( ic, t);
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
- m.set( ic, prev);
- }
- }
- }else{
- Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
- std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
- if( it!=tat->d_data.end() ){
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
- }
- }
- }
-}
-
-int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
- Assert( options::eagerInstQuant() );
- InstMatch m;
- for( int i=0; i<(int)t.getNumChildren(); i++ ){
- if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- m.set(d_match_pattern[i], t[i]);
- }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
- return 0;
- }
- }
- return qe->addInstantiation( f, m ) ? 1 : 0;
-}
-
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+/********************* */ +/*! \file inst_match_generator.cpp +** \verbatim +** Original author: ajreynol +** Major contributors: bobot +** Minor contributors (to current version): barrett, mdeters +** This file is part of the CVC4 prototype. +** Copyright (c) 2009-2012 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief Implementation of inst match generator class +**/ + +#include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; + +namespace CVC4 { +namespace theory { +namespace inst { + + +InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){ + initializePattern( pat, qe ); +} + +InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){ + if( pats.size()==1 ){ + initializePattern( pats[0], qe ); + }else{ + initializePatterns( pats, qe ); + } +} + +void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){ + int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy; + for( int i=0; i<(int)pats.size(); i++ ){ + d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) ); + } + d_pattern = Node::null(); + d_match_pattern = Node::null(); + d_cg = NULL; +} + +void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ + Debug("inst-match-gen") << "Pattern term is " << pat << std::endl; + Assert( pat.hasAttribute(InstConstantAttribute()) ); + d_pattern = pat; + d_match_pattern = pat; + if( d_match_pattern.getKind()==NOT ){ + //we want to add the children of the NOT + d_match_pattern = d_pattern[0]; + } + if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){ + if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){ + Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) ); + //swap sides + d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); + d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern; + if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching + d_match_pattern = d_match_pattern[1]; + }else{ + d_match_pattern = d_pattern[0][0]; + } + }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){ + Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) ); + if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching + d_match_pattern = d_match_pattern[0]; + } + } + } + int childMatchPolicy = MATCH_GEN_DEFAULT; + for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ + if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( d_match_pattern[i].getKind()!=INST_CONSTANT ){ + d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) ); + d_children_index.push_back( i ); + } + } + } + + Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; + + //create candidate generator + if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); + //we will be producing candidates via literal matching heuristics + if( d_pattern.getKind()!=NOT ){ + //candidates will be all equalities + d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern ); + }else{ + //candidates will be all disequalities + d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); + } + }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){ + Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); + if( d_pattern.getKind()==NOT ){ + Unimplemented("Disequal generator unimplemented"); + }else{ + Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); + //we are matching only in a particular equivalence class + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); + //store the equivalence class that we will call d_cg->reset( ... ) on + d_eq_class = d_pattern[1]; + } + }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ + //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ + //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; + //} + //we will be scanning lists trying to find d_match_pattern.getOperator() + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); + }else{ + d_cg = new CandidateGeneratorQueue; + if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ + Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; + //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; + d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; + }else{ + Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl; + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; + } + //we will treat this as match gen internal arithmetic + d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC; + } + } +} + +/** get match (not modulo equality) */ +bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){ + Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" + << m.size() << ")" << ", " << d_children.size() << std::endl; + Assert( !d_match_pattern.isNull() ); + if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ + return true; + }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){ + return getMatchArithmetic( t, m, qe ); + }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ + return false; + }else{ + EqualityQuery* q = qe->getEqualityQuery(); + //add m to partial match vector + std::vector< InstMatch > partial; + partial.push_back( InstMatch( &m ) ); + //if t is null + Assert( !t.isNull() ); + Assert( !t.hasAttribute(InstConstantAttribute()) ); + Assert( t.getKind()==d_match_pattern.getKind() ); + Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() ); + //first, check if ground arguments are not equal, or a match is in conflict + for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ + if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( d_match_pattern[i].getKind()==INST_CONSTANT ){ + if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){ + //match is in conflict + Debug("matching-debug") << "Match in conflict " << t[i] << " and " + << d_match_pattern[i] << " because " + << partial[0].get(d_match_pattern[i]) + << std::endl; + Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl; + return false; + } + } + }else{ + if( !q->areEqual( d_match_pattern[i], t[i] ) ){ + Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; + //ground arguments are not equal + return false; + } + } + } + //now, fit children into match + //we will be requesting candidates for matching terms for each child + std::vector< Node > reps; + for( int i=0; i<(int)d_children.size(); i++ ){ + Node rep = q->getRepresentative( t[ d_children_index[i] ] ); + reps.push_back( rep ); + d_children[i]->d_cg->reset( rep ); + } + + //combine child matches + int index = 0; + while( index>=0 && index<(int)d_children.size() ){ + partial.push_back( InstMatch( &partial[index] ) ); + if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){ + index++; + }else{ + d_children[index]->d_cg->reset( reps[index] ); + partial.pop_back(); + if( !partial.empty() ){ + partial.pop_back(); + } + index--; + } + } + if( index>=0 ){ + m = partial.back(); + return true; + }else{ + return false; + } + } +} + +bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){ + bool success = false; + Node t; + do{ + //get the next candidate term t + t = d_cg->getNextCandidate(); + //if t not null, try to fit it into match m + if( !t.isNull() && t.getType()==d_match_pattern.getType() ){ + success = getMatch( t, m, qe ); + } + }while( !success && !t.isNull() ); + if (saveMatched) m.d_matched = t; + return success; +} + +bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){ + Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl; + if( !d_arith_coeffs.empty() ){ + NodeBuilder<> tb(kind::PLUS); + Node ic = Node::null(); + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + Debug("matching-arith") << it->first << " -> " << it->second << std::endl; + if( !it->first.isNull() ){ + if( m.find( it->first )==m.end() ){ + //see if we can choose this to set + if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){ + ic = it->first; + } + }else{ + Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl; + Node tm = m.get( it->first ); + if( !it->second.isNull() ){ + tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm ); + } + tb << tm; + } + }else{ + tb << it->second; + } + } + if( !ic.isNull() ){ + Node tm; + if( tb.getNumChildren()==0 ){ + tm = t; + }else{ + tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; + tm = NodeManager::currentNM()->mkNode( MINUS, t, tm ); + } + if( !d_arith_coeffs[ ic ].isNull() ){ + Assert( !ic.getType().isInteger() ); + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() ); + tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm ); + } + m.set( ic, Rewriter::rewrite( tm )); + //set the rest to zeros + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + if( !it->first.isNull() ){ + if( m.find( it->first )==m.end() ){ + m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) ); + } + } + } + Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl; + return true; + }else{ + return false; + } + }else{ + return false; + } +} + + +/** reset instantiation round */ +void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ + if( d_match_pattern.isNull() ){ + for( int i=0; i<(int)d_children.size(); i++ ){ + d_children[i]->resetInstantiationRound( qe ); + } + }else{ + if( d_cg ){ + d_cg->resetInstantiationRound(); + } + } +} + +void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ + if( d_match_pattern.isNull() ){ + for( int i=0; i<(int)d_children.size(); i++ ){ + d_children[i]->reset( eqc, qe ); + } + d_partial.clear(); + }else{ + if( !d_eq_class.isNull() ){ + //we have a specific equivalence class in mind + //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term + //just look in equivalence class of the RHS + d_cg->reset( d_eq_class ); + }else{ + d_cg->reset( eqc ); + } + } +} + +bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + m.d_matched = Node::null(); + if( d_match_pattern.isNull() ){ + int index = (int)d_partial.size(); + while( index>=0 && index<(int)d_children.size() ){ + if( index>0 ){ + d_partial.push_back( InstMatch( &d_partial[index-1] ) ); + }else{ + d_partial.push_back( InstMatch() ); + } + if( d_children[index]->getNextMatch( d_partial[index], qe ) ){ + index++; + }else{ + d_children[index]->reset( Node::null(), qe ); + d_partial.pop_back(); + if( !d_partial.empty() ){ + d_partial.pop_back(); + } + index--; + } + } + if( index>=0 ){ + m = d_partial.back(); + d_partial.pop_back(); + return true; + }else{ + return false; + } + }else{ + bool res = getNextMatch2( m, qe, true ); + Assert(!res || !m.d_matched.isNull()); + return res; + } +} + + + +int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ + //now, try to add instantiation for each match produced + int addedLemmas = 0; + InstMatch m; + while( getNextMatch( m, qe ) ){ + //m.makeInternal( d_quantEngine->getEqualityQuery() ); + m.add( baseMatch ); + if( qe->addInstantiation( f, m ) ){ + addedLemmas++; + if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){ + return addedLemmas; + } + } + m.clear(); + } + //return number of lemmas added + return addedLemmas; +} + +int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ + Assert( options::eagerInstQuant() ); + if( !d_match_pattern.isNull() ){ + InstMatch m; + if( getMatch( t, m, qe ) ){ + if( qe->addInstantiation( f, m ) ){ + return 1; + } + } + }else{ + for( int i=0; i<(int)d_children.size(); i++ ){ + d_children[i]->addTerm( f, t, qe ); + } + } + return 0; +} + +/** constructors */ +InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) : +d_f( f ){ + Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl; + std::map< Node, std::vector< Node > > var_contains; + qe->getTermDatabase()->getVarContains( f, pats, var_contains ); + //convert to indicies + for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){ + Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: "; + for( int i=0; i<(int)it->second.size(); i++ ){ + Debug("smart-multi-trigger") << it->second[i] << " "; + int index = it->second[i].getAttribute(InstVarNumAttribute()); + d_var_contains[ it->first ].push_back( index ); + d_var_to_node[ index ].push_back( it->first ); + } + Debug("smart-multi-trigger") << std::endl; + } + for( int i=0; i<(int)pats.size(); i++ ){ + Node n = pats[i]; + //make the match generator + d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) ); + //compute unique/shared variables + std::vector< int > unique_vars; + std::map< int, bool > shared_vars; + int numSharedVars = 0; + for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ + if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){ + Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl; + unique_vars.push_back( d_var_contains[n][j] ); + }else{ + shared_vars[ d_var_contains[n][j] ] = true; + numSharedVars++; + } + } + //we use the latest shared variables, then unique variables + std::vector< int > vars; + int index = i==0 ? (int)(pats.size()-1) : (i-1); + while( numSharedVars>0 && index!=i ){ + for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){ + if( it->second ){ + if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!= + d_var_contains[ pats[index] ].end() ){ + vars.push_back( it->first ); + shared_vars[ it->first ] = false; + numSharedVars--; + } + } + } + index = index==0 ? (int)(pats.size()-1) : (index-1); + } + vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() ); + Debug("smart-multi-trigger") << " Index[" << i << "]: "; + for( int i=0; i<(int)vars.size(); i++ ){ + Debug("smart-multi-trigger") << vars[i] << " "; + } + Debug("smart-multi-trigger") << std::endl; + //make ordered inst match trie + InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder; + imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() ); + d_children_trie.push_back( InstMatchTrieOrdered( imtio ) ); + } + +} + +/** reset instantiation round (call this whenever equivalence classes have changed) */ +void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){ + for( int i=0; i<(int)d_children.size(); i++ ){ + d_children[i]->resetInstantiationRound( qe ); + } +} + +/** reset, eqc is the equivalence class to search in (any if eqc=null) */ +void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){ + for( int i=0; i<(int)d_children.size(); i++ ){ + d_children[i]->reset( eqc, qe ); + } +} + +int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ + int addedLemmas = 0; + Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl; + for( int i=0; i<(int)d_children.size(); i++ ){ + Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl; + std::vector< InstMatch > newMatches; + InstMatch m; + while( d_children[i]->getNextMatch( m, qe ) ){ + m.makeRepresentative( qe ); + newMatches.push_back( InstMatch( &m ) ); + m.clear(); + } + for( int j=0; j<(int)newMatches.size(); j++ ){ + processNewMatch( qe, newMatches[j], i, addedLemmas ); + } + } + return addedLemmas; +} + +void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){ + //see if these produce new matches + d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true ); + //possibly only do the following if we know that new matches will be produced? + //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that + // we can safely skip the following lines, even when we have already produced this match. + Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl; + //process new instantiations + int childIndex = (fromChildIndex+1)%(int)d_children.size(); + std::vector< IndexedTrie > unique_var_tries; + processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(), + unique_var_tries, 0, childIndex, fromChildIndex, true ); +} + +void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr, + std::vector< IndexedTrie >& unique_var_tries, + int trieIndex, int childIndex, int endChildIndex, bool modEq ){ + if( childIndex==endChildIndex ){ + //now, process unique variables + processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 ); + }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){ + int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex]; + Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); + if( m.find( curr_ic )==m.end() ){ + //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME + // //unique variable(s), defer calculation + // unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) ); + // int newChildIndex = (childIndex+1)%(int)d_children.size(); + // processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries, + // 0, newChildIndex, endChildIndex, modEq ); + //}else{ + //shared and non-set variable, add to InstMatch + for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){ + InstMatch mn( &m ); + mn.set( curr_ic, it->first); + processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries, + trieIndex+1, childIndex, endChildIndex, modEq ); + } + //} + }else{ + //shared and set variable, try to merge + Node n = m.get( curr_ic ); + std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n ); + if( it!=tr->d_data.end() ){ + processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries, + trieIndex+1, childIndex, endChildIndex, modEq ); + } + if( modEq ){ + //check modulo equality for other possible instantiations + if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), + qe->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + if( en!=n ){ + std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en ); + if( itc!=tr->d_data.end() ){ + processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries, + trieIndex+1, childIndex, endChildIndex, modEq ); + } + } + ++eqc; + } + } + } + } + }else{ + int newChildIndex = (childIndex+1)%(int)d_children.size(); + processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries, + 0, newChildIndex, endChildIndex, modEq ); + } +} + +void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, + std::vector< IndexedTrie >& unique_var_tries, + int uvtIndex, InstMatchTrie* tr, int trieIndex ){ + if( uvtIndex<(int)unique_var_tries.size() ){ + int childIndex = unique_var_tries[uvtIndex].first.first; + if( !tr ){ + tr = unique_var_tries[uvtIndex].second; + trieIndex = unique_var_tries[uvtIndex].first.second; + } + if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){ + int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex]; + Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); + //unique non-set variable, add to InstMatch + for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){ + InstMatch mn( &m ); + mn.set( curr_ic, it->first); + processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 ); + } + }else{ + processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 ); + } + }else{ + //m is an instantiation + if( qe->addInstantiation( d_f, m ) ){ + addedLemmas++; + Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl; + } + } +} + +int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ + Assert( options::eagerInstQuant() ); + int addedLemmas = 0; + for( int i=0; i<(int)d_children.size(); i++ ){ + if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){ + InstMatch m; + //if it produces a match, then process it with the rest + if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){ + processNewMatch( qe, m, i, addedLemmas ); + } + } + } + return addedLemmas; +} + +int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ + InstMatch m; + m.add( baseMatch ); + int addedLemmas = 0; + if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){ + for( int i=0; i<2; i++ ){ + addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) ); + } + }else{ + addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) ); + } + return addedLemmas; +} + +void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){ + if( argIndex==(int)d_match_pattern.getNumChildren() ){ + //m is an instantiation + if( qe->addInstantiation( d_f, m ) ){ + addedLemmas++; + Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl; + } + }else{ + if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){ + Node ic = d_match_pattern[argIndex]; + for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ + Node t = it->first; + if( ( m.get( ic ).isNull() || m.get( ic )==t ) && ic.getType()==t.getType() ){ + Node prev = m.get( ic ); + m.set( ic, t); + addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + m.set( ic, prev); + } + } + }else{ + Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); + std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); + if( it!=tat->d_data.end() ){ + addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + } + } + } +} + +int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ + Assert( options::eagerInstQuant() ); + InstMatch m; + for( int i=0; i<(int)t.getNumChildren(); i++ ){ + if( d_match_pattern[i].getKind()==INST_CONSTANT ){ + m.set(d_match_pattern[i], t[i]); + }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){ + return 0; + } + } + return qe->addInstantiation( f, m ) ? 1 : 0; +} + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index af65e809b..dd3663e0a 100755 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -1,192 +1,192 @@ -/********************* */
-/*! \file inst_match_generator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief inst match generator class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
-
-#include "theory/quantifiers/inst_match.h"
-#include <map>
-
-namespace CVC4 {
-namespace theory {
-
-class QuantifiersEngine;
-namespace quantifiers{
- class TermArgTrie;
-}
-
-namespace inst {
-
-/** base class for producing InstMatch objects */
-class IMGenerator {
-public:
- /** reset instantiation round (call this at beginning of instantiation round) */
- virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
- /** get the next match. must call reset( eqc ) before this function. */
- virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
- /** add instantiations directly */
- virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
- /** add ground term t, called when t is added to term db */
- virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
-};/* class IMGenerator */
-
-class CandidateGenerator;
-
-class InstMatchGenerator : public IMGenerator {
-private:
- /** candidate generator */
- CandidateGenerator* d_cg;
- /** policy to use for matching */
- int d_matchPolicy;
- /** children generators */
- std::vector< InstMatchGenerator* > d_children;
- std::vector< int > d_children_index;
- /** partial vector */
- std::vector< InstMatch > d_partial;
- /** eq class */
- Node d_eq_class;
- /** for arithmetic matching */
- std::map< Node, Node > d_arith_coeffs;
- /** initialize pattern */
- void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );
- void initializePattern( Node pat, QuantifiersEngine* qe );
-public:
- enum {
- //options for producing matches
- MATCH_GEN_DEFAULT = 0,
- MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers
- //others (internally used)
- MATCH_GEN_INTERNAL_ARITHMETIC,
- MATCH_GEN_INTERNAL_ERROR,
- };
-private:
- /** get the next match. must call d_cg->reset( ... ) before using.
- only valid for use where !d_match_pattern.isNull().
- */
- bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );
- /** for arithmetic */
- bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
-public:
- /** get the match against ground term or formula t.
- d_match_pattern and t should have the same shape.
- only valid for use where !d_match_pattern.isNull().
- */
- bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
-
- /** constructors */
- InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );
- InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
- /** destructor */
- ~InstMatchGenerator(){}
- /** The pattern we are producing matches for.
- If null, this is a multi trigger that is merging matches from d_children.
- */
- Node d_pattern;
- /** match pattern */
- Node d_match_pattern;
-public:
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe );
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- void reset( Node eqc, QuantifiersEngine* qe );
- /** get the next match. must call reset( eqc ) before this function. */
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
- /** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGenerator */
-
-/** smart multi-trigger implementation */
-class InstMatchGeneratorMulti : public IMGenerator {
-private:
- /** indexed trie */
- typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
- /** process new match */
- void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
- /** process new instantiations */
- void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
- std::vector< IndexedTrie >& unique_var_tries,
- int trieIndex, int childIndex, int endChildIndex, bool modEq );
- /** process new instantiations 2 */
- void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
- std::vector< IndexedTrie >& unique_var_tries,
- int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
-private:
- /** var contains (variable indices) for each pattern node */
- std::map< Node, std::vector< int > > d_var_contains;
- /** variable indices contained to pattern nodes */
- std::map< int, std::vector< Node > > d_var_to_node;
- /** quantifier to use */
- Node d_f;
- /** policy to use for matching */
- int d_matchPolicy;
- /** children generators */
- std::vector< InstMatchGenerator* > d_children;
- /** inst match tries for each child */
- std::vector< InstMatchTrieOrdered > d_children_trie;
- /** calculate matches */
- void calculateMatches( QuantifiersEngine* qe );
-public:
- /** constructors */
- InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
- /** destructor */
- ~InstMatchGeneratorMulti(){}
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe );
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- void reset( Node eqc, QuantifiersEngine* qe );
- /** get the next match. must call reset( eqc ) before this function. (not implemented) */
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
- /** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorMulti */
-
-/** smart (single)-trigger implementation */
-class InstMatchGeneratorSimple : public IMGenerator {
-private:
- /** quantifier for match term */
- Node d_f;
- /** match term */
- Node d_match_pattern;
- /** add instantiations */
- void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
-public:
- /** constructors */
- InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}
- /** destructor */
- ~InstMatchGeneratorSimple(){}
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe ) {}
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- void reset( Node eqc, QuantifiersEngine* qe ) {}
- /** get the next match. must call reset( eqc ) before this function. (not implemented) */
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
- /** add instantiations */
- int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** add ground term t, possibly add instantiations */
- int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorSimple */
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file inst_match_generator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief inst match generator class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H + +#include "theory/quantifiers/inst_match.h" +#include <map> + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; +namespace quantifiers{ + class TermArgTrie; +} + +namespace inst { + +/** base class for producing InstMatch objects */ +class IMGenerator { +public: + /** reset instantiation round (call this at beginning of instantiation round) */ + virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0; + /** get the next match. must call reset( eqc ) before this function. */ + virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; + /** add instantiations directly */ + virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; + /** add ground term t, called when t is added to term db */ + virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0; +};/* class IMGenerator */ + +class CandidateGenerator; + +class InstMatchGenerator : public IMGenerator { +private: + /** candidate generator */ + CandidateGenerator* d_cg; + /** policy to use for matching */ + int d_matchPolicy; + /** children generators */ + std::vector< InstMatchGenerator* > d_children; + std::vector< int > d_children_index; + /** partial vector */ + std::vector< InstMatch > d_partial; + /** eq class */ + Node d_eq_class; + /** for arithmetic matching */ + std::map< Node, Node > d_arith_coeffs; + /** initialize pattern */ + void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ); + void initializePattern( Node pat, QuantifiersEngine* qe ); +public: + enum { + //options for producing matches + MATCH_GEN_DEFAULT = 0, + MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers + //others (internally used) + MATCH_GEN_INTERNAL_ARITHMETIC, + MATCH_GEN_INTERNAL_ERROR, + }; +private: + /** get the next match. must call d_cg->reset( ... ) before using. + only valid for use where !d_match_pattern.isNull(). + */ + bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false ); + /** for arithmetic */ + bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); +public: + /** get the match against ground term or formula t. + d_match_pattern and t should have the same shape. + only valid for use where !d_match_pattern.isNull(). + */ + bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ); + + /** constructors */ + InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 ); + InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); + /** destructor */ + ~InstMatchGenerator(){} + /** The pattern we are producing matches for. + If null, this is a multi trigger that is merging matches from d_children. + */ + Node d_pattern; + /** match pattern */ + Node d_match_pattern; +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound( QuantifiersEngine* qe ); + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + void reset( Node eqc, QuantifiersEngine* qe ); + /** get the next match. must call reset( eqc ) before this function. */ + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); + /** add instantiations */ + int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + /** add ground term t */ + int addTerm( Node f, Node t, QuantifiersEngine* qe ); +};/* class InstMatchGenerator */ + +/** smart multi-trigger implementation */ +class InstMatchGeneratorMulti : public IMGenerator { +private: + /** indexed trie */ + typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie; + /** process new match */ + void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ); + /** process new instantiations */ + void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr, + std::vector< IndexedTrie >& unique_var_tries, + int trieIndex, int childIndex, int endChildIndex, bool modEq ); + /** process new instantiations 2 */ + void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, + std::vector< IndexedTrie >& unique_var_tries, + int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 ); +private: + /** var contains (variable indices) for each pattern node */ + std::map< Node, std::vector< int > > d_var_contains; + /** variable indices contained to pattern nodes */ + std::map< int, std::vector< Node > > d_var_to_node; + /** quantifier to use */ + Node d_f; + /** policy to use for matching */ + int d_matchPolicy; + /** children generators */ + std::vector< InstMatchGenerator* > d_children; + /** inst match tries for each child */ + std::vector< InstMatchTrieOrdered > d_children_trie; + /** calculate matches */ + void calculateMatches( QuantifiersEngine* qe ); +public: + /** constructors */ + InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); + /** destructor */ + ~InstMatchGeneratorMulti(){} + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound( QuantifiersEngine* qe ); + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + void reset( Node eqc, QuantifiersEngine* qe ); + /** get the next match. must call reset( eqc ) before this function. (not implemented) */ + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } + /** add instantiations */ + int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + /** add ground term t */ + int addTerm( Node f, Node t, QuantifiersEngine* qe ); +};/* class InstMatchGeneratorMulti */ + +/** smart (single)-trigger implementation */ +class InstMatchGeneratorSimple : public IMGenerator { +private: + /** quantifier for match term */ + Node d_f; + /** match term */ + Node d_match_pattern; + /** add instantiations */ + void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ); +public: + /** constructors */ + InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){} + /** destructor */ + ~InstMatchGeneratorSimple(){} + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound( QuantifiersEngine* qe ) {} + /** reset, eqc is the equivalence class to search in (any if eqc=null) */ + void reset( Node eqc, QuantifiersEngine* qe ) {} + /** get the next match. must call reset( eqc ) before this function. (not implemented) */ + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } + /** add instantiations */ + int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); + /** add ground term t, possibly add instantiations */ + int addTerm( Node f, Node t, QuantifiersEngine* qe ); +};/* class InstMatchGeneratorSimple */ + +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index d79ddee31..aba311500 100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -1,403 +1,403 @@ -/********************* */
-/*! \file inst_strategy_cbqi.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of cbqi instantiation strategies
- **/
-
-#include "theory/quantifiers/inst_strategy_cbqi.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::theory::arith;
-using namespace CVC4::theory::datatypes;
-
-#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
-
-InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
- InstStrategy( ie ), d_th( th ), d_counter( 0 ){
- d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
-}
-
-bool InstStrategySimplex::calculateShouldProcess( Node f ){
- //DO_THIS
- return false;
-}
-
-void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
- Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
- d_instRows.clear();
- d_tableaux_term.clear();
- d_tableaux.clear();
- d_ceTableaux.clear();
- //search for instantiation rows in simplex tableaux
- ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();
- for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
- ArithVar x = (*it).first;
- if( d_th->d_partialModel.hasEitherBound( x ) ){
- Node n = (*it).second;
- Node f;
- NodeBuilder<> t(kind::PLUS);
- if( n.getKind()==PLUS ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- addTermToRow( x, n[i], f, t );
- }
- }else{
- addTermToRow( x, n, f, t );
- }
- if( f!=Node::null() ){
- d_instRows[f].push_back( x );
- //this theory has constraints from f
- Debug("quant-arith") << "Has constraints from " << f << std::endl;
- //set that we should process it
- d_quantActive[ f ] = true;
- //set tableaux term
- if( t.getNumChildren()==0 ){
- d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
- }else if( t.getNumChildren()==1 ){
- d_tableaux_term[x] = t.getChild( 0 );
- }else{
- d_tableaux_term[x] = t;
- }
- }
- }
- }
- //print debug
- debugPrint( "quant-arith-debug" );
- d_counter++;
-}
-
-int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
- if( e<2 ){
- return STATUS_UNFINISHED;
- }else if( e==2 ){
- //Notice() << f << std::endl;
- //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
- //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
- Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;
- for( int j=0; j<(int)d_instRows[f].size(); j++ ){
- ArithVar x = d_instRows[f][j];
- if( !d_ceTableaux[x].empty() ){
- Debug("quant-arith-simplex") << "Check row " << x << std::endl;
- //instantiation row will be A*e + B*t = beta,
- // where e is a vector of terms , and t is vector of ground terms.
- // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
- // We will construct the term ( beta - B*t)/coeff to use for e_i.
- InstMatch m;
- //By default, choose the first instantiation constant to be e_i.
- Node var = d_ceTableaux[x].begin()->first;
- if( var.getType().isInteger() ){
- std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();
- //try to find coefficent that is +/- 1
- while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){
- ++it;
- if( it==d_ceTableaux[x].end() ){
- var = Node::null();
- }else{
- var = it->first;
- }
- }
- //otherwise, try one that divides all ground term coefficients? DO_THIS
- }
- if( !var.isNull() ){
- Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
- doInstantiation( f, d_tableaux_term[x], x, m, var );
- }else{
- Debug("quant-arith-simplex") << "Could not find var." << std::endl;
- }
- ////choose a new variable based on alternation strategy
- //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
- //Node var;
- //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
- // if( index==0 ){
- // var = it->first;
- // break;
- // }
- // index--;
- //}
- //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
- }
- }
- }
- return STATUS_UNKNOWN;
-}
-
-
-void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
- if( n.getKind()==MULT ){
- if( n[1].hasAttribute(InstConstantAttribute()) ){
- f = n[1].getAttribute(InstConstantAttribute());
- if( n[1].getKind()==INST_CONSTANT ){
- d_ceTableaux[x][ n[1] ] = n[0];
- }else{
- d_tableaux_ce_term[x][ n[1] ] = n[0];
- }
- }else{
- d_tableaux[x][ n[1] ] = n[0];
- t << n;
- }
- }else{
- if( n.hasAttribute(InstConstantAttribute()) ){
- f = n.getAttribute(InstConstantAttribute());
- if( n.getKind()==INST_CONSTANT ){
- d_ceTableaux[x][ n ] = Node::null();
- }else{
- d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
- }
- }else{
- d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
- t << n;
- }
- }
-}
-
-void InstStrategySimplex::debugPrint( const char* c ){
- ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();
- for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
- ArithVar x = (*it).first;
- Node n = (*it).second;
- //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
- Debug(c) << x << " : " << n << ", bounds = ";
- if( d_th->d_partialModel.hasLowerBound( x ) ){
- Debug(c) << d_th->d_partialModel.getLowerBound( x );
- }else{
- Debug(c) << "-infty";
- }
- Debug(c) << " <= ";
- Debug(c) << d_th->d_partialModel.getAssignment( x );
- Debug(c) << " <= ";
- if( d_th->d_partialModel.hasUpperBound( x ) ){
- Debug(c) << d_th->d_partialModel.getUpperBound( x );
- }else{
- Debug(c) << "+infty";
- }
- Debug(c) << std::endl;
- //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl;
- //Debug(c) << " ";
- //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
- // Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
- //}
- //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
- // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
- //}
- //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
- // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
- //}
- //Debug(c) << std::endl;
- //}
- }
- Debug(c) << std::endl;
-
- for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){
- Node f = d_quantEngine->getQuantifier( q );
- Debug(c) << f << std::endl;
- Debug(c) << " Inst constants: ";
- for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
- if( i>0 ){
- Debug( c ) << ", ";
- }
- Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
- }
- Debug(c) << std::endl;
- Debug(c) << " Instantiation rows: ";
- for( int i=0; i<(int)d_instRows[f].size(); i++ ){
- if( i>0 ){
- Debug(c) << ", ";
- }
- Debug(c) << d_instRows[f][i];
- }
- Debug(c) << std::endl;
- }
-}
-
-//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
-// where var is an instantiation constant from f,
-// t[e] is a vector of terms containing instantiation constants from f,
-// and term is a ground term (c1*t1 + ... + cn*tn).
-// We construct the term ( beta - term )/coeff to use as an instantiation for var.
-bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
- //first try +delta
- if( doInstantiation2( f, term, x, m, var ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);
- return true;
- }else{
-#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
- //otherwise try -delta
- if( doInstantiation2( f, term, x, m, var, true ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);
- return true;
- }else{
- return false;
- }
-#else
- return false;
-#endif
- }
-}
-
-bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
- // make term ( beta - term )/coeff
- Node beta = getTableauxValue( x, minus_delta );
- Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
- if( !d_ceTableaux[x][var].isNull() ){
- if( var.getType().isInteger() ){
- Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
- instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );
- }else{
- Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );
- instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
- }
- }
- instVal = Rewriter::rewrite( instVal );
- //use as instantiation value for var
- m.set(var, instVal);
- Debug("quant-arith") << "Add instantiation " << m << std::endl;
- return d_quantEngine->addInstantiation( f, m );
-}
-
-Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
- if( d_th->d_arithvarNodeMap.hasArithVar(n) ){
- ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );
- return getTableauxValue( v, minus_delta );
- }else{
- return NodeManager::currentNM()->mkConst( Rational(0) );
- }
-}
-
-Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
- const Rational& delta = d_th->d_partialModel.getDelta();
- DeltaRational drv = d_th->d_partialModel.getAssignment( v );
- Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
- return mkRationalNode(qmodel);
-}
-
-
-InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :
- InstStrategy( qe ), d_th( th ){
-
-}
-
-bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){
- //DO_THIS
- return false;
-}
-
-void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
- Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
- if( e<2 ){
- return InstStrategy::STATUS_UNFINISHED;
- }else if( e==2 ){
- InstMatch m;
- for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
- Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
- if( i.getType().isDatatype() ){
- Node n = getValueFor( i );
- Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
- m.set(i,n);
- }
- }
- //d_quantEngine->addInstantiation( f, m );
- }
- return InstStrategy::STATUS_UNKNOWN;
-}
-
-Node InstStrategyDatatypesValue::getValueFor( Node n ){
- //simply get the ground value for n in the current model, if it exists,
- // or return an arbitrary ground term otherwise
- if( !n.hasAttribute(InstConstantAttribute()) ){
- return n;
- }else{
- return n;
- }
- /* FIXME
-
- Debug("quant-datatypes-debug") << "get value for " << n << std::endl;
- if( !n.hasAttribute(InstConstantAttribute()) ){
- return n;
- }else{
- Assert( n.getType().isDatatype() );
- //check if in equivalence class with ground term
- Node rep = getRepresentative( n );
- Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;
- if( !rep.hasAttribute(InstConstantAttribute()) ){
- return rep;
- }else{
- if( !n.getType().isDatatype() ){
- return n.getType().mkGroundTerm();
- }else{
- if( n.getKind()==APPLY_CONSTRUCTOR ){
- std::vector< Node > children;
- children.push_back( n.getOperator() );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- children.push_back( getValueFor( n[i] ) );
- }
- return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
- }else{
- const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
- TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;
- //otherwise, use which constructor the inst constant is current chosen to be
- if( labels->find( n )!=labels->end() ){
- TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;
- int tIndex = -1;
- if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){
- Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;
- tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());
- }else{
- Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;
- //must find a possible choice
- vector< bool > possibleCons;
- possibleCons.resize( dt.getNumConstructors(), true );
- for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {
- Node leqn = (*j);
- possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
- }
- for( unsigned int j=0; j<possibleCons.size(); j++ ) {
- if( possibleCons[j] ){
- tIndex = j;
- break;
- }
- }
- }
- Assert( tIndex!=-1 );
- Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );
- Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;
- std::vector< Node > children;
- children.push_back( cons );
- for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {
- Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );
- if( n.hasAttribute(InstConstantAttribute()) ){
- InstConstantAttribute ica;
- sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );
- }
- Node snn = getValueFor( sn );
- children.push_back( snn );
- }
- return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
- }else{
- return n.getType().mkGroundTerm();
- }
- }
- }
- }
- }
- */
-}
+/********************* */ +/*! \file inst_strategy_cbqi.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): bobot, mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of cbqi instantiation strategies + **/ + +#include "theory/quantifiers/inst_strategy_cbqi.h" +#include "theory/arith/theory_arith.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::theory::arith; +using namespace CVC4::theory::datatypes; + +#define ARITH_INSTANTIATOR_USE_MINUS_DELTA + +InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : + InstStrategy( ie ), d_th( th ), d_counter( 0 ){ + d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); +} + +bool InstStrategySimplex::calculateShouldProcess( Node f ){ + //DO_THIS + return false; +} + +void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){ + Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl; + d_instRows.clear(); + d_tableaux_term.clear(); + d_tableaux.clear(); + d_ceTableaux.clear(); + //search for instantiation rows in simplex tableaux + ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap(); + for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){ + ArithVar x = (*it).first; + if( d_th->d_partialModel.hasEitherBound( x ) ){ + Node n = (*it).second; + Node f; + NodeBuilder<> t(kind::PLUS); + if( n.getKind()==PLUS ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + addTermToRow( x, n[i], f, t ); + } + }else{ + addTermToRow( x, n, f, t ); + } + if( f!=Node::null() ){ + d_instRows[f].push_back( x ); + //this theory has constraints from f + Debug("quant-arith") << "Has constraints from " << f << std::endl; + //set that we should process it + d_quantActive[ f ] = true; + //set tableaux term + if( t.getNumChildren()==0 ){ + d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) ); + }else if( t.getNumChildren()==1 ){ + d_tableaux_term[x] = t.getChild( 0 ); + }else{ + d_tableaux_term[x] = t; + } + } + } + } + //print debug + debugPrint( "quant-arith-debug" ); + d_counter++; +} + +int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ + if( e<2 ){ + return STATUS_UNFINISHED; + }else if( e==2 ){ + //Notice() << f << std::endl; + //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl; + //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl; + Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl; + for( int j=0; j<(int)d_instRows[f].size(); j++ ){ + ArithVar x = d_instRows[f][j]; + if( !d_ceTableaux[x].empty() ){ + Debug("quant-arith-simplex") << "Check row " << x << std::endl; + //instantiation row will be A*e + B*t = beta, + // where e is a vector of terms , and t is vector of ground terms. + // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant + // We will construct the term ( beta - B*t)/coeff to use for e_i. + InstMatch m; + //By default, choose the first instantiation constant to be e_i. + Node var = d_ceTableaux[x].begin()->first; + if( var.getType().isInteger() ){ + std::map< Node, Node >::iterator it = d_ceTableaux[x].begin(); + //try to find coefficent that is +/- 1 + while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){ + ++it; + if( it==d_ceTableaux[x].end() ){ + var = Node::null(); + }else{ + var = it->first; + } + } + //otherwise, try one that divides all ground term coefficients? DO_THIS + } + if( !var.isNull() ){ + Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; + doInstantiation( f, d_tableaux_term[x], x, m, var ); + }else{ + Debug("quant-arith-simplex") << "Could not find var." << std::endl; + } + ////choose a new variable based on alternation strategy + //int index = d_counter%(int)d_th->d_ceTableaux[x].size(); + //Node var; + //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){ + // if( index==0 ){ + // var = it->first; + // break; + // } + // index--; + //} + //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var ); + } + } + } + return STATUS_UNKNOWN; +} + + +void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){ + if( n.getKind()==MULT ){ + if( n[1].hasAttribute(InstConstantAttribute()) ){ + f = n[1].getAttribute(InstConstantAttribute()); + if( n[1].getKind()==INST_CONSTANT ){ + d_ceTableaux[x][ n[1] ] = n[0]; + }else{ + d_tableaux_ce_term[x][ n[1] ] = n[0]; + } + }else{ + d_tableaux[x][ n[1] ] = n[0]; + t << n; + } + }else{ + if( n.hasAttribute(InstConstantAttribute()) ){ + f = n.getAttribute(InstConstantAttribute()); + if( n.getKind()==INST_CONSTANT ){ + d_ceTableaux[x][ n ] = Node::null(); + }else{ + d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); + } + }else{ + d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); + t << n; + } + } +} + +void InstStrategySimplex::debugPrint( const char* c ){ + ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap(); + for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){ + ArithVar x = (*it).first; + Node n = (*it).second; + //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){ + Debug(c) << x << " : " << n << ", bounds = "; + if( d_th->d_partialModel.hasLowerBound( x ) ){ + Debug(c) << d_th->d_partialModel.getLowerBound( x ); + }else{ + Debug(c) << "-infty"; + } + Debug(c) << " <= "; + Debug(c) << d_th->d_partialModel.getAssignment( x ); + Debug(c) << " <= "; + if( d_th->d_partialModel.hasUpperBound( x ) ){ + Debug(c) << d_th->d_partialModel.getUpperBound( x ); + }else{ + Debug(c) << "+infty"; + } + Debug(c) << std::endl; + //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl; + //Debug(c) << " "; + //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){ + // Debug(c) << "( " << it2->first << ", " << it2->second << " ) "; + //} + //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){ + // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) "; + //} + //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){ + // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) "; + //} + //Debug(c) << std::endl; + //} + } + Debug(c) << std::endl; + + for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){ + Node f = d_quantEngine->getQuantifier( q ); + Debug(c) << f << std::endl; + Debug(c) << " Inst constants: "; + for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + if( i>0 ){ + Debug( c ) << ", "; + } + Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); + } + Debug(c) << std::endl; + Debug(c) << " Instantiation rows: "; + for( int i=0; i<(int)d_instRows[f].size(); i++ ){ + if( i>0 ){ + Debug(c) << ", "; + } + Debug(c) << d_instRows[f][i]; + } + Debug(c) << std::endl; + } +} + +//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta, +// where var is an instantiation constant from f, +// t[e] is a vector of terms containing instantiation constants from f, +// and term is a ground term (c1*t1 + ... + cn*tn). +// We construct the term ( beta - term )/coeff to use as an instantiation for var. +bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){ + //first try +delta + if( doInstantiation2( f, term, x, m, var ) ){ + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith); + return true; + }else{ +#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA + //otherwise try -delta + if( doInstantiation2( f, term, x, m, var, true ) ){ + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus); + return true; + }else{ + return false; + } +#else + return false; +#endif + } +} + +bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ + // make term ( beta - term )/coeff + Node beta = getTableauxValue( x, minus_delta ); + Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); + if( !d_ceTableaux[x][var].isNull() ){ + if( var.getType().isInteger() ){ + Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); + instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal ); + }else{ + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() ); + instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); + } + } + instVal = Rewriter::rewrite( instVal ); + //use as instantiation value for var + m.set(var, instVal); + Debug("quant-arith") << "Add instantiation " << m << std::endl; + return d_quantEngine->addInstantiation( f, m ); +} + +Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){ + if( d_th->d_arithvarNodeMap.hasArithVar(n) ){ + ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n ); + return getTableauxValue( v, minus_delta ); + }else{ + return NodeManager::currentNM()->mkConst( Rational(0) ); + } +} + +Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ + const Rational& delta = d_th->d_partialModel.getDelta(); + DeltaRational drv = d_th->d_partialModel.getAssignment( v ); + Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta ); + return mkRationalNode(qmodel); +} + + +InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) : + InstStrategy( qe ), d_th( th ){ + +} + +bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){ + //DO_THIS + return false; +} + +void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){ + +} + +int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){ + Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl; + if( e<2 ){ + return InstStrategy::STATUS_UNFINISHED; + }else if( e==2 ){ + InstMatch m; + for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){ + Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); + if( i.getType().isDatatype() ){ + Node n = getValueFor( i ); + Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl; + m.set(i,n); + } + } + //d_quantEngine->addInstantiation( f, m ); + } + return InstStrategy::STATUS_UNKNOWN; +} + +Node InstStrategyDatatypesValue::getValueFor( Node n ){ + //simply get the ground value for n in the current model, if it exists, + // or return an arbitrary ground term otherwise + if( !n.hasAttribute(InstConstantAttribute()) ){ + return n; + }else{ + return n; + } + /* FIXME + + Debug("quant-datatypes-debug") << "get value for " << n << std::endl; + if( !n.hasAttribute(InstConstantAttribute()) ){ + return n; + }else{ + Assert( n.getType().isDatatype() ); + //check if in equivalence class with ground term + Node rep = getRepresentative( n ); + Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl; + if( !rep.hasAttribute(InstConstantAttribute()) ){ + return rep; + }else{ + if( !n.getType().isDatatype() ){ + return n.getType().mkGroundTerm(); + }else{ + if( n.getKind()==APPLY_CONSTRUCTOR ){ + std::vector< Node > children; + children.push_back( n.getOperator() ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + children.push_back( getValueFor( n[i] ) ); + } + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + }else{ + const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); + TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels; + //otherwise, use which constructor the inst constant is current chosen to be + if( labels->find( n )!=labels->end() ){ + TheoryDatatypes::EqList* lbl = (*labels->find( n )).second; + int tIndex = -1; + if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){ + Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl; + tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr()); + }else{ + Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl; + //must find a possible choice + vector< bool > possibleCons; + possibleCons.resize( dt.getNumConstructors(), true ); + for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) { + Node leqn = (*j); + possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false; + } + for( unsigned int j=0; j<possibleCons.size(); j++ ) { + if( possibleCons[j] ){ + tIndex = j; + break; + } + } + } + Assert( tIndex!=-1 ); + Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() ); + Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl; + std::vector< Node > children; + children.push_back( cons ); + for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) { + Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n ); + if( n.hasAttribute(InstConstantAttribute()) ){ + InstConstantAttribute ica; + sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) ); + } + Node snn = getValueFor( sn ); + children.push_back( snn ); + } + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + }else{ + return n.getType().mkGroundTerm(); + } + } + } + } + } + */ +} diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 3ee423fe7..1c9565de6 100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -1,110 +1,110 @@ -/********************* */
-/*! \file inst_strategy_cbqi.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief instantiator_arith_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INST_STRATEGT_CBQI_H
-#define __CVC4__INST_STRATEGT_CBQI_H
-
-#include "theory/quantifiers/instantiation_engine.h"
-#include "theory/arith/arithvar_node_map.h"
-
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-
-namespace arith {
- class TheoryArith;
-}
-
-namespace datatypes {
- class TheoryDatatypes;
-}
-
-namespace quantifiers {
-
-
-class InstStrategySimplex : public InstStrategy{
-protected:
- /** calculate if we should process this quantifier */
- bool calculateShouldProcess( Node f );
-private:
- /** reference to theory arithmetic */
- arith::TheoryArith* d_th;
- /** delta */
- std::map< TypeNode, Node > d_deltas;
- /** for each quantifier, simplex rows */
- std::map< Node, std::vector< arith::ArithVar > > d_instRows;
- /** tableaux */
- std::map< arith::ArithVar, Node > d_tableaux_term;
- std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
- std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;
- /** ce tableaux */
- std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;
- /** get value */
- Node getTableauxValue( Node n, bool minus_delta = false );
- Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );
- /** do instantiation */
- bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );
- bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
- /** add term to row */
- void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );
- /** print debug */
- void debugPrint( const char* c );
-private:
- /** */
- int d_counter;
- /** negative one */
- Node d_negOne;
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
- ~InstStrategySimplex(){}
- /** identify */
- std::string identify() const { return std::string("Simplex"); }
-};
-
-
-class InstStrategyDatatypesValue : public InstStrategy
-{
-protected:
- /** calculate if we should process this quantifier */
- bool calculateShouldProcess( Node f );
-private:
- /** reference to theory datatypes */
- datatypes::TheoryDatatypes* d_th;
- /** get value function */
- Node getValueFor( Node n );
-public:
- //constructor
- InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );
- ~InstStrategyDatatypesValue(){}
- /** reset instantiation */
- void processResetInstantiationRound( Theory::Effort effort );
- /** process method, returns a status */
- int process( Node f, Theory::Effort effort, int e );
- /** identify */
- std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
-
-};/* class InstStrategy */
-
-}
-}
-}
-
+/********************* */ +/*! \file inst_strategy_cbqi.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief instantiator_arith_instantiator + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__INST_STRATEGT_CBQI_H +#define __CVC4__INST_STRATEGT_CBQI_H + +#include "theory/quantifiers/instantiation_engine.h" +#include "theory/arith/arithvar_node_map.h" + +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { + +namespace arith { + class TheoryArith; +} + +namespace datatypes { + class TheoryDatatypes; +} + +namespace quantifiers { + + +class InstStrategySimplex : public InstStrategy{ +protected: + /** calculate if we should process this quantifier */ + bool calculateShouldProcess( Node f ); +private: + /** reference to theory arithmetic */ + arith::TheoryArith* d_th; + /** delta */ + std::map< TypeNode, Node > d_deltas; + /** for each quantifier, simplex rows */ + std::map< Node, std::vector< arith::ArithVar > > d_instRows; + /** tableaux */ + std::map< arith::ArithVar, Node > d_tableaux_term; + std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term; + std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux; + /** ce tableaux */ + std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux; + /** get value */ + Node getTableauxValue( Node n, bool minus_delta = false ); + Node getTableauxValue( arith::ArithVar v, bool minus_delta = false ); + /** do instantiation */ + bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var ); + bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); + /** add term to row */ + void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t ); + /** print debug */ + void debugPrint( const char* c ); +private: + /** */ + int d_counter; + /** negative one */ + Node d_negOne; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e ); +public: + InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie ); + ~InstStrategySimplex(){} + /** identify */ + std::string identify() const { return std::string("Simplex"); } +}; + + +class InstStrategyDatatypesValue : public InstStrategy +{ +protected: + /** calculate if we should process this quantifier */ + bool calculateShouldProcess( Node f ); +private: + /** reference to theory datatypes */ + datatypes::TheoryDatatypes* d_th; + /** get value function */ + Node getValueFor( Node n ); +public: + //constructor + InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe ); + ~InstStrategyDatatypesValue(){} + /** reset instantiation */ + void processResetInstantiationRound( Theory::Effort effort ); + /** process method, returns a status */ + int process( Node f, Theory::Effort effort, int e ); + /** identify */ + std::string identify() const { return std::string("InstStrategyDatatypesValue"); } + +};/* class InstStrategy */ + +} +} +} + #endif
\ No newline at end of file diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 48af334ff..edf9d976c 100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -1,379 +1,379 @@ -/********************* */
-/*! \file inst_strategy_e_matching.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): bobot
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of e matching instantiation strategies
- **/
-
-#include "theory/quantifiers/inst_strategy_e_matching.h"
-
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/inst_match_generator.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
-using namespace CVC4::theory::quantifiers;
-
-#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
-//#define MULTI_TRIGGER_FULL_EFFORT_HALF
-#define MULTI_MULTI_TRIGGERS
-
-struct sortQuantifiersForSymbol {
- QuantifiersEngine* d_qe;
- bool operator() (Node i, Node j) {
- int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );
- int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );
- if( nqfsi<nqfsj ){
- return true;
- }else if( nqfsi>nqfsj ){
- return false;
- }else{
- return false;
- }
- }
-};
-
-void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
- //reset triggers
- for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
- for( int i=0; i<(int)it->second.size(); i++ ){
- it->second[i]->resetInstantiationRound();
- it->second[i]->reset( Node::null() );
- }
- }
-}
-
-int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
- if( e==0 ){
- return STATUS_UNFINISHED;
- }else if( e==1 ){
- d_counter[f]++;
- Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;
- //Notice() << "Try user-provided patterns..." << std::endl;
- for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
- bool processTrigger = true;
- if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){
-//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
-// processTrigger = d_counter[f]%2==0;
-//#endif
- }
- if( processTrigger ){
- //if( d_user_gen[f][i]->isMultiTrigger() )
- //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;
- InstMatch baseMatch;
- int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
- //if( d_user_gen[f][i]->isMultiTrigger() )
- //Notice() << " Done, numInst = " << numInst << "." << std::endl;
- d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
- if( d_user_gen[f][i]->isMultiTrigger() ){
- d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
- }
- //d_quantEngine->d_hasInstantiated[f] = true;
- }
- }
- Debug("quant-uf-strategy") << "done." << std::endl;
- //Notice() << "done" << std::endl;
- }
- return STATUS_UNKNOWN;
-}
-
-void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
- //add to generators
- std::vector< Node > nodes;
- for( int i=0; i<(int)pat.getNumChildren(); i++ ){
- nodes.push_back( pat[i] );
- }
- if( Trigger::isUsableTrigger( nodes, f ) ){
- //extend to literal matching
- d_quantEngine->getPhaseReqTerms( f, nodes );
- //check match option
- int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
- d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
- options::smartTriggers() ) );
- }
-}
-/*
-InstStrategyUserPatterns::Statistics::Statistics():
- d_instantiations("InstStrategyUserPatterns::Instantiations", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyUserPatterns::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-*/
-
-void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
- //reset triggers
- for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
- for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
- itt->first->resetInstantiationRound();
- itt->first->reset( Node::null() );
- }
- }
-}
-
-int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
- int peffort = f.getNumChildren()==3 ? 2 : 1;
- //int peffort = f.getNumChildren()==3 ? 2 : 1;
- //int peffort = 1;
- if( e<peffort ){
- return STATUS_UNFINISHED;
- }else{
- bool gen = false;
- if( e==peffort ){
- if( d_counter.find( f )==d_counter.end() ){
- d_counter[f] = 0;
- gen = true;
- }else{
- d_counter[f]++;
- gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;
- }
- }else{
- gen = true;
- }
- if( gen ){
- generateTriggers( f );
- }
- Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
- //Notice() << "Try auto-generated triggers..." << std::endl;
- for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
- Trigger* tr = itt->first;
- if( tr ){
- bool processTrigger = itt->second;
- if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){
-#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
- processTrigger = d_counter[f]%2==0;
-#endif
- }
- if( processTrigger ){
- //if( tr->isMultiTrigger() )
- Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl;
- InstMatch baseMatch;
- int numInst = tr->addInstantiations( baseMatch );
- //if( tr->isMultiTrigger() )
- Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl;
- if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
- d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;
- }else{
- d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;
- }
- if( tr->isMultiTrigger() ){
- d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
- }
- //d_quantEngine->d_hasInstantiated[f] = true;
- }
- }
- }
- Debug("quant-uf-strategy") << "done." << std::endl;
- //Notice() << "done" << std::endl;
- }
- return STATUS_UNKNOWN;
-}
-
-void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
- Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
- if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
- //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
- d_patTerms[0][f].clear();
- d_patTerms[1][f].clear();
- std::vector< Node > patTermsF;
- Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );
- Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;
- Debug("auto-gen-trigger") << " ";
- for( int i=0; i<(int)patTermsF.size(); i++ ){
- Debug("auto-gen-trigger") << patTermsF[i] << " ";
- }
- Debug("auto-gen-trigger") << std::endl;
- //extend to literal matching (if applicable)
- d_quantEngine->getPhaseReqTerms( f, patTermsF );
- //sort into single/multi triggers
- std::map< Node, std::vector< Node > > varContains;
- d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );
- for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
- if( it->second.size()==f[0].getNumChildren() ){
- d_patTerms[0][f].push_back( it->first );
- d_is_single_trigger[ it->first ] = true;
- }else{
- d_patTerms[1][f].push_back( it->first );
- d_is_single_trigger[ it->first ] = false;
- }
- }
- d_made_multi_trigger[f] = false;
- Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
- Debug("auto-gen-trigger") << " ";
- for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
- Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";
- }
- Debug("auto-gen-trigger") << std::endl;
- Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
- Debug("auto-gen-trigger") << " ";
- for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){
- Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";
- }
- Debug("auto-gen-trigger") << std::endl;
- }
-
- //populate candidate pattern term vector for the current trigger
- std::vector< Node > patTerms;
-#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
- //try to add single triggers first
- for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
- if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){
- patTerms.push_back( d_patTerms[0][f][i] );
- }
- }
- //if no single triggers exist, add multi trigger terms
- if( patTerms.empty() ){
- patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
- }
-#else
- patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );
- patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
-#endif
-
- if( !patTerms.empty() ){
- Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
- //sort terms based on relevance
- if( d_rlv_strategy==RELEVANCE_DEFAULT ){
- sortQuantifiersForSymbol sqfs;
- sqfs.d_qe = d_quantEngine;
- //sort based on # occurrences (this will cause Trigger to select rarer symbols)
- std::sort( patTerms.begin(), patTerms.end(), sqfs );
- Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
- for( int i=0; i<(int)patTerms.size(); i++ ){
- Debug("relevant-trigger") << " " << patTerms[i] << " (";
- Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
- }
- //Notice() << "Terms based on relevance: " << std::endl;
- //for( int i=0; i<(int)patTerms.size(); i++ ){
- // Notice() << " " << patTerms[i] << " (";
- // Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
- //}
- }
- //now, generate the trigger...
- int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
- Trigger* tr = NULL;
- if( d_is_single_trigger[ patTerms[0] ] ){
- tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,
- options::smartTriggers() );
- d_single_trigger_gen[ patTerms[0] ] = true;
- }else{
- //if we are re-generating triggers, shuffle based on some method
- if( d_made_multi_trigger[f] ){
-#ifndef MULTI_MULTI_TRIGGERS
- return;
-#endif
- std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
- }else{
- d_made_multi_trigger[f] = true;
- }
- //will possibly want to get an old trigger
- tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,
- options::smartTriggers() );
- }
- if( tr ){
- if( tr->isMultiTrigger() ){
- //disable all other multi triggers
- for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){
- if( it->first->isMultiTrigger() ){
- d_auto_gen_trigger[f][ it->first ] = false;
- }
- }
- }
- //making it during an instantiation round, so must reset
- if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){
- tr->resetInstantiationRound();
- tr->reset( Node::null() );
- }
- d_auto_gen_trigger[f][tr] = true;
- //if we are generating additional triggers...
- if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){
- int index = 0;
- if( index<(int)patTerms.size() ){
- //Notice() << "check add additional" << std::endl;
- //check if similar patterns exist, and if so, add them additionally
- int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
- index++;
- bool success = true;
- while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
- success = false;
- if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
- d_single_trigger_gen[ patTerms[index] ] = true;
- Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
- options::smartTriggers() );
- if( tr2 ){
- //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
- tr2->resetInstantiationRound();
- tr2->reset( Node::null() );
- d_auto_gen_trigger[f][tr2] = true;
- }
- success = true;
- }
- index++;
- }
- //Notice() << "done check add additional" << std::endl;
- }
- }
- }
- }
-}
-/*
-InstStrategyAutoGenTriggers::Statistics::Statistics():
- d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),
- d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
- StatisticsRegistry::registerStat(&d_instantiations_min);
-}
-
-InstStrategyAutoGenTriggers::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations);
- StatisticsRegistry::unregisterStat(&d_instantiations_min);
-}
-*/
-
-void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
- if( e<5 ){
- return STATUS_UNFINISHED;
- }else{
- if( d_guessed.find( f )==d_guessed.end() ){
- d_guessed[f] = true;
- Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;
- InstMatch m;
- if( d_quantEngine->addInstantiation( f, m ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
- //d_quantEngine->d_hasInstantiated[f] = true;
- }
- }
- return STATUS_UNKNOWN;
- }
-}
-/*
-InstStrategyFreeVariable::Statistics::Statistics():
- d_instantiations("InstStrategyGuess::Instantiations", 0)
-{
- StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyFreeVariable::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-*/
+/********************* */ +/*! \file inst_strategy_e_matching.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: mdeters + ** Minor contributors (to current version): bobot + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of e matching instantiation strategies + **/ + +#include "theory/quantifiers/inst_strategy_e_matching.h" + +#include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/inst_match_generator.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::inst; +using namespace CVC4::theory::quantifiers; + +#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER +//#define MULTI_TRIGGER_FULL_EFFORT_HALF +#define MULTI_MULTI_TRIGGERS + +struct sortQuantifiersForSymbol { + QuantifiersEngine* d_qe; + bool operator() (Node i, Node j) { + int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() ); + int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() ); + if( nqfsi<nqfsj ){ + return true; + }else if( nqfsi>nqfsj ){ + return false; + }else{ + return false; + } + } +}; + +void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){ + //reset triggers + for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){ + for( int i=0; i<(int)it->second.size(); i++ ){ + it->second[i]->resetInstantiationRound(); + it->second[i]->reset( Node::null() ); + } + } +} + +int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ + if( e==0 ){ + return STATUS_UNFINISHED; + }else if( e==1 ){ + d_counter[f]++; + Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl; + //Notice() << "Try user-provided patterns..." << std::endl; + for( int i=0; i<(int)d_user_gen[f].size(); i++ ){ + bool processTrigger = true; + if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){ +//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF +// processTrigger = d_counter[f]%2==0; +//#endif + } + if( processTrigger ){ + //if( d_user_gen[f][i]->isMultiTrigger() ) + //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl; + InstMatch baseMatch; + int numInst = d_user_gen[f][i]->addInstantiations( baseMatch ); + //if( d_user_gen[f][i]->isMultiTrigger() ) + //Notice() << " Done, numInst = " << numInst << "." << std::endl; + d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst; + if( d_user_gen[f][i]->isMultiTrigger() ){ + d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; + } + //d_quantEngine->d_hasInstantiated[f] = true; + } + } + Debug("quant-uf-strategy") << "done." << std::endl; + //Notice() << "done" << std::endl; + } + return STATUS_UNKNOWN; +} + +void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ + //add to generators + std::vector< Node > nodes; + for( int i=0; i<(int)pat.getNumChildren(); i++ ){ + nodes.push_back( pat[i] ); + } + if( Trigger::isUsableTrigger( nodes, f ) ){ + //extend to literal matching + d_quantEngine->getPhaseReqTerms( f, nodes ); + //check match option + int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; + d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, + options::smartTriggers() ) ); + } +} +/* +InstStrategyUserPatterns::Statistics::Statistics(): + d_instantiations("InstStrategyUserPatterns::Instantiations", 0) +{ + StatisticsRegistry::registerStat(&d_instantiations); +} + +InstStrategyUserPatterns::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_instantiations); +} +*/ + +void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){ + //reset triggers + for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){ + for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){ + itt->first->resetInstantiationRound(); + itt->first->reset( Node::null() ); + } + } +} + +int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ + int peffort = f.getNumChildren()==3 ? 2 : 1; + //int peffort = f.getNumChildren()==3 ? 2 : 1; + //int peffort = 1; + if( e<peffort ){ + return STATUS_UNFINISHED; + }else{ + bool gen = false; + if( e==peffort ){ + if( d_counter.find( f )==d_counter.end() ){ + d_counter[f] = 0; + gen = true; + }else{ + d_counter[f]++; + gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0; + } + }else{ + gen = true; + } + if( gen ){ + generateTriggers( f ); + } + Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl; + //Notice() << "Try auto-generated triggers..." << std::endl; + for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){ + Trigger* tr = itt->first; + if( tr ){ + bool processTrigger = itt->second; + if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){ +#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF + processTrigger = d_counter[f]%2==0; +#endif + } + if( processTrigger ){ + //if( tr->isMultiTrigger() ) + Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl; + InstMatch baseMatch; + int numInst = tr->addInstantiations( baseMatch ); + //if( tr->isMultiTrigger() ) + Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl; + if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ + d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst; + }else{ + d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst; + } + if( tr->isMultiTrigger() ){ + d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; + } + //d_quantEngine->d_hasInstantiated[f] = true; + } + } + } + Debug("quant-uf-strategy") << "done." << std::endl; + //Notice() << "done" << std::endl; + } + return STATUS_UNKNOWN; +} + +void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ + Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl; + if( d_patTerms[0].find( f )==d_patTerms[0].end() ){ + //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy + d_patTerms[0][f].clear(); + d_patTerms[1][f].clear(); + std::vector< Node > patTermsF; + Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true ); + Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl; + Debug("auto-gen-trigger") << " "; + for( int i=0; i<(int)patTermsF.size(); i++ ){ + Debug("auto-gen-trigger") << patTermsF[i] << " "; + } + Debug("auto-gen-trigger") << std::endl; + //extend to literal matching (if applicable) + d_quantEngine->getPhaseReqTerms( f, patTermsF ); + //sort into single/multi triggers + std::map< Node, std::vector< Node > > varContains; + d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains ); + for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ + if( it->second.size()==f[0].getNumChildren() ){ + d_patTerms[0][f].push_back( it->first ); + d_is_single_trigger[ it->first ] = true; + }else{ + d_patTerms[1][f].push_back( it->first ); + d_is_single_trigger[ it->first ] = false; + } + } + d_made_multi_trigger[f] = false; + Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl; + Debug("auto-gen-trigger") << " "; + for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ + Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " "; + } + Debug("auto-gen-trigger") << std::endl; + Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl; + Debug("auto-gen-trigger") << " "; + for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){ + Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " "; + } + Debug("auto-gen-trigger") << std::endl; + } + + //populate candidate pattern term vector for the current trigger + std::vector< Node > patTerms; +#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER + //try to add single triggers first + for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ + if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){ + patTerms.push_back( d_patTerms[0][f][i] ); + } + } + //if no single triggers exist, add multi trigger terms + if( patTerms.empty() ){ + patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() ); + } +#else + patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() ); + patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() ); +#endif + + if( !patTerms.empty() ){ + Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl; + //sort terms based on relevance + if( d_rlv_strategy==RELEVANCE_DEFAULT ){ + sortQuantifiersForSymbol sqfs; + sqfs.d_qe = d_quantEngine; + //sort based on # occurrences (this will cause Trigger to select rarer symbols) + std::sort( patTerms.begin(), patTerms.end(), sqfs ); + Debug("relevant-trigger") << "Terms based on relevance: " << std::endl; + for( int i=0; i<(int)patTerms.size(); i++ ){ + Debug("relevant-trigger") << " " << patTerms[i] << " ("; + Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl; + } + //Notice() << "Terms based on relevance: " << std::endl; + //for( int i=0; i<(int)patTerms.size(); i++ ){ + // Notice() << " " << patTerms[i] << " ("; + // Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl; + //} + } + //now, generate the trigger... + int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; + Trigger* tr = NULL; + if( d_is_single_trigger[ patTerms[0] ] ){ + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, + options::smartTriggers() ); + d_single_trigger_gen[ patTerms[0] ] = true; + }else{ + //if we are re-generating triggers, shuffle based on some method + if( d_made_multi_trigger[f] ){ +#ifndef MULTI_MULTI_TRIGGERS + return; +#endif + std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly + }else{ + d_made_multi_trigger[f] = true; + } + //will possibly want to get an old trigger + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, + options::smartTriggers() ); + } + if( tr ){ + if( tr->isMultiTrigger() ){ + //disable all other multi triggers + for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){ + if( it->first->isMultiTrigger() ){ + d_auto_gen_trigger[f][ it->first ] = false; + } + } + } + //making it during an instantiation round, so must reset + if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){ + tr->resetInstantiationRound(); + tr->reset( Node::null() ); + } + d_auto_gen_trigger[f][tr] = true; + //if we are generating additional triggers... + if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){ + int index = 0; + if( index<(int)patTerms.size() ){ + //Notice() << "check add additional" << std::endl; + //check if similar patterns exist, and if so, add them additionally + int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() ); + index++; + bool success = true; + while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){ + success = false; + if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ + d_single_trigger_gen[ patTerms[index] ] = true; + Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, + options::smartTriggers() ); + if( tr2 ){ + //Notice() << "Add additional trigger " << patTerms[index] << std::endl; + tr2->resetInstantiationRound(); + tr2->reset( Node::null() ); + d_auto_gen_trigger[f][tr2] = true; + } + success = true; + } + index++; + } + //Notice() << "done check add additional" << std::endl; + } + } + } + } +} +/* +InstStrategyAutoGenTriggers::Statistics::Statistics(): + d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0), + d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0) +{ + StatisticsRegistry::registerStat(&d_instantiations); + StatisticsRegistry::registerStat(&d_instantiations_min); +} + +InstStrategyAutoGenTriggers::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_instantiations); + StatisticsRegistry::unregisterStat(&d_instantiations_min); +} +*/ + +void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ +} + +int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ + if( e<5 ){ + return STATUS_UNFINISHED; + }else{ + if( d_guessed.find( f )==d_guessed.end() ){ + d_guessed[f] = true; + Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl; + InstMatch m; + if( d_quantEngine->addInstantiation( f, m ) ){ + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); + //d_quantEngine->d_hasInstantiated[f] = true; + } + } + return STATUS_UNKNOWN; + } +} +/* +InstStrategyFreeVariable::Statistics::Statistics(): + d_instantiations("InstStrategyGuess::Instantiations", 0) +{ + StatisticsRegistry::registerStat(&d_instantiations); +} + +InstStrategyFreeVariable::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_instantiations); +} +*/ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 23f0d8a54..b5ff90a62 100755 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -1,135 +1,135 @@ -/********************* */
-/*! \file inst_strategy_e_matching.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief E matching instantiation strategies
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H
-#define __CVC4__INST_STRATEGY_E_MATCHING_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
-#include "context/context.h"
-#include "context/context_mm.h"
-
-#include "util/statistics_registry.h"
-#include "theory/quantifiers/instantiation_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-//instantiation strategies
-
-class InstStrategyUserPatterns : public InstStrategy{
-private:
- /** explicitly provided patterns */
- std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
- /** counter for quantifiers */
- std::map< Node, int > d_counter;
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstStrategyUserPatterns( QuantifiersEngine* ie ) :
- InstStrategy( ie ){}
- ~InstStrategyUserPatterns(){}
-public:
- /** add pattern */
- void addUserPattern( Node f, Node pat );
- /** get num patterns */
- int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
- /** get user pattern */
- inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
- /** identify */
- std::string identify() const { return std::string("UserPatterns"); }
-};/* class InstStrategyUserPatterns */
-
-class InstStrategyAutoGenTriggers : public InstStrategy{
-public:
- enum {
- RELEVANCE_NONE,
- RELEVANCE_DEFAULT,
- };
-private:
- /** trigger generation strategy */
- int d_tr_strategy;
- /** relevance strategy */
- int d_rlv_strategy;
- /** regeneration */
- bool d_regenerate;
- int d_regenerate_frequency;
- /** generate additional triggers */
- bool d_generate_additional;
- /** triggers for each quantifier */
- std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
- std::map< Node, int > d_counter;
- /** single, multi triggers for each quantifier */
- std::map< Node, std::vector< Node > > d_patTerms[2];
- std::map< Node, bool > d_is_single_trigger;
- std::map< Node, bool > d_single_trigger_gen;
- std::map< Node, bool > d_made_multi_trigger;
-private:
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
- /** generate triggers */
- void generateTriggers( Node f );
-public:
- /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
- rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
- rgfr is the frequency at which triggers are generated */
- InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :
- InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){
- setRegenerateFrequency( rgfr );
- }
- ~InstStrategyAutoGenTriggers(){}
-public:
- /** get auto-generated trigger */
- inst::Trigger* getAutoGenTrigger( Node f );
- /** identify */
- std::string identify() const { return std::string("AutoGenTriggers"); }
- /** set regenerate frequency, if fr<0, turn off regenerate */
- void setRegenerateFrequency( int fr ){
- if( fr<0 ){
- d_regenerate = false;
- }else{
- d_regenerate_frequency = fr;
- d_regenerate = true;
- }
- }
- /** set generate additional */
- void setGenerateAdditional( bool val ) { d_generate_additional = val; }
-};/* class InstStrategyAutoGenTriggers */
-
-class InstStrategyFreeVariable : public InstStrategy{
-private:
- /** guessed instantiations */
- std::map< Node, bool > d_guessed;
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstStrategyFreeVariable( QuantifiersEngine* qe ) :
- InstStrategy( qe ){}
- ~InstStrategyFreeVariable(){}
- /** identify */
- std::string identify() const { return std::string("FreeVariable"); }
-};/* class InstStrategyFreeVariable */
-
-}
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif
+/********************* */ +/*! \file inst_strategy_e_matching.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): bobot, mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief E matching instantiation strategies + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H +#define __CVC4__INST_STRATEGY_E_MATCHING_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/trigger.h" + +#include "context/context.h" +#include "context/context_mm.h" + +#include "util/statistics_registry.h" +#include "theory/quantifiers/instantiation_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +//instantiation strategies + +class InstStrategyUserPatterns : public InstStrategy{ +private: + /** explicitly provided patterns */ + std::map< Node, std::vector< inst::Trigger* > > d_user_gen; + /** counter for quantifiers */ + std::map< Node, int > d_counter; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e ); +public: + InstStrategyUserPatterns( QuantifiersEngine* ie ) : + InstStrategy( ie ){} + ~InstStrategyUserPatterns(){} +public: + /** add pattern */ + void addUserPattern( Node f, Node pat ); + /** get num patterns */ + int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); } + /** get user pattern */ + inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; } + /** identify */ + std::string identify() const { return std::string("UserPatterns"); } +};/* class InstStrategyUserPatterns */ + +class InstStrategyAutoGenTriggers : public InstStrategy{ +public: + enum { + RELEVANCE_NONE, + RELEVANCE_DEFAULT, + }; +private: + /** trigger generation strategy */ + int d_tr_strategy; + /** relevance strategy */ + int d_rlv_strategy; + /** regeneration */ + bool d_regenerate; + int d_regenerate_frequency; + /** generate additional triggers */ + bool d_generate_additional; + /** triggers for each quantifier */ + std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger; + std::map< Node, int > d_counter; + /** single, multi triggers for each quantifier */ + std::map< Node, std::vector< Node > > d_patTerms[2]; + std::map< Node, bool > d_is_single_trigger; + std::map< Node, bool > d_single_trigger_gen; + std::map< Node, bool > d_made_multi_trigger; +private: + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e ); + /** generate triggers */ + void generateTriggers( Node f ); +public: + /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all) + rstrt is the relevance setting for trigger (use only relevant triggers vs. use all) + rgfr is the frequency at which triggers are generated */ + InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) : + InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){ + setRegenerateFrequency( rgfr ); + } + ~InstStrategyAutoGenTriggers(){} +public: + /** get auto-generated trigger */ + inst::Trigger* getAutoGenTrigger( Node f ); + /** identify */ + std::string identify() const { return std::string("AutoGenTriggers"); } + /** set regenerate frequency, if fr<0, turn off regenerate */ + void setRegenerateFrequency( int fr ){ + if( fr<0 ){ + d_regenerate = false; + }else{ + d_regenerate_frequency = fr; + d_regenerate = true; + } + } + /** set generate additional */ + void setGenerateAdditional( bool val ) { d_generate_additional = val; } +};/* class InstStrategyAutoGenTriggers */ + +class InstStrategyFreeVariable : public InstStrategy{ +private: + /** guessed instantiations */ + std::map< Node, bool > d_guessed; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e ); +public: + InstStrategyFreeVariable( QuantifiersEngine* qe ) : + InstStrategy( qe ){} + ~InstStrategyFreeVariable(){} + /** identify */ + std::string identify() const { return std::string("FreeVariable"); } +};/* class InstStrategyFreeVariable */ + +} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index c116b73f5..5c7c9415e 100755 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -1,375 +1,375 @@ -/********************* */
-/*! \file macros.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Sort inference module
- **
- ** This class implements quantifiers macro definitions.
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/macros.h"
-#include "theory/rewriter.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-
-bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
- //first, collect macro definitions
- for( size_t i=0; i<assertions.size(); i++ ){
- if( assertions[i].getKind()==FORALL ){
- std::vector< Node > args;
- for( size_t j=0; j<assertions[i][0].getNumChildren(); j++ ){
- args.push_back( assertions[i][0][j] );
- }
- //look at the body of the quantifier for macro definition
- process( assertions[i][1], true, args, assertions[i] );
- }
- }
- //create macro defs
- for( std::map< Node, std::vector< std::pair< Node, Node > > >::iterator it = d_macro_def_cases.begin();
- it != d_macro_def_cases.end(); ++it ){
- //create ite based on case definitions
- Node val;
- for( size_t i=0; i<it->second.size(); ++i ){
- if( it->second[i].first.isNull() ){
- Assert( i==0 );
- val = it->second[i].second;
- }else{
- //if value is null, must generate it
- if( val.isNull() ){
- std::stringstream ss;
- ss << "mdo_" << it->first << "_$$";
- Node op = NodeManager::currentNM()->mkSkolem( ss.str(), it->first.getType(), "op created during macro definitions" );
- //will be defined in terms of fresh operator
- std::vector< Node > children;
- children.push_back( op );
- children.insert( children.end(), d_macro_basis[ it->first ].begin(), d_macro_basis[ it->first ].end() );
- val = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- }
- val = NodeManager::currentNM()->mkNode( ITE, it->second[i].first, it->second[i].second, val );
- }
- }
- d_macro_defs[ it->first ] = val;
- Trace("macros-def") << "* " << val << " is a macro for " << it->first << std::endl;
- }
- //now simplify bodies
- for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
- d_macro_defs[ it->first ] = Rewriter::rewrite( simplify( it->second ) );
- }
- bool retVal = false;
- if( doRewrite && !d_macro_defs.empty() ){
- //now, rewrite based on macro definitions
- for( size_t i=0; i<assertions.size(); i++ ){
- Node prev = assertions[i];
- assertions[i] = simplify( assertions[i] );
- if( prev!=assertions[i] ){
- assertions[i] = Rewriter::rewrite( assertions[i] );
- Trace("macros-rewrite") << "Rewrite " << prev << " to " << assertions[i] << std::endl;
- retVal = true;
- }
- }
- }
- return retVal;
-}
-
-bool QuantifierMacros::contains( Node n, Node n_s ){
- if( n==n_s ){
- return true;
- }else{
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( contains( n[i], n_s ) ){
- return true;
- }
- }
- return false;
- }
-}
-
-bool QuantifierMacros::containsBadOp( Node n, Node n_op ){
- if( n!=n_op ){
- if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- if( op==n_op.getOperator() ){
- return true;
- }
- if( d_macro_def_cases.find( op )!=d_macro_def_cases.end() && !d_macro_def_cases[op].empty() ){
- return true;
- }
- }
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( containsBadOp( n[i], n_op ) ){
- return true;
- }
- }
- }
- return false;
-}
-
-bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
- return pol && n.getKind()==EQUAL;//( n.getKind()==EQUAL || n.getKind()==IFF );
-}
-
-void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){
- if( n.getKind()==APPLY_UF ){
- candidates.push_back( n );
- }else if( n.getKind()==PLUS ){
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- getMacroCandidates( n[i], candidates );
- }
- }else if( n.getKind()==MULT ){
- //if the LHS is a constant
- if( n.getNumChildren()==2 && n[0].isConst() ){
- getMacroCandidates( n[1], candidates );
- }
- }
-}
-
-Node QuantifierMacros::solveInEquality( Node n, Node lit ){
- if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
- //return the opposite side of the equality if defined that way
- for( int i=0; i<2; i++ ){
- if( lit[i]==n ){
- return lit[ i==0 ? 1 : 0];
- }
- }
- //must solve for term n in the literal lit
- if( lit[0].getType().isInteger() || lit[0].getType().isReal() ){
- Node coeff;
- Node term;
- //could be solved for on LHS
- if( lit[0].getKind()==MULT && lit[0][1]==n ){
- Assert( lit[0][0].isConst() );
- term = lit[1];
- coeff = lit[0][0];
- }else{
- Assert( lit[1].getKind()==PLUS );
- std::vector< Node > plus_children;
- //find monomial with n
- for( size_t j=0; j<lit[1].getNumChildren(); j++ ){
- if( lit[1][j]==n ){
- Assert( coeff.isNull() );
- coeff = NodeManager::currentNM()->mkConst( Rational(1) );
- }else if( lit[1][j].getKind()==MULT && lit[1][j][1]==n ){
- Assert( coeff.isNull() );
- Assert( lit[1][j][0].isConst() );
- coeff = lit[1][j][0];
- }else{
- plus_children.push_back( lit[1][j] );
- }
- }
- if( !coeff.isNull() ){
- term = NodeManager::currentNM()->mkNode( PLUS, plus_children );
- term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );
- }
- }
- if( !coeff.isNull() ){
- coeff = NodeManager::currentNM()->mkConst( Rational(1) / coeff.getConst<Rational>() );
- term = NodeManager::currentNM()->mkNode( MULT, coeff, term );
- term = Rewriter::rewrite( term );
- return term;
- }
- }
- }
- Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;
- return Node::null();
-}
-
-bool QuantifierMacros::isConsistentDefinition( Node op, Node cond, Node def ){
- if( d_macro_def_cases[op].empty() || ( cond.isNull() && !d_macro_def_cases[op][0].first.isNull() ) ){
- return true;
- }else{
- return false;
- }
-}
-
-bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ){
- if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
- if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
- if( retOnly ){
- return true;
- }else{
- vars.push_back( n );
- }
- }
- }
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){
- return true;
- }
- }
- return false;
-}
-
-bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
- std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){
- bool success = true;
- for( size_t a=0; a<v_quant.size(); a++ ){
- if( !solved[ v_quant[a] ].isNull() ){
- vars.push_back( v_quant[a] );
- subs.push_back( solved[ v_quant[a] ] );
- }else{
- if( reqComplete ){
- success = false;
- break;
- }
- }
- }
- return success;
-}
-
-void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
- if( n.getKind()==NOT ){
- process( n[0], !pol, args, f );
- }else if( n.getKind()==AND || n.getKind()==OR || n.getKind()==IMPLIES ){
- //bool favorPol = (n.getKind()==AND)==pol;
- //conditional?
- }else if( n.getKind()==ITE ){
- //can not do anything
- }else{
- //literal case
- if( isMacroLiteral( n, pol ) ){
- std::vector< Node > candidates;
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- getMacroCandidates( n[i], candidates );
- }
- for( size_t i=0; i<candidates.size(); i++ ){
- Node m = candidates[i];
- Node op = m.getOperator();
- if( !containsBadOp( n, m ) ){
- std::vector< Node > fvs;
- getFreeVariables( m, args, fvs, false );
- //get definition and condition
- Node n_def = solveInEquality( m, n ); //definition for the macro
- //definition must exist and not contain any free variables apart from fvs
- if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) ){
- Node n_cond; //condition when this definition holds
- //conditional must not contain any free variables apart from fvs
- if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){
- Trace("macros") << m << " is possible macro in " << f << std::endl;
- //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
- // x1 ... xn are distinct variables
- if( d_macro_basis[op].empty() ){
- for( size_t a=0; a<m.getNumChildren(); a++ ){
- std::stringstream ss;
- ss << "mda_" << op << "_$$";
- Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
- d_macro_basis[op].push_back( v );
- }
- }
- std::vector< Node > eq;
- for( size_t a=0; a<m.getNumChildren(); a++ ){
- eq.push_back( m[a] );
- }
- //solve system of equations "d_macro_basis[op] = m" for variables in fvs
- std::map< Node, Node > solved;
- //solve obvious cases first
- for( size_t a=0; a<eq.size(); a++ ){
- if( std::find( fvs.begin(), fvs.end(), eq[a] )!=fvs.end() ){
- if( solved[ eq[a] ].isNull() ){
- solved[ eq[a] ] = d_macro_basis[op][a];
- }
- }
- }
- //now, apply substitution for obvious cases
- std::vector< Node > vars;
- std::vector< Node > subs;
- getSubstitution( fvs, solved, vars, subs, false );
- for( size_t a=0; a<eq.size(); a++ ){
- eq[a] = eq[a].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- }
-
- Trace("macros-eq") << "Solve system of equations : " << std::endl;
- for( size_t a=0; a<m.getNumChildren(); a++ ){
- if( d_macro_basis[op][a]!=eq[a] ){
- Trace("macros-eq") << " " << d_macro_basis[op][a] << " = " << eq[a] << std::endl;
- }
- }
- Trace("macros-eq") << " for ";
- for( size_t a=0; a<fvs.size(); a++ ){
- if( solved[ fvs[a] ].isNull() ){
- Trace("macros-eq") << fvs[a] << " ";
- }
- }
- Trace("macros-eq") << std::endl;
- //DO_THIS
-
-
- vars.clear();
- subs.clear();
- if( getSubstitution( fvs, solved, vars, subs, true ) ){
- //build condition
- std::vector< Node > conds;
- if( !n_cond.isNull() ){
- //must apply substitution obtained from solving system of equations to original condition
- n_cond = n_cond.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- conds.push_back( n_cond );
- }
- for( size_t a=0; a<eq.size(); a++ ){
- //collect conditions based on solving argument's system of equations
- if( d_macro_basis[op][a]!=eq[a] ){
- conds.push_back( NodeManager::currentNM()->mkNode( eq[a].getType().isBoolean() ? IFF : EQUAL, d_macro_basis[op][a], eq[a] ) );
- }
- }
- //build the condition
- if( !conds.empty() ){
- n_cond = conds.size()==1 ? conds[0] : NodeManager::currentNM()->mkNode( AND, conds );
- }
- //apply the substitution to the
- n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- //now see if definition is consistent with others
- if( isConsistentDefinition( op, n_cond, n_def ) ){
- //must clear if it is a base definition
- if( n_cond.isNull() ){
- d_macro_def_cases[ op ].clear();
- }
- d_macro_def_cases[ op ].push_back( std::pair< Node, Node >( n_cond, n_def ) );
- }
- }
- }
- }
- }
- }
- }
- }
-}
-
-Node QuantifierMacros::simplify( Node n ){
- Trace("macros-debug") << "simplify " << n << std::endl;
- std::vector< Node > children;
- bool childChanged = false;
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- Node nn = simplify( n[i] );
- children.push_back( nn );
- childChanged = childChanged || nn!=n[i];
- }
- if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){
- //do subsitutition
- Node ret = d_macro_defs[op];
- ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() );
- return ret;
- }
- }
- if( childChanged ){
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.insert( children.begin(), n.getOperator() );
- }
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }else{
- return n;
- }
-}
+/********************* */ +/*! \file macros.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Sort inference module + ** + ** This class implements quantifiers macro definitions. + **/ + +#include <vector> + +#include "theory/quantifiers/macros.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; +using namespace CVC4::context; + +bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ + //first, collect macro definitions + for( size_t i=0; i<assertions.size(); i++ ){ + if( assertions[i].getKind()==FORALL ){ + std::vector< Node > args; + for( size_t j=0; j<assertions[i][0].getNumChildren(); j++ ){ + args.push_back( assertions[i][0][j] ); + } + //look at the body of the quantifier for macro definition + process( assertions[i][1], true, args, assertions[i] ); + } + } + //create macro defs + for( std::map< Node, std::vector< std::pair< Node, Node > > >::iterator it = d_macro_def_cases.begin(); + it != d_macro_def_cases.end(); ++it ){ + //create ite based on case definitions + Node val; + for( size_t i=0; i<it->second.size(); ++i ){ + if( it->second[i].first.isNull() ){ + Assert( i==0 ); + val = it->second[i].second; + }else{ + //if value is null, must generate it + if( val.isNull() ){ + std::stringstream ss; + ss << "mdo_" << it->first << "_$$"; + Node op = NodeManager::currentNM()->mkSkolem( ss.str(), it->first.getType(), "op created during macro definitions" ); + //will be defined in terms of fresh operator + std::vector< Node > children; + children.push_back( op ); + children.insert( children.end(), d_macro_basis[ it->first ].begin(), d_macro_basis[ it->first ].end() ); + val = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + } + val = NodeManager::currentNM()->mkNode( ITE, it->second[i].first, it->second[i].second, val ); + } + } + d_macro_defs[ it->first ] = val; + Trace("macros-def") << "* " << val << " is a macro for " << it->first << std::endl; + } + //now simplify bodies + for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){ + d_macro_defs[ it->first ] = Rewriter::rewrite( simplify( it->second ) ); + } + bool retVal = false; + if( doRewrite && !d_macro_defs.empty() ){ + //now, rewrite based on macro definitions + for( size_t i=0; i<assertions.size(); i++ ){ + Node prev = assertions[i]; + assertions[i] = simplify( assertions[i] ); + if( prev!=assertions[i] ){ + assertions[i] = Rewriter::rewrite( assertions[i] ); + Trace("macros-rewrite") << "Rewrite " << prev << " to " << assertions[i] << std::endl; + retVal = true; + } + } + } + return retVal; +} + +bool QuantifierMacros::contains( Node n, Node n_s ){ + if( n==n_s ){ + return true; + }else{ + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( contains( n[i], n_s ) ){ + return true; + } + } + return false; + } +} + +bool QuantifierMacros::containsBadOp( Node n, Node n_op ){ + if( n!=n_op ){ + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( op==n_op.getOperator() ){ + return true; + } + if( d_macro_def_cases.find( op )!=d_macro_def_cases.end() && !d_macro_def_cases[op].empty() ){ + return true; + } + } + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( containsBadOp( n[i], n_op ) ){ + return true; + } + } + } + return false; +} + +bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ + return pol && n.getKind()==EQUAL;//( n.getKind()==EQUAL || n.getKind()==IFF ); +} + +void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){ + if( n.getKind()==APPLY_UF ){ + candidates.push_back( n ); + }else if( n.getKind()==PLUS ){ + for( size_t i=0; i<n.getNumChildren(); i++ ){ + getMacroCandidates( n[i], candidates ); + } + }else if( n.getKind()==MULT ){ + //if the LHS is a constant + if( n.getNumChildren()==2 && n[0].isConst() ){ + getMacroCandidates( n[1], candidates ); + } + } +} + +Node QuantifierMacros::solveInEquality( Node n, Node lit ){ + if( lit.getKind()==IFF || lit.getKind()==EQUAL ){ + //return the opposite side of the equality if defined that way + for( int i=0; i<2; i++ ){ + if( lit[i]==n ){ + return lit[ i==0 ? 1 : 0]; + } + } + //must solve for term n in the literal lit + if( lit[0].getType().isInteger() || lit[0].getType().isReal() ){ + Node coeff; + Node term; + //could be solved for on LHS + if( lit[0].getKind()==MULT && lit[0][1]==n ){ + Assert( lit[0][0].isConst() ); + term = lit[1]; + coeff = lit[0][0]; + }else{ + Assert( lit[1].getKind()==PLUS ); + std::vector< Node > plus_children; + //find monomial with n + for( size_t j=0; j<lit[1].getNumChildren(); j++ ){ + if( lit[1][j]==n ){ + Assert( coeff.isNull() ); + coeff = NodeManager::currentNM()->mkConst( Rational(1) ); + }else if( lit[1][j].getKind()==MULT && lit[1][j][1]==n ){ + Assert( coeff.isNull() ); + Assert( lit[1][j][0].isConst() ); + coeff = lit[1][j][0]; + }else{ + plus_children.push_back( lit[1][j] ); + } + } + if( !coeff.isNull() ){ + term = NodeManager::currentNM()->mkNode( PLUS, plus_children ); + term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term ); + } + } + if( !coeff.isNull() ){ + coeff = NodeManager::currentNM()->mkConst( Rational(1) / coeff.getConst<Rational>() ); + term = NodeManager::currentNM()->mkNode( MULT, coeff, term ); + term = Rewriter::rewrite( term ); + return term; + } + } + } + Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl; + return Node::null(); +} + +bool QuantifierMacros::isConsistentDefinition( Node op, Node cond, Node def ){ + if( d_macro_def_cases[op].empty() || ( cond.isNull() && !d_macro_def_cases[op][0].first.isNull() ) ){ + return true; + }else{ + return false; + } +} + +bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ){ + if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){ + if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ + if( retOnly ){ + return true; + }else{ + vars.push_back( n ); + } + } + } + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){ + return true; + } + } + return false; +} + +bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, + std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){ + bool success = true; + for( size_t a=0; a<v_quant.size(); a++ ){ + if( !solved[ v_quant[a] ].isNull() ){ + vars.push_back( v_quant[a] ); + subs.push_back( solved[ v_quant[a] ] ); + }else{ + if( reqComplete ){ + success = false; + break; + } + } + } + return success; +} + +void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){ + if( n.getKind()==NOT ){ + process( n[0], !pol, args, f ); + }else if( n.getKind()==AND || n.getKind()==OR || n.getKind()==IMPLIES ){ + //bool favorPol = (n.getKind()==AND)==pol; + //conditional? + }else if( n.getKind()==ITE ){ + //can not do anything + }else{ + //literal case + if( isMacroLiteral( n, pol ) ){ + std::vector< Node > candidates; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + getMacroCandidates( n[i], candidates ); + } + for( size_t i=0; i<candidates.size(); i++ ){ + Node m = candidates[i]; + Node op = m.getOperator(); + if( !containsBadOp( n, m ) ){ + std::vector< Node > fvs; + getFreeVariables( m, args, fvs, false ); + //get definition and condition + Node n_def = solveInEquality( m, n ); //definition for the macro + //definition must exist and not contain any free variables apart from fvs + if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) ){ + Node n_cond; //condition when this definition holds + //conditional must not contain any free variables apart from fvs + if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){ + Trace("macros") << m << " is possible macro in " << f << std::endl; + //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where + // x1 ... xn are distinct variables + if( d_macro_basis[op].empty() ){ + for( size_t a=0; a<m.getNumChildren(); a++ ){ + std::stringstream ss; + ss << "mda_" << op << "_$$"; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); + d_macro_basis[op].push_back( v ); + } + } + std::vector< Node > eq; + for( size_t a=0; a<m.getNumChildren(); a++ ){ + eq.push_back( m[a] ); + } + //solve system of equations "d_macro_basis[op] = m" for variables in fvs + std::map< Node, Node > solved; + //solve obvious cases first + for( size_t a=0; a<eq.size(); a++ ){ + if( std::find( fvs.begin(), fvs.end(), eq[a] )!=fvs.end() ){ + if( solved[ eq[a] ].isNull() ){ + solved[ eq[a] ] = d_macro_basis[op][a]; + } + } + } + //now, apply substitution for obvious cases + std::vector< Node > vars; + std::vector< Node > subs; + getSubstitution( fvs, solved, vars, subs, false ); + for( size_t a=0; a<eq.size(); a++ ){ + eq[a] = eq[a].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + } + + Trace("macros-eq") << "Solve system of equations : " << std::endl; + for( size_t a=0; a<m.getNumChildren(); a++ ){ + if( d_macro_basis[op][a]!=eq[a] ){ + Trace("macros-eq") << " " << d_macro_basis[op][a] << " = " << eq[a] << std::endl; + } + } + Trace("macros-eq") << " for "; + for( size_t a=0; a<fvs.size(); a++ ){ + if( solved[ fvs[a] ].isNull() ){ + Trace("macros-eq") << fvs[a] << " "; + } + } + Trace("macros-eq") << std::endl; + //DO_THIS + + + vars.clear(); + subs.clear(); + if( getSubstitution( fvs, solved, vars, subs, true ) ){ + //build condition + std::vector< Node > conds; + if( !n_cond.isNull() ){ + //must apply substitution obtained from solving system of equations to original condition + n_cond = n_cond.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + conds.push_back( n_cond ); + } + for( size_t a=0; a<eq.size(); a++ ){ + //collect conditions based on solving argument's system of equations + if( d_macro_basis[op][a]!=eq[a] ){ + conds.push_back( NodeManager::currentNM()->mkNode( eq[a].getType().isBoolean() ? IFF : EQUAL, d_macro_basis[op][a], eq[a] ) ); + } + } + //build the condition + if( !conds.empty() ){ + n_cond = conds.size()==1 ? conds[0] : NodeManager::currentNM()->mkNode( AND, conds ); + } + //apply the substitution to the + n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + //now see if definition is consistent with others + if( isConsistentDefinition( op, n_cond, n_def ) ){ + //must clear if it is a base definition + if( n_cond.isNull() ){ + d_macro_def_cases[ op ].clear(); + } + d_macro_def_cases[ op ].push_back( std::pair< Node, Node >( n_cond, n_def ) ); + } + } + } + } + } + } + } + } +} + +Node QuantifierMacros::simplify( Node n ){ + Trace("macros-debug") << "simplify " << n << std::endl; + std::vector< Node > children; + bool childChanged = false; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + Node nn = simplify( n[i] ); + children.push_back( nn ); + childChanged = childChanged || nn!=n[i]; + } + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){ + //do subsitutition + Node ret = d_macro_defs[op]; + ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() ); + return ret; + } + } + if( childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } +} diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index b1fbb3e68..f4e58665d 100755 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -1,62 +1,62 @@ -/********************* */
-/*! \file macros.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Pre-process step for detecting quantifier macro definitions
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_MACROS_H
-#define __CVC4__QUANTIFIERS_MACROS_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class QuantifierMacros{
-private:
- void process( Node n, bool pol, std::vector< Node >& args, Node f );
- bool contains( Node n, Node n_s );
- bool containsBadOp( Node n, Node n_op );
- bool isMacroLiteral( Node n, bool pol );
- void getMacroCandidates( Node n, std::vector< Node >& candidates );
- Node solveInEquality( Node n, Node lit );
- bool isConsistentDefinition( Node op, Node cond, Node def );
- bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly );
- bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
- std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete );
- //map from operators to macro basis terms
- std::map< Node, std::vector< Node > > d_macro_basis;
- //map from operators to map from conditions to definition cases
- std::map< Node, std::vector< std::pair< Node, Node > > > d_macro_def_cases;
- //map from operators to macro definition
- std::map< Node, Node > d_macro_defs;
-private:
- Node simplify( Node n );
-public:
- QuantifierMacros(){}
- ~QuantifierMacros(){}
-
- bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file macros.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process step for detecting quantifier macro definitions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_MACROS_H +#define __CVC4__QUANTIFIERS_MACROS_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class QuantifierMacros{ +private: + void process( Node n, bool pol, std::vector< Node >& args, Node f ); + bool contains( Node n, Node n_s ); + bool containsBadOp( Node n, Node n_op ); + bool isMacroLiteral( Node n, bool pol ); + void getMacroCandidates( Node n, std::vector< Node >& candidates ); + Node solveInEquality( Node n, Node lit ); + bool isConsistentDefinition( Node op, Node cond, Node def ); + bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ); + bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, + std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ); + //map from operators to macro basis terms + std::map< Node, std::vector< Node > > d_macro_basis; + //map from operators to map from conditions to definition cases + std::map< Node, std::vector< std::pair< Node, Node > > > d_macro_def_cases; + //map from operators to macro definition + std::map< Node, Node > d_macro_defs; +private: + Node simplify( Node n ); +public: + QuantifierMacros(){} + ~QuantifierMacros(){} + + bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index d1b0e0fea..a78cd5612 100755 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -1,145 +1,145 @@ -/********************* */
-/*! \file quant_util.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot, mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of quantifier utilities
- **/
-
-#include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
-void QuantRelevance::registerQuantifier( Node f ){
- //compute symbols in f
- std::vector< Node > syms;
- computeSymbols( f[1], syms );
- d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() );
- //set initial relevance
- int minRelevance = -1;
- for( int i=0; i<(int)syms.size(); i++ ){
- d_syms_quants[ syms[i] ].push_back( f );
- int r = getRelevance( syms[i] );
- if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){
- minRelevance = r;
- }
- }
- if( minRelevance!=-1 ){
- setRelevance( f, minRelevance+1 );
- }
-}
-
-
-/** compute symbols */
-void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){
- if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- if( std::find( syms.begin(), syms.end(), op )==syms.end() ){
- syms.push_back( op );
- }
- }
- if( n.getKind()!=FORALL ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- computeSymbols( n[i], syms );
- }
- }
-}
-
-/** set relevance */
-void QuantRelevance::setRelevance( Node s, int r ){
- if( d_computeRel ){
- int rOld = getRelevance( s );
- if( rOld==-1 || r<rOld ){
- d_relevance[s] = r;
- if( s.getKind()==FORALL ){
- for( int i=0; i<(int)d_syms[s].size(); i++ ){
- setRelevance( d_syms[s][i], r );
- }
- }else{
- for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){
- setRelevance( d_syms_quants[s][i], r+1 );
- }
- }
- }
- }
-}
-
-
-QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
- std::map< Node, int > phaseReqs2;
- computePhaseReqs( n, false, phaseReqs2 );
- for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
- if( it->second==1 ){
- d_phase_reqs[ it->first ] = true;
- }else if( it->second==-1 ){
- d_phase_reqs[ it->first ] = false;
- }
- }
- Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;
- //now, compute if any patterns are equality required
- if( computeEq ){
- for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
- Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl;
- if( it->first.getKind()==EQUAL ){
- if( it->first[0].hasAttribute(InstConstantAttribute()) ){
- if( !it->first[1].hasAttribute(InstConstantAttribute()) ){
- d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
- d_phase_reqs_equality[ it->first[0] ] = it->second;
- Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
- }
- }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){
- d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
- d_phase_reqs_equality[ it->first[1] ] = it->second;
- Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
- }
- }
- }
- }
-}
-
-void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
- bool newReqPol = false;
- bool newPolarity;
- if( n.getKind()==NOT ){
- newReqPol = true;
- newPolarity = !polarity;
- }else if( n.getKind()==OR || n.getKind()==IMPLIES ){
- if( !polarity ){
- newReqPol = true;
- newPolarity = false;
- }
- }else if( n.getKind()==AND ){
- if( polarity ){
- newReqPol = true;
- newPolarity = true;
- }
- }else{
- int val = polarity ? 1 : -1;
- if( phaseReqs.find( n )==phaseReqs.end() ){
- phaseReqs[n] = val;
- }else if( val!=phaseReqs[n] ){
- phaseReqs[n] = 0;
- }
- }
- if( newReqPol ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( n.getKind()==IMPLIES && i==0 ){
- computePhaseReqs( n[i], !newPolarity, phaseReqs );
- }else{
- computePhaseReqs( n[i], newPolarity, phaseReqs );
- }
- }
- }
-}
+/********************* */ +/*! \file quant_util.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of quantifier utilities + **/ + +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; + +void QuantRelevance::registerQuantifier( Node f ){ + //compute symbols in f + std::vector< Node > syms; + computeSymbols( f[1], syms ); + d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() ); + //set initial relevance + int minRelevance = -1; + for( int i=0; i<(int)syms.size(); i++ ){ + d_syms_quants[ syms[i] ].push_back( f ); + int r = getRelevance( syms[i] ); + if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){ + minRelevance = r; + } + } + if( minRelevance!=-1 ){ + setRelevance( f, minRelevance+1 ); + } +} + + +/** compute symbols */ +void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){ + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( std::find( syms.begin(), syms.end(), op )==syms.end() ){ + syms.push_back( op ); + } + } + if( n.getKind()!=FORALL ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + computeSymbols( n[i], syms ); + } + } +} + +/** set relevance */ +void QuantRelevance::setRelevance( Node s, int r ){ + if( d_computeRel ){ + int rOld = getRelevance( s ); + if( rOld==-1 || r<rOld ){ + d_relevance[s] = r; + if( s.getKind()==FORALL ){ + for( int i=0; i<(int)d_syms[s].size(); i++ ){ + setRelevance( d_syms[s][i], r ); + } + }else{ + for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){ + setRelevance( d_syms_quants[s][i], r+1 ); + } + } + } + } +} + + +QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ + std::map< Node, int > phaseReqs2; + computePhaseReqs( n, false, phaseReqs2 ); + for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){ + if( it->second==1 ){ + d_phase_reqs[ it->first ] = true; + }else if( it->second==-1 ){ + d_phase_reqs[ it->first ] = false; + } + } + Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl; + //now, compute if any patterns are equality required + if( computeEq ){ + for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){ + Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; + if( it->first.getKind()==EQUAL ){ + if( it->first[0].hasAttribute(InstConstantAttribute()) ){ + if( !it->first[1].hasAttribute(InstConstantAttribute()) ){ + d_phase_reqs_equality_term[ it->first[0] ] = it->first[1]; + d_phase_reqs_equality[ it->first[0] ] = it->second; + Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; + } + }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){ + d_phase_reqs_equality_term[ it->first[1] ] = it->first[0]; + d_phase_reqs_equality[ it->first[1] ] = it->second; + Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; + } + } + } + } +} + +void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){ + bool newReqPol = false; + bool newPolarity; + if( n.getKind()==NOT ){ + newReqPol = true; + newPolarity = !polarity; + }else if( n.getKind()==OR || n.getKind()==IMPLIES ){ + if( !polarity ){ + newReqPol = true; + newPolarity = false; + } + }else if( n.getKind()==AND ){ + if( polarity ){ + newReqPol = true; + newPolarity = true; + } + }else{ + int val = polarity ? 1 : -1; + if( phaseReqs.find( n )==phaseReqs.end() ){ + phaseReqs[n] = val; + }else if( val!=phaseReqs[n] ){ + phaseReqs[n] = 0; + } + } + if( newReqPol ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( n.getKind()==IMPLIES && i==0 ){ + computePhaseReqs( n[i], !newPolarity, phaseReqs ); + }else{ + computePhaseReqs( n[i], newPolarity, phaseReqs ); + } + } + } +} diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index bb6855c47..1daaf3ea1 100755 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -1,99 +1,99 @@ -/********************* */
-/*! \file quant_util.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, bobot
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief quantifier util
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANT_UTIL_H
-#define __CVC4__THEORY__QUANT_UTIL_H
-
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-
-#include <ext/hash_set>
-#include <iostream>
-#include <map>
-
-namespace CVC4 {
-namespace theory {
-
-
-class QuantRelevance
-{
-private:
- /** for computing relavance */
- bool d_computeRel;
- /** map from quantifiers to symbols they contain */
- std::map< Node, std::vector< Node > > d_syms;
- /** map from symbols to quantifiers */
- std::map< Node, std::vector< Node > > d_syms_quants;
- /** relevance for quantifiers and symbols */
- std::map< Node, int > d_relevance;
- /** compute symbols */
- void computeSymbols( Node n, std::vector< Node >& syms );
-public:
- QuantRelevance( bool cr ) : d_computeRel( cr ){}
- ~QuantRelevance(){}
- /** register quantifier */
- void registerQuantifier( Node f );
- /** set relevance */
- void setRelevance( Node s, int r );
- /** get relevance */
- int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }
- /** get number of quantifiers for symbol s */
- int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }
-};
-
-class QuantPhaseReq
-{
-private:
- /** helper functions compute phase requirements */
- void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );
-public:
- QuantPhaseReq( Node n, bool computeEq = false );
- ~QuantPhaseReq(){}
- /** is phase required */
- bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }
- /** get phase requirement */
- bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; }
- /** phase requirements for each quantifier for each instantiation literal */
- std::map< Node, bool > d_phase_reqs;
- std::map< Node, bool > d_phase_reqs_equality;
- std::map< Node, Node > d_phase_reqs_equality_term;
-};
-
-
-class EqualityQuery {
-public:
- EqualityQuery(){}
- virtual ~EqualityQuery(){};
- /** reset */
- virtual void reset() = 0;
- /** contains term */
- virtual bool hasTerm( Node a ) = 0;
- /** get the representative of the equivalence class of a */
- virtual Node getRepresentative( Node a ) = 0;
- /** returns true if a and b are equal in the current context */
- virtual bool areEqual( Node a, Node b ) = 0;
- /** returns true is a and b are disequal in the current context */
- virtual bool areDisequal( Node a, Node b ) = 0;
- /** get the equality engine associated with this query */
- virtual eq::EqualityEngine* getEngine() = 0;
- /** get the equivalence class of a */
- virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-};/* class EqualityQuery */
-
-}
-}
-
-#endif
+/********************* */ +/*! \file quant_util.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): mdeters, bobot + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief quantifier util + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANT_UTIL_H +#define __CVC4__THEORY__QUANT_UTIL_H + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +#include <ext/hash_set> +#include <iostream> +#include <map> + +namespace CVC4 { +namespace theory { + + +class QuantRelevance +{ +private: + /** for computing relavance */ + bool d_computeRel; + /** map from quantifiers to symbols they contain */ + std::map< Node, std::vector< Node > > d_syms; + /** map from symbols to quantifiers */ + std::map< Node, std::vector< Node > > d_syms_quants; + /** relevance for quantifiers and symbols */ + std::map< Node, int > d_relevance; + /** compute symbols */ + void computeSymbols( Node n, std::vector< Node >& syms ); +public: + QuantRelevance( bool cr ) : d_computeRel( cr ){} + ~QuantRelevance(){} + /** register quantifier */ + void registerQuantifier( Node f ); + /** set relevance */ + void setRelevance( Node s, int r ); + /** get relevance */ + int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; } + /** get number of quantifiers for symbol s */ + int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); } +}; + +class QuantPhaseReq +{ +private: + /** helper functions compute phase requirements */ + void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ); +public: + QuantPhaseReq( Node n, bool computeEq = false ); + ~QuantPhaseReq(){} + /** is phase required */ + bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); } + /** get phase requirement */ + bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; } + /** phase requirements for each quantifier for each instantiation literal */ + std::map< Node, bool > d_phase_reqs; + std::map< Node, bool > d_phase_reqs_equality; + std::map< Node, Node > d_phase_reqs_equality_term; +}; + + +class EqualityQuery { +public: + EqualityQuery(){} + virtual ~EqualityQuery(){}; + /** reset */ + virtual void reset() = 0; + /** contains term */ + virtual bool hasTerm( Node a ) = 0; + /** get the representative of the equivalence class of a */ + virtual Node getRepresentative( Node a ) = 0; + /** returns true if a and b are equal in the current context */ + virtual bool areEqual( Node a, Node b ) = 0; + /** returns true is a and b are disequal in the current context */ + virtual bool areDisequal( Node a, Node b ) = 0; + /** get the equality engine associated with this query */ + virtual eq::EqualityEngine* getEngine() = 0; + /** get the equivalence class of a */ + virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; +};/* class EqualityQuery */ + +} +} + +#endif diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 2f6dc47db..108c09c87 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -9,33 +9,33 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Implementation of QuantifiersAttributes class
- **/
-
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/options.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){
- if( n.getKind()==FORALL ){
- if( attr=="axiom" ){
- Trace("quant-attr") << "Set axiom " << n << std::endl;
- AxiomAttribute aa;
- n.setAttribute( aa, true );
- }else if( attr=="conjecture" ){
- Trace("quant-attr") << "Set conjecture " << n << std::endl;
- ConjectureAttribute ca;
- n.setAttribute( ca, true );
- }
- }else{
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- setUserAttribute( attr, n[i] );
- }
- }
-}
+ ** \brief Implementation of QuantifiersAttributes class + **/ + +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/options.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){ + if( n.getKind()==FORALL ){ + if( attr=="axiom" ){ + Trace("quant-attr") << "Set axiom " << n << std::endl; + AxiomAttribute aa; + n.setAttribute( aa, true ); + }else if( attr=="conjecture" ){ + Trace("quant-attr") << "Set conjecture " << n << std::endl; + ConjectureAttribute ca; + n.setAttribute( ca, true ); + } + }else{ + for( size_t i=0; i<n.getNumChildren(); i++ ){ + setUserAttribute( attr, n[i] ); + } + } +} diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 88bac8bc9..f5a8a749a 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -9,43 +9,43 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Attributes for the theory quantifiers
- **
- ** Attributes for the theory quantifiers.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
-#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
-
-#include "theory/rewriter.h"
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** Attribute true for quantifiers that are axioms */
-struct AxiomAttributeId {};
-typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
-
-/** Attribute true for quantifiers that are conjecture */
-struct ConjectureAttributeId {};
-typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
-
-struct QuantifiersAttributes
-{
- /** set user attribute
- * This function will apply a custom set of attributes to all top-level universal
- * quantifiers contained in n
- */
- static void setUserAttribute( const std::string& attr, Node n );
-};
-
-
-}
-}
-}
-
-#endif
+ ** \brief Attributes for the theory quantifiers + ** + ** Attributes for the theory quantifiers. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H + +#include "theory/rewriter.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Attribute true for quantifiers that are axioms */ +struct AxiomAttributeId {}; +typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; + +/** Attribute true for quantifiers that are conjecture */ +struct ConjectureAttributeId {}; +typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; + +struct QuantifiersAttributes +{ + /** set user attribute + * This function will apply a custom set of attributes to all top-level universal + * quantifiers contained in n + */ + static void setUserAttribute( const std::string& attr, Node n ); +}; + + +} +} +} + +#endif |