Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/skolemize.cpp	Lines:	184	206	89.3 %
Date:	2021-09-29	Branches:	415	992	41.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Andres Noetzli
 *
 * 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 of skolemization utility.
 */

#include "theory/quantifiers/skolemize.h"

#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "proof/proof.h"
#include "proof/proof_node_manager.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
#include "theory/sort_inference.h"
#include "util/rational.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

Skolemize::Skolemize(Env& env,
                     QuantifiersState& qs,
                     TermRegistry& tr,
                     ProofNodeManager* pnm)
    : EnvObj(env),
      d_qstate(qs),
      d_treg(tr),
      d_skolemized(userContext()),
      d_pnm(pnm),
      d_epg(pnm == nullptr
                ? nullptr
                : new EagerProofGenerator(pnm, userContext(), "Skolemize::epg"))
{
}

TrustNode Skolemize::process(Node q)
{
  Assert(q.getKind() == FORALL);
  // do skolemization
  if (d_skolemized.find(q) != d_skolemized.end())
  {
    return TrustNode::null();
  }
  Node lem;
  ProofGenerator* pg = nullptr;
  if (isProofEnabled() && !options::dtStcInduction()
      && !options::intWfInduction())
  {
    // if using proofs and not using induction, we use the justified
    // skolemization
    NodeManager* nm = NodeManager::currentNM();
    SkolemManager* skm = nm->getSkolemManager();
    std::vector<Node> echildren(q.begin(), q.end());
    echildren[1] = echildren[1].notNode();
    Node existsq = nm->mkNode(EXISTS, echildren);
    Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv");
    Node qnot = q.notNode();
    CDProof cdp(d_pnm);
    cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {});
    std::shared_ptr<ProofNode> pf = cdp.getProofFor(res);
    std::vector<Node> assumps;
    assumps.push_back(qnot);
    std::shared_ptr<ProofNode> pfs = d_pnm->mkScope({pf}, assumps);
    lem = nm->mkNode(IMPLIES, qnot, res);
    d_epg->setProofFor(lem, pfs);
    pg = d_epg.get();
    Trace("quantifiers-sk")
        << "Skolemize (with proofs) : " << d_skolem_constants[q] << " for "
        << std::endl;
    Trace("quantifiers-sk") << "   " << q << std::endl;
    Trace("quantifiers-sk") << "   " << res << std::endl;
  }
  else
  {
    // otherwise, we use the more general skolemization with inductive
    // strengthening, which does not support proofs
    Node body = getSkolemizedBody(q);
    NodeBuilder nb(kind::OR);
    nb << q << body.notNode();
    lem = nb;
  }
  d_skolemized[q] = lem;
  // triggered when skolemizing
  d_treg.processSkolemization(q, d_skolem_constants[q]);
  return TrustNode::mkTrustLemma(lem, pg);
}

bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems)
{
  std::unordered_map<Node, std::vector<Node>>::iterator it =
      d_skolem_constants.find(q);
  if (it != d_skolem_constants.end())
  {
    skolems.insert(skolems.end(), it->second.begin(), it->second.end());
    return true;
  }
  return false;
}

Node Skolemize::getSkolemConstant(Node q, unsigned i)
{
  std::unordered_map<Node, std::vector<Node>>::iterator it =
      d_skolem_constants.find(q);
  if (it != d_skolem_constants.end())
  {
    if (i < it->second.size())
    {
      return it->second[i];
    }
  }
  return Node::null();
}

void Skolemize::getSelfSel(const DType& dt,
                           const DTypeConstructor& dc,
                           Node n,
                           TypeNode ntn,
                           std::vector<Node>& selfSel)
{
  TypeNode tspec;
  if (dt.isParametric())
  {
    tspec = dc.getSpecializedConstructorType(n.getType());
    Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
                          << std::endl;
    Assert(tspec.getNumChildren() == dc.getNumArgs());
  }
  Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
                        << dt.getName() << std::endl;
  NodeManager* nm = NodeManager::currentNM();
  for (unsigned j = 0; j < dc.getNumArgs(); j++)
  {
    std::vector<Node> ssc;
    if (dt.isParametric())
    {
      Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
                            << std::endl;
      if (tspec[j] == ntn)
      {
        ssc.push_back(n);
      }
    }
    else
    {
      TypeNode tn = dc[j].getRangeType();
      Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
      if (tn == ntn)
      {
        ssc.push_back(n);
      }
    }
    for (unsigned k = 0; k < ssc.size(); k++)
    {
      Node ss = nm->mkNode(
          APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(n.getType(), j), n);
      if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
      {
        selfSel.push_back(ss);
      }
    }
  }
}

Node Skolemize::mkSkolemizedBody(Node f,
                                 Node n,
                                 std::vector<TNode>& fvs,
                                 std::vector<Node>& sk,
                                 Node& sub,
                                 std::vector<unsigned>& sub_vars)
{
  NodeManager* nm = NodeManager::currentNM();
  // compute the argument types from the free variables
  std::vector<TypeNode> argTypes;
  for (TNode v : fvs)
  {
    argTypes.push_back(v.getType());
  }
  SkolemManager* sm = nm->getSkolemManager();
  Assert(sk.empty() || sk.size() == f[0].getNumChildren());
  // calculate the variables and substitution
  std::vector<TNode> ind_vars;
  std::vector<unsigned> ind_var_indicies;
  std::vector<TNode> vars;
  std::vector<unsigned> var_indicies;
  for (unsigned i = 0; i < f[0].getNumChildren(); i++)
  {
    if (isInductionTerm(f[0][i]))
    {
      ind_vars.push_back(f[0][i]);
      ind_var_indicies.push_back(i);
    }
    else
    {
      vars.push_back(f[0][i]);
      var_indicies.push_back(i);
    }
    Node s;
    // make the new function symbol or use existing
    if (i >= sk.size())
    {
      if (argTypes.empty())
      {
        s = sm->mkDummySkolem(
            "skv", f[0][i].getType(), "created during skolemization");
      }
      else
      {
        TypeNode typ = nm->mkFunctionType(argTypes, f[0][i].getType());
        Node op = sm->mkDummySkolem(
            "skop", typ, "op created during pre-skolemization");
        // DOTHIS: set attribute on op, marking that it should not be selected
        // as trigger
        std::vector<Node> funcArgs;
        funcArgs.push_back(op);
        funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
        s = nm->mkNode(kind::APPLY_UF, funcArgs);
      }
      sk.push_back(s);
    }
    else
    {
      Assert(sk[i].getType() == f[0][i].getType());
    }
  }
  Node ret;
  if (vars.empty())
  {
    ret = n;
  }
  else
  {
    std::vector<Node> var_sk;
    for (unsigned i = 0; i < var_indicies.size(); i++)
    {
      var_sk.push_back(sk[var_indicies[i]]);
    }
    Assert(vars.size() == var_sk.size());
    ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end());
  }
  if (!ind_vars.empty())
  {
    Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
    Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
    Node n_str_ind;
    TypeNode tn = ind_vars[0].getType();
    Node k = sk[ind_var_indicies[0]];
    Node nret = ret.substitute(ind_vars[0], k);
    // note : everything is under a negation
    // the following constructs ~( R( x, k ) => ~P( x ) )
    if (options::dtStcInduction() && tn.isDatatype())
    {
      const DType& dt = tn.getDType();
      std::vector<Node> disj;
      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
      {
        std::vector<Node> selfSel;
        getSelfSel(dt, dt[i], k, tn, selfSel);
        std::vector<Node> conj;
        conj.push_back(nm->mkNode(APPLY_TESTER, dt[i].getTester(), k).negate());
        for (unsigned j = 0; j < selfSel.size(); j++)
        {
          conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
        }
        disj.push_back(conj.size() == 1 ? conj[0] : nm->mkNode(OR, conj));
      }
      Assert(!disj.empty());
      n_str_ind = disj.size() == 1 ? disj[0] : nm->mkNode(AND, disj);
    }
    else if (options::intWfInduction() && tn.isInteger())
    {
      Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0)));
      Node iret = ret.substitute(ind_vars[0],
                                 nm->mkNode(MINUS, k, nm->mkConst(Rational(1))))
                      .negate();
      n_str_ind = nm->mkNode(OR, icond.negate(), iret);
      n_str_ind = nm->mkNode(AND, icond, n_str_ind);
    }
    else
    {
      Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0]
                      << ", type = " << tn << std::endl;
      Assert(false);
    }
    Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;

    std::vector<Node> rem_ind_vars;
    rem_ind_vars.insert(
        rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
    if (!rem_ind_vars.empty())
    {
      Node bvl = nm->mkNode(BOUND_VAR_LIST, rem_ind_vars);
      nret = nm->mkNode(FORALL, bvl, nret);
      nret = Rewriter::rewrite(nret);
      sub = nret;
      sub_vars.insert(
          sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
      n_str_ind = nm->mkNode(FORALL, bvl, n_str_ind.negate()).negate();
    }
    ret = nm->mkNode(OR, nret, n_str_ind);
  }
  Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
                                << " returns : " << ret << std::endl;
  // if it has an instantiation level, set the skolemized body to that level
  if (f.hasAttribute(InstLevelAttribute()))
  {
    QuantAttributes::setInstantiationLevelAttr(
        ret, f.getAttribute(InstLevelAttribute()));
  }

  Trace("quantifiers-sk") << "Skolemize : " << sk << " for " << std::endl;
  Trace("quantifiers-sk") << "   " << f << std::endl;

  return ret;
}

Node Skolemize::getSkolemizedBody(Node f)
{
  Assert(f.getKind() == FORALL);
  std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f);
  if (it == d_skolem_body.end())
  {
    std::vector<TNode> fvs;
    Node sub;
    std::vector<unsigned> sub_vars;
    Node ret =
        mkSkolemizedBody(f, f[1], fvs, d_skolem_constants[f], sub, sub_vars);
    d_skolem_body[f] = ret;
    // store sub quantifier information
    if (!sub.isNull())
    {
      // if we are skolemizing one at a time, we already know the skolem
      // constants of the sub-quantified formula, store them
      Assert(d_skolem_constants[sub].empty());
      for (unsigned i = 0; i < sub_vars.size(); i++)
      {
        d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]);
      }
    }
    Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
    SortInference* si = d_qstate.getSortInference();
    if (si != nullptr)
    {
      for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
      {
        // carry information for sort inference
        si->setSkolemVar(f, f[0][i], d_skolem_constants[f][i]);
      }
    }
    return ret;
  }
  return it->second;
}

bool Skolemize::isInductionTerm(Node n)
{
  TypeNode tn = n.getType();
  if (options::dtStcInduction() && tn.isDatatype())
  {
    const DType& dt = tn.getDType();
    return !dt.isCodatatype();
  }
  if (options::intWfInduction() && tn.isInteger())
  {
    return true;
  }
  return false;
}

void Skolemize::getSkolemTermVectors(
    std::map<Node, std::vector<Node> >& sks) const
{
  std::unordered_map<Node, std::vector<Node>>::const_iterator itk;
  for (const auto& p : d_skolemized)
  {
    Node q = p.first;
    itk = d_skolem_constants.find(q);
    Assert(itk != d_skolem_constants.end());
    sks[q].insert(sks[q].end(), itk->second.begin(), itk->second.end());
  }
}

bool Skolemize::isProofEnabled() const { return d_epg != nullptr; }

}  // 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, Andres Noetzli
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		* Implementation of skolemization utility.
14		*/
15
16		#include "theory/quantifiers/skolemize.h"
17
18		#include "expr/dtype.h"
19		#include "expr/dtype_cons.h"
20		#include "expr/skolem_manager.h"
21		#include "options/quantifiers_options.h"
22		#include "options/smt_options.h"
23		#include "proof/proof.h"
24		#include "proof/proof_node_manager.h"
25		#include "theory/quantifiers/quantifiers_attributes.h"
26		#include "theory/quantifiers/quantifiers_state.h"
27		#include "theory/quantifiers/term_registry.h"
28		#include "theory/quantifiers/term_util.h"
29		#include "theory/rewriter.h"
30		#include "theory/sort_inference.h"
31		#include "util/rational.h"
32
33		using namespace cvc5::kind;
34
35		namespace cvc5 {
36		namespace theory {
37		namespace quantifiers {
38
39	6271	Skolemize::Skolemize(Env& env,
40		QuantifiersState& qs,
41		TermRegistry& tr,
42	6271	ProofNodeManager* pnm)
43		: EnvObj(env),
44		d_qstate(qs),
45		d_treg(tr),
46	6271	d_skolemized(userContext()),
47		d_pnm(pnm),
48		d_epg(pnm == nullptr
49		? nullptr
50	12542	: new EagerProofGenerator(pnm, userContext(), "Skolemize::epg"))
51		{
52	6271	}
53
54	4100	TrustNode Skolemize::process(Node q)
55		{
56	4100	Assert(q.getKind() == FORALL);
57		// do skolemization
58	4100	if (d_skolemized.find(q) != d_skolemized.end())
59		{
60	2852	return TrustNode::null();
61		}
62	2496	Node lem;
63	1248	ProofGenerator* pg = nullptr;
64	2501	if (isProofEnabled() && !options::dtStcInduction()
65	1253	&& !options::intWfInduction())
66		{
67		// if using proofs and not using induction, we use the justified
68		// skolemization
69	5	NodeManager* nm = NodeManager::currentNM();
70	5	SkolemManager* skm = nm->getSkolemManager();
71	10	std::vector<Node> echildren(q.begin(), q.end());
72	5	echildren[1] = echildren[1].notNode();
73	10	Node existsq = nm->mkNode(EXISTS, echildren);
74	10	Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv");
75	10	Node qnot = q.notNode();
76	10	CDProof cdp(d_pnm);
77	5	cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {});
78	10	std::shared_ptr<ProofNode> pf = cdp.getProofFor(res);
79	10	std::vector<Node> assumps;
80	5	assumps.push_back(qnot);
81	10	std::shared_ptr<ProofNode> pfs = d_pnm->mkScope({pf}, assumps);
82	5	lem = nm->mkNode(IMPLIES, qnot, res);
83	5	d_epg->setProofFor(lem, pfs);
84	5	pg = d_epg.get();
85	10	Trace("quantifiers-sk")
86	5	<< "Skolemize (with proofs) : " << d_skolem_constants[q] << " for "
87	5	<< std::endl;
88	5	Trace("quantifiers-sk") << " " << q << std::endl;
89	5	Trace("quantifiers-sk") << " " << res << std::endl;
90		}
91		else
92		{
93		// otherwise, we use the more general skolemization with inductive
94		// strengthening, which does not support proofs
95	2486	Node body = getSkolemizedBody(q);
96	2486	NodeBuilder nb(kind::OR);
97	1243	nb << q << body.notNode();
98	1243	lem = nb;
99		}
100	1248	d_skolemized[q] = lem;
101		// triggered when skolemizing
102	1248	d_treg.processSkolemization(q, d_skolem_constants[q]);
103	1248	return TrustNode::mkTrustLemma(lem, pg);
104		}
105
106	6	bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems)
107		{
108		std::unordered_map<Node, std::vector<Node>>::iterator it =
109	6	d_skolem_constants.find(q);
110	6	if (it != d_skolem_constants.end())
111		{
112	6	skolems.insert(skolems.end(), it->second.begin(), it->second.end());
113	6	return true;
114		}
115		return false;
116		}
117
118		Node Skolemize::getSkolemConstant(Node q, unsigned i)
119		{
120		std::unordered_map<Node, std::vector<Node>>::iterator it =
121		d_skolem_constants.find(q);
122		if (it != d_skolem_constants.end())
123		{
124		if (i < it->second.size())
125		{
126		return it->second[i];
127		}
128		}
129		return Node::null();
130		}
131
132	28	void Skolemize::getSelfSel(const DType& dt,
133		const DTypeConstructor& dc,
134		Node n,
135		TypeNode ntn,
136		std::vector<Node>& selfSel)
137		{
138	56	TypeNode tspec;
139	28	if (dt.isParametric())
140		{
141		tspec = dc.getSpecializedConstructorType(n.getType());
142		Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
143		<< std::endl;
144		Assert(tspec.getNumChildren() == dc.getNumArgs());
145		}
146	56	Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
147	28	<< dt.getName() << std::endl;
148	28	NodeManager* nm = NodeManager::currentNM();
149	54	for (unsigned j = 0; j < dc.getNumArgs(); j++)
150		{
151	52	std::vector<Node> ssc;
152	26	if (dt.isParametric())
153		{
154		Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
155		<< std::endl;
156		if (tspec[j] == ntn)
157		{
158		ssc.push_back(n);
159		}
160		}
161		else
162		{
163	52	TypeNode tn = dc[j].getRangeType();
164	26	Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
165	26	if (tn == ntn)
166		{
167	14	ssc.push_back(n);
168		}
169		}
170	40	for (unsigned k = 0; k < ssc.size(); k++)
171		{
172		Node ss = nm->mkNode(
173	28	APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(n.getType(), j), n);
174	14	if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
175		{
176	14	selfSel.push_back(ss);
177		}
178		}
179		}
180	28	}
181
182	1254	Node Skolemize::mkSkolemizedBody(Node f,
183		Node n,
184		std::vector<TNode>& fvs,
185		std::vector<Node>& sk,
186		Node& sub,
187		std::vector<unsigned>& sub_vars)
188		{
189	1254	NodeManager* nm = NodeManager::currentNM();
190		// compute the argument types from the free variables
191	2508	std::vector<TypeNode> argTypes;
192	1264	for (TNode v : fvs)
193		{
194	10	argTypes.push_back(v.getType());
195		}
196	1254	SkolemManager* sm = nm->getSkolemManager();
197	1254	Assert(sk.empty() \|\| sk.size() == f[0].getNumChildren());
198		// calculate the variables and substitution
199	2508	std::vector<TNode> ind_vars;
200	2508	std::vector<unsigned> ind_var_indicies;
201	2508	std::vector<TNode> vars;
202	2508	std::vector<unsigned> var_indicies;
203	3117	for (unsigned i = 0; i < f[0].getNumChildren(); i++)
204		{
205	1863	if (isInductionTerm(f[0][i]))
206		{
207	23	ind_vars.push_back(f[0][i]);
208	23	ind_var_indicies.push_back(i);
209		}
210		else
211		{
212	1840	vars.push_back(f[0][i]);
213	1840	var_indicies.push_back(i);
214		}
215	3726	Node s;
216		// make the new function symbol or use existing
217	1863	if (i >= sk.size())
218		{
219	1857	if (argTypes.empty())
220		{
221	5550	s = sm->mkDummySkolem(
222	3700	"skv", f[0][i].getType(), "created during skolemization");
223		}
224		else
225		{
226	14	TypeNode typ = nm->mkFunctionType(argTypes, f[0][i].getType());
227		Node op = sm->mkDummySkolem(
228	14	"skop", typ, "op created during pre-skolemization");
229		// DOTHIS: set attribute on op, marking that it should not be selected
230		// as trigger
231	14	std::vector<Node> funcArgs;
232	7	funcArgs.push_back(op);
233	7	funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
234	7	s = nm->mkNode(kind::APPLY_UF, funcArgs);
235		}
236	1857	sk.push_back(s);
237		}
238		else
239		{
240	6	Assert(sk[i].getType() == f[0][i].getType());
241		}
242		}
243	1254	Node ret;
244	1254	if (vars.empty())
245		{
246	17	ret = n;
247		}
248		else
249		{
250	2474	std::vector<Node> var_sk;
251	3077	for (unsigned i = 0; i < var_indicies.size(); i++)
252		{
253	1840	var_sk.push_back(sk[var_indicies[i]]);
254		}
255	1237	Assert(vars.size() == var_sk.size());
256	1237	ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end());
257		}
258	1254	if (!ind_vars.empty())
259		{
260	17	Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
261	17	Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
262	34	Node n_str_ind;
263	34	TypeNode tn = ind_vars[0].getType();
264	34	Node k = sk[ind_var_indicies[0]];
265	34	Node nret = ret.substitute(ind_vars[0], k);
266		// note : everything is under a negation
267		// the following constructs ~( R( x, k ) => ~P( x ) )
268	17	if (options::dtStcInduction() && tn.isDatatype())
269		{
270	14	const DType& dt = tn.getDType();
271	28	std::vector<Node> disj;
272	42	for (unsigned i = 0; i < dt.getNumConstructors(); i++)
273		{
274	56	std::vector<Node> selfSel;
275	28	getSelfSel(dt, dt[i], k, tn, selfSel);
276	56	std::vector<Node> conj;
277	28	conj.push_back(nm->mkNode(APPLY_TESTER, dt[i].getTester(), k).negate());
278	42	for (unsigned j = 0; j < selfSel.size(); j++)
279		{
280	14	conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
281		}
282	28	disj.push_back(conj.size() == 1 ? conj[0] : nm->mkNode(OR, conj));
283		}
284	14	Assert(!disj.empty());
285	14	n_str_ind = disj.size() == 1 ? disj[0] : nm->mkNode(AND, disj);
286		}
287	3	else if (options::intWfInduction() && tn.isInteger())
288		{
289	6	Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0)));
290	6	Node iret = ret.substitute(ind_vars[0],
291	6	nm->mkNode(MINUS, k, nm->mkConst(Rational(1))))
292	6	.negate();
293	3	n_str_ind = nm->mkNode(OR, icond.negate(), iret);
294	3	n_str_ind = nm->mkNode(AND, icond, n_str_ind);
295		}
296		else
297		{
298		Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0]
299		<< ", type = " << tn << std::endl;
300		Assert(false);
301		}
302	17	Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
303
304	34	std::vector<Node> rem_ind_vars;
305	17	rem_ind_vars.insert(
306	34	rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
307	17	if (!rem_ind_vars.empty())
308		{
309	10	Node bvl = nm->mkNode(BOUND_VAR_LIST, rem_ind_vars);
310	5	nret = nm->mkNode(FORALL, bvl, nret);
311	5	nret = Rewriter::rewrite(nret);
312	5	sub = nret;
313	5	sub_vars.insert(
314	10	sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
315	5	n_str_ind = nm->mkNode(FORALL, bvl, n_str_ind.negate()).negate();
316		}
317	17	ret = nm->mkNode(OR, nret, n_str_ind);
318		}
319	2508	Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
320	1254	<< " returns : " << ret << std::endl;
321		// if it has an instantiation level, set the skolemized body to that level
322	1254	if (f.hasAttribute(InstLevelAttribute()))
323		{
324		QuantAttributes::setInstantiationLevelAttr(
325		ret, f.getAttribute(InstLevelAttribute()));
326		}
327
328	1254	Trace("quantifiers-sk") << "Skolemize : " << sk << " for " << std::endl;
329	1254	Trace("quantifiers-sk") << " " << f << std::endl;
330
331	2508	return ret;
332		}
333
334	1243	Node Skolemize::getSkolemizedBody(Node f)
335		{
336	1243	Assert(f.getKind() == FORALL);
337	1243	std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f);
338	1243	if (it == d_skolem_body.end())
339		{
340	2478	std::vector<TNode> fvs;
341	2478	Node sub;
342	2478	std::vector<unsigned> sub_vars;
343		Node ret =
344	2478	mkSkolemizedBody(f, f[1], fvs, d_skolem_constants[f], sub, sub_vars);
345	1239	d_skolem_body[f] = ret;
346		// store sub quantifier information
347	1239	if (!sub.isNull())
348		{
349		// if we are skolemizing one at a time, we already know the skolem
350		// constants of the sub-quantified formula, store them
351	5	Assert(d_skolem_constants[sub].empty());
352	11	for (unsigned i = 0; i < sub_vars.size(); i++)
353		{
354	6	d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]);
355		}
356		}
357	1239	Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
358	1239	SortInference* si = d_qstate.getSortInference();
359	1239	if (si != nullptr)
360		{
361		for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
362		{
363		// carry information for sort inference
364		si->setSkolemVar(f, f[0][i], d_skolem_constants[f][i]);
365		}
366		}
367	1239	return ret;
368		}
369	4	return it->second;
370		}
371
372	3864	bool Skolemize::isInductionTerm(Node n)
373		{
374	7728	TypeNode tn = n.getType();
375	3864	if (options::dtStcInduction() && tn.isDatatype())
376		{
377	981	const DType& dt = tn.getDType();
378	981	return !dt.isCodatatype();
379		}
380	2883	if (options::intWfInduction() && tn.isInteger())
381		{
382	803	return true;
383		}
384	2080	return false;
385		}
386
387	4	void Skolemize::getSkolemTermVectors(
388		std::map<Node, std::vector<Node> >& sks) const
389		{
390	4	std::unordered_map<Node, std::vector<Node>>::const_iterator itk;
391	7	for (const auto& p : d_skolemized)
392		{
393	6	Node q = p.first;
394	3	itk = d_skolem_constants.find(q);
395	3	Assert(itk != d_skolem_constants.end());
396	3	sks[q].insert(sks[q].end(), itk->second.begin(), itk->second.end());
397		}
398	4	}
399
400	1248	bool Skolemize::isProofEnabled() const { return d_epg != nullptr; }
401
402		} // namespace quantifiers
403		} // namespace theory
404	22746	} // namespace cvc5