mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Register cnf_nnf_simplifier and add nnf2 tactic wrapper

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-21 23:27:28 +00:00
parent 14560cdc33
commit 292cf76b2c
2 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/cnf_nnf.h
View file

@ -63,3 +63,7 @@ public:
void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_defined_names.pop(n); }
};
/*
ADD_SIMPLIFIER("nnf", "put goal in negation normal form.", "alloc(cnf_nnf_simplifier, m, p, s)")
*/

11
src/tactic/core/nnf_tactic.h
View file

@ -58,15 +58,26 @@ Once all negations are pushed inside, the resulting formula is in NNF.
#pragma once
#include "util/params.h"
#include "tactic/dependent_expr_state_tactic.h"
#include "ast/simplifiers/cnf_nnf.h"
class ast_manager;
class tactic;
tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref());
inline tactic * mk_nnf2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
return alloc(dependent_expr_state_tactic, m, p,
[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
return alloc(cnf_nnf_simplifier, m, p, s);
});
}
/*
ADD_TACTIC("snf", "put goal in skolem normal form.", "mk_snf_tactic(m, p)")
ADD_TACTIC("nnf", "put goal in negation normal form.", "mk_nnf_tactic(m, p)")
ADD_TACTIC("nnf2", "put goal in negation normal form.", "mk_nnf2_tactic(m, p)")
*/