** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
#include "expr/node.h"
#include "expr/proof_checker.h"
#include "expr/proof_node.h"
+#include "theory/quantifiers/extended_rewrite.h"
-namespace CVC4 {
+namespace cvc5 {
namespace theory {
-/**
+/**
* Identifiers for rewriters and substitutions, which we abstractly
* classify as "methods". Methods have a unique identifier in the internal
* proof calculus implemented by the checker below.
//---------------------------- Rewriters
// Rewriter::rewrite(n)
RW_REWRITE,
+ // d_ext_rew.extendedRewrite(n);
+ RW_EXT_REWRITE,
+ // Rewriter::rewriteExtEquality(n)
+ RW_REWRITE_EQ_EXT,
+ // Evaluator::evaluate(n)
+ RW_EVALUATE,
// identity
RW_IDENTITY,
+ // theory preRewrite, note this is only intended to be used as an argument
+ // to THEORY_REWRITE in the final proof. It is not implemented in
+ // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
+ RW_REWRITE_THEORY_PRE,
+ // same as above, for theory postRewrite
+ RW_REWRITE_THEORY_POST,
//---------------------------- Substitutions
// (= x y) is interpreted as x -> y, using Node::substitute
SB_DEFAULT,
BuiltinProofRuleChecker() {}
~BuiltinProofRuleChecker() {}
/**
- * Apply rewrite on n (in witness form). This encapsulates the exact behavior
- * of a REWRITE step in a proof. Rewriting is performed on the Skolem form of
- * n.
+ * Apply rewrite on n (in skolem form). This encapsulates the exact behavior
+ * of a REWRITE step in a proof.
*
- * @param n The node (in witness form) to rewrite,
+ * @param n The node to rewrite,
* @param idr The method identifier of the rewriter, by default RW_REWRITE
* specifying a call to Rewriter::rewrite.
* @return The rewritten form of n.
*/
- static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
+ Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
/**
- * Apply substitution on n (in witness form). This encapsulates the exact
- * behavior of a SUBS step in a proof. Substitution is on the Skolem form of
- * n.
+ * Get substitution for literal exp. Updates vars/subs to the substitution
+ * specified by exp for the substitution method ids.
+ */
+ static bool getSubstitutionForLit(Node exp,
+ TNode& var,
+ TNode& subs,
+ MethodId ids = MethodId::SB_DEFAULT);
+ /**
+ * Get substitution for formula exp. Adds to vars/subs to the substitution
+ * specified by exp for the substitution method ids, which may be multiple
+ * substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other
+ * substitution types always interpret applications of AND as a formula).
+ * The vector "from" are the literals from exp that each substitution in
+ * vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then
+ * vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }.
+ */
+ static bool getSubstitutionFor(Node exp,
+ std::vector<TNode>& vars,
+ std::vector<TNode>& subs,
+ std::vector<TNode>& from,
+ MethodId ids = MethodId::SB_DEFAULT);
+
+ /**
+ * Apply substitution on n in skolem form. This encapsulates the exact
+ * behavior of a SUBS step in a proof.
*
- * @param n The node (in witness form) to substitute,
- * @param exp The (set of) equalities (in witness form) corresponding to the
- * substitution
+ * @param n The node to substitute,
+ * @param exp The (set of) equalities/literals/formulas that the substitution
+ * is derived from
* @param ids The method identifier of the substitution, by default SB_DEFAULT
* specifying that lhs/rhs of equalities are interpreted as a substitution.
* @return The substituted form of n.
*
* Combines the above two steps.
*
- * @param n The node (in witness form) to substitute and rewrite,
- * @param exp The (set of) equalities (in witness form) corresponding to the
- * substitution
+ * @param n The node to substitute and rewrite,
+ * @param exp The (set of) equalities corresponding to the substitution
* @param ids The method identifier of the substitution.
* @param idr The method identifier of the rewriter.
* @return The substituted, rewritten form of n.
*/
- static Node applySubstitutionRewrite(Node n,
- const std::vector<Node>& exp,
- MethodId ids = MethodId::SB_DEFAULT,
- MethodId idr = MethodId::RW_REWRITE);
- /** get a rewriter Id from a node, return false if we fail */
+ Node applySubstitutionRewrite(Node n,
+ const std::vector<Node>& exp,
+ MethodId ids = MethodId::SB_DEFAULT,
+ MethodId idr = MethodId::RW_REWRITE);
+ /** get a method identifier from a node, return false if we fail */
static bool getMethodId(TNode n, MethodId& i);
+ /**
+ * Get method identifiers from args starting at the given index. Store their
+ * values into ids, idr. This method returns false if args does not contain
+ * valid method identifiers at position index in args.
+ */
+ bool getMethodIds(const std::vector<Node>& args,
+ MethodId& ids,
+ MethodId& idr,
+ size_t index);
+ /**
+ * Add method identifiers ids and idr as nodes to args. This does not add ids
+ * or idr if their values are the default ones.
+ */
+ static void addMethodIds(std::vector<Node>& args, MethodId ids, MethodId idr);
+
+ /** get a TheoryId from a node, return false if we fail */
+ static bool getTheoryId(TNode n, TheoryId& tid);
+ /** Make a TheoryId into a node */
+ static Node mkTheoryIdNode(TheoryId tid);
/** Register all rules owned by this rule checker into pc. */
void registerTo(ProofChecker* pc) override;
-
protected:
/** Return the conclusion of the given proof step, or null if it is invalid */
Node checkInternal(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args) override;
- /** get method identifiers */
- bool getMethodIds(const std::vector<Node>& args,
- MethodId& ids,
- MethodId& idr,
- size_t index);
- /**
- * Apply rewrite (on Skolem form). id is the identifier of the rewriter.
- */
- static Node applyRewriteExternal(Node n, MethodId idr = MethodId::RW_REWRITE);
- /**
- * Apply substitution for n (on Skolem form), where exp is an equality
- * (or set of equalities) in Witness form. Returns the result of
- * n * sigma{ids}(exp), where sigma{ids} is a substitution based on method
- * identifier ids.
- */
- static Node applySubstitutionExternal(Node n, Node exp, MethodId ids);
- /** Same as above, for a list of substitutions in exp */
- static Node applySubstitutionExternal(Node n,
- const std::vector<Node>& exp,
- MethodId ids);
+
+ /** extended rewriter object */
+ quantifiers::ExtendedRewriter d_ext_rewriter;
};
} // namespace builtin
} // namespace theory
-} // namespace CVC4
+} // namespace cvc5
#endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */
projects / cvc5.git / blobdiff