mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Added ParamDescr.ToString()

Browse source 
Formatting

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-10-12 16:44:46 +01:00
parent 4d70722769
commit 42c27b7a46
5 changed files with 90 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

76
Microsoft.Z3/Context.cs
View file

@ -50,7 +50,7 @@ namespace Microsoft.Z3
Contract.Requires(settings != null);
IntPtr cfg = Native.Z3_mk_config();
foreach(KeyValuePair<string,string> kv in settings)
foreach (KeyValuePair<string, string> kv in settings)
Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
m_ctx = Native.Z3_mk_context_rc(cfg);
Native.Z3_del_config(cfg);
@ -88,7 +88,7 @@ namespace Microsoft.Z3
/// </summary>
internal Symbol[] MkSymbols(string[] names)
{
Contract.Ensures(names == null || Contract.Result<Symbol[]>() != null);
Contract.Ensures(names == null || Contract.Result<Symbol[]>() != null);
Contract.Ensures(names != null || Contract.Result<Symbol[]>() == null);
Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.Result<Symbol[]>().Length == names.Length);
Contract.Ensures(Contract.Result<Symbol[]>() == null || Contract.ForAll(Contract.Result<Symbol[]>(), s => s != null));
@ -129,7 +129,7 @@ namespace Microsoft.Z3
if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
}
}
/// <summary>
/// Retrieves the Real sort of the context.
@ -204,7 +204,7 @@ namespace Microsoft.Z3
Contract.Requires(domain != null);
Contract.Requires(range != null);
Contract.Ensures(Contract.Result<ArraySort>() != null);
CheckContextMatch(domain);
CheckContextMatch(range);
return new ArraySort(this, domain, range);
@ -392,9 +392,9 @@ namespace Microsoft.Z3
Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
CheckContextMatch(constructor);
cla[i] = new ConstructorList(this, constructor);
n_constr[i] = cla[i].NativeObject;
n_constr[i] = cla[i].NativeObject;
}
IntPtr[] n_res = new IntPtr[n];
IntPtr[] n_res = new IntPtr[n];
Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
DatatypeSort[] res = new DatatypeSort[n];
for (uint i = 0; i < n; i++)
@ -526,7 +526,7 @@ namespace Microsoft.Z3
CheckContextMatch(range);
return new FuncDecl(this, MkSymbol(name), null, range);
}
}
/// <summary>
/// Creates a fresh constant function declaration with a name prefixed with <paramref name="prefix"/>.
@ -728,7 +728,7 @@ namespace Microsoft.Z3
CheckContextMatch(f);
CheckContextMatch(args);
return Expr.Create(this, f, args);
}
}
#region Propositional
/// <summary>
@ -800,7 +800,7 @@ namespace Microsoft.Z3
CheckContextMatch(a);
return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
}
/// <summary>
/// Create an expression representing an if-then-else: <c>ite(t1, t2, t3)</c>.
/// </summary>
@ -895,7 +895,7 @@ namespace Microsoft.Z3
/// </summary>
public ArithExpr MkAdd(params ArithExpr[] t)
{
Contract.Requires(t != null);
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<ArithExpr>() != null);
@ -1167,7 +1167,7 @@ namespace Microsoft.Z3
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
@ -1634,8 +1634,8 @@ namespace Microsoft.Z3
{
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
@ -1658,7 +1658,7 @@ namespace Microsoft.Z3
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
@ -1683,7 +1683,7 @@ namespace Microsoft.Z3
Contract.Requires(t1 != null);
Contract.Requires(t2 != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
@ -1700,7 +1700,7 @@ namespace Microsoft.Z3
{
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
CheckContextMatch(t);
return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
}
@ -2147,7 +2147,7 @@ namespace Microsoft.Z3
{
Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, a => a != null));
CheckContextMatch(args);
return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
}
@ -2213,7 +2213,7 @@ namespace Microsoft.Z3
Contract.Requires(arg1 != null);
Contract.Requires(arg2 != null);
Contract.Ensures(Contract.Result<Expr>() != null);
CheckContextMatch(arg1);
CheckContextMatch(arg2);
return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
@ -2538,7 +2538,7 @@ namespace Microsoft.Z3
Contract.Requires(Contract.ForAll(names, n => n != null));
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
Contract.Ensures(Contract.Result<Quantifier>() != null);
return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
@ -2607,7 +2607,7 @@ namespace Microsoft.Z3
Contract.Requires(Contract.ForAll(names, n => n != null));
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
Contract.Ensures(Contract.Result<Quantifier>() != null);
if (universal)
@ -2626,7 +2626,7 @@ namespace Microsoft.Z3
Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
Contract.Ensures(Contract.Result<Quantifier>() != null);
if (universal)
@ -2702,10 +2702,10 @@ namespace Microsoft.Z3
uint cdn = Symbol.ArrayLength(declNames);
uint cd = AST.ArrayLength(decls);
if (csn != cs || cdn != cd)
throw new Z3Exception("Argument size mismatch");
throw new Z3Exception("Argument size mismatch");
Native.Z3_parse_smtlib_string(nCtx, str,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
}
/// <summary>
@ -2722,7 +2722,7 @@ namespace Microsoft.Z3
throw new Z3Exception("Argument size mismatch");
Native.Z3_parse_smtlib_file(nCtx, fileName,
AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
}
/// <summary>
@ -2811,7 +2811,7 @@ namespace Microsoft.Z3
res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
return res;
}
}
}
/// <summary>
/// Parse the given string using the SMT-LIB2 parser.
@ -2965,7 +2965,7 @@ namespace Microsoft.Z3
Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
Contract.Ensures(Contract.Result<Tactic>() != null);
CheckContextMatch(t1);
CheckContextMatch(t2);
CheckContextMatch(ts);
@ -2982,7 +2982,7 @@ namespace Microsoft.Z3
last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
}
else
else
return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
}
@ -3313,7 +3313,7 @@ namespace Microsoft.Z3
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
@ -3328,7 +3328,7 @@ namespace Microsoft.Z3
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
@ -3343,7 +3343,7 @@ namespace Microsoft.Z3
Contract.Requires(p1 != null);
Contract.Requires(p2 != null);
Contract.Ensures(Contract.Result<Probe>() != null);
CheckContextMatch(p1);
CheckContextMatch(p2);
return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
@ -3423,7 +3423,7 @@ namespace Microsoft.Z3
/// <summary>
/// Create a Fixedpoint context.
/// </summary>
public Fixedpoint MkFixedpoint()
public Fixedpoint MkFixedpoint()
{
Contract.Ensures(Contract.Result<Fixedpoint>() != null);
@ -3464,7 +3464,7 @@ namespace Microsoft.Z3
{
return a.NativeObject;
}
/// <summary>
/// Return a string describing all available parameters to <c>Expr.Simplify</c>.
/// </summary>
@ -3478,14 +3478,10 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieves parameter descriptions for simplifier.
/// </summary>
public ParamDescrs SimplifyParameterDescriptions
{
get
{
return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx));
}
}
public ParamDescrs SimplifyParameterDescriptions
{
get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); }
}
/// <summary>
/// Enable/disable printing of warning messages to the console.

38
Microsoft.Z3/Fixedpoint.cs
View file

@ -34,10 +34,11 @@ namespace Microsoft.Z3
/// </summary>
public string Help
{
get {
get
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject);
}
return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject);
}
}
/// <summary>
@ -56,13 +57,10 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieves parameter descriptions for Fixedpoint solver.
/// </summary>
public ParamDescrs ParameterDescriptions
{
get
{
return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject));
}
}
public ParamDescrs ParameterDescriptions
{
get { return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject)); }
}
/// <summary>
@ -146,7 +144,7 @@ namespace Microsoft.Z3
Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
Context.CheckContextMatch(relations);
Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject,
Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject,
AST.ArrayLength(relations), AST.ArrayToNative(relations));
switch (r)
{
@ -179,7 +177,7 @@ namespace Microsoft.Z3
/// <summary>
/// Update named rule into in the fixedpoint solver.
/// </summary>
public void UpdateRule(BoolExpr rule, Symbol name)
public void UpdateRule(BoolExpr rule, Symbol name)
{
Contract.Requires(rule != null);
@ -210,18 +208,18 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve the number of levels explored for a given predicate.
/// </summary>
public uint GetNumLevels(FuncDecl predicate)
{
return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject);
}
public uint GetNumLevels(FuncDecl predicate)
{
return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject);
}
/// <summary>
/// Retrieve the cover of a predicate.
/// </summary>
public Expr GetCoverDelta(int level, FuncDecl predicate)
{
IntPtr res = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject);
return (res == IntPtr.Zero) ? null : Expr.Create(Context, res);
IntPtr res = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject);
return (res == IntPtr.Zero) ? null : Expr.Create(Context, res);
}
/// <summary>
@ -230,7 +228,7 @@ namespace Microsoft.Z3
/// </summary>
public void AddCover(int level, FuncDecl predicate, Expr property)
{
Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
}
/// <summary>
@ -259,7 +257,7 @@ namespace Microsoft.Z3
public string ToString(BoolExpr[] queries)
{
return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
AST.ArrayLength(queries), AST.ArrayToNative(queries));
}

23
Microsoft.Z3/ParamDescrs.cs
View file

@ -23,7 +23,7 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// A ParameterSet represents a configuration in the form of Symbol/value pairs.
/// A ParamDescrs describes a set of parameters.
/// </summary>
[ContractVerification(true)]
public class ParamDescrs : Z3Object
@ -62,6 +62,27 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// The size of the ParamDescrs.
/// </summary>
public uint Size
{
get { return Native.Z3_param_descrs_size(Context.nCtx, NativeObject); }
}
/// <summary>
/// Retrieves a string representation of the ParamDescrs.
/// </summary>
public override string ToString()
{
String res = "";
Symbol[] n = Names;
if (n.Length > 0) res = n[0].ToString();
for (uint i = 1; i < n.Length; i++)
res += " " + n[i].ToString();
return res;
}
#region Internal
internal ParamDescrs(Context ctx, IntPtr obj)
: base(ctx, obj)

5
Microsoft.Z3/Solver.cs
View file

@ -60,10 +60,7 @@ namespace Microsoft.Z3
/// </summary>
public ParamDescrs ParameterDescriptions
{
get
{
return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject));
}
get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); }
}

26
Microsoft.Z3/Tactic.cs
View file

@ -39,21 +39,19 @@ namespace Microsoft.Z3
get
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_tactic_get_help(Context.nCtx, NativeObject); }
return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
}
}
/// <summary>
/// Retrieves parameter descriptions for Tactics.
/// </summary>
public ParamDescrs ParameterDescriptions
{
get
{
return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject));
}
}
public ParamDescrs ParameterDescriptions
{
get { return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); }
}
/// <summary>
@ -83,7 +81,7 @@ namespace Microsoft.Z3
{
Contract.Requires(g != null);
Contract.Ensures(Contract.Result<ApplyResult>() != null);
return Apply(g);
}
}
@ -103,11 +101,13 @@ namespace Microsoft.Z3
}
#region Internal
internal Tactic(Context ctx, IntPtr obj) : base(ctx, obj)
internal Tactic(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal Tactic(Context ctx, string name) : base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name))
internal Tactic(Context ctx, string name)
: base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name))
{
Contract.Requires(ctx != null);
}
@ -123,7 +123,7 @@ namespace Microsoft.Z3
{
Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
}
};
};
internal override void IncRef(IntPtr o)
{