From beb73911f71daa6711390264221e7b4de7dc8c6c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 14 Sep 2016 10:42:39 -0500 Subject: [PATCH] Lemma cache in theory sep. Minor optimization for sets. Minor improvements to EPR --- src/theory/quantifiers/quant_util.cpp | 26 +++++++++++++++++++++++++ src/theory/quantifiers/quant_util.h | 10 +++++++++- src/theory/quantifiers_engine.cpp | 12 ++++++++++++ src/theory/quantifiers_engine.h | 2 ++ src/theory/sep/theory_sep.cpp | 18 ++++++++++------- src/theory/sep/theory_sep.h | 2 ++ src/theory/sets/theory_sets_private.cpp | 23 +++++++++++++--------- 7 files changed, 76 insertions(+), 17 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; imkNode( 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(); } }; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 5b50526c4..e48c6eafe 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1246,6 +1246,18 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } +bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) { + if( d_qepr ){ + Assert( !options::incrementalSolving() ); + if( d_qepr->isEPR( tn ) && !d_qepr->hasEPRAxiom( tn ) ){ + Node lem = d_qepr->mkEPRAxiom( tn ); + Trace("quant-epr") << "EPR lemma for " << tn << " : " << lem << std::endl; + getOutputChannel().lemma( lem ); + } + } + return false; +} + void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bcc33327e..25542e49e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -333,6 +333,8 @@ public: bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true ); + /** add EPR axiom */ + bool addEPRAxiom( TypeNode tn ); /** mark relevant quantified formula, this will indicate it should be checked before the others */ void markRelevant( Node q ); /** has added lemma */ diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index e96badfd3..7ee5a1b73 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -36,6 +36,7 @@ namespace sep { TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_SEP, c, u, out, valuation, logicInfo), + d_lemmas_produced_c(u), d_notify(*this), d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true), d_conflict(c, false), @@ -1025,14 +1026,14 @@ void TheorySep::initializeBounds() { d_type_ref_card_id[e] = r; //must include this constant back into EPR handling if( qepr && qepr->isEPR( tn ) ){ - qepr->d_consts[tn].push_back( e ); + qepr->addEPRConstant( tn, e ); } } //EPR must include nil ref if( qepr && qepr->isEPR( tn ) ){ Node nr = getNilRef( tn ); if( !qepr->isEPRConstant( tn, nr ) ){ - qepr->d_consts[tn].push_back( nr ); + qepr->addEPRConstant( tn, nr ); } } } @@ -1530,9 +1531,9 @@ void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ) if( pb[0][1]!=p[0][1] ){ conc.push_back( pb[0][1].eqNode( p[0][1] ).negate() ); } - if( pb[1]!=p[1] ){ - conc.push_back( pb[1].eqNode( p[1] ).negate() ); - } + //if( pb[1]!=p[1] ){ + // conc.push_back( pb[1].eqNode( p[1] ).negate() ); + //} Node n_conc = conc.empty() ? d_false : ( conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::OR, conc ) ); sendLemma( exp, n_conc, "PTO_NEG_PROP" ); } @@ -1631,8 +1632,11 @@ void TheorySep::doPendingFacts() { } int index = d_pending_lem[i]; Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, d_pending_exp[index], d_pending[index] ); - d_out->lemma( lem ); - Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl; + if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ + d_lemmas_produced_c.insert( lem ); + d_out->lemma( lem ); + Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl; + } } } d_pending_exp.clear(); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 1ca78801b..982fc3c70 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -44,6 +44,8 @@ class TheorySep : public Theory { ///////////////////////////////////////////////////////////////////////////// private: + /** all lemmas sent */ + NodeSet d_lemmas_produced_c; /** True node for predicates = true */ Node d_true; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index dbe94ff4b..ec6bb7fcd 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1249,15 +1249,20 @@ Node TheorySetsPrivate::getLemma() { Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet()); TypeNode elementType = n[0].getType().getSetElementType(); - Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType); - Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]); - - if(n[0].getKind() == kind::EMPTYSET) { - lemma = OR(n, l2); - } else if(n[1].getKind() == kind::EMPTYSET) { - lemma = OR(n, l1); - } else { - lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); + // { x } != { y } => x != y + if( n[0].getKind()==kind::SINGLETON && n[1].getKind()==kind::SINGLETON ){ + lemma = OR(n, NodeManager::currentNM()->mkNode( elementType.isBoolean() ? kind::IFF : kind::EQUAL, n[0][0], n[1][0] ).negate() ); + }else{ + Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType); + Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]); + + if(n[0].getKind() == kind::EMPTYSET) { + lemma = OR(n, l2); + } else if(n[1].getKind() == kind::EMPTYSET) { + lemma = OR(n, l1); + } else { + lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); + } } } -- 2.30.2