diff options
| author | Ying Sheng <sqy1415@gmail.com> | 2020-06-30 04:50:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-30 08:50:40 -0300 |
| commit | 724d8cf23ae74158b36b408643298c49c3b20833 (patch) | |
| tree | 737db246271ec879aaae7e62e49b858faf473e35 /src/options | |
| parent | 6303c25fc375f33b27398f9b8c4b70901785a5f1 (diff) | |
Interpolation step 1 (#4638)
This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
The first step creates the API framework, while omits the implementation for getting interpolation.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/smt_options.toml | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 303448d1b..c104cb3e7 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -669,6 +669,34 @@ header = "options/smt_options.h" help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" [[option]] + name = "produceInterpols" + category = "undocumented" + long = "produce-interpols=MODE" + type = "ProduceInterpols" + default = "NONE" + read_only = true + help = "support the get-interpol command" + help_mode = "Interpolants grammar mode" +[[option.mode.NONE]] + name = "none" + help = "don't compute interpolants" +[[option.mode.DEFAULT]] + name = "default" + help = "use the default grammar for the theory or the user-defined grammar if given" +[[option.mode.ASSUMPTIONS]] + name = "assumptions" + help = "use only operators that occur in the assumptions" +[[option.mode.CONJECTURE]] + name = "conjecture" + help = "use only operators that occur in the conjecture" +[[option.mode.SHARED]] + name = "shared" + help = "use only operators that occur both in the assumptions and the conjecture" +[[option.mode.ALL]] + name = "all" + help = "use only operators that occur either in the assumptions or the conjecture" + +[[option]] name = "produceAbducts" category = "undocumented" long = "produce-abducts" @@ -678,6 +706,15 @@ header = "options/smt_options.h" help = "support the get-abduct command" [[option]] + name = "checkInterpols" + category = "regular" + long = "check-interpols" + type = "bool" + default = "false" + read_only = true + help = "checks whether produced solutions to get-interpol are correct" + +[[option]] name = "checkAbducts" category = "regular" long = "check-abducts" |