mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Merge pull request #261 from paulp/help-tactic

Browse source 
Changed references to help-tactics to help-tactic.
This commit is contained in:
Nikolaj Bjorner 2015-10-25 16:06:41 -07:00
commit 5c572d8fea
6 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/dotnet/Probe.cs
View file

@ -28,7 +28,7 @@ namespace Microsoft.Z3
/// which solver and/or preprocessing step will be used. /// which solver and/or preprocessing step will be used.
/// The complete list of probes may be obtained using the procedures <c>Context.NumProbes</c> /// The complete list of probes may be obtained using the procedures <c>Context.NumProbes</c>
/// and <c>Context.ProbeNames</c>. /// and <c>Context.ProbeNames</c>.
/// It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end. /// It may also be obtained using the command <c>(help-tactic)</c> in the SMT 2.0 front-end.
/// </summary> /// </summary>
[ContractVerification(true)] [ContractVerification(true)]
public class Probe : Z3Object public class Probe : Z3Object

2
src/api/dotnet/Tactic.cs
View file

@ -26,7 +26,7 @@ namespace Microsoft.Z3
/// Tactics are the basic building block for creating custom solvers for specific problem domains. /// Tactics are the basic building block for creating custom solvers for specific problem domains.
/// The complete list of tactics may be obtained using <c>Context.NumTactics</c> /// The complete list of tactics may be obtained using <c>Context.NumTactics</c>
/// and <c>Context.TacticNames</c>. /// and <c>Context.TacticNames</c>.
/// It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end. /// It may also be obtained using the command <c>(help-tactic)</c> in the SMT 2.0 front-end.
/// </summary> /// </summary>
[ContractVerification(true)] [ContractVerification(true)]
public class Tactic : Z3Object public class Tactic : Z3Object

2
src/api/java/Probe.java
View file

@ -22,7 +22,7 @@ package com.microsoft.z3;
* may be used to decide which solver and/or preprocessing step will be used. * may be used to decide which solver and/or preprocessing step will be used.
* The complete list of probes may be obtained using the procedures * The complete list of probes may be obtained using the procedures
* {@code Context.NumProbes} and {@code Context.ProbeNames}. It may * {@code Context.NumProbes} and {@code Context.ProbeNames}. It may
* also be obtained using the command {@code (help-tactics)} in the SMT 2.0 * also be obtained using the command {@code (help-tactic)} in the SMT 2.0
* front-end. * front-end.
**/ **/
public class Probe extends Z3Object public class Probe extends Z3Object

2
src/api/java/Tactic.java
View file

@ -21,7 +21,7 @@ package com.microsoft.z3;
* Tactics are the basic building block for creating custom solvers for specific * Tactics are the basic building block for creating custom solvers for specific
* problem domains. The complete list of tactics may be obtained using * problem domains. The complete list of tactics may be obtained using
* {@code Context.NumTactics} and {@code Context.TacticNames}. It may * {@code Context.NumTactics} and {@code Context.TacticNames}. It may
* also be obtained using the command {@code (help-tactics)} in the SMT 2.0 * also be obtained using the command {@code (help-tactic)} in the SMT 2.0
* front-end. * front-end.
**/ **/
public class Tactic extends Z3Object public class Tactic extends Z3Object

4
src/api/ml/z3.mli
View file

@ -2779,7 +2779,7 @@ end
which solver and/or preprocessing step will be used. which solver and/or preprocessing step will be used.
The complete list of probes may be obtained using the procedures [Context.NumProbes] The complete list of probes may be obtained using the procedures [Context.NumProbes]
and [Context.ProbeNames]. and [Context.ProbeNames].
It may also be obtained using the command [(help-tactics)] in the SMT 2.0 front-end. It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end.
*) *)
module Probe : module Probe :
sig sig
@ -2841,7 +2841,7 @@ end
Tactics are the basic building block for creating custom solvers for specific problem domains. Tactics are the basic building block for creating custom solvers for specific problem domains.
The complete list of tactics may be obtained using [Context.get_num_tactics] The complete list of tactics may be obtained using [Context.get_num_tactics]
and [Context.get_tactic_names]. and [Context.get_tactic_names].
It may also be obtained using the command [(help-tactics)] in the SMT 2.0 front-end. It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end.
*) *)
module Tactic : module Tactic :
sig sig

4
src/api/z3_api.h
View file

@ -6650,7 +6650,7 @@ END_MLAPI_EXCLUDE
/** /**
\brief Return a tactic associated with the given name. \brief Return a tactic associated with the given name.
The complete list of tactics may be obtained using the procedures #Z3_get_num_tactics and #Z3_get_tactic_name. The complete list of tactics may be obtained using the procedures #Z3_get_num_tactics and #Z3_get_tactic_name.
It may also be obtained using the command <tt>(help-tactics)</tt> in the SMT 2.0 front-end. It may also be obtained using the command <tt>(help-tactic)</tt> in the SMT 2.0 front-end.
Tactics are the basic building block for creating custom solvers for specific problem domains. Tactics are the basic building block for creating custom solvers for specific problem domains.
@ -6677,7 +6677,7 @@ END_MLAPI_EXCLUDE
/** /**
\brief Return a probe associated with the given name. \brief Return a probe associated with the given name.
The complete list of probes may be obtained using the procedures #Z3_get_num_probes and #Z3_get_probe_name. The complete list of probes may be obtained using the procedures #Z3_get_num_probes and #Z3_get_probe_name.
It may also be obtained using the command <tt>(help-tactics)</tt> in the SMT 2.0 front-end. It may also be obtained using the command <tt>(help-tactic)</tt> in the SMT 2.0 front-end.
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide Probes are used to inspect a goal (aka problem) and collect information that may be used to decide
which solver and/or preprocessing step will be used. which solver and/or preprocessing step will be used.