Remove more instances of ufHo (#7087)

Towards replacing that option with a logic check throughout.

diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 9d25dd76043663cd23aa5c9fcf4fa8e3183fc1f6..29c4bf1699602e4cf4245ee0a2f2fe3129982fac 100644 (file)
--- 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 1e78d103ef421a41524624e383dcebe7fd9f3077..a331409f118ae93a4ab90a25ebf46d46cd033ac4 100644 (file)
--- 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 cad545ca628fc3e82292fce017d8b4d6a13646ae..db2db9937e486cbec86863d840f208f427803929 100644 (file)
--- 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 1dc7ff3c36ec94c357b50e4bf073b1873d288ae4..279be5e10b691c696ba2e31ff32de3bd9132d282 100644 (file)
--- 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 db98b47fa8befbcce44ddedc217b908fd58c6868..cd9445bb0a7131b165fb294a90eb21574bcbe033 100644 (file)
--- 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<bool>(true);

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 02a83789910900115c24b8ceac0d426b5ecffe57..291cd1905b1a861a53cf304af4d839956db656e5 100644 (file)
--- 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 e43cb26c899c3e6066b848c8c6d1e184d056eb18..2acbe2388c29a635ac40936cd0e8c613b1bb9f0e 100644 (file)
--- 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<Node>& 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<TypeNode> argTypes = type.getArgTypes();
   std::vector<Node> args;
@@ -1397,7 +1398,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
   Trace("model-builder") << "Assigning function values..." << std::endl;
   std::vector<Node> 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 195ba9e0f5665a6fae95cc20af23aee275156b11..71458a913df24ccf845fccc5f7e1c36775d71353 100644 (file)
--- 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<Node> 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<Node, bool>& 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 853ae719b2435db1b2ed5970b1b21396fabe301d..af2bf4a3b307b146b2ac8e7534c138b4c3faca5b 100644 (file)
--- 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<Node>::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 3525786d5a3fdffdbfff2b126f00618d613cc2f4..9c506f2acf7e75eaa08e92242fd744f5190765d5 100644 (file)
--- 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<SkolemLemma>& 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<SkolemLemma>& 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<Node>& 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 082fe349eea0ab6203e402eb9c5524a6efb3dd0e..f4bedb4b840cecce17844a9ef7780815e6e0e3ba 100644 (file)
--- 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<Node> vars;
         std::vector<Node> 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 23576b7a1cf70841fe7afd24b4d09c9a576696dc..dfa797f71d1eafea2a259c7d05362b2bac8bf4fa 100644 (file)
--- 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