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

4 files changed, 63 insertions, 6 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 8f07384d6..ab74fbc79 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1017,11 +1017,20 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-inv-templ=MODE"
   type       = "CVC4::theory::quantifiers::SygusInvTemplMode"
-  default    = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE"
+  default    = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
   handler    = "stringToSygusInvTemplMode"
   includes   = ["options/quantifiers_modes.h"]
   read_only  = true
-  help       = "template mode for sygus invariant synthesis"
+  help       = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
+
+[[option]]
+  name       = "sygusInvTemplWhenSyntax"
+  category   = "regular"
+  long       = "sygus-inv-templ-when-sg"
+  type       = "bool"
+  default    = "false"
+  read_only  = false
+  help       = "use invariant templates (with solution reconstruction) for syntax guided problems"
 
 [[option]]
   name       = "sygusInvAutoUnfold"
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index d59f1f370..a951ec867 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -154,7 +155,26 @@ void CegConjectureSingleInv::initialize( Node q ) {
       //check if it is single invocation
       if (!d_sip->isPurelySingleInvocation())
       {
-        if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
+        SygusInvTemplMode tmode = options::sygusInvTemplMode();
+        if (tmode != SYGUS_INV_TEMPL_MODE_NONE)
+        {
+          // currently only works for single predicate synthesis
+          if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate())
+          {
+            tmode = SYGUS_INV_TEMPL_MODE_NONE;
+          }
+          else if (!options::sygusInvTemplWhenSyntax())
+          {
+            // only use invariant templates if no syntactic restrictions
+            if (CegGrammarConstructor::hasSyntaxRestrictions(q))
+            {
+              tmode = SYGUS_INV_TEMPL_MODE_NONE;
+            }
+          }
+        }
+
+        if (tmode != SYGUS_INV_TEMPL_MODE_NONE)
+        {
           //if we are doing invariant templates, then construct the template
           Trace("cegqi-si") << "- Do transition inference..." << std::endl;
           d_ti[q].process( qq );
@@ -234,12 +254,15 @@ void CegConjectureSingleInv::initialize( Node q ) {
                 }
               }
             }
+            Trace("cegqi-inv") << "Make the template... " << tmode << " "
+                               << templ << std::endl;
             if( templ.isNull() ){
-              if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+              if (tmode == SYGUS_INV_TEMPL_MODE_PRE)
+              {
                 //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] );
                 templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] );
               }else{
-                Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST );
+                Assert(tmode == SYGUS_INV_TEMPL_MODE_POST);
                 //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) );
                 templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] );
               }
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;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 4e486f88f..d8a77848b 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -83,7 +83,13 @@ public:
   *   fun is for naming
   */
   static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
-private:
+  /**
+   * Returns true iff there are syntax restrictions on the
+   * functions-to-synthesize of sygus conjecture q.
+   */
+  static bool hasSyntaxRestrictions(Node q);
+
+ private:
   /** reference to quantifier engine */
   QuantifiersEngine * d_qe;
   /** parent conjecture