mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-06 07:53:59 +00:00
Code Activity

add convex interior generalizer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-06-10 10:51:56 -04:00
parent 455618bb2b
commit 0210156bf0
4 changed files with 192 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/muz_qe/pdr_generalizers.h
View file

@ -73,6 +73,23 @@ namespace pdr {
virtual void collect_statistics(statistics& st) const;
};
class core_convex_hull_generalizer : public core_generalizer {
ast_manager& m;
arith_util a;
expr_ref_vector m_sigma;
expr_ref_vector m_trail;
obj_map<func_decl, expr*> m_left;
obj_map<func_decl, expr*> m_right;
bool mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv);
void mk_convex(expr* fml, unsigned index, expr_ref_vector& conv);
bool mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result);
bool translate(func_decl* fn, unsigned index, expr_ref& result);
public:
core_convex_hull_generalizer(context& ctx);
virtual ~core_convex_hull_generalizer() {}
virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
};
class core_multi_generalizer : public core_generalizer {
core_bool_inductive_generalizer m_gen;
public: