mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

add way to unit test mbp from command line

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-21 14:22:00 -07:00 • committed by Arie Gurfinkel
parent 20300bbf94
commit 7642106e73
4 changed files with 17 additions and 174 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/qe/qe_mbp.h
View file

@ -40,6 +40,8 @@ namespace qe {
virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { };
static expr_ref pick_equality(ast_manager& m, model& model, expr* t);
static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits);
//static void partition_args(model& model, app_ref_vector const& sels, expr_ref_vector& lits);
static void erase(expr_ref_vector& lits, unsigned& i);
static void push_back(expr_ref_vector& lits, expr* lit);
static void mark_rec(expr_mark& visited, expr* e);