summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp3
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp29
-rw-r--r--src/theory/quantifiers/trigger.cpp11
-rw-r--r--src/theory/quantifiers/trigger.h1
-rw-r--r--src/theory/quantifiers_engine.cpp7
5 files changed, 26 insertions, 25 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index c775bb558..0b8e0e462 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -700,7 +700,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
d_tg_alloc[0].reset( this, TypeNode::null() );
while( d_tg_alloc[0].getNextTerm( this, depth ) ){
Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth );
- if( d_tg_alloc[0].getDepth( this )==depth ){
+ //if( d_tg_alloc[0].getDepth( this )==depth ){
+ if( (int)d_tg_gdepth==d_tg_gdepth_limit ){
//construct term
Node nn = d_tg_alloc[0].getTerm( this );
if( getUniversalRepresentative( nn )==nn ){
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index df7f06aff..ef1997d4c 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -68,12 +68,12 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
bool processTrigger = true;
if( processTrigger ){
- //if( d_user_gen[f][i]->isMultiTrigger() )
- Trace("process-trigger") << " Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl;
+ Trace("process-trigger") << " Process (user) ";
+ d_user_gen[f][i]->debugPrint("process-trigger");
+ Trace("process-trigger") << "..." << std::endl;
InstMatch baseMatch( f );
int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
- //if( d_user_gen[f][i]->isMultiTrigger() )
- Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
+ Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
if( d_user_gen[f][i]->isMultiTrigger() ){
d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
@@ -89,17 +89,22 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
//add to generators
+ bool usable = true;
std::vector< Node > nodes;
for( int i=0; i<(int)pat.getNumChildren(); i++ ){
nodes.push_back( pat[i] );
+ if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], f ) ){
+ Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
+ usable = false;
+ break;
+ }
}
- if( Trigger::isUsableTrigger( nodes, f ) ){
+ if( usable ){
//extend to literal matching
d_quantEngine->getPhaseReqTerms( f, nodes );
//check match option
int matchOption = 0;
- d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
- options::smartTriggers() ) );
+ d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
}
}
@@ -156,14 +161,12 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
bool processTrigger = itt->second;
if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
d_processed_trigger[f][tr] = true;
- //if( tr->isMultiTrigger() )
- Trace("process-trigger") << " Process ";
- tr->debugPrint("process-trigger");
- Trace("process-trigger") << "..." << std::endl;
+ Trace("process-trigger") << " Process ";
+ tr->debugPrint("process-trigger");
+ Trace("process-trigger") << "..." << std::endl;
InstMatch baseMatch( f );
int numInst = tr->addInstantiations( baseMatch );
- //if( tr->isMultiTrigger() )
- Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
+ Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;
}else{
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 4a99852d1..11ec0210d 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -210,15 +210,6 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt
return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
}
-bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
- for( int i=0; i<(int)nodes.size(); i++ ){
- if( !isUsableTrigger( nodes[i], f ) ){
- return false;
- }
- }
- return true;
-}
-
bool Trigger::isUsable( Node n, Node f ){
if( quantifiers::TermDb::getInstConstAttr(n)==f ){
if( isAtomicTrigger( n ) ){
@@ -234,7 +225,7 @@ bool Trigger::isUsable( Node n, Node f ){
std::map< Node, Node > coeffs;
if( isBooleanTermTrigger( n ) ){
return true;
- }
+ }
}
return false;
}else{
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 1a3ae3fcd..74a87591f 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -105,7 +105,6 @@ public:
static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false );
public:
/** is usable trigger */
- static bool isUsableTrigger( std::vector< Node >& nodes, Node f );
static bool isUsableTrigger( Node n, Node f );
static bool isAtomicTrigger( Node n );
static bool isAtomicTriggerKind( Kind k );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a00592e8b..4c29c8f9a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -195,6 +195,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
//reset relevant information
d_conflict = false;
d_hasAddedLemma = false;
+
+ //flush previous lemmas (for instance, if was interupted)
+ flushLemmas();
+ if( d_hasAddedLemma ){
+ return;
+ }
+
d_term_db->reset( e );
d_eq_query->reset();
if( d_rel_dom ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback