summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node_algorithm.cpp37
-rw-r--r--src/expr/node_algorithm.h9
-rw-r--r--src/smt/smt_engine.cpp3
-rw-r--r--src/theory/quantifiers/cegqi/ceg_instantiator.cpp3
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp2
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp30
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h1
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<HasClosureTag, bool> HasClosureAttr;
+typedef expr::Attribute<HasClosureComputedTag, bool> 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<Node, NodeHashFunction>& 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
@@ -70,6 +70,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.
* @param n The node under investigation
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; i<q[0].getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 0ec87f239..4f670bef4 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -490,7 +490,7 @@ Node InstStrategyCegqi::doNestedQENode(
Trace("cbqi-nqe") << " " << ceq << std::endl;
Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl;
//should not contain quantifiers
- Assert(!QuantifiersRewriter::containsQuantifiers(d_nested_qe[ceq]));
+ Assert(!expr::hasClosure(d_nested_qe[ceq]));
}
Assert(d_quantEngine->getTermUtil()->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<ContainsQuantAttributeId, uint64_t> 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<TNode>& fvs);
public:
static Node rewriteRewriteRule( Node r );
- static bool containsQuantifiers( Node n );
static bool isPrenexNormalForm( Node n );
/** preprocess
*
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback