From ada1fc44c9b5b8746a2e1e4046032282149768b5 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 12 Nov 2015 11:00:44 +0100 Subject: [PATCH] Minor fixes and improvements to purify quant, relational triggers. --- .../quantifiers/inst_match_generator.cpp | 16 ++++++------- .../quantifiers/quantifiers_rewriter.cpp | 20 ++++++++-------- src/theory/quantifiers/quantifiers_rewriter.h | 4 ++-- src/theory/quantifiers/relevant_domain.cpp | 11 +++++---- src/theory/quantifiers/relevant_domain.h | 4 ++-- src/theory/quantifiers/term_database.cpp | 23 +++++++++++++++++++ src/theory/quantifiers/term_database.h | 5 ++++ src/theory/quantifiers/trigger.cpp | 5 ++-- 8 files changed, 58 insertions(+), 30 deletions(-) diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 2b4854305..f4e8861dc 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -238,21 +238,19 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern; Node t_match; if( pol ){ - if (pat.getKind()==GT) { - Node r = NodeManager::currentNM()->mkConst( Rational(-1) ); - t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + if( pat.getKind()==GT ){ + t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermDatabase()->d_one); }else{ t_match = t; } }else{ - if(pat.getKind()==EQUAL) { - Node r = NodeManager::currentNM()->mkConst( Rational(1) ); - t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + if( pat.getKind()==EQUAL ){ + Assert( t.getType().isReal() ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); }else if( pat.getKind()==IFF ){ - t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) ); + t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) ); }else if( pat.getKind()==GEQ ){ - Node r = NodeManager::currentNM()->mkConst( Rational(1) ); - t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); }else if( pat.getKind()==GT ){ t_match = t; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 8f055473d..1e2ac21a0 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -83,10 +83,10 @@ bool QuantifiersRewriter::isCube( Node n ){ } } -int QuantifiersRewriter::getPurifyId( Node n, std::vector< Node >& args ){ +int QuantifiersRewriter::getPurifyId( Node n ){ if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ return 1; - }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::containsTerms( n, args ) ){ + }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::hasBoundVarAttr( n ) ){ return 0; }else{ return -1; @@ -768,7 +768,7 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){ return body; } -bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) { +bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) { if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ return false; }else{ @@ -776,7 +776,7 @@ bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& a std::map< Node, std::vector< int > >::iterator it = var_parent.find( v ); if( it!=var_parent.end() ){ Assert( !it->second.empty() ); - int id = getPurifyId( s, args ); + int id = getPurifyId( s ); return it->second.size()==1 && it->second[0]==id; } } @@ -790,7 +790,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto for( unsigned i=0; i<2; i++ ){ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] ); if( ita!=args.end() ){ - if( isVariableElim( lit[i], lit[1-i], args, var_parent ) ){ + if( isVariableElim( lit[i], lit[1-i], var_parent ) ){ Trace("var-elim-quant") << "Variable eliminate based on equality : " << lit[i] << " -> " << lit[1-i] << std::endl; vars.push_back( lit[i] ); subs.push_back( lit[1-i] ); @@ -809,7 +809,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto Node veq_c; Node val; int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL ); - if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, args, var_parent ) ){ + if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){ Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl; vars.push_back( itm->first ); subs.push_back( val ); @@ -1689,17 +1689,17 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, return it->second; }else{ Node ret = body; - if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::containsTerms( ret, args ) ){ + if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::hasBoundVarAttr( ret ) ){ std::vector< Node > children; bool childrenChanged = false; - int id = getPurifyId( body, args ); + int id = getPurifyId( body ); for( unsigned i=0; i& args ); + static int getPurifyId( Node n ); private: static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); @@ -41,7 +41,7 @@ private: static Node computeClause( Node n ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); static bool isConditionalVariableElim( Node n, int pol=0 ); - static bool isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ); + static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ); static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs, std::map< Node, std::vector< int > >& var_parent ); static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 8e3304b6a..49bbe5680 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -56,12 +56,12 @@ RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() { } } -void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) { +void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) { std::map< Node, Node > rterms; for( unsigned i=0; igetRepresentative( d_terms[i] ); + r = qe->getEqualityQuery()->getRepresentative( d_terms[i] ); } if( rterms.find( r )==rterms.end() ){ rterms[r] = d_terms[i]; @@ -132,7 +132,7 @@ void RelevantDomain::compute(){ RDomain * r = it2->second; RDomain * rp = r->getParent(); if( r==rp ){ - r->removeRedundantTerms( d_model ); + r->removeRedundantTerms( d_qe ); for( unsigned i=0; id_terms.size(); i++ ){ Trace("rel-dom") << r->d_terms[i] << " "; } @@ -190,7 +190,7 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { }else if( varCount==1 ){ int oCh = varCh==0 ? 1 : 0; bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] ); - Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << std::endl; + Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << ", pol = " << pol << ", hasPol = " << hasPol << ", kind = " << n.getKind() << std::endl; //the negative occurrence adds the term to the domain if( !hasPol || !pol ){ rds[varCh]->addTerm( n[oCh], ng ); @@ -202,7 +202,6 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { rds[varCh]->addTerm( QuantArith::offset( n[oCh], i==0 ? 1 : -1 ), ng ); } }else if( n.getKind()==GEQ ){ - Node nt = QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ); rds[varCh]->addTerm( QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ), ng ); } } @@ -228,6 +227,7 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { } } +/* Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) { RDomain * rf = getRDomain( f, i ); Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl; @@ -248,3 +248,4 @@ Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) { return r; } } +*/ diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 7d1c60f80..25c821e10 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -37,7 +37,7 @@ private: void merge( RDomain * r ); void addTerm( Node t, bool nonGround = false ); RDomain * getParent(); - void removeRedundantTerms( FirstOrderModel * fm ); + void removeRedundantTerms( QuantifiersEngine * qe ); bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } }; std::map< Node, std::map< int, RDomain * > > d_rel_doms; @@ -56,7 +56,7 @@ public: void compute(); RDomain * getRDomain( Node n, int i ); - Node getRelevantTerm( Node f, int i, Node r ); + //Node getRelevantTerm( Node f, int i, Node r ); };/* class RelevantDomain */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e41af5e2d..79e62a6cd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -699,6 +699,29 @@ bool TermDb::hasInstConstAttr( Node n ) { return !getInstConstAttr(n).isNull(); } +Node TermDb::getBoundVarAttr( Node n ) { + if (!n.hasAttribute(BoundVarAttribute()) ){ + Node bv; + if( n.getKind()==BOUND_VARIABLE ){ + bv = n; + }else{ + for( unsigned i=0; i >::const_iterator it = d_inst_constants.find( q ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f809aa5b8..8ce6aeaf0 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -59,6 +59,9 @@ typedef expr::Attribute< NoMatchAttributeId, struct InstConstantAttributeId {}; typedef expr::Attribute InstConstantAttribute; +struct BoundVarAttributeId {}; +typedef expr::Attribute BoundVarAttribute; + struct InstLevelAttributeId {}; typedef expr::Attribute InstLevelAttribute; @@ -262,6 +265,8 @@ public: static Node getInstConstAttr( Node n ); static bool hasInstConstAttr( Node n ); + static Node getBoundVarAttr( Node n ); + static bool hasBoundVarAttr( Node n ); //for skolem diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 1f332e909..fdfa77b02 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -250,9 +250,10 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ Node rtr; bool do_negate = hasPol && pol; + bool is_arith = n[0].getType().isReal(); for( unsigned i=0; i<2; i++) { if( n[1-i].getKind()==INST_CONSTANT ){ - if( isUsableTrigger(n[i], f) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ){ + if( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) && ( !do_negate || is_arith ) ){ rtr = n; break; } @@ -263,7 +264,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { } } } - if( n[0].getType().isInteger() ){ + if( is_arith ){ //try to rearrange? std::map< Node, Node > m; if( QuantArith::getMonomialSumLit(n, m) ){ -- 2.30.2