From: Andrew Reynolds Date: Sat, 4 Jan 2014 04:36:55 +0000 (-0600) Subject: Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen... X-Git-Tag: cvc5-1.0.0~7167 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ce92038d8455637e313a1c2d0ce5d31a3d42b10;p=cvc5.git Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 539622877..014d3c603 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1142,16 +1142,9 @@ void SmtEngine::setLogicInternal() throw() { options::instWhenMode.set( INST_WHEN_LAST_CALL ); } } - if ( ! options::fmfInstGen.wasSetByUser()) { - //if full model checking is on, disable inst-gen techniques - if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ - options::fmfInstGen.set( false ); - }else{ - options::fmfInstGen.set( true ); - } - } if ( options::fmfBoundInt() ){ - if( options::mbqiMode()!=quantifiers::MBQI_NONE ){ + if( options::mbqiMode()!=quantifiers::MBQI_NONE && + options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){ //if bounded integers are set, must use full model check for MBQI options::mbqiMode.set( quantifiers::MBQI_FMC ); } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index c94775aec..797ca8f70 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -169,7 +169,7 @@ void FirstOrderModelIG::resetEvaluate(){ // each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ ++d_eval_formulas; - //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl; + Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl; //Notice() << "Eval " << n << std::endl; if( n.getKind()==NOT ){ int val = evaluate( n[0], depIndex, ri ); @@ -447,7 +447,7 @@ void FirstOrderModelIG::makeEvalUfModel( Node n ){ d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] ); d_uf_model_gen[op].makeModel( this, d_eval_uf_model[n] ); //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl; - //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 ); + //d_eval_uf_model[n].debugPrint( std::cout, d_qe->getModel(), 2 ); } } } @@ -578,7 +578,7 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a void FirstOrderModelFmc::processInitialize( bool ispre ) { if( ispre ){ - if( options::fmfFmcInterval() && intervalOp.isNull() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && intervalOp.isNull() ){ std::vector< TypeNode > types; for(unsigned i=0; i<2; i++){ types.push_back(NodeManager::currentNM()->integerType()); @@ -616,7 +616,7 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) { Node FirstOrderModelFmc::getStarElement(TypeNode tn) { Node st = getStar(tn); - if( options::fmfFmcInterval() && tn.isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && tn.isInteger() ){ st = getInterval( st, st ); } return st; diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 174e26a5a..c7d7b7415 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -60,9 +60,9 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { return true; } } - if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){ + if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){ //for star: check if all children are defined and have generalizations - if( options::fmfFmcCoverSimplify() && c[index]==st ){ + if( c[index]==st ){ ///options::fmfFmcCoverSimplify() //check if all children exist and are complete int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0); if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){ @@ -92,7 +92,7 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector return d_data; }else{ int minIndex = -1; - if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){ for( std::map::iterator it = d_child.begin(); it != d_child.end(); ++it ){ //if( !m->isInterval( it->first ) ){ // std::cout << "Not an interval during getGenIndex " << it->first << std::endl; @@ -327,7 +327,7 @@ QModelBuilder( c, qe ){ bool FullModelChecker::optBuildAtFullModel() { //need to build after full model has taken effect if we are constructing interval models // this is because we need to have a constant in all integer equivalence classes - return options::fmfFmcInterval(); + return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL; } void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ @@ -443,7 +443,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; } children.push_back(ri); - if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){ + if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ if (fm->isModelBasisTerm(ri) ) { ri = fm->getStar( ri.getType() ); }else{ @@ -485,7 +485,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } - if( options::fmfFmcInterval() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){ convertIntervalModel( fm, op ); } @@ -1103,7 +1103,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, } }else{ if( !v.isNull() ){ - if( options::fmfFmcInterval() && v.getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && v.getType().isInteger() ){ for (std::map::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { if( fm->isInRange( v, it->first ) ){ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); @@ -1165,7 +1165,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c Trace("fmc-debug3") << "isCompat " << c << std::endl; Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; i & co Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; i & cond ) { - Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl; + Trace("fmc-debug") << "Make default vec, intervals = " << (options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL) << std::endl; //get function symbol for f cond.push_back(d_quant_cond[f]); for (unsigned i=0; iaddInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ - d_quant_basis_match_added[f] = true; - return 1; - }else{ - //shouldn't happen usually, but will occur if x != y is a required literal for f. - //Notice() << "No model basis for " << f << std::endl; - d_quant_basis_match_added[f] = false; - } + Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; + //add model basis instantiation + if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ + d_quant_basis_match_added[f] = true; + return 1; + }else{ + //shouldn't happen usually, but will occur if x != y is a required literal for f. + //Notice() << "No model basis for " << f << std::endl; + d_quant_basis_match_added[f] = false; } } return 0; @@ -418,6 +416,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i //if evaluate(...)==1, then the instantiation is already true in the model // depIndex is the index of the least significant variable that this evaluation relies upon depIndex = riter.getNumTerms()-1; + Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermDatabase()->getInstConstantBody( f ) << std::endl; eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); if( eval==1 ){ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 5006a8a61..f314584cd 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -37,7 +37,7 @@ ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ){ Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; - if( options::mbqiMode()==MBQI_FMC || options::fmfBoundInt() ){ + if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){ Trace("model-engine-debug") << "...make fmc builder." << std::endl; d_builder = new fmcheck::FullModelChecker( c, qe ); }else if( options::mbqiMode()==MBQI_INTERVAL ){ @@ -212,7 +212,7 @@ int ModelEngine::checkModel(){ } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1; + int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : 1; for( int e=0; egetNumAssertedQuantifiers(); i++ ){ @@ -230,6 +230,8 @@ int ModelEngine::checkModel(){ if( optOneQuantPerRound() && d_addedLemmas>0 ){ break; } + }else{ + Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl; } } } @@ -248,11 +250,12 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ d_builder->d_addedLemmas = 0; d_builder->d_incomplete_check = false; if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ + Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl; d_triedLemmas += d_builder->d_triedLemmas; d_addedLemmas += d_builder->d_addedLemmas; d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check; }else{ - Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; + Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; Debug("inst-fmf-ei") << " Instantiation Constants: "; for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 7c4cb3651..d5c755ad2 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -65,7 +65,7 @@ typedef enum { /** mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, /** mbqi with integer intervals */ - //MBQI_FMC_INTERVAL, + MBQI_FMC_INTERVAL, /** mbqi with interval abstraction of uninterpreted sorts */ MBQI_INTERVAL, } MbqiMode; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index f485b981c..190c7ddc9 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -76,9 +76,8 @@ option eagerInstQuant --eager-inst-quant bool :default false option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.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 cbqi --enable-cbqi bool :default false + turns on counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default false turns on recursive counterexample-based quantifier instantiation @@ -97,30 +96,23 @@ option finiteModelFind --finite-model-find bool :default false option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation +option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false + only add one instantiation per quantifier per round for mbqi +option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false + only add instantiations for one quantifier per round for mbqi -option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true - disable simple models in full model check for finite model finding -option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true - disable covering simplification of fmc models -option fmfFmcInterval --fmf-fmc-interval bool :default false - construct interval models for fmc models - -option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false - only add one instantiation per quantifier per round for fmf -option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false - only add instantiations for one 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) -option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true - enable Inst-Gen instantiation techniques for finite model finding (default) -/disable Inst-Gen instantiation techniques for finite model finding +option fmfInstGen /--disable-fmf-inst-gen bool :default true + disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques - +option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true + disable simple models in full model check for finite model finding option fmfBoundInt --fmf-bound-int bool :default false finite model finding on bounded integer quantification diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index a119bcaf6..4929fa60b 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -87,9 +87,12 @@ instgen \n\ + Use instantiation algorithm that mimics Inst-Gen calculus. \n\ \n\ fmc \n\ -+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ Modulo Theories.\n\ \n\ +fmc-interval \n\ ++ Same as fmc, but with intervals for models of integer functions.\n\ +\n\ interval \n\ + Use algorithm that abstracts domain elements as intervals. \n\ \n\ @@ -166,6 +169,8 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi return MBQI_INST_GEN; } else if(optarg == "fmc") { return MBQI_FMC; + } else if(optarg == "fmc-interval") { + return MBQI_FMC_INTERVAL; } else if(optarg == "interval") { return MBQI_INTERVAL; } else if(optarg == "help") { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0388a2979..5def2a832 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -51,7 +51,8 @@ d_lemmas_produced_c(u){ Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; //the model object - if( options::mbqiMode()==quantifiers::MBQI_FMC || options::fmfBoundInt() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC || + options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" ); diff --git a/src/theory/uf/options b/src/theory/uf/options index cfa6e6c04..26f87da79 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -15,20 +15,14 @@ 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 ufssTotality --uf-ss-totality bool :default false always use totality axioms for enforcing cardinality constraints option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1 apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default) -option ufssTotalityLazy --uf-ss-totality-lazy bool :default false - apply totality axioms lazily option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false apply symmetry breaking for totality axioms option ufssAbortCardinality --uf-ss-abort-card=N int :default -1 tells the uf strong solver a cardinality to abort at (-1 == no limit, default) -option ufssSmartSplits --uf-ss-smart-split bool :default false - use smart splitting heuristic for uf strong solver option ufssExplainedCliques --uf-ss-explained-cliques bool :default false use explained clique lemmas for uf strong solver option ufssSimpleCliques --uf-ss-simple-cliques bool :default true diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index a4cefe269..54a3075a1 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -428,12 +428,10 @@ void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){ void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){ if( !d_conflict ){ if( d_regions_map.find( n )==d_regions_map.end() ){ - if( !options::ufssTotalityLazy() ){ - //must generate totality axioms for every cardinality we have allocated thus far - for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){ - if( applyTotality( it->first ) ){ - addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() ); - } + //must generate totality axioms for every cardinality we have allocated thus far + for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){ + if( applyTotality( it->first ) ){ + addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() ); } } if( options::ufssTotality() ){ @@ -449,9 +447,6 @@ void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){ d_regions_index = 0; } d_regions_map[n] = d_regions_index; - if( options::ufssSmartSplits() ){ - setSplitScore( n, 0 ); - } Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n << std::endl; Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl; if( d_regions_indexgetOutputChannel() ); - } - } - } - } - }else{ + if( !applyTotality( d_cardinality ) ){ //do splitting on demand bool addedLemma = false; if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){ @@ -1073,7 +1057,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ //out->propagateAsDecision( lem[0] ); d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality ); - if( applyTotality( d_aloc_cardinality ) && !options::ufssTotalityLazy() ){ + if( applyTotality( d_aloc_cardinality ) ){ //must send totality axioms for each existing term for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){ addTotalityAxiom( (*it).first, d_aloc_cardinality, &d_thss->getOutputChannel() ); @@ -1085,27 +1069,11 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ Node s; if( r->hasSplits() ){ - if( !options::ufssSmartSplits() ){ - //take the first split you find - for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){ - if( (*it).second ){ - s = (*it).first; - break; - } - } - }else{ - int maxScore = -1; - std::vector< Node > splits; - for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){ - if( (*it).second ){ - int score1 = d_split_score[ (*it).first[0] ]; - int score2 = d_split_score[ (*it).first[1] ]; - int score = score1maxScore ){ - maxScore = -1; - s = (*it).first; - } - } + //take the first split you find + for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){ + if( (*it).second ){ + s = (*it).first; + break; } } Assert( s!=Node::null() ); @@ -1474,11 +1442,6 @@ Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) { StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ) { - if( options::ufssColoringSat() ){ - d_term_amb = new TermDisambiguator( th->getQuantifiersEngine(), c ); - }else{ - d_term_amb = NULL; - } if( options::ufssDiseqPropagation() ){ d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this ); }else{ @@ -1628,13 +1591,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ if( level==Theory::EFFORT_FULL ){ debugPrint( "uf-ss-debug" ); } - if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){ - int lemmas = d_term_amb->disambiguateTerms( d_out ); - d_statistics.d_disamb_term_lemmas += lemmas; - if( lemmas>=0 ){ - return; - } - } for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ it->second->check( level, d_out ); if( it->second->isConflict() ){ @@ -1646,11 +1602,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ if( !d_conflict && options::ufssSymBreak() ){ d_sym_break->check( level ); } - //disambiguate terms if necessary - //if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){ - // Assert( d_term_amb!=NULL ); - // d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out ); - //} Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl; } } @@ -1918,76 +1869,6 @@ StrongSolverTheoryUF::Statistics::~Statistics(){ } -int TermDisambiguator::disambiguateTerms( OutputChannel* out ){ - Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl; - int lemmaAdded = 0; - //otherwise, determine ambiguous pairs of ground terms for relevant sorts - quantifiers::TermDb* db = d_qe->getTermDatabase(); - for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){ - Debug("uf-ss-disamb") << "Check " << it->first << std::endl; - if( it->second.size()>1 ){ - if(involvesRelevantType( it->second[0] ) ){ - for( int i=0; i<(int)it->second.size(); i++ ){ - for( int j=(i+1); j<(int)it->second.size(); j++ ){ - Kind knd = it->second[i].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL; - Node eq = NodeManager::currentNM()->mkNode( knd, it->second[i], it->second[j] ); - eq = Rewriter::rewrite(eq); - //determine if they are ambiguous - if( d_term_amb.find( eq )==d_term_amb.end() ){ - Debug("uf-ss-disamb") << "Check disambiguate " << it->second[i] << " " << it->second[j] << std::endl; - d_term_amb[ eq ] = true; - //if they are equal - if( d_qe->getEqualityQuery()->areEqual( it->second[i], it->second[j] ) ){ - d_term_amb[ eq ] = false; - }else{ - //if an argument is disequal, then they are not ambiguous - for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){ - if( d_qe->getEqualityQuery()->areDisequal( it->second[i][k], it->second[j][k] ) ){ - d_term_amb[ eq ] = false; - break; - } - } - } - if( d_term_amb[ eq ] ){ - Debug("uf-ss-disamb") << "Disambiguate " << it->second[i] << " " << it->second[j] << std::endl; - //must add lemma - std::vector< Node > children; - children.push_back( eq ); - for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){ - Kind knd2 = it->second[i][k].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL; - Node eqc = NodeManager::currentNM()->mkNode( knd2, it->second[i][k], it->second[j][k] ); - children.push_back( eqc.notNode() ); - } - Assert( children.size()>1 ); - Node lem = NodeManager::currentNM()->mkNode( OR, children ); - Trace( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl; - //Notice() << "*** Disambiguate lemma : " << lem << std::endl; - out->lemma( lem ); - d_term_amb[ eq ] = false; - lemmaAdded++; - return lemmaAdded; - } - } - } - } - } - } - } - Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl; - return lemmaAdded; -} - -bool TermDisambiguator::involvesRelevantType( Node n ){ - if( n.getKind()==APPLY_UF ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getType().isSort() ){ - return true; - } - } - } - return false; -} - DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss) : d_qe(qe), d_ufss(ufss){ d_true = NodeManager::currentNM()->mkConst( true ); diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 4f41ebf2e..3ed1ea985 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -37,7 +37,6 @@ class SubsortSymmetryBreaker; namespace uf { class TheoryUF; -class TermDisambiguator; class DisequalityPropagator; class StrongSolverTheoryUF{ @@ -320,8 +319,6 @@ private: /** check */ void checkCombinedCardinality(); private: - /** term disambiguator */ - TermDisambiguator* d_term_amb; /** disequality propagator */ DisequalityPropagator* d_deq_prop; /** symmetry breaking techniques */ @@ -331,8 +328,6 @@ public: ~StrongSolverTheoryUF() {} /** get theory */ TheoryUF* getTheory() { return d_th; } - /** term disambiguator */ - TermDisambiguator* getTermDisambiguator() { return d_term_amb; } /** disequality propagator */ DisequalityPropagator* getDisequalityPropagator() { return d_deq_prop; } /** symmetry breaker */ @@ -401,23 +396,6 @@ public: Statistics d_statistics; };/* class StrongSolverTheoryUF */ - -class TermDisambiguator -{ -private: - /** quantifiers engine */ - QuantifiersEngine* d_qe; - /** whether two terms are ambiguous (indexed by equalities) */ - context::CDHashMap d_term_amb; - /** involves relevant type */ - static bool involvesRelevantType( Node n ); -public: - TermDisambiguator( QuantifiersEngine* qe, context::Context* c ) : d_qe( qe ), d_term_amb( c ){} - ~TermDisambiguator(){} - /** check ambiguous terms */ - int disambiguateTerms( OutputChannel* out ); -}; - class DisequalityPropagator { private: