diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-17 13:34:54 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 13:34:54 -0600 |
commit | 0f03dbb1378354adcfef635a93f8b13987c2d983 (patch) | |
tree | 6c6dcc0e806b0867d19d01cb045a5a50764bf0e0 /src/theory/quantifiers/term_util.cpp | |
parent | d107bf9b8b4dd206580681e601a033742029ec79 (diff) |
Move methods from term util to quantifiers registry (#5916)
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
Diffstat (limited to 'src/theory/quantifiers/term_util.cpp')
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 85 |
1 files changed, 5 insertions, 80 deletions
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index b0a067630..97a731fb9 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -47,24 +47,11 @@ TermUtil::~TermUtil(){ } -void TermUtil::registerQuantifier( Node q ){ - if( d_inst_constants.find( q )==d_inst_constants.end() ){ - Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - d_vars[q].push_back( q[0][i] ); - d_var_num[q][q[0][i]] = i; - //make instantiation constants - Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() ); - d_inst_constants_map[ic] = q; - d_inst_constants[ q ].push_back( ic ); - Debug("quantifiers-engine") << " " << ic << std::endl; - //set the var number attribute - InstVarNumAttribute ivna; - ic.setAttribute( ivna, i ); - InstConstantAttribute ica; - ic.setAttribute( ica, q ); - } - } +size_t TermUtil::getVariableNum(Node q, Node v) +{ + Node::iterator it = std::find(q[0].begin(), q[0].end(), v); + Assert(it != q[0].end()); + return it - q[0].begin(); } Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) { @@ -168,68 +155,6 @@ Node TermUtil::getQuantSimplify( Node n ) { return getRemoveQuantifiers(q); } -/** get the i^th instantiation constant of q */ -Node TermUtil::getInstantiationConstant( Node q, int i ) const { - std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); - if( it!=d_inst_constants.end() ){ - return it->second[i]; - }else{ - return Node::null(); - } -} - -/** get number of instantiation constants for q */ -unsigned TermUtil::getNumInstantiationConstants( Node q ) const { - std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); - if( it!=d_inst_constants.end() ){ - return it->second.size(); - }else{ - return 0; - } -} - -Node TermUtil::getInstConstantBody( Node q ){ - std::map< Node, Node >::iterator it = d_inst_const_body.find( q ); - if( it==d_inst_const_body.end() ){ - Node n = substituteBoundVariablesToInstConstants(q[1], q); - d_inst_const_body[ q ] = n; - return n; - }else{ - return it->second; - } -} - -Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q) -{ - registerQuantifier( q ); - return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() ); -} - -Node TermUtil::substituteInstConstantsToBoundVariables(Node n, Node q) -{ - registerQuantifier( q ); - return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() ); -} - -Node TermUtil::substituteBoundVariables(Node n, - Node q, - std::vector<Node>& terms) -{ - registerQuantifier(q); - Assert(d_vars[q].size() == terms.size()); - return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() ); -} - -Node TermUtil::substituteInstConstants(Node n, Node q, std::vector<Node>& terms) -{ - registerQuantifier(q); - Assert(d_inst_constants[q].size() == terms.size()); - return n.substitute(d_inst_constants[q].begin(), - d_inst_constants[q].end(), - terms.begin(), - terms.end()); -} - void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics) { computeVarContainsInternal(n, INST_CONSTANT, ics); |