changing theoryOf in shared mode with arrays to move equalities to arrays

disabled in bitvectors due to non-stably infinite problems

the option to enable it is --theoryof-mode=term

2 files changed, 38 insertions, 1 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 8961d5b57..c912023ad 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -165,7 +165,9 @@ Options::Options() :
   bitvectorEagerBitblast(false),
   bitvectorEagerFullcheck(false),
   bitvectorShareLemmas(false),
-  sat_refine_conflicts(false)
+  sat_refine_conflicts(false),
+  theoryOfModeSetByUser(false),
+  theoryOfMode(theory::THEORY_OF_TYPE_BASED)
 {
 }
 
@@ -236,6 +238,7 @@ Additional CVC4 options:\n\
    --no-repeat-simp       do not make multiple passes with nonclausal simplifier\n\
    --replay=file          replay decisions from file\n\
    --replay-log=file      log decisions and propagations to file\n\
+   --theoryof-mode=mode   mode for theoryof\n\
   SAT:\n\
    --random-freq=P        frequency of random decisions in the sat solver\n\
                           (P=0.0 by default)\n\
@@ -333,6 +336,16 @@ none\n\
 + do not perform nonclausal simplification\n\
 ";
 
+static const string theoryofHelp = "\
+TheoryOf modes currently supported by the --theoryof-mode option:\n\
+\n\
+type (default) \n\
++ type variables, constants and equalities by type\n\
+\n\
+term \n\
++ type variables as uninterpreted, equalities by the parametric theory\n\
+";
+
 static const string decisionHelp = "\
 Decision modes currently supported by the --decision option:\n\
 \n\
@@ -580,6 +593,7 @@ enum OptionValue {
   BITVECTOR_SHARE_LEMMAS,
   BITVECTOR_EAGER_FULLCHECK,
   SAT_REFINE_CONFLICTS,
+  THEORYOF_MODE,
   OPTION_VALUE_END
 };/* enum OptionValue */
 
@@ -708,6 +722,7 @@ static struct option cmdlineOptions[] = {
   { "bitblast-share-lemmas", no_argument, NULL, BITVECTOR_SHARE_LEMMAS },
   { "bitblast-eager-fullcheck", no_argument, NULL, BITVECTOR_EAGER_FULLCHECK },
   { "refine-conflicts", no_argument, NULL, SAT_REFINE_CONFLICTS },
+  { "theoryof-mode", required_argument, NULL, THEORYOF_MODE },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -981,6 +996,21 @@ throw(OptionException) {
       }
       break;
 
+    case THEORYOF_MODE:
+      if (!strcmp(optarg, "type")) {
+        theoryOfModeSetByUser = true;
+        theoryOfMode = theory::THEORY_OF_TYPE_BASED;
+      } else if (!strcmp(optarg, "term")) {
+        theoryOfModeSetByUser = true;
+        theoryOfMode = theory::THEORY_OF_TERM_BASED;
+      } else if (!strcmp(optarg, "help")) {
+        puts(theoryofHelp.c_str());
+        exit(1);
+      } else {
+        throw OptionException(string("unknown option for --theoryof-mode: `") +
+                              optarg + "'.  Try --theoryof-mode help.");
+      }
+      break;
     case DECISION_MODE:
       if(!strcmp(optarg, "internal")) {
         decisionMode = DECISION_STRATEGY_INTERNAL;
diff --git a/src/util/options.h b/src/util/options.h
index 7dbba2439..bc99b5feb 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -30,6 +30,7 @@
 #include "util/lemma_output_channel.h"
 #include "util/lemma_input_channel.h"
 #include "util/tls.h"
+#include "theory/theoryof_mode.h"
 
 #include <vector>
 
@@ -491,6 +492,12 @@ struct CVC4_PUBLIC Options {
   /** Refine conflicts by doing another full check after a conflict */
   bool sat_refine_conflicts;
 
+  /** Was theoryOf mode set by user */
+  bool theoryOfModeSetByUser;
+
+  /** Which theoryOf mode are we using */
+  theory::TheoryOfMode theoryOfMode;
+
   Options();
 
   /**