summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/Makefile.am4
-rw-r--r--src/theory/uf/inst_strategy.cpp13
-rw-r--r--src/theory/uf/options12
-rw-r--r--src/theory/uf/options_handlers.h33
-rw-r--r--src/theory/uf/theory_uf.cpp8
-rw-r--r--src/theory/uf/theory_uf_instantiator.cpp14
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp17
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 );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback