mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

merge commit

Browse source 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-11-18 15:07:18 -08:00
parent 0d15b6abb7
commit f476f94954
3 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/api/dotnet/Solver.cs
View file

@ -429,11 +429,12 @@ namespace Microsoft.Z3
var lvl = BacktrackLevel;
BacktrackLevel = uint.MaxValue;
ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
if (r.Size == 1 && ((Expr)r[0]).IsFalse) {
var v = r.ToBoolExprArray();
if (v.Length == 1 && v[0].IsFalse) {
break;
}
yield return r.ToBoolExprArray();
if (r.Size == 0) {
yield return v;
if (v.Length == 0) {
break;
}
}

2
src/tactic/generic_model_converter.cpp
View file

@ -87,5 +87,7 @@ void generic_model_converter::collect(ast_pp_util& visitor) {
}
void generic_model_converter::operator()(expr_ref& fml) {
// TODO: traverse expression and retrieve minimum trail index
// TODO: add func = expr starting at that index, removing from table if index is the same
NOT_IMPLEMENTED_YET();
}

8
src/tactic/generic_model_converter.h
View file

@ -32,7 +32,9 @@ class generic_model_converter : public model_converter {
m_f(f, m), m_def(d, m), m_instruction(i) {}
};
ast_manager& m;
vector<entry> m_entries;
vector<entry> m_add_entries;
vector<entry> m_hide_entries;
obj_map<func_decl_ref, unsigned> m_first_idx;
public:
generic_model_converter(ast_manager & m): m(m) {}
@ -40,9 +42,9 @@ public:
void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); }
void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); }
void hide(func_decl * f) { m_hide_entries.push_back(entry(f, 0, m, HIDE)); }
void add(func_decl * d, expr* e) { m_entries.push_back(entry(d, e, m, ADD)); }
void add(func_decl * d, expr* e) { m_add_entries.push_back(entry(d, e, m, ADD)); }
virtual void operator()(model_ref & md, unsigned goal_idx);