summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/ematching/inst_match_generator.cpp13
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp45
-rw-r--r--src/theory/quantifiers/quant_conflict_find.h8
3 files changed, 48 insertions, 18 deletions
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index eb3f6232d..78fb987f1 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -426,6 +426,7 @@ int InstMatchGenerator::getNextMatch(Node f,
Node t = d_curr_first_candidate;
do{
Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
+ Assert(!qe->inConflict());
//if t not null, try to fit it into match m
if( !t.isNull() ){
if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
@@ -439,7 +440,7 @@ int InstMatchGenerator::getNextMatch(Node f,
}
//get the next candidate term t
if( success<0 ){
- t = d_cg->getNextCandidate();
+ t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate();
}else{
d_curr_first_candidate = d_cg->getNextCandidate();
}
@@ -1029,10 +1030,11 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
if( d_pol ){
tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
}else{
- Node r = qe->getEqualityQuery()->getRepresentative( d_eqc );
//iterate over all classes except r
tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
- if( tat ){
+ if (tat && !qe->inConflict())
+ {
+ Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
if( it->first!=r ){
InstMatch m( q );
@@ -1042,12 +1044,13 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
}
}
}
- tat = NULL;
}
+ tat = nullptr;
}
}
Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
- if( tat ){
+ if (tat && !qe->inConflict())
+ {
InstMatch m( q );
addInstantiations( m, qe, addedLemmas, 0, tat );
}
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 02c9aedf5..92a355348 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -268,7 +268,10 @@ bool QuantInfo::reset_round( QuantConflictFind * p ) {
d_mg->reset_round( p );
for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
- it->second->reset_round( p );
+ if (!it->second->reset_round(p))
+ {
+ return false;
+ }
}
//now, reset for matching
d_mg->reset( p, false, this );
@@ -1178,11 +1181,14 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars
}
}
-
-void MatchGen::reset_round( QuantConflictFind * p ) {
+bool MatchGen::reset_round(QuantConflictFind* p)
+{
d_wasSet = false;
for( unsigned i=0; i<d_children.size(); i++ ){
- d_children[i].reset_round( p );
+ if (!d_children[i].reset_round(p))
+ {
+ return false;
+ }
}
for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
@@ -1194,18 +1200,31 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
//}else if( e==-1 ){
// d_ground_eval[0] = p->d_false;
//}
- //modified
- for( unsigned i=0; i<2; i++ ){
- if( p->getTermDatabase()->isEntailed( d_n, i==0 ) ){
+ //modified
+ TermDb* tdb = p->getTermDatabase();
+ QuantifiersEngine* qe = p->getQuantifiersEngine();
+ for( unsigned i=0; i<2; i++ ){
+ if (tdb->isEntailed(d_n, i == 0))
+ {
d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
}
+ if (qe->inConflict())
+ {
+ return false;
+ }
}
}else if( d_type==typ_eq ){
- for (unsigned i = 0; i < d_n.getNumChildren(); i++)
+ TermDb* tdb = p->getTermDatabase();
+ QuantifiersEngine* qe = p->getQuantifiersEngine();
+ for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
{
if (!expr::hasBoundVar(d_n[i]))
{
- TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]);
+ TNode t = tdb->getEntailedTerm(d_n[i]);
+ if (qe->inConflict())
+ {
+ return false;
+ }
if (t.isNull())
{
d_ground_eval[i] = d_n[i];
@@ -1220,6 +1239,7 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
d_qni_bound_cons.clear();
d_qni_bound_cons_var.clear();
d_qni_bound.clear();
+ return true;
}
void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
@@ -2038,9 +2058,10 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
}
}
Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
- if( d_conflict || d_quantEngine->inConflict() ){
- break;
- }
+ }
+ if (d_conflict || d_quantEngine->inConflict())
+ {
+ break;
}
}
}
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index d76495b52..0469e958b 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -90,7 +90,13 @@ public:
std::vector< MatchGen > d_children;
short d_type;
bool d_type_not;
- void reset_round( QuantConflictFind * p );
+ /** reset round
+ *
+ * Called once at the beginning of each full/last-call effort, prior to
+ * processing this match generator. This method returns false if the reset
+ * failed, e.g. if a conflict was encountered during term indexing.
+ */
+ bool reset_round(QuantConflictFind* p);
void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );
bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
bool isValid() { return d_type!=typ_invalid; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback