diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-04 17:30:18 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-04 17:30:18 -0500 |
commit | aed7130284c04f7ada79db1ed3d4a8ddb08d3543 (patch) | |
tree | 5388d8ef1af23934fe381d0f1b5da796d5176a19 /src/theory/quantifiers/inst_gen.cpp | |
parent | 9c0b2f6abd82564df0686cca826015f4eb9095fa (diff) |
fixed files with DOS newlines; fixed contrib/ scripts to use git
Diffstat (limited to 'src/theory/quantifiers/inst_gen.cpp')
-rw-r--r--[-rwxr-xr-x] | src/theory/quantifiers/inst_gen.cpp | 594 |
1 files changed, 296 insertions, 298 deletions
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index d3bd6ad03..dea371e9c 100755..100644 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -1,298 +1,296 @@ -/********************* */
-/*! \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: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 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 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(); + } + } + } + } +} |