diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index f3335d80f..afb3e8875 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-16 Notes: - + --*/ using System; @@ -41,7 +41,7 @@ namespace test_mapi /// forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i /// /// Where, finvis a fresh function declaration. - /// + /// public static BoolExpr InjAxiom(Context ctx, FuncDecl f, int i) { Sort[] domain = f.Domain; @@ -155,11 +155,11 @@ namespace test_mapi } /// - /// Assert the axiom: function f is commutative. + /// Assert the axiom: function f is commutative. /// /// /// This example uses the SMT-LIB parser to simplify the axiom construction. - /// + /// private static BoolExpr CommAxiom(Context ctx, FuncDecl f) { Sort t = f.Range; @@ -453,7 +453,7 @@ namespace test_mapi /// /// Sudoku solving example. - /// + /// static void SudokuExample(Context ctx) { Console.WriteLine("SudokuExample"); @@ -649,7 +649,7 @@ namespace test_mapi } /// - /// Prove that f(x, y) = f(w, v) implies y = v when + /// Prove that f(x, y) = f(w, v) implies y = v when /// f is injective in the second argument. /// public static void QuantifierExample3(Context ctx) @@ -687,7 +687,7 @@ namespace test_mapi } /// - /// Prove that f(x, y) = f(w, v) implies y = v when + /// Prove that f(x, y) = f(w, v) implies y = v when /// f is injective in the second argument. /// public static void QuantifierExample4(Context ctx) @@ -726,7 +726,7 @@ namespace test_mapi /// /// Some basic tests. - /// + /// static void BasicTests(Context ctx) { Console.WriteLine("BasicTests"); @@ -759,7 +759,7 @@ namespace test_mapi foreach (BoolExpr a in g.Formulas) solver.Assert(a); - if (solver.Check() != Status.SATISFIABLE) + if (solver.Check() != Status.SATISFIABLE) throw new TestFailedException(); ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g); @@ -965,7 +965,7 @@ namespace test_mapi /// /// Shows how to read an SMT1 file. - /// + /// static void SMT1FileTest(string filename) { Console.Write("SMT File test "); @@ -1020,7 +1020,7 @@ namespace test_mapi // break; // case Z3_ast_kind.Z3_QUANTIFIER_AST: // q.Enqueue(((Quantifier)cur).Args[0]); - // break; + // break; // case Z3_ast_kind.Z3_VAR_AST: break; // case Z3_ast_kind.Z3_NUMERAL_AST: break; // case Z3_ast_kind.Z3_FUNC_DECL_AST: break; @@ -1158,7 +1158,7 @@ namespace test_mapi /// Prove x = y implies g(x) = g(y), and /// disprove x = y implies g(g(x)) = g(y). /// - /// This function demonstrates how to create uninterpreted + /// This function demonstrates how to create uninterpreted /// types and functions. public static void ProveExample1(Context ctx) { @@ -1203,8 +1203,8 @@ namespace test_mapi /// Prove not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 . /// Then, show that z < -1 is not implied. /// - /// This example demonstrates how to combine uninterpreted functions - /// and arithmetic. + /// This example demonstrates how to combine uninterpreted functions + /// and arithmetic. public static void ProveExample2(Context ctx) { Console.WriteLine("ProveExample2"); @@ -1255,7 +1255,7 @@ namespace test_mapi /// /// Show how push & pop can be used to create "backtracking" points. /// - /// This example also demonstrates how big numbers can be + /// This example also demonstrates how big numbers can be /// created in ctx. public static void PushPopExample1(Context ctx) { @@ -1318,7 +1318,7 @@ namespace test_mapi /// /// Tuples. /// - /// Check that the projection of a tuple + /// Check that the projection of a tuple /// returns the corresponding element. public static void TupleExample(Context ctx) { @@ -1328,7 +1328,7 @@ namespace test_mapi TupleSort tuple = ctx.MkTupleSort( ctx.MkSymbol("mk_tuple"), // name of tuple constructor new Symbol[] { ctx.MkSymbol("first"), ctx.MkSymbol("second") }, // names of projection operators - new Sort[] { int_type, int_type } // types of projection operators + new Sort[] { int_type, int_type } // types of projection operators ); FuncDecl first = tuple.FieldDecls[0]; // declarations are for projections FuncDecl second = tuple.FieldDecls[1]; @@ -1342,7 +1342,7 @@ namespace test_mapi } /// - /// Simple bit-vector example. + /// Simple bit-vector example. /// /// /// This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers @@ -1366,7 +1366,7 @@ namespace test_mapi /// /// Find x and y such that: x ^ y - 103 == x * y - /// + /// public static void BitvectorExample2(Context ctx) { Console.WriteLine("BitvectorExample2"); @@ -1446,7 +1446,7 @@ namespace test_mapi /// /// Display the declarations, assumptions and formulas in a SMT-LIB string. - /// + /// public static void ParserExample4(Context ctx) { Console.WriteLine("ParserExample4"); @@ -1504,7 +1504,7 @@ namespace test_mapi /// /// Create an enumeration data type. - /// + /// public static void EnumExample(Context ctx) { Console.WriteLine("EnumExample"); @@ -1603,7 +1603,7 @@ namespace test_mapi /// /// Create a binary tree datatype. - /// + /// public static void TreeExample(Context ctx) { Console.WriteLine("TreeExample"); @@ -1681,14 +1681,14 @@ namespace test_mapi // // Declare the names of the accessors for cons. - // Then declare the sorts of the accessors. + // Then declare the sorts of the accessors. // For this example, all sorts refer to the new types 'forest' and 'tree' // being declared, so we pass in null for both sorts1 and sorts2. // On the other hand, the sort_refs arrays contain the indices of the // two new sorts being declared. The first element in sort1_refs // points to 'tree', which has index 1, the second element in sort1_refs array // points to 'forest', which has index 0. - // + // Symbol[] head_tail1 = new Symbol[] { ctx.MkSymbol("head"), ctx.MkSymbol("tail") }; Sort[] sorts1 = new Sort[] { null, null }; uint[] sort1_refs = new uint[] { 1, 0 }; // the first item points to a tree, the second to a forest @@ -1860,7 +1860,7 @@ namespace test_mapi } /// - /// Demonstrate how to use Pushand Popto + /// Demonstrate how to use Pushand Popto /// control the size of models. /// /// Note: this test is specialized to 32-bit bitvectors. @@ -1954,7 +1954,7 @@ namespace test_mapi /// /// Simplifier example. - /// + /// public static void SimplifierExample(Context ctx) { Console.WriteLine("SimplifierExample"); @@ -1970,7 +1970,7 @@ namespace test_mapi } /// - /// Extract unsatisfiable core example + /// Extract unsatisfiable core example /// public static void UnsatCoreAndProofExample(Context ctx) { @@ -2023,7 +2023,7 @@ namespace test_mapi BoolExpr pb = ctx.MkBoolConst("PredB"); BoolExpr pc = ctx.MkBoolConst("PredC"); BoolExpr pd = ctx.MkBoolConst("PredD"); - + BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc }); BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc }); BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc)); @@ -2042,7 +2042,7 @@ namespace test_mapi if (result == Status.UNSATISFIABLE) { - Console.WriteLine("unsat"); + Console.WriteLine("unsat"); Console.WriteLine("core: "); foreach (Expr c in solver.UnsatCore) { @@ -2066,7 +2066,7 @@ namespace test_mapi Console.WriteLine("{0}", t1); // But you cannot mix numerals of different sorts // even if the size of their domains are the same: - // Console.WriteLine("{0}", ctx.MkEq(s1, t1)); + // Console.WriteLine("{0}", ctx.MkEq(s1, t1)); } public static void FloatingPointExample1(Context ctx) @@ -2084,7 +2084,7 @@ namespace test_mapi BoolExpr a = ctx.MkAnd(ctx.MkFPEq(x, y), ctx.MkFPEq(y, z)); Check(ctx, ctx.MkNot(a), Status.UNSATISFIABLE); - /* nothing is equal to NaN according to floating-point + /* nothing is equal to NaN according to floating-point * equality, so NaN == k should be unsatisfiable. */ FPExpr k = (FPExpr)ctx.MkConst("x", s); FPExpr nan = ctx.MkFPNaN(s); @@ -2125,7 +2125,7 @@ namespace test_mapi FPRMExpr rm = (FPRMExpr)ctx.MkConst(ctx.MkSymbol("rm"), rm_sort); BitVecExpr x = (BitVecExpr)ctx.MkConst(ctx.MkSymbol("x"), ctx.MkBitVecSort(64)); - FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort); + FPExpr y = (FPExpr)ctx.MkConst(ctx.MkSymbol("y"), double_sort); FPExpr fp_val = ctx.MkFP(42, double_sort); BoolExpr c1 = ctx.MkEq(y, fp_val); @@ -2138,7 +2138,7 @@ namespace test_mapi /* Generic solver */ Solver s = ctx.MkSolver(); s.Assert(c5); - + Console.WriteLine(s); if (s.Check() != Status.SATISFIABLE) @@ -2210,8 +2210,8 @@ namespace test_mapi } // These examples need proof generation turned on and auto-config set to false. - using (Context ctx = new Context(new Dictionary() - { {"proof", "true" }, + using (Context ctx = new Context(new Dictionary() + { {"proof", "true" }, {"auto-config", "false" } })) { QuantifierExample3(ctx); diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 446a66bc5..d9064f423 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -28,7 +28,7 @@ Revision History: bool is_numeral_sort(Z3_context c, Z3_sort ty) { sort * _ty = to_sort(ty); family_id fid = _ty->get_family_id(); - if (fid != mk_c(c)->get_arith_fid() && + if (fid != mk_c(c)->get_arith_fid() && fid != mk_c(c)->get_bv_fid() && fid != mk_c(c)->get_datalog_fid() && fid != mk_c(c)->get_fpa_fid()) { @@ -160,7 +160,7 @@ extern "C" { expr* e = to_expr(a); if (!e) { SET_ERROR_CODE(Z3_INVALID_ARG); - return Z3_FALSE; + return Z3_FALSE; } if (mk_c(c)->autil().is_numeral(e, r)) { return Z3_TRUE; @@ -174,11 +174,11 @@ extern "C" { r = rational(v, rational::ui64()); return Z3_TRUE; } - return Z3_FALSE; + return Z3_FALSE; Z3_CATCH_RETURN(Z3_FALSE); } - + Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a) { Z3_TRY; // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. @@ -196,11 +196,11 @@ extern "C" { mpf_rounding_mode rm; if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) { switch (rm) { - case OP_FPA_RM_NEAREST_TIES_TO_EVEN: - return mk_c(c)->mk_external_string("roundNearestTiesToEven"); + case OP_FPA_RM_NEAREST_TIES_TO_EVEN: + return mk_c(c)->mk_external_string("roundNearestTiesToEven"); break; case OP_FPA_RM_NEAREST_TIES_TO_AWAY: - return mk_c(c)->mk_external_string("roundNearestTiesToAway"); + return mk_c(c)->mk_external_string("roundNearestTiesToAway"); break; case OP_FPA_RM_TOWARD_POSITIVE: return mk_c(c)->mk_external_string("roundTowardPositive"); @@ -212,7 +212,7 @@ extern "C" { default: return mk_c(c)->mk_external_string("roundTowardZero"); break; - } + } } else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) { return mk_c(c)->mk_external_string(fu.fm().to_string(tmp)); @@ -261,7 +261,7 @@ extern "C" { Z3_bool Z3_API Z3_get_numeral_small(Z3_context c, Z3_ast a, long long* num, long long* den) { Z3_TRY; - // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. + // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_small(c, a, num, den); RESET_ERROR_CODE(); rational r; @@ -289,8 +289,8 @@ extern "C" { // This function invokes Z3_get_numeral_int64, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_int(c, v, i); RESET_ERROR_CODE(); - if (!i) { - SET_ERROR_CODE(Z3_INVALID_ARG); + if (!i) { + SET_ERROR_CODE(Z3_INVALID_ARG); return Z3_FALSE; } long long l; @@ -301,17 +301,17 @@ extern "C" { return Z3_FALSE; Z3_CATCH_RETURN(Z3_FALSE); } - + Z3_bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned* u) { Z3_TRY; // This function invokes Z3_get_numeral_uint64, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_uint(c, v, u); RESET_ERROR_CODE(); - if (!u) { - SET_ERROR_CODE(Z3_INVALID_ARG); + if (!u) { + SET_ERROR_CODE(Z3_INVALID_ARG); return Z3_FALSE; } - unsigned long long l; + unsigned long long l; if (Z3_get_numeral_uint64(c, v, &l) && (l <= 0xFFFFFFFF)) { *u = static_cast(l); return Z3_TRUE; @@ -319,7 +319,7 @@ extern "C" { return Z3_FALSE; Z3_CATCH_RETURN(Z3_FALSE); } - + Z3_bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, unsigned long long* u) { Z3_TRY; // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. @@ -339,7 +339,7 @@ extern "C" { return Z3_FALSE; Z3_CATCH_RETURN(Z3_FALSE); } - + Z3_bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, long long* i) { Z3_TRY; // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index d56ba4af1..2e08d3dab 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -309,7 +309,7 @@ namespace Microsoft.Z3 /// /// Create a new finite domain sort. - /// The result is a sort + /// The result is a sort /// /// The name used to identify the sort /// The size of the sort @@ -324,9 +324,9 @@ namespace Microsoft.Z3 /// /// Create a new finite domain sort. - /// The result is a sort - /// Elements of the sort are created using , - /// and the elements range from 0 to size-1. + /// The result is a sort + /// Elements of the sort are created using , + /// and the elements range from 0 to size-1. /// /// The name used to identify the sort /// The size of the sort @@ -457,16 +457,16 @@ namespace Microsoft.Z3 /// /// Update a datatype field at expression t with value v. - /// The function performs a record update at t. The field - /// that is passed in as argument is updated with value v, - /// the remainig fields of t are unchanged. - /// - public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) - { - return Expr.Create(this, Native.Z3_datatype_update_field( - nCtx, field.NativeObject, - t.NativeObject, v.NativeObject)); - } + /// The function performs a record update at t. The field + /// that is passed in as argument is updated with value v, + /// the remainig fields of t are unchanged. + /// + public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) + { + return Expr.Create(this, Native.Z3_datatype_update_field( + nCtx, field.NativeObject, + t.NativeObject, v.NativeObject)); + } #endregion #endregion @@ -2613,13 +2613,13 @@ namespace Microsoft.Z3 /// is an array of patterns, is an array /// with the sorts of the bound variables, is an array with the /// 'names' of the bound variables, and is the body of the - /// quantifier. Quantifiers are associated with weights indicating the importance of + /// quantifier. Quantifiers are associated with weights indicating the importance of /// using the quantifier during instantiation. - /// Note that the bound variables are de-Bruijn indices created using . - /// Z3 applies the convention that the last element in and - /// refers to the variable with index 0, the second to last element - /// of and refers to the variable - /// with index 1, etc. + /// Note that the bound variables are de-Bruijn indices created using . + /// Z3 applies the convention that the last element in and + /// refers to the variable with index 0, the second to last element + /// of and refers to the variable + /// with index 1, etc. /// /// the sorts of the bound variables. /// names of the bound variables @@ -2650,8 +2650,8 @@ namespace Microsoft.Z3 /// Create a universal Quantifier. /// /// - /// Creates a universal quantifier using a list of constants that will - /// form the set of bound variables. + /// Creates a universal quantifier using a list of constants that will + /// form the set of bound variables. /// /// public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) @@ -2670,7 +2670,7 @@ namespace Microsoft.Z3 /// Create an existential Quantifier. /// /// - /// Creates an existential quantifier using de-Brujin indexed variables. + /// Creates an existential quantifier using de-Brujin indexed variables. /// (). /// public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) @@ -2692,8 +2692,8 @@ namespace Microsoft.Z3 /// Create an existential Quantifier. /// /// - /// Creates an existential quantifier using a list of constants that will - /// form the set of bound variables. + /// Creates an existential quantifier using a list of constants that will + /// form the set of bound variables. /// /// public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) @@ -4499,7 +4499,7 @@ namespace Microsoft.Z3 readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10); readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10); readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10); - readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10); + readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10); /// /// AST DRQ diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index a20a25935..a49b31f70 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-20 Notes: - + --*/ using System; @@ -23,7 +23,7 @@ using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// - /// Expressions are terms. + /// Expressions are terms. /// [ContractVerification(true)] public class Expr : AST @@ -74,7 +74,7 @@ namespace Microsoft.Z3 /// /// The arguments of the expression. - /// + /// public Expr[] Args { get @@ -109,9 +109,9 @@ namespace Microsoft.Z3 /// /// /// The result is the new expression. The arrays from and to must have size num_exprs. - /// For every i smaller than num_exprs, we must have that + /// For every i smaller than num_exprs, we must have that /// sort of from[i] must be equal to sort of to[i]. - /// + /// public Expr Substitute(Expr[] from, Expr[] to) { Contract.Requires(from != null); @@ -174,7 +174,7 @@ namespace Microsoft.Z3 /// /// Returns a string representation of the expression. - /// + /// public override string ToString() { return base.ToString(); @@ -442,15 +442,15 @@ namespace Microsoft.Z3 get { return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && - (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) + (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_ARRAY_SORT); } } /// - /// Indicates whether the term is an array store. + /// Indicates whether the term is an array store. /// - /// It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). + /// It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). /// Array store takes at least 3 arguments. public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } } @@ -480,7 +480,7 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is an as-array term. /// - /// An as-array term is n array value that behaves as the function graph of the + /// An as-array term is n array value that behaves as the function graph of the /// function passed as parameter. public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } } #endregion @@ -761,21 +761,21 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is a coercion from integer to bit-vector /// - /// This function is not supported by the decision procedures. Only the most + /// This function is not supported by the decision procedures. Only the most /// rudimentary simplification rules are applied to this function. public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } } /// /// Indicates whether the term is a coercion from bit-vector to integer /// - /// This function is not supported by the decision procedures. Only the most + /// This function is not supported by the decision procedures. Only the most /// rudimentary simplification rules are applied to this function. public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } } /// /// Indicates whether the term is a bit-vector carry /// - /// Compute the carry bit in a full-adder. The meaning is given by the + /// Compute the carry bit in a full-adder. The meaning is given by the /// equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } } @@ -795,15 +795,15 @@ namespace Microsoft.Z3 public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } } /// - /// Indicates whether the term is a label literal (used by the Boogie Verification condition generator). + /// Indicates whether the term is a label literal (used by the Boogie Verification condition generator). /// /// A label literal has a set of string parameters. It takes no arguments. public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } } - #endregion + #endregion #region Proof Terms /// - /// Indicates whether the term is a binary equivalence modulo namings. + /// Indicates whether the term is a binary equivalence modulo namings. /// /// This binary predicate is used in proof terms. /// It captures equisatisfiability and equivalence modulo renamings. @@ -838,8 +838,8 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is a proof for (R t t), where R is a reflexive relation. /// - /// This proof object has no antecedents. - /// The only reflexive relations that are used are + /// This proof object has no antecedents. + /// The only reflexive relations that are used are /// equivalence modulo namings, equality and equivalence. /// That is, R is either '~', '=' or 'iff'. public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } } @@ -859,8 +859,8 @@ namespace Microsoft.Z3 /// Indicates whether the term is a proof by transitivity of a relation /// /// - /// Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof - /// for (R t u). + /// Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof + /// for (R t u). /// T1: (R t s) /// T2: (R s u) /// [trans T1 T2]: (R t u) @@ -872,17 +872,17 @@ namespace Microsoft.Z3 /// /// /// Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. - /// It combines several symmetry and transitivity proofs. + /// It combines several symmetry and transitivity proofs. /// Example: /// T1: (R a b) /// T2: (R c b) /// T3: (R c d) - /// [trans* T1 T2 T3]: (R a d) + /// [trans* T1 T2 T3]: (R a d) /// R must be a symmetric and transitive relation. - /// + /// /// Assuming that this proof object is a proof for (R s t), then /// a proof checker must check if it is possible to prove (R s t) - /// using the antecedents, symmetry and transitivity. That is, + /// using the antecedents, symmetry and transitivity. That is, /// if there is a path from s to t, if we view every /// antecedent (R a b) as an edge between a and b. /// @@ -896,14 +896,14 @@ namespace Microsoft.Z3 /// T1: (R t_1 s_1) /// ... /// Tn: (R t_n s_n) - /// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) + /// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) /// Remark: if t_i == s_i, then the antecedent Ti is suppressed. /// That is, reflexivity proofs are supressed to save space. /// public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } } /// - /// Indicates whether the term is a quant-intro proof + /// Indicates whether the term is a quant-intro proof /// /// /// Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). @@ -913,7 +913,7 @@ namespace Microsoft.Z3 public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } } /// - /// Indicates whether the term is a distributivity proof object. + /// Indicates whether the term is a distributivity proof object. /// /// /// Given that f (= or) distributes over g (= and), produces a proof for @@ -923,9 +923,9 @@ namespace Microsoft.Z3 /// (= (f (g a b) (g c d)) /// (g (f a c) (f a d) (f b c) (f b d))) /// where each f and g can have arbitrary number of arguments. - /// + /// /// This proof object has no antecedents. - /// Remark. This rule is used by the CNF conversion pass and + /// Remark. This rule is used by the CNF conversion pass and /// instantiated by f = or, and g = and. /// public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } } @@ -946,7 +946,7 @@ namespace Microsoft.Z3 /// /// Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). /// T1: (not (or l_1 ... l_n)) - /// [not-or-elim T1]: (not l_i) + /// [not-or-elim T1]: (not l_i) /// public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } } @@ -956,16 +956,16 @@ namespace Microsoft.Z3 /// /// A proof for a local rewriting step (= t s). /// The head function symbol of t is interpreted. - /// + /// /// This proof object has no antecedents. - /// The conclusion of a rewrite rule is either an equality (= t s), + /// The conclusion of a rewrite rule is either an equality (= t s), /// an equivalence (iff t s), or equi-satisfiability (~ t s). /// Remark: if f is bool, then = is iff. - /// + /// /// Examples: /// (= (+ x 0) x) /// (= (+ x 1 2) (+ 3 x)) - /// (iff (or x false) x) + /// (iff (or x false) x) /// public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } } @@ -997,8 +997,8 @@ namespace Microsoft.Z3 /// Indicates whether the term is a proof for pulling quantifiers out. /// /// - /// A proof for (iff P Q) where Q is in prenex normal form. - /// This proof object is only used if the parameter PROOF_MODE is 1. + /// A proof for (iff P Q) where Q is in prenex normal form. + /// This proof object is only used if the parameter PROOF_MODE is 1. /// This proof object has no antecedents /// public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } } @@ -1010,8 +1010,8 @@ namespace Microsoft.Z3 /// A proof for: /// (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) /// (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) - /// ... - /// (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) + /// ... + /// (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) /// This proof object has no antecedents /// public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } } @@ -1021,8 +1021,8 @@ namespace Microsoft.Z3 /// /// /// A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) - /// (forall (x_1 ... x_n) p[x_1 ... x_n])) - /// + /// (forall (x_1 ... x_n) p[x_1 ... x_n])) + /// /// It is used to justify the elimination of unused variables. /// This proof object has no antecedents. /// @@ -1035,9 +1035,9 @@ namespace Microsoft.Z3 /// A proof for destructive equality resolution: /// (iff (forall (x) (or (not (= x t)) P[x])) P[t]) /// if x does not occur in t. - /// + /// /// This proof object has no antecedents. - /// + /// /// Several variables can be eliminated simultaneously. /// public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } } @@ -1062,7 +1062,7 @@ namespace Microsoft.Z3 /// /// T1: false /// [lemma T1]: (or (not l_1) ... (not l_n)) - /// + /// /// This proof object has one antecedent: a hypothetical proof for false. /// It converts the proof in a proof for (or (not l_1) ... (not l_n)), /// when T1 contains the hypotheses: l_1, ..., l_n. @@ -1104,9 +1104,9 @@ namespace Microsoft.Z3 /// /// /// [comm]: (= (f a b) (f b a)) - /// + /// /// f is a commutative operator. - /// + /// /// This proof object has no antecedents. /// Remark: if f is bool, then = is iff. /// @@ -1117,7 +1117,7 @@ namespace Microsoft.Z3 /// /// /// Proof object used to justify Tseitin's like axioms: - /// + /// /// (or (not (and p q)) p) /// (or (not (and p q)) q) /// (or (not (and p q r)) p) @@ -1138,7 +1138,7 @@ namespace Microsoft.Z3 /// (or (ite a b c) a (not c)) /// (or (not (not a)) (not a)) /// (or (not a) a) - /// + /// /// This proof object has no antecedents. /// Note: all axioms are propositional tautologies. /// Note also that 'and' and 'or' can take multiple arguments. @@ -1155,19 +1155,19 @@ namespace Microsoft.Z3 /// Introduces a name for a formula/term. /// Suppose e is an expression with free variables x, and def-intro /// introduces the name n(x). The possible cases are: - /// + /// /// When e is of Boolean type: /// [def-intro]: (and (or n (not e)) (or (not n) e)) - /// + /// /// or: /// [def-intro]: (or (not n) e) /// when e only occurs positively. - /// + /// /// When e is of the form (ite cond th el): /// [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el))) - /// + /// /// Otherwise: - /// [def-intro]: (= n e) + /// [def-intro]: (= n e) /// public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } } @@ -1195,7 +1195,7 @@ namespace Microsoft.Z3 /// /// /// Proof for a (positive) NNF step. Example: - /// + /// /// T1: (not s_1) ~ r_1 /// T2: (not s_2) ~ r_2 /// T3: s_1 ~ r_1' @@ -1207,9 +1207,9 @@ namespace Microsoft.Z3 /// (a) When creating the NNF of a positive force quantifier. /// The quantifier is retained (unless the bound variables are eliminated). /// Example - /// T1: q ~ q_new + /// T1: q ~ q_new /// [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new)) - /// + /// /// (b) When recursively creating NNF over Boolean formulas, where the top-level /// connective is changed during NNF conversion. The relevant Boolean connectives /// for NNF_POS are 'implies', 'iff', 'xor', 'ite'. @@ -1223,7 +1223,7 @@ namespace Microsoft.Z3 /// /// /// Proof for a (negative) NNF step. Examples: - /// + /// /// T1: (not s_1) ~ r_1 /// ... /// Tn: (not s_n) ~ r_n @@ -1248,9 +1248,9 @@ namespace Microsoft.Z3 /// /// /// A proof for (~ P Q) where Q is in negation normal form. - /// - /// This proof object is only used if the parameter PROOF_MODE is 1. - /// + /// + /// This proof object is only used if the parameter PROOF_MODE is 1. + /// /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. /// public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } } @@ -1260,8 +1260,8 @@ namespace Microsoft.Z3 /// /// /// A proof for (~ P Q) where Q is in conjunctive normal form. - /// This proof object is only used if the parameter PROOF_MODE is 1. - /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. + /// This proof object is only used if the parameter PROOF_MODE is 1. + /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. /// public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } } @@ -1269,11 +1269,11 @@ namespace Microsoft.Z3 /// Indicates whether the term is a proof for a Skolemization step /// /// - /// Proof for: - /// + /// Proof for: + /// /// [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) /// [sk]: (~ (exists x (p x y)) (p (sk y) y)) - /// + /// /// This proof object has no antecedents. /// public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } } @@ -1285,7 +1285,7 @@ namespace Microsoft.Z3 /// Modus ponens style rule for equi-satisfiability. /// T1: p /// T2: (~ p q) - /// [mp~ T1 T2]: q + /// [mp~ T1 T2]: q /// public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } } @@ -1294,15 +1294,15 @@ namespace Microsoft.Z3 /// /// /// Generic proof for theory lemmas. - /// + /// /// The theory lemma function comes with one or more parameters. /// The first parameter indicates the name of the theory. /// For the theory of arithmetic, additional parameters provide hints for - /// checking the theory lemma. + /// checking the theory lemma. /// The hints for arithmetic are: /// - farkas - followed by rational coefficients. Multiply the coefficients to the /// inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. - /// - triangle-eq - Indicates a lemma related to the equivalence: + /// - triangle-eq - Indicates a lemma related to the equivalence: /// (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) /// - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. /// @@ -1318,7 +1318,7 @@ namespace Microsoft.Z3 get { return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && - Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) + Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_RELATION_SORT); } } @@ -1328,7 +1328,7 @@ namespace Microsoft.Z3 /// /// /// Insert a record into a relation. - /// The function takes n+1 arguments, where the first argument is the relation and the remaining n elements + /// The function takes n+1 arguments, where the first argument is the relation and the remaining n elements /// correspond to the n columns of the relation. /// public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } } @@ -1349,7 +1349,7 @@ namespace Microsoft.Z3 public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } } /// - /// Indicates whether the term is the union or convex hull of two relations. + /// Indicates whether the term is the union or convex hull of two relations. /// /// The function takes two arguments. public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } } @@ -1371,7 +1371,7 @@ namespace Microsoft.Z3 /// /// /// Filter (restrict) a relation with respect to a predicate. - /// The first argument is a relation. + /// The first argument is a relation. /// The second argument is a predicate with free de-Brujin indices /// corresponding to the columns of the relation. /// So the first column in the relation has index 0. @@ -1385,9 +1385,9 @@ namespace Microsoft.Z3 /// Intersect the first relation with respect to negation /// of the second relation (the function takes two arguments). /// Logically, the specification can be described by a function - /// + /// /// target = filter_by_negation(pos, neg, columns) - /// + /// /// where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that /// target are elements in x in pos, such that there is no y in neg that agrees with /// x on the columns c1, d1, .., cN, dN. @@ -1397,7 +1397,7 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is the renaming of a column in a relation /// - /// + /// /// The function takes one argument. /// The parameters contain the renaming as a cycle. /// @@ -1422,10 +1422,10 @@ namespace Microsoft.Z3 /// Indicates whether the term is a relational clone (copy) /// /// - /// Create a fresh copy (clone) of a relation. + /// Create a fresh copy (clone) of a relation. /// The function is logically the identity, but - /// in the context of a register machine allows - /// for terms of kind + /// in the context of a register machine allows + /// for terms of kind /// to perform destructive updates to the first argument. /// public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } } @@ -1481,11 +1481,11 @@ namespace Microsoft.Z3 /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven /// public bool IsFPRMRoundNearestTiesToEven{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } - + /// /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway /// - public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } + public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } /// /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative @@ -1506,11 +1506,11 @@ namespace Microsoft.Z3 /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven /// public bool IsFPRMExprRNE{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } } - + /// /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway /// - public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } + public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } } /// /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative @@ -1530,9 +1530,9 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is a floating-point rounding mode numeral /// - public bool IsFPRMExpr { - get { - return IsApp && + public bool IsFPRMExpr { + get { + return IsApp && (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY|| FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN || FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE || @@ -1540,7 +1540,7 @@ namespace Microsoft.Z3 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO); } } - + /// /// Indicates whether the term is a floating-point +oo /// @@ -1586,7 +1586,7 @@ namespace Microsoft.Z3 /// Indicates whether the term is a floating-point multiplication term /// public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } } - + /// /// Indicates whether the term is a floating-point divison term /// @@ -1680,12 +1680,12 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is a floating-point isNegative predicate term /// - public bool IsFPisNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } } + public bool IsFPisNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } } /// /// Indicates whether the term is a floating-point isPositive predicate term /// - public bool IsFPisPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } } + public bool IsFPisPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } } /// /// Indicates whether the term is a floating-point constructor term @@ -1715,7 +1715,7 @@ namespace Microsoft.Z3 /// /// Indicates whether the term is a floating-point conversion to real term /// - public bool IsFPToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } } + public bool IsFPToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } } /// @@ -1761,8 +1761,8 @@ namespace Microsoft.Z3 #endregion #region Internal - /// - /// Constructor for Expr + /// + /// Constructor for Expr /// internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }