mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-17 02:30:01 +00:00
Code Activity

Add factor_simplifier and factor2 tactic wrapping the simplifier

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:45:51 +00:00
parent 886361006f
commit 42d3a13ddf
4 changed files with 318 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/ast/simplifiers/factor_simplifier.h Normal file
View file

@ -0,0 +1,38 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
factor_simplifier.h
Abstract:
Polynomial factorization simplifier.
Author:
Leonardo de Moura (leonardo) 2012-02-03
--*/
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
#include "util/params.h"
class factor_simplifier : public dependent_expr_simplifier {
struct rw_cfg;
struct rw;
params_ref m_params;
scoped_ptr<rw> m_rw;
public:
factor_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s);
char const* name() const override { return "factor"; }
void updt_params(params_ref const& p) override;
void collect_param_descrs(param_descrs& r) override;
void reduce() override;
};
dependent_expr_simplifier* mk_factor_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s);