Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/ext_theory.cpp	Lines:	162	250	64.8 %
Date:	2021-09-12	Branches:	276	711	38.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tim King
 *
 * 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.
 * ****************************************************************************
 *
 * Extended theory interface.
 *
 * This implements a generic module, used by theory solvers, for performing
 * "context-dependent simplification", as described in Reynolds et al
 * "Designing Theory Solvers with Extensions", FroCoS 2017.
 */

#include "theory/ext_theory.h"

#include "base/check.h"
#include "smt/smt_statistics_registry.h"
#include "theory/output_channel.h"
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"

using namespace std;

namespace cvc5 {
namespace theory {

const char* toString(ExtReducedId id)
{
  switch (id)
  {
    case ExtReducedId::SR_CONST: return "SR_CONST";
    case ExtReducedId::REDUCTION: return "REDUCTION";
    case ExtReducedId::ARITH_SR_ZERO: return "ARITH_SR_ZERO";
    case ExtReducedId::ARITH_SR_LINEAR: return "ARITH_SR_LINEAR";
    case ExtReducedId::STRINGS_SR_CONST: return "STRINGS_SR_CONST";
    case ExtReducedId::STRINGS_NEG_CTN_DEQ: return "STRINGS_NEG_CTN_DEQ";
    case ExtReducedId::STRINGS_POS_CTN: return "STRINGS_POS_CTN";
    case ExtReducedId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
    case ExtReducedId::STRINGS_REGEXP_INTER: return "STRINGS_REGEXP_INTER";
    case ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME:
      return "STRINGS_REGEXP_INTER_SUBSUME";
    case ExtReducedId::STRINGS_REGEXP_INCLUDE: return "STRINGS_REGEXP_INCLUDE";
    case ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG:
      return "STRINGS_REGEXP_INCLUDE_NEG";
    default: return "?ExtReducedId?";
  }
}

std::ostream& operator<<(std::ostream& out, ExtReducedId id)
{
  out << toString(id);
  return out;
}

bool ExtTheoryCallback::getCurrentSubstitution(
    int effort,
    const std::vector<Node>& vars,
    std::vector<Node>& subs,
    std::map<Node, std::vector<Node> >& exp)
{
  return false;
}
bool ExtTheoryCallback::isExtfReduced(
    int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id)
{
  id = ExtReducedId::SR_CONST;
  return n.isConst();
}
bool ExtTheoryCallback::getReduction(int effort,
                                    Node n,
                                    Node& nr,
                                    bool& isSatDep)
{
  return false;
}

ExtTheory::ExtTheory(ExtTheoryCallback& p,
                     context::Context* c,
                     context::UserContext* u,
                     TheoryInferenceManager& im)
    : d_parent(p),
      d_im(im),
      d_ext_func_terms(c),
      d_extfExtReducedIdMap(c),
      d_ci_inactive(u),
      d_has_extf(c),
      d_lemmas(u),
      d_pp_lemmas(u)
{
  d_true = NodeManager::currentNM()->mkConst(true);
}

// Gets all leaf terms in n.
std::vector<Node> ExtTheory::collectVars(Node n)
{
  std::vector<Node> vars;
  std::set<Node> visited;
  std::vector<Node> worklist;
  worklist.push_back(n);
  while (!worklist.empty())
  {
    Node current = worklist.back();
    worklist.pop_back();
    if (current.isConst() || visited.count(current) > 0)
    {
      continue;
    }
    visited.insert(current);
    // Treat terms not belonging to this theory as leaf
    // note : chould include terms not belonging to this theory
    // (commented below)
    if (current.getNumChildren() > 0)
    {
      worklist.insert(worklist.end(), current.begin(), current.end());
    }
    else
    {
      vars.push_back(current);
    }
  }
  return vars;
}

Node ExtTheory::getSubstitutedTerm(int effort,
                                   Node term,
                                   std::vector<Node>& exp)
{
  std::vector<Node> terms;
  terms.push_back(term);
  std::vector<Node> sterms;
  std::vector<std::vector<Node> > exps;
  getSubstitutedTerms(effort, terms, sterms, exps);
  Assert(sterms.size() == 1);
  Assert(exps.size() == 1);
  exp.insert(exp.end(), exps[0].begin(), exps[0].end());
  return sterms[0];
}

// do inferences
void ExtTheory::getSubstitutedTerms(int effort,
                                    const std::vector<Node>& terms,
                                    std::vector<Node>& sterms,
                                    std::vector<std::vector<Node> >& exp)
{
  Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / "
                      << d_ext_func_terms.size() << " extended functions."
                      << std::endl;
  if (!terms.empty())
  {
    // all variables we need to find a substitution for
    std::vector<Node> vars;
    std::vector<Node> sub;
    std::map<Node, std::vector<Node> > expc;
    for (const Node& n : terms)
    {
      // do substitution, rewrite
      std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
      Assert(iti != d_extf_info.end());
      for (const Node& v : iti->second.d_vars)
      {
        if (std::find(vars.begin(), vars.end(), v) == vars.end())
        {
          vars.push_back(v);
        }
      }
    }
    bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc);
    // get the current substitution for all variables
    Assert(!useSubs || vars.size() == sub.size());
    for (const Node& n : terms)
    {
      Node ns = n;
      std::vector<Node> expn;
      if (useSubs)
      {
        // do substitution
        ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end());
        if (ns != n)
        {
          // build explanation: explanation vars = sub for each vars in FV(n)
          std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
          Assert(iti != d_extf_info.end());
          for (const Node& v : iti->second.d_vars)
          {
            std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
            if (itx != expc.end())
            {
              for (const Node& e : itx->second)
              {
                if (std::find(expn.begin(), expn.end(), e) == expn.end())
                {
                  expn.push_back(e);
                }
              }
            }
          }
        }
        Trace("extt-debug") << "  have " << n << " == " << ns
                            << ", exp size=" << expn.size() << "." << std::endl;
      }
      // add to vector
      sterms.push_back(ns);
      exp.push_back(expn);
    }
  }
}

bool ExtTheory::doInferencesInternal(int effort,
                                     const std::vector<Node>& terms,
                                     std::vector<Node>& nred,
                                     bool batch,
                                     bool isRed)
{
  if (batch)
  {
    bool addedLemma = false;
    if (isRed)
    {
      for (const Node& n : terms)
      {
        Node nr;
        // note: could do reduction with substitution here
        bool satDep = false;
        if (!d_parent.getReduction(effort, n, nr, satDep))
        {
          nred.push_back(n);
        }
        else
        {
          if (!nr.isNull() && n != nr)
          {
            Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, n, nr);
            if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY, true))
            {
              Trace("extt-lemma")
                  << "ExtTheory : reduction lemma : " << lem << std::endl;
              addedLemma = true;
            }
          }
          markReduced(n, ExtReducedId::REDUCTION, satDep);
        }
      }
    }
    else
    {
      std::vector<Node> sterms;
      std::vector<std::vector<Node> > exp;
      getSubstitutedTerms(effort, terms, sterms, exp);
      std::map<Node, unsigned> sterm_index;
      NodeManager* nm = NodeManager::currentNM();
      for (unsigned i = 0, size = terms.size(); i < size; i++)
      {
        bool processed = false;
        if (sterms[i] != terms[i])
        {
          Node sr = Rewriter::rewrite(sterms[i]);
          // ask the theory if this term is reduced, e.g. is it constant or it
          // is a non-extf term.
          ExtReducedId id;
          if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i], id))
          {
            processed = true;
            markReduced(terms[i], id);
            // We have exp[i] => terms[i] = sr, convert this to a clause.
            // This ensures the proof infrastructure can process this as a
            // normal theory lemma.
            Node eq = terms[i].eqNode(sr);
            Node lem = eq;
            if (!exp[i].empty())
            {
              std::vector<Node> eei;
              for (const Node& e : exp[i])
              {
                eei.push_back(e.negate());
              }
              eei.push_back(eq);
              lem = nm->mkNode(kind::OR, eei);
            }

            Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq
                                << " by " << exp[i] << std::endl;
            Trace("extt-debug") << "...send lemma " << lem << std::endl;
            if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY))
            {
              Trace("extt-lemma")
                  << "ExtTheory : substitution + rewrite lemma : " << lem
                  << std::endl;
              addedLemma = true;
            }
          }
          else
          {
            // check if we have already reduced this
            std::map<Node, unsigned>::iterator itsi = sterm_index.find(sr);
            if (itsi == sterm_index.end())
            {
              sterm_index[sr] = i;
            }
            else
            {
              // unsigned j = itsi->second;
              // note : can add (non-reducing) lemma :
              //   exp[j] ^ exp[i] => sterms[i] = sterms[j]
            }

            Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
          }
        }
        else
        {
          Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
        }
        if (!processed)
        {
          nred.push_back(terms[i]);
        }
      }
    }
    return addedLemma;
  }
  // non-batch
  std::vector<Node> nnred;
  if (terms.empty())
  {
    for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
         it != d_ext_func_terms.end();
         ++it)
    {
      if ((*it).second && !isContextIndependentInactive((*it).first))
      {
        std::vector<Node> nterms;
        nterms.push_back((*it).first);
        if (doInferencesInternal(effort, nterms, nnred, true, isRed))
        {
          return true;
        }
      }
    }
  }
  else
  {
    for (const Node& n : terms)
    {
      std::vector<Node> nterms;
      nterms.push_back(n);
      if (doInferencesInternal(effort, nterms, nnred, true, isRed))
      {
        return true;
      }
    }
  }
  return false;
}

bool ExtTheory::sendLemma(Node lem, InferenceId id, bool preprocess)
{
  if (preprocess)
  {
    if (d_pp_lemmas.find(lem) == d_pp_lemmas.end())
    {
      d_pp_lemmas.insert(lem);
      d_im.lemma(lem, id);
      return true;
    }
  }
  else
  {
    if (d_lemmas.find(lem) == d_lemmas.end())
    {
      d_lemmas.insert(lem);
      d_im.lemma(lem, id);
      return true;
    }
  }
  return false;
}

bool ExtTheory::doInferences(int effort,
                             const std::vector<Node>& terms,
                             std::vector<Node>& nred,
                             bool batch)
{
  if (!terms.empty())
  {
    return doInferencesInternal(effort, terms, nred, batch, false);
  }
  return false;
}

bool ExtTheory::doInferences(int effort, std::vector<Node>& nred, bool batch)
{
  std::vector<Node> terms = getActive();
  return doInferencesInternal(effort, terms, nred, batch, false);
}

bool ExtTheory::doReductions(int effort,
                             const std::vector<Node>& terms,
                             std::vector<Node>& nred,
                             bool batch)
{
  if (!terms.empty())
  {
    return doInferencesInternal(effort, terms, nred, batch, true);
  }
  return false;
}

bool ExtTheory::doReductions(int effort, std::vector<Node>& nred, bool batch)
{
  const std::vector<Node> terms = getActive();
  return doInferencesInternal(effort, terms, nred, batch, true);
}

// Register term.
void ExtTheory::registerTerm(Node n)
{
  if (d_extf_kind.find(n.getKind()) != d_extf_kind.end())
  {
    if (d_ext_func_terms.find(n) == d_ext_func_terms.end())
    {
      Trace("extt-debug") << "Found extended function : " << n << std::endl;
      d_ext_func_terms[n] = true;
      d_has_extf = n;
      d_extf_info[n].d_vars = collectVars(n);
    }
  }
}

// mark reduced
void ExtTheory::markReduced(Node n, ExtReducedId rid, bool satDep)
{
  Trace("extt-debug") << "Mark reduced " << n << std::endl;
  registerTerm(n);
  Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
  d_ext_func_terms[n] = false;
  d_extfExtReducedIdMap[n] = rid;
  if (!satDep)
  {
    d_ci_inactive[n] = rid;
  }

  // update has_extf
  if (d_has_extf.get() == n)
  {
    for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
         it != d_ext_func_terms.end();
         ++it)
    {
      // if not already reduced
      if ((*it).second && !isContextIndependentInactive((*it).first))
      {
        d_has_extf = (*it).first;
      }
    }
  }
}

bool ExtTheory::isContextIndependentInactive(Node n) const
{
  ExtReducedId rid = ExtReducedId::UNKNOWN;
  return isContextIndependentInactive(n, rid);
}

bool ExtTheory::isContextIndependentInactive(Node n, ExtReducedId& rid) const
{
  NodeExtReducedIdMap::iterator it = d_ci_inactive.find(n);
  if (it != d_ci_inactive.end())
  {
    rid = it->second;
    return true;
  }
  return false;
}

void ExtTheory::getTerms(std::vector<Node>& terms)
{
  for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
       it != d_ext_func_terms.end();
       ++it)
  {
    terms.push_back((*it).first);
  }
}

bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); }

bool ExtTheory::isActive(Node n) const
{
  ExtReducedId rid = ExtReducedId::UNKNOWN;
  return isActive(n, rid);
}

bool ExtTheory::isActive(Node n, ExtReducedId& rid) const
{
  NodeBoolMap::const_iterator it = d_ext_func_terms.find(n);
  if (it != d_ext_func_terms.end())
  {
    if ((*it).second)
    {
      return !isContextIndependentInactive(n, rid);
    }
    NodeExtReducedIdMap::const_iterator itr = d_extfExtReducedIdMap.find(n);
    Assert(itr != d_extfExtReducedIdMap.end());
    rid = itr->second;
    return false;
  }
  return false;
}

// get active
std::vector<Node> ExtTheory::getActive() const
{
  std::vector<Node> active;
  for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
       it != d_ext_func_terms.end();
       ++it)
  {
    // if not already reduced
    if ((*it).second && !isContextIndependentInactive((*it).first))
    {
      active.push_back((*it).first);
    }
  }
  return active;
}

std::vector<Node> ExtTheory::getActive(Kind k) const
{
  std::vector<Node> active;
  for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
       it != d_ext_func_terms.end();
       ++it)
  {
    // if not already reduced
    if ((*it).first.getKind() == k && (*it).second
        && !isContextIndependentInactive((*it).first))
    {
      active.push_back((*it).first);
    }
  }
  return active;
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Tim King
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		* Extended theory interface.
14		*
15		* This implements a generic module, used by theory solvers, for performing
16		* "context-dependent simplification", as described in Reynolds et al
17		* "Designing Theory Solvers with Extensions", FroCoS 2017.
18		*/
19
20		#include "theory/ext_theory.h"
21
22		#include "base/check.h"
23		#include "smt/smt_statistics_registry.h"
24		#include "theory/output_channel.h"
25		#include "theory/quantifiers_engine.h"
26		#include "theory/rewriter.h"
27		#include "theory/substitutions.h"
28
29		using namespace std;
30
31		namespace cvc5 {
32		namespace theory {
33
34		const char* toString(ExtReducedId id)
35		{
36		switch (id)
37		{
38		case ExtReducedId::SR_CONST: return "SR_CONST";
39		case ExtReducedId::REDUCTION: return "REDUCTION";
40		case ExtReducedId::ARITH_SR_ZERO: return "ARITH_SR_ZERO";
41		case ExtReducedId::ARITH_SR_LINEAR: return "ARITH_SR_LINEAR";
42		case ExtReducedId::STRINGS_SR_CONST: return "STRINGS_SR_CONST";
43		case ExtReducedId::STRINGS_NEG_CTN_DEQ: return "STRINGS_NEG_CTN_DEQ";
44		case ExtReducedId::STRINGS_POS_CTN: return "STRINGS_POS_CTN";
45		case ExtReducedId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
46		case ExtReducedId::STRINGS_REGEXP_INTER: return "STRINGS_REGEXP_INTER";
47		case ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME:
48		return "STRINGS_REGEXP_INTER_SUBSUME";
49		case ExtReducedId::STRINGS_REGEXP_INCLUDE: return "STRINGS_REGEXP_INCLUDE";
50		case ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG:
51		return "STRINGS_REGEXP_INCLUDE_NEG";
52		default: return "?ExtReducedId?";
53		}
54		}
55
56		std::ostream& operator<<(std::ostream& out, ExtReducedId id)
57		{
58		out << toString(id);
59		return out;
60		}
61
62		bool ExtTheoryCallback::getCurrentSubstitution(
63		int effort,
64		const std::vector<Node>& vars,
65		std::vector<Node>& subs,
66		std::map<Node, std::vector<Node> >& exp)
67		{
68		return false;
69		}
70		bool ExtTheoryCallback::isExtfReduced(
71		int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id)
72		{
73		id = ExtReducedId::SR_CONST;
74		return n.isConst();
75		}
76		bool ExtTheoryCallback::getReduction(int effort,
77		Node n,
78		Node& nr,
79		bool& isSatDep)
80		{
81		return false;
82		}
83
84	15110	ExtTheory::ExtTheory(ExtTheoryCallback& p,
85		context::Context* c,
86		context::UserContext* u,
87	15110	TheoryInferenceManager& im)
88		: d_parent(p),
89		d_im(im),
90		d_ext_func_terms(c),
91		d_extfExtReducedIdMap(c),
92		d_ci_inactive(u),
93		d_has_extf(c),
94		d_lemmas(u),
95	15110	d_pp_lemmas(u)
96		{
97	15110	d_true = NodeManager::currentNM()->mkConst(true);
98	15110	}
99
100		// Gets all leaf terms in n.
101	17691	std::vector<Node> ExtTheory::collectVars(Node n)
102		{
103	17691	std::vector<Node> vars;
104	35382	std::set<Node> visited;
105	35382	std::vector<Node> worklist;
106	17691	worklist.push_back(n);
107	237323	while (!worklist.empty())
108		{
109	183131	Node current = worklist.back();
110	109816	worklist.pop_back();
111	109816	if (current.isConst() \|\| visited.count(current) > 0)
112		{
113	36501	continue;
114		}
115	73315	visited.insert(current);
116		// Treat terms not belonging to this theory as leaf
117		// note : chould include terms not belonging to this theory
118		// (commented below)
119	73315	if (current.getNumChildren() > 0)
120		{
121	47056	worklist.insert(worklist.end(), current.begin(), current.end());
122		}
123		else
124		{
125	26259	vars.push_back(current);
126		}
127		}
128	35382	return vars;
129		}
130
131		Node ExtTheory::getSubstitutedTerm(int effort,
132		Node term,
133		std::vector<Node>& exp)
134		{
135		std::vector<Node> terms;
136		terms.push_back(term);
137		std::vector<Node> sterms;
138		std::vector<std::vector<Node> > exps;
139		getSubstitutedTerms(effort, terms, sterms, exps);
140		Assert(sterms.size() == 1);
141		Assert(exps.size() == 1);
142		exp.insert(exp.end(), exps[0].begin(), exps[0].end());
143		return sterms[0];
144		}
145
146		// do inferences
147	34435	void ExtTheory::getSubstitutedTerms(int effort,
148		const std::vector<Node>& terms,
149		std::vector<Node>& sterms,
150		std::vector<std::vector<Node> >& exp)
151		{
152	68870	Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / "
153	68870	<< d_ext_func_terms.size() << " extended functions."
154	34435	<< std::endl;
155	34435	if (!terms.empty())
156		{
157		// all variables we need to find a substitution for
158	8924	std::vector<Node> vars;
159	8924	std::vector<Node> sub;
160	8924	std::map<Node, std::vector<Node> > expc;
161	37337	for (const Node& n : terms)
162		{
163		// do substitution, rewrite
164	32875	std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
165	32875	Assert(iti != d_extf_info.end());
166	87641	for (const Node& v : iti->second.d_vars)
167		{
168	54766	if (std::find(vars.begin(), vars.end(), v) == vars.end())
169		{
170	25441	vars.push_back(v);
171		}
172		}
173		}
174	4462	bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc);
175		// get the current substitution for all variables
176	4462	Assert(!useSubs \|\| vars.size() == sub.size());
177	37337	for (const Node& n : terms)
178		{
179	65750	Node ns = n;
180	65750	std::vector<Node> expn;
181	32875	if (useSubs)
182		{
183		// do substitution
184	20659	ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end());
185	20659	if (ns != n)
186		{
187		// build explanation: explanation vars = sub for each vars in FV(n)
188	6976	std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
189	6976	Assert(iti != d_extf_info.end());
190	20177	for (const Node& v : iti->second.d_vars)
191		{
192	13201	std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
193	13201	if (itx != expc.end())
194		{
195	15512	for (const Node& e : itx->second)
196		{
197	7756	if (std::find(expn.begin(), expn.end(), e) == expn.end())
198		{
199	7756	expn.push_back(e);
200		}
201		}
202		}
203		}
204		}
205	41318	Trace("extt-debug") << " have " << n << " == " << ns
206	20659	<< ", exp size=" << expn.size() << "." << std::endl;
207		}
208		// add to vector
209	32875	sterms.push_back(ns);
210	32875	exp.push_back(expn);
211		}
212		}
213	34435	}
214
215	34435	bool ExtTheory::doInferencesInternal(int effort,
216		const std::vector<Node>& terms,
217		std::vector<Node>& nred,
218		bool batch,
219		bool isRed)
220		{
221	34435	if (batch)
222		{
223	34435	bool addedLemma = false;
224	34435	if (isRed)
225		{
226		for (const Node& n : terms)
227		{
228		Node nr;
229		// note: could do reduction with substitution here
230		bool satDep = false;
231		if (!d_parent.getReduction(effort, n, nr, satDep))
232		{
233		nred.push_back(n);
234		}
235		else
236		{
237		if (!nr.isNull() && n != nr)
238		{
239		Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, n, nr);
240		if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY, true))
241		{
242		Trace("extt-lemma")
243		<< "ExtTheory : reduction lemma : " << lem << std::endl;
244		addedLemma = true;
245		}
246		}
247		markReduced(n, ExtReducedId::REDUCTION, satDep);
248		}
249		}
250		}
251		else
252		{
253	68870	std::vector<Node> sterms;
254	68870	std::vector<std::vector<Node> > exp;
255	34435	getSubstitutedTerms(effort, terms, sterms, exp);
256	68870	std::map<Node, unsigned> sterm_index;
257	34435	NodeManager* nm = NodeManager::currentNM();
258	67310	for (unsigned i = 0, size = terms.size(); i < size; i++)
259		{
260	32875	bool processed = false;
261	32875	if (sterms[i] != terms[i])
262		{
263	13952	Node sr = Rewriter::rewrite(sterms[i]);
264		// ask the theory if this term is reduced, e.g. is it constant or it
265		// is a non-extf term.
266		ExtReducedId id;
267	6976	if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i], id))
268		{
269	5402	processed = true;
270	5402	markReduced(terms[i], id);
271		// We have exp[i] => terms[i] = sr, convert this to a clause.
272		// This ensures the proof infrastructure can process this as a
273		// normal theory lemma.
274	10804	Node eq = terms[i].eqNode(sr);
275	10804	Node lem = eq;
276	5402	if (!exp[i].empty())
277		{
278	10804	std::vector<Node> eei;
279	11314	for (const Node& e : exp[i])
280		{
281	5912	eei.push_back(e.negate());
282		}
283	5402	eei.push_back(eq);
284	5402	lem = nm->mkNode(kind::OR, eei);
285		}
286
287	10804	Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq
288	5402	<< " by " << exp[i] << std::endl;
289	5402	Trace("extt-debug") << "...send lemma " << lem << std::endl;
290	5402	if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY))
291		{
292	3034	Trace("extt-lemma")
293	1517	<< "ExtTheory : substitution + rewrite lemma : " << lem
294	1517	<< std::endl;
295	1517	addedLemma = true;
296		}
297		}
298		else
299		{
300		// check if we have already reduced this
301	1574	std::map<Node, unsigned>::iterator itsi = sterm_index.find(sr);
302	1574	if (itsi == sterm_index.end())
303		{
304	1325	sterm_index[sr] = i;
305		}
306		else
307		{
308		// unsigned j = itsi->second;
309		// note : can add (non-reducing) lemma :
310		// exp[j] ^ exp[i] => sterms[i] = sterms[j]
311		}
312
313	1574	Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
314		}
315		}
316		else
317		{
318	25899	Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
319		}
320	32875	if (!processed)
321		{
322	27473	nred.push_back(terms[i]);
323		}
324		}
325		}
326	34435	return addedLemma;
327		}
328		// non-batch
329		std::vector<Node> nnred;
330		if (terms.empty())
331		{
332		for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
333		it != d_ext_func_terms.end();
334		++it)
335		{
336		if ((it).second && !isContextIndependentInactive((it).first))
337		{
338		std::vector<Node> nterms;
339		nterms.push_back((*it).first);
340		if (doInferencesInternal(effort, nterms, nnred, true, isRed))
341		{
342		return true;
343		}
344		}
345		}
346		}
347		else
348		{
349		for (const Node& n : terms)
350		{
351		std::vector<Node> nterms;
352		nterms.push_back(n);
353		if (doInferencesInternal(effort, nterms, nnred, true, isRed))
354		{
355		return true;
356		}
357		}
358		}
359		return false;
360		}
361
362	5402	bool ExtTheory::sendLemma(Node lem, InferenceId id, bool preprocess)
363		{
364	5402	if (preprocess)
365		{
366		if (d_pp_lemmas.find(lem) == d_pp_lemmas.end())
367		{
368		d_pp_lemmas.insert(lem);
369		d_im.lemma(lem, id);
370		return true;
371		}
372		}
373		else
374		{
375	5402	if (d_lemmas.find(lem) == d_lemmas.end())
376		{
377	1517	d_lemmas.insert(lem);
378	1517	d_im.lemma(lem, id);
379	1517	return true;
380		}
381		}
382	3885	return false;
383		}
384
385		bool ExtTheory::doInferences(int effort,
386		const std::vector<Node>& terms,
387		std::vector<Node>& nred,
388		bool batch)
389		{
390		if (!terms.empty())
391		{
392		return doInferencesInternal(effort, terms, nred, batch, false);
393		}
394		return false;
395		}
396
397	34435	bool ExtTheory::doInferences(int effort, std::vector<Node>& nred, bool batch)
398		{
399	68870	std::vector<Node> terms = getActive();
400	68870	return doInferencesInternal(effort, terms, nred, batch, false);
401		}
402
403		bool ExtTheory::doReductions(int effort,
404		const std::vector<Node>& terms,
405		std::vector<Node>& nred,
406		bool batch)
407		{
408		if (!terms.empty())
409		{
410		return doInferencesInternal(effort, terms, nred, batch, true);
411		}
412		return false;
413		}
414
415		bool ExtTheory::doReductions(int effort, std::vector<Node>& nred, bool batch)
416		{
417		const std::vector<Node> terms = getActive();
418		return doInferencesInternal(effort, terms, nred, batch, true);
419		}
420
421		// Register term.
422	727734	void ExtTheory::registerTerm(Node n)
423		{
424	727734	if (d_extf_kind.find(n.getKind()) != d_extf_kind.end())
425		{
426	177501	if (d_ext_func_terms.find(n) == d_ext_func_terms.end())
427		{
428	17691	Trace("extt-debug") << "Found extended function : " << n << std::endl;
429	17691	d_ext_func_terms[n] = true;
430	17691	d_has_extf = n;
431	17691	d_extf_info[n].d_vars = collectVars(n);
432		}
433		}
434	727734	}
435
436		// mark reduced
437	159810	void ExtTheory::markReduced(Node n, ExtReducedId rid, bool satDep)
438		{
439	159810	Trace("extt-debug") << "Mark reduced " << n << std::endl;
440	159810	registerTerm(n);
441	159810	Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
442	159810	d_ext_func_terms[n] = false;
443	159810	d_extfExtReducedIdMap[n] = rid;
444	159810	if (!satDep)
445		{
446		d_ci_inactive[n] = rid;
447		}
448
449		// update has_extf
450	159810	if (d_has_extf.get() == n)
451		{
452	228284	for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
453	228284	it != d_ext_func_terms.end();
454		++it)
455		{
456		// if not already reduced
457	219726	if ((it).second && !isContextIndependentInactive((it).first))
458		{
459	76776	d_has_extf = (*it).first;
460		}
461		}
462		}
463	159810	}
464
465	901463	bool ExtTheory::isContextIndependentInactive(Node n) const
466		{
467	901463	ExtReducedId rid = ExtReducedId::UNKNOWN;
468	901463	return isContextIndependentInactive(n, rid);
469		}
470
471	1287668	bool ExtTheory::isContextIndependentInactive(Node n, ExtReducedId& rid) const
472		{
473	1287668	NodeExtReducedIdMap::iterator it = d_ci_inactive.find(n);
474	1287668	if (it != d_ci_inactive.end())
475		{
476		rid = it->second;
477		return true;
478		}
479	1287668	return false;
480		}
481
482	4433	void ExtTheory::getTerms(std::vector<Node>& terms)
483		{
484	38348	for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
485	38348	it != d_ext_func_terms.end();
486		++it)
487		{
488	33915	terms.push_back((*it).first);
489		}
490	4433	}
491
492		bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); }
493
494	386205	bool ExtTheory::isActive(Node n) const
495		{
496	386205	ExtReducedId rid = ExtReducedId::UNKNOWN;
497	386205	return isActive(n, rid);
498		}
499
500	386205	bool ExtTheory::isActive(Node n, ExtReducedId& rid) const
501		{
502	386205	NodeBoolMap::const_iterator it = d_ext_func_terms.find(n);
503	386205	if (it != d_ext_func_terms.end())
504		{
505	386205	if ((*it).second)
506		{
507	386205	return !isContextIndependentInactive(n, rid);
508		}
509		NodeExtReducedIdMap::const_iterator itr = d_extfExtReducedIdMap.find(n);
510		Assert(itr != d_extfExtReducedIdMap.end());
511		rid = itr->second;
512		return false;
513		}
514		return false;
515		}
516
517		// get active
518	110426	std::vector<Node> ExtTheory::getActive() const
519		{
520	110426	std::vector<Node> active;
521	1369703	for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
522	1369703	it != d_ext_func_terms.end();
523		++it)
524		{
525		// if not already reduced
526	1259277	if ((it).second && !isContextIndependentInactive((it).first))
527		{
528	823213	active.push_back((*it).first);
529		}
530		}
531	110426	return active;
532		}
533
534	8150	std::vector<Node> ExtTheory::getActive(Kind k) const
535		{
536	8150	std::vector<Node> active;
537	35479	for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
538	35479	it != d_ext_func_terms.end();
539		++it)
540		{
541		// if not already reduced
542	62165	if ((it).first.getKind() == k && (it).second
543	56132	&& !isContextIndependentInactive((*it).first))
544		{
545	1474	active.push_back((*it).first);
546		}
547		}
548	8150	return active;
549		}
550
551		} // namespace theory
552	29511	} // namespace cvc5