diff options
Diffstat (limited to 'src/theory')
65 files changed, 1189 insertions, 148 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 9d6939ac9..7a4cde04d 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -74,6 +74,7 @@ libtheory_la_LIBADD = \ @builddir@/rewriterules/librewriterules.la EXTRA_DIST = \ + options_handlers.h \ rewriter_tables_template.h \ instantiator_tables_template.cpp \ theory_traits_template.h \ 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(); diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index e4c814660..8b8a5bd48 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -22,4 +22,5 @@ libarrays_la_SOURCES = \ theory_arrays_model.h \ theory_arrays_model.cpp -EXTRA_DIST = kinds +EXTRA_DIST = \ + kinds diff --git a/src/theory/arrays/options b/src/theory/arrays/options new file mode 100644 index 000000000..bf8afc589 --- /dev/null +++ b/src/theory/arrays/options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module ARRAYS "theory/arrays/options.h" Arrays theory + +endmodule diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index 67c42d124..f5a722737 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -17,6 +17,7 @@ #include "theory/theory_engine.h" #include "theory/arrays/theory_arrays_instantiator.h" #include "theory/arrays/theory_arrays.h" +#include "theory/quantifiers/options.h" #include "theory/rr_candidate_generator.h" using namespace std; @@ -38,7 +39,7 @@ void InstantiatorTheoryArrays::preRegisterTerm( Node t ){ void InstantiatorTheoryArrays::assertNode( Node assertion ){ Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << 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()) ){ diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index c591ef7fb..a68ee62cd 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -15,4 +15,5 @@ libbooleans_la_SOURCES = \ circuit_propagator.h \ circuit_propagator.cpp -EXTRA_DIST = kinds +EXTRA_DIST = \ + kinds diff --git a/src/theory/booleans/options b/src/theory/booleans/options new file mode 100644 index 000000000..ae14de58b --- /dev/null +++ b/src/theory/booleans/options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module BOOLEANS "theory/booleans/options.h" Boolean theory + +endmodule diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am index 4b2d566b4..ad471bae7 100644 --- a/src/theory/builtin/Makefile.am +++ b/src/theory/builtin/Makefile.am @@ -13,4 +13,5 @@ libbuiltin_la_SOURCES = \ theory_builtin.h \ theory_builtin.cpp -EXTRA_DIST = kinds +EXTRA_DIST = \ + kinds diff --git a/src/theory/builtin/options b/src/theory/builtin/options new file mode 100644 index 000000000..699f361c9 --- /dev/null +++ b/src/theory/builtin/options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module BUILTIN "theory/builtin/options.h" Builtin theory + +endmodule diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 1f698de0f..669cbe9e0 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -32,4 +32,5 @@ libbv_la_SOURCES = \ theory_bv_rewriter.cpp \ cd_set_collection.h -EXTRA_DIST = kinds +EXTRA_DIST = \ + kinds diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 60a98e6e5..c86f14398 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -25,6 +25,7 @@ #include "prop/sat_solver_factory.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/bv/theory_bv.h" +#include "theory/bv/options.h" using namespace std; @@ -98,7 +99,7 @@ void Bitblaster::bbAtom(TNode node) { // asserting that the atom is true iff the definition holds Node atom_definition = mkNode(kind::IFF, node, atom_bb); - if (!Options::current()->bitvectorEagerBitblast) { + if (!options::bitvectorEagerBitblast()) { d_cnfStream->convertAndAssert(atom_definition, true, false); d_bitblastedAtoms.insert(node); } else { @@ -150,7 +151,7 @@ Node Bitblaster::bbOptimize(TNode node) { /// Public methods void Bitblaster::addAtom(TNode atom) { - if (!Options::current()->bitvectorEagerBitblast) { + if (!options::bitvectorEagerBitblast()) { d_cnfStream->ensureLiteral(atom); SatLiteral lit = d_cnfStream->getLiteral(atom); d_satSolver->addMarkerLiteral(lit); diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 24d6b300b..b0d04f952 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -20,6 +20,7 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/bv/bitblaster.h" +#include "theory/bv/options.h" using namespace std; using namespace CVC4; @@ -57,7 +58,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory: BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl; //// Eager bit-blasting - if (Options::current()->bitvectorEagerBitblast) { + if (options::bitvectorEagerBitblast()) { for (unsigned i = 0; i < assertions.size(); ++i) { TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i]; if (atom.getKind() != kind::BITVECTOR_BITOF) { @@ -105,7 +106,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory: } // solving - if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) { + if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) { Assert(!d_bv->inConflict()); BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n"; bool ok = d_bitblaster->solve(); diff --git a/src/theory/bv/options b/src/theory/bv/options new file mode 100644 index 000000000..72db63c09 --- /dev/null +++ b/src/theory/bv/options @@ -0,0 +1,17 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module BV "theory/bv/options.h" Bitvector theory + +option bitvectorEagerBitblast --bitblast-eager bool + eagerly bitblast the bitvectors to the main SAT solver + +option bitvectorShareLemmas --bitblast-share-lemmas bool + share lemmas from the bitblasting solver with the main solver + +option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool + check the bitblasting eagerly + +endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index da2dd77f6..b6dcc6662 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -21,6 +21,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/valuation.h" #include "theory/bv/bitblaster.h" +#include "theory/bv/options.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" using namespace CVC4; @@ -69,7 +70,7 @@ TheoryBV::Statistics::~Statistics() { void TheoryBV::preRegisterTerm(TNode node) { BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; - if (Options::current()->bitvectorEagerBitblast) { + if (options::bitvectorEagerBitblast()) { // don't use the equality engine in the eager bit-blasting return; } @@ -261,7 +262,7 @@ Node TheoryBV::explain(TNode node) { void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); - if (!Options::current()->bitvectorEagerBitblast && d_useEqualityEngine) { + if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) { d_equalitySolver.addSharedTerm(t); } } @@ -269,7 +270,7 @@ void TheoryBV::addSharedTerm(TNode t) { EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { - if (Options::current()->bitvectorEagerBitblast) { + if (options::bitvectorEagerBitblast()) { return EQUALITY_UNKNOWN; } diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp index a0f303c21..2563ef0d7 100644 --- a/src/theory/candidate_generator.cpp +++ b/src/theory/candidate_generator.cpp @@ -29,7 +29,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; bool CandidateGenerator::isLegalCandidate( Node n ){ - return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) ); + return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute()) ) ); } void CandidateGeneratorQueue::addCandidate( Node n ) { diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am index 8b5fbe979..b3aa318d5 100644 --- a/src/theory/datatypes/Makefile.am +++ b/src/theory/datatypes/Makefile.am @@ -14,4 +14,5 @@ libdatatypes_la_SOURCES = \ theory_datatypes_instantiator.h \ theory_datatypes_instantiator.cpp -EXTRA_DIST = kinds +EXTRA_DIST = \ + kinds diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options new file mode 100644 index 000000000..8a76e8134 --- /dev/null +++ b/src/theory/datatypes/options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module DATATYPES "theory/datatypes/options.h" Datatypes theory + +endmodule diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp index b4b85c9fb..8ecf37fe2 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.cpp +++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/theory_datatypes_instantiator.h" #include "theory/datatypes/theory_datatypes.h" #include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/rr_candidate_generator.h" @@ -35,7 +36,7 @@ Instantiator( c, ie, th ){ void InstantiatorTheoryDatatypes::assertNode( Node assertion ){ Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::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()) ){ @@ -51,7 +52,7 @@ void InstantiatorTheoryDatatypes::processResetInstantiationRound( Theory::Effort int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ){ Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl; - if( Options::current()->cbqi ){ + if( options::cbqi() ){ if( e<2 ){ return InstStrategy::STATUS_UNFINISHED; }else if( e==2 ){ diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp index bad7e34cb..f7c21c555 100644 --- a/src/theory/inst_match.cpp +++ b/src/theory/inst_match.cpp @@ -20,6 +20,7 @@ #include "theory/candidate_generator.h" #include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/equality_engine.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" @@ -106,7 +107,7 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ } void InstMatch::makeInternal( QuantifiersEngine* qe ){ - if( Options::current()->cbqi ){ + if( options::cbqi() ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ if( it->second.hasAttribute(InstConstantAttribute()) ){ d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); @@ -121,7 +122,7 @@ void InstMatch::makeInternal( QuantifiersEngine* qe ){ void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); - if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){ + if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){ d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); } } @@ -591,7 +592,7 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif } int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ - Assert( Options::current()->eagerInstQuant ); + Assert( options::eagerInstQuant() ); if( !d_match_pattern.isNull() ){ InstMatch m; if( getMatch( t, m, qe ) ){ @@ -808,7 +809,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, } int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ - Assert( Options::current()->eagerInstQuant ); + Assert( options::eagerInstQuant() ); int addedLemmas = 0; for( int i=0; i<(int)d_children.size(); i++ ){ if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){ @@ -866,7 +867,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin } int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ - Assert( Options::current()->eagerInstQuant ); + Assert( options::eagerInstQuant() ); InstMatch m; for( int i=0; i<(int)t.getNumChildren(); i++ ){ if( d_match_pattern[i].getKind()==INST_CONSTANT ){ diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h index ae11f429c..fb42909e0 100644 --- a/src/theory/ite_simplifier.h +++ b/src/theory/ite_simplifier.h @@ -39,7 +39,6 @@ #include "theory/shared_terms_database.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" -#include "util/options.h" #include "util/stats.h" #include "util/hash.h" #include "util/cache.h" diff --git a/src/theory/options b/src/theory/options new file mode 100644 index 000000000..40d26472f --- /dev/null +++ b/src/theory/options @@ -0,0 +1,14 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module THEORY "theory/options.h" Theory layer + +expert-option theoryRegistration /--no-theory-registration bool :default true + disable theory reg (not safe for some theories) + +expert-option theoryOfMode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h" + mode for theoryof + +endmodule diff --git a/src/theory/options_handlers.h b/src/theory/options_handlers.h new file mode 100644 index 000000000..b5c8a1fc0 --- /dev/null +++ b/src/theory/options_handlers.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \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, 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 Custom handlers and predicates for TheoryEngine options + ** + ** Custom handlers and predicates for TheoryEngine options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__OPTIONS_HANDLERS_H +#define __CVC4__THEORY__OPTIONS_HANDLERS_H + +namespace CVC4 { +namespace theory { + +static const std::string theoryOfModeHelp = "\ +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\ +"; + +inline TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, SmtEngine* smt) { + if(optarg == "type") { + return THEORY_OF_TYPE_BASED; + } else if(optarg == "term") { + return THEORY_OF_TERM_BASED; + } else if(optarg == "help") { + puts(theoryOfModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --theoryof-mode: `") + + optarg + "'. Try --theoryof-mode help."); + } +} + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__OPTIONS_HANDLERS_H */ diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 316e2fbff..5172001fc 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -17,6 +17,10 @@ libquantifiers_la_SOURCES = \ instantiation_engine.cpp \ model_engine.h \ model_engine.cpp \ + inst_when_mode.cpp \ + inst_when_mode.h \ + literal_match_mode.cpp \ + literal_match_mode.h \ relevant_domain.h \ relevant_domain.cpp \ rep_set_iterator.h \ @@ -28,4 +32,6 @@ libquantifiers_la_SOURCES = \ model_builder.h \ model_builder.cpp -EXTRA_DIST = kinds
\ No newline at end of file +EXTRA_DIST = \ + kinds \ + options_handlers.h diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 1c6b47867..5d7317cbc 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -54,10 +54,10 @@ void FirstOrderModel::initialize(){ initializeModelForTerm( f[1] ); } //for debugging - if( Options::current()->printModelEngine ){ + if( Trace.isOn("model-engine") ){ for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){ if( it->first.isSort() ){ - Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; } } } @@ -181,4 +181,4 @@ void FirstOrderModel::toStream(std::ostream& out){ out << std::endl; } #endif -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/inst_when_mode.cpp b/src/theory/quantifiers/inst_when_mode.cpp new file mode 100644 index 000000000..b60148c21 --- /dev/null +++ b/src/theory/quantifiers/inst_when_mode.cpp @@ -0,0 +1,47 @@ +/********************* */ +/*! \file inst_when_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 <iostream> +#include "theory/quantifiers/inst_when_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) { + switch(mode) { + case theory::quantifiers::INST_WHEN_PRE_FULL: + out << "INST_WHEN_PRE_FULL"; + break; + case theory::quantifiers::INST_WHEN_FULL: + out << "INST_WHEN_FULL"; + break; + case theory::quantifiers::INST_WHEN_FULL_LAST_CALL: + out << "INST_WHEN_FULL_LAST_CALL"; + break; + case theory::quantifiers::INST_WHEN_LAST_CALL: + out << "INST_WHEN_LAST_CALL"; + break; + default: + out << "InstWhenMode!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ + diff --git a/src/theory/quantifiers/inst_when_mode.h b/src/theory/quantifiers/inst_when_mode.h new file mode 100644 index 000000000..2cfba4935 --- /dev/null +++ b/src/theory/quantifiers/inst_when_mode.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file inst_when_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_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H +#define __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +typedef enum { + /** Apply instantiation round before full effort (possibly at standard effort) */ + INST_WHEN_PRE_FULL, + /** Apply instantiation round at full effort or above */ + INST_WHEN_FULL, + /** Apply instantiation round at full effort half the time, and last call always */ + INST_WHEN_FULL_LAST_CALL, + /** Apply instantiation round at last call only */ + INST_WHEN_LAST_CALL, +} InstWhenMode; + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 2b79cd8b9..fb3e6fb36 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -18,6 +18,7 @@ #include "theory/theory_engine.h" #include "theory/uf/theory_uf_instantiator.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" @@ -65,7 +66,7 @@ void InstantiationEngine::addCbqiLemma( Node f ){ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //if counterexample-based quantifier instantiation is active - if( Options::current()->cbqi ){ + if( options::cbqi() ){ //check if any cbqi lemma has not been added yet bool addedLemma = false; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ @@ -136,9 +137,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ return false; }else{ Debug("inst-engine-ctrl") << "---Done. " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl; - if( Options::current()->printInstEngine ){ - Message() << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl; - } + Trace("inst-engine") << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl; //flush lemmas to output channel d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); return true; @@ -153,11 +152,11 @@ void InstantiationEngine::check( Theory::Effort e ){ } //determine if we should perform check, based on instWhenMode bool performCheck = false; - if( Options::current()->instWhenMode==Options::INST_WHEN_FULL ){ + if( options::instWhenMode()==INST_WHEN_FULL ){ performCheck = ( e >= Theory::EFFORT_FULL ); - }else if( Options::current()->instWhenMode==Options::INST_WHEN_FULL_LAST_CALL ){ + }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){ performCheck = ( ( e==Theory::EFFORT_FULL && ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); - }else if( Options::current()->instWhenMode==Options::INST_WHEN_LAST_CALL ){ + }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){ performCheck = ( e >= Theory::EFFORT_LAST_CALL ); }else{ performCheck = true; @@ -165,9 +164,9 @@ void InstantiationEngine::check( Theory::Effort e ){ if( performCheck ){ Debug("inst-engine") << "IE: Check " << e << " " << ierCounter << std::endl; double clSet = 0; - if( Options::current()->printInstEngine ){ + if( Trace.isOn("inst-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); - Message() << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; + Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; } bool quantActive = false; //for each quantifier currently asserted, @@ -178,7 +177,7 @@ void InstantiationEngine::check( Theory::Effort e ){ << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){ + if( options::cbqi() && hasAddedCbqiLemma( n ) ){ Node cel = d_ce_lit[ n ]; bool active, value; bool ceValue = false; @@ -232,21 +231,21 @@ void InstantiationEngine::check( Theory::Effort e ){ Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl; d_quantEngine->getOutputChannel().setIncomplete(); }else{ - Assert( Options::current()->finiteModelFind ); + Assert( options::finiteModelFind() ); Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl; } } } }else{ if( e==Theory::EFFORT_LAST_CALL ){ - if( Options::current()->cbqi ){ + if( options::cbqi() ){ debugSat( SAT_CBQI ); } } } - if( Options::current()->printInstEngine ){ + if( Trace.isOn("inst-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Message() << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl; + Trace("inst-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl; } } } @@ -302,9 +301,9 @@ bool InstantiationEngine::hasNonArithmeticVariable( Node f ){ } bool InstantiationEngine::doCbqi( Node f ){ - if( Options::current()->cbqiSetByUser ){ - return Options::current()->cbqi; - }else if( Options::current()->cbqi ){ + if( options::cbqi.wasSetByUser() ){ + return options::cbqi(); + }else if( options::cbqi() ){ //if quantifier has a non-arithmetic variable, then do not use cbqi //if quantifier has an APPLY_UF term, then do not use cbqi return !hasNonArithmeticVariable( f ) && !hasApplyUf( f[1] ); diff --git a/src/theory/quantifiers/literal_match_mode.cpp b/src/theory/quantifiers/literal_match_mode.cpp new file mode 100644 index 000000000..87b4b94fe --- /dev/null +++ b/src/theory/quantifiers/literal_match_mode.cpp @@ -0,0 +1,43 @@ +/********************* */ +/*! \file literal_match_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 <iostream> +#include "theory/quantifiers/literal_match_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) { + switch(mode) { + case theory::quantifiers::LITERAL_MATCH_NONE: + out << "LITERAL_MATCH_NONE"; + break; + case theory::quantifiers::LITERAL_MATCH_PREDICATE: + out << "LITERAL_MATCH_PREDICATE"; + break; + case theory::quantifiers::LITERAL_MATCH_EQUALITY: + out << "LITERAL_MATCH_EQUALITY"; + break; + default: + out << "LiteralMatchMode!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/literal_match_mode.h b/src/theory/quantifiers/literal_match_mode.h new file mode 100644 index 000000000..189f0a235 --- /dev/null +++ b/src/theory/quantifiers/literal_match_mode.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \file literal_match_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_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H +#define __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +typedef enum { + /** Do not consider polarity of patterns */ + LITERAL_MATCH_NONE, + /** Consider polarity of boolean predicates only */ + LITERAL_MATCH_PREDICATE, + /** Consider polarity of boolean predicates, as well as equalities */ + LITERAL_MATCH_EQUALITY, +} LiteralMatchMode; + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 9cd5020fb..5d49c914f 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -90,11 +90,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m ) { } } } - if( Options::current()->printModelEngine ){ + if( Trace.isOn("model-engine") ){ if( d_addedLemmas>0 ){ - Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl; + Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl; }else{ - Message() << "No InstGen lemmas..." << std::endl; + Trace("model-engine") << "No InstGen lemmas..." << std::endl; } } Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl; @@ -388,11 +388,11 @@ void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){ } bool ModelEngineBuilder::optUseModel() { - return Options::current()->fmfModelBasedInst; + return options::fmfModelBasedInst(); } bool ModelEngineBuilder::optInstGen(){ - return Options::current()->fmfInstGen; + return options::fmfInstGen(); } bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index ddaaa5b6f..4d91c8c95 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -21,6 +21,7 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/uf/theory_uf_instantiator.h" +#include "theory/quantifiers/options.h" #include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" @@ -64,9 +65,9 @@ void ModelEngine::check( Theory::Effort e ){ if( addedLemmas==0 ){ //quantifiers are initialized, we begin an instantiation round double clSet = 0; - if( Options::current()->printModelEngine ){ + if( Trace.isOn("model-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); - Message() << "---Model Engine Round---" << std::endl; + Trace("model-engine") << "---Model Engine Round---" << std::endl; } Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl; ++(d_statistics.d_inst_rounds); @@ -108,11 +109,11 @@ void ModelEngine::check( Theory::Effort e ){ } Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; - if( Options::current()->printModelEngine ){ - Message() << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; - Message() << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; + if( Trace.isOn("model-engine") ){ + Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Message() << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; } #ifdef ME_PRINT_WARNINGS if( addedLemmas>10000 ){ @@ -145,11 +146,11 @@ void ModelEngine::assertNode( Node f ){ } bool ModelEngine::optOneInstPerQuantRound(){ - return Options::current()->fmfOneInstPerRound; + return options::fmfOneInstPerRound(); } bool ModelEngine::optUseRelevantDomain(){ - return Options::current()->fmfRelevantDomain; + return options::fmfRelevantDomain(); } bool ModelEngine::optOneQuantPerRound(){ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options new file mode 100644 index 000000000..91e831092 --- /dev/null +++ b/src/theory/quantifiers/options @@ -0,0 +1,89 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers + +# Whether to mini-scope quantifiers. +# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to +# ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) +option miniscopeQuant /--disable-miniscope-quant bool :default true + disable miniscope quantifiers + +# Whether to mini-scope quantifiers based on formulas with no free variables. +# For example, forall x. ( P( x ) V Q ) will be rewritten to +# ( forall x. P( x ) ) V Q +option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true + disable miniscope quantifiers for ground subformulas + +# Whether to prenex (nested universal) quantifiers +option prenexQuant /--disable-prenex-quant bool :default true + disable prenexing of quantified formulas + +# Whether to variable-eliminate quantifiers. +# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to +# forall y. P( c, y ) +option varElimQuant --var-elim-quant bool :default false + enable variable elimination of quantified formulas + +# Whether to CNF quantifier bodies +option cnfQuant --cnf-quant bool :default false + apply CNF conversion to quantified formulas + +# Whether to pre-skolemize quantifier bodies. +# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to +# forall x. P( x ) => f( S( x ) ) = x +option preSkolemQuant --pre-skolem-quant bool :default false + apply skolemization eagerly to bodies of quantified formulas + +# Whether to use smart triggers +option smartTriggers /--disable-smart-triggers bool :default true + disable smart triggers + +# Whether to consider terms in the bodies of quantifiers for matching +option registerQuantBodyTerms --register-quant-body-terms bool :default false + consider ground terms within bodies of quantified formulas for matching + +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :include "theory/quantifiers/inst_when_mode.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" + when to apply instantiation + +option eagerInstQuant --eager-inst-quant bool :default false + apply quantifier instantiation eagerly + +option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/literal_match_mode.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" + choose literal matching mode + +option cbqi --enable-cbqi/--disable-cbqi bool :default false + turns on counterexample-based quantifier instantiation [off by default] +/turns off counterexample-based quantifier instantiation + +option userPatternsQuant /--ignore-user-patterns bool :default true + ignore user-provided patterns for quantifier instantiation + +option flipDecision --enable-flip-decision/ bool :default false + turns on flip decision heuristic + +option finiteModelFind --finite-model-find bool :default false + use finite model finding heuristic for quantifier instantiation + +option ufssRegions /--disable-uf-ss-regions bool :default true + disable region-based method for discovering cliques and splits in uf strong solver +option ufssEagerSplits --uf-ss-eager-split bool :default false + add splits eagerly for uf strong solver +option ufssColoringSat --uf-ss-coloring-sat bool :default false + use coloring-based SAT heuristic for uf strong solver + +option fmfModelBasedInst /--disable-fmf-mbqi bool :default true + disable model-based quantifier instantiation for finite model finding + +option fmfInstGen /--disable-fmf-inst-gen bool :default true + disable Inst-Gen instantiation techniques for finite model finding +option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false + only add one instantiation per quantifier per round for fmf +option fmfInstEngine --fmf-inst-engine bool :default false + use instantiation engine in conjunction with finite model finding +option fmfRelevantDomain --fmf-relevant-domain bool :default false + use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) + +endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h new file mode 100644 index 000000000..24734e8c8 --- /dev/null +++ b/src/theory/quantifiers/options_handlers.h @@ -0,0 +1,111 @@ +/********************* */ +/*! \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-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_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H +#define __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H + +#include <string> + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +static const std::string instWhenHelp = "\ +Modes currently supported by the --inst-when option:\n\ +\n\ +full\n\ ++ Run instantiation round at full effort, before theory combination.\n\ +\n\ +full-last-call (default)\n\ ++ Alternate running instantiation rounds at full effort and last\n\ + call. In other words, interleave instantiation and theory combination.\n\ +\n\ +last-call\n\ ++ Run instantiation at last call effort, after theory combination.\n\ +\n\ +"; + +static const std::string literalMatchHelp = "\ +Literal match modes currently supported by the --literal-match option:\n\ +\n\ +none (default)\n\ ++ Do not use literal matching.\n\ +\n\ +predicate\n\ ++ Consider the phase requirements of predicate literals when applying heuristic\n\ + quantifier instantiation. For example, the trigger P( x ) in the quantified \n\ + formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\ + terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\ + Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ +\n\ +"; + +inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "pre-full") { + return INST_WHEN_PRE_FULL; + } else if(optarg == "full") { + return INST_WHEN_FULL; + } else if(optarg == "full-last-call") { + return INST_WHEN_FULL_LAST_CALL; + } else if(optarg == "last-call") { + return INST_WHEN_LAST_CALL; + } else if(optarg == "help") { + puts(instWhenHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --inst-when: `") + + optarg + "'. Try --inst-when help."); + } +} + +inline void checkInstWhenMode(std::string option, InstWhenMode mode, SmtEngine* smt) throw(OptionException) { + if(mode == INST_WHEN_PRE_FULL) { + throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release."); + } +} + +inline LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "none") { + return LITERAL_MATCH_NONE; + } else if(optarg == "predicate") { + return LITERAL_MATCH_PREDICATE; + } else if(optarg == "equality") { + return LITERAL_MATCH_EQUALITY; + } else if(optarg == "help") { + puts(literalMatchHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --literal-matching: `") + + optarg + "'. Try --literal-matching help."); + } +} + +inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, SmtEngine* smt) throw(OptionException) { + if(mode == LITERAL_MATCH_EQUALITY) { + throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release."); + } +} + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index c397e9d05..800fa910c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,6 +15,7 @@ **/ #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; @@ -690,14 +691,14 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit } bool QuantifiersRewriter::doMiniscopingNoFreeVar(){ - return Options::current()->miniscopeQuantFreeVar; + return options::miniscopeQuantFreeVar(); } bool QuantifiersRewriter::doMiniscopingAnd(){ - if( Options::current()->miniscopeQuant ){ + if( options::miniscopeQuant() ){ return true; }else{ - if( Options::current()->cbqi ){ + if( options::cbqi() ){ return true; }else{ return false; @@ -709,13 +710,13 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) }else if( computeOption==COMPUTE_PRE_SKOLEM ){ - return Options::current()->preSkolemQuant && !duringRewrite; + return options::preSkolemQuant() && !duringRewrite; }else if( computeOption==COMPUTE_PRENEX ){ - return Options::current()->prenexQuant; + return options::prenexQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - return Options::current()->varElimQuant; + return options::varElimQuant(); }else if( computeOption==COMPUTE_CNF ){ - return Options::current()->cnfQuant && !duringRewrite;// || Options::current()->finiteModelFind; + return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind(); }else{ return false; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 945c82bf9..bb8fafb14 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -61,7 +61,7 @@ void TermDb::addTermEfficient( Node n, std::set< Node >& added){ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ //don't add terms in quantifier bodies - if( withinQuant && !Options::current()->registerQuantBodyTerms ){ + if( withinQuant && !options::registerQuantBodyTerms() ){ return; } if( d_processed.find( n )==d_processed.end() ){ @@ -82,7 +82,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); for( int i=0; i<(int)n.getNumChildren(); i++ ){ addTerm( n[i], added, withinQuant ); - if( Options::current()->efficientEMatching ){ + if( options::efficientEMatching() ){ if( d_parents[n[i]][op].empty() ){ //must add parent to equivalence class info Node nir = d_ith->getRepresentative( n[i] ); @@ -97,7 +97,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Assert(!getParents(n[i],op,i).empty()); } } - if( Options::current()->eagerInstQuant ){ + if( options::eagerInstQuant() ){ if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ int addedLemmas = 0; for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){ @@ -115,7 +115,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } } }else{ - if( Options::current()->efficientEMatching && !n.hasAttribute(InstConstantAttribute())){ + if( options::efficientEMatching() && !n.hasAttribute(InstConstantAttribute())){ //Efficient e-matching must be notified //The term in triggers are not important here Debug("term-db") << "New in this branch term " << n << std::endl; @@ -196,7 +196,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ Node mbt; if( d_type_map[ tn ].empty() ){ std::stringstream ss; - ss << Expr::setlanguage(Options::current()->outputLanguage); + ss << Expr::setlanguage(options::outputLanguage()); ss << "e_" << tn; mbt = NodeManager::currentNM()->mkVar( ss.str(), tn ); }else{ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 27310e21b..3d41d28b7 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -27,6 +27,7 @@ #include <map> #include <time.h> #include "theory/quantifiers/theory_quantifiers_instantiator.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" using namespace std; diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp index 84b6c65c7..8486a3a84 100644 --- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp +++ b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/theory_quantifiers_instantiator.h" #include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/options.h" #include "theory/theory_engine.h" using namespace std; @@ -32,7 +33,7 @@ Instantiator( c, ie, th ){ void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){ Debug("quant-quant-assert") << "InstantiatorTheoryQuantifiers::check: " << assertion << std::endl; - if( Options::current()->cbqi ){ + if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ Debug("quant-quant-assert") << " -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl; setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 471bc9ac1..4d94d8d83 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -22,6 +22,7 @@ #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" @@ -72,14 +73,14 @@ d_active( c ){ d_model = new quantifiers::FirstOrderModel( this, c, "FirstOrderModel" ); //add quantifiers modules - if( !Options::current()->finiteModelFind || Options::current()->fmfInstEngine ){ + if( !options::finiteModelFind() || options::fmfInstEngine() ){ //the instantiation must set incomplete flag unless finite model finding is turned on - d_inst_engine = new quantifiers::InstantiationEngine( this, !Options::current()->finiteModelFind ); + d_inst_engine = new quantifiers::InstantiationEngine( this, !options::finiteModelFind() ); d_modules.push_back( d_inst_engine ); }else{ d_inst_engine = NULL; } - if( Options::current()->finiteModelFind ){ + if( options::finiteModelFind() ){ d_model_engine = new quantifiers::ModelEngine( this ); d_modules.push_back( d_model_engine ); }else{ @@ -130,7 +131,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } //build the model if not done so already // this happens if no quantifiers are currently asserted and no model-building module is enabled - if( Options::current()->produceModels && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model_set ){ + if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model_set ){ d_te->getModelBuilder()->buildModel( d_model ); } } @@ -209,7 +210,7 @@ void QuantifiersEngine::registerQuantifier( Node f ){ Node ceBody = d_term_db->getCounterexampleBody( quants[q] ); generatePhaseReqs( quants[q], ceBody ); //also register it with the strong solver - if( Options::current()->finiteModelFind ){ + if( options::finiteModelFind() ){ ((uf::TheoryUF*)d_te->getTheory( THEORY_UF ))->getStrongSolver()->registerQuantifier( quants[q] ); } } @@ -253,7 +254,7 @@ void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ std::set< Node > added; getTermDatabase()->addTerm( n, added, withinQuant ); - if( Options::current()->efficientEMatching ){ + if( options::efficientEMatching() ){ uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF ); d_ith->newTerms(added); } @@ -423,7 +424,7 @@ void QuantifiersEngine::flushLemmas( OutputChannel* out ){ } void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ - if( Options::current()->literalMatchMode!=Options::LITERAL_MATCH_NONE ){ + if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE ){ bool printed = false; // doing literal-based matching (consider polarity of literals) for( int i=0; i<(int)nodes.size(); i++ ){ diff --git a/src/theory/rewriterules/options b/src/theory/rewriterules/options new file mode 100644 index 000000000..285e489be --- /dev/null +++ b/src/theory/rewriterules/options @@ -0,0 +1,14 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module REWRITE_RULES "theory/rewriterules/options.h" Rewrite Rules + +option efficientEMatching --efficient-e-matching bool :default false + use efficient E-matching (only for rewrite rules) + +option rewriteRulesAsAxioms --rewrite-rules-as-axioms bool :default false + whether to convert rewrite rules to usual axioms (for debugging only) + +endmodule diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 57bc6d9cf..b4ae93653 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -23,7 +23,7 @@ #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriter.h" -#include "util/options.h" +#include "theory/rewriterules/options.h" using namespace std; @@ -292,13 +292,13 @@ Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector<Node> & pattern // Debug("rewriterules") << "createTrigger:"; getQuantifiersEngine()->registerPattern(pattern); return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern, - Options::current()->efficientEMatching? + options::efficientEMatching()? Trigger::MATCH_GEN_EFFICIENT_E_MATCH : Trigger::MATCH_GEN_DEFAULT, true, Trigger::TR_MAKE_NEW, false); - // Options::current()->smartMultiTriggers); + // options::smartMultiTriggers()); }; bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested, diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index 1ad8fdaa7..edea7a3c0 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -21,7 +21,7 @@ #include "theory/rewriterules/theory_rewriterules_params.h" #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriterules/theory_rewriterules.h" -#include "util/options.h" +#include "theory/rewriterules/options.h" #include "theory/quantifiers/term_database.h" @@ -110,7 +110,7 @@ inline void addPattern(TheoryRewriteRules & re, if (tri.getKind() == kind::NOT && tri[0].getKind() == kind::APPLY_UF) tri = tri[0]; pattern.push_back( - Options::current()->rewriteRulesAsAxioms? + options::rewriteRulesAsAxioms()? static_cast<Node>(tri): re.getQuantifiersEngine()->getTermDatabase()-> convertNodeToPattern(tri,r,vars,inst_constants)); @@ -224,7 +224,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r) //If we convert to usual axioms - if(Options::current()->rewriteRulesAsAxioms){ + if(options::rewriteRulesAsAxioms()){ NodeBuilder<> forallB(kind::FORALL); forallB << r[0]; NodeBuilder<> guardsB(kind::AND); diff --git a/src/theory/rr_inst_match.h b/src/theory/rr_inst_match.h index d89b221bb..68b6e1bfd 100644 --- a/src/theory/rr_inst_match.h +++ b/src/theory/rr_inst_match.h @@ -35,6 +35,9 @@ #include "expr/node_manager.h" #include "expr/node_builder.h" +#include "theory/quantifiers/options.h" +#include "theory/rewriterules/options.h" + //#define USE_EFFICIENT_E_MATCHING namespace CVC4 { @@ -65,8 +68,8 @@ public: /** legal candidate */ static inline bool isLegalCandidate( TNode n ){ return !n.getAttribute(NoMatchAttribute()) && - ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute())) && - ( !Options::current()->efficientEMatching || n.hasAttribute(AvailableInTermDb()) ); + ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute())) && + ( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) ); } }; diff --git a/src/theory/theory.h b/src/theory/theory.h index 24551637b..f3a9db394 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -32,7 +32,7 @@ #include "context/context.h" #include "context/cdlist.h" #include "context/cdo.h" -#include "util/options.h" +#include "options/options.h" #include "util/stats.h" #include "util/dump.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1fb7305d4..6fbd4a417 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -24,7 +24,7 @@ #include "expr/attribute.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "util/options.h" +#include "options/options.h" #include "util/lemma_output_channel.h" #include "theory/theory.h" @@ -38,6 +38,7 @@ #include "theory/model.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/first_order_model.h" @@ -349,7 +350,7 @@ void TheoryEngine::check(Theory::Effort effort) { if( d_logicInfo.isQuantified() ){ ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->performCheck(Theory::EFFORT_LAST_CALL); // if we have given up, then possibly flip decision - if(Options::current()->flipDecision) { + if(options::flipDecision()) { if(d_incomplete && !d_inConflict && !d_lemmasAdded) { if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) { d_incomplete = false; @@ -357,7 +358,7 @@ void TheoryEngine::check(Theory::Effort effort) { } } //if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built - }else if( Options::current()->produceModels ){ + }else if( options::produceModels() ){ //must build model at this point d_curr_model_builder->buildModel( d_curr_model ); } @@ -1114,8 +1115,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable } // Share with other portfolio threads - if(Options::current()->lemmaOutputChannel != NULL) { - Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr()); + if(options::lemmaOutputChannel() != NULL) { + options::lemmaOutputChannel()->notifyNewLemma(node.toExpr()); } // Remove the ITEs diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 449f4adc3..de04c878c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -36,7 +36,8 @@ #include "theory/shared_terms_database.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" -#include "util/options.h" +#include "options/options.h" +#include "smt/options.h" #include "util/stats.h" #include "util/hash.h" #include "util/cache.h" diff --git a/src/theory/trigger.cpp b/src/theory/trigger.cpp index 92573d464..f895f6814 100644 --- a/src/theory/trigger.cpp +++ b/src/theory/trigger.cpp @@ -20,6 +20,7 @@ #include "theory/uf/theory_uf_instantiator.h" #include "theory/candidate_generator.h" #include "theory/uf/equality_engine.h" +#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; @@ -95,7 +96,7 @@ d_quantEngine( qe ), d_f( f ){ ++(qe->d_statistics.d_multi_triggers); } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; - if( Options::current()->eagerInstQuant ){ + if( options::eagerInstQuant() ){ Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF ); uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); for( int i=0; i<(int)d_nodes.size(); i++ ){ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 61330bbde..e027f8909 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -24,4 +24,6 @@ libuf_la_SOURCES = \ theory_uf_model.h \ theory_uf_model.cpp -EXTRA_DIST = kinds +EXTRA_DIST = \ + kinds \ + options_handlers.h diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 5696251ed..9d644ae8d 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -20,6 +20,7 @@ #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" #include "theory/uf/equality_engine.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" using namespace std; @@ -144,9 +145,9 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ //extend to literal matching d_quantEngine->getPhaseReqTerms( f, nodes ); //check match option - int matchOption = Options::current()->efficientEMatching ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; + int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, - Options::current()->smartTriggers ) ); + options::smartTriggers() ) ); } } @@ -298,11 +299,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ //} } //now, generate the trigger... - int matchOption = Options::current()->efficientEMatching ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; + int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; Trigger* tr = NULL; if( d_is_single_trigger[ patTerms[0] ] ){ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, - Options::current()->smartTriggers ); + options::smartTriggers() ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ //if we are re-generating triggers, shuffle based on some method @@ -316,7 +317,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } //will possibly want to get an old trigger tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, - Options::current()->smartTriggers ); + options::smartTriggers() ); } if( tr ){ if( tr->isMultiTrigger() ){ @@ -347,7 +348,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( d_quantEngine->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ d_single_trigger_gen[ patTerms[index] ] = true; Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, - Options::current()->smartTriggers ); + options::smartTriggers() ); if( tr2 ){ //Notice() << "Add additional trigger " << patTerms[index] << std::endl; tr2->resetInstantiationRound(); diff --git a/src/theory/uf/options b/src/theory/uf/options new file mode 100644 index 000000000..6f6900da0 --- /dev/null +++ b/src/theory/uf/options @@ -0,0 +1,12 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module UF "theory/uf/options.h" Uninterpreted functions theory + +option ufSymmetryBreaker uf-symmetry-breaker --enable-symmetry-breaker/--disable-symmetry-breaker bool :read-write :default true + use UF symmetry breaker (Deharbe et al., CADE 2011) +/turns off UF symmetry breaker (Deharbe et al., CADE 2011) + +endmodule diff --git a/src/theory/uf/options_handlers.h b/src/theory/uf/options_handlers.h new file mode 100644 index 000000000..b08ae9d64 --- /dev/null +++ b/src/theory/uf/options_handlers.h @@ -0,0 +1,33 @@ +/********************* */ +/*! \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-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 Custom handlers and predicates for TheoryUF options + ** + ** Custom handlers and predicates for TheoryUF options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__OPTIONS_HANDLERS_H +#define __CVC4__THEORY__UF__OPTIONS_HANDLERS_H + +namespace CVC4 { +namespace theory { +namespace uf { + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__UF__OPTIONS_HANDLERS_H */ + diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index d24878a62..5b8470567 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -18,6 +18,8 @@ **/ #include "theory/uf/theory_uf.h" +#include "theory/uf/options.h" +#include "theory/quantifiers/options.h" #include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/model.h" @@ -33,7 +35,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ - d_thss(Options::current()->finiteModelFind ? new StrongSolverTheoryUf(c, u, out, this) : NULL), + d_thss(options::finiteModelFind() ? new StrongSolverTheoryUf(c, u, out, this) : NULL), d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"), d_conflict(c, false), d_literalsToPropagate(c), @@ -179,7 +181,7 @@ void TheoryUF::presolve() { // TimerStat::CodeTimer codeTimer(d_presolveTimer); Debug("uf") << "uf: begin presolve()" << endl; - if(Options::current()->ufSymmetryBreaker) { + if(options::ufSymmetryBreaker()) { vector<Node> newClauses; d_symb.apply(newClauses); for(vector<Node>::const_iterator i = newClauses.begin(); @@ -299,7 +301,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { } } - if(Options::current()->ufSymmetryBreaker) { + if(options::ufSymmetryBreaker()) { d_symb.assertFormula(n); } }/* TheoryUF::ppStaticLearn() */ diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index 48092b340..ea253cbdb 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -19,6 +19,8 @@ #include "theory/uf/theory_uf.h" #include "theory/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/rewriterules/options.h" #include "theory/quantifiers/term_database.h" using namespace std; @@ -91,11 +93,11 @@ inline void outputEqClassInfo( const char* c, const EqClassInfo* eci){ InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) : Instantiator( c, qe, th ) { - if( !Options::current()->finiteModelFind || Options::current()->fmfInstEngine ){ - if( Options::current()->cbqi ){ + if( !options::finiteModelFind() || options::fmfInstEngine() ){ + if( options::cbqi() ){ addInstStrategy( new InstStrategyCheckCESolved( this, qe ) ); } - if( Options::current()->userPatternsQuant ){ + if( options::userPatternsQuant() ){ d_isup = new InstStrategyUserPatterns( this, qe ); addInstStrategy( d_isup ); }else{ @@ -106,7 +108,7 @@ Instantiator( c, qe, th ) i_ag->setGenerateAdditional( true ); addInstStrategy( i_ag ); //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) ); - if( !Options::current()->finiteModelFind ){ + if( !options::finiteModelFind() ){ addInstStrategy( new InstStrategyFreeVariable( this, qe ) ); } //d_isup->setPriorityOver( i_ag ); @@ -124,7 +126,7 @@ void InstantiatorTheoryUf::assertNode( Node assertion ) Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl; //preRegisterTerm( assertion ); 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()) ){ @@ -337,7 +339,7 @@ void InstantiatorTheoryUf::newTerms(SetNode& s){ /** merge */ void InstantiatorTheoryUf::merge( TNode a, TNode b ){ - if( Options::current()->efficientEMatching ){ + if( options::efficientEMatching() ){ //merge eqc_ops of b into a EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a ); EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b ); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 895a7d056..70b07daa6 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -19,6 +19,7 @@ #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf_instantiator.h" #include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" //#define USE_SMART_SPLITS @@ -194,7 +195,7 @@ struct sortExternalDegree { }; bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality ){ - if( Options::current()->ufssRegions && d_total_diseq_external>=long(cardinality) ){ + if( options::ufssRegions() && d_total_diseq_external>=long(cardinality) ){ //The number of external disequalities is greater than or equal to cardinality. //Thus, a clique of size cardinality+1 may exist between nodes in d_regions[i] and other regions //Check if this is actually the case: must have n nodes with outgoing degree (cardinality+1-n) for some n>0 @@ -243,7 +244,7 @@ bool StrongSolverTheoryUf::ConflictFind::Region::check( Theory::Effort level, in } } return true; - }else if( Options::current()->ufssRegions || Options::current()->ufssEagerSplits || level==Theory::EFFORT_FULL ){ + }else if( options::ufssRegions() || options::ufssEagerSplits() || level==Theory::EFFORT_FULL ){ //build test clique, up to size cardinality+1 if( d_testCliqueSize<=long(cardinality) ){ std::vector< Node > newClique; @@ -584,7 +585,7 @@ void StrongSolverTheoryUf::ConflictFind::explainClique( std::vector< Node >& cli /** new node */ void StrongSolverTheoryUf::ConflictFind::newEqClass( Node n ){ if( d_regions_map.find( n )==d_regions_map.end() ){ - if( !Options::current()->ufssRegions ){ + if( !options::ufssRegions() ){ //if not using regions, always add new equivalence classes to region index = 0 d_regions_index = 0; } @@ -594,7 +595,7 @@ void StrongSolverTheoryUf::ConflictFind::newEqClass( Node n ){ if( d_regions_index<d_regions.size() ){ d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true); d_regions[ d_regions_index ]->d_valid = true; - Assert( !Options::current()->ufssRegions || d_regions[ d_regions_index ]->getNumReps()==0 ); + Assert( !options::ufssRegions() || d_regions[ d_regions_index ]->getNumReps()==0 ); }else{ d_regions.push_back( new Region( this, d_th->getSatContext() ) ); } @@ -882,7 +883,7 @@ void StrongSolverTheoryUf::ConflictFind::check( Theory::Effort level, OutputChan } bool addedLemma = false; //do splitting on demand - if( level==Theory::EFFORT_FULL || Options::current()->ufssEagerSplits ){ + if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){ Debug("uf-ss-debug") << "Add splits?" << std::endl; //see if we have any recommended splits from large regions for( int i=0; i<(int)d_regions_index; i++ ){ @@ -902,7 +903,7 @@ void StrongSolverTheoryUf::ConflictFind::check( Theory::Effort level, OutputChan if( level==Theory::EFFORT_FULL ){ if( !addedLemma ){ Debug("uf-ss") << "No splits added." << std::endl; - if( Options::current()->ufssColoringSat ){ + if( options::ufssColoringSat() ){ //otherwise, try to disambiguate individual terms if( !disambiguateTerms( out ) ){ //no disequalities can be propagated @@ -1000,7 +1001,7 @@ void StrongSolverTheoryUf::ConflictFind::setCardinality( int c, OutputChannel* o } void StrongSolverTheoryUf::ConflictFind::getRepresentatives( std::vector< Node >& reps ){ - if( !Options::current()->ufssColoringSat ){ + if( !options::ufssColoringSat() ){ bool foundRegion = false; for( int i=0; i<(int)d_regions_index; i++ ){ //should not have multiple regions at this point @@ -1045,7 +1046,7 @@ Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){ if( d_cardinality_lemma.find( d_cardinality )==d_cardinality_lemma.end() ){ if( d_cardinality_lemma_term.isNull() ){ std::stringstream ss; - ss << Expr::setlanguage(Options::current()->outputLanguage); + ss << Expr::setlanguage(options::outputLanguage()); ss << "t_" << d_type; d_cardinality_lemma_term = NodeManager::currentNM()->mkVar( ss.str(), d_type ); } |