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.

diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index 1466a945d341dfcf7742d1786b96ac957cd6fbe0..665b32faa54cbd14531cbca571d32b78ca733022 100644 (file)
--- 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;

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 72906929bb680148e83a32fbbf5d30b1db28202d..7fe9559f99f7fd2495175f7f4e9dc5b4d2e41dfd 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -108,6 +108,7 @@ enum RewriteRuleId
   EvalSle,
   EvalITEBv,
   EvalComp,
+  EvalEagerAtom,
 
   /// simplification rules
   /// all of these rules decrease formula size
@@ -270,6 +271,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case EvalSltBv:           out << "EvalSltBv";           return out;
   case EvalITEBv:           out << "EvalITEBv";           return out;
   case EvalComp:            out << "EvalComp";            return out;
+  case EvalEagerAtom: out << "EvalEagerAtom"; return out;
   case EvalExtract :        out << "EvalExtract";         return out;
   case EvalSignExtend :     out << "EvalSignExtend";      return out;
   case EvalRotateLeft :     out << "EvalRotateLeft";      return out;

diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 4320e3b81cac2f54cba5d548a490e754a82ed738..1c229ed722db705753732d1749ac2218c6af0752 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -491,6 +491,18 @@ Node RewriteRule<EvalComp>::apply(TNode node) {
   return utils::mkConst(1, 0);
 }
 
+template <>
+inline bool RewriteRule<EvalEagerAtom>::applies(TNode node)
+{
+  return (node.getKind() == kind::BITVECTOR_EAGER_ATOM && node[0].isConst());
+}
+
+template <>
+inline Node RewriteRule<EvalEagerAtom>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
+  return node[0];
+}
 }
 }
 }  // namespace cvc5

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 9b3fde6fb2a6891a71b5fdd1f2c95238cbe92af6..bda2123510ec62a2e147c27b1fd0739f27984496 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -382,6 +382,14 @@ RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite)
   return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
+RewriteResponse TheoryBVRewriter::RewriteEagerAtom(TNode node, bool prerewrite)
+{
+  Node resultNode =
+      LinearRewriteStrategy<RewriteRule<EvalEagerAtom>>::apply(node);
+
+  return RewriteResponse(REWRITE_DONE, resultNode);
+}
+
 RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
   Node resultNode = node; 
   resultNode = LinearRewriteStrategy
@@ -732,6 +740,7 @@ void TheoryBVRewriter::initializeRewrites() {
   d_rewriteTable [ kind::BITVECTOR_ULTBV ] = RewriteUltBv;
   d_rewriteTable [ kind::BITVECTOR_SLTBV ] = RewriteSltBv;
   d_rewriteTable [ kind::BITVECTOR_ITE ] = RewriteITEBv;
+  d_rewriteTable[kind::BITVECTOR_EAGER_ATOM] = RewriteEagerAtom;
 
   d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat;
   d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV;

diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index e351840846ca17f9c6008b3e455dbf53ee252929..56eb718dff467f456b0e6351590722fc5115f804 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -97,6 +97,7 @@ class TheoryBVRewriter : public TheoryRewriter
   static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteEagerAtom(TNode node, bool prerewrite = false);
 
   static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);