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 ) ){
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();
}
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;
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() ){
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 );
}
void debugPrint( const char* c );
/** is complete? */
bool isComplete();
- /** make complete */
- void makeComplete( Node f, QuantifiersEngine* qe );
/** make representative */
void makeRepresentative( QuantifiersEngine* qe );
/** empty */
}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;
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
}
}
}
+ }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 );
}
}
}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 ){
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 ) );
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;
}
}
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();
//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 );
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;
//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;
//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;
RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
- d_true = NodeManager::currentNM()->mkConst( true );
d_needsSort = false;
}
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() );
}
}else{
return it->second;
}
-}
\ No newline at end of file
+}
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 */
}
}
-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 ) );
}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 ) {
//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 );
+ }
}
}
}
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 ) ){
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 ){
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{
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 ];
}
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 ){
}
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++;
}
}
}
-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);
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);
}
-/** 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{
}
}
-/** 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{
}
}
-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
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++ ){
}
}
-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 ) {
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() ){
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(){}
/** 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*/
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
//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 */
/** 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
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 */
QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
d_te( te ),
d_lemmas_produced_c(u),
-d_skolemized(u){
+d_skolemized(u),
+d_presolve(u, true){
d_eq_query = new EqualityQueryQuantifiersEngine( this );
d_term_db = new quantifiers::TermDb( c, u, this );
d_tr_trie = new inst::TriggerTrie;
for( unsigned i=0; i<d_modules.size(); i++ ){
d_modules[i]->presolve();
}
+ d_term_db->presolve();
+ d_presolve = false;
+ //clear presolve cache
+ for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
+ addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
+ }
+ d_presolve_cache.clear();
+ d_presolve_cache_wq.clear();
+ d_presolve_cache_wic.clear();
}
void QuantifiersEngine::check( Theory::Effort e ){
}
}
}
+
+ d_hasAddedLemma = false;
+
Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl;
if( needsCheck ){
Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
}
//reset relevant information
- d_hasAddedLemma = false;
//flush previous lemmas (for instance, if was interupted), or other lemmas to process
flushLemmas();
Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
}else{
Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl;
- d_hasAddedLemma = false;
}
//SAT case
if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
}
void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
- std::set< Node > added;
- getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
- //maybe have triggered instantiations if we are doing eager instantiation
- if( options::eagerInstQuant() ){
- flushLemmas();
- }
- //added contains also the Node that just have been asserted in this branch
- if( d_quant_rel ){
- for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
- if( !withinQuant ){
- d_quant_rel->setRelevance( i->getOperator(), 0 );
+ if( d_presolve ){
+ d_presolve_cache.push_back( n );
+ d_presolve_cache_wq.push_back( withinQuant );
+ d_presolve_cache_wic.push_back( withinInstClosure );
+ }else{
+ std::set< Node > added;
+ getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
+ //maybe have triggered instantiations if we are doing eager instantiation
+ if( options::eagerInstQuant() ){
+ flushLemmas();
+ }
+ //added contains also the Node that just have been asserted in this branch
+ if( d_quant_rel ){
+ for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
+ if( !withinQuant ){
+ d_quant_rel->setRelevance( i->getOperator(), 0 );
+ }
}
}
}
}
-Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
+Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms ){
Node body;
//process partial instantiation if necessary
- if( d_term_db->d_vars[f].size()!=vars.size() ){
- body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ if( d_term_db->d_vars[q].size()!=vars.size() ){
+ body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
std::vector< Node > uninst_vars;
//doing a partial instantiation, must add quantifier for all uninstantiated variables
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- if( std::find( vars.begin(), vars.end(), f[0][i] )==vars.end() ){
- uninst_vars.push_back( f[0][i] );
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ if( std::find( vars.begin(), vars.end(), q[0][i] )==vars.end() ){
+ uninst_vars.push_back( q[0][i] );
}
}
Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
- Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
+ Trace("partial-inst") << "Partial instantiation : " << q << std::endl;
Trace("partial-inst") << " : " << body << std::endl;
}else{
if( options::cbqi() ){
- body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
}else{
//do optimized version
- Node icb = d_term_db->getInstConstantBody( f );
+ Node icb = d_term_db->getInstConstantBody( q );
body = getSubstitute( icb, terms );
if( Debug.isOn("check-inst") ){
- Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+ Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
if( body!=body2 ){
Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
}
return body;
}
-Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
+Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m ){
std::vector< Node > vars;
std::vector< Node > terms;
- computeTermVector( f, m, vars, terms );
- return getInstantiation( f, vars, terms );
+ computeTermVector( q, m, vars, terms );
+ return getInstantiation( q, vars, terms );
}
-Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
- d_term_db->makeInstantiationConstantsFor( f );
- return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
+Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms ) {
+ return getInstantiation( q, d_term_db->d_vars[q], terms );
}
/*
d_phase_req_waiting[lit] = req;
}
-bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){
+bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){
std::vector< Node > terms;
- m.getTerms( this, f, terms );
- return addInstantiation( f, terms, mkRep, modEq, modInst, doVts );
+ m.getTerms( this, q, terms );
+ return addInstantiation( q, terms, mkRep, modEq, modInst, doVts );
}
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) {
+bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) {
// For resource-limiting (also does a time check).
getOutputChannel().safePoint(options::quantifierStep());
- Assert( terms.size()==f[0].getNumChildren() );
- Trace("inst-add-debug") << "For quantified formula " << f << ", add instantiation: " << std::endl;
+ Assert( terms.size()==q[0].getNumChildren() );
+ Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
for( unsigned i=0; i<terms.size(); i++ ){
- Trace("inst-add-debug") << " " << f[0][i] << " -> " << terms[i] << std::endl;
+ Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i] << std::endl;
//make it representative, this is helpful for recognizing duplication
if( mkRep ){
//pick the best possible representative for instantiation, based on past use and simplicity of term
- terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
+ terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
}
}
//check based on instantiation level
if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
for( unsigned i=0; i<terms.size(); i++ ){
- if( !d_term_db->isTermEligibleForInstantiation( terms[i], f, true ) ){
+ if( !d_term_db->isTermEligibleForInstantiation( terms[i], q, true ) ){
return false;
}
}
if( options::instNoEntail() ){
std::map< TNode, TNode > subs;
for( unsigned i=0; i<terms.size(); i++ ){
- subs[f[0][i]] = terms[i];
+ subs[q[0][i]] = terms[i];
}
- if( d_term_db->isEntailed( f[1], subs, false, true ) ){
+ if( d_term_db->isEntailed( q[1], subs, false, true ) ){
Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
return false;
}
if( options::incrementalSolving() ){
Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
inst::CDInstMatchTrie* imt;
- std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f );
+ std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
if( it!=d_c_inst_match_trie.end() ){
imt = it->second;
}else{
imt = new CDInstMatchTrie( getUserContext() );
- d_c_inst_match_trie[f] = imt;
+ d_c_inst_match_trie[q] = imt;
}
- alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst );
+ alreadyExists = !imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst );
}else{
Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
- alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst );
+ alreadyExists = !d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst );
}
if( alreadyExists ){
Trace("inst-add-debug") << " -> Already exists." << std::endl;
//add the instantiation
Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
- bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms, doVts );
+ bool addedInst = addInstantiation( q, d_term_db->d_vars[q], terms, doVts );
//report the result
if( addedInst ){
Trace("inst-add-debug") << " -> Success." << std::endl;
/** inst round counters */
int d_ierCounter;
int d_ierCounter_lc;
+ /** has presolve been called */
+ context::CDO< bool > d_presolve;
+ /** presolve cache */
+ std::vector< Node > d_presolve_cache;
+ std::vector< bool > d_presolve_cache_wq;
+ std::vector< bool > d_presolve_cache_wic;
private:
KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
public:
void flushLemmas();
public:
/** get instantiation */
- Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
+ Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms );
/** get instantiation */
- Node getInstantiation( Node f, InstMatch& m );
+ Node getInstantiation( Node q, InstMatch& m );
/** get instantiation */
- Node getInstantiation( Node f, std::vector< Node >& terms );
+ Node getInstantiation( Node q, std::vector< Node >& terms );
/** do substitution */
Node getSubstitute( Node n, std::vector< Node >& terms );
/** add lemma lem */
/** add require phase */
void addRequirePhase( Node lit, bool req );
/** do instantiation specified by m */
- bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+ bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
/** add instantiation */
- bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+ bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
/** split on node n */
bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
/** add split equality */
}
void TheoryEngine::eqNotifyNewClass(TNode t){
- d_quantEngine->addTermToDatabase( t );
+ if( d_logicInfo.isQuantified() ){
+ d_quantEngine->addTermToDatabase( t );
+ }
}
void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
quant-fun-proc-unmacro.smt2 \
quant-fun-proc-unfd.smt2 \
bug654-dd.smt2 \
- bug-fmf-fun-skolem.smt2
+ bug-fmf-fun-skolem.smt2 \
+ bug674.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
--- /dev/null
+; COMMAND-LINE: --quant-ind --incremental --rewrite-divk
+(set-logic ALL_SUPPORTED)
+(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2))))
+(define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil))))
+; EXPECT: unsat
+(push 1)
+(assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0)))))))
+(check-sat)
+(pop 1)
+
+(assert (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0))))
+
+; EXPECT: unsat
+(push 1)
+(assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst)) (= (rev (app $l1$0 $l2$0)) (app (rev $l2$0) (rev $l1$0))))))))
+(check-sat)
+(pop 1)
+
+(assert (forall (($l1$0 Lst) ($l2$0 Lst)) (= (rev (app $l1$0 $l2$0)) (app (rev $l2$0) (rev $l1$0)))))
+
+; EXPECT: unsat
+(push 1)
+(assert (not (=> true (and (forall (($l1$0 Lst)) (= (rev (rev $l1$0)) $l1$0))))))
+(check-sat)
+(pop 1)
+
+
projects / cvc5.git / commitdiff