diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index df502f115..b179d44a5 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-15 Notes: - + --*/ using System; @@ -48,9 +48,9 @@ namespace Microsoft.Z3 /// Constructor. /// /// - /// The following parameters can be set: + /// The following parameters can be set: /// - proof (Boolean) Enable proof generation - /// - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting + /// - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting /// - trace (Boolean) Tracing support for VCC /// - trace_file_name (String) Trace out file for VCC traces /// - timeout (unsigned) default timeout (in milliseconds) used for solvers @@ -59,7 +59,7 @@ namespace Microsoft.Z3 /// - model model generation for solvers, this parameter can be overwritten when creating a solver /// - model_validate validate models produced by solvers /// - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver - /// Note that in previous versions of Z3, this constructor was also used to set global and module parameters. + /// Note that in previous versions of Z3, this constructor was also used to set global and module parameters. /// For this purpose we should now use /// public Context(Dictionary settings) @@ -158,7 +158,7 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort; } } @@ -206,7 +206,7 @@ namespace Microsoft.Z3 /// /// Create a real sort. - /// + /// public RealSort MkRealSort() { Contract.Ensures(Contract.Result() != null); @@ -239,7 +239,7 @@ namespace Microsoft.Z3 /// /// Create a new tuple sort. - /// + /// public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) { Contract.Requires(name != null); @@ -308,7 +308,7 @@ namespace Microsoft.Z3 } /// - /// Create a new finite domain sort. + /// Create a new finite domain sort. /// The result is a sort /// /// The name used to identify the sort @@ -323,9 +323,9 @@ namespace Microsoft.Z3 } /// - /// Create a new finite domain sort. + /// Create a new finite domain sort. /// The result is a sort - /// Elements of the sort are created using , + /// Elements of the sort are created using , /// and the elements range from 0 to size-1. /// /// The name used to identify the sort @@ -346,8 +346,8 @@ namespace Microsoft.Z3 /// name of recognizer function. /// names of the constructor fields. /// field sorts, 0 if the field sort refers to a recursive sort. - /// reference to datatype sort that is an argument to the constructor; - /// if the corresponding sort reference is 0, then the value in sort_refs should be an index + /// reference to datatype sort that is an argument to the constructor; + /// if the corresponding sort reference is 0, then the value in sort_refs should be an index /// referring to one of the recursive datatypes that is declared. public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null) { @@ -459,13 +459,13 @@ 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. + /// the remainig fields of t are unchanged. /// - public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) + 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)); + t.NativeObject, v.NativeObject)); } #endregion @@ -653,7 +653,7 @@ namespace Microsoft.Z3 } /// - /// Creates a fresh Constant of sort and a + /// Creates a fresh Constant of sort and a /// name prefixed with . /// public Expr MkFreshConst(string prefix, Sort range) @@ -679,7 +679,7 @@ namespace Microsoft.Z3 /// /// Create a Boolean constant. - /// + /// public BoolExpr MkBoolConst(Symbol name) { Contract.Requires(name != null); @@ -690,7 +690,7 @@ namespace Microsoft.Z3 /// /// Create a Boolean constant. - /// + /// public BoolExpr MkBoolConst(string name) { Contract.Ensures(Contract.Result() != null); @@ -700,7 +700,7 @@ namespace Microsoft.Z3 /// /// Creates an integer constant. - /// + /// public IntExpr MkIntConst(Symbol name) { Contract.Requires(name != null); @@ -781,7 +781,7 @@ namespace Microsoft.Z3 #region Propositional /// /// The true Term. - /// + /// public BoolExpr MkTrue() { Contract.Ensures(Contract.Result() != null); @@ -791,7 +791,7 @@ namespace Microsoft.Z3 /// /// The false Term. - /// + /// public BoolExpr MkFalse() { Contract.Ensures(Contract.Result() != null); @@ -801,7 +801,7 @@ namespace Microsoft.Z3 /// /// Creates a Boolean value. - /// + /// public BoolExpr MkBool(bool value) { Contract.Ensures(Contract.Result() != null); @@ -839,7 +839,7 @@ namespace Microsoft.Z3 /// /// Mk an expression representing not(a). - /// + /// public BoolExpr MkNot(BoolExpr a) { Contract.Requires(a != null); @@ -849,7 +849,7 @@ namespace Microsoft.Z3 return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject)); } - /// + /// /// Create an expression representing an if-then-else: ite(t1, t2, t3). /// /// An expression with Boolean sort @@ -942,7 +942,7 @@ namespace Microsoft.Z3 #region Arithmetic /// /// Create an expression representing t[0] + t[1] + .... - /// + /// public ArithExpr MkAdd(params ArithExpr[] t) { Contract.Requires(t != null); @@ -955,7 +955,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing t[0] * t[1] * .... - /// + /// public ArithExpr MkMul(params ArithExpr[] t) { Contract.Requires(t != null); @@ -968,7 +968,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing t[0] - t[1] - .... - /// + /// public ArithExpr MkSub(params ArithExpr[] t) { Contract.Requires(t != null); @@ -981,7 +981,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing -t. - /// + /// public ArithExpr MkUnaryMinus(ArithExpr t) { Contract.Requires(t != null); @@ -993,7 +993,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing t1 / t2. - /// + /// public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2) { Contract.Requires(t1 != null); @@ -1037,7 +1037,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing t1 ^ t2. - /// + /// public ArithExpr MkPower(ArithExpr t1, ArithExpr t2) { Contract.Requires(t1 != null); @@ -1051,7 +1051,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing t1 < t2 - /// + /// public BoolExpr MkLt(ArithExpr t1, ArithExpr t2) { Contract.Requires(t1 != null); @@ -1065,7 +1065,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing t1 <= t2 - /// + /// public BoolExpr MkLe(ArithExpr t1, ArithExpr t2) { Contract.Requires(t1 != null); @@ -1079,7 +1079,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing t1 > t2 - /// + /// public BoolExpr MkGt(ArithExpr t1, ArithExpr t2) { Contract.Requires(t1 != null); @@ -1093,7 +1093,7 @@ namespace Microsoft.Z3 /// /// Create an expression representing t1 >= t2 - /// + /// public BoolExpr MkGe(ArithExpr t1, ArithExpr t2) { Contract.Requires(t1 != null); @@ -1370,7 +1370,7 @@ namespace Microsoft.Z3 /// - The \c floor of t1/t2 if \c t2 is different from zero, and t1*t2 >= 0. /// /// - The \c ceiling of t1/t2 if \c t2 is different from zero, and t1*t2 < 0. - /// + /// /// If t2 is zero, then the result is undefined. /// The arguments must have the same bit-vector sort. /// @@ -1389,7 +1389,7 @@ namespace Microsoft.Z3 /// Unsigned remainder. /// /// - /// It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. + /// It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. /// If t2 is zero, then the result is undefined. /// The arguments must have the same bit-vector sort. /// @@ -1446,7 +1446,7 @@ namespace Microsoft.Z3 /// /// Unsigned less-than /// - /// + /// /// The arguments must have the same bit-vector sort. /// public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2) @@ -1463,7 +1463,7 @@ namespace Microsoft.Z3 /// /// Two's complement signed less-than /// - /// + /// /// The arguments must have the same bit-vector sort. /// public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2) @@ -1480,7 +1480,7 @@ namespace Microsoft.Z3 /// /// Unsigned less-than or equal to. /// - /// + /// /// The arguments must have the same bit-vector sort. /// public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2) @@ -1497,7 +1497,7 @@ namespace Microsoft.Z3 /// /// Two's complement signed less-than or equal to. /// - /// + /// /// The arguments must have the same bit-vector sort. /// public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2) @@ -1514,7 +1514,7 @@ namespace Microsoft.Z3 /// /// Unsigned greater than or equal to. /// - /// + /// /// The arguments must have the same bit-vector sort. /// public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2) @@ -1531,7 +1531,7 @@ namespace Microsoft.Z3 /// /// Two's complement signed greater than or equal to. /// - /// + /// /// The arguments must have the same bit-vector sort. /// public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2) @@ -1548,7 +1548,7 @@ namespace Microsoft.Z3 /// /// Unsigned greater-than. /// - /// + /// /// The arguments must have the same bit-vector sort. /// public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2) @@ -1565,7 +1565,7 @@ namespace Microsoft.Z3 /// /// Two's complement signed greater-than. /// - /// + /// /// The arguments must have the same bit-vector sort. /// public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2) @@ -1582,11 +1582,11 @@ namespace Microsoft.Z3 /// /// Bit-vector concatenation. /// - /// + /// /// The arguments must have a bit-vector sort. /// /// - /// The result is a bit-vector of size n1+n2, where n1 (n2) + /// The result is a bit-vector of size n1+n2, where n1 (n2) /// is the size of t1 (t2). /// public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2) @@ -1603,9 +1603,9 @@ namespace Microsoft.Z3 /// /// Bit-vector extraction. /// - /// + /// /// Extract the bits down to from a bitvector of - /// size m to yield a new bitvector of size n, where + /// size m to yield a new bitvector of size n, where /// n = high - low + 1. /// The argument must have a bit-vector sort. /// @@ -1621,7 +1621,7 @@ namespace Microsoft.Z3 /// /// Bit-vector sign extension. /// - /// + /// /// Sign-extends the given bit-vector to the (signed) equivalent bitvector of /// size m+i, where \c m is the size of the given bit-vector. /// The argument must have a bit-vector sort. @@ -1638,7 +1638,7 @@ namespace Microsoft.Z3 /// /// Bit-vector zero extension. /// - /// + /// /// Extend the given bit-vector with zeros to the (unsigned) equivalent /// bitvector of size m+i, where \c m is the size of the /// given bit-vector. @@ -1655,7 +1655,7 @@ namespace Microsoft.Z3 /// /// Bit-vector repetition. - /// + /// /// /// The argument must have a bit-vector sort. /// @@ -1674,10 +1674,10 @@ namespace Microsoft.Z3 /// /// It is equivalent to multiplication by 2^x where \c x is the value of . /// - /// NB. The semantics of shift operations varies between environments. This - /// definition does not necessarily capture directly the semantics of the + /// NB. The semantics of shift operations varies between environments. This + /// definition does not necessarily capture directly the semantics of the /// programming language or assembly architecture you are modeling. - /// + /// /// The arguments must have a bit-vector sort. /// public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2) @@ -1697,10 +1697,10 @@ namespace Microsoft.Z3 /// /// It is equivalent to unsigned division by 2^x where \c x is the value of . /// - /// NB. The semantics of shift operations varies between environments. This - /// definition does not necessarily capture directly the semantics of the + /// NB. The semantics of shift operations varies between environments. This + /// definition does not necessarily capture directly the semantics of the /// programming language or assembly architecture you are modeling. - /// + /// /// The arguments must have a bit-vector sort. /// public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2) @@ -1721,11 +1721,11 @@ namespace Microsoft.Z3 /// It is like logical shift right except that the most significant /// bits of the result always copy the most significant bit of the /// second argument. - /// - /// NB. The semantics of shift operations varies between environments. This - /// definition does not necessarily capture directly the semantics of the + /// + /// NB. The semantics of shift operations varies between environments. This + /// definition does not necessarily capture directly the semantics of the /// programming language or assembly architecture you are modeling. - /// + /// /// The arguments must have a bit-vector sort. /// public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2) @@ -1811,10 +1811,10 @@ namespace Microsoft.Z3 /// Create an bit bit-vector from the integer argument . /// /// - /// NB. This function is essentially treated as uninterpreted. + /// NB. This function is essentially treated as uninterpreted. /// So you cannot expect Z3 to precisely reflect the semantics of this function /// when solving constraints with this function. - /// + /// /// The argument must be of integer sort. /// public BitVecExpr MkInt2BV(uint n, IntExpr t) @@ -1830,15 +1830,15 @@ namespace Microsoft.Z3 /// Create an integer from the bit-vector argument . /// /// - /// If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. - /// So the result is non-negative and in the range [0..2^N-1], where + /// If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. + /// So the result is non-negative and in the range [0..2^N-1], where /// N are the number of bits in . /// If \c is_signed is true, \c t1 is treated as a signed bit-vector. /// - /// NB. This function is essentially treated as uninterpreted. + /// NB. This function is essentially treated as uninterpreted. /// So you cannot expect Z3 to precisely reflect the semantics of this function /// when solving constraints with this function. - /// + /// /// The argument must be of bit-vector sort. /// public IntExpr MkBV2Int(BitVecExpr t, bool signed) @@ -1988,7 +1988,7 @@ namespace Microsoft.Z3 #region Arrays /// /// Create an array constant. - /// + /// public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range) { Contract.Requires(name != null); @@ -2001,7 +2001,7 @@ namespace Microsoft.Z3 /// /// Create an array constant. - /// + /// public ArrayExpr MkArrayConst(string name, Sort domain, Sort range) { Contract.Requires(domain != null); @@ -2012,13 +2012,13 @@ namespace Microsoft.Z3 } /// - /// Array read. + /// Array read. /// /// - /// The argument a is the array and i is the index - /// of the array that gets read. - /// - /// The node a must have an array sort [domain -> range], + /// The argument a is the array and i is the index + /// of the array that gets read. + /// + /// The node a must have an array sort [domain -> range], /// and i must have the sort domain. /// The sort of the result is range. /// @@ -2036,18 +2036,18 @@ namespace Microsoft.Z3 } /// - /// Array update. + /// Array update. /// /// - /// The node a must have an array sort [domain -> range], + /// The node a must have an array sort [domain -> range], /// i must have sort domain, /// v must have sort range. The sort of the result is [domain -> range]. /// The semantics of this function is given by the theory of arrays described in the SMT-LIB /// standard. See http://smtlib.org for more details. - /// The result of this function is an array that is equal to a + /// The result of this function is an array that is equal to a /// (with respect to select) - /// on all indices except for i, where it maps to v - /// (and the select of a with + /// on all indices except for i, where it maps to v + /// (and the select of a with /// respect to i may be a different value). /// /// @@ -2069,7 +2069,7 @@ namespace Microsoft.Z3 /// Create a constant array. /// /// - /// The resulting term is an array, such that a selecton an arbitrary index + /// The resulting term is an array, such that a selecton an arbitrary index /// produces the value v. /// /// @@ -2111,8 +2111,8 @@ namespace Microsoft.Z3 /// Access the array default value. /// /// - /// Produces the default range value, for arrays that can be represented as - /// finite maps with a default range value. + /// Produces the default range value, for arrays that can be represented as + /// finite maps with a default range value. /// public Expr MkTermArray(ArrayExpr array) { @@ -2275,27 +2275,27 @@ namespace Microsoft.Z3 /// /// Create an at-most-k constraint. /// - public BoolExpr MkAtMost(BoolExpr[] args, uint k) + public BoolExpr MkAtMost(BoolExpr[] args, uint k) { Contract.Requires(args != null); Contract.Requires(Contract.Result() != null); CheckContextMatch(args); - return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length, + return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length, AST.ArrayToNative(args), k)); } /// /// Create a pseudo-Boolean less-or-equal constraint. /// - public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k) + public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k) { Contract.Requires(args != null); Contract.Requires(coeffs != null); Contract.Requires(args.Length == coeffs.Length); Contract.Requires(Contract.Result() != null); CheckContextMatch(args); - return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length, - AST.ArrayToNative(args), + return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length, + AST.ArrayToNative(args), coeffs, k)); } #endregion @@ -2304,7 +2304,7 @@ namespace Microsoft.Z3 #region General Numerals /// - /// Create a Term of a given sort. + /// Create a Term of a given sort. /// /// A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*. /// The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. @@ -2320,7 +2320,7 @@ namespace Microsoft.Z3 /// /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - /// It is slightly faster than MakeNumeral since it is not necessary to parse a string. + /// It is slightly faster than MakeNumeral since it is not necessary to parse a string. /// /// Value of the numeral /// Sort of the numeral @@ -2336,7 +2336,7 @@ namespace Microsoft.Z3 /// /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - /// It is slightly faster than MakeNumeral since it is not necessary to parse a string. + /// It is slightly faster than MakeNumeral since it is not necessary to parse a string. /// /// Value of the numeral /// Sort of the numeral @@ -2352,7 +2352,7 @@ namespace Microsoft.Z3 /// /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - /// It is slightly faster than MakeNumeral since it is not necessary to parse a string. + /// It is slightly faster than MakeNumeral since it is not necessary to parse a string. /// /// Value of the numeral /// Sort of the numeral @@ -2368,7 +2368,7 @@ namespace Microsoft.Z3 /// /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. - /// It is slightly faster than MakeNumeral since it is not necessary to parse a string. + /// It is slightly faster than MakeNumeral since it is not necessary to parse a string. /// /// Value of the numeral /// Sort of the numeral @@ -2417,7 +2417,7 @@ namespace Microsoft.Z3 /// /// Create a real numeral. /// - /// value of the numeral. + /// value of the numeral. /// A Term with value and sort Real public RatNum MkReal(int v) { @@ -2429,7 +2429,7 @@ namespace Microsoft.Z3 /// /// Create a real numeral. /// - /// value of the numeral. + /// value of the numeral. /// A Term with value and sort Real public RatNum MkReal(uint v) { @@ -2441,7 +2441,7 @@ namespace Microsoft.Z3 /// /// Create a real numeral. /// - /// value of the numeral. + /// value of the numeral. /// A Term with value and sort Real public RatNum MkReal(long v) { @@ -2453,7 +2453,7 @@ namespace Microsoft.Z3 /// /// Create a real numeral. /// - /// value of the numeral. + /// value of the numeral. /// A Term with value and sort Real public RatNum MkReal(ulong v) { @@ -2478,7 +2478,7 @@ namespace Microsoft.Z3 /// /// Create an integer numeral. /// - /// value of the numeral. + /// value of the numeral. /// A Term with value and sort Integer public IntNum MkInt(int v) { @@ -2490,7 +2490,7 @@ namespace Microsoft.Z3 /// /// Create an integer numeral. /// - /// value of the numeral. + /// value of the numeral. /// A Term with value and sort Integer public IntNum MkInt(uint v) { @@ -2502,7 +2502,7 @@ namespace Microsoft.Z3 /// /// Create an integer numeral. /// - /// value of the numeral. + /// value of the numeral. /// A Term with value and sort Integer public IntNum MkInt(long v) { @@ -2514,7 +2514,7 @@ namespace Microsoft.Z3 /// /// Create an integer numeral. /// - /// value of the numeral. + /// value of the numeral. /// A Term with value and sort Integer public IntNum MkInt(ulong v) { @@ -2540,7 +2540,7 @@ namespace Microsoft.Z3 /// /// Create a bit-vector numeral. /// - /// value of the numeral. + /// value of the numeral. /// the size of the bit-vector public BitVecNum MkBV(int v, uint size) { @@ -2552,7 +2552,7 @@ namespace Microsoft.Z3 /// /// Create a bit-vector numeral. /// - /// value of the numeral. + /// value of the numeral. /// the size of the bit-vector public BitVecNum MkBV(uint v, uint size) { @@ -2593,12 +2593,12 @@ namespace Microsoft.Z3 /// Create a universal Quantifier. /// /// - /// Creates a forall formula, where is the weight, + /// Creates a forall formula, where is the weight, /// 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 using the quantifier during instantiation. + /// the importance of using the quantifier during instantiation. /// /// the sorts of the bound variables. /// names of the bound variables @@ -2725,9 +2725,9 @@ namespace Microsoft.Z3 /// /// /// The default mode for pretty printing expressions is to produce - /// SMT-LIB style output where common subexpressions are printed + /// SMT-LIB style output where common subexpressions are printed /// at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. - /// To print shared common subexpressions only once, + /// To print shared common subexpressions only once, /// use the Z3_PRINT_LOW_LEVEL mode. /// To print in way that conforms to SMT-LIB standards and uses let /// expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT. @@ -2766,13 +2766,13 @@ namespace Microsoft.Z3 } /// - /// Parse the given string using the SMT-LIB parser. + /// Parse the given string using the SMT-LIB parser. /// /// - /// The symbol table of the parser can be initialized using the given sorts and declarations. - /// The symbols in the arrays and - /// don't need to match the names of the sorts and declarations in the arrays - /// and . This is a useful feature since we can use arbitrary names to + /// The symbol table of the parser can be initialized using the given sorts and declarations. + /// The symbols in the arrays and + /// don't need to match the names of the sorts and declarations in the arrays + /// and . This is a useful feature since we can use arbitrary names to /// reference sorts and declarations. /// public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) @@ -2789,7 +2789,7 @@ namespace Microsoft.Z3 } /// - /// Parse the given file using the SMT-LIB parser. + /// Parse the given file using the SMT-LIB parser. /// /// public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) @@ -2894,7 +2894,7 @@ namespace Microsoft.Z3 } /// - /// Parse the given string using the SMT-LIB2 parser. + /// Parse the given string using the SMT-LIB2 parser. /// /// /// A conjunction of assertions in the scope (up to push/pop) at the end of the string. @@ -2914,7 +2914,7 @@ namespace Microsoft.Z3 } /// - /// Parse the given file using the SMT-LIB2 parser. + /// Parse the given file using the SMT-LIB2 parser. /// /// public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) @@ -2938,12 +2938,12 @@ namespace Microsoft.Z3 /// Creates a new Goal. /// /// - /// Note that the Context must have been created with proof generation support if + /// Note that the Context must have been created with proof generation support if /// is set to true here. /// /// Indicates whether model generation should be enabled. /// Indicates whether unsat core generation should be enabled. - /// Indicates whether proof generation should be enabled. + /// Indicates whether proof generation should be enabled. public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false) { Contract.Ensures(Contract.Result() != null); @@ -3002,7 +3002,7 @@ namespace Microsoft.Z3 /// /// Creates a new Tactic. - /// + /// public Tactic MkTactic(string name) { Contract.Ensures(Contract.Result() != null); @@ -3044,7 +3044,7 @@ namespace Microsoft.Z3 /// /// Create a tactic that applies to a Goal and - /// then to every subgoal produced by . + /// then to every subgoal produced by . /// /// /// Shorthand for AndThen. @@ -3075,7 +3075,7 @@ namespace Microsoft.Z3 } /// - /// Create a tactic that applies to a goal for milliseconds. + /// Create a tactic that applies to a goal for milliseconds. /// /// /// If does not terminate within milliseconds, then it fails. @@ -3090,11 +3090,11 @@ namespace Microsoft.Z3 } /// - /// Create a tactic that applies to a given goal if the probe - /// evaluates to true. + /// Create a tactic that applies to a given goal if the probe + /// evaluates to true. /// /// - /// If evaluates to false, then the new tactic behaves like the skip tactic. + /// If evaluates to false, then the new tactic behaves like the skip tactic. /// public Tactic When(Probe p, Tactic t) { @@ -3108,7 +3108,7 @@ namespace Microsoft.Z3 } /// - /// Create a tactic that applies to a given goal if the probe + /// Create a tactic that applies to a given goal if the probe /// evaluates to true and otherwise. /// public Tactic Cond(Probe p, Tactic t1, Tactic t2) @@ -3125,7 +3125,7 @@ namespace Microsoft.Z3 } /// - /// Create a tactic that keeps applying until the goal is not + /// Create a tactic that keeps applying until the goal is not /// modified anymore or the maximum number of iterations is reached. /// public Tactic Repeat(Tactic t, uint max = uint.MaxValue) @@ -3208,7 +3208,7 @@ namespace Microsoft.Z3 } /// - /// Create a tactic that applies the given tactics in parallel. + /// Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). /// public Tactic ParOr(params Tactic[] t) { @@ -3235,7 +3235,7 @@ namespace Microsoft.Z3 } /// - /// Interrupt the execution of a Z3 procedure. + /// Interrupt the execution of a Z3 procedure. /// /// This procedure can be used to interrupt: solvers, simplifiers and tactics. public void Interrupt() @@ -3282,7 +3282,7 @@ namespace Microsoft.Z3 /// /// Creates a new Probe. - /// + /// public Probe MkProbe(string name) { Contract.Ensures(Contract.Result() != null); @@ -3421,13 +3421,13 @@ namespace Microsoft.Z3 #region Solvers /// - /// Creates a new (incremental) solver. + /// Creates a new (incremental) solver. /// /// - /// This solver also uses a set of builtin tactics for handling the first - /// check-sat command, and check-sat commands that take more than a given - /// number of milliseconds to be solved. - /// + /// This solver also uses a set of builtin tactics for handling the first + /// check-sat command, and check-sat commands that take more than a given + /// number of milliseconds to be solved. + /// public Solver MkSolver(Symbol logic = null) { Contract.Ensures(Contract.Result() != null); @@ -3440,7 +3440,7 @@ namespace Microsoft.Z3 /// /// Creates a new (incremental) solver. - /// + /// /// public Solver MkSolver(string logic) { @@ -3450,7 +3450,7 @@ namespace Microsoft.Z3 } /// - /// Creates a new (incremental) solver. + /// Creates a new (incremental) solver. /// public Solver MkSimpleSolver() { @@ -3505,14 +3505,14 @@ namespace Microsoft.Z3 #region RoundingMode Sort /// /// Create the floating-point RoundingMode sort. - /// + /// public FPRMSort MkFPRoundingModeSort() { Contract.Ensures(Contract.Result() != null); return new FPRMSort(this); } #endregion - + #region Numerals /// /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. @@ -3602,7 +3602,7 @@ namespace Microsoft.Z3 { Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx)); - } + } #endregion #endregion @@ -3690,12 +3690,12 @@ namespace Microsoft.Z3 return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx)); } #endregion - + #region Numerals /// /// Create a NaN of sort s. - /// - /// FloatingPoint sort. + /// + /// FloatingPoint sort. public FPNum MkFPNaN(FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3704,8 +3704,8 @@ namespace Microsoft.Z3 /// /// Create a floating-point infinity of sort s. - /// - /// FloatingPoint sort. + /// + /// FloatingPoint sort. /// indicates whether the result should be negative. public FPNum MkFPInf(FPSort s, bool negative) { @@ -3715,8 +3715,8 @@ namespace Microsoft.Z3 /// /// Create a floating-point zero of sort s. - /// - /// FloatingPoint sort. + /// + /// FloatingPoint sort. /// indicates whether the result should be negative. public FPNum MkFPZero(FPSort s, bool negative) { @@ -3726,9 +3726,9 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from a float. - /// + /// /// numeral value. - /// FloatingPoint sort. + /// FloatingPoint sort. public FPNum MkFPNumeral(float v, FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3737,7 +3737,7 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from a float. - /// + /// /// numeral value. /// FloatingPoint sort. public FPNum MkFPNumeral(double v, FPSort s) @@ -3748,9 +3748,9 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from an int. - /// + /// /// numeral value. - /// FloatingPoint sort. + /// FloatingPoint sort. public FPNum MkFPNumeral(int v, FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3759,11 +3759,11 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from a sign bit and two integers. - /// + /// /// the sign. /// the significand. /// the exponent. - /// FloatingPoint sort. + /// FloatingPoint sort. public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3772,11 +3772,11 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. - /// + /// /// the sign. /// the significand. /// the exponent. - /// FloatingPoint sort. + /// FloatingPoint sort. public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3785,9 +3785,9 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from a float. - /// + /// /// numeral value. - /// FloatingPoint sort. + /// FloatingPoint sort. public FPNum MkFP(float v, FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3796,7 +3796,7 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from a float. - /// + /// /// numeral value. /// FloatingPoint sort. public FPNum MkFP(double v, FPSort s) @@ -3807,9 +3807,9 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from an int. - /// + /// /// numeral value. - /// FloatingPoint sort. + /// FloatingPoint sort. public FPNum MkFP(int v, FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3818,11 +3818,11 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from a sign bit and two integers. - /// - /// the sign. + /// + /// the sign. /// the exponent. /// the significand. - /// FloatingPoint sort. + /// FloatingPoint sort. public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3831,11 +3831,11 @@ namespace Microsoft.Z3 /// /// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. - /// - /// the sign. + /// + /// the sign. /// the exponent. /// the significand. - /// FloatingPoint sort. + /// FloatingPoint sort. public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s) { Contract.Ensures(Contract.Result() != null); @@ -3849,17 +3849,17 @@ namespace Microsoft.Z3 /// Floating-point absolute value /// /// floating-point term - public FPExpr MkFPAbs(FPExpr t) + public FPExpr MkFPAbs(FPExpr t) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject)); } - + /// /// Floating-point negation /// /// floating-point term - public FPExpr MkFPNeg(FPExpr t) + public FPExpr MkFPNeg(FPExpr t) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject)); @@ -3871,7 +3871,7 @@ namespace Microsoft.Z3 /// rounding mode term /// floating-point term /// floating-point term - public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) + public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject)); @@ -3883,36 +3883,36 @@ namespace Microsoft.Z3 /// rounding mode term /// floating-point term /// floating-point term - public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) + public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject)); } - + /// /// Floating-point multiplication /// /// rounding mode term /// floating-point term /// floating-point term - public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) + public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject)); } - + /// /// Floating-point division /// /// rounding mode term /// floating-point term /// floating-point term - public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) + public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject)); } - + /// /// Floating-point fused multiply-add /// @@ -3923,49 +3923,49 @@ namespace Microsoft.Z3 /// floating-point term /// floating-point term /// floating-point term - public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) + public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject)); } - + /// /// Floating-point square root - /// - /// rounding mode term - /// floating-point term - public FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t) + /// + /// rounding mode term + /// floating-point term + public FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject)); } - + /// /// Floating-point remainder - /// + /// /// floating-point term /// floating-point term - public FPExpr MkFPRem(FPExpr t1, FPExpr t2) + public FPExpr MkFPRem(FPExpr t1, FPExpr t2) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject)); } /// - /// Floating-point roundToIntegral. Rounds a floating-point number to + /// Floating-point roundToIntegral. Rounds a floating-point number to /// the closest integer, again represented as a floating-point number. - /// + /// /// term of RoundingMode sort /// floating-point term public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t) - { + { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject)); } /// /// Minimum of floating-point numbers. - /// + /// /// floating-point term /// floating-point term public FPExpr MkFPMin(FPExpr t1, FPExpr t2) @@ -3976,55 +3976,55 @@ namespace Microsoft.Z3 /// /// Maximum of floating-point numbers. - /// + /// /// floating-point term /// floating-point term public FPExpr MkFPMax(FPExpr t1, FPExpr t2) { Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject)); - } - + } + /// /// Floating-point less than or equal. - /// + /// /// floating-point term /// floating-point term - public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2) - { + public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2) + { Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject)); } /// /// Floating-point less than. - /// + /// /// floating-point term /// floating-point term - public BoolExpr MkFPLt(FPExpr t1, FPExpr t2) - { + public BoolExpr MkFPLt(FPExpr t1, FPExpr t2) + { Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject)); } - + /// /// Floating-point greater than or equal. - /// + /// /// floating-point term /// floating-point term - public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2) - { + public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2) + { Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject)); } /// /// Floating-point greater than. - /// + /// /// floating-point term /// floating-point term - public BoolExpr MkFPGt(FPExpr t1, FPExpr t2) - { + public BoolExpr MkFPGt(FPExpr t1, FPExpr t2) + { Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject)); } @@ -4045,28 +4045,28 @@ namespace Microsoft.Z3 /// /// Predicate indicating whether t is a normal floating-point number. - /// - /// floating-point term - public BoolExpr MkFPIsNormal(FPExpr t) - { + /// + /// floating-point term + public BoolExpr MkFPIsNormal(FPExpr t) + { Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject)); } - + /// /// Predicate indicating whether t is a subnormal floating-point number. - /// - /// floating-point term - public BoolExpr MkFPIsSubnormal(FPExpr t) - { + /// + /// floating-point term + public BoolExpr MkFPIsSubnormal(FPExpr t) + { Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject)); } /// /// Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0. - /// - /// floating-point term + /// + /// floating-point term public BoolExpr MkFPIsZero(FPExpr t) { Contract.Ensures(Contract.Result() != null); @@ -4075,8 +4075,8 @@ namespace Microsoft.Z3 /// /// Predicate indicating whether t is a floating-point number representing +oo or -oo. - /// - /// floating-point term + /// + /// floating-point term public BoolExpr MkFPIsInfinite(FPExpr t) { Contract.Ensures(Contract.Result() != null); @@ -4085,18 +4085,18 @@ namespace Microsoft.Z3 /// /// Predicate indicating whether t is a NaN. - /// - /// floating-point term - public BoolExpr MkFPIsNaN(FPExpr t) - { + /// + /// floating-point term + public BoolExpr MkFPIsNaN(FPExpr t) + { Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject)); } /// /// Predicate indicating whether t is a negative floating-point number. - /// - /// floating-point term + /// + /// floating-point term public BoolExpr MkFPIsNegative(FPExpr t) { Contract.Ensures(Contract.Result() != null); @@ -4105,13 +4105,13 @@ namespace Microsoft.Z3 /// /// Predicate indicating whether t is a positive floating-point number. - /// - /// floating-point term + /// + /// floating-point term public BoolExpr MkFPIsPositive(FPExpr t) { Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject)); - } + } #endregion #region Conversions to FloatingPoint terms @@ -4119,9 +4119,9 @@ namespace Microsoft.Z3 /// Create an expression of FloatingPoint sort from three bit-vector expressions. /// /// - /// This is the operator named `fp' in the SMT FP theory definition. - /// Note that sgn is required to be a bit-vector of size 1. Significand and exponent - /// are required to be greater than 1 and 2 respectively. The FloatingPoint sort + /// This is the operator named `fp' in the SMT FP theory definition. + /// Note that sgn is required to be a bit-vector of size 1. Significand and exponent + /// are required to be greater than 1 and 2 respectively. The FloatingPoint sort /// of the resulting expression is automatically determined from the bit-vector sizes /// of the arguments. /// @@ -4138,9 +4138,9 @@ namespace Microsoft.Z3 /// Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. /// /// - /// Produces a term that represents the conversion of a bit-vector term bv to a - /// floating-point term of sort s. The bit-vector size of bv (m) must be equal - /// to ebits+sbits of s. The format of the bit-vector is as defined by the + /// Produces a term that represents the conversion of a bit-vector term bv to a + /// floating-point term of sort s. The bit-vector size of bv (m) must be equal + /// to ebits+sbits of s. The format of the bit-vector is as defined by the /// IEEE 754-2008 interchange format. /// /// bit-vector value (of size m). @@ -4190,8 +4190,8 @@ namespace Microsoft.Z3 /// /// /// Produces a term that represents the conversion of the bit-vector term t into a - /// floating-point term of sort s. The bit-vector t is taken to be in signed - /// 2's complement format (when signed==true, otherwise unsigned). If necessary, the + /// floating-point term of sort s. The bit-vector t is taken to be in signed + /// 2's complement format (when signed==true, otherwise unsigned). If necessary, the /// result will be rounded according to rounding mode rm. /// /// RoundingMode term. @@ -4212,7 +4212,7 @@ namespace Microsoft.Z3 /// /// /// Produces a term that represents the conversion of a floating-point term t to a different - /// FloatingPoint sort s. If necessary, rounding according to rm is applied. + /// FloatingPoint sort s. If necessary, rounding according to rm is applied. /// /// FloatingPoint sort /// floating-point rounding mode term @@ -4230,9 +4230,9 @@ namespace Microsoft.Z3 /// /// /// Produces a term that represents the conversion of the floating-poiunt term t into a - /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, + /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, /// the result will be rounded according to rounding mode rm. - /// + /// /// RoundingMode term. /// FloatingPoint term /// Size of the resulting bit-vector. @@ -4251,9 +4251,9 @@ namespace Microsoft.Z3 /// /// /// Produces a term that represents the conversion of the floating-poiunt term t into a - /// real number. Note that this type of conversion will often result in non-linear + /// real number. Note that this type of conversion will often result in non-linear /// constraints over real terms. - /// + /// /// FloatingPoint term public RealExpr MkFPToReal(FPExpr t) { @@ -4267,10 +4267,10 @@ namespace Microsoft.Z3 /// Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. /// /// - /// The size of the resulting bit-vector is automatically determined. Note that - /// IEEE 754-2008 allows multiple different representations of NaN. This conversion - /// knows only one NaN and it will always produce the same bit-vector represenatation of - /// that NaN. + /// The size of the resulting bit-vector is automatically determined. Note that + /// IEEE 754-2008 allows multiple different representations of NaN. This conversion + /// knows only one NaN and it will always produce the same bit-vector represenatation of + /// that NaN. /// /// FloatingPoint term. public BitVecExpr MkFPToIEEEBV(FPExpr t) @@ -4283,13 +4283,13 @@ namespace Microsoft.Z3 /// Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. /// /// - /// Produces a term that represents the conversion of sig * 2^exp into a + /// Produces a term that represents the conversion of sig * 2^exp into a /// floating-point term of sort s. If necessary, the result will be rounded /// according to rounding mode rm. /// /// RoundingMode term. /// Exponent term of Int sort. - /// Significand term of Real sort. + /// Significand term of Real sort. /// FloatingPoint sort. public BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) { @@ -4303,10 +4303,10 @@ namespace Microsoft.Z3 /// /// Wraps an AST. /// - /// This function is used for transitions between native and - /// managed objects. Note that must be a + /// This function is used for transitions between native and + /// managed objects. Note that must be a /// native object obtained from Z3 (e.g., through ) - /// and that it must have a correct reference count (see e.g., + /// and that it must have a correct reference count (see e.g., /// . /// /// The native pointer to wrap. @@ -4319,11 +4319,11 @@ namespace Microsoft.Z3 /// /// Unwraps an AST. /// - /// This function is used for transitions between native and - /// managed objects. It returns the native pointer to the AST. Note that + /// This function is used for transitions between native and + /// managed objects. It returns the native pointer to the AST. Note that /// AST objects are reference counted and unwrapping an AST disables automatic - /// reference counting, i.e., all references to the IntPtr that is returned - /// must be handled externally and through native calls (see e.g., + /// reference counting, i.e., all references to the IntPtr that is returned + /// must be handled externally and through native calls (see e.g., /// ). /// /// The AST to unwrap. @@ -4348,16 +4348,16 @@ namespace Microsoft.Z3 public ParamDescrs SimplifyParameterDescriptions { get { return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx)); } - } + } #endregion #region Error Handling ///// ///// A delegate which is executed when an error is raised. - ///// + ///// ///// ///// Note that it is possible for memory leaks to occur if error handlers - ///// throw exceptions. + ///// throw exceptions. ///// //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString); @@ -4392,7 +4392,7 @@ namespace Microsoft.Z3 internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode) { - // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors. + // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors. } internal void InitContext() @@ -4474,7 +4474,7 @@ namespace Microsoft.Z3 /// ASTMap DRQ /// public IDecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ASTMap_DRQ; } } - + /// /// ASTVector DRQ /// @@ -4534,7 +4534,7 @@ namespace Microsoft.Z3 /// Tactic DRQ /// public IDecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Tactic_DRQ; } } - + /// /// FixedPoint DRQ /// diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 1bc01857b..4497e6970 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2563,7 +2563,7 @@ public class Context extends IDisposable } /** - * Create a tactic that applies the given tactics in parallel. + * Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). **/ public Tactic parOr(Tactic... t) { diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 02f29d080..32ca24128 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2941,7 +2941,7 @@ sig Alias for [UsingParams]*) val with_ : context -> tactic -> Params.params -> tactic - (** Create a tactic that applies the given tactics in parallel. *) + (** Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). *) val par_or : context -> tactic list -> tactic (** Create a tactic that applies a tactic to a given goal and then another tactic diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index ab2ad3922..de5abb874 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -37,7 +37,7 @@ tactic_cmd::~tactic_cmd() { } tactic * tactic_cmd::mk(ast_manager & m) { - return (*m_factory)(m, params_ref()); + return (*m_factory)(m, params_ref()); } probe_info::probe_info(symbol const & n, char const * d, probe * p): @@ -62,12 +62,12 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "declare a new tactic, use (help-tactic) for the tactic language syntax."; } virtual unsigned get_arity() const { return 2; } virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_decl = 0; } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { if (m_name == symbol::null) return CPK_SYMBOL; return CPK_SEXPR; } virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_name = s; } - virtual void set_next_arg(cmd_context & ctx, sexpr * n) { m_decl = n; } + virtual void set_next_arg(cmd_context & ctx, sexpr * n) { m_decl = n; } virtual void execute(cmd_context & ctx) { tactic_ref t = sexpr2tactic(ctx, m_decl); // make sure the tactic is well formed. ctx.insert_user_tactic(m_name, m_decl); @@ -82,7 +82,7 @@ ATOMIC_CMD(get_user_tactics_cmd, "get-user-tactics", "display tactics defined us for (bool first = true; it != end; ++it) { if (first) first = false; else buf << "\n "; buf << "(declare-tactic " << it->m_key << " "; - it->m_value->display(buf); + it->m_value->display(buf); buf << ")"; } std::string r = buf.str(); @@ -94,8 +94,8 @@ void help_tactic(cmd_context & ctx) { std::ostringstream buf; buf << "combinators:\n"; buf << "- (and-then +) executes the given tactics sequencially.\n"; - buf << "- (or-else +) tries the given tactics in sequence until one of them succeeds.\n"; - buf << "- (par-or +) executes the given tactics in parallel until one of them succeeds.\n"; + buf << "- (or-else +) tries the given tactics in sequence until one of them succeeds (i.e., the first that doesn't fail).\n"; + buf << "- (par-or +) executes the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).\n"; buf << "- (par-then ) executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel.\n"; buf << "- (try-for ) excutes the given tactic for at most milliseconds, it fails if the execution takes more than milliseconds.\n"; buf << "- (if ) if evaluates to true, then execute the first tactic. Otherwise execute the second.\n"; @@ -134,8 +134,8 @@ public: } virtual char const * get_usage() const { return " ( )*"; } - - virtual void prepare(cmd_context & ctx) { + + virtual void prepare(cmd_context & ctx) { parametric_cmd::prepare(ctx); m_tactic = 0; } @@ -144,17 +144,17 @@ public: if (m_tactic == 0) return CPK_SEXPR; return parametric_cmd::next_arg_kind(ctx); } - + virtual void set_next_arg(cmd_context & ctx, sexpr * arg) { m_tactic = arg; } - + virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { insert_timeout(p); insert_max_memory(p); p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); } - + void display_statistics(cmd_context & ctx, tactic * t) { statistics stats; get_memory_statistics(stats); @@ -181,7 +181,7 @@ public: p.insert("print_proof", CPK_BOOL, "(default: false) print proof."); p.insert("print_model", CPK_BOOL, "(default: false) print model."); } - + virtual void execute(cmd_context & ctx) { params_ref p = ctx.params().merge_default_params(ps()); tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p); @@ -200,7 +200,7 @@ public: { tactic & t = *tref; cancel_eh eh(t); - { + { scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); cmd_context::scoped_watch sw(ctx); @@ -212,7 +212,7 @@ public: if (r == l_undef) { if (reason_unknown != "") { result->m_unknown = reason_unknown; - // ctx.diagnostic_stream() << "\"" << escaped(reason_unknown.c_str(), true) << "\"" << std::endl; + // ctx.diagnostic_stream() << "\"" << escaped(reason_unknown.c_str(), true) << "\"" << std::endl; } else { result->m_unknown = "unknown"; @@ -231,7 +231,7 @@ public: } t.collect_statistics(result->m_stats); } - + if (ctx.produce_unsat_cores()) { ptr_vector core_elems; m.linearize(core, core_elems); @@ -247,7 +247,7 @@ public: ctx.regular_stream() << ")" << std::endl; } } - + if (ctx.produce_models() && md) { result->m_model = md; if (p.get_bool("print_model", false)) { @@ -291,7 +291,7 @@ public: #endif exec_given_tactic_cmd::init_pdescrs(ctx, p); } - + virtual void execute(cmd_context & ctx) { params_ref p = ctx.params().merge_default_params(ps()); tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p); @@ -300,9 +300,9 @@ public: ast_manager & m = ctx.m(); goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); - - unsigned timeout = p.get_uint("timeout", UINT_MAX); - + + unsigned timeout = p.get_uint("timeout", UINT_MAX); + goal_ref_buffer result_goals; model_converter_ref mc; proof_converter_ref pc; @@ -311,7 +311,7 @@ public: std::string reason_unknown; bool failed = false; cancel_eh eh(t); - { + { scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); cmd_context::scoped_watch sw(ctx); @@ -323,7 +323,7 @@ public: failed = true; } } - + if (!failed && p.get_bool("print", true)) { bool print_dependencies = p.get_bool("print_dependencies", false); ctx.regular_stream() << "(goals\n"; @@ -343,7 +343,7 @@ public: } #endif - if (!failed && p.get_bool("print_benchmark", false)) { + if (!failed && p.get_bool("print_benchmark", false)) { unsigned num_goals = result_goals.size(); SASSERT(num_goals > 0); if (num_goals == 1) { @@ -374,10 +374,10 @@ public: ctx.display_smt2_benchmark(ctx.regular_stream(), 1, assertions); } } - - if (!failed && mc && p.get_bool("print_model_converter", false)) + + if (!failed && mc && p.get_bool("print_model_converter", false)) mc->display(ctx.regular_stream()); - + if (p.get_bool("print_statistics", false)) display_statistics(ctx, tref.get()); } @@ -573,7 +573,7 @@ static tactic * mk_echo(cmd_context & ctx, sexpr * n) { sexpr * curr = n->get_child(i); bool last = (i == num_children - 1); tactic * t; - if (curr->is_string()) + if (curr->is_string()) t = mk_echo_tactic(ctx, curr->get_string().c_str(), last); else t = mk_probe_value_tactic(ctx, 0, sexpr2probe(ctx, curr), last); @@ -701,11 +701,11 @@ tactic * sexpr2tactic(cmd_context & ctx, sexpr * n) { } } -static probe * mk_not_probe (cmd_context & ctx, sexpr * n) { - SASSERT(n->is_composite()); - unsigned num_children = n->get_num_children(); - if (num_children != 2) - throw cmd_exception("invalid probe expression, one argument expected", n->get_line(), n->get_pos()); +static probe * mk_not_probe (cmd_context & ctx, sexpr * n) { + SASSERT(n->is_composite()); + unsigned num_children = n->get_num_children(); + if (num_children != 2) + throw cmd_exception("invalid probe expression, one argument expected", n->get_line(), n->get_pos()); return mk_not(sexpr2probe(ctx, n->get_child(1))); } @@ -775,7 +775,7 @@ probe * sexpr2probe(cmd_context & ctx, sexpr * n) { if (!head->is_symbol()) throw cmd_exception("invalid probe, symbol expected", n->get_line(), n->get_pos()); symbol const & p_name = head->get_symbol(); - + if (p_name == "=") return mk_eq_probe(ctx, n); else if (p_name == "<=") @@ -792,13 +792,13 @@ probe * sexpr2probe(cmd_context & ctx, sexpr * n) { return mk_or_probe(ctx, n); else if (p_name == "=>" || p_name == "implies") return mk_implies_probe(ctx, n); - else if (p_name == "not") + else if (p_name == "not") return mk_not_probe(ctx, n); else if (p_name == "*") return mk_mul_probe(ctx, n); - else if (p_name == "+") + else if (p_name == "+") return mk_add_probe(ctx, n); - else if (p_name == "-") + else if (p_name == "-") return mk_sub_probe(ctx, n); else if (p_name == "/") return mk_div_probe(ctx, n);