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

#pragma once

#include "nlsat/nlsat_types.h"
#include "nlsat/nlsat_clause.h"

namespace nlsat {
    class simplify {
        struct imp;
        imp * m_imp;
    public:
        simplify(solver& s, atom_vector& atoms, clause_vector& clauses, clause_vector& learned, pmanager & pm);
        ~simplify();

        void operator()();
    };
}