sygusComp2018: update policies for solution reconstruction (#2109)

7 files changed, 87 insertions, 63 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 3bb0fc51a..bf973bd97 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -102,7 +102,7 @@ void CegConjecture::assign( Node q ) {
   // we now finalize the single invocation module, based on the syntax restrictions
   if (d_qe->getQuantAttributes()->isSygus(q))
   {
-    d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() );
+    d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted());
   }
 
   Assert( d_candidates.empty() );
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index f568fcf3e..9a6fad52a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -17,6 +17,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -49,7 +50,6 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe,
       d_cosi(new CegqiOutputSingleInv(this)),
       d_cinst(NULL),
       d_c_inst_match_trie(NULL),
-      d_has_ites(true),
       d_single_invocation(false) {
   //  third and fourth arguments set to (false,false) until we have solution
   //  reconstruction for delta and infinity
@@ -290,8 +290,9 @@ void CegConjectureSingleInv::initialize( Node q ) {
   }
 }
 
-void CegConjectureSingleInv::finishInit( bool syntaxRestricted, bool hasItes ) {
-  d_has_ites = hasItes;
+void CegConjectureSingleInv::finishInit(bool syntaxRestricted)
+{
+  Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl;
   // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled
   if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && d_single_invocation && syntaxRestricted ){
     d_single_invocation = false;
@@ -458,13 +459,6 @@ struct sortSiInstanceIndices {
 
 
 Node CegConjectureSingleInv::postProcessSolution( Node n ){
-  ////remove boolean ITE (not allowed for sygus comp 2015)
-  //if( n.getKind()==ITE && n.getType().isBoolean() ){
-  //  Node n1 = postProcessSolution( n[1] );
-  //  Node n2 = postProcessSolution( n[2] );
-  //  return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ),
-  //                                               NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) );
-  //}else{
   bool childChanged = false;
   Kind k = n.getKind();
   if( n.getKind()==INTS_DIVISION_TOTAL ){
@@ -488,7 +482,6 @@ Node CegConjectureSingleInv::postProcessSolution( Node n ){
   }else{
     return n;
   }
-  //}
 }
 
 
@@ -573,15 +566,34 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
 
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
-  if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus ){
+  if (options::cegqiSingleInvReconstruct() != CEGQI_SI_RCONS_MODE_NONE
+      && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus)
+  {
     d_sol->preregisterConjecture( d_orig_conjecture );
-    d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed );
+    int enumLimit = -1;
+    if (options::cegqiSingleInvReconstruct() == CEGQI_SI_RCONS_MODE_TRY)
+    {
+      enumLimit = 0;
+    }
+    else if (options::cegqiSingleInvReconstruct()
+             == CEGQI_SI_RCONS_MODE_ALL_LIMIT)
+    {
+      enumLimit = options::cegqiSingleInvReconstructLimit();
+    }
+    d_sygus_solution =
+        d_sol->reconstructSolution(s, stn, reconstructed, enumLimit);
     if( reconstructed==1 ){
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
     }
   }else{
     Trace("csi-sol") << "Post-process solution..." << std::endl;
     Node prev = d_solution;
+    if (options::minSynthSol())
+    {
+      d_solution =
+          d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(
+              d_solution);
+    }
     d_solution = postProcessSolution( d_solution );
     if( prev!=d_solution ){
       Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl;
@@ -631,11 +643,6 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
 }
 
 bool CegConjectureSingleInv::needsCheck() {
-  if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_ALL_ABORT ){
-    if( !d_has_ites ){
-      return d_inst.empty();
-    }
-  }
   return true;
 }
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index b6fda18ed..b368a0689 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -146,9 +146,6 @@ class CegConjectureSingleInv {
   Node d_orig_solution;
   Node d_solution;
   Node d_sygus_solution;
-  // whether the grammar for our solution allows ITEs, this tells us when reconstruction is infeasible
-  bool d_has_ites;
-
  public:
   // lemmas produced
   std::vector<Node> d_lemmas_produced;
@@ -191,10 +188,13 @@ class CegConjectureSingleInv {
   void getInitialSingleInvLemma( std::vector< Node >& lems );
   // initialize this class for synthesis conjecture q
   void initialize( Node q );
-  // finish initialize, sets up final decisions about whether to use single invocation techniques
-  //  syntaxRestricted is whether the syntax for solutions for the initialized conjecture is restricted
-  //  hasItes is whether the syntax for solutions for the initialized conjecture allows ITEs
-  void finishInit( bool syntaxRestricted, bool hasItes );
+  /** finish initialize
+   *
+   * This method sets up final decisions about whether to use single invocation
+   * techniques. The argument syntaxRestricted is whether the syntax for
+   * solutions for the initialized conjecture is restricted.
+   */
+  void finishInit(bool syntaxRestricted);
   //check
   bool check( std::vector< Node >& lems );
   //get solution
@@ -202,8 +202,6 @@ class CegConjectureSingleInv {
   //reconstruct to syntax
   Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed,
                             bool rconsSygus = true );
-  // has ites
-  bool hasITEs() { return d_has_ites; }
   // is single invocation
   bool isSingleInvocation() const { return !d_single_inv.isNull(); }
   //needs check
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 861d71946..44835cc26 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -639,7 +639,11 @@ void CegConjectureSingleInvSol::preregisterConjecture( Node q ) {
   registerEquivalentTerms( n );
 }
 
-Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int& reconstructed ) {
+Node CegConjectureSingleInvSol::reconstructSolution(Node sol,
+                                                    TypeNode stn,
+                                                    int& reconstructed,
+                                                    int enumLimit)
+{
   Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
   int status;
   d_root_id = collectReconstructNodes( sol, stn, status );
@@ -649,23 +653,34 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
     Assert( !ret.isNull() );
     reconstructed = 1;
     return ret;
-  }else{
-    //Trace("csi-debug-sol") << "Induced solution template is : " << d_templ_solution << std::endl;
-    if( Trace.isOn("csi-rcons") ){
-      for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){
-        TypeNode tn = it->first;
-        Assert( tn.isDatatype() );
-        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-        Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() << " : " << std::endl;
-        for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-          if( d_reconstruct.find( it2->second )==d_reconstruct.end() ){
-            Trace("csi-rcons") << "  " << it2->first << std::endl;
-          }
+  }
+  if (Trace.isOn("csi-rcons"))
+  {
+    for (std::map<TypeNode, std::map<Node, int> >::iterator it =
+             d_rcons_to_id.begin();
+         it != d_rcons_to_id.end();
+         ++it)
+    {
+      TypeNode tn = it->first;
+      Assert(tn.isDatatype());
+      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName()
+                         << " : " << std::endl;
+      for (std::map<Node, int>::iterator it2 = it->second.begin();
+           it2 != it->second.end();
+           ++it2)
+      {
+        if (d_reconstruct.find(it2->second) == d_reconstruct.end())
+        {
+          Trace("csi-rcons") << "  " << it2->first << std::endl;
         }
-        Assert( !it->second.empty() );
       }
+      Assert(!it->second.empty());
     }
-    unsigned index = 0;
+  }
+  if (enumLimit != 0)
+  {
+    int index = 0;
     std::map< TypeNode, bool > active;
     for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){
       active[it->first] = true;
@@ -712,13 +727,16 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
       if( index%100==0 ){
         Trace("csi-rcons-stats") << "Tried " << index << " for each type."  << std::endl;
       }
-    }while( !active.empty() );
-
-    // we ran out of elements, return null
-    reconstructed = -1;
-    Warning() << CommandFailure("Cannot get synth function: reconstruction to syntax failed.");
-    return Node::null(); // return sol;
+    } while (!active.empty() && (enumLimit < 0 || index < enumLimit));
   }
+
+  // we ran out of elements, return null
+  reconstructed = -1;
+  Warning() << CommandFailure(
+      "Cannot get synth function: reconstruction to syntax failed.");
+  // could return sol here, however, we choose to fail by returning null, since
+  // it indicates a failure.
+  return Node::null();
 }
 
 int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, int& status ) {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
index 0e5347f2e..8d18611cf 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -68,8 +68,16 @@ private:
    * matches the grammar corresponding to sygus datatype stn.
    * The value reconstructed is set to 1 if we successfully return a node,
    * otherwise it is set to -1.
+   *
+   * This method quickly tries to match sol to the grammar induced by stn. If
+   * this fails, we use enumerative techniques to try to repair the solution.
+   * The number of iterations for this enumeration is bounded by the argument
+   * enumLimit if it is positive, and unbounded otherwise.
    */
-  Node reconstructSolution(Node sol, TypeNode stn, int& reconstructed);
+  Node reconstructSolution(Node sol,
+                           TypeNode stn,
+                           int& reconstructed,
+                           int enumLimit);
   /** preregister conjecture
    *
    * q : the synthesis conjecture this class is for.
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 5bbd71fbe..efffa046f 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -33,7 +33,7 @@ namespace quantifiers {
 
 CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
                                              CegConjecture* p)
-    : d_qe(qe), d_parent(p), d_is_syntax_restricted(false), d_has_ite(true)
+    : d_qe(qe), d_parent(p), d_is_syntax_restricted(false)
 {
 }
 
@@ -198,6 +198,7 @@ Node CegGrammarConstructor::process(Node q,
   std::vector<Node> qchildren;
   Node qbody_subs = q[1];
   std::map<Node, Node> synth_fun_vars;
+  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
   {
     Node sf = q[0][i];
@@ -245,16 +246,10 @@ Node CegGrammarConstructor::process(Node q,
         Trace("cegqi-debug") << "  body is now : " << qbody_subs << std::endl;
       }
     }
-    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
-    // check grammar restrictions
-    if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
-      if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
-        d_has_ite = false;
-      }
-    }
-    Assert( tn.isDatatype() );
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    Assert( dt.isSygus() );
+    tds->registerSygusType(tn);
+    Assert(tn.isDatatype());
+    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    Assert(dt.isSygus());
     if( !dt.getSygusAllowAll() ){
       d_is_syntax_restricted = true;
     }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index fcb4b3348..c99c431ea 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -62,8 +62,6 @@ public:
               const std::vector<Node>& ebvl);
  /** is the syntax restricted? */
  bool isSyntaxRestricted() { return d_is_syntax_restricted; }
- /** does the syntax allow ITE expressions? */
- bool hasSyntaxITE() { return d_has_ite; }
  /** make the default sygus datatype type corresponding to builtin type range
  *   bvl is the set of free variables to include in the grammar
  *   fun is for naming