Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/single_inv_partition.cpp	Lines:	270	304	88.8 %
Date:	2021-11-06	Branches:	509	1032	49.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, 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.
 * ****************************************************************************
 *
 * Utility for processing single invocation synthesis conjectures.
 */
#include "theory/quantifiers/single_inv_partition.h"

#include <sstream>

#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"

using namespace cvc5;
using namespace cvc5::kind;
using namespace std;

namespace cvc5 {
namespace theory {
namespace quantifiers {

bool SingleInvocationPartition::init(Node n)
{
  // first, get types of arguments for functions
  std::vector<TypeNode> typs;
  std::map<Node, bool> visited;
  std::vector<Node> funcs;
  if (inferArgTypes(n, typs, visited))
  {
    return init(funcs, typs, n, false);
  }
  else
  {
    Trace("si-prt") << "Could not infer argument types." << std::endl;
    return false;
  }
}

Node SingleInvocationPartition::getFirstOrderVariableForFunction(Node f) const
{
  std::map<Node, Node>::const_iterator it = d_func_fo_var.find(f);
  if (it != d_func_fo_var.end())
  {
    return it->second;
  }
  return Node::null();
}

Node SingleInvocationPartition::getFunctionForFirstOrderVariable(Node v) const
{
  std::map<Node, Node>::const_iterator it = d_fo_var_to_func.find(v);
  if (it != d_fo_var_to_func.end())
  {
    return it->second;
  }
  return Node::null();
}

Node SingleInvocationPartition::getFunctionInvocationFor(Node f) const
{
  std::map<Node, Node>::const_iterator it = d_func_inv.find(f);
  if (it != d_func_inv.end())
  {
    return it->second;
  }
  return Node::null();
}

void SingleInvocationPartition::getFunctionVariables(
    std::vector<Node>& fvars) const
{
  fvars.insert(fvars.end(), d_func_vars.begin(), d_func_vars.end());
}

void SingleInvocationPartition::getFunctions(std::vector<Node>& fs) const
{
  fs.insert(fs.end(), d_all_funcs.begin(), d_all_funcs.end());
}

void SingleInvocationPartition::getSingleInvocationVariables(
    std::vector<Node>& sivars) const
{
  sivars.insert(sivars.end(), d_si_vars.begin(), d_si_vars.end());
}

void SingleInvocationPartition::getAllVariables(std::vector<Node>& vars) const
{
  vars.insert(vars.end(), d_all_vars.begin(), d_all_vars.end());
}

// gets the argument type list for the first APPLY_UF we see
bool SingleInvocationPartition::inferArgTypes(Node n,
                                              std::vector<TypeNode>& typs,
                                              std::map<Node, bool>& visited)
{
  if (visited.find(n) == visited.end())
  {
    visited[n] = true;
    if (n.getKind() != FORALL)
    {
      if (n.getKind() == APPLY_UF)
      {
        for (unsigned i = 0; i < n.getNumChildren(); i++)
        {
          typs.push_back(n[i].getType());
        }
        return true;
      }
      else
      {
        for (unsigned i = 0; i < n.getNumChildren(); i++)
        {
          if (inferArgTypes(n[i], typs, visited))
          {
            return true;
          }
        }
      }
    }
  }
  return false;
}

bool SingleInvocationPartition::init(std::vector<Node>& funcs, Node n)
{
  Trace("si-prt") << "Initialize with " << funcs.size() << " input functions ("
                  << funcs << ")..." << std::endl;
  std::vector<TypeNode> typs;
  if (!funcs.empty())
  {
    TypeNode tn0 = funcs[0].getType();
    if (tn0.isFunction())
    {
      for (unsigned i = 0, nargs = tn0.getNumChildren() - 1; i < nargs; i++)
      {
        typs.push_back(tn0[i]);
      }
    }
    for (unsigned i = 1, size = funcs.size(); i < size; i++)
    {
      TypeNode tni = funcs[i].getType();
      if (tni.getNumChildren() != tn0.getNumChildren())
      {
        // can't anti-skolemize functions of different sort
        Trace("si-prt") << "...type mismatch" << std::endl;
        return false;
      }
      else if (tni.isFunction())
      {
        for (unsigned j = 0, nargs = tni.getNumChildren() - 1; j < nargs; j++)
        {
          if (tni[j] != typs[j])
          {
            Trace("si-prt") << "...argument type mismatch" << std::endl;
            return false;
          }
        }
      }
    }
  }
  Trace("si-prt") << "#types = " << typs.size() << std::endl;
  return init(funcs, typs, n, true);
}

bool SingleInvocationPartition::init(std::vector<Node>& funcs,
                                     std::vector<TypeNode>& typs,
                                     Node n,
                                     bool has_funcs)
{
  Assert(d_arg_types.empty());
  Assert(d_input_funcs.empty());
  Assert(d_si_vars.empty());
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  d_has_input_funcs = has_funcs;
  d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end());
  d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end());
  Trace("si-prt") << "Initialize..." << std::endl;
  for (unsigned j = 0; j < d_arg_types.size(); j++)
  {
    std::stringstream ss;
    ss << "s_" << j;
    Node si_v = nm->mkBoundVar(ss.str(), d_arg_types[j]);
    d_si_vars.push_back(si_v);
  }
  Assert(d_si_vars.size() == d_arg_types.size());
  for (const Node& inf : d_input_funcs)
  {
    Node sk = sm->mkDummySkolem("_sik", inf.getType());
    d_input_func_sks.push_back(sk);
  }
  Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl;
  Trace("si-prt") << "Get conjuncts..." << std::endl;
  std::vector<Node> conj;
  if (collectConjuncts(n, true, conj))
  {
    Trace("si-prt") << "...success." << std::endl;
    for (unsigned i = 0; i < conj.size(); i++)
    {
      std::vector<Node> si_terms;
      std::vector<Node> si_subs;
      Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl;
      // do DER on conjunct
      // Must avoid eliminating the first-order input functions in the
      // getQuantSimplify step below. We use a substitution to avoid this.
      // This makes it so that e.g. the synthesis conjecture:
      //   exists f. f!=0 ^ P
      // is not rewritten to exists f. (f=0 => false) ^ P and subsquently
      // rewritten to exists f. false ^ P by the elimination f -> 0.
      Node cr = conj[i].substitute(d_input_funcs.begin(),
                                   d_input_funcs.end(),
                                   d_input_func_sks.begin(),
                                   d_input_func_sks.end());
      cr = TermUtil::getQuantSimplify(cr);
      cr = cr.substitute(d_input_func_sks.begin(),
                         d_input_func_sks.end(),
                         d_input_funcs.begin(),
                         d_input_funcs.end());
      if (cr != conj[i])
      {
        Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
      }
      std::map<Node, bool> visited;
      // functions to arguments
      std::vector<Node> args;
      Subs sb;
      bool singleInvocation = true;
      bool ngroundSingleInvocation = false;
      if (processConjunct(cr, visited, args, sb))
      {
        for (size_t j = 0, vsize = sb.d_vars.size(); j < vsize; j++)
        {
          Node s = sb.d_subs[j];
          si_terms.push_back(s);
          Node op = s.hasOperator() ? s.getOperator() : s;
          Assert(d_func_fo_var.find(op) != d_func_fo_var.end());
          si_subs.push_back(d_func_fo_var[op]);
        }
        std::map<Node, Node> subs_map;
        std::map<Node, Node> subs_map_rev;
        // normalize the invocations
        if (!sb.empty())
        {
          cr = sb.apply(cr);
        }
        std::vector<Node> children;
        children.push_back(cr);
        sb.clear();
        Trace("si-prt") << "...single invocation, with arguments: "
                        << std::endl;
        for (unsigned j = 0; j < args.size(); j++)
        {
          Trace("si-prt") << args[j] << " ";
          if (args[j].getKind() == BOUND_VARIABLE && !sb.contains(args[j]))
          {
            sb.add(args[j], d_si_vars[j]);
          }
          else
          {
            children.push_back(d_si_vars[j].eqNode(args[j]).negate());
          }
        }
        Trace("si-prt") << std::endl;
        cr = nm->mkOr(children);
        cr = sb.apply(cr);
        Trace("si-prt-debug") << "...normalized invocations to " << cr
                              << std::endl;
        // now must check if it has other bound variables
        std::unordered_set<Node> fvs;
        expr::getFreeVariables(cr, fvs);
        // bound variables must be contained in the single invocation variables
        for (const Node& bv : fvs)
        {
          if (std::find(d_si_vars.begin(), d_si_vars.end(), bv)
              == d_si_vars.end())
          {
            // getFreeVariables also collects functions in the rare case that
            // we are synthesizing a function with 0 arguments, take this into
            // account here.
            if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bv)
                == d_input_funcs.end())
            {
              Trace("si-prt")
                  << "...not ground single invocation." << std::endl;
              ngroundSingleInvocation = true;
              singleInvocation = false;
            }
          }
        }
        if (singleInvocation)
        {
          Trace("si-prt") << "...ground single invocation" << std::endl;
        }
      }
      else
      {
        Trace("si-prt") << "...not single invocation." << std::endl;
        singleInvocation = false;
        // rename bound variables with maximal overlap with si_vars
        std::unordered_set<Node> fvs;
        expr::getFreeVariables(cr, fvs);
        std::vector<Node> termsNs;
        std::vector<Node> subsNs;
        for (const Node& v : fvs)
        {
          TypeNode tn = v.getType();
          Trace("si-prt-debug")
              << "Fit bound var: " << v << " with si." << std::endl;
          for (unsigned k = 0; k < d_si_vars.size(); k++)
          {
            if (tn == d_arg_types[k])
            {
              if (std::find(subsNs.begin(), subsNs.end(), d_si_vars[k])
                  == subsNs.end())
              {
                termsNs.push_back(v);
                subsNs.push_back(d_si_vars[k]);
                Trace("si-prt-debug") << "  ...use " << d_si_vars[k]
                                      << std::endl;
                break;
              }
            }
          }
        }
        Assert(termsNs.size() == subsNs.size());
        cr = cr.substitute(
            termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end());
      }
      cr = Rewriter::rewrite(cr);
      Trace("si-prt") << ".....got si=" << singleInvocation
                      << ", result : " << cr << std::endl;
      d_conjuncts[2].push_back(cr);
      std::unordered_set<Node> fvs;
      expr::getFreeVariables(cr, fvs);
      d_all_vars.insert(fvs.begin(), fvs.end());
      if (singleInvocation)
      {
        // replace with single invocation formulation
        Assert(si_terms.size() == si_subs.size());
        cr = cr.substitute(
            si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end());
        cr = Rewriter::rewrite(cr);
        Trace("si-prt") << ".....si version=" << cr << std::endl;
        d_conjuncts[0].push_back(cr);
      }
      else
      {
        d_conjuncts[1].push_back(cr);
        if (ngroundSingleInvocation)
        {
          d_conjuncts[3].push_back(cr);
        }
      }
    }
  }
  else
  {
    Trace("si-prt") << "...failed." << std::endl;
    return false;
  }
  return true;
}

bool SingleInvocationPartition::collectConjuncts(Node n,
                                                 bool pol,
                                                 std::vector<Node>& conj)
{
  if ((!pol && n.getKind() == OR) || (pol && n.getKind() == AND))
  {
    for (unsigned i = 0; i < n.getNumChildren(); i++)
    {
      if (!collectConjuncts(n[i], pol, conj))
      {
        return false;
      }
    }
  }
  else if (n.getKind() == NOT)
  {
    return collectConjuncts(n[0], !pol, conj);
  }
  else if (n.getKind() == FORALL)
  {
    return false;
  }
  else
  {
    if (!pol)
    {
      n = TermUtil::simpleNegate(n);
    }
    Trace("si-prt") << "Conjunct : " << n << std::endl;
    conj.push_back(n);
  }
  return true;
}

bool SingleInvocationPartition::processConjunct(Node n,
                                                std::map<Node, bool>& visited,
                                                std::vector<Node>& args,
                                                Subs& sb)
{
  std::map<Node, bool>::iterator it = visited.find(n);
  if (it != visited.end())
  {
    return true;
  }
  else
  {
    bool ret = true;
    for (unsigned i = 0; i < n.getNumChildren(); i++)
    {
      if (!processConjunct(n[i], visited, args, sb))
      {
        ret = false;
      }
    }
    if (ret)
    {
      Node f;
      bool success = false;
      if (d_has_input_funcs)
      {
        f = n.hasOperator() ? n.getOperator() : n;
        if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f)
            != d_input_funcs.end())
        {
          // If n is an application of a function-to-synthesize f, or is
          // itself a function-to-synthesize, then n must be fully applied.
          // This catches cases where n is a function-to-synthesize that occurs
          // in a higher-order context.
          // If the type of n is functional, then it is not fully applied.
          if (n.getType().isFunction())
          {
            ret = false;
            success = false;
          }
          else
          {
            success = true;
          }
        }
      }
      else
      {
        if (n.getKind() == kind::APPLY_UF)
        {
          f = n.getOperator();
          success = true;
        }
      }
      if (success)
      {
        Trace("si-prt-debug") << "Process " << n << std::endl;
        if (!sb.contains(n))
        {
          // check if it matches the type requirement
          if (isAntiSkolemizableType(f))
          {
            if (args.empty())
            {
              // record arguments
              for (unsigned i = 0; i < n.getNumChildren(); i++)
              {
                args.push_back(n[i]);
              }
            }
            else
            {
              // arguments must be the same as those already recorded
              for (unsigned i = 0; i < n.getNumChildren(); i++)
              {
                if (args[i] != n[i])
                {
                  Trace("si-prt-debug") << "...bad invocation : " << n
                                        << " at arg " << i << "." << std::endl;
                  ret = false;
                  break;
                }
              }
            }
            if (ret)
            {
              sb.add(n, d_func_inv[f]);
            }
          }
          else
          {
            Trace("si-prt-debug") << "... " << f << " is a bad operator."
                                  << std::endl;
            ret = false;
          }
        }
      }
    }
    visited[n] = ret;
    return ret;
  }
}

bool SingleInvocationPartition::isAntiSkolemizableType(Node f)
{
  std::map<Node, bool>::iterator it = d_funcs.find(f);
  if (it != d_funcs.end())
  {
    return it->second;
  }
  else
  {
    TypeNode tn = f.getType();
    bool ret = false;
    if (((tn.isFunction() && tn.getNumChildren() == d_arg_types.size() + 1)
         || (d_arg_types.empty() && tn.getNumChildren() == 0)))
    {
      ret = true;
      std::vector<Node> children;
      children.push_back(f);
      // TODO: permutations of arguments
      for (unsigned i = 0; i < d_arg_types.size(); i++)
      {
        children.push_back(d_si_vars[i]);
        if (tn[i] != d_arg_types[i])
        {
          ret = false;
          break;
        }
      }
      if (ret)
      {
        Node t;
        if (children.size() > 1)
        {
          t = NodeManager::currentNM()->mkNode(kind::APPLY_UF, children);
        }
        else
        {
          t = children[0];
        }
        d_func_inv[f] = t;
        std::stringstream ss;
        ss << "F_" << f;
        TypeNode rt;
        if (d_arg_types.empty())
        {
          rt = tn;
        }
        else
        {
          rt = tn.getRangeType();
        }
        Node v = NodeManager::currentNM()->mkBoundVar(ss.str(), rt);
        d_func_fo_var[f] = v;
        d_fo_var_to_func[v] = f;
        d_func_vars.push_back(v);
        d_all_funcs.push_back(f);
      }
    }
    d_funcs[f] = ret;
    return ret;
  }
}

Node SingleInvocationPartition::getConjunct(int index)
{
  return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst(true)
                                    : (d_conjuncts[index].size() == 1
                                           ? d_conjuncts[index][0]
                                           : NodeManager::currentNM()->mkNode(
                                                 AND, d_conjuncts[index]));
}

void SingleInvocationPartition::debugPrint(const char* c)
{
  Trace(c) << "Single invocation variables : ";
  for (unsigned i = 0; i < d_si_vars.size(); i++)
  {
    Trace(c) << d_si_vars[i] << " ";
  }
  Trace(c) << std::endl;
  Trace(c) << "Functions : " << std::endl;
  for (std::map<Node, bool>::iterator it = d_funcs.begin(); it != d_funcs.end();
       ++it)
  {
    Trace(c) << "  " << it->first << " : ";
    if (it->second)
    {
      Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first]
               << std::endl;
    }
    else
    {
      Trace(c) << "not incorporated." << std::endl;
    }
  }
  for (unsigned i = 0; i < 4; i++)
  {
    Trace(c) << (i == 0 ? "Single invocation"
                        : (i == 1 ? "Non-single invocation"
                                  : (i == 2 ? "All"
                                            : "Non-ground single invocation")));
    Trace(c) << " conjuncts: " << std::endl;
    for (unsigned j = 0; j < d_conjuncts[i].size(); j++)
    {
      Trace(c) << "  " << (j + 1) << " : " << d_conjuncts[i][j] << std::endl;
    }
  }
  Trace(c) << std::endl;
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Utility for processing single invocation synthesis conjectures.
14		*/
15		#include "theory/quantifiers/single_inv_partition.h"
16
17		#include <sstream>
18
19		#include "expr/node_algorithm.h"
20		#include "expr/skolem_manager.h"
21		#include "theory/quantifiers/term_util.h"
22		#include "theory/rewriter.h"
23
24		using namespace cvc5;
25		using namespace cvc5::kind;
26		using namespace std;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace quantifiers {
31
32		bool SingleInvocationPartition::init(Node n)
33		{
34		// first, get types of arguments for functions
35		std::vector<TypeNode> typs;
36		std::map<Node, bool> visited;
37		std::vector<Node> funcs;
38		if (inferArgTypes(n, typs, visited))
39		{
40		return init(funcs, typs, n, false);
41		}
42		else
43		{
44		Trace("si-prt") << "Could not infer argument types." << std::endl;
45		return false;
46		}
47		}
48
49	126	Node SingleInvocationPartition::getFirstOrderVariableForFunction(Node f) const
50		{
51	126	std::map<Node, Node>::const_iterator it = d_func_fo_var.find(f);
52	126	if (it != d_func_fo_var.end())
53		{
54	126	return it->second;
55		}
56		return Node::null();
57		}
58
59		Node SingleInvocationPartition::getFunctionForFirstOrderVariable(Node v) const
60		{
61		std::map<Node, Node>::const_iterator it = d_fo_var_to_func.find(v);
62		if (it != d_fo_var_to_func.end())
63		{
64		return it->second;
65		}
66		return Node::null();
67		}
68
69	126	Node SingleInvocationPartition::getFunctionInvocationFor(Node f) const
70		{
71	126	std::map<Node, Node>::const_iterator it = d_func_inv.find(f);
72	126	if (it != d_func_inv.end())
73		{
74	126	return it->second;
75		}
76		return Node::null();
77		}
78
79	140	void SingleInvocationPartition::getFunctionVariables(
80		std::vector<Node>& fvars) const
81		{
82	140	fvars.insert(fvars.end(), d_func_vars.begin(), d_func_vars.end());
83	140	}
84
85	519	void SingleInvocationPartition::getFunctions(std::vector<Node>& fs) const
86		{
87	519	fs.insert(fs.end(), d_all_funcs.begin(), d_all_funcs.end());
88	519	}
89
90	144	void SingleInvocationPartition::getSingleInvocationVariables(
91		std::vector<Node>& sivars) const
92		{
93	144	sivars.insert(sivars.end(), d_si_vars.begin(), d_si_vars.end());
94	144	}
95
96	4	void SingleInvocationPartition::getAllVariables(std::vector<Node>& vars) const
97		{
98	4	vars.insert(vars.end(), d_all_vars.begin(), d_all_vars.end());
99	4	}
100
101		// gets the argument type list for the first APPLY_UF we see
102		bool SingleInvocationPartition::inferArgTypes(Node n,
103		std::vector<TypeNode>& typs,
104		std::map<Node, bool>& visited)
105		{
106		if (visited.find(n) == visited.end())
107		{
108		visited[n] = true;
109		if (n.getKind() != FORALL)
110		{
111		if (n.getKind() == APPLY_UF)
112		{
113		for (unsigned i = 0; i < n.getNumChildren(); i++)
114		{
115		typs.push_back(n[i].getType());
116		}
117		return true;
118		}
119		else
120		{
121		for (unsigned i = 0; i < n.getNumChildren(); i++)
122		{
123		if (inferArgTypes(n[i], typs, visited))
124		{
125		return true;
126		}
127		}
128		}
129		}
130		}
131		return false;
132		}
133
134	552	bool SingleInvocationPartition::init(std::vector<Node>& funcs, Node n)
135		{
136	1104	Trace("si-prt") << "Initialize with " << funcs.size() << " input functions ("
137	552	<< funcs << ")..." << std::endl;
138	1104	std::vector<TypeNode> typs;
139	552	if (!funcs.empty())
140		{
141	1081	TypeNode tn0 = funcs[0].getType();
142	552	if (tn0.isFunction())
143		{
144	1704	for (unsigned i = 0, nargs = tn0.getNumChildren() - 1; i < nargs; i++)
145		{
146	1232	typs.push_back(tn0[i]);
147		}
148		}
149	1143	for (unsigned i = 1, size = funcs.size(); i < size; i++)
150		{
151	1205	TypeNode tni = funcs[i].getType();
152	614	if (tni.getNumChildren() != tn0.getNumChildren())
153		{
154		// can't anti-skolemize functions of different sort
155	23	Trace("si-prt") << "...type mismatch" << std::endl;
156	23	return false;
157		}
158	591	else if (tni.isFunction())
159		{
160	2039	for (unsigned j = 0, nargs = tni.getNumChildren() - 1; j < nargs; j++)
161		{
162	1520	if (tni[j] != typs[j])
163		{
164		Trace("si-prt") << "...argument type mismatch" << std::endl;
165		return false;
166		}
167		}
168		}
169		}
170		}
171	529	Trace("si-prt") << "#types = " << typs.size() << std::endl;
172	529	return init(funcs, typs, n, true);
173		}
174
175	529	bool SingleInvocationPartition::init(std::vector<Node>& funcs,
176		std::vector<TypeNode>& typs,
177		Node n,
178		bool has_funcs)
179		{
180	529	Assert(d_arg_types.empty());
181	529	Assert(d_input_funcs.empty());
182	529	Assert(d_si_vars.empty());
183	529	NodeManager* nm = NodeManager::currentNM();
184	529	SkolemManager* sm = nm->getSkolemManager();
185	529	d_has_input_funcs = has_funcs;
186	529	d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end());
187	529	d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end());
188	529	Trace("si-prt") << "Initialize..." << std::endl;
189	1749	for (unsigned j = 0; j < d_arg_types.size(); j++)
190		{
191	2440	std::stringstream ss;
192	1220	ss << "s_" << j;
193	2440	Node si_v = nm->mkBoundVar(ss.str(), d_arg_types[j]);
194	1220	d_si_vars.push_back(si_v);
195		}
196	529	Assert(d_si_vars.size() == d_arg_types.size());
197	1643	for (const Node& inf : d_input_funcs)
198		{
199	2228	Node sk = sm->mkDummySkolem("_sik", inf.getType());
200	1114	d_input_func_sks.push_back(sk);
201		}
202	529	Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl;
203	529	Trace("si-prt") << "Get conjuncts..." << std::endl;
204	1058	std::vector<Node> conj;
205	529	if (collectConjuncts(n, true, conj))
206		{
207	525	Trace("si-prt") << "...success." << std::endl;
208	2121	for (unsigned i = 0; i < conj.size(); i++)
209		{
210	3192	std::vector<Node> si_terms;
211	3192	std::vector<Node> si_subs;
212	1596	Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl;
213		// do DER on conjunct
214		// Must avoid eliminating the first-order input functions in the
215		// getQuantSimplify step below. We use a substitution to avoid this.
216		// This makes it so that e.g. the synthesis conjecture:
217		// exists f. f!=0 ^ P
218		// is not rewritten to exists f. (f=0 => false) ^ P and subsquently
219		// rewritten to exists f. false ^ P by the elimination f -> 0.
220	1596	Node cr = conj[i].substitute(d_input_funcs.begin(),
221		d_input_funcs.end(),
222		d_input_func_sks.begin(),
223	3192	d_input_func_sks.end());
224	1596	cr = TermUtil::getQuantSimplify(cr);
225	1596	cr = cr.substitute(d_input_func_sks.begin(),
226		d_input_func_sks.end(),
227		d_input_funcs.begin(),
228		d_input_funcs.end());
229	1596	if (cr != conj[i])
230		{
231	703	Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
232		}
233	3192	std::map<Node, bool> visited;
234		// functions to arguments
235	3192	std::vector<Node> args;
236	3192	Subs sb;
237	1596	bool singleInvocation = true;
238	1596	bool ngroundSingleInvocation = false;
239	1596	if (processConjunct(cr, visited, args, sb))
240		{
241	3440	for (size_t j = 0, vsize = sb.d_vars.size(); j < vsize; j++)
242		{
243	3912	Node s = sb.d_subs[j];
244	1956	si_terms.push_back(s);
245	3912	Node op = s.hasOperator() ? s.getOperator() : s;
246	1956	Assert(d_func_fo_var.find(op) != d_func_fo_var.end());
247	1956	si_subs.push_back(d_func_fo_var[op]);
248		}
249	2968	std::map<Node, Node> subs_map;
250	2968	std::map<Node, Node> subs_map_rev;
251		// normalize the invocations
252	1484	if (!sb.empty())
253		{
254	1436	cr = sb.apply(cr);
255		}
256	2968	std::vector<Node> children;
257	1484	children.push_back(cr);
258	1484	sb.clear();
259	2968	Trace("si-prt") << "...single invocation, with arguments: "
260	1484	<< std::endl;
261	4605	for (unsigned j = 0; j < args.size(); j++)
262		{
263	3121	Trace("si-prt") << args[j] << " ";
264	3121	if (args[j].getKind() == BOUND_VARIABLE && !sb.contains(args[j]))
265		{
266	1302	sb.add(args[j], d_si_vars[j]);
267		}
268		else
269		{
270	1819	children.push_back(d_si_vars[j].eqNode(args[j]).negate());
271		}
272		}
273	1484	Trace("si-prt") << std::endl;
274	1484	cr = nm->mkOr(children);
275	1484	cr = sb.apply(cr);
276	2968	Trace("si-prt-debug") << "...normalized invocations to " << cr
277	1484	<< std::endl;
278		// now must check if it has other bound variables
279	2968	std::unordered_set<Node> fvs;
280	1484	expr::getFreeVariables(cr, fvs);
281		// bound variables must be contained in the single invocation variables
282	6610	for (const Node& bv : fvs)
283		{
284	15378	if (std::find(d_si_vars.begin(), d_si_vars.end(), bv)
285	15378	== d_si_vars.end())
286		{
287		// getFreeVariables also collects functions in the rare case that
288		// we are synthesizing a function with 0 arguments, take this into
289		// account here.
290	6015	if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bv)
291	6015	== d_input_funcs.end())
292		{
293	98	Trace("si-prt")
294	49	<< "...not ground single invocation." << std::endl;
295	49	ngroundSingleInvocation = true;
296	49	singleInvocation = false;
297		}
298		}
299		}
300	1484	if (singleInvocation)
301		{
302	1454	Trace("si-prt") << "...ground single invocation" << std::endl;
303		}
304		}
305		else
306		{
307	112	Trace("si-prt") << "...not single invocation." << std::endl;
308	112	singleInvocation = false;
309		// rename bound variables with maximal overlap with si_vars
310	224	std::unordered_set<Node> fvs;
311	112	expr::getFreeVariables(cr, fvs);
312	224	std::vector<Node> termsNs;
313	224	std::vector<Node> subsNs;
314	782	for (const Node& v : fvs)
315		{
316	1340	TypeNode tn = v.getType();
317	1340	Trace("si-prt-debug")
318	670	<< "Fit bound var: " << v << " with si." << std::endl;
319	4853	for (unsigned k = 0; k < d_si_vars.size(); k++)
320		{
321	4565	if (tn == d_arg_types[k])
322		{
323	8718	if (std::find(subsNs.begin(), subsNs.end(), d_si_vars[k])
324	8718	== subsNs.end())
325		{
326	382	termsNs.push_back(v);
327	382	subsNs.push_back(d_si_vars[k]);
328	764	Trace("si-prt-debug") << " ...use " << d_si_vars[k]
329	382	<< std::endl;
330	382	break;
331		}
332		}
333		}
334		}
335	112	Assert(termsNs.size() == subsNs.size());
336	112	cr = cr.substitute(
337		termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end());
338		}
339	1596	cr = Rewriter::rewrite(cr);
340	3192	Trace("si-prt") << ".....got si=" << singleInvocation
341	1596	<< ", result : " << cr << std::endl;
342	1596	d_conjuncts[2].push_back(cr);
343	3192	std::unordered_set<Node> fvs;
344	1596	expr::getFreeVariables(cr, fvs);
345	1596	d_all_vars.insert(fvs.begin(), fvs.end());
346	1596	if (singleInvocation)
347		{
348		// replace with single invocation formulation
349	1454	Assert(si_terms.size() == si_subs.size());
350	1454	cr = cr.substitute(
351		si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end());
352	1454	cr = Rewriter::rewrite(cr);
353	1454	Trace("si-prt") << ".....si version=" << cr << std::endl;
354	1454	d_conjuncts[0].push_back(cr);
355		}
356		else
357		{
358	142	d_conjuncts[1].push_back(cr);
359	142	if (ngroundSingleInvocation)
360		{
361	30	d_conjuncts[3].push_back(cr);
362		}
363		}
364		}
365		}
366		else
367		{
368	4	Trace("si-prt") << "...failed." << std::endl;
369	4	return false;
370		}
371	525	return true;
372		}
373
374	1954	bool SingleInvocationPartition::collectConjuncts(Node n,
375		bool pol,
376		std::vector<Node>& conj)
377		{
378	1954	if ((!pol && n.getKind() == OR) \|\| (pol && n.getKind() == AND))
379		{
380	1549	for (unsigned i = 0; i < n.getNumChildren(); i++)
381		{
382	1312	if (!collectConjuncts(n[i], pol, conj))
383		{
384	4	return false;
385		}
386		}
387		}
388	1713	else if (n.getKind() == NOT)
389		{
390	113	return collectConjuncts(n[0], !pol, conj);
391		}
392	1600	else if (n.getKind() == FORALL)
393		{
394	4	return false;
395		}
396		else
397		{
398	1596	if (!pol)
399		{
400	111	n = TermUtil::simpleNegate(n);
401		}
402	1596	Trace("si-prt") << "Conjunct : " << n << std::endl;
403	1596	conj.push_back(n);
404		}
405	1833	return true;
406		}
407
408	30987	bool SingleInvocationPartition::processConjunct(Node n,
409		std::map<Node, bool>& visited,
410		std::vector<Node>& args,
411		Subs& sb)
412		{
413	30987	std::map<Node, bool>::iterator it = visited.find(n);
414	30987	if (it != visited.end())
415		{
416	12539	return true;
417		}
418		else
419		{
420	18448	bool ret = true;
421	47839	for (unsigned i = 0; i < n.getNumChildren(); i++)
422		{
423	29391	if (!processConjunct(n[i], visited, args, sb))
424		{
425	254	ret = false;
426		}
427		}
428	18448	if (ret)
429		{
430	36416	Node f;
431	18208	bool success = false;
432	18208	if (d_has_input_funcs)
433		{
434	18208	f = n.hasOperator() ? n.getOperator() : n;
435	54624	if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f)
436	54624	!= d_input_funcs.end())
437		{
438		// If n is an application of a function-to-synthesize f, or is
439		// itself a function-to-synthesize, then n must be fully applied.
440		// This catches cases where n is a function-to-synthesize that occurs
441		// in a higher-order context.
442		// If the type of n is functional, then it is not fully applied.
443	2194	if (n.getType().isFunction())
444		{
445	4	ret = false;
446	4	success = false;
447		}
448		else
449		{
450	2190	success = true;
451		}
452		}
453		}
454		else
455		{
456		if (n.getKind() == kind::APPLY_UF)
457		{
458		f = n.getOperator();
459		success = true;
460		}
461		}
462	18208	if (success)
463		{
464	2190	Trace("si-prt-debug") << "Process " << n << std::endl;
465	2190	if (!sb.contains(n))
466		{
467		// check if it matches the type requirement
468	2190	if (isAntiSkolemizableType(f))
469		{
470	2182	if (args.empty())
471		{
472		// record arguments
473	5089	for (unsigned i = 0; i < n.getNumChildren(); i++)
474		{
475	3515	args.push_back(n[i]);
476		}
477		}
478		else
479		{
480		// arguments must be the same as those already recorded
481	2062	for (unsigned i = 0; i < n.getNumChildren(); i++)
482		{
483	1568	if (args[i] != n[i])
484		{
485	228	Trace("si-prt-debug") << "...bad invocation : " << n
486	114	<< " at arg " << i << "." << std::endl;
487	114	ret = false;
488	114	break;
489		}
490		}
491		}
492	2182	if (ret)
493		{
494	2068	sb.add(n, d_func_inv[f]);
495		}
496		}
497		else
498		{
499	16	Trace("si-prt-debug") << "... " << f << " is a bad operator."
500	8	<< std::endl;
501	8	ret = false;
502		}
503		}
504		}
505		}
506	18448	visited[n] = ret;
507	18448	return ret;
508		}
509		}
510
511	2190	bool SingleInvocationPartition::isAntiSkolemizableType(Node f)
512		{
513	2190	std::map<Node, bool>::iterator it = d_funcs.find(f);
514	2190	if (it != d_funcs.end())
515		{
516	1207	return it->second;
517		}
518		else
519		{
520	1966	TypeNode tn = f.getType();
521	983	bool ret = false;
522	2866	if (((tn.isFunction() && tn.getNumChildren() == d_arg_types.size() + 1)
523	1066	\|\| (d_arg_types.empty() && tn.getNumChildren() == 0)))
524		{
525	975	ret = true;
526	1950	std::vector<Node> children;
527	975	children.push_back(f);
528		// TODO: permutations of arguments
529	3507	for (unsigned i = 0; i < d_arg_types.size(); i++)
530		{
531	2532	children.push_back(d_si_vars[i]);
532	2532	if (tn[i] != d_arg_types[i])
533		{
534		ret = false;
535		break;
536		}
537		}
538	975	if (ret)
539		{
540	1950	Node t;
541	975	if (children.size() > 1)
542		{
543	900	t = NodeManager::currentNM()->mkNode(kind::APPLY_UF, children);
544		}
545		else
546		{
547	75	t = children[0];
548		}
549	975	d_func_inv[f] = t;
550	1950	std::stringstream ss;
551	975	ss << "F_" << f;
552	1950	TypeNode rt;
553	975	if (d_arg_types.empty())
554		{
555	75	rt = tn;
556		}
557		else
558		{
559	900	rt = tn.getRangeType();
560		}
561	1950	Node v = NodeManager::currentNM()->mkBoundVar(ss.str(), rt);
562	975	d_func_fo_var[f] = v;
563	975	d_fo_var_to_func[v] = f;
564	975	d_func_vars.push_back(v);
565	975	d_all_funcs.push_back(f);
566		}
567		}
568	983	d_funcs[f] = ret;
569	983	return ret;
570		}
571		}
572
573	144	Node SingleInvocationPartition::getConjunct(int index)
574		{
575	144	return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst(true)
576	144	: (d_conjuncts[index].size() == 1
577	92	? d_conjuncts[index][0]
578		: NodeManager::currentNM()->mkNode(
579	380	AND, d_conjuncts[index]));
580		}
581
582	525	void SingleInvocationPartition::debugPrint(const char* c)
583		{
584	525	Trace(c) << "Single invocation variables : ";
585	1739	for (unsigned i = 0; i < d_si_vars.size(); i++)
586		{
587	1214	Trace(c) << d_si_vars[i] << " ";
588		}
589	525	Trace(c) << std::endl;
590	525	Trace(c) << "Functions : " << std::endl;
591	1508	for (std::map<Node, bool>::iterator it = d_funcs.begin(); it != d_funcs.end();
592		++it)
593		{
594	983	Trace(c) << " " << it->first << " : ";
595	983	if (it->second)
596		{
597	1950	Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first]
598	975	<< std::endl;
599		}
600		else
601		{
602	8	Trace(c) << "not incorporated." << std::endl;
603		}
604		}
605	2625	for (unsigned i = 0; i < 4; i++)
606		{
607	3675	Trace(c) << (i == 0 ? "Single invocation"
608	2625	: (i == 1 ? "Non-single invocation"
609	1050	: (i == 2 ? "All"
610		: "Non-ground single invocation")));
611	2100	Trace(c) << " conjuncts: " << std::endl;
612	5322	for (unsigned j = 0; j < d_conjuncts[i].size(); j++)
613		{
614	3222	Trace(c) << " " << (j + 1) << " : " << d_conjuncts[i][j] << std::endl;
615		}
616		}
617	525	Trace(c) << std::endl;
618	525	}
619
620		} // namespace quantifiers
621		} // namespace theory
622	31137	} // namespace cvc5