diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 26 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 10 |
2 files changed, 35 insertions, 1 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; + } +} + diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 049644ffb..d8e57b1ca 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -177,6 +177,8 @@ private: void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ); /** non-epr */ std::map< TypeNode, bool > d_non_epr; + /** axioms for epr */ + std::map< TypeNode, Node > d_epr_axiom; public: QuantEPR(){} virtual ~QuantEPR(){} @@ -191,9 +193,15 @@ public: /** finish init */ void finishInit(); /** is EPR */ - bool isEPR( TypeNode tn ) { return d_non_epr.find( tn )!=d_non_epr.end() ? false : true; } + bool isEPR( TypeNode tn ) const { return d_non_epr.find( tn )==d_non_epr.end(); } /** is EPR constant */ bool isEPRConstant( TypeNode tn, Node k ); + /** add EPR constant */ + void addEPRConstant( TypeNode tn, Node k ); + /** get EPR axiom */ + Node mkEPRAxiom( TypeNode tn ); + /** has EPR axiom */ + bool hasEPRAxiom( TypeNode tn ) const { return d_epr_axiom.find( tn )!=d_epr_axiom.end(); } }; } |