Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/dynamic_rewrite.cpp	Lines:	76	89	85.4 %
Date:	2021-05-24	Branches:	162	358	45.3 %


/******************************************************************************
 * 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 dynamic_rewriter.
 */

#include "theory/quantifiers/dynamic_rewrite.h"

#include "expr/skolem_manager.h"
#include "theory/rewriter.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

DynamicRewriter::DynamicRewriter(const std::string& name,
                                 context::UserContext* u)
    : d_equalityEngine(u, "DynamicRewriter::" + name, true), d_rewrites(u)
{
  d_equalityEngine.addFunctionKind(kind::APPLY_UF);
}

void DynamicRewriter::addRewrite(Node a, Node b)
{
  Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl;
  if (a == b)
  {
    Trace("dyn-rewrite") << "...equal." << std::endl;
    return;
  }

  // add to the equality engine
  Node ai = toInternal(a);
  Node bi = toInternal(b);
  if (ai.isNull() || bi.isNull())
  {
    Trace("dyn-rewrite") << "...not internalizable." << std::endl;
    return;
  }
  Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl;

  Trace("dyn-rewrite-debug") << "assert eq..." << std::endl;
  Node eq = ai.eqNode(bi);
  d_rewrites.push_back(eq);
  d_equalityEngine.assertEquality(eq, true, eq);
  Assert(d_equalityEngine.consistent());
  Trace("dyn-rewrite-debug") << "Finished" << std::endl;
}

bool DynamicRewriter::areEqual(Node a, Node b)
{
  if (a == b)
  {
    return true;
  }
  Trace("dyn-rewrite-debug") << "areEqual? : " << a << " " << b << std::endl;
  // add to the equality engine
  Node ai = toInternal(a);
  Node bi = toInternal(b);
  if (ai.isNull() || bi.isNull())
  {
    Trace("dyn-rewrite") << "...not internalizable." << std::endl;
    return false;
  }
  Trace("dyn-rewrite-debug") << "internal : " << ai << " " << bi << std::endl;
  d_equalityEngine.addTerm(ai);
  d_equalityEngine.addTerm(bi);
  Trace("dyn-rewrite-debug") << "...added terms" << std::endl;
  return d_equalityEngine.areEqual(ai, bi);
}

Node DynamicRewriter::toInternal(Node a)
{
  std::map<Node, Node>::iterator it = d_term_to_internal.find(a);
  if (it != d_term_to_internal.end())
  {
    return it->second;
  }
  Node ret = a;

  if (!a.isVar())
  {
    std::vector<Node> children;
    if (a.hasOperator())
    {
      Node op = a.getOperator();
      if (a.getKind() != APPLY_UF)
      {
        op = d_ois_trie[op].getSymbol(a);
        // if this term involves an argument that is not of first class type,
        // we cannot reason about it. This includes operators like str.in-re.
        if (op.isNull())
        {
          return Node::null();
        }
      }
      children.push_back(op);
    }
    for (const Node& ca : a)
    {
      Node cai = toInternal(ca);
      if (cai.isNull())
      {
        return Node::null();
      }
      children.push_back(cai);
    }
    if (!children.empty())
    {
      if (children.size() == 1)
      {
        ret = children[0];
      }
      else
      {
        ret = NodeManager::currentNM()->mkNode(APPLY_UF, children);
      }
    }
  }
  d_term_to_internal[a] = ret;
  d_internal_to_term[ret] = a;
  return ret;
}

Node DynamicRewriter::toExternal(Node ai)
{
  std::map<Node, Node>::iterator it = d_internal_to_term.find(ai);
  if (it != d_internal_to_term.end())
  {
    return it->second;
  }
  return Node::null();
}

Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  std::vector<TypeNode> ctypes;
  for (const Node& cn : n)
  {
    ctypes.push_back(cn.getType());
  }
  ctypes.push_back(n.getType());

  OpInternalSymTrie* curr = this;
  for (unsigned i = 0, size = ctypes.size(); i < size; i++)
  {
    // cannot handle certain types (e.g. regular expressions or functions)
    if (!ctypes[i].isFirstClass())
    {
      return Node::null();
    }
    curr = &(curr->d_children[ctypes[i]]);
  }
  if (!curr->d_sym.isNull())
  {
    return curr->d_sym;
  }
  // make UF operator
  TypeNode utype;
  if (ctypes.size() == 1)
  {
    utype = ctypes[0];
  }
  else
  {
    utype = nm->mkFunctionType(ctypes);
  }
  Node f = sm->mkDummySkolem("ufd", utype, "internal op for dynamic_rewriter");
  curr->d_sym = f;
  return f;
}

}  // 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 dynamic_rewriter.
14		*/
15
16		#include "theory/quantifiers/dynamic_rewrite.h"
17
18		#include "expr/skolem_manager.h"
19		#include "theory/rewriter.h"
20
21		using namespace std;
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28	7	DynamicRewriter::DynamicRewriter(const std::string& name,
29	7	context::UserContext* u)
30	7	: d_equalityEngine(u, "DynamicRewriter::" + name, true), d_rewrites(u)
31		{
32	7	d_equalityEngine.addFunctionKind(kind::APPLY_UF);
33	7	}
34
35	105	void DynamicRewriter::addRewrite(Node a, Node b)
36		{
37	105	Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl;
38	105	if (a == b)
39		{
40		Trace("dyn-rewrite") << "...equal." << std::endl;
41		return;
42		}
43
44		// add to the equality engine
45	210	Node ai = toInternal(a);
46	210	Node bi = toInternal(b);
47	105	if (ai.isNull() \|\| bi.isNull())
48		{
49		Trace("dyn-rewrite") << "...not internalizable." << std::endl;
50		return;
51		}
52	105	Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl;
53
54	105	Trace("dyn-rewrite-debug") << "assert eq..." << std::endl;
55	210	Node eq = ai.eqNode(bi);
56	105	d_rewrites.push_back(eq);
57	105	d_equalityEngine.assertEquality(eq, true, eq);
58	105	Assert(d_equalityEngine.consistent());
59	105	Trace("dyn-rewrite-debug") << "Finished" << std::endl;
60		}
61
62	802	bool DynamicRewriter::areEqual(Node a, Node b)
63		{
64	802	if (a == b)
65		{
66		return true;
67		}
68	802	Trace("dyn-rewrite-debug") << "areEqual? : " << a << " " << b << std::endl;
69		// add to the equality engine
70	1604	Node ai = toInternal(a);
71	1604	Node bi = toInternal(b);
72	802	if (ai.isNull() \|\| bi.isNull())
73		{
74		Trace("dyn-rewrite") << "...not internalizable." << std::endl;
75		return false;
76		}
77	802	Trace("dyn-rewrite-debug") << "internal : " << ai << " " << bi << std::endl;
78	802	d_equalityEngine.addTerm(ai);
79	802	d_equalityEngine.addTerm(bi);
80	802	Trace("dyn-rewrite-debug") << "...added terms" << std::endl;
81	802	return d_equalityEngine.areEqual(ai, bi);
82		}
83
84	3988	Node DynamicRewriter::toInternal(Node a)
85		{
86	3988	std::map<Node, Node>::iterator it = d_term_to_internal.find(a);
87	3988	if (it != d_term_to_internal.end())
88		{
89	3013	return it->second;
90		}
91	1950	Node ret = a;
92
93	975	if (!a.isVar())
94		{
95	1932	std::vector<Node> children;
96	966	if (a.hasOperator())
97		{
98	1912	Node op = a.getOperator();
99	956	if (a.getKind() != APPLY_UF)
100		{
101	956	op = d_ois_trie[op].getSymbol(a);
102		// if this term involves an argument that is not of first class type,
103		// we cannot reason about it. This includes operators like str.in-re.
104	956	if (op.isNull())
105		{
106		return Node::null();
107		}
108		}
109	956	children.push_back(op);
110		}
111	2873	for (const Node& ca : a)
112		{
113	3814	Node cai = toInternal(ca);
114	1907	if (cai.isNull())
115		{
116		return Node::null();
117		}
118	1907	children.push_back(cai);
119		}
120	966	if (!children.empty())
121		{
122	956	if (children.size() == 1)
123		{
124		ret = children[0];
125		}
126		else
127		{
128	956	ret = NodeManager::currentNM()->mkNode(APPLY_UF, children);
129		}
130		}
131		}
132	975	d_term_to_internal[a] = ret;
133	975	d_internal_to_term[ret] = a;
134	975	return ret;
135		}
136
137	244	Node DynamicRewriter::toExternal(Node ai)
138		{
139	244	std::map<Node, Node>::iterator it = d_internal_to_term.find(ai);
140	244	if (it != d_internal_to_term.end())
141		{
142	244	return it->second;
143		}
144		return Node::null();
145		}
146
147	956	Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
148		{
149	956	NodeManager* nm = NodeManager::currentNM();
150	956	SkolemManager* sm = nm->getSkolemManager();
151	1912	std::vector<TypeNode> ctypes;
152	2863	for (const Node& cn : n)
153		{
154	1907	ctypes.push_back(cn.getType());
155		}
156	956	ctypes.push_back(n.getType());
157
158	956	OpInternalSymTrie* curr = this;
159	3819	for (unsigned i = 0, size = ctypes.size(); i < size; i++)
160		{
161		// cannot handle certain types (e.g. regular expressions or functions)
162	2863	if (!ctypes[i].isFirstClass())
163		{
164		return Node::null();
165		}
166	2863	curr = &(curr->d_children[ctypes[i]]);
167		}
168	956	if (!curr->d_sym.isNull())
169		{
170	928	return curr->d_sym;
171		}
172		// make UF operator
173	56	TypeNode utype;
174	28	if (ctypes.size() == 1)
175		{
176		utype = ctypes[0];
177		}
178		else
179		{
180	28	utype = nm->mkFunctionType(ctypes);
181		}
182	56	Node f = sm->mkDummySkolem("ufd", utype, "internal op for dynamic_rewriter");
183	28	curr->d_sym = f;
184	28	return f;
185		}
186
187		} // namespace quantifiers
188		} // namespace theory
189	28191	} // namespace cvc5