summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/candidate_generator.cpp4
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp4
-rw-r--r--src/theory/quantifiers/inst_match.cpp11
-rw-r--r--src/theory/quantifiers/inst_match.h2
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp47
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.h1
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp4
-rw-r--r--src/theory/quantifiers/rewrite_engine.cpp5
-rw-r--r--src/theory/quantifiers/rewrite_engine.h1
-rw-r--r--src/theory/quantifiers/term_database.cpp254
-rw-r--r--src/theory/quantifiers/term_database.h89
11 files changed, 196 insertions, 226 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 48041e894..4619d74e5 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -100,7 +100,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
if( d_mode==cand_term_db ){
//get next candidate term in the uf term database
while( d_term_iter<d_term_iter_limit ){
- Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+ Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter );
d_term_iter++;
if( isLegalCandidate( n ) ){
if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
@@ -221,7 +221,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() );
//must return something
d_firstTime = false;
- return d_qe->getTermDatabase()->getFreeVariableForType( d_match_pattern_type );
+ return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type );
}
return Node::null();
}
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 896cf5dff..1cdad589b 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1722,8 +1722,8 @@ void TermGenEnv::collectSignatureInformation() {
d_func_args.clear();
TypeNode tnull;
for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
- if( !getTermDatabase()->d_op_map[it->first].empty() ){
- Node nn = getTermDatabase()->d_op_map[it->first][0];
+ if( getTermDatabase()->getNumGroundTerms( it->first )>0 ){
+ Node nn = getTermDatabase()->getGroundTerm( it->first, 0 );
Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
bool do_enum = true;
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index cb969088d..180ccc448 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -88,15 +88,6 @@ bool InstMatch::empty() {
return true;
}
-void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
- for( unsigned i=0; i<d_vals.size(); i++ ){
- if( d_vals[i].isNull() ){
- Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
- d_vals[i] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
- }
- }
-}
-
void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
for( unsigned i=0; i<d_vals.size(); i++ ){
if( !d_vals[i].isNull() ){
@@ -132,7 +123,7 @@ void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& in
Node val = get( i );
if( val.isNull() ){
Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
- val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+ val = qe->getTermDatabase()->getModelBasisTerm( ic.getType() );
}
inst.push_back( val );
}
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 21220491f..6424b67d3 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -53,8 +53,6 @@ public:
void debugPrint( const char* c );
/** is complete? */
bool isComplete();
- /** make complete */
- void makeComplete( Node f, QuantifiersEngine* qe );
/** make representative */
void makeRepresentative( QuantifiersEngine* qe );
/** empty */
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 67b9d9ca2..3a626cb92 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -76,11 +76,13 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
}else{
std::map< Node, std::map< Node, bool > > subs_proc;
//Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
+ bool is_cv = false;
Node pv;
if( curr_var.empty() ){
pv = d_vars[i];
}else{
pv = curr_var.back();
+ is_cv = true;
}
TypeNode pvtn = pv.getType();
Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl;
@@ -89,19 +91,23 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
pv_value = d_qe->getModel()->getValue( pv );
Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
}
+ Node pvr = pv;
+ if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){
+ pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv );
+ }
//if in effort=2, we must choose at least one model value
if( (i+1)<d_vars.size() || effort!=2 ){
+
//[1] easy case : pv is in the equivalence class as another term not containing pv
Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
- std::map< Node, Node >::iterator itr = d_curr_rep.find( pv );
- if( itr!=d_curr_rep.end() ){
- std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( itr->second );
- Assert( it_eqc!=d_curr_eqc.end() );
+ std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
+ if( it_eqc!=d_curr_eqc.end() ){
+ Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl;
for( unsigned k=0; k<it_eqc->second.size(); k++ ){
Node n = it_eqc->second[k];
if( n!=pv ){
- Trace("cbqi-inst-debug") << "..[1] " << i << "...try based on equal term " << n << std::endl;
+ Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl;
//compute d_subs_fv, which program variables are contained in n
computeProgVars( n );
//must be an eligible term
@@ -130,22 +136,24 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
}
}
}
+ }else{
+ Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
}
//[2] : we can solve an equality for pv
if( pvtn.isInteger() || pvtn.isReal() ){
///iterate over equivalence classes to find cases where we can solve for the variable
TypeNode pvtnb = pvtn.getBaseType();
- Trace("cbqi-inst-debug") << "[2] try based on solving over equivalence classes." << std::endl;
+ Trace("cbqi-inst-debug") << "[2] try based on solving arithmetic equivalence classes." << std::endl;
for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){
Node r = d_curr_type_eqc[pvtnb][k];
- std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( r );
+ std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
std::vector< Node > lhs;
std::vector< bool > lhs_v;
std::vector< Node > lhs_coeff;
- Assert( it_eqc!=d_curr_eqc.end() );
- for( unsigned kk=0; kk<it_eqc->second.size(); kk++ ){
- Node n = it_eqc->second[kk];
+ Assert( it_reqc!=d_curr_eqc.end() );
+ for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
+ Node n = it_reqc->second[kk];
Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
//compute the variables in n
computeProgVars( n );
@@ -228,11 +236,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
}
}
}else if( pvtn.isDatatype() ){
+ Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl;
//look in equivalence class for a constructor
- if( itr!=d_curr_rep.end() ){
- std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( itr->second );
- Assert( it_eqc!=d_curr_eqc.end() );
- Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl;
+ if( it_eqc!=d_curr_eqc.end() ){
for( unsigned k=0; k<it_eqc->second.size(); k++ ){
Node n = it_eqc->second[k];
if( n.getKind()==APPLY_CONSTRUCTOR ){
@@ -240,6 +246,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
cons[pv] = n.getOperator();
const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype();
unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() );
+ if( is_cv ){
+ curr_var.pop_back();
+ }
//now must solve for selectors applied to pv
for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
@@ -253,12 +262,15 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
curr_var.pop_back();
}
+ if( is_cv ){
+ curr_var.push_back( pv );
+ }
break;
}
}
}
}else{
- Trace("cbqi-inst-debug2") << "... " << i << " does not have a representative." << std::endl;
+ Trace("cbqi-inst-debug2") << "... " << i << " does not have an eqc." << std::endl;
}
}
@@ -1122,7 +1134,6 @@ void CegInstantiator::processAssertions() {
Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl;
d_curr_asserts.clear();
d_curr_eqc.clear();
- d_curr_rep.clear();
d_curr_type_eqc.clear();
eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
@@ -1140,7 +1151,6 @@ void CegInstantiator::processAssertions() {
//collect information about eqc
if( ee->hasTerm( pv ) ){
Node pvr = ee->getRepresentative( pv );
- d_curr_rep[pv] = pvr;
if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){
Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl;
eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
@@ -1191,11 +1201,14 @@ void CegInstantiator::processAssertions() {
d_curr_type_eqc[rtn].push_back( r );
if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl;
+ Trace("cbqi-proc-debug") << " ";
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
while( !eqc_i.isFinished() ){
+ Trace("cbqi-proc-debug") << *eqc_i << " ";
d_curr_eqc[r].push_back( *eqc_i );
++eqc_i;
}
+ Trace("cbqi-proc-debug") << std::endl;
}
}
++eqcs_i;
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 6447da1a9..2074e0f4b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -58,7 +58,6 @@ private:
//current assertions
std::map< TheoryId, std::vector< Node > > d_curr_asserts;
std::map< Node, std::vector< Node > > d_curr_eqc;
- std::map< Node, Node > d_curr_rep;
std::map< TypeNode, std::vector< Node > > d_curr_type_eqc;
//auxiliary variables
std::vector< Node > d_aux_vars;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 47c2e1c5b..b7d82bc9e 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -458,9 +458,7 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
//check constraints
for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
//apply substitution to the tconstraint
- Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(),
- p->getTermDatabase()->d_vars[d_q].end(),
- terms.begin(), terms.end() );
+ Node cons = p->getTermDatabase()->getInstantiatedNode( it->first, d_q, terms );
cons = it->second ? cons : cons.negate();
if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
return true;
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 05e33c7b2..a70d36ac0 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -38,7 +38,6 @@ struct PrioritySort {
RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
- d_true = NodeManager::currentNM()->mkConst( true );
d_needsSort = false;
}
@@ -277,7 +276,7 @@ void RewriteEngine::registerQuantifier( Node f ) {
body_c.push_back( d_rr[f][1][j].negate() );
}
}
- }else if( d_rr[f][1]!=d_true ){
+ }else if( d_rr[f][1]!=d_quantEngine->getTermDatabase()->d_true ){
if( MatchGen::isHandled( d_rr[f][1] ) ){
body_c.push_back( d_rr[f][1].negate() );
}
@@ -307,4 +306,4 @@ Node RewriteEngine::getInstConstNode( Node n, Node q ) {
}else{
return it->second;
}
-} \ No newline at end of file
+}
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 2e2578af5..6ad76c541 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -39,7 +39,6 @@ class RewriteEngine : public QuantifiersModule
std::vector< Node > d_rr_quant;
std::vector< Node > d_priority_order;
std::map< Node, Node > d_rr;
- Node d_true;
/** explicitly provided patterns */
std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
/** get the quantifer info object */
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() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 477b964ee..682a9f8e0 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -134,15 +134,10 @@ private:
std::hash_set< Node, NodeHashFunction > d_processed;
/** terms processed */
std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
-private:
/** select op map */
std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
- /** count number of ground terms per operator (user-context dependent) */
- NodeIntMap d_op_ccount;
/** set has term */
void setHasTerm( Node n );
- /** may complete */
- std::map< TypeNode, bool > d_may_complete;
public:
TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
~TermDb(){}
@@ -152,25 +147,34 @@ public:
/** constants */
Node d_zero;
Node d_one;
- /** ground terms */
- unsigned getNumGroundTerms( Node f );
- /** count number of non-redundant ground terms per operator */
- std::map< Node, int > d_op_nonred_count;
+
/** map from operators to ground terms for that operator */
std::map< Node, std::vector< Node > > d_op_map;
+ /** map from type nodes to terms of that type */
+ std::map< TypeNode, std::vector< Node > > d_type_map;
+
+
+ /** count number of non-redundant ground terms per operator */
+ std::map< Node, int > d_op_nonred_count;
+ /**mapping from UF terms to representatives of their arguments */
+ std::map< TNode, std::vector< TNode > > d_arg_reps;
+ /** map from operators to trie */
+ std::map< Node, TermArgTrie > d_func_map_trie;
+ std::map< Node, TermArgTrie > d_func_map_eqc_trie;
/** has map */
std::map< Node, bool > d_has_map;
/** map from reps to a term in eqc in d_has_map */
std::map< Node, Node > d_term_elig_eqc;
- /** map from operators to trie */
- std::map< Node, TermArgTrie > d_func_map_trie;
- std::map< Node, TermArgTrie > d_func_map_eqc_trie;
- /**mapping from UF terms to representatives of their arguments */
- std::map< TNode, std::vector< TNode > > d_arg_reps;
- /** map from type nodes to terms of that type */
- std::map< TypeNode, std::vector< Node > > d_type_map;
+
+public:
+ /** ground terms for operator */
+ unsigned getNumGroundTerms( Node f );
+ /** get ground term for operator */
+ Node getGroundTerm( Node f, unsigned i );
/** add a term to the database */
void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
+ /** presolve (called once per user check-sat) */
+ void presolve();
/** reset (calculate which terms are active) */
void reset( Theory::Effort effort );
/** get operator*/
@@ -200,8 +204,7 @@ public:
Node getEligibleTermInEqc( TNode r );
/** is inst closure */
bool isInstClosure( Node r );
- /** may complete */
- bool mayComplete( TypeNode tn );
+
//for model basis
private:
//map from types to model basis terms
@@ -220,12 +223,14 @@ public:
//get model basis term for op
Node getModelBasisOpTerm( Node op );
//get model basis
- Node getModelBasis( Node f, Node n );
+ Node getModelBasis( Node q, Node n );
//get model basis body
- Node getModelBasisBody( Node f );
+ Node getModelBasisBody( Node q );
//for inst constant
private:
+ /** map from universal quantifiers to the list of variables */
+ std::map< Node, std::vector< Node > > d_vars;
/** map from universal quantifiers to the list of instantiation constants */
std::map< Node, std::vector< Node > > d_inst_constants;
/** map from universal quantifiers to their inst constant body */
@@ -235,30 +240,32 @@ private:
/** instantiation constants to universal quantifiers */
std::map< Node, Node > d_inst_constants_map;
/** make instantiation constants for */
- void makeInstantiationConstantsFor( Node f );
+ void makeInstantiationConstantsFor( Node q );
public:
- /** get the i^th instantiation constant of f */
- Node getInstantiationConstant( Node f, int i ) const;
- /** get number of instantiation constants for f */
- int getNumInstantiationConstants( Node f ) const;
- /** get the ce body f[e/x] */
- Node getInstConstantBody( Node f );
+ /** get the i^th instantiation constant of q */
+ Node getInstantiationConstant( Node q, int i ) const;
+ /** get number of instantiation constants for q */
+ int getNumInstantiationConstants( Node q ) const;
+ /** get the ce body q[e/x] */
+ Node getInstConstantBody( Node q );
/** get counterexample literal (for cbqi) */
- Node getCounterexampleLiteral( Node f );
- /** returns node n with bound vars of f replaced by instantiation constants of f
+ Node getCounterexampleLiteral( Node q );
+ /** returns node n with bound vars of q replaced by instantiation constants of q
node n : is the future pattern
- node f : is the quantifier containing which bind the variable
+ node q : is the quantifier containing which bind the variable
return a pattern where the variable are replaced by variable for
instantiation.
*/
- Node getInstConstantNode( Node n, Node f );
+ Node getInstConstantNode( Node n, Node q );
+ /** get substituted node */
+ Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
static Node getInstConstAttr( Node n );
static bool hasInstConstAttr( Node n );
//for bound variables
public:
//get bound variables in n
- static void getBoundVars( Node n, std::vector< Node >& bvs);
+ static void getBoundVars( Node n, std::vector< Node >& bvs );
//for skolem
@@ -285,24 +292,16 @@ private:
std::vector< TypeEnumerator > d_typ_enum;
// closed enumerable type cache
std::map< TypeNode, bool > d_typ_closed_enum;
+ /** may complete */
+ std::map< TypeNode, bool > d_may_complete;
public:
//get nth term for type
Node getEnumerateTerm( TypeNode tn, unsigned index );
//does this type have an enumerator that produces constants that are handled by ground theory solvers
bool isClosedEnumerableType( TypeNode tn );
-
-//miscellaneous
-public:
- /** map from universal quantifiers to the list of variables */
- std::map< Node, std::vector< Node > > d_vars;
- /** free variable for instantiation constant type */
- std::map< TypeNode, Node > d_free_vars;
-public:
- /** get free variable for instantiation constant */
- Node getFreeVariableForInstConstant( Node n );
- /** get free variable for type */
- Node getFreeVariableForType( TypeNode tn );
-
+ // may complete
+ bool mayComplete( TypeNode tn );
+
//for triggers
private:
/** helper function for compute var contains */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback