diff options
Diffstat (limited to 'src/theory/quantifiers')
5 files changed, 26 insertions, 12 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 72e7d7e68..272914c25 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -302,7 +302,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, // this helps robustness, since picking the same literal every time may // lead to a stream of value instantiations, whereas with randomization // we may find an invertible literal that leads to a useful instantiation. - std::random_shuffle(iti->second.begin(), iti->second.end()); + std::shuffle(iti->second.begin(), iti->second.end(), Random::getRandom()); if (Trace.isOn("cegqi-bv")) { diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 0dc704219..1d2f9a322 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" +#include "util/random.h" using namespace CVC4; using namespace CVC4::kind; @@ -773,7 +774,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) d_tge.d_var_id[ it->first ] = it->second; d_tge.d_var_limit[ it->first ] = it->second; } - std::random_shuffle( rt_types.begin(), rt_types.end() ); + std::shuffle(rt_types.begin(), rt_types.end(), Random::getRandom()); std::map< TypeNode, std::vector< Node > > conj_rhs; for( unsigned i=0; i<rt_types.size(); i++ ){ @@ -1812,11 +1813,17 @@ void TermGenEnv::collectSignatureInformation() { } } //shuffle functions - for( std::map< TypeNode, std::vector< TNode > >::iterator it = d_typ_tg_funcs.begin(); it != d_typ_tg_funcs.end(); ++it ){ - std::random_shuffle( it->second.begin(), it->second.end() ); - if( it->first.isNull() ){ + for (std::map<TypeNode, std::vector<TNode> >::iterator it = + d_typ_tg_funcs.begin(); + it != d_typ_tg_funcs.end(); + ++it) + { + std::shuffle(it->second.begin(), it->second.end(), Random::getRandom()); + if (it->first.isNull()) + { Trace("sg-gen-tg-debug") << "In this order : "; - for( unsigned i=0; i<it->second.size(); i++ ){ + for (unsigned i = 0; i < it->second.size(); i++) + { Trace("sg-gen-tg-debug") << it->second[i] << " "; } Trace("sg-gen-tg-debug") << std::endl; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index cfcfcc5a5..6784fb8e3 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" +#include "util/random.h" using namespace std; @@ -453,10 +454,15 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ return; } } - //if we are re-generating triggers, shuffle based on some method - if( d_made_multi_trigger[f] ){ - std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly - }else{ + // if we are re-generating triggers, shuffle based on some method + if (d_made_multi_trigger[f]) + { + std::shuffle(patTerms.begin(), + patTerms.end(), + Random::getRandom()); // shuffle randomly + } + else + { d_made_multi_trigger[f] = true; } //will possibly want to get an old trigger diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index d1217d01d..c262c77e5 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -79,7 +79,7 @@ Node SygusUnif::constructBestStringToConcat( { Assert(!strs.empty()); std::vector<Node> strs_tmp = strs; - std::random_shuffle(strs_tmp.begin(), strs_tmp.end()); + std::shuffle(strs_tmp.begin(), strs_tmp.end(), Random::getRandom()); // prefer one that has incremented by more than 0 for (const Node& ns : strs_tmp) { diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 4fe3cfbed..bd9274f91 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1143,7 +1143,8 @@ Node SygusUnifIo::constructSol( // try a random strategy if (snode.d_strats.size() > 1) { - std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end()); + std::shuffle( + snode.d_strats.begin(), snode.d_strats.end(), Random::getRandom()); } // ITE always first if we have not yet solved // the reasoning is that splitting on conditions only subdivides the problem |