summaryrefslogtreecommitdiff
path: root/src/theory/uf/theory_uf.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r--src/theory/uf/theory_uf.cpp12
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 099b56a33..6fdc969a4 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -204,21 +204,21 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
}
//--------------------------------- end standard check
-TrustNode TheoryUF::expandDefinition(Node node)
+TrustNode TheoryUF::ppRewrite(TNode node)
{
- Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : "
- << node << std::endl;
+ Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
+ << std::endl;
if( node.getKind()==kind::HO_APPLY ){
if( !options::ufHo() ){
std::stringstream ss;
ss << "Partial function applications are not supported in default mode, try --uf-ho.";
throw LogicException(ss.str());
}
- Node ret = d_ho->expandDefinition(node);
+ Node ret = d_ho->ppRewrite(node);
if (ret != node)
{
- Trace("uf-exp-def") << "TheoryUF::expandDefinition: higher-order: "
- << node << " to " << ret << std::endl;
+ Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node
+ << " to " << ret << std::endl;
return TrustNode::mkTrustRewrite(node, ret, nullptr);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback