summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/Makefile.am9
-rw-r--r--src/theory/arith/arith_heuristic_pivot_rule.cpp43
-rw-r--r--src/theory/arith/arith_heuristic_pivot_rule.h39
-rw-r--r--src/theory/arith/arith_propagation_mode.cpp46
-rw-r--r--src/theory/arith/arith_propagation_mode.h40
-rw-r--r--src/theory/arith/arith_unate_lemma_mode.cpp46
-rw-r--r--src/theory/arith/arith_unate_lemma_mode.h40
-rw-r--r--src/theory/arith/options55
-rw-r--r--src/theory/arith/options_handlers.h124
-rw-r--r--src/theory/arith/simplex.cpp23
-rw-r--r--src/theory/arith/simplex.h2
-rw-r--r--src/theory/arith/theory_arith.cpp34
-rw-r--r--src/theory/arith/theory_arith_instantiator.cpp7
13 files changed, 476 insertions, 32 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 68b580c54..b71f07852 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -38,8 +38,15 @@ libarith_la_SOURCES = \
theory_arith.cpp \
dio_solver.h \
dio_solver.cpp \
+ arith_heuristic_pivot_rule.h \
+ arith_heuristic_pivot_rule.cpp \
+ arith_unate_lemma_mode.h \
+ arith_unate_lemma_mode.cpp \
+ arith_propagation_mode.h \
+ arith_propagation_mode.cpp \
theory_arith_instantiator.h \
theory_arith_instantiator.cpp
EXTRA_DIST = \
- kinds
+ kinds \
+ options_handlers.h
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.cpp b/src/theory/arith/arith_heuristic_pivot_rule.cpp
new file mode 100644
index 000000000..1a2958556
--- /dev/null
+++ b/src/theory/arith/arith_heuristic_pivot_rule.cpp
@@ -0,0 +1,43 @@
+/********************* */
+/*! \file arith_heuristic_pivot_rule.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/arith/arith_heuristic_pivot_rule.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, ArithHeuristicPivotRule rule) {
+ switch(rule) {
+ case MINIMUM:
+ out << "MINIMUM";
+ break;
+ case BREAK_TIES:
+ out << "BREAK_TIES";
+ break;
+ case MAXIMUM:
+ out << "MAXIMUM";
+ break;
+ default:
+ out << "ArithHeuristicPivotRule!UNKNOWN";
+ }
+
+ return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/theory/arith/arith_heuristic_pivot_rule.h
new file mode 100644
index 000000000..ef0f8cfe5
--- /dev/null
+++ b/src/theory/arith/arith_heuristic_pivot_rule.h
@@ -0,0 +1,39 @@
+/********************* */
+/*! \file arith_heuristic_pivot_rule.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
+#define __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+typedef enum {
+ MINIMUM,
+ BREAK_TIES,
+ MAXIMUM
+} ArithHeuristicPivotRule;
+
+std::ostream& operator<<(std::ostream& out, ArithHeuristicPivotRule rule) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */
diff --git a/src/theory/arith/arith_propagation_mode.cpp b/src/theory/arith/arith_propagation_mode.cpp
new file mode 100644
index 000000000..08c56ad3b
--- /dev/null
+++ b/src/theory/arith/arith_propagation_mode.cpp
@@ -0,0 +1,46 @@
+/********************* */
+/*! \file arith_propagation_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/arith/arith_propagation_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, ArithPropagationMode mode) {
+ switch(mode) {
+ case NO_PROP:
+ out << "NO_PROP";
+ break;
+ case UNATE_PROP:
+ out << "UNATE_PROP";
+ break;
+ case BOUND_INFERENCE_PROP:
+ out << "BOUND_INFERENCE_PROP";
+ break;
+ case BOTH_PROP:
+ out << "BOTH_PROP";
+ break;
+ default:
+ out << "ArithPropagationMode!UNKNOWN";
+ }
+
+ return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/arith_propagation_mode.h b/src/theory/arith/arith_propagation_mode.h
new file mode 100644
index 000000000..507862415
--- /dev/null
+++ b/src/theory/arith/arith_propagation_mode.h
@@ -0,0 +1,40 @@
+/********************* */
+/*! \file arith_propagation_mode.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
+#define __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+typedef enum {
+ NO_PROP,
+ UNATE_PROP,
+ BOUND_INFERENCE_PROP,
+ BOTH_PROP
+} ArithPropagationMode;
+
+std::ostream& operator<<(std::ostream& out, ArithPropagationMode rule) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */
diff --git a/src/theory/arith/arith_unate_lemma_mode.cpp b/src/theory/arith/arith_unate_lemma_mode.cpp
new file mode 100644
index 000000000..58f5d7850
--- /dev/null
+++ b/src/theory/arith/arith_unate_lemma_mode.cpp
@@ -0,0 +1,46 @@
+/********************* */
+/*! \file arith_unate_lemma_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/arith/arith_unate_lemma_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode mode) {
+ switch(mode) {
+ case NO_PRESOLVE_LEMMAS:
+ out << "NO_PRESOLVE_LEMMAS";
+ break;
+ case INEQUALITY_PRESOLVE_LEMMAS:
+ out << "INEQUALITY_PRESOLVE_LEMMAS";
+ break;
+ case EQUALITY_PRESOLVE_LEMMAS:
+ out << "EQUALITY_PRESOLVE_LEMMAS";
+ break;
+ case ALL_PRESOLVE_LEMMAS:
+ out << "ALL_PRESOLVE_LEMMAS";
+ break;
+ default:
+ out << "ArithUnateLemmaMode!UNKNOWN";
+ }
+
+ return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/arith_unate_lemma_mode.h b/src/theory/arith/arith_unate_lemma_mode.h
new file mode 100644
index 000000000..71ee26ded
--- /dev/null
+++ b/src/theory/arith/arith_unate_lemma_mode.h
@@ -0,0 +1,40 @@
+/********************* */
+/*! \file arith_unate_lemma_mode.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
+#define __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+typedef enum {
+ NO_PRESOLVE_LEMMAS,
+ INEQUALITY_PRESOLVE_LEMMAS,
+ EQUALITY_PRESOLVE_LEMMAS,
+ ALL_PRESOLVE_LEMMAS
+} ArithUnateLemmaMode;
+
+std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode rule) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */
diff --git a/src/theory/arith/options b/src/theory/arith/options
new file mode 100644
index 000000000..8b45a6da2
--- /dev/null
+++ b/src/theory/arith/options
@@ -0,0 +1,55 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module ARITH "theory/arith/options.h" Arithmetic theory
+
+option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::theory::arith::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_unate_lemma_mode.h"
+ determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)
+
+option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::theory::arith::stringToArithPropagationMode :default BOTH_PROP :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_propagation_mode.h"
+ turns on arithmetic propagation (default is 'old', see --arith-prop=help)
+
+# The maximum number of difference pivots to do per invocation of simplex.
+# If this is negative, the number of pivots done is the number of variables.
+# If this is not set by the user, different logics are free to chose different
+# defaults.
+option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write
+ the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection
+
+# The maximum number of variable order pivots to do per invocation of simplex.
+# If this is negative, the number of pivots done is unlimited.
+# If this is not set by the user, different logics are free to chose different
+# defaults.
+expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write
+ limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule
+
+option arithHeuristicPivotRule --heuristic-pivot-rule=RULE ArithHeuristicPivotRule :handler CVC4::theory::arith::stringToArithHeuristicPivotRule :default MINIMUM :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_heuristic_pivot_rule.h"
+ change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)
+
+# The number of pivots before simplex rechecks every basic variable for a conflict
+option arithSimplexCheckPeriod --simplex-check-period=N uint16_t :default 200
+ the number of pivots to do in simplex before rechecking for a conflict on all variables
+
+# This is the pivots per basic variable that can be done using heuristic choices
+# before variable order must be used.
+# If this is not set by the user, different logics are free to chose different
+# defaults.
+option arithPivotThreshold --pivot-threshold=N uint16_t :default 2 :read-write
+ sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order
+
+option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16
+ sets the maximum row length to be used in propagation
+
+option arithDioSolver /--disable-dio-solver bool :default true
+ use Linear Diophantine Equation solver (Griggio, JSAT 2012)
+/turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)
+
+# Whether to split (= x y) into (and (<= x y) (>= x y)) in
+# arithmetic preprocessing.
+option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-equalities bool :default false :read-write
+ turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
+/turns off the preprocessing rewrite turning equalities into a conjunction of inequalities
+
+endmodule
diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
new file mode 100644
index 000000000..3eafe2ef0
--- /dev/null
+++ b/src/theory/arith/options_handlers.h
@@ -0,0 +1,124 @@
+/********************* */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Custom handlers and predicates for arithmetic options
+ **
+ ** Custom handlers and predicates for arithmetic options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H
+
+#include <string>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+static const std::string arithPresolveLemmasHelp = "\
+Presolve lemmas are generated before SAT search begins using the relationship\n\
+of constant terms and polynomials.\n\
+Modes currently supported by the --arith-presolve-lemmas option:\n\
++ none \n\
++ ineqs \n\
+ Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
++ eqs \n\
+ Outputs lemmas of the general forms\n\
+ (= p c) implies (<= p d) for c < d, or\n\
+ (= p c) implies (not (= p d)) for c != d.\n\
++ all \n\
+ A combination of inequalities and equalities.\n\
+";
+
+static const std::string propagationModeHelp = "\
+This decides on kind of propagation arithmetic attempts to do during the search.\n\
++ none\n\
++ unate\n\
+ use constraints to do unate propagation\n\
++ bi (Bounds Inference)\n\
+ infers bounds on basic variables using the upper and lower bounds of the\n\
+ non-basic variables in the tableau.\n\
++both\n\
+";
+
+static const std::string heuristicPivotRulesHelp = "\
+This decides on the rule used by simplex during hueristic rounds\n\
+for deciding the next basic variable to select.\n\
+Heuristic pivot rules available:\n\
++min\n\
+ The minimum abs() value of the variable's violation of its bound. (default)\n\
++min-break-ties\n\
+ The minimum violation with ties broken by variable order (total)\n\
++max\n\
+ The maximum violation the bound\n\
+";
+
+inline ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "all") {
+ return ALL_PRESOLVE_LEMMAS;
+ } else if(optarg == "none") {
+ return NO_PRESOLVE_LEMMAS;
+ } else if(optarg == "ineqs") {
+ return INEQUALITY_PRESOLVE_LEMMAS;
+ } else if(optarg == "eqs") {
+ return EQUALITY_PRESOLVE_LEMMAS;
+ } else if(optarg == "help") {
+ puts(arithPresolveLemmasHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --unate-lemmas: `") +
+ optarg + "'. Try --unate-lemmas help.");
+ }
+}
+
+inline ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "none") {
+ return NO_PROP;
+ } else if(optarg == "unate") {
+ return UNATE_PROP;
+ } else if(optarg == "bi") {
+ return BOUND_INFERENCE_PROP;
+ } else if(optarg == "both") {
+ return BOTH_PROP;
+ } else if(optarg == "help") {
+ puts(propagationModeHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --arith-prop: `") +
+ optarg + "'. Try --arith-prop help.");
+ }
+}
+
+inline ArithHeuristicPivotRule stringToArithHeuristicPivotRule(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ if(optarg == "min") {
+ return MINIMUM;
+ } else if(optarg == "min-break-ties") {
+ return BREAK_TIES;
+ } else if(optarg == "max") {
+ return MAXIMUM;
+ } else if(optarg == "help") {
+ puts(heuristicPivotRulesHelp.c_str());
+ exit(1);
+ } else {
+ throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") +
+ optarg + "'. Try --heuristic-pivot-rule help.");
+ }
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H */
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 63bb42e7a..e77067d61 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -19,6 +19,7 @@
#include "theory/arith/simplex.h"
+#include "theory/arith/options.h"
using namespace std;
@@ -41,14 +42,14 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq,
d_pivotsInRound(),
d_DELTA_ZERO(0,0)
{
- switch(Options::ArithHeuristicPivotRule rule = Options::current()->arithHeuristicPivotRule) {
- case Options::MINIMUM:
+ switch(ArithHeuristicPivotRule rule = options::arithHeuristicPivotRule()) {
+ case MINIMUM:
d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
break;
- case Options::BREAK_TIES:
+ case BREAK_TIES:
d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
break;
- case Options::MAXIMUM:
+ case MAXIMUM:
d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
break;
default:
@@ -262,13 +263,13 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
}
}
static const bool verbose = false;
- exactResult |= Options::current()->arithStandardCheckVarOrderPivots < 0;
- const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : Options::current()->arithStandardCheckVarOrderPivots;
+ exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
+ const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : options::arithStandardCheckVarOrderPivots();
- uint32_t checkPeriod = Options::current()->arithSimplexCheckPeriod;
+ uint32_t checkPeriod = options::arithSimplexCheckPeriod();
if(result == Result::SAT_UNKNOWN){
- uint32_t numDifferencePivots = Options::current()->arithHeuristicPivots < 0 ?
- d_numVariables + 1 : Options::current()->arithHeuristicPivots;
+ uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ?
+ d_numVariables + 1 : options::arithHeuristicPivots();
// The signed to unsigned conversion is safe.
uint32_t pivotsRemaining = numDifferencePivots;
while(!d_queue.empty() &&
@@ -421,7 +422,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
--remainingIterations;
- bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= Options::current()->arithPivotThreshold;
+ bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= options::arithPivotThreshold();
if(!useVarOrderPivot){
d_pivotsInRound.add(x_i);
}
@@ -429,7 +430,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
Debug("playground") << "pivots in rounds: " << d_pivotsInRound.count(x_i)
<< " use " << useVarOrderPivot
- << " threshold " << Options::current()->arithPivotThreshold
+ << " threshold " << options::arithPivotThreshold()
<< endl;
PreferenceFunction pf = useVarOrderPivot ? minVarOrder : minBoundAndRowCount;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 33c6537de..324f3b21b 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -60,7 +60,7 @@
#include "context/cdlist.h"
#include "util/dense_map.h"
-#include "util/options.h"
+#include "options/options.h"
#include "util/stats.h"
#include "util/result.h"
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c68e9cf54..d55860c41 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -42,6 +42,8 @@
#include "theory/arith/normal_form.h"
#include "theory/model.h"
+#include "theory/arith/options.h"
+
#include <stdint.h>
using namespace std;
@@ -651,7 +653,7 @@ Node TheoryArith::ppRewrite(TNode atom) {
<< a << endl;
}
- if (a.getKind() == kind::EQUAL && Options::current()->arithRewriteEq) {
+ if (a.getKind() == kind::EQUAL && options::arithRewriteEq()) {
Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1];
Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1];
Node rewritten = Rewriter::rewrite(leq.andNode(geq));
@@ -1536,8 +1538,8 @@ void TheoryArith::check(Effort effortLevel){
// This should be fine if sat or unknown
if(!emmittedConflictOrSplit &&
- (Options::current()->arithPropagationMode == Options::UNATE_PROP ||
- Options::current()->arithPropagationMode == Options::BOTH_PROP)){
+ (options::arithPropagationMode() == UNATE_PROP ||
+ options::arithPropagationMode() == BOTH_PROP)){
TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
Assert(d_qflraStatus != Result::UNSAT);
@@ -1600,7 +1602,7 @@ void TheoryArith::check(Effort effortLevel){
if(!emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()){
Node possibleConflict = Node::null();
- if(!emmittedConflictOrSplit && Options::current()->arithDioSolver){
+ if(!emmittedConflictOrSplit && options::arithDioSolver()){
possibleConflict = callDioSolver();
if(possibleConflict != Node::null()){
revertOutOfConflict();
@@ -1610,7 +1612,7 @@ void TheoryArith::check(Effort effortLevel){
}
}
- if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->arithDioSolver){
+ if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){
Node possibleLemma = dioCutting();
if(!possibleLemma.isNull()){
Debug("arith") << "dio cut " << possibleLemma << endl;
@@ -1791,8 +1793,8 @@ Node TheoryArith::explain(TNode n) {
void TheoryArith::propagate(Effort e) {
// This uses model values for safety. Disable for now.
if(d_qflraStatus == Result::SAT &&
- (Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
- Options::current()->arithPropagationMode == Options::BOTH_PROP)
+ (options::arithPropagationMode() == BOUND_INFERENCE_PROP ||
+ options::arithPropagationMode() == BOTH_PROP)
&& hasAnyUpdates()){
propagateCandidates();
}else{
@@ -2039,21 +2041,21 @@ void TheoryArith::presolve(){
}
vector<Node> lemmas;
- switch(Options::current()->arithUnateLemmaMode){
- case Options::NO_PRESOLVE_LEMMAS:
+ switch(options::arithUnateLemmaMode()){
+ case NO_PRESOLVE_LEMMAS:
break;
- case Options::INEQUALITY_PRESOLVE_LEMMAS:
+ case INEQUALITY_PRESOLVE_LEMMAS:
d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
break;
- case Options::EQUALITY_PRESOLVE_LEMMAS:
+ case EQUALITY_PRESOLVE_LEMMAS:
d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
break;
- case Options::ALL_PRESOLVE_LEMMAS:
+ case ALL_PRESOLVE_LEMMAS:
d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
break;
default:
- Unhandled(Options::current()->arithUnateLemmaMode);
+ Unhandled(options::arithUnateLemmaMode());
}
vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
@@ -2063,7 +2065,7 @@ void TheoryArith::presolve(){
d_out->lemma(lem);
}
- // if(Options::current()->arithUnateLemmaMode == Options::ALL_UNATE){
+ // if(options::arithUnateLemmaMode() == Options::ALL_UNATE){
// vector<Node> lemmas;
// d_constraintDatabase.outputAllUnateLemmas(lemmas);
// vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
@@ -2187,7 +2189,7 @@ void TheoryArith::propagateCandidates(){
for(; i != end; ++i){
ArithVar var = *i;
if(d_tableau.isBasic(var) &&
- d_tableau.getRowLength(d_tableau.basicToRowIndex(var)) <= Options::current()->arithPropagateMaxLength){
+ d_tableau.getRowLength(d_tableau.basicToRowIndex(var)) <= options::arithPropagateMaxLength()){
d_candidateBasics.softAdd(var);
}else{
Tableau::ColIterator basicIter = d_tableau.colIterator(var);
@@ -2197,7 +2199,7 @@ void TheoryArith::propagateCandidates(){
ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
Assert(entry.getColVar() == var);
Assert(d_tableau.isBasic(rowVar));
- if(d_tableau.getRowLength(ridx) <= Options::current()->arithPropagateMaxLength){
+ if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){
d_candidateBasics.softAdd(rowVar);
}
}
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index ab3a1548e..1682897ae 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -17,6 +17,7 @@
#include "theory/arith/theory_arith_instantiator.h"
#include "theory/arith/theory_arith.h"
#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
using namespace std;
@@ -179,7 +180,7 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
Instantiator( c, ie, th ){
- if( Options::current()->cbqi ){
+ if( options::cbqi() ){
addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) );
}
}
@@ -191,7 +192,7 @@ void InstantiatorTheoryArith::preRegisterTerm( Node t ){
void InstantiatorTheoryArith::assertNode( Node assertion ){
Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
d_quantEngine->addTermToDatabase( assertion );
- if( Options::current()->cbqi ){
+ if( options::cbqi() ){
if( assertion.hasAttribute(InstConstantAttribute()) ){
setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
}else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
@@ -201,7 +202,7 @@ void InstantiatorTheoryArith::assertNode( Node assertion ){
}
void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){
- if( Options::current()->cbqi ){
+ if( options::cbqi() ){
Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
d_instRows.clear();
d_tableaux_term.clear();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback