1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 Fixedpoints.cs 7 8 Abstract: 9 10 Z3 Managed API: Fixedpoints 11 12 Author: 13 14 Christoph Wintersteiger (cwinter) 2012-03-21 15 16 Notes: 17 18 --*/ 19 20 using System; 21 using System.Diagnostics; 22 using System.Linq; 23 24 namespace Microsoft.Z3 25 { 26 /// <summary> 27 /// Object for managing fixedpoints 28 /// </summary> 29 public class Fixedpoint : Z3Object 30 { 31 32 /// <summary> 33 /// A string that describes all available fixedpoint solver parameters. 34 /// </summary> 35 public string Help 36 { 37 get 38 { 39 return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject); 40 } 41 } 42 43 /// <summary> 44 /// Sets the fixedpoint solver parameters. 45 /// </summary> 46 public Params Parameters 47 { 48 set 49 { 50 Debug.Assert(value != null); 51 Context.CheckContextMatch(value); 52 Native.Z3_fixedpoint_set_params(Context.nCtx, NativeObject, value.NativeObject); 53 } 54 } 55 56 /// <summary> 57 /// Retrieves parameter descriptions for Fixedpoint solver. 58 /// </summary> 59 public ParamDescrs ParameterDescriptions 60 { 61 get { return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject)); } 62 } 63 64 65 /// <summary> 66 /// Assert a constraint (or multiple) into the fixedpoint solver. 67 /// </summary> Assert(params BoolExpr[] constraints)68 public void Assert(params BoolExpr[] constraints) 69 { 70 Debug.Assert(constraints != null); 71 Debug.Assert(constraints.All(c => c != null)); 72 73 Context.CheckContextMatch<BoolExpr>(constraints); 74 foreach (BoolExpr a in constraints) 75 { 76 Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject); 77 } 78 } 79 80 /// <summary> 81 /// Alias for Assert. 82 /// </summary> Add(params BoolExpr[] constraints)83 public void Add(params BoolExpr[] constraints) 84 { 85 Assert(constraints); 86 } 87 88 /// <summary> 89 /// Register predicate as recursive relation. 90 /// </summary> RegisterRelation(FuncDecl f)91 public void RegisterRelation(FuncDecl f) 92 { 93 Debug.Assert(f != null); 94 95 Context.CheckContextMatch(f); 96 Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject); 97 } 98 99 /// <summary> 100 /// Add rule into the fixedpoint solver. 101 /// </summary> AddRule(BoolExpr rule, Symbol name = null)102 public void AddRule(BoolExpr rule, Symbol name = null) 103 { 104 Debug.Assert(rule != null); 105 106 Context.CheckContextMatch(rule); 107 Native.Z3_fixedpoint_add_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name)); 108 } 109 110 /// <summary> 111 /// Add table fact to the fixedpoint solver. 112 /// </summary> AddFact(FuncDecl pred, params uint[] args)113 public void AddFact(FuncDecl pred, params uint[] args) 114 { 115 Debug.Assert(pred != null); 116 Debug.Assert(args != null); 117 118 Context.CheckContextMatch(pred); 119 Native.Z3_fixedpoint_add_fact(Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, args); 120 } 121 122 /// <summary> 123 /// Query the fixedpoint solver. 124 /// A query is a conjunction of constraints. The constraints may include the recursively defined relations. 125 /// The query is satisfiable if there is an instance of the query variables and a derivation for it. 126 /// The query is unsatisfiable if there are no derivations satisfying the query variables. 127 /// </summary> Query(BoolExpr query)128 public Status Query(BoolExpr query) 129 { 130 Debug.Assert(query != null); 131 132 Context.CheckContextMatch(query); 133 Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query(Context.nCtx, NativeObject, query.NativeObject); 134 switch (r) 135 { 136 case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; 137 case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; 138 default: return Status.UNKNOWN; 139 } 140 } 141 142 /// <summary> 143 /// Query the fixedpoint solver. 144 /// A query is an array of relations. 145 /// The query is satisfiable if there is an instance of some relation that is non-empty. 146 /// The query is unsatisfiable if there are no derivations satisfying any of the relations. 147 /// </summary> Query(params FuncDecl[] relations)148 public Status Query(params FuncDecl[] relations) 149 { 150 Debug.Assert(relations != null); 151 Debug.Assert(relations.All(rel => rel != null)); 152 153 Context.CheckContextMatch<FuncDecl>(relations); 154 Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject, 155 AST.ArrayLength(relations), AST.ArrayToNative(relations)); 156 switch (r) 157 { 158 case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; 159 case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; 160 default: return Status.UNKNOWN; 161 } 162 } 163 164 /// <summary> 165 /// Update named rule into in the fixedpoint solver. 166 /// </summary> UpdateRule(BoolExpr rule, Symbol name)167 public void UpdateRule(BoolExpr rule, Symbol name) 168 { 169 Debug.Assert(rule != null); 170 171 Context.CheckContextMatch(rule); 172 Native.Z3_fixedpoint_update_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name)); 173 } 174 175 /// <summary> 176 /// Retrieve satisfying instance or instances of solver, 177 /// or definitions for the recursive predicates that show unsatisfiability. 178 /// </summary> GetAnswer()179 public Expr GetAnswer() 180 { 181 IntPtr ans = Native.Z3_fixedpoint_get_answer(Context.nCtx, NativeObject); 182 return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans); 183 } 184 185 /// <summary> 186 /// Retrieve explanation why fixedpoint engine returned status Unknown. 187 /// </summary> GetReasonUnknown()188 public string GetReasonUnknown() 189 { 190 191 return Native.Z3_fixedpoint_get_reason_unknown(Context.nCtx, NativeObject); 192 } 193 194 /// <summary> 195 /// Retrieve the number of levels explored for a given predicate. 196 /// </summary> GetNumLevels(FuncDecl predicate)197 public uint GetNumLevels(FuncDecl predicate) 198 { 199 return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject); 200 } 201 202 /// <summary> 203 /// Retrieve the cover of a predicate. 204 /// </summary> GetCoverDelta(int level, FuncDecl predicate)205 public Expr GetCoverDelta(int level, FuncDecl predicate) 206 { 207 IntPtr res = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject); 208 return (res == IntPtr.Zero) ? null : Expr.Create(Context, res); 209 } 210 211 /// <summary> 212 /// Add <tt>property</tt> about the <tt>predicate</tt>. 213 /// The property is added at <tt>level</tt>. 214 /// </summary> AddCover(int level, FuncDecl predicate, Expr property)215 public void AddCover(int level, FuncDecl predicate, Expr property) 216 { 217 Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject); 218 } 219 220 /// <summary> 221 /// Retrieve internal string representation of fixedpoint object. 222 /// </summary> ToString()223 public override string ToString() 224 { 225 return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, 0, null); 226 } 227 228 /// <summary> 229 /// Instrument the Datalog engine on which table representation to use for recursive predicate. 230 /// </summary> SetPredicateRepresentation(FuncDecl f, Symbol[] kinds)231 public void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds) 232 { 233 Debug.Assert(f != null); 234 235 Native.Z3_fixedpoint_set_predicate_representation(Context.nCtx, NativeObject, 236 f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds)); 237 238 } 239 240 /// <summary> 241 /// Convert benchmark given as set of axioms, rules and queries to a string. 242 /// </summary> ToString(params BoolExpr[] queries)243 public string ToString(params BoolExpr[] queries) 244 { 245 246 return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, 247 AST.ArrayLength(queries), AST.ArrayToNative(queries)); 248 } 249 250 /// <summary> 251 /// Retrieve set of rules added to fixedpoint context. 252 /// </summary> 253 public BoolExpr[] Rules 254 { 255 get 256 { 257 258 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)); 259 return av.ToBoolExprArray(); 260 } 261 } 262 263 /// <summary> 264 /// Retrieve set of assertions added to fixedpoint context. 265 /// </summary> 266 public BoolExpr[] Assertions 267 { 268 get 269 { 270 271 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)); 272 return av.ToBoolExprArray(); 273 } 274 } 275 276 /// <summary> 277 /// Fixedpoint statistics. 278 /// </summary> 279 public Statistics Statistics 280 { 281 get 282 { 283 284 return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject)); 285 } 286 } 287 288 /// <summary> 289 /// Parse an SMT-LIB2 file with fixedpoint rules. 290 /// Add the rules to the current fixedpoint context. 291 /// Return the set of queries in the file. 292 /// </summary> ParseFile(string file)293 public BoolExpr[] ParseFile(string file) 294 { 295 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)); 296 return av.ToBoolExprArray(); 297 } 298 299 /// <summary> 300 /// Similar to ParseFile. Instead it takes as argument a string. 301 /// </summary> ParseString(string s)302 public BoolExpr[] ParseString(string s) 303 { 304 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)); 305 return av.ToBoolExprArray(); 306 } 307 308 309 #region Internal Fixedpoint(Context ctx, IntPtr obj)310 internal Fixedpoint(Context ctx, IntPtr obj) 311 : base(ctx, obj) 312 { 313 Debug.Assert(ctx != null); 314 } Fixedpoint(Context ctx)315 internal Fixedpoint(Context ctx) 316 : base(ctx, Native.Z3_mk_fixedpoint(ctx.nCtx)) 317 { 318 Debug.Assert(ctx != null); 319 } 320 321 internal class DecRefQueue : IDecRefQueue 322 { DecRefQueue()323 public DecRefQueue() : base() { } DecRefQueue(uint move_limit)324 public DecRefQueue(uint move_limit) : base(move_limit) { } IncRef(Context ctx, IntPtr obj)325 internal override void IncRef(Context ctx, IntPtr obj) 326 { 327 Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj); 328 } 329 DecRef(Context ctx, IntPtr obj)330 internal override void DecRef(Context ctx, IntPtr obj) 331 { 332 Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj); 333 } 334 }; 335 IncRef(IntPtr o)336 internal override void IncRef(IntPtr o) 337 { 338 Context.Fixedpoint_DRQ.IncAndClear(Context, o); 339 base.IncRef(o); 340 } 341 DecRef(IntPtr o)342 internal override void DecRef(IntPtr o) 343 { 344 Context.Fixedpoint_DRQ.Add(o); 345 base.DecRef(o); 346 } 347 #endregion 348 } 349 } 350