Enable post-condition strenghtening by default for non-syntax restricted invariant synthesis (#1703)

1 files changed, 19 insertions, 0 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 1ca774c5d..08b0dc837 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -36,6 +36,25 @@ CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
 {
 }
 
+bool CegGrammarConstructor::hasSyntaxRestrictions(Node q)
+{
+  Assert(q.getKind() == FORALL);
+  for (const Node& f : q[0])
+  {
+    Node gv = f.getAttribute(SygusSynthGrammarAttribute());
+    if (!gv.isNull())
+    {
+      TypeNode tn = gv.getType();
+      if (tn.isDatatype()
+          && static_cast<DatatypeType>(tn.toType()).getDatatype().isSygus())
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
 void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts ){
   std::unordered_map<TNode, bool, TNodeHashFunction> visited;
   std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;