Adds support for proofs for regular expression elimination in TheoryStrings::ppRewrite via a coarse-grained rule RE_ELIM.
This rule is updated by this PR to distinguish whether we apply aggressive elimination. Aggressive elimination is not currently supported, since it is non-deterministic due to generating fresh BOUND_VARIABLE.
// fixed length of component i of the regular expression concatenation R.
RE_UNFOLD_NEG_CONCAT_FIXED,
// ======== Regular expression elimination
- // Children: (P:F)
- // Arguments: none
+ // Children: none
+ // Arguments: (F, b)
// ---------------------
- // Conclusion: R
- // where R = strings::RegExpElimination::eliminate(F).
+ // Conclusion: (= F strings::RegExpElimination::eliminate(F, b))
+ // where b is a Boolean indicating whether we are using aggressive
+ // eliminations. Notice this rule concludes (= F F) if no eliminations
+ // are performed for F.
RE_ELIM,
//======================== Code points
// Children: none
}
else if (id == PfRule::RE_ELIM)
{
- Assert(children.size() == 1);
- Assert(args.empty());
- return RegExpElimination::eliminate(children[0]);
+ Assert(children.empty());
+ Assert(args.size() == 2);
+ bool isAgg;
+ if (!getBool(args[1], isAgg))
+ {
+ return Node::null();
+ }
+ Node ea = RegExpElimination::eliminate(args[0], isAgg);
+ // if we didn't eliminate, then this trivially proves the reflexive equality
+ if (ea.isNull())
+ {
+ ea = args[0];
+ }
+ return args[0].eqNode(ea);
}
else if (id == PfRule::STRING_CODE_INJ)
{
#include "theory/strings/regexp_entail.h"
#include "theory/strings/theory_strings_utils.h"
-using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::strings;
-RegExpElimination::RegExpElimination()
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+RegExpElimination::RegExpElimination(bool isAgg,
+ ProofNodeManager* pnm,
+ context::Context* c)
+ : d_isAggressive(isAgg),
+ d_pnm(pnm),
+ d_epg(pnm == nullptr
+ ? nullptr
+ : new EagerProofGenerator(pnm, c, "RegExpElimination::epg"))
{
}
-Node RegExpElimination::eliminate(Node atom)
+Node RegExpElimination::eliminate(Node atom, bool isAgg)
{
Assert(atom.getKind() == STRING_IN_REGEXP);
if (atom[1].getKind() == REGEXP_CONCAT)
{
- return eliminateConcat(atom);
+ return eliminateConcat(atom, isAgg);
}
else if (atom[1].getKind() == REGEXP_STAR)
{
- return eliminateStar(atom);
+ return eliminateStar(atom, isAgg);
}
return Node::null();
}
-Node RegExpElimination::eliminateConcat(Node atom)
+TrustNode RegExpElimination::eliminateTrusted(Node atom)
+{
+ Node eatom = eliminate(atom, d_isAggressive);
+ if (!eatom.isNull())
+ {
+ // Currently aggressive doesnt work due to fresh bound variables
+ if (isProofEnabled() && !d_isAggressive)
+ {
+ Node eq = atom.eqNode(eatom);
+ Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive);
+ std::shared_ptr<ProofNode> pn =
+ d_pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq);
+ d_epg->setProofFor(eq, pn);
+ return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get());
+ }
+ return TrustNode::mkTrustRewrite(atom, eatom, nullptr);
+ }
+ return TrustNode::null();
+}
+
+Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
{
NodeManager* nm = NodeManager::currentNM();
Node x = atom[0];
// otherwise, we can use indexof to represent some next occurrence
if (gap_exact[i + 1] && i + 1 != size)
{
- if (!options::regExpElimAgg())
+ if (!isAgg)
{
canProcess = false;
break;
}
}
- if (!options::regExpElimAgg())
+ if (!isAgg)
{
return Node::null();
}
return Node::null();
}
-Node RegExpElimination::eliminateStar(Node atom)
+Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
{
- if (!options::regExpElimAgg())
+ if (!isAgg)
{
return Node::null();
}
<< "." << std::endl;
return atomElim;
}
+bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; }
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
#define CVC4__THEORY__STRINGS__REGEXP_ELIM_H
#include "expr/node.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/trust_node.h"
namespace CVC4 {
namespace theory {
class RegExpElimination
{
public:
- RegExpElimination();
+ /**
+ * @param isAgg Whether aggressive eliminations are enabled
+ * @param pnm The proof node manager to use (for proofs)
+ * @param c The context to use (for proofs)
+ */
+ RegExpElimination(bool isAgg = false,
+ ProofNodeManager* pnm = nullptr,
+ context::Context* c = nullptr);
/** eliminate membership
*
* This method takes as input a regular expression membership atom of the
* form (str.in.re x R). If this method returns a non-null node ret, then ret
* is equivalent to atom.
+ *
+ * @param atom The node to eliminate
+ * @param isAgg Whether we apply aggressive elimination techniques
+ * @return The node with regular expressions eliminated, or null if atom
+ * was unchanged.
+ */
+ static Node eliminate(Node atom, bool isAgg);
+
+ /**
+ * Return the trust node corresponding to rewriting n based on eliminate
+ * above.
*/
- static Node eliminate(Node atom);
+ TrustNode eliminateTrusted(Node atom);
private:
/** return elimination
*/
static Node returnElim(Node atom, Node atomElim, const char* id);
/** elimination for regular expression concatenation */
- static Node eliminateConcat(Node atom);
+ static Node eliminateConcat(Node atom, bool isAgg);
/** elimination for regular expression star */
- static Node eliminateStar(Node atom);
+ static Node eliminateStar(Node atom, bool isAgg);
+ /** Are proofs enabled? */
+ bool isProofEnabled() const;
+ /** Are aggressive eliminations enabled? */
+ bool d_isAggressive;
+ /** Pointer to the proof node manager */
+ ProofNodeManager* d_pnm;
+ /** An eager proof generator for storing proofs in eliminate trusted above */
+ std::unique_ptr<EagerProofGenerator> d_epg;
}; /* class RegExpElimination */
} // namespace strings
TrustNode TheoryStrings::ppRewrite(TNode atom)
{
Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
+ TrustNode ret;
Node atomRet = atom;
if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
{
// aggressive elimination of regular expression membership
- Node atomElim = d_regexp_elim.eliminate(atomRet);
- if (!atomElim.isNull())
+ ret = d_regexp_elim.eliminateTrusted(atomRet);
+ if (!ret.isNull())
{
- Trace("strings-ppr") << " rewrote " << atom << " -> " << atomElim
+ Trace("strings-ppr") << " rewrote " << atom << " -> " << ret.getNode()
<< " via regular expression elimination."
<< std::endl;
- atomRet = atomElim;
+ atomRet = ret.getNode();
}
}
if( !options::stringLazyPreproc() ){
//eager preprocess here
std::vector< Node > new_nodes;
StringsPreprocess* p = d_esolver.getPreprocess();
- Node ret = p->processAssertion(atomRet, new_nodes);
- if (ret != atomRet)
+ Node pret = p->processAssertion(atomRet, new_nodes);
+ if (pret != atomRet)
{
- Trace("strings-ppr") << " rewrote " << atomRet << " -> " << ret
+ Trace("strings-ppr") << " rewrote " << atomRet << " -> " << pret
<< ", with " << new_nodes.size() << " lemmas."
<< std::endl;
for (const Node& lem : new_nodes)
++(d_statistics.d_lemmasEagerPreproc);
d_out->lemma(lem);
}
- atomRet = ret;
+ atomRet = pret;
+ // Don't support proofs yet, thus we must return nullptr. This is the
+ // case even if we had proven the elimination via regexp elimination
+ // above.
+ ret = TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
}else{
Assert(new_nodes.empty());
}
}
- if (atomRet != atom)
- {
- return TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
- }
- return TrustNode::null();
+ return ret;
}
/** run the given inference step */
projects / cvc5.git / commitdiff