diff options
| -rw-r--r-- | src/theory/uf/ho_extension.cpp | 4 | ||||
| -rw-r--r-- | src/theory/uf/ho_extension.h | 4 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 12 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.h | 2 | ||||
| -rw-r--r-- | test/regress/regress1/ho/NUM925^1.p | 2 | ||||
| -rw-r--r-- | test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress2/ho/involved_parsing_ALG248^3.p | 2 |
7 files changed, 14 insertions, 14 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index d7de0a025..66bcbc76f 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -36,14 +36,14 @@ HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im) d_true = NodeManager::currentNM()->mkConst(true); } -Node HoExtension::expandDefinition(Node node) +Node HoExtension::ppRewrite(Node node) { // convert HO_APPLY to APPLY_UF if fully applied if (node[0].getType().getNumChildren() == 2) { Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; Node ret = getApplyUfForHoApply(node); - Trace("uf-ho") << "uf-ho : expandDefinition : " << node << " to " << ret + Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret << std::endl; return ret; } diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index fa9c5c612..0e82dbda6 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -54,7 +54,7 @@ class HoExtension public: HoExtension(TheoryState& state, TheoryInferenceManager& im); - /** expand definition + /** ppRewrite * * This returns the expanded form of node. * @@ -63,7 +63,7 @@ class HoExtension * function variables for function heads that are not variables via the * getApplyUfForHoApply method below. */ - Node expandDefinition(Node node); + Node ppRewrite(Node node); /** check higher order * 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); } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 4a63d9584..3f76919eb 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -142,7 +142,7 @@ private: bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; - TrustNode expandDefinition(Node node) override; + TrustNode ppRewrite(TNode node) override; void preRegisterTerm(TNode term) override; TrustNode explain(TNode n) override; diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p index d2977ddb8..e162a63a4 100644 --- a/test/regress/regress1/ho/NUM925^1.p +++ b/test/regress/regress1/ho/NUM925^1.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho +% COMMAND-LINE: --uf-ho --ho-elim % EXPECT: % SZS status Theorem for NUM925^1 %------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 index edb55d756..313ff68a1 100644 --- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 +++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models +; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models --ho-elim ; EXPECT: unsat (set-logic ALL) diff --git a/test/regress/regress2/ho/involved_parsing_ALG248^3.p b/test/regress/regress2/ho/involved_parsing_ALG248^3.p index 5ad693629..d0577dd1f 100644 --- a/test/regress/regress2/ho/involved_parsing_ALG248^3.p +++ b/test/regress/regress2/ho/involved_parsing_ALG248^3.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho +% COMMAND-LINE: --uf-ho --ho-elim % EXPECT: % SZS status Theorem for involved_parsing_ALG248^3 %------------------------------------------------------------------------------ |