Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/transition_inference.cpp	Lines:	280	298	94.0 %
Date:	2021-05-24	Branches:	521	1118	46.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of utility for inferring whether a synthesis conjecture
 * encodes a transition system.
 */
#include "theory/quantifiers/sygus/transition_inference.h"

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

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

bool DetTrace::DetTraceTrie::add(Node loc, const std::vector<Node>& val)
{
  DetTraceTrie* curr = this;
  for (const Node& v : val)
  {
    curr = &(curr->d_children[v]);
  }
  if (curr->d_children.empty())
  {
    curr->d_children[loc].clear();
    return true;
  }
  return false;
}

Node DetTrace::DetTraceTrie::constructFormula(const std::vector<Node>& vars,
                                              unsigned index)
{
  NodeManager* nm = NodeManager::currentNM();
  if (index == vars.size())
  {
    return nm->mkConst(true);
  }
  std::vector<Node> disj;
  for (std::pair<const Node, DetTraceTrie>& p : d_children)
  {
    Node eq = vars[index].eqNode(p.first);
    if (index < vars.size() - 1)
    {
      Node conc = p.second.constructFormula(vars, index + 1);
      disj.push_back(nm->mkNode(AND, eq, conc));
    }
    else
    {
      disj.push_back(eq);
    }
  }
  Assert(!disj.empty());
  return disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
}

bool DetTrace::increment(Node loc, std::vector<Node>& vals)
{
  if (d_trie.add(loc, vals))
  {
    for (unsigned i = 0, vsize = vals.size(); i < vsize; i++)
    {
      d_curr[i] = vals[i];
    }
    return true;
  }
  return false;
}

Node DetTrace::constructFormula(const std::vector<Node>& vars)
{
  return d_trie.constructFormula(vars);
}

void DetTrace::print(const char* c) const
{
  for (const Node& n : d_curr)
  {
    Trace(c) << n << " ";
  }
}

Node TransitionInference::getFunction() const { return d_func; }

void TransitionInference::getVariables(std::vector<Node>& vars) const
{
  vars.insert(vars.end(), d_vars.begin(), d_vars.end());
}

Node TransitionInference::getPreCondition() const { return d_pre.d_this; }
Node TransitionInference::getPostCondition() const { return d_post.d_this; }
Node TransitionInference::getTransitionRelation() const
{
  return d_trans.d_this;
}

void TransitionInference::getConstantSubstitution(
    const std::vector<Node>& vars,
    const std::vector<Node>& disjuncts,
    std::vector<Node>& const_var,
    std::vector<Node>& const_subs,
    bool reqPol)
{
  for (const Node& d : disjuncts)
  {
    Node sn;
    if (!const_var.empty())
    {
      sn = d.substitute(const_var.begin(),
                        const_var.end(),
                        const_subs.begin(),
                        const_subs.end());
      sn = Rewriter::rewrite(sn);
    }
    else
    {
      sn = d;
    }
    bool slit_pol = sn.getKind() != NOT;
    Node slit = sn.getKind() == NOT ? sn[0] : sn;
    if (slit.getKind() == EQUAL && slit_pol == reqPol)
    {
      // check if it is a variable equality
      TNode v;
      Node s;
      for (unsigned r = 0; r < 2; r++)
      {
        if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end())
        {
          if (!expr::hasSubterm(slit[1 - r], slit[r]))
          {
            v = slit[r];
            s = slit[1 - r];
            break;
          }
        }
      }
      if (v.isNull())
      {
        // solve for var
        std::map<Node, Node> msum;
        if (ArithMSum::getMonomialSumLit(slit, msum))
        {
          for (std::pair<const Node, Node>& m : msum)
          {
            if (std::find(vars.begin(), vars.end(), m.first) != vars.end())
            {
              Node veq_c;
              Node val;
              int ires = ArithMSum::isolate(m.first, msum, veq_c, val, EQUAL);
              if (ires != 0 && veq_c.isNull()
                  && !expr::hasSubterm(val, m.first))
              {
                v = m.first;
                s = val;
              }
            }
          }
        }
      }
      if (!v.isNull())
      {
        TNode ts = s;
        for (unsigned k = 0, csize = const_subs.size(); k < csize; k++)
        {
          const_subs[k] = Rewriter::rewrite(const_subs[k].substitute(v, ts));
        }
        Trace("cegqi-inv-debug2")
            << "...substitution : " << v << " -> " << s << std::endl;
        const_var.push_back(v);
        const_subs.push_back(s);
      }
    }
  }
}

void TransitionInference::process(Node n, Node f)
{
  // set the function
  d_func = f;
  process(n);
}

void TransitionInference::process(Node n)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  d_complete = true;
  d_trivial = true;
  std::vector<Node> n_check;
  if (n.getKind() == AND)
  {
    for (const Node& nc : n)
    {
      n_check.push_back(nc);
    }
  }
  else
  {
    n_check.push_back(n);
  }
  for (const Node& nn : n_check)
  {
    std::map<bool, std::map<Node, bool> > visited;
    std::map<bool, Node> terms;
    std::vector<Node> disjuncts;
    Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn
                       << std::endl;
    if (!processDisjunct(nn, terms, disjuncts, visited, true))
    {
      d_complete = false;
      continue;
    }
    if (terms.empty())
    {
      continue;
    }
    Node curr;
    // The component that this disjunct contributes to, where
    // 1 : pre-condition, -1 : post-condition, 0 : transition relation
    int comp_num;
    std::map<bool, Node>::iterator itt = terms.find(false);
    if (itt != terms.end())
    {
      curr = itt->second;
      if (terms.find(true) != terms.end())
      {
        comp_num = 0;
      }
      else
      {
        comp_num = -1;
      }
    }
    else
    {
      curr = terms[true];
      comp_num = 1;
    }
    Trace("cegqi-inv-debug2") << "  normalize based on " << curr << std::endl;
    std::vector<Node> vars;
    std::vector<Node> svars;
    getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts);
    for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
    {
      Trace("cegqi-inv-debug2") << "  apply " << disjuncts[j] << std::endl;
      disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
          vars.begin(), vars.end(), svars.begin(), svars.end()));
      Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
    }
    std::vector<Node> const_var;
    std::vector<Node> const_subs;
    if (comp_num == 0)
    {
      // transition
      Assert(terms.find(true) != terms.end());
      Node next = terms[true];
      next = Rewriter::rewrite(next.substitute(
          vars.begin(), vars.end(), svars.begin(), svars.end()));
      Trace("cegqi-inv-debug")
          << "transition next predicate : " << next << std::endl;
      // make the primed variables if we have not already
      if (d_prime_vars.empty())
      {
        for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; j++)
        {
          Node v = sm->mkDummySkolem(
              "ir", next[j].getType(), "template inference rev argument");
          d_prime_vars.push_back(v);
        }
      }
      // normalize the other direction
      Trace("cegqi-inv-debug2") << "  normalize based on " << next << std::endl;
      std::vector<Node> rvars;
      std::vector<Node> rsvars;
      getNormalizedSubstitution(next, d_prime_vars, rvars, rsvars, disjuncts);
      Assert(rvars.size() == rsvars.size());
      for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
      {
        Trace("cegqi-inv-debug2") << "  apply " << disjuncts[j] << std::endl;
        disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
            rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end()));
        Trace("cegqi-inv-debug2") << "  ..." << disjuncts[j] << std::endl;
      }
      getConstantSubstitution(
          d_prime_vars, disjuncts, const_var, const_subs, false);
    }
    else
    {
      getConstantSubstitution(d_vars, disjuncts, const_var, const_subs, false);
    }
    Node res;
    if (disjuncts.empty())
    {
      res = nm->mkConst(false);
    }
    else if (disjuncts.size() == 1)
    {
      res = disjuncts[0];
    }
    else
    {
      res = nm->mkNode(OR, disjuncts);
    }
    if (expr::hasBoundVar(res))
    {
      Trace("cegqi-inv-debug2") << "...failed, free variable." << std::endl;
      d_complete = false;
      continue;
    }
    Trace("cegqi-inv") << "*** inferred "
                       << (comp_num == 1 ? "pre"
                                         : (comp_num == -1 ? "post" : "trans"))
                       << "-condition : " << res << std::endl;
    Component& c =
        (comp_num == 1 ? d_pre : (comp_num == -1 ? d_post : d_trans));
    c.d_conjuncts.push_back(res);
    if (!const_var.empty())
    {
      bool has_const_eq = const_var.size() == d_vars.size();
      Trace("cegqi-inv") << "    with constant substitution, complete = "
                         << has_const_eq << " : " << std::endl;
      for (unsigned i = 0, csize = const_var.size(); i < csize; i++)
      {
        Trace("cegqi-inv") << "      " << const_var[i] << " -> "
                           << const_subs[i] << std::endl;
        if (has_const_eq)
        {
          c.d_const_eq[res][const_var[i]] = const_subs[i];
        }
      }
      Trace("cegqi-inv") << "...size = " << const_var.size()
                         << ", #vars = " << d_vars.size() << std::endl;
    }
  }

  // finalize the components
  for (int i = -1; i <= 1; i++)
  {
    Component& c = (i == 1 ? d_pre : (i == -1 ? d_post : d_trans));
    Node ret;
    if (c.d_conjuncts.empty())
    {
      ret = nm->mkConst(true);
    }
    else if (c.d_conjuncts.size() == 1)
    {
      ret = c.d_conjuncts[0];
    }
    else
    {
      ret = nm->mkNode(AND, c.d_conjuncts);
    }
    if (i == 0 || i == 1)
    {
      // pre-condition and transition are negated
      ret = TermUtil::simpleNegate(ret);
    }
    c.d_this = ret;
  }
}
void TransitionInference::getNormalizedSubstitution(
    Node curr,
    const std::vector<Node>& pvars,
    std::vector<Node>& vars,
    std::vector<Node>& subs,
    std::vector<Node>& disjuncts)
{
  for (unsigned j = 0, nchild = curr.getNumChildren(); j < nchild; j++)
  {
    if (curr[j].getKind() == BOUND_VARIABLE)
    {
      // if the argument is a bound variable, add to the renaming
      vars.push_back(curr[j]);
      subs.push_back(pvars[j]);
    }
    else
    {
      // otherwise, treat as a constraint on the variable
      // For example, this transforms e.g. a precondition clause
      // I( 0, 1 ) to x1 != 0 OR x2 != 1 OR I( x1, x2 ).
      Node eq = curr[j].eqNode(pvars[j]);
      disjuncts.push_back(eq.negate());
    }
  }
}

bool TransitionInference::processDisjunct(
    Node n,
    std::map<bool, Node>& terms,
    std::vector<Node>& disjuncts,
    std::map<bool, std::map<Node, bool> >& visited,
    bool topLevel)
{
  if (visited[topLevel].find(n) != visited[topLevel].end())
  {
    return true;
  }
  visited[topLevel][n] = true;
  bool childTopLevel = n.getKind() == OR && topLevel;
  // if another part mentions UF or a free variable, then fail
  bool lit_pol = n.getKind() != NOT;
  Node lit = n.getKind() == NOT ? n[0] : n;
  // is it an application of the function-to-synthesize? Yes if we haven't
  // encountered a function or if it matches the existing d_func.
  if (lit.getKind() == APPLY_UF
      && (d_func.isNull() || lit.getOperator() == d_func))
  {
    Node op = lit.getOperator();
    // initialize the variables
    if (d_trivial)
    {
      d_trivial = false;
      d_func = op;
      Trace("cegqi-inv-debug") << "Use " << op << " with args ";
      NodeManager* nm = NodeManager::currentNM();
      SkolemManager* sm = nm->getSkolemManager();
      for (const Node& l : lit)
      {
        Node v =
            sm->mkDummySkolem("i", l.getType(), "template inference argument");
        d_vars.push_back(v);
        Trace("cegqi-inv-debug") << v << " ";
      }
      Trace("cegqi-inv-debug") << std::endl;
    }
    Assert(!d_func.isNull());
    if (topLevel)
    {
      if (terms.find(lit_pol) == terms.end())
      {
        terms[lit_pol] = lit;
        return true;
      }
      else
      {
        Trace("cegqi-inv-debug")
            << "...failed, repeated inv-app : " << lit << std::endl;
        return false;
      }
    }
    Trace("cegqi-inv-debug")
        << "...failed, non-entailed inv-app : " << lit << std::endl;
    return false;
  }
  else if (topLevel && !childTopLevel)
  {
    disjuncts.push_back(n);
  }
  for (const Node& nc : n)
  {
    if (!processDisjunct(nc, terms, disjuncts, visited, childTopLevel))
    {
      return false;
    }
  }
  return true;
}

TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt,
                                                    Node loc,
                                                    bool fwd)
{
  Component& c = fwd ? d_pre : d_post;
  Assert(c.has(loc));
  std::map<Node, std::map<Node, Node> >::iterator it = c.d_const_eq.find(loc);
  if (it != c.d_const_eq.end())
  {
    std::vector<Node> next;
    for (const Node& v : d_vars)
    {
      Assert(it->second.find(v) != it->second.end());
      next.push_back(it->second[v]);
      dt.d_curr.push_back(it->second[v]);
    }
    Trace("cegqi-inv-debug2") << "dtrace : initial increment" << std::endl;
    bool ret = dt.increment(loc, next);
    AlwaysAssert(ret);
    return TRACE_INC_SUCCESS;
  }
  return TRACE_INC_INVALID;
}

TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt,
                                                   Node loc,
                                                   bool fwd)
{
  Assert(d_trans.has(loc));
  // check if it satisfies the pre/post condition
  Node cc = fwd ? getPostCondition() : getPreCondition();
  Assert(!cc.isNull());
  Node ccr = Rewriter::rewrite(cc.substitute(
      d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
  if (ccr.isConst())
  {
    if (ccr.getConst<bool>() == (fwd ? false : true))
    {
      Trace("cegqi-inv-debug2") << "dtrace : counterexample" << std::endl;
      return TRACE_INC_CEX;
    }
  }

  // terminates?
  Node c = getTransitionRelation();
  Assert(!c.isNull());

  Assert(d_vars.size() == dt.d_curr.size());
  Node cr = Rewriter::rewrite(c.substitute(
      d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
  if (cr.isConst())
  {
    if (!cr.getConst<bool>())
    {
      Trace("cegqi-inv-debug2") << "dtrace : terminated" << std::endl;
      return TRACE_INC_TERMINATE;
    }
    return TRACE_INC_INVALID;
  }
  if (!fwd)
  {
    // only implemented in forward direction
    Assert(false);
    return TRACE_INC_INVALID;
  }
  Component& cm = d_trans;
  std::map<Node, std::map<Node, Node> >::iterator it = cm.d_const_eq.find(loc);
  if (it == cm.d_const_eq.end())
  {
    return TRACE_INC_INVALID;
  }
  std::vector<Node> next;
  for (const Node& pv : d_prime_vars)
  {
    Assert(it->second.find(pv) != it->second.end());
    Node pvs = it->second[pv];
    Assert(d_vars.size() == dt.d_curr.size());
    Node pvsr = Rewriter::rewrite(pvs.substitute(
        d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
    next.push_back(pvsr);
  }
  if (dt.increment(loc, next))
  {
    Trace("cegqi-inv-debug2") << "dtrace : success increment" << std::endl;
    return TRACE_INC_SUCCESS;
  }
  // looped
  Trace("cegqi-inv-debug2") << "dtrace : looped" << std::endl;
  return TRACE_INC_TERMINATE;
}

TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt, bool fwd)
{
  Trace("cegqi-inv-debug2") << "Initialize trace" << std::endl;
  Component& c = fwd ? d_pre : d_post;
  if (c.d_conjuncts.size() == 1)
  {
    return initializeTrace(dt, c.d_conjuncts[0], fwd);
  }
  return TRACE_INC_INVALID;
}

TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt, bool fwd)
{
  if (d_trans.d_conjuncts.size() == 1)
  {
    return incrementTrace(dt, d_trans.d_conjuncts[0], fwd);
  }
  return TRACE_INC_INVALID;
}

Node TransitionInference::constructFormulaTrace(DetTrace& dt) const
{
  return dt.constructFormula(d_vars);
}

}  // 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, Andres Noetzli, 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		* Implementation of utility for inferring whether a synthesis conjecture
14		* encodes a transition system.
15		*/
16		#include "theory/quantifiers/sygus/transition_inference.h"
17
18		#include "expr/node_algorithm.h"
19		#include "expr/skolem_manager.h"
20		#include "theory/arith/arith_msum.h"
21		#include "theory/quantifiers/term_util.h"
22		#include "theory/rewriter.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace quantifiers {
29
30	428	bool DetTrace::DetTraceTrie::add(Node loc, const std::vector<Node>& val)
31		{
32	428	DetTraceTrie* curr = this;
33	1270	for (const Node& v : val)
34		{
35	842	curr = &(curr->d_children[v]);
36		}
37	428	if (curr->d_children.empty())
38		{
39	428	curr->d_children[loc].clear();
40	428	return true;
41		}
42		return false;
43		}
44
45	14	Node DetTrace::DetTraceTrie::constructFormula(const std::vector<Node>& vars,
46		unsigned index)
47		{
48	14	NodeManager* nm = NodeManager::currentNM();
49	14	if (index == vars.size())
50		{
51		return nm->mkConst(true);
52		}
53	28	std::vector<Node> disj;
54	48	for (std::pair<const Node, DetTraceTrie>& p : d_children)
55		{
56	68	Node eq = vars[index].eqNode(p.first);
57	34	if (index < vars.size() - 1)
58		{
59	20	Node conc = p.second.constructFormula(vars, index + 1);
60	10	disj.push_back(nm->mkNode(AND, eq, conc));
61		}
62		else
63		{
64	24	disj.push_back(eq);
65		}
66		}
67	14	Assert(!disj.empty());
68	14	return disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
69		}
70
71	428	bool DetTrace::increment(Node loc, std::vector<Node>& vals)
72		{
73	428	if (d_trie.add(loc, vals))
74		{
75	1270	for (unsigned i = 0, vsize = vals.size(); i < vsize; i++)
76		{
77	842	d_curr[i] = vals[i];
78		}
79	428	return true;
80		}
81		return false;
82		}
83
84	4	Node DetTrace::constructFormula(const std::vector<Node>& vars)
85		{
86	4	return d_trie.constructFormula(vars);
87		}
88
89	432	void DetTrace::print(const char* c) const
90		{
91	1280	for (const Node& n : d_curr)
92		{
93	848	Trace(c) << n << " ";
94		}
95	432	}
96
97	37	Node TransitionInference::getFunction() const { return d_func; }
98
99	37	void TransitionInference::getVariables(std::vector<Node>& vars) const
100		{
101	37	vars.insert(vars.end(), d_vars.begin(), d_vars.end());
102	37	}
103
104	37	Node TransitionInference::getPreCondition() const { return d_pre.d_this; }
105	461	Node TransitionInference::getPostCondition() const { return d_post.d_this; }
106	432	Node TransitionInference::getTransitionRelation() const
107		{
108	432	return d_trans.d_this;
109		}
110
111	92	void TransitionInference::getConstantSubstitution(
112		const std::vector<Node>& vars,
113		const std::vector<Node>& disjuncts,
114		std::vector<Node>& const_var,
115		std::vector<Node>& const_subs,
116		bool reqPol)
117		{
118	454	for (const Node& d : disjuncts)
119		{
120	724	Node sn;
121	362	if (!const_var.empty())
122		{
123	181	sn = d.substitute(const_var.begin(),
124		const_var.end(),
125		const_subs.begin(),
126		const_subs.end());
127	181	sn = Rewriter::rewrite(sn);
128		}
129		else
130		{
131	181	sn = d;
132		}
133	362	bool slit_pol = sn.getKind() != NOT;
134	724	Node slit = sn.getKind() == NOT ? sn[0] : sn;
135	362	if (slit.getKind() == EQUAL && slit_pol == reqPol)
136		{
137		// check if it is a variable equality
138	260	TNode v;
139	260	Node s;
140	208	for (unsigned r = 0; r < 2; r++)
141		{
142	186	if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end())
143		{
144	108	if (!expr::hasSubterm(slit[1 - r], slit[r]))
145		{
146	108	v = slit[r];
147	108	s = slit[1 - r];
148	108	break;
149		}
150		}
151		}
152	130	if (v.isNull())
153		{
154		// solve for var
155	44	std::map<Node, Node> msum;
156	22	if (ArithMSum::getMonomialSumLit(slit, msum))
157		{
158	88	for (std::pair<const Node, Node>& m : msum)
159		{
160	66	if (std::find(vars.begin(), vars.end(), m.first) != vars.end())
161		{
162	44	Node veq_c;
163	44	Node val;
164	22	int ires = ArithMSum::isolate(m.first, msum, veq_c, val, EQUAL);
165	44	if (ires != 0 && veq_c.isNull()
166	44	&& !expr::hasSubterm(val, m.first))
167		{
168	22	v = m.first;
169	22	s = val;
170		}
171		}
172		}
173		}
174		}
175	130	if (!v.isNull())
176		{
177	260	TNode ts = s;
178	560	for (unsigned k = 0, csize = const_subs.size(); k < csize; k++)
179		{
180	430	const_subs[k] = Rewriter::rewrite(const_subs[k].substitute(v, ts));
181		}
182	260	Trace("cegqi-inv-debug2")
183	130	<< "...substitution : " << v << " -> " << s << std::endl;
184	130	const_var.push_back(v);
185	130	const_subs.push_back(s);
186		}
187		}
188		}
189	92	}
190
191	42	void TransitionInference::process(Node n, Node f)
192		{
193		// set the function
194	42	d_func = f;
195	42	process(n);
196	42	}
197
198	42	void TransitionInference::process(Node n)
199		{
200	42	NodeManager* nm = NodeManager::currentNM();
201	42	SkolemManager* sm = nm->getSkolemManager();
202	42	d_complete = true;
203	42	d_trivial = true;
204	84	std::vector<Node> n_check;
205	42	if (n.getKind() == AND)
206		{
207	120	for (const Node& nc : n)
208		{
209	89	n_check.push_back(nc);
210		}
211		}
212		else
213		{
214	11	n_check.push_back(n);
215		}
216	142	for (const Node& nn : n_check)
217		{
218	192	std::map<bool, std::map<Node, bool> > visited;
219	192	std::map<bool, Node> terms;
220	192	std::vector<Node> disjuncts;
221	200	Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn
222	100	<< std::endl;
223	105	if (!processDisjunct(nn, terms, disjuncts, visited, true))
224		{
225	5	d_complete = false;
226	5	continue;
227		}
228	95	if (terms.empty())
229		{
230	3	continue;
231		}
232	184	Node curr;
233		// The component that this disjunct contributes to, where
234		// 1 : pre-condition, -1 : post-condition, 0 : transition relation
235		int comp_num;
236	92	std::map<bool, Node>::iterator itt = terms.find(false);
237	92	if (itt != terms.end())
238		{
239	62	curr = itt->second;
240	62	if (terms.find(true) != terms.end())
241		{
242	25	comp_num = 0;
243		}
244		else
245		{
246	37	comp_num = -1;
247		}
248		}
249		else
250		{
251	30	curr = terms[true];
252	30	comp_num = 1;
253		}
254	92	Trace("cegqi-inv-debug2") << " normalize based on " << curr << std::endl;
255	184	std::vector<Node> vars;
256	184	std::vector<Node> svars;
257	92	getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts);
258	450	for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
259		{
260	358	Trace("cegqi-inv-debug2") << " apply " << disjuncts[j] << std::endl;
261	358	disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
262		vars.begin(), vars.end(), svars.begin(), svars.end()));
263	358	Trace("cegqi-inv-debug2") << " ..." << disjuncts[j] << std::endl;
264		}
265	184	std::vector<Node> const_var;
266	184	std::vector<Node> const_subs;
267	92	if (comp_num == 0)
268		{
269		// transition
270	25	Assert(terms.find(true) != terms.end());
271	50	Node next = terms[true];
272	25	next = Rewriter::rewrite(next.substitute(
273		vars.begin(), vars.end(), svars.begin(), svars.end()));
274	50	Trace("cegqi-inv-debug")
275	25	<< "transition next predicate : " << next << std::endl;
276		// make the primed variables if we have not already
277	25	if (d_prime_vars.empty())
278		{
279	139	for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; j++)
280		{
281		Node v = sm->mkDummySkolem(
282	228	"ir", next[j].getType(), "template inference rev argument");
283	114	d_prime_vars.push_back(v);
284		}
285		}
286		// normalize the other direction
287	25	Trace("cegqi-inv-debug2") << " normalize based on " << next << std::endl;
288	50	std::vector<Node> rvars;
289	50	std::vector<Node> rsvars;
290	25	getNormalizedSubstitution(next, d_prime_vars, rvars, rsvars, disjuncts);
291	25	Assert(rvars.size() == rsvars.size());
292	139	for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
293		{
294	114	Trace("cegqi-inv-debug2") << " apply " << disjuncts[j] << std::endl;
295	114	disjuncts[j] = Rewriter::rewrite(disjuncts[j].substitute(
296		rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end()));
297	114	Trace("cegqi-inv-debug2") << " ..." << disjuncts[j] << std::endl;
298		}
299	25	getConstantSubstitution(
300		d_prime_vars, disjuncts, const_var, const_subs, false);
301		}
302		else
303		{
304	67	getConstantSubstitution(d_vars, disjuncts, const_var, const_subs, false);
305		}
306	184	Node res;
307	92	if (disjuncts.empty())
308		{
309	3	res = nm->mkConst(false);
310		}
311	89	else if (disjuncts.size() == 1)
312		{
313	22	res = disjuncts[0];
314		}
315		else
316		{
317	67	res = nm->mkNode(OR, disjuncts);
318		}
319	92	if (expr::hasBoundVar(res))
320		{
321		Trace("cegqi-inv-debug2") << "...failed, free variable." << std::endl;
322		d_complete = false;
323		continue;
324		}
325	184	Trace("cegqi-inv") << "*** inferred "
326	246	<< (comp_num == 1 ? "pre"
327	154	: (comp_num == -1 ? "post" : "trans"))
328	92	<< "-condition : " << res << std::endl;
329	92	Component& c =
330		(comp_num == 1 ? d_pre : (comp_num == -1 ? d_post : d_trans));
331	92	c.d_conjuncts.push_back(res);
332	92	if (!const_var.empty())
333		{
334	50	bool has_const_eq = const_var.size() == d_vars.size();
335	100	Trace("cegqi-inv") << " with constant substitution, complete = "
336	50	<< has_const_eq << " : " << std::endl;
337	180	for (unsigned i = 0, csize = const_var.size(); i < csize; i++)
338		{
339	260	Trace("cegqi-inv") << " " << const_var[i] << " -> "
340	130	<< const_subs[i] << std::endl;
341	130	if (has_const_eq)
342		{
343	51	c.d_const_eq[res][const_var[i]] = const_subs[i];
344		}
345		}
346	100	Trace("cegqi-inv") << "...size = " << const_var.size()
347	50	<< ", #vars = " << d_vars.size() << std::endl;
348		}
349		}
350
351		// finalize the components
352	168	for (int i = -1; i <= 1; i++)
353		{
354	126	Component& c = (i == 1 ? d_pre : (i == -1 ? d_post : d_trans));
355	252	Node ret;
356	126	if (c.d_conjuncts.empty())
357		{
358	37	ret = nm->mkConst(true);
359		}
360	89	else if (c.d_conjuncts.size() == 1)
361		{
362	87	ret = c.d_conjuncts[0];
363		}
364		else
365		{
366	2	ret = nm->mkNode(AND, c.d_conjuncts);
367		}
368	126	if (i == 0 \|\| i == 1)
369		{
370		// pre-condition and transition are negated
371	84	ret = TermUtil::simpleNegate(ret);
372		}
373	126	c.d_this = ret;
374		}
375	42	}
376	117	void TransitionInference::getNormalizedSubstitution(
377		Node curr,
378		const std::vector<Node>& pvars,
379		std::vector<Node>& vars,
380		std::vector<Node>& subs,
381		std::vector<Node>& disjuncts)
382		{
383	659	for (unsigned j = 0, nchild = curr.getNumChildren(); j < nchild; j++)
384		{
385	542	if (curr[j].getKind() == BOUND_VARIABLE)
386		{
387		// if the argument is a bound variable, add to the renaming
388	501	vars.push_back(curr[j]);
389	501	subs.push_back(pvars[j]);
390		}
391		else
392		{
393		// otherwise, treat as a constraint on the variable
394		// For example, this transforms e.g. a precondition clause
395		// I( 0, 1 ) to x1 != 0 OR x2 != 1 OR I( x1, x2 ).
396	82	Node eq = curr[j].eqNode(pvars[j]);
397	41	disjuncts.push_back(eq.negate());
398		}
399		}
400	117	}
401
402	2229	bool TransitionInference::processDisjunct(
403		Node n,
404		std::map<bool, Node>& terms,
405		std::vector<Node>& disjuncts,
406		std::map<bool, std::map<Node, bool> >& visited,
407		bool topLevel)
408		{
409	2229	if (visited[topLevel].find(n) != visited[topLevel].end())
410		{
411	559	return true;
412		}
413	1670	visited[topLevel][n] = true;
414	1670	bool childTopLevel = n.getKind() == OR && topLevel;
415		// if another part mentions UF or a free variable, then fail
416	1670	bool lit_pol = n.getKind() != NOT;
417	3340	Node lit = n.getKind() == NOT ? n[0] : n;
418		// is it an application of the function-to-synthesize? Yes if we haven't
419		// encountered a function or if it matches the existing d_func.
420	3340	if (lit.getKind() == APPLY_UF
421	3340	&& (d_func.isNull() \|\| lit.getOperator() == d_func))
422		{
423	244	Node op = lit.getOperator();
424		// initialize the variables
425	122	if (d_trivial)
426		{
427	41	d_trivial = false;
428	41	d_func = op;
429	41	Trace("cegqi-inv-debug") << "Use " << op << " with args ";
430	41	NodeManager* nm = NodeManager::currentNM();
431	41	SkolemManager* sm = nm->getSkolemManager();
432	240	for (const Node& l : lit)
433		{
434		Node v =
435	398	sm->mkDummySkolem("i", l.getType(), "template inference argument");
436	199	d_vars.push_back(v);
437	199	Trace("cegqi-inv-debug") << v << " ";
438		}
439	41	Trace("cegqi-inv-debug") << std::endl;
440		}
441	122	Assert(!d_func.isNull());
442	122	if (topLevel)
443		{
444	117	if (terms.find(lit_pol) == terms.end())
445		{
446	117	terms[lit_pol] = lit;
447	117	return true;
448		}
449		else
450		{
451		Trace("cegqi-inv-debug")
452		<< "...failed, repeated inv-app : " << lit << std::endl;
453		return false;
454		}
455		}
456	10	Trace("cegqi-inv-debug")
457	5	<< "...failed, non-entailed inv-app : " << lit << std::endl;
458	5	return false;
459		}
460	1548	else if (topLevel && !childTopLevel)
461		{
462	329	disjuncts.push_back(n);
463		}
464	3668	for (const Node& nc : n)
465		{
466	2129	if (!processDisjunct(nc, terms, disjuncts, visited, childTopLevel))
467		{
468	9	return false;
469		}
470		}
471	1539	return true;
472		}
473
474	28	TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt,
475		Node loc,
476		bool fwd)
477		{
478	28	Component& c = fwd ? d_pre : d_post;
479	28	Assert(c.has(loc));
480	28	std::map<Node, std::map<Node, Node> >::iterator it = c.d_const_eq.find(loc);
481	28	if (it != c.d_const_eq.end())
482		{
483	16	std::vector<Node> next;
484	22	for (const Node& v : d_vars)
485		{
486	14	Assert(it->second.find(v) != it->second.end());
487	14	next.push_back(it->second[v]);
488	14	dt.d_curr.push_back(it->second[v]);
489		}
490	8	Trace("cegqi-inv-debug2") << "dtrace : initial increment" << std::endl;
491	8	bool ret = dt.increment(loc, next);
492	8	AlwaysAssert(ret);
493	8	return TRACE_INC_SUCCESS;
494		}
495	20	return TRACE_INC_INVALID;
496		}
497
498	424	TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt,
499		Node loc,
500		bool fwd)
501		{
502	424	Assert(d_trans.has(loc));
503		// check if it satisfies the pre/post condition
504	848	Node cc = fwd ? getPostCondition() : getPreCondition();
505	424	Assert(!cc.isNull());
506	848	Node ccr = Rewriter::rewrite(cc.substitute(
507	848	d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
508	424	if (ccr.isConst())
509		{
510	424	if (ccr.getConst<bool>() == (fwd ? false : true))
511		{
512		Trace("cegqi-inv-debug2") << "dtrace : counterexample" << std::endl;
513		return TRACE_INC_CEX;
514		}
515		}
516
517		// terminates?
518	848	Node c = getTransitionRelation();
519	424	Assert(!c.isNull());
520
521	424	Assert(d_vars.size() == dt.d_curr.size());
522	848	Node cr = Rewriter::rewrite(c.substitute(
523	848	d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
524	424	if (cr.isConst())
525		{
526	4	if (!cr.getConst<bool>())
527		{
528	4	Trace("cegqi-inv-debug2") << "dtrace : terminated" << std::endl;
529	4	return TRACE_INC_TERMINATE;
530		}
531		return TRACE_INC_INVALID;
532		}
533	420	if (!fwd)
534		{
535		// only implemented in forward direction
536		Assert(false);
537		return TRACE_INC_INVALID;
538		}
539	420	Component& cm = d_trans;
540	420	std::map<Node, std::map<Node, Node> >::iterator it = cm.d_const_eq.find(loc);
541	420	if (it == cm.d_const_eq.end())
542		{
543		return TRACE_INC_INVALID;
544		}
545	840	std::vector<Node> next;
546	1248	for (const Node& pv : d_prime_vars)
547		{
548	828	Assert(it->second.find(pv) != it->second.end());
549	1656	Node pvs = it->second[pv];
550	828	Assert(d_vars.size() == dt.d_curr.size());
551	1656	Node pvsr = Rewriter::rewrite(pvs.substitute(
552	1656	d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
553	828	next.push_back(pvsr);
554		}
555	420	if (dt.increment(loc, next))
556		{
557	420	Trace("cegqi-inv-debug2") << "dtrace : success increment" << std::endl;
558	420	return TRACE_INC_SUCCESS;
559		}
560		// looped
561		Trace("cegqi-inv-debug2") << "dtrace : looped" << std::endl;
562		return TRACE_INC_TERMINATE;
563		}
564
565	29	TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt, bool fwd)
566		{
567	29	Trace("cegqi-inv-debug2") << "Initialize trace" << std::endl;
568	29	Component& c = fwd ? d_pre : d_post;
569	29	if (c.d_conjuncts.size() == 1)
570		{
571	28	return initializeTrace(dt, c.d_conjuncts[0], fwd);
572		}
573	1	return TRACE_INC_INVALID;
574		}
575
576	424	TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt, bool fwd)
577		{
578	424	if (d_trans.d_conjuncts.size() == 1)
579		{
580	424	return incrementTrace(dt, d_trans.d_conjuncts[0], fwd);
581		}
582		return TRACE_INC_INVALID;
583		}
584
585	4	Node TransitionInference::constructFormulaTrace(DetTrace& dt) const
586		{
587	4	return dt.constructFormula(d_vars);
588		}
589
590		} // namespace quantifiers
591		} // namespace theory
592	28191	} // namespace cvc5