z3-src 500.0.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
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);