Skip to content
This repository has been archived by the owner on May 7, 2021. It is now read-only.
/ CVC4-archived Public archive

Commit

Permalink
(proof-new) Add quantifiers proof checker (#4593)
Browse files Browse the repository at this point in the history 
Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms.

This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges.
  • Loading branch information
@ajreynol
ajreynol authored Jun 16, 2020
1 parent e5f51e8 commit df98bc9
Show file tree
Hide file tree
Showing 5 changed files with 341 additions and 143 deletions.
2 changes: 2 additions & 0 deletions src/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -534,6 +534,8 @@ libcvc4_add_sources(
theory/quantifiers/instantiate.h
theory/quantifiers/lazy_trie.cpp
theory/quantifiers/lazy_trie.h
theory/quantifiers/proof_checker.cpp
theory/quantifiers/proof_checker.h
theory/quantifiers/quant_conflict_find.cpp
theory/quantifiers/quant_conflict_find.h
theory/quantifiers/quant_epr.cpp
Expand Down
23 changes: 14 additions & 9 deletions src/expr/proof_rule.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,15 +31,6 @@ const char* toString(PfRule id)
case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
//================================================= Equality rules
case PfRule::REFL: return "REFL";
case PfRule::SYMM: return "SYMM";
case PfRule::TRANS: return "TRANS";
case PfRule::CONG: return "CONG";
case PfRule::TRUE_INTRO: return "TRUE_INTRO";
case PfRule::TRUE_ELIM: return "TRUE_ELIM";
case PfRule::FALSE_INTRO: return "FALSE_INTRO";
case PfRule::FALSE_ELIM: return "FALSE_ELIM";
//================================================= Boolean rules
case PfRule::SPLIT: return "SPLIT";
case PfRule::AND_ELIM: return "AND_ELIM";
Expand Down Expand Up @@ -85,6 +76,20 @@ const char* toString(PfRule id)
case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1";
case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2";
case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3";
//================================================= Equality rules
case PfRule::REFL: return "REFL";
case PfRule::SYMM: return "SYMM";
case PfRule::TRANS: return "TRANS";
case PfRule::CONG: return "CONG";
case PfRule::TRUE_INTRO: return "TRUE_INTRO";
case PfRule::TRUE_ELIM: return "TRUE_ELIM";
case PfRule::FALSE_INTRO: return "FALSE_INTRO";
case PfRule::FALSE_ELIM: return "FALSE_ELIM";
//================================================= Quantifiers rules
case PfRule::WITNESS_INTRO: return "WITNESS_INTRO";
case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
case PfRule::SKOLEMIZE: return "SKOLEMIZE";
case PfRule::INSTANTIATE: return "INSTANTIATE";
//================================================= Unknown rule
case PfRule::UNKNOWN: return "UNKNOWN";
default: return "?";
Expand Down
301 changes: 167 additions & 134 deletions src/expr/proof_rule.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,55 +71,102 @@ enum class PfRule : uint32_t
// has the conclusion (=> F F) and has no free assumptions. More generally, a
// proof with no free assumptions always concludes a valid formula.
SCOPE,
//================================================= Equality rules
// ======== Reflexive

//======================== Builtin theory (common node operations)
// ======== Substitution
// Children: (P1:F1, ..., Pn:Fn)
// Arguments: (t, (ids)?)
// ---------------------------------------------------------------
// Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
// where sigma{ids}(Fi) are substitutions, which notice are applied in
// reverse order.
// Notice that ids is a MethodId identifier, which determines how to convert
// the formulas F1, ..., Fn into substitutions.
SUBS,
// ======== Rewrite
// Children: none
// Arguments: (t)
// ---------------------
// Conclusion: (= t t)
REFL,
// ======== Symmetric
// Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
// Arguments: none
// -----------------------
// Conclusion: (= t2 t1) or (not (= t2 t1))
SYMM,
// ======== Transitivity
// Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
// Arguments: none
// -----------------------
// Conclusion: (= t1 tn)
TRANS,
// ======== Congruence (subsumed by Substitute?)
// Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
// Arguments: (f)
// ---------------------------------------------
// Conclusion: (= (f t1 ... tn) (f s1 ... sn))
CONG,
// ======== True intro
// Children: (P:F)
// Arguments: none
// ----------------------------------------
// Conclusion: (= F true)
TRUE_INTRO,
// ======== True elim
// Children: (P:(= F true)
// Arguments: none
// Arguments: (t, (idr)?)
// ----------------------------------------
// Conclusion: (= t Rewriter{idr}(t))
// where idr is a MethodId identifier, which determines the kind of rewriter
// to apply, e.g. Rewriter::rewrite.
REWRITE,
// ======== Substitution + Rewriting equality introduction
//
// In this rule, we provide a term t and conclude that it is equal to its
// rewritten form under a (proven) substitution.
//
// Children: (P1:F1, ..., Pn:Fn)
// Arguments: (t, (ids (idr)?)?)
// ---------------------------------------------------------------
// Conclusion: (= t t')
// where
// t' is
// toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
// toSkolem(...) converts terms from witness form to Skolem form,
// toWitness(...) converts terms from Skolem form to witness form.
//
// Notice that:
// toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
// In other words, from the point of view of Skolem forms, this rule
// transforms t to t' by standard substitution + rewriting.
//
// The argument ids and idr is optional and specify the identifier of the
// substitution and rewriter respectively to be used. For details, see
// theory/builtin/proof_checker.h.
MACRO_SR_EQ_INTRO,
// ======== Substitution + Rewriting predicate introduction
//
// In this rule, we provide a formula F and conclude it, under the condition
// that it rewrites to true under a proven substitution.
//
// Children: (P1:F1, ..., Pn:Fn)
// Arguments: (F, (ids (idr)?)?)
// ---------------------------------------------------------------
// Conclusion: F
TRUE_ELIM,
// ======== False intro
// Children: (P:(not F))
// Arguments: none
// where
// Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
// where ids and idr are method identifiers.
//
// Notice that we apply rewriting on the witness form of F, meaning that this
// rule may conclude an F whose Skolem form is justified by the definition of
// its (fresh) Skolem variables. Furthermore, notice that the rewriting and
// substitution is applied only within the side condition, meaning the
// rewritten form of the witness form of F does not escape this rule.
MACRO_SR_PRED_INTRO,
// ======== Substitution + Rewriting predicate elimination
//
// In this rule, if we have proven a formula F, then we may conclude its
// rewritten form under a proven substitution.
//
// Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
// Arguments: ((ids (idr)?)?)
// ----------------------------------------
// Conclusion: (= F false)
FALSE_INTRO,
// ======== False elim
// Children: (P:(= F false)
// Arguments: none
// Conclusion: F'
// where
// F' is
// toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
// where ids and idr are method identifiers.
//
// We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
MACRO_SR_PRED_ELIM,
// ======== Substitution + Rewriting predicate transform
//
// In this rule, if we have proven a formula F, then we may provide a formula
// G and conclude it if F and G are equivalent after rewriting under a proven
// substitution.
//
// Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
// Arguments: (G, (ids (idr)?)?)
// ----------------------------------------
// Conclusion: (not F)
FALSE_ELIM,
// Conclusion: G
// where
// Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
// Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
//
// Notice that we apply rewriting on the witness form of F and G, similar to
// MACRO_SR_PRED_INTRO.
MACRO_SR_PRED_TRANSFORM,

//================================================= Boolean rules
// ======== Split
Expand Down Expand Up @@ -378,101 +425,87 @@ enum class PfRule : uint32_t
// Conclusion: (or (ite C F1 F2) (not F1) (not F2))
CNF_ITE_NEG3,

//======================== Builtin theory (common node operations)
// ======== Substitution
// Children: (P1:F1, ..., Pn:Fn)
// Arguments: (t, (ids)?)
// ---------------------------------------------------------------
// Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
// where sigma{ids}(Fi) are substitutions, which notice are applied in
// reverse order.
// Notice that ids is a MethodId identifier, which determines how to convert
// the formulas F1, ..., Fn into substitutions.
SUBS,
// ======== Rewrite
//================================================= Equality rules
// ======== Reflexive
// Children: none
// Arguments: (t, (idr)?)
// Arguments: (t)
// ---------------------
// Conclusion: (= t t)
REFL,
// ======== Symmetric
// Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
// Arguments: none
// -----------------------
// Conclusion: (= t2 t1) or (not (= t2 t1))
SYMM,
// ======== Transitivity
// Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
// Arguments: none
// -----------------------
// Conclusion: (= t1 tn)
TRANS,
// ======== Congruence (subsumed by Substitute?)
// Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
// Arguments: (f)
// ---------------------------------------------
// Conclusion: (= (f t1 ... tn) (f s1 ... sn))
CONG,
// ======== True intro
// Children: (P:F)
// Arguments: none
// ----------------------------------------
// Conclusion: (= F true)
TRUE_INTRO,
// ======== True elim
// Children: (P:(= F true)
// Arguments: none
// ----------------------------------------
// Conclusion: (= t Rewriter{idr}(t))
// where idr is a MethodId identifier, which determines the kind of rewriter
// to apply, e.g. Rewriter::rewrite.
REWRITE,
// ======== Substitution + Rewriting equality introduction
//
// In this rule, we provide a term t and conclude that it is equal to its
// rewritten form under a (proven) substitution.
//
// Children: (P1:F1, ..., Pn:Fn)
// Arguments: (t, (ids (idr)?)?)
// ---------------------------------------------------------------
// Conclusion: (= t t')
// where
// t' is
// toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
// toSkolem(...) converts terms from witness form to Skolem form,
// toWitness(...) converts terms from Skolem form to witness form.
//
// Notice that:
// toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
// In other words, from the point of view of Skolem forms, this rule
// transforms t to t' by standard substitution + rewriting.
//
// The argument ids and idr is optional and specify the identifier of the
// substitution and rewriter respectively to be used. For details, see
// theory/builtin/proof_checker.h.
MACRO_SR_EQ_INTRO,
// ======== Substitution + Rewriting predicate introduction
//
// In this rule, we provide a formula F and conclude it, under the condition
// that it rewrites to true under a proven substitution.
//
// Children: (P1:F1, ..., Pn:Fn)
// Arguments: (F, (ids (idr)?)?)
// ---------------------------------------------------------------
// Conclusion: F
// where
// Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
// where ids and idr are method identifiers.
//
// Notice that we apply rewriting on the witness form of F, meaning that this
// rule may conclude an F whose Skolem form is justified by the definition of
// its (fresh) Skolem variables. Furthermore, notice that the rewriting and
// substitution is applied only within the side condition, meaning the
// rewritten form of the witness form of F does not escape this rule.
MACRO_SR_PRED_INTRO,
// ======== Substitution + Rewriting predicate elimination
//
// In this rule, if we have proven a formula F, then we may conclude its
// rewritten form under a proven substitution.
//
// Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
// Arguments: ((ids (idr)?)?)
TRUE_ELIM,
// ======== False intro
// Children: (P:(not F))
// Arguments: none
// ----------------------------------------
// Conclusion: F'
// where
// F' is
// toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
// where ids and idr are method identifiers.
//
// We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
MACRO_SR_PRED_ELIM,
// ======== Substitution + Rewriting predicate transform
//
// In this rule, if we have proven a formula F, then we may provide a formula
// G and conclude it if F and G are equivalent after rewriting under a proven
// substitution.
//
// Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
// Arguments: (G, (ids (idr)?)?)
// Conclusion: (= F false)
FALSE_INTRO,
// ======== False elim
// Children: (P:(= F false)
// Arguments: none
// ----------------------------------------
// Conclusion: G
// where
// Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
// Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
//
// Notice that we apply rewriting on the witness form of F and G, similar to
// MACRO_SR_PRED_INTRO.
MACRO_SR_PRED_TRANSFORM,
// Conclusion: (not F)
FALSE_ELIM,

//================================================= Quantifiers rules
// ======== Witness intro
// Children: (P:F[t])
// Arguments: (t)
// ----------------------------------------
// Conclusion: (= t (witness ((x T)) F[x]))
// where x is a BOUND_VARIABLE unique to the pair F,t.
WITNESS_INTRO,
// ======== Exists intro
// Children: (P:F[t])
// Arguments: (t)
// ----------------------------------------
// Conclusion: (exists ((x T)) F[x])
// where x is a BOUND_VARIABLE unique to the pair F,t.
EXISTS_INTRO,
// ======== Skolemize
// Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
// Arguments: none
// ----------------------------------------
// Conclusion: F*sigma
// sigma maps x1 ... xn to their representative skolems obtained by
// SkolemManager::mkSkolemize, returned in the skolems argument of that
// method.
SKOLEMIZE,
// ======== Instantiate
// Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
// Arguments: (t1 ... tn)
// ----------------------------------------
// Conclusion: F*sigma
// sigma maps x1 ... xn to t1 ... tn.
INSTANTIATE,

//================================================= Unknown rule
UNKNOWN,
Expand Down
Loading

0 comments on commit df98bc9

Please sign in to comment.