Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/dynamic_rewrite.cpp	Lines:	76	89	85.4 %
Date:	2021-11-07	Branches:	162	356	45.5 %


/******************************************************************************
 * 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 "smt/env.h"
#include "theory/rewriter.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

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