From: Andrew Reynolds Date: Fri, 21 May 2021 20:16:20 +0000 (-0500) Subject: (proof-new) Minor documentation sync (#6592) X-Git-Tag: cvc5-1.0.0~1710 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7f3cf539939c717692d1309bda742801817ad64;p=cvc5.git (proof-new) Minor documentation sync (#6592) --- diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 3146160bb..215c61210 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -76,7 +76,8 @@ class ProofNodeUpdaterCallback * (ProofNodeUpdaterCallback::shouldUpdate) * and overwrites them based on the update procedure of the callback * (ProofNodeUpdaterCallback::update), which uses local CDProof objects that - * should be filled in the callback for each ProofNode to update. + * should be filled in the callback for each ProofNode to update. This update + * process is applied in a *pre-order* traversal. */ class ProofNodeUpdater { diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index c2a6a30f6..f4e8078dc 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -52,6 +52,7 @@ const char* toString(PfRule id) case PfRule::FACTORING: return "FACTORING"; case PfRule::REORDERING: return "REORDERING"; case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION"; + case PfRule::MACRO_RESOLUTION_TRUST: return "MACRO_RESOLUTION_TRUST"; case PfRule::SPLIT: return "SPLIT"; case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; case PfRule::MODUS_PONENS: return "MODUS_PONENS"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index e4c33a840..9771dda31 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -41,6 +41,10 @@ namespace cvc5 { * (2) SCOPE, which closes the scope of assumptions. * The core rules additionally correspond to generic operations that are done * internally on nodes, e.g. calling Rewriter::rewrite. + * + * Rules with prefix MACRO_ are those that can be defined in terms of other + * rules. These exist for convienience. We provide their definition in the line + * "Macro:". */ enum class PfRule : uint32_t { @@ -181,7 +185,6 @@ enum class PfRule : uint32_t // where F' and G' are the result of each side of the equation above. Here, // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above. MACRO_SR_PRED_TRANSFORM, - //================================================= Processing rules // ======== Remove Term Formulas Axiom // Children: none @@ -214,7 +217,7 @@ enum class PfRule : uint32_t // the quantifiers rewriter involves constructing new bound variables that are // not guaranteed to be consistent on each call. THEORY_REWRITE, - // The rules in this section have the signature of a "trusted rule": + // The remaining rules in this section have the signature of a "trusted rule": // // Children: none // Arguments: (F) @@ -907,8 +910,8 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s))) // where - // r_t = (witness ((z String)) (= z (suf t1 (str.len s1)))), - // r_s = (witness ((z String)) (= z (suf s1 (str.len t1)))). + // r_t = (skolem (suf t1 (str.len s1)))), + // r_s = (skolem (suf s1 (str.len t1)))). // // or the reverse form of the above: // @@ -918,9 +921,8 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2))) // where - // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len - // s2))))), r_s = (witness ((z String)) (= z (pre s2 (- (str.len s2) - // (str.len t2))))). + // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2))))), + // r_s = (skolem (pre s2 (- (str.len s2) (str.len t2))))). // // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and // (pre x n) is shorthand for (str.substr x 0 n). @@ -932,7 +934,7 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (= t1 (str.++ c r)) // where - // r = (witness ((z String)) (= z (suf t1 1))). + // r = (skolem (suf t1 1)). // // or the reverse form of the above: // @@ -942,7 +944,7 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (= t2 (str.++ r c)) // where - // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) 1)))). + // r = (skolem (pre t2 (- (str.len t2) 1))). CONCAT_CSPLIT, // ======== Concat length propagate // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), @@ -951,7 +953,7 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (= t1 (str.++ s1 r_t)) // where - // r_t = (witness ((z String)) (= z (suf t1 (str.len s1)))) + // r_t = (skolem (suf t1 (str.len s1))) // // or the reverse form of the above: // @@ -961,8 +963,7 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (= t2 (str.++ r_t s2)) // where - // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len - // s2))))). + // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2)))). CONCAT_LPROP, // ======== Concat constant propagate // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)), @@ -975,7 +976,7 @@ enum class PfRule : uint32_t // w3 is (pre w2 p), // w4 is (suf w2 p), // p = Word::overlap((suf w2 1), w1), - // r = (witness ((z String)) (= z (suf t1 (str.len w3)))). + // r = (skolem (suf t1 (str.len w3))). // In other words, w4 is the largest suffix of (suf w2 1) that can contain a // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1. // @@ -991,7 +992,7 @@ enum class PfRule : uint32_t // w3 is (suf w2 (- (str.len w2) p)), // w4 is (pre w2 (- (str.len w2) p)), // p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1), - // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len w3))))). + // r = (skolem (pre t2 (- (str.len t2) (str.len w3)))). // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1)) // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore // be contained in t2. @@ -1007,14 +1008,14 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n)) // where - // w1 is (witness ((z String)) (= z (pre t n))) - // w2 is (witness ((z String)) (= z (suf t n))) + // w1 is (skolem (pre t n)) + // w2 is (skolem (suf t n)) STRING_DECOMPOSE, // ======== Length positive // Children: none // Arguments: (t) // --------------------- - // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t 0))) + // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0)) STRING_LENGTH_POS, // ======== Length non-empty // Children: (P1:(not (= t ""))) @@ -1030,15 +1031,15 @@ enum class PfRule : uint32_t // Conclusion: (and R (= t w)) // where w = strings::StringsPreprocess::reduce(t, R, ...). // In other words, R is the reduction predicate for extended term t, and w is - // (witness ((z T)) (= z t)) + // (skolem t) // Notice that the free variables of R are w and the free variables of t. STRING_REDUCTION, // ======== Eager Reduction // Children: none - // Arguments: (t, id?) + // Arguments: (t) // --------------------- // Conclusion: R - // where R = strings::TermRegistry::eagerReduce(t, id). + // where R = strings::TermRegistry::eagerReduce(t). STRING_EAGER_REDUCTION, //======================== Regular expressions // ======== Regular expression intersection @@ -1141,7 +1142,6 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (<= i greatestIntLessThan(c)}) INT_TIGHT_UB, - // ======== Tightening Strict Integer Lower Bounds // Children: (P:(> i c)) // where i has integer type. @@ -1149,7 +1149,6 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (>= i leastIntGreaterThan(c)}) INT_TIGHT_LB, - // ======== Trichotomy of the reals // Children: (A B) // Arguments: (C) @@ -1161,14 +1160,12 @@ enum class PfRule : uint32_t // note that "not" here denotes arithmetic negation, flipping // >= to <, etc. ARITH_TRICHOTOMY, - // ======== Arithmetic operator elimination // Children: none // Arguments: (t) // --------------------- // Conclusion: arith::OperatorElim::getAxiomFor(t) ARITH_OP_ELIM_AXIOM, - // ======== Int Trust // Children: (P1 ... Pn) // Arguments: (Q) @@ -1223,7 +1220,6 @@ enum class PfRule : uint32_t // Conclusion: (and (>= real.pi l) (<= real.pi u)) // Where l (u) is a valid lower (upper) bound on pi. ARITH_TRANS_PI, - //======== Exp at negative values // Children: none // Arguments: (t) @@ -1289,7 +1285,6 @@ enum class PfRule : uint32_t // exponential function is the following: // e^x = \sum_{n=0}^{\infty} x^n / n! ARITH_TRANS_EXP_APPROX_BELOW, - //======== Sine is always between -1 and 1 // Children: none // Arguments: (t) diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 53633a123..0968aa1f9 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -66,6 +66,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM); d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION_TRUST); d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION); + d_pfpp->setEliminateRule(PfRule::MACRO_ARITH_SCALE_SUM_UB); if (options::proofGranularityMode() != options::ProofGranularityMode::REWRITE) { diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 1606fbb50..c0b368e6e 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -130,7 +130,7 @@ class EagerProofGenerator : public ProofGenerator * @param isConflict Whether the returned trust node is a conflict (otherwise * it is a lemma), * @return The trust node corresponding to the fact that this generator has - * a proof of (children => exp), or of exp if children is empty. + * a proof of (exp => conc), or of conc if exp is empty. */ TrustNode mkTrustNode(Node conc, PfRule id,