mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 05:41:23 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-07-14 13:18:16 -07:00
commit d7b3aaffbd
11 changed files with 79 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2134,31 +2134,31 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create an empty set. /// Create an empty set.
/// </summary> /// </summary>
public Expr MkEmptySet(Sort domain) public ArrayExpr MkEmptySet(Sort domain)
{ {
Contract.Requires(domain != null); Contract.Requires(domain != null);
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(domain); CheckContextMatch(domain);
return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject)); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
} }
/// <summary> /// <summary>
/// Create the full set. /// Create the full set.
/// </summary> /// </summary>
public Expr MkFullSet(Sort domain) public ArrayExpr MkFullSet(Sort domain)
{ {
Contract.Requires(domain != null); Contract.Requires(domain != null);
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(domain); CheckContextMatch(domain);
return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject)); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
} }
/// <summary> /// <summary>
/// Add an element to the set. /// Add an element to the set.
/// </summary> /// </summary>
public Expr MkSetAdd(Expr set, Expr element) public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
{ {
Contract.Requires(set != null); Contract.Requires(set != null);
Contract.Requires(element != null); Contract.Requires(element != null);
@ -2166,14 +2166,14 @@ namespace Microsoft.Z3
CheckContextMatch(set); CheckContextMatch(set);
CheckContextMatch(element); CheckContextMatch(element);
return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject)); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
} }
/// <summary> /// <summary>
/// Remove an element from a set. /// Remove an element from a set.
/// </summary> /// </summary>
public Expr MkSetDel(Expr set, Expr element) public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
{ {
Contract.Requires(set != null); Contract.Requires(set != null);
Contract.Requires(element != null); Contract.Requires(element != null);
@ -2181,38 +2181,38 @@ namespace Microsoft.Z3
CheckContextMatch(set); CheckContextMatch(set);
CheckContextMatch(element); CheckContextMatch(element);
return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject)); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
} }
/// <summary> /// <summary>
/// Take the union of a list of sets. /// Take the union of a list of sets.
/// </summary> /// </summary>
public Expr MkSetUnion(params Expr[] args) public ArrayExpr MkSetUnion(params ArrayExpr[] args)
{ {
Contract.Requires(args != null); Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, a => a != null)); Contract.Requires(Contract.ForAll(args, a => a != null));
CheckContextMatch(args); CheckContextMatch(args);
return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args))); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
} }
/// <summary> /// <summary>
/// Take the intersection of a list of sets. /// Take the intersection of a list of sets.
/// </summary> /// </summary>
public Expr MkSetIntersection(params Expr[] args) public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
{ {
Contract.Requires(args != null); Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, a => a != null)); Contract.Requires(Contract.ForAll(args, a => a != null));
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(args); CheckContextMatch(args);
return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args))); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
} }
/// <summary> /// <summary>
/// Take the difference between two sets. /// Take the difference between two sets.
/// </summary> /// </summary>
public Expr MkSetDifference(Expr arg1, Expr arg2) public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
{ {
Contract.Requires(arg1 != null); Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null); Contract.Requires(arg2 != null);
@ -2220,25 +2220,25 @@ namespace Microsoft.Z3
CheckContextMatch(arg1); CheckContextMatch(arg1);
CheckContextMatch(arg2); CheckContextMatch(arg2);
return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject)); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
} }
/// <summary> /// <summary>
/// Take the complement of a set. /// Take the complement of a set.
/// </summary> /// </summary>
public Expr MkSetComplement(Expr arg) public ArrayExpr MkSetComplement(ArrayExpr arg)
{ {
Contract.Requires(arg != null); Contract.Requires(arg != null);
Contract.Ensures(Contract.Result<Expr>() != null); Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(arg); CheckContextMatch(arg);
return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject)); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
} }
/// <summary> /// <summary>
/// Check for set membership. /// Check for set membership.
/// </summary> /// </summary>
public BoolExpr MkSetMembership(Expr elem, Expr set) public BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
{ {
Contract.Requires(elem != null); Contract.Requires(elem != null);
Contract.Requires(set != null); Contract.Requires(set != null);
@ -2252,7 +2252,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Check for subsetness of sets. /// Check for subsetness of sets.
/// </summary> /// </summary>
public BoolExpr MkSetSubset(Expr arg1, Expr arg2) public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
{ {
Contract.Requires(arg1 != null); Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null); Contract.Requires(arg2 != null);

15
src/api/java/AST.java
View file

@ -22,10 +22,8 @@ import com.microsoft.z3.enumerations.Z3_ast_kind;
/** /**
* The abstract syntax tree (AST) class. * The abstract syntax tree (AST) class.
**/ **/
public class AST extends Z3Object public class AST extends Z3Object implements Comparable
{ {
/* Overloaded operators are not translated. */
/** /**
* Object comparison. * Object comparison.
* *
@ -35,7 +33,7 @@ public class AST extends Z3Object
{ {
AST casted = null; AST casted = null;
try try
{ {
casted = AST.class.cast(o); casted = AST.class.cast(o);
} catch (ClassCastException e) } catch (ClassCastException e)
@ -43,8 +41,13 @@ public class AST extends Z3Object
return false; return false;
} }
return this.getNativeObject() == casted.getNativeObject(); return
} (this == casted) ||
(this != null) &&
(casted != null) &&
(getContext().nCtx() == casted.getContext().nCtx()) &&
(Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
}
/** /**
* Object Comparison. * Object Comparison.

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

@ -1725,32 +1725,31 @@ public class Context extends IDisposable
/** /**
* Create an empty set. * Create an empty set.
**/ **/
public Expr mkEmptySet(Sort domain) public ArrayExpr mkEmptySet(Sort domain)
{ {
checkContextMatch(domain); checkContextMatch(domain);
return Expr.create(this, return (ArrayExpr)Expr.create(this,
Native.mkEmptySet(nCtx(), domain.getNativeObject())); Native.mkEmptySet(nCtx(), domain.getNativeObject()));
} }
/** /**
* Create the full set. * Create the full set.
**/ **/
public Expr mkFullSet(Sort domain) public ArrayExpr mkFullSet(Sort domain)
{ {
checkContextMatch(domain); checkContextMatch(domain);
return Expr.create(this, return (ArrayExpr)Expr.create(this,
Native.mkFullSet(nCtx(), domain.getNativeObject())); Native.mkFullSet(nCtx(), domain.getNativeObject()));
} }
/** /**
* Add an element to the set. * Add an element to the set.
**/ **/
public Expr mkSetAdd(Expr set, Expr element) public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
{ {
checkContextMatch(set); checkContextMatch(set);
checkContextMatch(element); checkContextMatch(element);
return Expr.create( return (ArrayExpr)Expr.create(this,
this,
Native.mkSetAdd(nCtx(), set.getNativeObject(), Native.mkSetAdd(nCtx(), set.getNativeObject(),
element.getNativeObject())); element.getNativeObject()));
} }
@ -1758,12 +1757,11 @@ public class Context extends IDisposable
/** /**
* Remove an element from a set. * Remove an element from a set.
**/ **/
public Expr mkSetDel(Expr set, Expr element) public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
{ {
checkContextMatch(set); checkContextMatch(set);
checkContextMatch(element); checkContextMatch(element);
return Expr.create( return (ArrayExpr)Expr.create(this,
this,
Native.mkSetDel(nCtx(), set.getNativeObject(), Native.mkSetDel(nCtx(), set.getNativeObject(),
element.getNativeObject())); element.getNativeObject()));
} }
@ -1771,11 +1769,10 @@ public class Context extends IDisposable
/** /**
* Take the union of a list of sets. * Take the union of a list of sets.
**/ **/
public Expr mkSetUnion(Expr... args) public ArrayExpr mkSetUnion(ArrayExpr... args)
{ {
checkContextMatch(args); checkContextMatch(args);
return Expr.create( return (ArrayExpr)Expr.create(this,
this,
Native.mkSetUnion(nCtx(), (int) args.length, Native.mkSetUnion(nCtx(), (int) args.length,
AST.arrayToNative(args))); AST.arrayToNative(args)));
} }
@ -1783,11 +1780,10 @@ public class Context extends IDisposable
/** /**
* Take the intersection of a list of sets. * Take the intersection of a list of sets.
**/ **/
public Expr mkSetIntersection(Expr... args) public ArrayExpr mkSetIntersection(ArrayExpr... args)
{ {
checkContextMatch(args); checkContextMatch(args);
return Expr.create( return (ArrayExpr)Expr.create(this,
this,
Native.mkSetIntersect(nCtx(), (int) args.length, Native.mkSetIntersect(nCtx(), (int) args.length,
AST.arrayToNative(args))); AST.arrayToNative(args)));
} }
@ -1795,12 +1791,11 @@ public class Context extends IDisposable
/** /**
* Take the difference between two sets. * Take the difference between two sets.
**/ **/
public Expr mkSetDifference(Expr arg1, Expr arg2) public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
{ {
checkContextMatch(arg1); checkContextMatch(arg1);
checkContextMatch(arg2); checkContextMatch(arg2);
return Expr.create( return (ArrayExpr)Expr.create(this,
this,
Native.mkSetDifference(nCtx(), arg1.getNativeObject(), Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
arg2.getNativeObject())); arg2.getNativeObject()));
} }
@ -1808,22 +1803,21 @@ public class Context extends IDisposable
/** /**
* Take the complement of a set. * Take the complement of a set.
**/ **/
public Expr mkSetComplement(Expr arg) public ArrayExpr mkSetComplement(ArrayExpr arg)
{ {
checkContextMatch(arg); checkContextMatch(arg);
return Expr.create(this, return (ArrayExpr)Expr.create(this,
Native.mkSetComplement(nCtx(), arg.getNativeObject())); Native.mkSetComplement(nCtx(), arg.getNativeObject()));
} }
/** /**
* Check for set membership. * Check for set membership.
**/ **/
public BoolExpr mkSetMembership(Expr elem, Expr set) public BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
{ {
checkContextMatch(elem); checkContextMatch(elem);
checkContextMatch(set); checkContextMatch(set);
return (BoolExpr) Expr.create( return (BoolExpr) Expr.create(this,
this,
Native.mkSetMember(nCtx(), elem.getNativeObject(), Native.mkSetMember(nCtx(), elem.getNativeObject(),
set.getNativeObject())); set.getNativeObject()));
} }
@ -1831,12 +1825,11 @@ public class Context extends IDisposable
/** /**
* Check for subsetness of sets. * Check for subsetness of sets.
**/ **/
public BoolExpr mkSetSubset(Expr arg1, Expr arg2) public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
{ {
checkContextMatch(arg1); checkContextMatch(arg1);
checkContextMatch(arg2); checkContextMatch(arg2);
return (BoolExpr) Expr.create( return (BoolExpr) Expr.create(this,
this,
Native.mkSetSubset(nCtx(), arg1.getNativeObject(), Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
arg2.getNativeObject())); arg2.getNativeObject()));
} }

23
src/api/java/FuncDecl.java
View file

@ -26,22 +26,6 @@ import com.microsoft.z3.enumerations.Z3_parameter_kind;
**/ **/
public class FuncDecl extends AST public class FuncDecl extends AST
{ {
/**
* Comparison operator.
*
* @return True if {@code a"/> and <paramref name="b} share the
* same context and are equal, false otherwise.
**/
/* Overloaded operators are not translated. */
/**
* Comparison operator.
*
* @return True if {@code a"/> and <paramref name="b} do not
* share the same context or are not equal, false otherwise.
**/
/* Overloaded operators are not translated. */
/** /**
* Object comparison. * Object comparison.
**/ **/
@ -55,7 +39,12 @@ public class FuncDecl extends AST
return false; return false;
} }
return this.getNativeObject() == casted.getNativeObject(); return
(this == casted) ||
(this != null) &&
(casted != null) &&
(getContext().nCtx() == casted.getContext().nCtx()) &&
(Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
} }
/** /**

9
src/api/java/Sort.java
View file

@ -25,8 +25,6 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
**/ **/
public class Sort extends AST public class Sort extends AST
{ {
/* Overloaded operators are not translated. */
/** /**
* Equality operator for objects of type Sort. * Equality operator for objects of type Sort.
* @param o * @param o
@ -42,7 +40,12 @@ public class Sort extends AST
return false; return false;
} }
return this.getNativeObject() == casted.getNativeObject(); return
(this == casted) ||
(this != null) &&
(casted != null) &&
(getContext().nCtx() == casted.getContext().nCtx()) &&
(Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
} }
/** /**

10
src/ast/ast.cpp
View file

@ -2046,8 +2046,14 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2
} }
app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) { app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
if (decl->get_arity() != num_args && !decl->is_right_associative() && bool type_error =
!decl->is_left_associative() && !decl->is_chainable()) { decl->get_arity() != num_args && !decl->is_right_associative() &&
!decl->is_left_associative() && !decl->is_chainable();
type_error |= (decl->get_arity() != num_args && num_args < 2 &&
decl->get_family_id() == m_basic_family_id && !decl->is_associative());
if (type_error) {
std::ostringstream buffer; std::ostringstream buffer;
buffer << "Wrong number of arguments (" << num_args buffer << "Wrong number of arguments (" << num_args
<< ") passed to function " << mk_pp(decl, *this); << ") passed to function " << mk_pp(decl, *this);

8
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -2975,7 +2975,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
m_bv_util.mk_zero_extend(2, lz)); m_bv_util.mk_zero_extend(2, lz));
shift = m_bv_util.mk_bv_sub(exp_m_lz, shift = m_bv_util.mk_bv_sub(exp_m_lz,
m_bv_util.mk_numeral(bv_sz - 1, ebits + 2)); m_bv_util.mk_numeral(bv_sz, ebits + 2));
shift_neg = m_bv_util.mk_bv_neg(shift); shift_neg = m_bv_util.mk_bv_neg(shift);
bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2); bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift); shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
@ -2987,8 +2987,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
// sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long // sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
// [1][ ... sig ... ][r][g][ ... s ...] // [1][ ... sig ... ][r][g][ ... s ...]
// [ ... ubv ... ][r][g][ ... s ... ] // [ ... ubv ... ][r][g][ ... s ... ]
expr_ref max_shift(m); // expr_ref max_shift(m);
max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz); // max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs); shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz); SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs); dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
@ -3440,7 +3440,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#ifdef Z3DEBUG #ifdef Z3DEBUG
return; // return;
// CMW: This works only for quantifier-free formulas. // CMW: This works only for quantifier-free formulas.
expr_ref new_e(m); expr_ref new_e(m);
new_e = m.mk_fresh_const(prefix, m.get_sort(e)); new_e = m.mk_fresh_const(prefix, m.get_sort(e));

1
src/ast/fpa_decl_plugin.cpp
View file

@ -629,7 +629,6 @@ func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, par
symbol name("fp.to_sbv"); symbol name("fp.to_sbv");
sort * bvs = m_bv_plugin->mk_sort(BV_SORT, 1, parameters); sort * bvs = m_bv_plugin->mk_sort(BV_SORT, 1, parameters);
return m_manager->mk_func_decl(name, arity, domain, bvs, func_decl_info(m_family_id, k, num_parameters, parameters)); return m_manager->mk_func_decl(name, arity, domain, bvs, func_decl_info(m_family_id, k, num_parameters, parameters));
} }
func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,

2
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -125,7 +125,7 @@ protected:
m_solver.assert_expr(fml1); m_solver.assert_expr(fml1);
lbool is_sat = m_solver.check(); lbool is_sat = m_solver.check();
TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";); TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";);
if (is_sat != l_false) { if (is_sat == l_true) {
TRACE("ctx_solver_simplify_tactic", TRACE("ctx_solver_simplify_tactic",
tout << "result is not equivalent to input\n"; tout << "result is not equivalent to input\n";
tout << mk_pp(fml1, m) << "\n";); tout << mk_pp(fml1, m) << "\n";);

6
src/smt/theory_arith_aux.h
View file

@ -1479,9 +1479,9 @@ namespace smt {
SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
SASSERT(min_gain.is_minus_one() || !min_gain.is_neg()); SASSERT(min_gain.is_minus_one() || !min_gain.is_neg());
SASSERT(!is_int(x_i) || min_gain.is_pos()); //SASSERT(!is_int(x_i) || min_gain.is_pos());
SASSERT(!is_int(x_i) || min_gain.is_int()); //SASSERT(!is_int(x_i) || min_gain.is_int());
SASSERT(!is_int(x_i) || max_gain.is_int()); //SASSERT(!is_int(x_i) || max_gain.is_int());
return is_tighter; return is_tighter;
} }

4
src/smt/theory_arith_core.h
View file

@ -3065,6 +3065,10 @@ namespace smt {
SASSERT(v != null_theory_var); SASSERT(v != null_theory_var);
inf_numeral const & val = get_value(v); inf_numeral const & val = get_value(v);
rational num = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational(); rational num = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
if (is_int(v) && !num.is_int()) {
TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";);
num = floor(num);
}
return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v))); return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
} }