mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix bug in extraction of models from Horn clauses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-26 14:24:25 -07:00
parent c15275b53b
commit 5b181156b2
2 changed files with 16 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz_qe/horn_subsume_model_converter.h
View file

@ -36,11 +36,13 @@ Subsumption transformation (remove Horn clause):
#define _HORN_SUBSUME_MODEL_CONVERTER_H_
#include "model_converter.h"
#include "th_rewriter.h"
class horn_subsume_model_converter : public model_converter {
ast_manager& m;
func_decl_ref_vector m_funcs;
expr_ref_vector m_bodies;
th_rewriter m_rewrite;
void add_default_false_interpretation(expr* e, model_ref& md);
@ -54,11 +56,11 @@ class horn_subsume_model_converter : public model_converter {
public:
horn_subsume_model_converter(ast_manager& m): m(m), m_funcs(m), m_bodies(m) {}
horn_subsume_model_converter(ast_manager& m): m(m), m_funcs(m), m_bodies(m), m_rewrite(m) {}
bool mk_horn(expr* clause, func_decl_ref& pred, expr_ref& body) const;
bool mk_horn(expr* clause, func_decl_ref& pred, expr_ref& body);
bool mk_horn(app* head, expr* body, func_decl_ref& pred, expr_ref& body_res) const;
bool mk_horn(app* head, expr* body, func_decl_ref& pred, expr_ref& body_res);
void insert(app* head, expr* body);