diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-16 21:35:05 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-16 21:35:05 +0000 |
commit | bc36750b551f1d0b571af1e2265b5dea42544e7d (patch) | |
tree | 4d8621cce48900fe3220d55b5fb451adeb125607 /src/util | |
parent | adae14a07b1019d092b4d5aa0cf809f9d0eca66d (diff) |
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
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/options.cpp | 32 | ||||
-rw-r--r-- | src/util/options.h | 7 |
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(); /** |