Use constant folding for evaluating BV eager atom (#6494)

This is work towards unifying top-level substitutions with model substitutions.

Currently, for model evaluation, BV eager atom preprocessing pass adds mappings (BV_EAGER_ATOM X) -> X to say how (BV_EAGER_ATOM X) should be evaluated in the model. This is not necessary since a rewrite rule (BV_EAGER_ATOM c) -> c for constant c would suffice.

This eliminates the call to addModelSubstitution in that preprocessing pass.

It also makes it so that we don't make true/false themselves into eager atoms.

1 files changed, 5 insertions, 1 deletions

diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index 1466a945d..665b32faa 100644
--- a/src/preprocessing/passes/bv_eager_atoms.cpp
+++ b/src/preprocessing/passes/bv_eager_atoms.cpp
@@ -37,8 +37,12 @@ PreprocessingPassResult BvEagerAtoms::applyInternal(
   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     TNode atom = (*assertionsToPreprocess)[i];
+    if (atom.isConst())
+    {
+      // don't bother making true/false into atoms
+      continue;
+    }
     Node eager_atom = nm->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
-    d_preprocContext->addModelSubstitution(eager_atom, atom);
     assertionsToPreprocess->replace(i, eager_atom);
   }
   return PreprocessingPassResult::NO_CONFLICT;