mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 03:27:52 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-01-15 11:56:01 -08:00
commit ee36662435
6 changed files with 92 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/dotnet/core/DummyContracts.cs
View file

@ -44,15 +44,21 @@ namespace System.Diagnostics.Contracts
public static class Contract
{
[Conditional("false")]
public static void Ensures(bool b) { }
[Conditional("false")]
public static void Requires(bool b) { }
[Conditional("false")]
public static void Assume(bool b, string msg) { }
[Conditional("false")]
public static void Assert(bool b) { }
public static bool ForAll(bool b) { return true; }
public static bool ForAll(Object c, Func<Object, bool> p) { return true; }
public static bool ForAll(int from, int to, Predicate<int> p) { return true; }
[Conditional("false")]
public static void Invariant(bool b) { }
public static T[] Result<T>() { return new T[1]; }
[Conditional("false")]
public static void EndContractBlock() { }
public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; }
}

16
src/smt/smt_solver.cpp
View file

@ -103,6 +103,7 @@ namespace smt {
virtual void assert_expr(expr * t, expr * a) {
solver_na2as::assert_expr(t, a);
SASSERT(!m_name2assertion.contains(a));
get_manager().inc_ref(t);
m_name2assertion.insert(a, t);
}
@ -112,6 +113,20 @@ namespace smt {
}
virtual void pop_core(unsigned n) {
unsigned cur_sz = m_assumptions.size();
if (n > 0 && cur_sz > 0) {
unsigned lvl = m_scopes.size();
SASSERT(n <= lvl);
unsigned new_lvl = lvl - n;
unsigned old_sz = m_scopes[new_lvl];
for (unsigned i = cur_sz - 1; i >= old_sz; i--) {
expr * key = m_assumptions[i].get();
SASSERT(m_name2assertion.contains(key));
expr * value = m_name2assertion.find(key);
m.dec_ref(value);
m_name2assertion.erase(key);
}
}
m_context.pop(n);
}
@ -274,6 +289,7 @@ namespace smt {
unsigned sz = core.size();
for (unsigned i = 0; i < sz; i++) {
expr_ref name(core[i], m);
SASSERT(m_name2assertion.contains(name));
expr_ref assrtn(m_name2assertion.find(name), m);
collect_pattern_func_decls(assrtn, pattern_fds);
}