From 522fd010b5a64574040c6e4d2a479fa0d8b569d2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 2 Sep 2021 13:06:46 -0500 Subject: [PATCH] Remove more instances of ufHo (#7087) Towards replacing that option with a logic check throughout. --- src/theory/model_manager.cpp | 2 +- src/theory/quantifiers/fmf/model_builder.cpp | 2 +- src/theory/sort_inference.cpp | 3 ++- src/theory/sort_inference.h | 7 +++++- src/theory/theory_engine.cpp | 2 +- src/theory/theory_model.cpp | 16 +++++++++----- src/theory/theory_model_builder.cpp | 17 ++++++++------- src/theory/theory_model_builder.h | 10 +++++---- src/theory/uf/ho_extension.cpp | 2 +- src/theory/uf/theory_uf.cpp | 23 ++++++++++++-------- src/theory/uf/theory_uf_rewriter.cpp | 10 ++++++--- src/theory/uf/theory_uf_rewriter.h | 3 +++ 12 files changed, 61 insertions(+), 36 deletions(-) diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index 9d25dd760..29c4bf169 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -59,7 +59,7 @@ void ModelManager::finishInit(eq::EqualityEngineNotify* notify) // not have a model builder if (d_modelBuilder == nullptr) { - d_alocModelBuilder.reset(new TheoryEngineModelBuilder); + d_alocModelBuilder.reset(new TheoryEngineModelBuilder(d_env)); d_modelBuilder = d_alocModelBuilder.get(); } // notice that the equality engine of the model has yet to be assigned. diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 1e78d103e..a331409f1 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -34,7 +34,7 @@ QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : TheoryEngineModelBuilder(), + : TheoryEngineModelBuilder(qs.getEnv()), d_addedLemmas(0), d_triedLemmas(0), d_qstate(qs), diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index cad545ca6..db2db9937 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -29,6 +29,7 @@ #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" +#include "smt/env.h" #include "theory/quantifiers/quant_util.h" #include "theory/rewriter.h" @@ -880,7 +881,7 @@ bool SortInference::isMonotonic( TypeNode tn ) { bool SortInference::isHandledApplyUf(Kind k) const { - return k == APPLY_UF && !options::ufHo(); + return k == APPLY_UF && !d_env.getLogicInfo().isHigherOrder(); } } // namespace theory diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h index 1dc7ff3c3..279be5e10 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -25,6 +25,9 @@ #include "expr/type_node.h" namespace cvc5 { + +class Env; + namespace theory { /** sort inference @@ -63,6 +66,8 @@ public: }; private: + /** Reference to the env */ + Env& d_env; /** the id count for all subsorts we have allocated */ int d_sortCount; UnionFind d_type_union_find; @@ -106,7 +111,7 @@ private: void reset(); public: - SortInference() : d_sortCount(1) {} + SortInference(Env& env) : d_env(env), d_sortCount(1) {} ~SortInference(){} /** initialize diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index db98b47fa..cd9445bb0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -264,7 +264,7 @@ TheoryEngine::TheoryEngine(Env& env) if (options::sortInference()) { - d_sortInfer.reset(new SortInference); + d_sortInfer.reset(new SortInference(env)); } d_true = NodeManager::currentNM()->mkConst(true); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 02a837899..291cd1905 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -40,7 +40,7 @@ TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels) d_enableFuncModels(enableFuncModels) { // must use function models when ufHo is enabled - Assert(d_enableFuncModels || !options::ufHo()); + Assert(d_enableFuncModels || !d_env.getLogicInfo().isHigherOrder()); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); } @@ -52,7 +52,8 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee) Assert(ee != nullptr); d_equalityEngine = ee; // The kinds we are treating as function application in congruence - d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo()); + d_equalityEngine->addFunctionKind( + kind::APPLY_UF, false, d_env.getLogicInfo().isHigherOrder()); d_equalityEngine->addFunctionKind(kind::HO_APPLY); d_equalityEngine->addFunctionKind(kind::SELECT); // d_equalityEngine->addFunctionKind(kind::STORE); @@ -293,7 +294,8 @@ Node TheoryModel::getModelValue(TNode n) const // return the representative of the term in the equality engine, if it exists TypeNode t = ret.getType(); bool eeHasTerm; - if (!options::ufHo() && (t.isFunction() || t.isPredicate())) + if (!d_env.getLogicInfo().isHigherOrder() + && (t.isFunction() || t.isPredicate())) { // functions are in the equality engine, but *not* as first-class members // when higher-order is disabled. In this case, we cannot query @@ -692,7 +694,8 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl; Assert(d_uf_models.find(f) == d_uf_models.end()); - if( options::ufHo() ){ + if (d_env.getLogicInfo().isHigherOrder()) + { //we must rewrite the function value since the definition needs to be a constant value f_def = Rewriter::rewrite( f_def ); Trace("model-builder-debug") @@ -705,7 +708,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { d_uf_models[f] = f_def; } - if (options::ufHo() && d_equalityEngine->hasTerm(f)) + if (d_env.getLogicInfo().isHigherOrder() && d_equalityEngine->hasTerm(f)) { Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl; // assign to representative if higher-order @@ -740,7 +743,8 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { Assert(d_env.getTopLevelSubstitutions().apply(n) == n); if( !hasAssignedFunctionDefinition( n ) ){ Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl; - if( options::ufHo() ){ + if (d_env.getLogicInfo().isHigherOrder()) + { // if in higher-order mode, assign function definitions modulo equality Node r = getRepresentative( n ); std::map< Node, Node >::iterator itf = func_to_rep.find( r ); diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index e43cb26c8..2acbe2388 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -21,6 +21,7 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "smt/env.h" #include "theory/rewriter.h" #include "theory/uf/theory_uf_model.h" @@ -31,6 +32,8 @@ using namespace cvc5::context; namespace cvc5 { namespace theory { +TheoryEngineModelBuilder::TheoryEngineModelBuilder(Env& env) : d_env(env) {} + void TheoryEngineModelBuilder::Assigner::initialize( TypeNode tn, TypeEnumeratorProperties* tep, const std::vector& aes) { @@ -64,8 +67,6 @@ Node TheoryEngineModelBuilder::Assigner::getNextAssignment() return n; } -TheoryEngineModelBuilder::TheoryEngineModelBuilder() {} - Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r) { eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine); @@ -129,7 +130,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) { // selectors are always assignable (where we guarantee that they are not // evaluatable here) - if (!options::ufHo()) + if (!d_env.getLogicInfo().isHigherOrder()) { Assert(!n.getType().isFunction()); return true; @@ -151,7 +152,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) else { // non-function variables, and fully applied functions - if (!options::ufHo()) + if (!d_env.getLogicInfo().isHigherOrder()) { // no functions exist, all functions are fully applied Assert(n.getKind() != kind::HO_APPLY); @@ -1228,7 +1229,7 @@ bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m) void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) { - Assert(!options::ufHo()); + Assert(!d_env.getLogicInfo().isHigherOrder()); uf::UfModelTree ufmt(f); Node default_v; for (size_t i = 0; i < m->d_uf_terms[f].size(); i++) @@ -1273,7 +1274,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) { - Assert(options::ufHo()); + Assert(d_env.getLogicInfo().isHigherOrder()); TypeNode type = f.getType(); std::vector argTypes = type.getArgTypes(); std::vector args; @@ -1397,7 +1398,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) Trace("model-builder") << "Assigning function values..." << std::endl; std::vector funcs_to_assign = m->getFunctionsToAssign(); - if (options::ufHo()) + if (d_env.getLogicInfo().isHigherOrder()) { // sort based on type size if higher-order Trace("model-builder") << "Sort functions by type..." << std::endl; @@ -1424,7 +1425,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) Trace("model-builder") << " Function #" << k << " is " << f << std::endl; // std::map< Node, std::vector< Node > >::iterator itht = // m->d_ho_uf_terms.find( f ); - if (!options::ufHo()) + if (!d_env.getLogicInfo().isHigherOrder()) { Trace("model-builder") << " Assign function value for " << f << " based on APPLY_UF" << std::endl; diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 195ba9e0f..71458a913 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -25,7 +25,7 @@ namespace cvc5 { -class TheoryEngine; +class Env; namespace theory { @@ -48,7 +48,7 @@ class TheoryEngineModelBuilder typedef std::unordered_set NodeSet; public: - TheoryEngineModelBuilder(); + TheoryEngineModelBuilder(Env& env); virtual ~TheoryEngineModelBuilder() {} /** * Should be called only on models m after they have been prepared @@ -207,8 +207,8 @@ class TheoryEngineModelBuilder * Assign all unassigned functions in the model m (those returned by * TheoryModel::getFunctionsToAssign), * using the two functions above. Currently: - * If ufHo is disabled, we call assignFunction for all functions. - * If ufHo is enabled, we call assignHoFunction. + * If HO logic is disabled, we call assignFunction for all functions. + * If HO logic is enabled, we call assignHoFunction. */ void assignFunctions(TheoryModel* m); @@ -315,6 +315,8 @@ class TheoryEngineModelBuilder Node v, std::map& visited); //---------------------------------end for debugging finite model finding + /** Reference to the env */ + Env& d_env; }; /* class TheoryEngineModelBuilder */ diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 853ae719b..af2bf4a3b 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -436,7 +436,7 @@ bool HoExtension::collectModelInfoHo(TheoryModel* m, for (std::set::iterator it = termSet.begin(); it != termSet.end(); ++it) { Node n = *it; - // For model-building with ufHo, we require that APPLY_UF is always + // For model-building with higher-order, we require that APPLY_UF is always // expanded to HO_APPLY. That is, we always expand to a fully applicative // encoding during model construction. if (!collectModelInfoHoTerm(n, m)) diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3525786d5..9c506f2ac 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -49,6 +49,7 @@ TheoryUF::TheoryUF(Env& env, d_ho(nullptr), d_functionsTerms(getSatContext()), d_symb(getUserContext(), instanceName), + d_rewriter(env.getLogicInfo().isHigherOrder()), d_state(env, valuation), d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false), d_notify(d_im, *this) @@ -94,8 +95,9 @@ void TheoryUF::finishInit() { d_thss.reset(new CardinalityExtension(d_state, d_im, this)); } // The kinds we are treating as function application in congruence - d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo()); - if (options::ufHo()) + d_equalityEngine->addFunctionKind( + kind::APPLY_UF, false, getLogicInfo().isHigherOrder()); + if (getLogicInfo().isHigherOrder()) { d_equalityEngine->addFunctionKind(kind::HO_APPLY); d_ho.reset(new HoExtension(d_state, d_im)); @@ -146,7 +148,7 @@ void TheoryUF::postCheck(Effort level) // check with the higher-order extension at full effort if (!d_state.isInConflict() && fullEffort(level)) { - if (options::ufHo()) + if (getLogicInfo().isHigherOrder()) { d_ho->check(); } @@ -169,7 +171,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) { case kind::EQUAL: { - if (options::ufHo() && options::ufHoExt()) + if (getLogicInfo().isHigherOrder() && options::ufHoExt()) { if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction()) { @@ -212,7 +214,8 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector& lems) Kind k = node.getKind(); if (k == kind::HO_APPLY) { - if( !options::ufHo() ){ + if (!getLogicInfo().isHigherOrder()) + { std::stringstream ss; ss << "Partial function applications are only supported with " "higher-order logic. Try adding the logic prefix HO_."; @@ -230,7 +233,8 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector& lems) { // check for higher-order // logic exception if higher-order is not enabled - if (isHigherOrderType(node.getOperator().getType()) && !options::ufHo()) + if (isHigherOrderType(node.getOperator().getType()) + && !getLogicInfo().isHigherOrder()) { std::stringstream ss; ss << "UF received an application whose operator has higher-order type " @@ -252,8 +256,8 @@ void TheoryUF::preRegisterTerm(TNode node) } // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order - //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() ); - Assert(node.getKind() != kind::HO_APPLY || options::ufHo()); + Assert(node.getKind() != kind::HO_APPLY + || getLogicInfo().isHigherOrder()); Kind k = node.getKind(); switch (k) @@ -314,7 +318,8 @@ TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); } bool TheoryUF::collectModelValues(TheoryModel* m, const std::set& termSet) { - if( options::ufHo() ){ + if (getLogicInfo().isHigherOrder()) + { // must add extensionality disequalities for all pairs of (non-disequal) // function equivalence classes. if (!d_ho->collectModelInfoHo(m, termSet)) diff --git a/src/theory/uf/theory_uf_rewriter.cpp b/src/theory/uf/theory_uf_rewriter.cpp index 082fe349e..f4bedb4b8 100644 --- a/src/theory/uf/theory_uf_rewriter.cpp +++ b/src/theory/uf/theory_uf_rewriter.cpp @@ -16,7 +16,6 @@ #include "theory/uf/theory_uf_rewriter.h" #include "expr/node_algorithm.h" -#include "options/uf_options.h" #include "theory/rewriter.h" #include "theory/substitutions.h" @@ -24,6 +23,11 @@ namespace cvc5 { namespace theory { namespace uf { +TheoryUfRewriter::TheoryUfRewriter(bool isHigherOrder) + : d_isHigherOrder(isHigherOrder) +{ +} + RewriteResponse TheoryUfRewriter::postRewrite(TNode node) { if (node.getKind() == kind::EQUAL) @@ -56,7 +60,7 @@ RewriteResponse TheoryUfRewriter::postRewrite(TNode node) Node ret; // build capture-avoiding substitution since in HOL shadowing may have // been introduced - if (options::ufHo()) + if (d_isHigherOrder) { std::vector vars; std::vector subs; @@ -119,7 +123,7 @@ RewriteResponse TheoryUfRewriter::postRewrite(TNode node) // build capture-avoiding substitution since in HOL shadowing may have // been introduced - if (options::ufHo()) + if (d_isHigherOrder) { Node arg = Rewriter::rewrite(node[1]); Node var = node[0][0][0]; diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 23576b7a1..dfa797f71 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -34,6 +34,7 @@ namespace uf { class TheoryUfRewriter : public TheoryRewriter { public: + TheoryUfRewriter(bool isHigherOrder = false); RewriteResponse postRewrite(TNode node) override; RewriteResponse preRewrite(TNode node) override; @@ -61,6 +62,8 @@ class TheoryUfRewriter : public TheoryRewriter * Then, f and g can be used as APPLY_UF operators, but (ite C f g), (lambda x1. (f x1)) as well as the variable x above are not. */ static bool canUseAsApplyUfOperator(TNode n); + /** Is the logic higher-order? */ + bool d_isHigherOrder; }; /* class TheoryUfRewriter */ } // namespace uf -- 2.30.2