Initialize the rewriter based on safe-options (cvc5#11300)

Makes it so that the floating points, bags, separation logic and finite
field theories do not provide a rewriter when they are disabled due to
`--safe-options`.

Makes it so that sets does not rewrite experimental arithmetic, set
cardinality or relation terms when their corresponding extensions are
disabled. Also makes arith operator elimination not reduce experimental
arithmetic terms when `arith-exp` is false.

src/theory/arith/arith_rewriter.cpp

@@ -48,13 +48,16 @@ namespace cvc5::internal {
 namespace theory {
 namespace arith {
 
-ArithRewriter::ArithRewriter(NodeManager* nm, OperatorElim& oe)
-    : TheoryRewriter(nm), d_opElim(oe)
+ArithRewriter::ArithRewriter(NodeManager* nm,
+                             OperatorElim& oe,
+                             bool expertEnabled)
+    : TheoryRewriter(nm), d_opElim(oe), d_expertEnabled(expertEnabled)
 {
   registerProofRewriteRule(ProofRewriteRule::ARITH_POW_ELIM,
                            TheoryRewriteCtx::PRE_DSL);
   registerProofRewriteRule(ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL,
                            TheoryRewriteCtx::DSL_SUBCALL);
+
   // we don't register ARITH_STRING_PRED_ENTAIL or
   // ARITH_STRING_PRED_SAFE_APPROX, as these are subsumed by
   // MACRO_ARITH_STRING_PRED_ENTAIL.
@@ -327,6 +330,11 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
       case Kind::POW2: return RewriteResponse(REWRITE_DONE, t);
       case Kind::INTS_ISPOW2: return RewriteResponse(REWRITE_DONE, t);
       case Kind::INTS_LOG2: return RewriteResponse(REWRITE_DONE, t);
+      case Kind::INTS_DIVISION:
+      case Kind::INTS_MODULUS: return rewriteIntsDivMod(t, true);
+      case Kind::INTS_DIVISION_TOTAL:
+      case Kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, true);
+      case Kind::ABS: return rewriteAbs(t);
       case Kind::EXPONENTIAL:
       case Kind::SINE:
       case Kind::COSINE:
@@ -340,12 +348,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
       case Kind::ARCCOSECANT:
       case Kind::ARCSECANT:
       case Kind::ARCCOTANGENT:
-      case Kind::SQRT: return preRewriteTranscendental(t);
-      case Kind::INTS_DIVISION:
-      case Kind::INTS_MODULUS: return rewriteIntsDivMod(t, true);
-      case Kind::INTS_DIVISION_TOTAL:
-      case Kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, true);
-      case Kind::ABS: return rewriteAbs(t);
+      case Kind::SQRT:
       case Kind::IS_INTEGER:
       case Kind::TO_INTEGER:
       case Kind::TO_REAL:
@@ -374,24 +377,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       case Kind::ADD: return postRewritePlus(t);
       case Kind::MULT:
       case Kind::NONLINEAR_MULT: return postRewriteMult(t);
-      case Kind::IAND: return postRewriteIAnd(t);
-      case Kind::POW2: return postRewritePow2(t);
       case Kind::INTS_ISPOW2: return postRewriteIntsIsPow2(t);
       case Kind::INTS_LOG2: return postRewriteIntsLog2(t);
-      case Kind::EXPONENTIAL:
-      case Kind::SINE:
-      case Kind::COSINE:
-      case Kind::TANGENT:
-      case Kind::COSECANT:
-      case Kind::SECANT:
-      case Kind::COTANGENT:
-      case Kind::ARCSINE:
-      case Kind::ARCCOSINE:
-      case Kind::ARCTANGENT:
-      case Kind::ARCCOSECANT:
-      case Kind::ARCSECANT:
-      case Kind::ARCCOTANGENT:
-      case Kind::SQRT: return postRewriteTranscendental(t);
       case Kind::INTS_DIVISION:
       case Kind::INTS_MODULUS: return rewriteIntsDivMod(t, false);
       case Kind::INTS_DIVISION_TOTAL:
@@ -409,10 +396,54 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
         return RewriteResponse(REWRITE_DONE, t);
       }
       case Kind::PI: return RewriteResponse(REWRITE_DONE, t);
+      // expert cases
+      case Kind::EXPONENTIAL:
+      case Kind::SINE:
+      case Kind::COSINE:
+      case Kind::TANGENT:
+      case Kind::COSECANT:
+      case Kind::SECANT:
+      case Kind::COTANGENT:
+      case Kind::ARCSINE:
+      case Kind::ARCCOSINE:
+      case Kind::ARCTANGENT:
+      case Kind::ARCCOSECANT:
+      case Kind::ARCSECANT:
+      case Kind::ARCCOTANGENT:
+      case Kind::SQRT:
+      case Kind::IAND:
+      case Kind::POW2: return postRewriteExpert(t);
       default: Unreachable();
     }
   }
 }
+RewriteResponse ArithRewriter::postRewriteExpert(TNode t)
+{
+  if (!d_expertEnabled)
+  {
+    return RewriteResponse(REWRITE_DONE, t);
+  }
+  switch (t.getKind())
+  {
+    case Kind::EXPONENTIAL:
+    case Kind::SINE:
+    case Kind::COSINE:
+    case Kind::TANGENT:
+    case Kind::COSECANT:
+    case Kind::SECANT:
+    case Kind::COTANGENT:
+    case Kind::ARCSINE:
+    case Kind::ARCCOSINE:
+    case Kind::ARCTANGENT:
+    case Kind::ARCCOSECANT:
+    case Kind::ARCSECANT:
+    case Kind::ARCCOTANGENT:
+    case Kind::SQRT: return postRewriteTranscendental(t);
+    case Kind::IAND: return postRewriteIAnd(t);
+    case Kind::POW2: return postRewritePow2(t);
+    default: Unreachable();
+  }
+}
 
 RewriteResponse ArithRewriter::rewriteRAN(TNode t)
 {
@@ -865,16 +896,19 @@ RewriteResponse ArithRewriter::rewriteExtIntegerOp(TNode t)
     Node ret = isPred ? nm->mkConst(true) : Node(t[0]);
     return returnRewrite(t, ret, Rewrite::INT_EXT_INT);
   }
-  if (t[0].getKind() == Kind::PI)
-  {
-    Node ret = isPred ? nm->mkConst(false) : nm->mkConstInt(Rational(3));
-    return returnRewrite(t, ret, Rewrite::INT_EXT_PI);
-  }
-  else if (t[0].getKind() == Kind::TO_REAL)
+  if (t[0].getKind() == Kind::TO_REAL)
   {
     Node ret = nm->mkNode(t.getKind(), t[0][0]);
     return returnRewrite(t, ret, Rewrite::INT_EXT_TO_REAL);
   }
+  if (d_expertEnabled)
+  {
+    if (t[0].getKind() == Kind::PI)
+    {
+      Node ret = isPred ? nm->mkConst(false) : nm->mkConstInt(Rational(3));
+      return returnRewrite(t, ret, Rewrite::INT_EXT_PI);
+    }
+  }
   return RewriteResponse(REWRITE_DONE, t);
 }
 
@@ -986,11 +1020,6 @@ RewriteResponse ArithRewriter::postRewriteIntsLog2(TNode t)
   return RewriteResponse(REWRITE_DONE, t);
 }
 
-RewriteResponse ArithRewriter::preRewriteTranscendental(TNode t)
-{
-  return RewriteResponse(REWRITE_DONE, t);
-}
-
 RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t)
 {
   Trace("arith-tf-rewrite")

src/theory/arith/arith_rewriter.h

@@ -33,7 +33,7 @@ class OperatorElim;
 class ArithRewriter : public TheoryRewriter
 {
  public:
-  ArithRewriter(NodeManager* nm, OperatorElim& oe);
+  ArithRewriter(NodeManager* nm, OperatorElim& oe, bool expertEnabled = true);
   RewriteResponse preRewrite(TNode n) override;
   RewriteResponse postRewrite(TNode n) override;
   /**
@@ -68,6 +68,9 @@ class ArithRewriter : public TheoryRewriter
   /** postRewrite for terms */
   RewriteResponse postRewriteTerm(TNode t);
 
+  /** Post-rewrites that are only available in expert mode */
+  RewriteResponse postRewriteExpert(TNode t);
+
   /** rewrite real algebraic numbers */
   RewriteResponse rewriteRAN(TNode t);
   /** rewrite variables */
@@ -108,8 +111,6 @@ class ArithRewriter : public TheoryRewriter
   /** postRewrite INTS_LOG2 */
   RewriteResponse postRewriteIntsLog2(TNode t);
 
-  /** preRewrite transcendental functions */
-  RewriteResponse preRewriteTranscendental(TNode t);
   /** postRewrite transcendental functions */
   RewriteResponse postRewriteTranscendental(TNode t);
 
@@ -127,6 +128,8 @@ class ArithRewriter : public TheoryRewriter
   Node rewriteIneqToBv(Kind k, const rewriter::Sum& sum, const Node& ineq);
   /** The operator elimination utility */
   OperatorElim& d_opElim;
+  /** Whether we permit reasoning about expert extensions of arithmetic */
+  bool d_expertEnabled;
 }; /* class ArithRewriter */
 
 }  // namespace arith

src/theory/arith/arith_utilities.cpp

@@ -120,10 +120,26 @@ Node mkOne(const TypeNode& tn, bool isNeg)
 
 bool isTranscendentalKind(Kind k)
 {
-  // many operators are eliminated during rewriting
-  Assert(k != Kind::TANGENT && k != Kind::COSINE && k != Kind::COSECANT
-         && k != Kind::SECANT && k != Kind::COTANGENT);
-  return k == Kind::EXPONENTIAL || k == Kind::SINE || k == Kind::PI;
+  switch (k)
+  {
+    case Kind::PI:
+    case Kind::EXPONENTIAL:
+    case Kind::SINE:
+    case Kind::COSINE:
+    case Kind::TANGENT:
+    case Kind::COSECANT:
+    case Kind::SECANT:
+    case Kind::COTANGENT:
+    case Kind::ARCSINE:
+    case Kind::ARCCOSINE:
+    case Kind::ARCTANGENT:
+    case Kind::ARCCOSECANT:
+    case Kind::ARCSECANT:
+    case Kind::ARCCOTANGENT:
+    case Kind::SQRT: return true;
+    default: break;
+  }
+  return false;
 }
 
 Node getApproximateConstant(Node c, bool isLower, unsigned prec)

src/theory/arith/theory_arith.cpp

@@ -50,7 +50,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
       d_nonlinearExtension(nullptr),
       d_opElim(d_env),
       d_arithPreproc(env, d_im, d_opElim),
-      d_rewriter(nodeManager(), d_opElim),
+      d_rewriter(nodeManager(), d_opElim, options().arith.arithExp),
       d_arithModelCacheSet(false),
       d_checker(nodeManager())
 {

src/theory/bags/theory_bags.cpp

@@ -52,7 +52,14 @@ TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
 
 TheoryBags::~TheoryBags() {}
 
-TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
+TheoryRewriter* TheoryBags::getTheoryRewriter()
+{
+  if (!options().bags.bags)
+  {
+    return nullptr;
+  }
+  return &d_rewriter;
+}
 
 ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; }
 

src/theory/ff/theory_ff.cpp

@@ -67,7 +67,14 @@ TheoryFiniteFields::TheoryFiniteFields(Env& env,
 
 TheoryFiniteFields::~TheoryFiniteFields() {}
 
-TheoryRewriter* TheoryFiniteFields::getTheoryRewriter() { return &d_rewriter; }
+TheoryRewriter* TheoryFiniteFields::getTheoryRewriter()
+{
+  if (!options().ff.ff)
+  {
+    return nullptr;
+  }
+  return &d_rewriter;
+}
 
 ProofRuleChecker* TheoryFiniteFields::getProofChecker() { return nullptr; }
 

src/theory/fp/theory_fp.cpp

@@ -57,7 +57,14 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation)
   d_inferManager = &d_im;
 }
 
-TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; }
+TheoryRewriter* TheoryFp::getTheoryRewriter()
+{
+  if (!options().fp.fp)
+  {
+    return nullptr;
+  }
+  return &d_rewriter;
+}
 
 ProofRuleChecker* TheoryFp::getProofChecker() { return nullptr; }
 

src/theory/rewriter.cpp

@@ -142,7 +142,15 @@ Node Rewriter::rewriteEqualityExt(TNode node)
 void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
                                       TheoryRewriter* trew)
 {
-  d_theoryRewriters[tid] = trew;
+  if (trew == nullptr)
+  {
+    // if nullptr, use the default (null) theory rewriter.
+    d_theoryRewriters[tid] = &d_nullTr;
+  }
+  else
+  {
+    d_theoryRewriters[tid] = trew;
+  }
 }
 
 TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)

src/theory/rewriter.h

@@ -176,6 +176,8 @@ class Rewriter {
 
   /** Theory rewriters used by this rewriter instance */
   TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
+  /** No-op theory rewriter, used when theory does not provide a rewriter */
+  NoOpTheoryRewriter d_nullTr;
 
   /** The proof generator */
   std::unique_ptr<TConvProofGenerator> d_tpg;

src/theory/rewriter_tables_template.h

@@ -81,7 +81,7 @@ void Rewriter::setPostRewriteCache(theory::TheoryId theoryId,
 }
 
 Rewriter::Rewriter(NodeManager* nm)
-    : d_nm(nm), d_resourceManager(nullptr), d_tpg(nullptr)
+    : d_nm(nm), d_resourceManager(nullptr), d_nullTr(nm), d_tpg(nullptr)
 {
 }
 

src/theory/sep/theory_sep.cpp

@@ -89,7 +89,14 @@ void TheorySep::initializeHeapTypes()
   }
 }
 
-TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
+TheoryRewriter* TheorySep::getTheoryRewriter()
+{
+  if (!options().sep.sep)
+  {
+    return nullptr;
+  }
+  return &d_rewriter;
+}
 
 ProofRuleChecker* TheorySep::getProofChecker() { return nullptr; }
 

src/theory/sets/theory_sets.cpp

@@ -32,7 +32,8 @@ TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_SETS, env, out, valuation),
       d_skCache(env.getNodeManager(), env.getRewriter()),
       d_state(env, valuation, d_skCache),
-      d_rewriter(nodeManager()),
+      d_rewriter(
+          nodeManager(), options().sets.setsCardExp, options().sets.relsExp),
       d_im(env, *this, &d_rewriter, d_state),
       d_cpacb(*this),
       d_internal(