diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/uf/inst_strategy.cpp | 13 | ||||
-rw-r--r-- | src/theory/uf/options | 12 | ||||
-rw-r--r-- | src/theory/uf/options_handlers.h | 33 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 8 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.cpp | 14 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 17 |
7 files changed, 77 insertions, 24 deletions
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 ); } |