summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r--src/theory/quantifiers/term_database.cpp254
1 files changed, 114 insertions, 140 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index bb35ac4cd..d6f8b3af7 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -78,7 +78,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
}
}
-TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
+TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
@@ -98,7 +98,11 @@ unsigned TermDb::getNumGroundTerms( Node f ) {
}else{
return 0;
}
- //return d_op_ccount[f];
+}
+
+Node TermDb::getGroundTerm( Node f, unsigned i ) {
+ Assert( i<d_op_map[f].size() );
+ return d_op_map[f][i];
}
Node TermDb::getOperator( Node n ) {
@@ -128,51 +132,42 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
//don't add terms in quantifier bodies
if( withinQuant && !options::registerQuantBodyTerms() ){
return;
- }
- bool rec = false;
- if( d_processed.find( n )==d_processed.end() ){
- d_processed.insert(n);
- if( !TermDb::hasInstConstAttr(n) ){
- Trace("term-db-debug") << "register term : " << n << std::endl;
- d_type_map[ n.getType() ].push_back( n );
- //if this is an atomic trigger, consider adding it
- //Call the children?
- if( inst::Trigger::isAtomicTrigger( n ) ){
- Trace("term-db") << "register term in db " << n << std::endl;
- Node op = getOperator( n );
- /*
- int occ = d_op_ccount[op];
- if( occ<(int)d_op_map[op].size() ){
- d_op_map[op][occ] = n;
- }else{
+ }else{
+ bool rec = false;
+ if( d_processed.find( n )==d_processed.end() ){
+ d_processed.insert(n);
+ if( !TermDb::hasInstConstAttr(n) ){
+ Trace("term-db-debug") << "register term : " << n << std::endl;
+ d_type_map[ n.getType() ].push_back( n );
+ //if this is an atomic trigger, consider adding it
+ if( inst::Trigger::isAtomicTrigger( n ) ){
+ Trace("term-db") << "register term in db " << n << std::endl;
+ Node op = getOperator( n );
d_op_map[op].push_back( n );
- }
- d_op_ccount[op].set( occ + 1 );
- */
- d_op_map[op].push_back( n );
- added.insert( n );
-
- if( options::eagerInstQuant() ){
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
- int addedLemmas = 0;
- for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
- addedLemmas += d_op_triggers[op][i]->addTerm( n );
+ added.insert( n );
+
+ if( options::eagerInstQuant() ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
+ int addedLemmas = 0;
+ for( unsigned i=0; i<d_op_triggers[op].size(); i++ ){
+ addedLemmas += d_op_triggers[op][i]->addTerm( n );
+ }
}
}
}
}
}
+ rec = true;
}
- rec = true;
- }
- if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
- d_iclosure_processed.insert( n );
- rec = true;
- }
- if( rec && n.getKind()!=FORALL ){
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- addTerm( n[i], added, withinQuant, withinInstClosure );
+ if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
+ d_iclosure_processed.insert( n );
+ rec = true;
+ }
+ if( rec && n.getKind()!=FORALL ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ addTerm( n[i], added, withinQuant, withinInstClosure );
+ }
}
}
}
@@ -413,25 +408,6 @@ bool TermDb::isInstClosure( Node r ) {
return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
}
-//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
-bool TermDb::mayComplete( TypeNode tn ) {
- std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
- if( it==d_may_complete.end() ){
- bool mc = false;
- if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
- Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
- Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
- Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
- eq = Rewriter::rewrite( eq );
- mc = eq==d_true;
- }
- d_may_complete[tn] = mc;
- return mc;
- }else{
- return it->second;
- }
-}
-
void TermDb::setHasTerm( Node n ) {
Trace("term-db-debug2") << "hasTerm : " << n << std::endl;
//if( inst::Trigger::isAtomicTrigger( n ) ){
@@ -441,13 +417,14 @@ void TermDb::setHasTerm( Node n ) {
setHasTerm( n[i] );
}
}
- /*
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- setHasTerm( n[i] );
- }
- }
- */
+}
+
+void TermDb::presolve() {
+ //reset the caches that are SAT context-independent
+ d_op_map.clear();
+ d_type_map.clear();
+ d_processed.clear();
+ d_iclosure_processed.clear();
}
void TermDb::reset( Theory::Effort effort ){
@@ -593,7 +570,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
Node mbt;
if( tn.isInteger() || tn.isReal() ){
- mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+ mbt = d_zero;
}else if( isClosedEnumerableType( tn ) ){
mbt = tn.mkGroundTerm();
}else{
@@ -603,6 +580,9 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
ss << "e_" << tn;
mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
+ if( options::instMaxLevel()!=-1 ){
+ QuantifiersEngine::setInstantiationLevelAttr( mbt, 0 );
+ }
}else{
mbt = d_type_map[ tn ][ 0 ];
}
@@ -632,24 +612,24 @@ Node TermDb::getModelBasisOpTerm( Node op ){
return d_model_basis_op_term[op];
}
-Node TermDb::getModelBasis( Node f, Node n ){
+Node TermDb::getModelBasis( Node q, Node n ){
//make model basis
- if( d_model_basis_terms.find( f )==d_model_basis_terms.end() ){
- for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
- d_model_basis_terms[f].push_back( getModelBasisTerm( f[0][j].getType() ) );
+ if( d_model_basis_terms.find( q )==d_model_basis_terms.end() ){
+ for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+ d_model_basis_terms[q].push_back( getModelBasisTerm( q[0][j].getType() ) );
}
}
- Node gn = n.substitute( d_inst_constants[f].begin(), d_inst_constants[f].end(),
- d_model_basis_terms[f].begin(), d_model_basis_terms[f].end() );
+ Node gn = n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(),
+ d_model_basis_terms[q].begin(), d_model_basis_terms[q].end() );
return gn;
}
-Node TermDb::getModelBasisBody( Node f ){
- if( d_model_basis_body.find( f )==d_model_basis_body.end() ){
- Node n = getInstConstantBody( f );
- d_model_basis_body[f] = getModelBasis( f, n );
+Node TermDb::getModelBasisBody( Node q ){
+ if( d_model_basis_body.find( q )==d_model_basis_body.end() ){
+ Node n = getInstConstantBody( q );
+ d_model_basis_body[q] = getModelBasis( q, n );
}
- return d_model_basis_body[f];
+ return d_model_basis_body[q];
}
void TermDb::computeModelBasisArgAttribute( Node n ){
@@ -660,7 +640,7 @@ void TermDb::computeModelBasisArgAttribute( Node n ){
}
uint64_t val = 0;
//determine if it has model basis attribute
- for( int j=0; j<(int)n.getNumChildren(); j++ ){
+ for( unsigned j=0; j<n.getNumChildren(); j++ ){
if( n[j].getAttribute(ModelBasisAttribute()) ){
val++;
}
@@ -670,21 +650,21 @@ void TermDb::computeModelBasisArgAttribute( Node n ){
}
}
-void TermDb::makeInstantiationConstantsFor( Node f ){
- if( d_inst_constants.find( f )==d_inst_constants.end() ){
- Debug("quantifiers-engine") << "Instantiation constants for " << f << " : " << std::endl;
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- d_vars[f].push_back( f[0][i] );
+void TermDb::makeInstantiationConstantsFor( 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] );
//make instantiation constants
- Node ic = NodeManager::currentNM()->mkInstConstant( f[0][i].getType() );
- d_inst_constants_map[ic] = f;
- d_inst_constants[ f ].push_back( ic );
+ 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);
+ ic.setAttribute( ivna, i );
InstConstantAttribute ica;
- ic.setAttribute(ica,f);
+ ic.setAttribute( ica, q );
//also set the no-match attribute
NoMatchAttribute nma;
ic.setAttribute(nma,true);
@@ -695,16 +675,16 @@ void TermDb::makeInstantiationConstantsFor( Node f ){
Node TermDb::getInstConstAttr( Node n ) {
if (!n.hasAttribute(InstConstantAttribute()) ){
- Node f;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- f = getInstConstAttr(n[i]);
- if( !f.isNull() ){
+ Node q;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ q = getInstConstAttr(n[i]);
+ if( !q.isNull() ){
break;
}
}
InstConstantAttribute ica;
- n.setAttribute(ica,f);
- if( !f.isNull() ){
+ n.setAttribute(ica, q);
+ if( !q.isNull() ){
//also set the no-match attribute
NoMatchAttribute nma;
n.setAttribute(nma,true);
@@ -730,9 +710,9 @@ void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
}
-/** get the i^th instantiation constant of f */
-Node TermDb::getInstantiationConstant( Node f, int i ) const {
- std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
+/** get the i^th instantiation constant of q */
+Node TermDb::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{
@@ -740,9 +720,9 @@ Node TermDb::getInstantiationConstant( Node f, int i ) const {
}
}
-/** get number of instantiation constants for f */
-int TermDb::getNumInstantiationConstants( Node f ) const {
- std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
+/** get number of instantiation constants for q */
+int TermDb::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 (int)it->second.size();
}else{
@@ -750,19 +730,19 @@ int TermDb::getNumInstantiationConstants( Node f ) const {
}
}
-Node TermDb::getInstConstantBody( Node f ){
- std::map< Node, Node >::iterator it = d_inst_const_body.find( f );
+Node TermDb::getInstConstantBody( Node q ){
+ std::map< Node, Node >::iterator it = d_inst_const_body.find( q );
if( it==d_inst_const_body.end() ){
- Node n = getInstConstantNode( f[1], f );
- d_inst_const_body[ f ] = n;
+ Node n = getInstConstantNode( q[1], q );
+ d_inst_const_body[ q ] = n;
return n;
}else{
return it->second;
}
}
-Node TermDb::getCounterexampleLiteral( Node f ){
- if( d_ce_lit.find( f )==d_ce_lit.end() ){
+Node TermDb::getCounterexampleLiteral( Node q ){
+ if( d_ce_lit.find( q )==d_ce_lit.end() ){
/*
Node ceBody = getInstConstantBody( f );
//check if any variable are of bad types, and fail if so
@@ -776,18 +756,23 @@ Node TermDb::getCounterexampleLiteral( Node f ){
Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
//otherwise, ensure literal
Node ceLit = d_quantEngine->getValuation().ensureLiteral( g );
- d_ce_lit[ f ] = ceLit;
+ d_ce_lit[ q ] = ceLit;
}
- return d_ce_lit[ f ];
+ return d_ce_lit[ q ];
}
-Node TermDb::getInstConstantNode( Node n, Node f ){
- makeInstantiationConstantsFor( f );
- Node n2 = n.substitute( d_vars[f].begin(), d_vars[f].end(),
- d_inst_constants[f].begin(), d_inst_constants[f].end() );
+Node TermDb::getInstConstantNode( Node n, Node q ){
+ makeInstantiationConstantsFor( q );
+ Node n2 = n.substitute( d_vars[q].begin(), d_vars[q].end(),
+ d_inst_constants[q].begin(), d_inst_constants[q].end() );
return n2;
}
+Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
+ Assert( d_vars[q].size()==terms.size() );
+ return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
+}
+
void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
for( unsigned j=0; j<dc.getNumArgs(); j++ ){
@@ -979,34 +964,23 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) {
}
}
-Node TermDb::getFreeVariableForInstConstant( Node n ){
- return getFreeVariableForType( n.getType() );
-}
-
-Node TermDb::getFreeVariableForType( TypeNode tn ) {
- if( d_free_vars.find( tn )==d_free_vars.end() ){
- for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){
- if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
- d_free_vars[tn] = d_type_map[ tn ][ i ];
- }
- }
- if( d_free_vars.find( tn )==d_free_vars.end() ){
- //if integer or real, make zero
- if( tn.isInteger() || tn.isReal() ){
- Rational z(0);
- d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
- }else{
- Node n = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" );
- d_free_vars[tn] = n;
- Trace("mkVar") << "FreeVar:: Make variable " << n << " : " << tn << std::endl;
- //must set instantiation level attribute to 0 if we are using instantiation max level
- if( options::instMaxLevel()!=-1 ){
- QuantifiersEngine::setInstantiationLevelAttr( n, 0 );
- }
- }
+//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
+bool TermDb::mayComplete( TypeNode tn ) {
+ std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
+ if( it==d_may_complete.end() ){
+ bool mc = false;
+ if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
+ Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
+ Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
+ Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
+ eq = Rewriter::rewrite( eq );
+ mc = eq==d_true;
}
+ d_may_complete[tn] = mc;
+ return mc;
+ }else{
+ return it->second;
}
- return d_free_vars[tn];
}
void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) {
@@ -1328,7 +1302,7 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) {
if( create ){
if( d_vts_delta_free.isNull() ){
d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" );
- Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
+ Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero );
d_quantEngine->getOutputChannel().lemma( delta_lem );
}
if( d_vts_delta.isNull() ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback