diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 9158734e4..c3ddfacff 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -474,6 +474,7 @@ void QuantEPR::registerAssertion( Node assertion ) { void QuantEPR::finishInit() { Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl; for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){ + Assert( d_epr_axiom.find( it->first )==d_epr_axiom.end() ); Trace("quant-epr-debug") << "process " << it->first << std::endl; if( d_non_epr.find( it->first )!=d_non_epr.end() ){ Trace("quant-epr-debug") << "...non-epr" << std::endl; @@ -497,3 +498,28 @@ bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) { return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end(); } +void QuantEPR::addEPRConstant( TypeNode tn, Node k ) { + Assert( isEPR( tn ) ); + Assert( d_epr_axiom.find( tn )==d_epr_axiom.end() ); + if( !isEPRConstant( tn, k ) ){ + d_consts[tn].push_back( k ); + } +} + +Node QuantEPR::mkEPRAxiom( TypeNode tn ) { + Assert( isEPR( tn ) ); + std::map< TypeNode, Node >::iterator ita = d_epr_axiom.find( tn ); + if( ita==d_epr_axiom.end() ){ + std::vector< Node > disj; + Node x = NodeManager::currentNM()->mkBoundVar( tn ); + for( unsigned i=0; i<d_consts[tn].size(); i++ ){ + disj.push_back( NodeManager::currentNM()->mkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) ); + } + Assert( !disj.empty() ); + d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) ); + return d_epr_axiom[tn]; + }else{ + return ita->second; + } +} + |