mirror of
https://github.com/Z3Prover/z3
synced 2025-08-28 14:08:55 +00:00
8fe357f1f2
* dev branch for simplification Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * bug fixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * bugfixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix factorization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * separate out simplification functionality * reorder initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * reorder initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Update README.md * initial warppers for seq-map/seq-fold Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * expose fold as well Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add C++ bindings for sequence operations Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add abs function to API Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add parameter validation to ternary and 4-ary functions for API #7219 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add pre-processing and reorder Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add pre-processing and reorder Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
16 lines
No EOL
339 B
C++
16 lines
No EOL
339 B
C++
#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()();
|
|
};
|
|
} |