diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/Makefile.am | 9 | ||||
-rw-r--r-- | src/theory/arith/arith_heuristic_pivot_rule.cpp | 43 | ||||
-rw-r--r-- | src/theory/arith/arith_heuristic_pivot_rule.h | 39 | ||||
-rw-r--r-- | src/theory/arith/arith_propagation_mode.cpp | 46 | ||||
-rw-r--r-- | src/theory/arith/arith_propagation_mode.h | 40 | ||||
-rw-r--r-- | src/theory/arith/arith_unate_lemma_mode.cpp | 46 | ||||
-rw-r--r-- | src/theory/arith/arith_unate_lemma_mode.h | 40 | ||||
-rw-r--r-- | src/theory/arith/options | 55 | ||||
-rw-r--r-- | src/theory/arith/options_handlers.h | 124 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 23 | ||||
-rw-r--r-- | src/theory/arith/simplex.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 34 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_instantiator.cpp | 7 |
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(); |