diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/Makefile.am | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_when_mode.cpp | 47 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_when_mode.h | 49 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 33 | ||||
-rw-r--r-- | src/theory/quantifiers/literal_match_mode.cpp | 43 | ||||
-rw-r--r-- | src/theory/quantifiers/literal_match_mode.h | 47 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 89 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 111 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_instantiator.cpp | 3 |
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()) ); |