From babbe0e30d769b5f68cb3f36820fbb5e176de7c5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 6 Feb 2020 17:30:53 -0600 Subject: [PATCH] Generalize containsQuantifiers to hasClosure (#3722) --- src/expr/node_algorithm.cpp | 37 +++++++++++++++++++ src/expr/node_algorithm.h | 9 +++++ src/smt/smt_engine.cpp | 3 +- .../quantifiers/cegqi/ceg_instantiator.cpp | 3 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 30 +++------------ src/theory/quantifiers/quantifiers_rewriter.h | 1 - 7 files changed, 55 insertions(+), 30 deletions(-) diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 9721845f7..9619e69d1 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -229,6 +229,43 @@ bool hasFreeVar(TNode n) return getFreeVariables(n, fvs, false); } +struct HasClosureTag +{ +}; +struct HasClosureComputedTag +{ +}; +/** Attribute true for expressions with closures in them */ +typedef expr::Attribute HasClosureAttr; +typedef expr::Attribute HasClosureComputedAttr; + +bool hasClosure(Node n) +{ + if (!n.getAttribute(HasClosureComputedAttr())) + { + bool hasC = false; + if (n.isClosure()) + { + hasC = true; + } + else + { + for (auto i = n.begin(); i != n.end() && !hasC; ++i) + { + hasC = hasClosure(*i); + } + } + if (!hasC && n.hasOperator()) + { + hasC = hasClosure(n.getOperator()); + } + n.setAttribute(HasClosureAttr(), hasC); + n.setAttribute(HasClosureComputedAttr(), true); + return hasC; + } + return n.getAttribute(HasClosureAttr()); +} + bool getFreeVariables(TNode n, std::unordered_set& fvs, bool computeFv) diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 03d77a2f9..929e1c5ef 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -69,6 +69,15 @@ bool hasBoundVar(TNode n); */ bool hasFreeVar(TNode n); +/** + * Returns true iff the node n contains a closure, that is, a node + * whose kind is FORALL, EXISTS, CHOICE, LAMBDA, or any other closure currently + * supported. + * @param n The node under investigation + * @return true iff this node contains a closure. + */ +bool hasClosure(Node n); + /** * Get the free variables in n, that is, the subterms of n of kind * BOUND_VARIABLE that are not bound in n, adds these to fvs. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 83d8fb612..6a63a991f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -95,7 +95,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/sygus_abduct.h" #include "theory/quantifiers/sygus/synth_engine.h" @@ -4828,7 +4827,7 @@ void SmtEngine::checkModel(bool hardFailure) { // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas if( hardFailure && !n.isConst() && n.getKind() != kind::LAMBDA ){ Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl; - AlwaysAssert(quantifiers::QuantifiersRewriter::containsQuantifiers(n)); + AlwaysAssert(expr::hasClosure(n)); Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n << endl; continue; } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 1d4a23af1..4f3ce4327 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1386,7 +1386,8 @@ void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& ter void CegInstantiator::presolve( Node q ) { //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing //only if no nested quantifiers - if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){ + if (!expr::hasClosure(q[1])) + { std::vector< Node > ps_vars; std::map< Node, std::vector< Node > > teq; for( unsigned i=0; igetTermUtil()->d_inst_constants[q].size() == inst_terms.size()); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d5bee4916..74d8ac3a6 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1546,7 +1546,8 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< uns if( itv!=visited[tindex].end() ){ return itv->second; } - if( containsQuantifiers( n ) ){ + if (expr::hasClosure(n)) + { Node ret = n; if (topLevel && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL @@ -2168,35 +2169,13 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { return rn; } -struct ContainsQuantAttributeId {}; -typedef expr::Attribute ContainsQuantAttribute; - -// check if the given node contains a universal quantifier -bool QuantifiersRewriter::containsQuantifiers( Node n ){ - if( n.hasAttribute(ContainsQuantAttribute()) ){ - return n.getAttribute(ContainsQuantAttribute())==1; - }else if( n.getKind() == kind::FORALL ){ - return true; - }else{ - bool cq = false; - for( unsigned i = 0; i < n.getNumChildren(); ++i ){ - if( containsQuantifiers( n[i] ) ){ - cq = true; - break; - } - } - ContainsQuantAttribute cqa; - n.setAttribute(cqa, cq ? 1 : 0); - return cq; - } -} bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { if( n.getKind()==FORALL ){ return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] ); }else if( n.getKind()==NOT ){ return n[0].getKind()!=NOT && isPrenexNormalForm( n[0] ); }else{ - return !containsQuantifiers( n ); + return !expr::hasClosure(n); } } @@ -2246,7 +2225,8 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v }else{ //check if it contains a quantifier as a subterm //if so, we will write this node - if( containsQuantifiers( n ) ){ + if (expr::hasClosure(n)) + { if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){ if( options::preSkolemQuantAgg() ){ Node nn; diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 56eac761e..e8f069882 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -205,7 +205,6 @@ private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector& fvs); public: static Node rewriteRewriteRule( Node r ); - static bool containsQuantifiers( Node n ); static bool isPrenexNormalForm( Node n ); /** preprocess * -- 2.30.2