mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove references to deprecated uses of PROOF_MODE #1531
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e5a1981694
commit
6e87622c8a
|
@ -919,7 +919,6 @@ extern "C" {
|
|||
case PR_REWRITE: return Z3_OP_PR_REWRITE;
|
||||
case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
|
||||
case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
|
||||
case PR_PULL_QUANT_STAR: return Z3_OP_PR_PULL_QUANT_STAR;
|
||||
case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
|
||||
case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
|
||||
case PR_DER: return Z3_OP_PR_DER;
|
||||
|
@ -936,9 +935,7 @@ extern "C" {
|
|||
case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
|
||||
case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
|
||||
case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
|
||||
case PR_NNF_STAR: return Z3_OP_PR_NNF_STAR;
|
||||
case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE;
|
||||
case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR;
|
||||
case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
|
||||
case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
|
||||
case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
|
||||
|
|
|
@ -932,7 +932,7 @@ namespace Microsoft.Z3
|
|||
/// Indicates whether the term is a proof by condensed transitivity of a relation
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
/// Condensed transitivity proof.
|
||||
/// It combines several symmetry and transitivity proofs.
|
||||
/// Example:
|
||||
/// T1: (R a b)
|
||||
|
@ -1035,14 +1035,11 @@ namespace Microsoft.Z3
|
|||
/// </summary>
|
||||
/// <remarks>
|
||||
/// A proof for rewriting an expression t into an expression s.
|
||||
/// This proof object is used if the parameter PROOF_MODE is 1.
|
||||
/// This proof object can have n antecedents.
|
||||
/// The antecedents are proofs for equalities used as substitution rules.
|
||||
/// The object is also used in a few cases if the parameter PROOF_MODE is 2.
|
||||
/// The cases are:
|
||||
/// The object is used in a few cases:
|
||||
/// - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
|
||||
/// - When converting bit-vectors to Booleans (BIT2BOOL=true)
|
||||
/// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
|
||||
/// </remarks>
|
||||
public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
|
||||
|
||||
|
@ -1054,15 +1051,6 @@ namespace Microsoft.Z3
|
|||
/// </remarks>
|
||||
public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the term is a proof for pulling quantifiers out.
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// A proof for (iff P Q) where Q is in prenex normal form.
|
||||
/// This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
/// This proof object has no antecedents
|
||||
/// </remarks>
|
||||
public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the term is a proof for pushing quantifiers in.
|
||||
|
@ -1304,28 +1292,6 @@ namespace Microsoft.Z3
|
|||
/// </remarks>
|
||||
public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// A proof for (~ P Q) where Q is in negation normal form.
|
||||
///
|
||||
/// This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
///
|
||||
/// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
|
||||
/// </remarks>
|
||||
public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// A proof for (~ P Q) where Q is in conjunctive normal form.
|
||||
/// This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
/// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
|
||||
/// </remarks>
|
||||
public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the term is a proof for a Skolemization step
|
||||
/// </summary>
|
||||
|
|
|
@ -1398,8 +1398,7 @@ public class Expr extends AST
|
|||
/**
|
||||
* Indicates whether the term is a proof by condensed transitivity of a
|
||||
* relation
|
||||
* Remarks: Condensed transitivity proof. This proof object is
|
||||
* only used if the parameter PROOF_MODE is 1. It combines several symmetry
|
||||
* Remarks: Condensed transitivity proof. It combines several symmetry
|
||||
* and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d)
|
||||
* [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.
|
||||
*
|
||||
|
@ -1506,14 +1505,11 @@ public class Expr extends AST
|
|||
/**
|
||||
* Indicates whether the term is a proof by rewriting
|
||||
* Remarks: A proof for
|
||||
* rewriting an expression t into an expression s. This proof object is used
|
||||
* if the parameter PROOF_MODE is 1. This proof object can have n
|
||||
* rewriting an expression t into an expression s. This proof object can have n
|
||||
* antecedents. The antecedents are proofs for equalities used as
|
||||
* substitution rules. The object is also used in a few cases if the
|
||||
* parameter PROOF_MODE is 2. The cases are: - When applying contextual
|
||||
* substitution rules. The object is used in a few cases . The cases are: - When applying contextual
|
||||
* simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to
|
||||
* Booleans (BIT2BOOL=true) - When pulling ite expression up
|
||||
* (PULL_CHEAP_ITE_TREES=true)
|
||||
* Booleans (BIT2BOOL=true)
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
|
@ -1534,17 +1530,6 @@ public class Expr extends AST
|
|||
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the term is a proof for pulling quantifiers out.
|
||||
*
|
||||
* Remarks: A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isProofPullQuantStar()
|
||||
{
|
||||
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the term is a proof for pushing quantifiers in.
|
||||
|
@ -1804,38 +1789,6 @@ public class Expr extends AST
|
|||
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the term is a proof for (~ P Q) here Q is in negation
|
||||
* normal form.
|
||||
* Remarks: A proof for (~ P Q) where Q is in negation normal
|
||||
* form.
|
||||
*
|
||||
* This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
*
|
||||
* This proof object may have n antecedents. Each antecedent is a
|
||||
* PR_DEF_INTRO.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isProofNNFStar()
|
||||
{
|
||||
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the term is a proof for (~ P Q) where Q is in
|
||||
* conjunctive normal form.
|
||||
* Remarks: A proof for (~ P Q) where Q is in
|
||||
* conjunctive normal form. This proof object is only used if the parameter
|
||||
* PROOF_MODE is 1. This proof object may have n antecedents. Each
|
||||
* antecedent is a PR_DEF_INTRO.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isProofCNFStar()
|
||||
{
|
||||
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the term is a proof for a Skolemization step
|
||||
|
|
|
@ -459,7 +459,7 @@ typedef enum
|
|||
[trans T1 T2]: (R t u)
|
||||
}
|
||||
|
||||
- Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
- Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof.
|
||||
It combines several symmetry and transitivity proofs.
|
||||
|
||||
Example:
|
||||
|
@ -539,21 +539,14 @@ typedef enum
|
|||
}
|
||||
|
||||
- Z3_OP_PR_REWRITE_STAR: A proof for rewriting an expression t into an expression s.
|
||||
This proof object is used if the parameter PROOF_MODE is 1.
|
||||
This proof object can have n antecedents.
|
||||
The antecedents are proofs for equalities used as substitution rules.
|
||||
The object is also used in a few cases if the parameter PROOF_MODE is 2.
|
||||
The cases are:
|
||||
The proof rule is used in a few cases. The cases are:
|
||||
- When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
|
||||
- When converting bit-vectors to Booleans (BIT2BOOL=true)
|
||||
- When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
|
||||
|
||||
- Z3_OP_PR_PULL_QUANT: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
|
||||
|
||||
- Z3_OP_PR_PULL_QUANT_STAR: A proof for (iff P Q) where Q is in prenex normal form.
|
||||
This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
This proof object has no antecedents.
|
||||
|
||||
- Z3_OP_PR_PUSH_QUANT: A proof for:
|
||||
|
||||
\nicebox{
|
||||
|
@ -726,15 +719,6 @@ typedef enum
|
|||
[nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
|
||||
(and (or r_1 r_2) (or r_1' r_2')))
|
||||
}
|
||||
- Z3_OP_PR_NNF_STAR: A proof for (~ P Q) where Q is in negation normal form.
|
||||
|
||||
This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
|
||||
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
|
||||
|
||||
- Z3_OP_PR_CNF_STAR: A proof for (~ P Q) where Q is in conjunctive normal form.
|
||||
This proof object is only used if the parameter PROOF_MODE is 1.
|
||||
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
|
||||
|
||||
- Z3_OP_PR_SKOLEMIZE: Proof for:
|
||||
|
||||
|
@ -1142,7 +1126,6 @@ typedef enum {
|
|||
Z3_OP_PR_REWRITE,
|
||||
Z3_OP_PR_REWRITE_STAR,
|
||||
Z3_OP_PR_PULL_QUANT,
|
||||
Z3_OP_PR_PULL_QUANT_STAR,
|
||||
Z3_OP_PR_PUSH_QUANT,
|
||||
Z3_OP_PR_ELIM_UNUSED_VARS,
|
||||
Z3_OP_PR_DER,
|
||||
|
@ -1159,8 +1142,6 @@ typedef enum {
|
|||
Z3_OP_PR_IFF_OEQ,
|
||||
Z3_OP_PR_NNF_POS,
|
||||
Z3_OP_PR_NNF_NEG,
|
||||
Z3_OP_PR_NNF_STAR,
|
||||
Z3_OP_PR_CNF_STAR,
|
||||
Z3_OP_PR_SKOLEMIZE,
|
||||
Z3_OP_PR_MODUS_PONENS_OEQ,
|
||||
Z3_OP_PR_TH_LEMMA,
|
||||
|
|
|
@ -663,7 +663,6 @@ basic_decl_plugin::basic_decl_plugin():
|
|||
m_not_or_elim_decl(nullptr),
|
||||
m_rewrite_decl(nullptr),
|
||||
m_pull_quant_decl(nullptr),
|
||||
m_pull_quant_star_decl(nullptr),
|
||||
m_push_quant_decl(nullptr),
|
||||
m_elim_unused_vars_decl(nullptr),
|
||||
m_der_decl(nullptr),
|
||||
|
@ -827,7 +826,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
|
|||
case PR_REWRITE: return mk_proof_decl("rewrite", k, 0, m_rewrite_decl);
|
||||
case PR_REWRITE_STAR: return mk_proof_decl("rewrite*", k, num_parents, m_rewrite_star_decls);
|
||||
case PR_PULL_QUANT: return mk_proof_decl("pull-quant", k, 0, m_pull_quant_decl);
|
||||
case PR_PULL_QUANT_STAR: return mk_proof_decl("pull-quant*", k, 0, m_pull_quant_star_decl);
|
||||
case PR_PUSH_QUANT: return mk_proof_decl("push-quant", k, 0, m_push_quant_decl);
|
||||
case PR_ELIM_UNUSED_VARS: return mk_proof_decl("elim-unused", k, 0, m_elim_unused_vars_decl);
|
||||
case PR_DER: return mk_proof_decl("der", k, 0, m_der_decl);
|
||||
|
@ -844,8 +842,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
|
|||
case PR_IFF_OEQ: return mk_proof_decl("iff~", k, 1, m_iff_oeq_decl);
|
||||
case PR_NNF_POS: return mk_proof_decl("nnf-pos", k, num_parents, m_nnf_pos_decls);
|
||||
case PR_NNF_NEG: return mk_proof_decl("nnf-neg", k, num_parents, m_nnf_neg_decls);
|
||||
case PR_NNF_STAR: return mk_proof_decl("nnf*", k, num_parents, m_nnf_star_decls);
|
||||
case PR_CNF_STAR: return mk_proof_decl("cnf*", k, num_parents, m_cnf_star_decls);
|
||||
case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl);
|
||||
case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
|
||||
case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
|
||||
|
@ -949,7 +945,6 @@ void basic_decl_plugin::finalize() {
|
|||
DEC_REF(m_not_or_elim_decl);
|
||||
DEC_REF(m_rewrite_decl);
|
||||
DEC_REF(m_pull_quant_decl);
|
||||
DEC_REF(m_pull_quant_star_decl);
|
||||
DEC_REF(m_push_quant_decl);
|
||||
DEC_REF(m_elim_unused_vars_decl);
|
||||
DEC_REF(m_der_decl);
|
||||
|
@ -975,8 +970,6 @@ void basic_decl_plugin::finalize() {
|
|||
DEC_ARRAY_REF(m_apply_def_decls);
|
||||
DEC_ARRAY_REF(m_nnf_pos_decls);
|
||||
DEC_ARRAY_REF(m_nnf_neg_decls);
|
||||
DEC_ARRAY_REF(m_nnf_star_decls);
|
||||
DEC_ARRAY_REF(m_cnf_star_decls);
|
||||
|
||||
DEC_ARRAY_REF(m_th_lemma_decls);
|
||||
DEC_REF(m_hyper_res_decl0);
|
||||
|
@ -2844,12 +2837,6 @@ proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
|
|||
return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
|
||||
if (proofs_disabled())
|
||||
return nullptr;
|
||||
return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
|
||||
if (proofs_disabled())
|
||||
return nullptr;
|
||||
|
@ -3094,15 +3081,6 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
|
|||
return mk_app(m_basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr());
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
|
||||
if (proofs_disabled())
|
||||
return nullptr;
|
||||
ptr_buffer<expr> args;
|
||||
args.append(num_proofs, (expr**) proofs);
|
||||
args.push_back(mk_oeq(s, t));
|
||||
return mk_app(m_basic_family_id, PR_NNF_STAR, args.size(), args.c_ptr());
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_skolemization(expr * q, expr * e) {
|
||||
if (proofs_disabled())
|
||||
return nullptr;
|
||||
|
@ -3111,15 +3089,6 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
|
|||
return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
|
||||
if (proofs_disabled())
|
||||
return nullptr;
|
||||
ptr_buffer<expr> args;
|
||||
args.append(num_proofs, (expr**) proofs);
|
||||
args.push_back(mk_oeq(s, t));
|
||||
return mk_app(m_basic_family_id, PR_CNF_STAR, args.size(), args.c_ptr());
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
|
||||
if (proofs_disabled())
|
||||
return nullptr;
|
||||
|
|
|
@ -1042,11 +1042,11 @@ enum basic_op_kind {
|
|||
|
||||
PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
|
||||
PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
|
||||
PR_PULL_QUANT_STAR, PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
|
||||
PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
|
||||
|
||||
PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
|
||||
|
||||
PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR,
|
||||
PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE,
|
||||
PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
|
||||
};
|
||||
|
||||
|
@ -1080,7 +1080,6 @@ protected:
|
|||
func_decl * m_not_or_elim_decl;
|
||||
func_decl * m_rewrite_decl;
|
||||
func_decl * m_pull_quant_decl;
|
||||
func_decl * m_pull_quant_star_decl;
|
||||
func_decl * m_push_quant_decl;
|
||||
func_decl * m_elim_unused_vars_decl;
|
||||
func_decl * m_der_decl;
|
||||
|
@ -1106,8 +1105,6 @@ protected:
|
|||
ptr_vector<func_decl> m_apply_def_decls;
|
||||
ptr_vector<func_decl> m_nnf_pos_decls;
|
||||
ptr_vector<func_decl> m_nnf_neg_decls;
|
||||
ptr_vector<func_decl> m_nnf_star_decls;
|
||||
ptr_vector<func_decl> m_cnf_star_decls;
|
||||
|
||||
ptr_vector<func_decl> m_th_lemma_decls;
|
||||
func_decl * m_hyper_res_decl0;
|
||||
|
@ -2182,7 +2179,6 @@ public:
|
|||
proof * mk_oeq_rewrite(expr * s, expr * t);
|
||||
proof * mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
|
||||
proof * mk_pull_quant(expr * e, quantifier * q);
|
||||
proof * mk_pull_quant_star(expr * e, quantifier * q);
|
||||
proof * mk_push_quant(quantifier * q, expr * e);
|
||||
proof * mk_elim_unused_vars(quantifier * q, expr * r);
|
||||
proof * mk_der(quantifier * q, expr * r);
|
||||
|
@ -2201,9 +2197,8 @@ public:
|
|||
|
||||
proof * mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
|
||||
proof * mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
|
||||
proof * mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
|
||||
proof * mk_skolemization(expr * q, expr * e);
|
||||
proof * mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
|
||||
|
||||
|
||||
proof * mk_and_elim(proof * p, unsigned i);
|
||||
proof * mk_not_or_elim(proof * p, unsigned i);
|
||||
|
|
|
@ -440,16 +440,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m););
|
||||
return false;
|
||||
}
|
||||
case PR_PULL_QUANT_STAR: {
|
||||
if (match_proof(p) &&
|
||||
match_fact(p, fact) &&
|
||||
match_iff(fact.get(), t1, t2)) {
|
||||
// TBD: check the enchilada.
|
||||
return true;
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m););
|
||||
return false;
|
||||
}
|
||||
case PR_PUSH_QUANT: {
|
||||
if (match_proof(p) &&
|
||||
match_fact(p, fact) &&
|
||||
|
@ -730,10 +720,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
// TBD:
|
||||
return true;
|
||||
}
|
||||
case PR_NNF_STAR: {
|
||||
// TBD:
|
||||
return true;
|
||||
}
|
||||
case PR_SKOLEMIZE: {
|
||||
// (exists ?x (p ?x y)) -> (p (sk y) y)
|
||||
// (not (forall ?x (p ?x y))) -> (not (p (sk y) y))
|
||||
|
@ -755,19 +741,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
|||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
case PR_CNF_STAR: {
|
||||
for (unsigned i = 0; i < proofs.size(); ++i) {
|
||||
if (match_op(proofs[i].get(), PR_DEF_INTRO, terms)) {
|
||||
// ok
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
// coarse grain CNF conversion.
|
||||
return true;
|
||||
}
|
||||
case PR_MODUS_PONENS_OEQ: {
|
||||
if (match_fact(p, fact) &&
|
||||
match_proof(p, p0, p1) &&
|
||||
|
|
|
@ -597,7 +597,6 @@ namespace smt {
|
|||
void theory_arith<Ext>::mk_to_int_axiom(app * n) {
|
||||
SASSERT(m_util.is_to_int(n));
|
||||
ast_manager & m = get_manager();
|
||||
context & ctx = get_context();
|
||||
expr* x = n->get_arg(0);
|
||||
|
||||
// to_int (to_real x) = x
|
||||
|
|
|
@ -5595,6 +5595,8 @@ namespace smt {
|
|||
// merge arg0 and arg1
|
||||
expr * arg0 = to_app(node)->get_arg(0);
|
||||
expr * arg1 = to_app(node)->get_arg(1);
|
||||
SASSERT(arg0 != node);
|
||||
SASSERT(arg1 != node);
|
||||
expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap);
|
||||
expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap);
|
||||
get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
|
||||
|
|
|
@ -582,7 +582,7 @@ struct ctx_simplify_tactic::imp {
|
|||
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
|
||||
expr * t = g.form(i);
|
||||
process(t, r);
|
||||
proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(t, r, 0, nullptr)); // TODO :-)
|
||||
proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(t, r));
|
||||
g.update(i, r, new_pr, g.dep(i));
|
||||
}
|
||||
}
|
||||
|
|
|
@ -382,7 +382,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
|
|||
change |= r != g.form(i);
|
||||
proof* new_pr = nullptr;
|
||||
if (g.proofs_enabled()) {
|
||||
new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
|
||||
new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
|
||||
}
|
||||
g.update(i, r, new_pr, g.dep(i));
|
||||
}
|
||||
|
@ -402,7 +402,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
|
|||
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
|
||||
proof* new_pr = nullptr;
|
||||
if (g.proofs_enabled()) {
|
||||
new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
|
||||
new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
|
||||
}
|
||||
g.update(i, r, new_pr, g.dep(i));
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue