/******************************************************************************

 * Top contributors (to current version):

 *   Abdalrhman Mohamed, Andrew Reynolds, Aina Niemetz

 *

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 *

 * Implementation for reconstruct.

 */

#include "theory/quantifiers/sygus/sygus_reconstruct.h"

#include "expr/node_algorithm.h"

#include "smt/command.h"

#include "theory/datatypes/sygus_datatype_utils.h"

#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {

namespace theory {

namespace quantifiers {

{

                                           TypeNode stn,

                                           int8_t& reconstructed,

                                           uint64_t enumLimit)

{

  // this method may get called multiple times with the same object. We need to

  // reset the state to avoid conflicts

  /** a set of builtin terms to reconstruct satisfied for each sygus datatype */

  // add the main obligation to the set of obligations

  // paramaters stn and sol constitute the main obligation to satisfy

  // We need to add the main obligation to the crd in case it cannot be broken

  // down by matching. By doing so, we can solve the obligation using

  // enumeration and crd (if it is in the grammar)

  // the set of unique (up to rewriting) patterns/shapes in the grammar used by

  // matching

  // algorithm

  {

    // enumeration phase

    // a temporary set of new terms to reconstruct cached for processing in the

    // match phase

    {

      // enumerate a new term

      {

      }

      // if enumerated term does not contain free variables, then its

      // corresponding obligation can be solved immediately

      {

        // check if the enumerated term solves an obligation

        {

          // if not, create an "artifical" obligation whose solution would be

          // the enumerated term

        }

        // mark the obligation as solved

        // Since we added the term to the candidate rewrite database, there is

        // no point in adding it to the pool too

      }

      // if there are no matches (all calls to notify return true)...

      {

        // then, this is a new term and we should add it to pool

        {

          {

            // try to match builtin term `t` with the enumerated term sz

            // cache the new obligations for processing in the match phase

            {

                  tempPair.second.cbegin(), tempPair.second.cend());

            }

          }

        }

      }

    }

    // match phase

    {

      // a temporary set of new terms to reconstruct cached for later processing

      {

        {

          {

            {

              // try to match each newly generated and cached term with patterns

              // in pool

              // cache the new terms for later processing

              {

                                                 tempPair.second.cend());

              }

            }

          }

        }

      }

    }

    // remove reconstructed terms from termsToRecons

  }

  {

  }

  // if the main obligation is solved, return the solution

  {

    // The algorithm mostly works with rewritten terms and may not notice that

    // the original terms contain variables eliminated by the rewriter. For

    // example, rewrite((ite true 0 z)) = 0. In such cases, we replace those

    // variables with ground values.

  }

  // we ran out of elements, return null

}

{

  // substitutions generated by match. Note that we might have already seen (and

  // even solved) obligations corresponsing to those substitutions

  // the builtin terms corresponding to sygus variables in the grammar are bound

  // variables. However, we want the `match` method to treat them as ground

  // terms. So, we add redundant substitutions

  // try to match the builtin term with the pattern sz

  {

    // the bound variables z generated by the enumerators are reused across

    // enumerated terms, so we need to replace them with our own skolems

    // remove redundant substitutions

    {

    }

    // for each match

    {

      RConsObligation* newOb;

      // did we come across an equivalent obligation before?

      {

        // if so, use the original obligation

        // while `match.second` is equivalent to `rep`, it may be easier to

        // reconstruct than `rep`. For example:

        //

        // Grammar: S -> p | q | (not S) | (and S S) | (or S S)

        // rep = (= p q)

        // match.second = (or (and p q) (and (not p) (not q)))

        //

        // In this case, `match.second` is easy to reconstruct by matching

        // because it only uses operators that are already in the grammar.

        // `rep`, on the other hand, cannot be reconstructed by matching and

        // can only be solved by enumeration (currently).

        //

        // At this point, we do not know which one is easier to reconstruct by

        // matching, so we add `match.second` to the set of equivalent builtin

        // terms in `repOb` and match against both terms.

        {

        }

      }

      else

      {

        // otherwise, create a new obligation of the corresponding sygus type

        // if the match is a constant and the grammar allows random constants

        {

          // then immediately solve the obligation

        }

        else

        {

          // otherwise, add this match to the list of obligations

        }

      }

    }

    // replace original free vars in sz with new ones

    {

    }

    // sz is solved if it has no sub-obligations or if all of them are solved

    {

      {

      }

    }

    {

      // As it traverses sz, substitute populates its input cache with TNodes

      // that are not preserved by this module and maybe destroyed after the

      // method call. To avoid referencing those unsafe TNodes throughout this

      // module, we pass a iterators of d_sol instead.

    }

    else

    {

      // add sz as a possible solution to ob

    }

  }

}

{

  // return if ob is already solved

  {

  }

  // First, mark ob as solved

  {

    // for each partial solution/parent of the now solved obligation `curr`

    {

      // remove `curr` and (possibly) other solved obligations from its list

      // of children

      {

      }

      // if the partial solution does not have any more children...

      {

        // then it is completely solved and can be used as a solution of its

        // corresponding obligation

        // pass iterators of d_sol to avoid populating it with unsafe TNodes

        // proceed only if parent obligation is not already solved

        {

          // repeat the same process for the parent obligation

        }

      }

      else

      {

        // if it does have remaining children, add it to the watch list of one

        // of them (picked arbitrarily)

      }

    }

  }

}

{

  // Cache the sygus variables introduced by the problem (which we treat as

  // ground terms when calling the `match` method) as opposed to the sygus

  // variables introduced by the enumerators (which we treat as bound

  // variables).

  {

  }

  // find the non-terminals of the grammar

  // initialize the enumerators and candidate rewrite databases. Notice here

  // that we treat the sygus variables introduced by the problem as bound

  // variables (needed for making sure that obligations are equal). This is fine

  // as we will never add variables that were introduced by the enumerators to

  // the database.

  {

  }

    TypeBuiltinSetMap& termsToRecons)

{

  {

    {

      {

      }

      else

      {

      }

    }

  }

{

  // get the set of bound variables in n

  // generate a ground value for each one of those variables

  {

  }

  // substitute the variables with ground values

}

                              Node n,

                              std::vector<Node>& vars,

                              std::vector<Node>& subs)

{

  {

    // We consider sygus variables as ground terms. So, if they are not equal to

    // their substitution, then s is not matchable with n and we try the next

    // term s. Example: If s = (+ z x) and n = (+ z y), then s is not matchable

    // with n and we return true

    {

    }

  }

  // Note: false here means that we finally found an s that is matchable with n,

  // so we should not add n to the pool

}

{

    const std::unordered_map<TypeNode, std::vector<Node>>& pool) const

{

  {

    {

    }

  }

}  // namespace quantifiers

}  // namespace theory