Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.

* support for new commands meta-info, declare-const, echo, get-model,
  reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
  this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
  in 2.0 mode)

What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
  Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
  (Currently :incremental and maybe others get "stuck" due to late driver
  integration.)

1 files changed, 6 insertions, 6 deletions

diff --git a/src/smt/options b/src/smt/options
index 3ee3dbecb..0dc416474 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -25,7 +25,7 @@ option expandDefinitions expand-definitions bool :default false
  always expand symbol definitions in output
 common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  support the get-value and get-model commands
-option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
 option dumpModels --dump-models bool :default false :link --produce-models
  output models after every SAT/INVALID/UNKNOWN response
@@ -45,10 +45,10 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns
 option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  support the get-assignment command
 
-# This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
-# is a mode in which the assertion list must be kept.  So it belongs here.
-common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
- force interactive mode
+undocumented-option interactiveMode interactive-mode bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
+ deprecated name for produce-assertions
+common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
+ keep an assertions list (enables get-assertions command)
 
 option doITESimp --ite-simp bool :read-write
  turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
@@ -93,7 +93,7 @@ common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long
  enable time limiting per query (give milliseconds)
 common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
  enable resource limiting (currently, roughly the number of SAT conflicts)
-common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
+common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long"
  enable resource limiting per query
 
 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false