mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-28 16:47:36 -08:00
commit 0c445cec57
11 changed files with 69 additions and 57 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/dotnet/Context.cs
View file

@ -113,7 +113,6 @@ namespace Microsoft.Z3
get
{
Contract.Ensures(Contract.Result<BoolSort>() != null);
if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
}
}
@ -134,7 +133,14 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieves the Real sort of the context.
/// </summary>
public RealSort RealSort { get { Contract.Ensures(Contract.Result<RealSort>() != null); if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort; } }
public RealSort RealSort
{
get
{
Contract.Ensures(Contract.Result<RealSort>() != null);
if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
}
}
/// <summary>
/// Create a new Boolean sort.

6
src/api/dotnet/Expr.cs
View file

@ -1532,8 +1532,7 @@ namespace Microsoft.Z3
{
case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort");
case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
}
}
@ -1544,8 +1543,7 @@ namespace Microsoft.Z3
case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort");
case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
}
return new Expr(ctx, obj);

6
src/api/java/Context.java
View file

@ -86,7 +86,6 @@ public class Context extends IDisposable
**/
public BoolSort BoolSort() throws Z3Exception
{
if (m_boolSort == null)
m_boolSort = new BoolSort(this);
return m_boolSort;
@ -97,7 +96,6 @@ public class Context extends IDisposable
**/
public IntSort IntSort() throws Z3Exception
{
if (m_intSort == null)
m_intSort = new IntSort(this);
return m_intSort;
@ -106,8 +104,10 @@ public class Context extends IDisposable
/**
* Retrieves the Real sort of the context.
**/
public RealSort RealSort()
public RealSort RealSort() throws Z3Exception
{
if (m_realSort== null)
m_realSort = new RealSort(this);
return m_realSort;
}

4
src/api/java/Expr.java
View file

@ -1786,8 +1786,6 @@ public class Expr extends AST
return new RatNum(ctx, obj);
case Z3_BV_SORT:
return new BitVecNum(ctx, obj);
case Z3_UNKNOWN_SORT:
throw new Z3Exception("Unknown Sort");
default: ;
}
}
@ -1806,8 +1804,6 @@ public class Expr extends AST
return new ArrayExpr(ctx, obj);
case Z3_DATATYPE_SORT:
return new DatatypeExpr(ctx, obj);
case Z3_UNKNOWN_SORT:
throw new Z3Exception("Unknown Sort");
default: ;
}

4
src/muz_qe/dl_context.cpp
View file

@ -994,7 +994,7 @@ namespace datalog {
p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
p.insert(":print-low-level-smt2", CPK_BOOL, "(default true) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
p.insert(":print-low-level-smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
PRIVATE_PARAMS(
p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL,
@ -1651,7 +1651,7 @@ namespace datalog {
expr_ref_vector rules(m);
svector<symbol> names;
bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
bool print_low_level = m_params.get_bool(":print-low-level-smt2", true);
bool print_low_level = m_params.get_bool(":print-low-level-smt2", false);
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);

21
src/muz_qe/pdr_context.cpp
View file

@ -266,7 +266,7 @@ namespace pdr {
}
else if (is_invariant(tgt_level, curr, false, assumes_level)) {
add_property(curr, tgt_level); // assumes_level?tgt_level:infty_level
add_property(curr, assumes_level?tgt_level:infty_level);
TRACE("pdr", tout << "is invariant: "<< tgt_level << " " << mk_pp(curr, m) << "\n";);
src[i] = src.back();
src.pop_back();
@ -293,9 +293,6 @@ namespace pdr {
bool pred_transformer::add_property1(expr * lemma, unsigned lvl) {
if (is_infty_level(lvl)) {
if (m.is_false(lemma)) {
return false;
}
if (!m_invariants.contains(lemma)) {
TRACE("pdr", tout << "property1: " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
m_invariants.push_back(lemma);
@ -410,7 +407,7 @@ namespace pdr {
add_property(result, level);
}
lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core) {
lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level) {
TRACE("pdr",
tout << "is-reachable: " << head()->get_name() << " level: " << n.level() << "\n";
tout << mk_pp(n.state(), m) << "\n";);
@ -427,6 +424,9 @@ namespace pdr {
tout << mk_pp(n.state(), m) << "\n";);
n.set_model(model);
}
else if (is_sat == l_false) {
uses_level = m_solver.assumes_level();
}
return is_sat;
}
@ -1640,7 +1640,8 @@ namespace pdr {
close_node(n);
}
else {
switch (expand_state(n, cube)) {
bool uses_level = true;
switch (expand_state(n, cube, uses_level)) {
case l_true:
if (n.level() == 0) {
TRACE("pdr", tout << "reachable\n";);
@ -1653,7 +1654,7 @@ namespace pdr {
break;
case l_false: {
core_generalizer::cores cores;
cores.push_back(std::make_pair(cube, true));
cores.push_back(std::make_pair(cube, uses_level));
for (unsigned i = 0; !cores.empty() && i < m_core_generalizers.size(); ++i) {
core_generalizer::cores new_cores;
@ -1666,7 +1667,7 @@ namespace pdr {
bool found_invariant = false;
for (unsigned i = 0; i < cores.size(); ++i) {
expr_ref_vector const& core = cores[i].first;
bool uses_level = cores[i].second;
uses_level = cores[i].second;
found_invariant = !uses_level || found_invariant;
expr_ref ncore(m_pm.mk_not_and(core), m);
TRACE("pdr", tout << "invariant state: " << (uses_level?"":"(inductive) ") << mk_pp(ncore, m) << "\n";);
@ -1690,8 +1691,8 @@ namespace pdr {
// return a property that blocks state and is implied by the
// predicate transformer (or some unfolding of it).
//
lbool context::expand_state(model_node& n, expr_ref_vector& result) {
return n.pt().is_reachable(n, &result);
lbool context::expand_state(model_node& n, expr_ref_vector& result, bool& uses_level) {
return n.pt().is_reachable(n, &result, uses_level);
}
void context::propagate(unsigned max_prop_lvl) {

4
src/muz_qe/pdr_context.h
View file

@ -140,7 +140,7 @@ namespace pdr {
bool propagate_to_next_level(unsigned level);
void add_property(expr * lemma, unsigned lvl); // add property 'p' to state at level.
lbool is_reachable(model_node& n, expr_ref_vector* core);
lbool is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level);
bool is_invariant(unsigned level, expr* co_state, bool inductive, bool& assumes_level, expr_ref_vector* core = 0);
bool check_inductive(unsigned level, expr_ref_vector& state, bool& assumes_level);
@ -309,7 +309,7 @@ namespace pdr {
void close_node(model_node& n);
void check_pre_closed(model_node& n);
void expand_node(model_node& n);
lbool expand_state(model_node& n, expr_ref_vector& cube);
lbool expand_state(model_node& n, expr_ref_vector& cube, bool& uses_level);
void create_children(model_node& n);
expr_ref mk_sat_answer() const;
expr_ref mk_unsat_answer() const;