diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-06 14:22:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-06 12:22:46 -0700 |
commit | 2f4af86757f34a31f2983f30b3321e7c0511aa32 (patch) | |
tree | 529154c8abbe912da9af0ce0e09142eff53afb42 /src | |
parent | 2283ee3b0327441c29caf26be977c1e4cd13c637 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/bv_eager_atoms.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 12 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 1 |
5 files changed, 29 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; diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 72906929b..7fe9559f9 100644 --- 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 4320e3b81..1c229ed72 100644 --- 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 9b3fde6fb..bda212351 100644 --- 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 e35184084..56eb718df 100644 --- 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); |