summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r--src/theory/quantifiers/inst_match.cpp420
1 files changed, 34 insertions, 386 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index e24b8f96a..da16010cd 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -13,41 +13,42 @@
**/
#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/term_database.h"
+
+#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_database.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 {
-InstMatch::InstMatch( TNode f ) {
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- d_vals.push_back( Node::null() );
- }
+InstMatch::InstMatch(TNode q)
+{
+ d_vals.resize(q[0].getNumChildren());
+ Assert(!d_vals.empty());
+ // resize must initialize with null nodes
+ Assert(d_vals[0].isNull());
}
InstMatch::InstMatch( InstMatch* m ) {
d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() );
}
-bool InstMatch::add( InstMatch& m ){
- for( unsigned i=0; i<d_vals.size(); i++ ){
+void InstMatch::add(InstMatch& m)
+{
+ for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+ {
if( d_vals[i].isNull() ){
d_vals[i] = m.d_vals[i];
}
}
- return true;
}
bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
- for( unsigned i=0; i<m.d_vals.size(); i++ ){
+ Assert(d_vals.size() == m.d_vals.size());
+ for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+ {
if( !m.d_vals[i].isNull() ){
if( d_vals[i].isNull() ){
d_vals[i] = m.d_vals[i];
@@ -63,7 +64,8 @@ bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
}
void InstMatch::debugPrint( const char* c ){
- for( unsigned i=0; i<d_vals.size(); i++ ){
+ for (unsigned i = 0, size = d_vals.size(); i < size; i++)
+ {
if( !d_vals[i].isNull() ){
Debug( c ) << " " << i << " -> " << d_vals[i] << std::endl;
}
@@ -71,8 +73,10 @@ void InstMatch::debugPrint( const char* c ){
}
bool InstMatch::isComplete() {
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( d_vals[i].isNull() ){
+ for (Node& v : d_vals)
+ {
+ if (v.isNull())
+ {
return false;
}
}
@@ -80,58 +84,37 @@ bool InstMatch::isComplete() {
}
bool InstMatch::empty() {
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( !d_vals[i].isNull() ){
+ for (Node& v : d_vals)
+ {
+ if (!v.isNull())
+ {
return false;
}
}
return true;
}
-void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( !d_vals[i].isNull() ){
- if( qe->getEqualityQuery()->getEngine()->hasTerm( d_vals[i] ) ){
- d_vals[i] = qe->getEqualityQuery()->getEngine()->getRepresentative( d_vals[i] );
- }
- }
- }
-}
-
-void InstMatch::applyRewrite(){
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( !d_vals[i].isNull() ){
- d_vals[i] = Rewriter::rewrite( d_vals[i] );
- }
- }
-}
-
void InstMatch::clear() {
for( unsigned i=0; i<d_vals.size(); i++ ){
d_vals[i] = Node::null();
}
}
-/** get value */
-
-Node InstMatch::get( int i ) {
- return d_vals[i];
-}
-
-void InstMatch::getTerms( Node f, std::vector< Node >& inst ){
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- inst.push_back( d_vals[i] );
- }
+Node InstMatch::get(int i) const { return d_vals[i]; }
+void InstMatch::getInst(std::vector<Node>& inst) const
+{
+ inst.insert(inst.end(), d_vals.begin(), d_vals.end());
}
void InstMatch::setValue( int i, TNode n ) {
d_vals[i] = n;
}
-
-bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
+bool InstMatch::set(EqualityQuery* q, int i, TNode n)
+{
Assert( i>=0 );
if( !d_vals[i].isNull() ){
- if( qe->getEqualityQuery()->areEqual( d_vals[i], n ) ){
+ if (q->areEqual(d_vals[i], n))
+ {
return true;
}else{
return false;
@@ -142,341 +125,6 @@ bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
}
}
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq,
- ImtIndexOrder* imtio, bool onlyExist, int index ) {
- if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
- return false;
- }else{
- int i_index = imtio ? imtio->d_order[index] : index;
- Node n = m[i_index];
- std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- bool ret = it->second.addInstMatch( qe, f, m, modEq, imtio, onlyExist, index+1 );
- if( !onlyExist || !ret ){
- return ret;
- }
- }
- if( modEq ){
- //check modulo equality if any other instantiation match exists
- if( !n.isNull() && 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 = d_data.find( en );
- if( itc!=d_data.end() ){
- if( itc->second.addInstMatch( qe, f, m, modEq, imtio, true, index+1 ) ){
- return false;
- }
- }
- }
- ++eqc;
- }
- }
- }
- if( !onlyExist ){
- d_data[n].addInstMatch( qe, f, m, modEq, imtio, false, index+1 );
- }
- return true;
- }
-}
-
-bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, ImtIndexOrder* imtio, int index ) {
- Assert( index<(int)q[0].getNumChildren() );
- Assert( !imtio || index<(int)imtio->d_order.size() );
- int i_index = imtio ? imtio->d_order[index] : index;
- Node n = m[i_index];
- std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- if( (index+1)==(int)q[0].getNumChildren() || ( imtio && (index+1)==(int)imtio->d_order.size() ) ){
- d_data.erase( n );
- return true;
- }else{
- return it->second.removeInstMatch( qe, q, m, imtio, index+1 );
- }
- }else{
- return false;
- }
-}
-
-bool InstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio, int index ){
- if( index==(int)q[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
- setInstLemma( lem );
- return true;
- }else{
- int i_index = imtio ? imtio->d_order[index] : index;
- std::map< Node, InstMatchTrie >::iterator it = d_data.find( m[i_index] );
- if( it!=d_data.end() ){
- return it->second.recordInstLemma( q, m, lem, imtio, index+1 );
- }else{
- return false;
- }
- }
-}
-
-void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const {
- if( terms.size()==q[0].getNumChildren() ){
- bool print;
- if( useActive ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- print = std::find( active.begin(), active.end(), lem )!=active.end();
- }else{
- print = false;
- }
- }else{
- print = true;
- }
- if( print ){
- if( firstTime ){
- out << "(instantiation " << q << std::endl;
- firstTime = false;
- }
- out << " ( ";
- for( unsigned i=0; i<terms.size(); i++ ){
- if( i>0 ){ out << ", ";}
- out << terms[i];
- }
- out << " )" << std::endl;
- }
- }else{
- for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second.print( out, q, terms, firstTime, useActive, active );
- terms.pop_back();
- }
- }
-}
-
-void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const {
- if( terms.size()==q[0].getNumChildren() ){
- if( useActive ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- if( std::find( active.begin(), active.end(), lem )!=active.end() ){
- insts.push_back( lem );
- }
- }
- }else{
- if( hasInstLemma() ){
- insts.push_back( getInstLemma() );
- }else{
- insts.push_back( qe->getInstantiation( q, terms, true ) );
- }
- }
- }else{
- for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second.getInstantiations( insts, q, terms, qe, useActive, active );
- terms.pop_back();
- }
- }
-}
-
-void InstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
- if( terms.size()==q[0].getNumChildren() ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){
- quant[lem] = q;
- tvec[lem].clear();
- tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() );
- }
- }
- }else{
- for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second.getExplanationForInstLemmas( q, terms, lems, quant, tvec );
- terms.pop_back();
- }
- }
-}
-
-CDInstMatchTrie::~CDInstMatchTrie() {
- for(std::map< Node, CDInstMatchTrie* >::iterator i = d_data.begin(),
- iend = d_data.end(); i != iend; ++i) {
- CDInstMatchTrie* current = (*i).second;
- delete current;
- }
- d_data.clear();
-}
-
-
-bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
- context::Context* c, bool modEq, int index, bool onlyExist ){
- bool reset = false;
- if( !d_valid.get() ){
- if( onlyExist ){
- return true;
- }else{
- d_valid.set( true );
- reset = true;
- }
- }
- if( index==(int)f[0].getNumChildren() ){
- return reset;
- }else{
- Node n = m[ index ];
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- bool ret = it->second->addInstMatch( qe, f, m, c, modEq, index+1, onlyExist );
- if( !onlyExist || !ret ){
- return reset || ret;
- }
- }
- if( modEq ){
- //check modulo equality if any other instantiation match exists
- if( !n.isNull() && 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, CDInstMatchTrie* >::iterator itc = d_data.find( en );
- if( itc!=d_data.end() ){
- if( itc->second->addInstMatch( qe, f, m, c, modEq, index+1, true ) ){
- return false;
- }
- }
- }
- ++eqc;
- }
- }
- }
-
- if( !onlyExist ){
- // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
- CDInstMatchTrie* imt = new CDInstMatchTrie( c );
- Assert(d_data.find(n) == d_data.end());
- d_data[n] = imt;
- imt->addInstMatch( qe, f, m, c, modEq, index+1, false );
- }
- return true;
- }
-}
-
-bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index ) {
- if( index==(int)q[0].getNumChildren() ){
- if( d_valid.get() ){
- d_valid.set( false );
- return true;
- }else{
- return false;
- }
- }else{
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] );
- if( it!=d_data.end() ){
- return it->second->removeInstMatch( qe, q, m, index+1 );
- }else{
- return false;
- }
- }
-}
-
-bool CDInstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index ) {
- if( index==(int)q[0].getNumChildren() ){
- if( d_valid.get() ){
- setInstLemma( lem );
- return true;
- }else{
- return false;
- }
- }else{
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] );
- if( it!=d_data.end() ){
- return it->second->recordInstLemma( q, m, lem, index+1 );
- }else{
- return false;
- }
- }
-}
-
-void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
- if( d_valid.get() ){
- if( terms.size()==q[0].getNumChildren() ){
- bool print;
- if( useActive ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- print = std::find( active.begin(), active.end(), lem )!=active.end();
- }else{
- print = false;
- }
- }else{
- print = true;
- }
- if( print ){
- if( firstTime ){
- out << "(instantiation " << q << std::endl;
- firstTime = false;
- }
- out << " ( ";
- for( unsigned i=0; i<terms.size(); i++ ){
- if( i>0 ) out << " ";
- out << terms[i];
- }
- out << " )" << std::endl;
- }
- }else{
- for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second->print( out, q, terms, firstTime, useActive, active );
- terms.pop_back();
- }
- }
- }
-}
-
-void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const{
- if( d_valid.get() ){
- if( terms.size()==q[0].getNumChildren() ){
- if( useActive ){
- if( hasInstLemma() ){
- Node lem = getInstLemma();
- if( std::find( active.begin(), active.end(), lem )!=active.end() ){
- insts.push_back( lem );
- }
- }
- }else{
- if( hasInstLemma() ){
- insts.push_back( getInstLemma() );
- }else{
- insts.push_back( qe->getInstantiation( q, terms, true ) );
- }
- }
- }else{
- for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second->getInstantiations( insts, q, terms, qe, useActive, active );
- terms.pop_back();
- }
- }
- }
-}
-
-
-void CDInstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
- if( d_valid.get() ){
- if( terms.size()==q[0].getNumChildren() ){
- if( hasInstLemma() ){
- Node lem;
- if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){
- quant[lem] = q;
- tvec[lem].clear();
- tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() );
- }
- }
- }else{
- for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
- terms.push_back( it->first );
- it->second->getExplanationForInstLemmas( q, terms, lems, quant, tvec );
- terms.pop_back();
- }
- }
- }
-}
-
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback