From 724d8cf23ae74158b36b408643298c49c3b20833 Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 30 Jun 2020 04:50:40 -0700 Subject: 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. --- src/options/smt_options.toml | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'src/options/smt_options.toml') 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 @@ -668,6 +668,34 @@ header = "options/smt_options.h" read_only = true 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" @@ -677,6 +705,15 @@ header = "options/smt_options.h" read_only = true 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" -- cgit v1.2.3