summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/Makefile.am8
-rw-r--r--src/theory/quantifiers/first_order_model.cpp6
-rw-r--r--src/theory/quantifiers/inst_when_mode.cpp47
-rw-r--r--src/theory/quantifiers/inst_when_mode.h49
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp33
-rw-r--r--src/theory/quantifiers/literal_match_mode.cpp43
-rw-r--r--src/theory/quantifiers/literal_match_mode.h47
-rw-r--r--src/theory/quantifiers/model_builder.cpp10
-rw-r--r--src/theory/quantifiers/model_engine.cpp17
-rw-r--r--src/theory/quantifiers/options89
-rw-r--r--src/theory/quantifiers/options_handlers.h111
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp15
-rw-r--r--src/theory/quantifiers/term_database.cpp10
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp1
-rw-r--r--src/theory/quantifiers/theory_quantifiers_instantiator.cpp3
15 files changed, 442 insertions, 47 deletions
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()) );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback