Skip to content

Commit 67574dc

Browse files
committed
add more documentation about OpenSMT options.
1 parent 4c4fd82 commit 67574dc

File tree

4 files changed

+24
-0
lines changed

4 files changed

+24
-0
lines changed

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,12 @@ static class OpenSMTOptions {
5757
@Option(secure = true, description = "Algorithm for LRA interpolation")
5858
LA algLra = LA.STRONG;
5959

60+
/**
61+
* This option controls the level of simplification applied to interpolants.
62+
*
63+
* <p>For details, please see the original sources:
64+
* https://github.com/usi-verification-and-security/opensmt/blob/7cef5bc983d7774874ffc177f06516c4e0f411f4/src/proof/InterpolationContext.cc#L933-L960
65+
*/
6066
@IntegerOption(min = 0, max = 4)
6167
@Option(
6268
secure = true,

src/org/sosy_lab/java_smt/solvers/opensmt/interpolationAlgorithms/Core.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,12 @@
1010

1111
package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
1212

13+
/**
14+
* Enumeration for the different algorithms for boolean interpolation.
15+
*
16+
* <p>For details, please see the original sources:
17+
* https://github.com/usi-verification-and-security/opensmt/blob/c267e01e1e0d4d4b7f9ba273dd910c070c1aa9b1/src/options/SMTConfig.h#L163-L168
18+
*/
1319
public enum Core {
1420
MCMILLAN(0),
1521
PUDLAK(1),

src/org/sosy_lab/java_smt/solvers/opensmt/interpolationAlgorithms/LA.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,12 @@
1010

1111
package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
1212

13+
/**
14+
* Enumeration for the different algorithms for LRA interpolation.
15+
*
16+
* <p>For details, please see the original sources:
17+
* https://github.com/usi-verification-and-security/opensmt/blob/c267e01e1e0d4d4b7f9ba273dd910c070c1aa9b1/src/options/SMTConfig.h#L172C42-L176
18+
*/
1319
public enum LA {
1420
STRONG(0),
1521
WEAK(2),

src/org/sosy_lab/java_smt/solvers/opensmt/interpolationAlgorithms/UF.java

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,12 @@
1010

1111
package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
1212

13+
/**
14+
* Enumeration for the different algorithms for UF interpolation.
15+
*
16+
* <p>For details, please see the original sources:
17+
* https://github.com/usi-verification-and-security/opensmt/blob/c267e01e1e0d4d4b7f9ba273dd910c070c1aa9b1/src/options/SMTConfig.h#L169-L171
18+
*/
1319
public enum UF {
1420
STRONG(0),
1521
WEAK(2),

0 commit comments

Comments
 (0)