1 /********************* */
2 /*! \file dynamic_rewrite.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
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.\endverbatim
12 ** \brief Implementation of dynamic_rewriter
15 #include "theory/quantifiers/dynamic_rewrite.h"
17 #include "theory/rewriter.h"
20 using namespace CVC4::kind
;
24 namespace quantifiers
{
26 DynamicRewriter::DynamicRewriter(const std::string
& name
,
27 context::UserContext
* u
)
28 : d_equalityEngine(u
, "DynamicRewriter::" + name
, true), d_rewrites(u
)
30 d_equalityEngine
.addFunctionKind(kind::APPLY_UF
);
33 void DynamicRewriter::addRewrite(Node a
, Node b
)
35 Trace("dyn-rewrite") << "Dyn-Rewriter : " << a
<< " == " << b
<< std::endl
;
38 Trace("dyn-rewrite") << "...equal." << std::endl
;
42 // add to the equality engine
43 Node ai
= toInternal(a
);
44 Node bi
= toInternal(b
);
45 if (ai
.isNull() || bi
.isNull())
47 Trace("dyn-rewrite") << "...not internalizable." << std::endl
;
50 Trace("dyn-rewrite-debug") << "Internal : " << ai
<< " " << bi
<< std::endl
;
52 Trace("dyn-rewrite-debug") << "assert eq..." << std::endl
;
53 Node eq
= ai
.eqNode(bi
);
54 d_rewrites
.push_back(eq
);
55 d_equalityEngine
.assertEquality(eq
, true, eq
);
56 Assert(d_equalityEngine
.consistent());
57 Trace("dyn-rewrite-debug") << "Finished" << std::endl
;
60 bool DynamicRewriter::areEqual(Node a
, Node b
)
66 Trace("dyn-rewrite-debug") << "areEqual? : " << a
<< " " << b
<< std::endl
;
67 // add to the equality engine
68 Node ai
= toInternal(a
);
69 Node bi
= toInternal(b
);
70 if (ai
.isNull() || bi
.isNull())
72 Trace("dyn-rewrite") << "...not internalizable." << std::endl
;
75 Trace("dyn-rewrite-debug") << "internal : " << ai
<< " " << bi
<< std::endl
;
76 d_equalityEngine
.addTerm(ai
);
77 d_equalityEngine
.addTerm(bi
);
78 Trace("dyn-rewrite-debug") << "...added terms" << std::endl
;
79 return d_equalityEngine
.areEqual(ai
, bi
);
82 Node
DynamicRewriter::toInternal(Node a
)
84 std::map
<Node
, Node
>::iterator it
= d_term_to_internal
.find(a
);
85 if (it
!= d_term_to_internal
.end())
93 std::vector
<Node
> children
;
96 Node op
= a
.getOperator();
97 if (a
.getKind() != APPLY_UF
)
99 op
= d_ois_trie
[op
].getSymbol(a
);
100 // if this term involves an argument that is not of first class type,
101 // we cannot reason about it. This includes operators like str.in-re.
107 children
.push_back(op
);
109 for (const Node
& ca
: a
)
111 Node cai
= toInternal(ca
);
116 children
.push_back(cai
);
118 if (!children
.empty())
120 if (children
.size() == 1)
126 ret
= NodeManager::currentNM()->mkNode(APPLY_UF
, children
);
130 d_term_to_internal
[a
] = ret
;
131 d_internal_to_term
[ret
] = a
;
135 Node
DynamicRewriter::toExternal(Node ai
)
137 std::map
<Node
, Node
>::iterator it
= d_internal_to_term
.find(ai
);
138 if (it
!= d_internal_to_term
.end())
145 Node
DynamicRewriter::OpInternalSymTrie::getSymbol(Node n
)
147 std::vector
<TypeNode
> ctypes
;
148 for (const Node
& cn
: n
)
150 ctypes
.push_back(cn
.getType());
152 ctypes
.push_back(n
.getType());
154 OpInternalSymTrie
* curr
= this;
155 for (unsigned i
= 0, size
= ctypes
.size(); i
< size
; i
++)
157 // cannot handle certain types (e.g. regular expressions or functions)
158 if (!ctypes
[i
].isFirstClass())
162 curr
= &(curr
->d_children
[ctypes
[i
]]);
164 if (!curr
->d_sym
.isNull())
170 if (ctypes
.size() == 1)
176 utype
= NodeManager::currentNM()->mkFunctionType(ctypes
);
178 Node f
= NodeManager::currentNM()->mkSkolem(
179 "ufd", utype
, "internal op for dynamic_rewriter");
184 } /* CVC4::theory::quantifiers namespace */
185 } /* CVC4::theory namespace */
186 } /* CVC4 namespace */