From c6d93155e795e5cce35f75d27766ae6c3d6c205c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 16 Jun 2014 18:05:36 +0200 Subject: [PATCH] More proof support for CASC : include skolemization --- src/theory/quantifiers/term_database.h | 4 +- src/theory/quantifiers/theory_quantifiers.cpp | 13 +------ src/theory/quantifiers/theory_quantifiers.h | 2 - src/theory/quantifiers_engine.cpp | 39 +++++++++++++++++-- src/theory/quantifiers_engine.h | 4 +- 5 files changed, 42 insertions(+), 20 deletions(-) diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e82fcd00d..383278f82 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -199,11 +199,11 @@ public: static void getBoundVars( Node n, std::vector< Node >& bvs); //for skolem private: - /** map from universal quantifiers to the list of skolem constants */ - std::map< Node, std::vector< Node > > d_skolem_constants; /** map from universal quantifiers to their skolemized body */ std::map< Node, Node > d_skolem_body; public: + /** map from universal quantifiers to the list of skolem constants */ + std::map< Node, std::vector< Node > > d_skolem_constants; /** make the skolemized body f[e/x] */ static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs, std::vector< Node >& sk ); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 8335a084a..5d016fd06 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -150,23 +150,14 @@ Node TheoryQuantifiers::getNextDecisionRequest(){ void TheoryQuantifiers::assertUniversal( Node n ){ Assert( n.getKind()==FORALL ); if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ - getQuantifiersEngine()->registerQuantifier( n ); - getQuantifiersEngine()->assertNode( n ); + getQuantifiersEngine()->assertQuantifier( n, true ); } } void TheoryQuantifiers::assertExistential( Node n ){ Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){ - if( d_skolemized.find( n )==d_skolemized.end() ){ - Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] ); - NodeBuilder<> nb(kind::OR); - nb << n[0] << body.notNode(); - Node lem = nb; - Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl; - d_out->lemma( lem, false, true ); - d_skolemized[n] = true; - } + getQuantifiersEngine()->assertQuantifier( n[0], false ); } } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 84b65cacd..5ce2e1a11 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -41,8 +41,6 @@ class InstantiationEngine; class TheoryQuantifiers : public Theory { private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - /** quantifiers that have been skolemized */ - std::map< Node, bool > d_skolemized; /** number of instantiations */ int d_numInstantiations; int d_baseDecLevel; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 66d8f9326..083137148 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -265,10 +265,31 @@ void QuantifiersEngine::registerPattern( std::vector & pattern) { } } -void QuantifiersEngine::assertNode( Node f ){ - d_model->assertQuantifier( f ); - for( int i=0; i<(int)d_modules.size(); i++ ){ - d_modules[i]->assertNode( f ); +void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ + if( !pol ){ + //do skolemization + if( d_skolemized.find( f )==d_skolemized.end() ){ + Node body = d_term_db->getSkolemizedBody( f ); + NodeBuilder<> nb(kind::OR); + nb << f << body.notNode(); + Node lem = nb; + if( Trace.isOn("quantifiers-sk") ){ + Node slem = Rewriter::rewrite( lem ); + Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + } + getOutputChannel().lemma( lem, false, true ); + d_skolemized[f] = true; + } + } + //assert to modules TODO : handle !pol + if( pol ){ + //register the quantifier + registerQuantifier( f ); + //assert it to each module + d_model->assertQuantifier( f ); + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->assertNode( f ); + } } } @@ -629,6 +650,16 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ } void QuantifiersEngine::printInstantiations( std::ostream& out ) { + for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ + out << "Skolem constants of " << it->first << " : " << std::endl; + out << " ( "; + for( unsigned i=0; id_skolem_constants[it->first].size(); i++ ){ + if( i>0 ){ out << ", "; } + out << d_term_db->d_skolem_constants[it->first][i]; + } + out << " )" << std::endl; + out << std::endl; + } if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ out << "Instantiations of " << it->first << " : " << std::endl; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 999a716ba..19f8c55fb 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -125,6 +125,8 @@ private: /** list of all instantiations produced for each quantifier */ std::map< Node, inst::InstMatchTrie > d_inst_match_trie; std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; + /** quantifiers that have been skolemized */ + std::map< Node, bool > d_skolemized; /** term database */ quantifiers::TermDb* d_term_db; /** all triggers will be stored in this trie */ @@ -179,7 +181,7 @@ public: /** register quantifier */ void registerPattern( std::vector & pattern); /** assert universal quantifier */ - void assertNode( Node f ); + void assertQuantifier( Node q, bool pol ); /** propagate */ void propagate( Theory::Effort level ); /** get next decision request */ -- 2.30.2