summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp1
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp5
-rw-r--r--src/theory/datatypes/theory_datatypes.h2
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp39
-rw-r--r--src/theory/quantifiers/conjecture_generator.h9
-rw-r--r--src/theory/quantifiers/options2
-rwxr-xr-xsrc/theory/quantifiers/quant_conflict_find.cpp12
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp31
-rw-r--r--test/regress/regress0/bug567.smt22
9 files changed, 66 insertions, 37 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 98cc7813d..cd3a7943e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1300,6 +1300,7 @@ void SmtEngine::setDefaults() {
}
}
if( options::dtStcInduction() ){
+ //leads to unfairness FIXME
if( !options::dtForceAssignment.wasSetByUser() ){
options::dtForceAssignment.set( true );
}
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f74384d59..8e90f5056 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -62,6 +62,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
d_equalityEngine.addFunctionKind(kind::APPLY_UF);
d_true = NodeManager::currentNM()->mkConst( true );
+ d_dtfCounter = 0;
}
TheoryDatatypes::~TheoryDatatypes() {
@@ -190,8 +191,8 @@ void TheoryDatatypes::check(Effort e) {
}
}
}
-
- if( !needSplit && options::dtForceAssignment() ){
+ //d_dtfCounter++;
+ if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
//for the sake of termination, we must choose the constructor of a ground term
//NEED GUARENTEE: groundTerm should not contain any subterms of the same type
// TODO: this is probably not good enough, actually need fair enumeration strategy
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 132077e29..3592dbe30 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -174,6 +174,8 @@ private:
context::CDList<TNode> d_consTerms;
/** All the selector terms that the theory has seen */
context::CDList<TNode> d_selTerms;
+ /** counter for forcing assignments (ensures fairness) */
+ unsigned d_dtfCounter;
private:
/** assert fact */
void assertFact( Node fact, Node exp );
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 17489b6ba..c775bb558 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -710,12 +710,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
Trace("sg-rel-term") << std::endl;
for( unsigned r=0; r<2; r++ ){
- Trace("sg-gen-tg-eqc") << "...from equivalence classes (" << r << ") : ";
+ Trace("sg-rel-term-debug") << "...from equivalence classes (" << r << ") : ";
int index = d_ccand_eqc[r].size()-1;
for( unsigned j=0; j<d_ccand_eqc[r][index].size(); j++ ){
- Trace("sg-gen-tg-eqc") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";
+ Trace("sg-rel-term-debug") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";
}
- Trace("sg-gen-tg-eqc") << std::endl;
+ Trace("sg-rel-term-debug") << std::endl;
}
TypeNode tnn = nn.getType();
Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;
@@ -766,7 +766,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
int index = d_ccand_eqc[1].size()-1;
for( unsigned j=0; j<d_ccand_eqc[1][index].size(); j++ ){
TNode r = d_ccand_eqc[1][index][j];
- Trace("sg-gen-tg-eqc") << " Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;
+ Trace("sg-rel-term-debug") << " Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;
std::map< TypeNode, std::map< unsigned, TNode > > subs;
std::map< TNode, bool > rev_subs;
//only get ground terms
@@ -779,17 +779,17 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
unsigned tindex = typ_to_subs_index[it->first];
for( std::map< unsigned, TNode >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
if( !firstTime ){
- Trace("sg-gen-tg-eqc") << ", ";
+ Trace("sg-rel-term-debug") << ", ";
}else{
firstTime = false;
- Trace("sg-gen-tg-eqc") << " ";
+ Trace("sg-rel-term-debug") << " ";
}
- Trace("sg-gen-tg-eqc") << it->first << ":x" << it2->first << " -> " << it2->second;
+ Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;
Assert( tindex+it2->first<gsubs_terms.size() );
gsubs_terms[tindex+it2->first] = it2->second;
}
}
- Trace("sg-gen-tg-eqc") << std::endl;
+ Trace("sg-rel-term-debug") << std::endl;
d_rel_pattern_subs_index[nn].addSubstitution( r, gsubs_vars, gsubs_terms );
}
}
@@ -1000,9 +1000,10 @@ bool ConjectureGenerator::considerCurrentTerm() {
std::map< TNode, bool > rev_subs;
unsigned mode;
if( r==0 ){
- mode = optReqDistinctVarPatterns() ? 1 : 0;
+ mode = optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;
+ mode = mode | (1 << 2 );
}else{
- mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? 2 : 0;
+ mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? ( 1 << 1 ) : 0;
}
d_tg_alloc[0].resetMatching( this, d_ccand_eqc[r][i-1][j], mode );
if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){
@@ -1539,9 +1540,9 @@ void TermGenerator::resetMatching( ConjectureGenerator * s, TNode eqc, unsigned
d_match_children_end.clear();
d_match_mode = mode;
//if this term generalizes, it must generalize a non-ground term
- if( mode<2 && s->isGroundEqc( eqc ) && d_status==5 ){
- d_match_status = -1;
- }
+ //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){
+ // d_match_status = -1;
+ //}
}
bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {
@@ -1572,13 +1573,19 @@ bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map<
//a variable
if( d_match_status==0 ){
d_match_status++;
- if( d_match_mode>=2 ){
+ if( (d_match_mode & ( 1 << 1 ))!=0 ){
//only ground terms
if( !s->isGroundEqc( eqc ) ){
return false;
}
+ }else if( (d_match_mode & ( 1 << 2 ))!=0 ){
+ //only non-ground terms
+ //if( s->isGroundEqc( eqc ) ){
+ // return false;
+ //}
}
- if( d_match_mode%2==1 ){
+ //store the match : restricted if match_mode.0 = 1
+ if( (d_match_mode & ( 1 << 0 ))!=0 ){
std::map< TNode, bool >::iterator it = rev_subs.find( eqc );
if( it==rev_subs.end() ){
rev_subs[eqc] = true;
@@ -1592,7 +1599,7 @@ bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map<
}else{
//clean up
subs[d_typ].erase( d_status_num );
- if( d_match_mode%2==1 ){
+ if( (d_match_mode & ( 1 << 0 ))!=0 ){
rev_subs.erase( eqc );
}
return false;
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 94a13829c..93cda7311 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -85,10 +85,10 @@ public:
//match status
int d_match_status;
int d_match_status_child_num;
- //match mode
- //1 : different variables must have different matches
- //2 : variables must map to ground terms
- //3 : both 1 and 2
+ //match mode bits
+ //0 : different variables must have different matches
+ //1 : variables must map to ground terms
+ //2 : variables must map to non-ground terms
unsigned d_match_mode;
//children
std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;
@@ -312,7 +312,6 @@ public: //for generalization
return isGeneralization( patg, pat, subs );
}
bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );
-
public: //for property enumeration
//process this candidate conjecture
void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index aa68aefcc..d30e5de4a 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -26,7 +26,7 @@ option prenexQuant /--disable-prenex-quant bool :default true
# forall y. P( c, y )
option varElimQuant /--disable-var-elim-quant bool :default true
disable simple variable elimination for quantified formulas
-option dtVarExpandQuant --dt-var-exp-quant bool :default false
+option dtVarExpandQuant --dt-var-exp-quant bool :default true
expand datatype variables bound to one constructor in quantifiers
option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 504c3dcff..ee4464f87 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2010,9 +2010,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
//try to make a matches making the body false
Trace("qcf-check-debug") << "Get next match..." << std::endl;
while( qi->d_mg->getNextMatch( this, qi ) ){
- Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
- qi->debugPrintMatch("qcf-check");
- Trace("qcf-check") << std::endl;
+ Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
+ qi->debugPrintMatch("qcf-inst");
+ Trace("qcf-inst") << std::endl;
std::vector< int > assigned;
if( !qi->isMatchSpurious( this ) ){
if( qi->completeMatch( this, assigned ) ){
@@ -2042,7 +2042,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
++(d_statistics.d_prop_inst);
}
}else{
- Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
+ Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
//Assert( false );
}
}
@@ -2050,10 +2050,10 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
qi->revertMatch( assigned );
d_tempCache.clear();
}else{
- Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
+ Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
}
}else{
- Trace("qcf-check") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
+ Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
}
}
if( d_conflict ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 624856671..754bfacb1 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -368,7 +368,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
//Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
if( it->first.getKind()==EQUAL ){
- if( it->second ){
+ if( it->second && options::varElimQuant() ){
for( int i=0; i<2; i++ ){
int j = i==0 ? 1 : 0;
std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
@@ -388,14 +388,33 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
}
}
}
- /*
- else if( options::dtVarExpandQuant() && it->first.getKind()==APPLY_TESTER && it->first[0].getKind()==BOUND_VARIABLE ){
- if( it->second ){
+ else if( it->first.getKind()==APPLY_TESTER ){
+ if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){
Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl;
std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
+ if( ita!=args.end() ){
+ vars.push_back( it->first[0] );
+ Expr testerExpr = it->first.getOperator().toExpr();
+ int index = Datatype::indexOf( testerExpr );
+ const Datatype& dt = Datatype::datatypeOf(testerExpr);
+ const DatatypeConstructor& c = dt[index];
+ std::vector< Node > newChildren;
+ newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
+ std::vector< Node > newVars;
+ for( unsigned j=0; j<c.getNumArgs(); j++ ){
+ TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
+ tn = tn[1];
+ Node v = NodeManager::currentNM()->mkBoundVar( tn );
+ newChildren.push_back( v );
+ newVars.push_back( v );
+ }
+ subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
+ Trace("dt-var-expand") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
+ args.erase( ita );
+ args.insert( args.end(), newVars.begin(), newVars.end() );
+ }
}
}
- */
}
if( !vars.empty() ){
Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl;
@@ -933,7 +952,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
}else if( computeOption==COMPUTE_PRENEX ){
return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
}else if( computeOption==COMPUTE_VAR_ELIMINATION ){
- return options::varElimQuant();
+ return options::varElimQuant() || options::dtVarExpandQuant();
}else if( computeOption==COMPUTE_CNF ){
return false;//return options::cnfQuant() ; FIXME
}else if( computeOption==COMPUTE_SPLIT ){
diff --git a/test/regress/regress0/bug567.smt2 b/test/regress/regress0/bug567.smt2
index 109940090..37403d8a3 100644
--- a/test/regress/regress0/bug567.smt2
+++ b/test/regress/regress0/bug567.smt2
@@ -1,7 +1,7 @@
(set-logic ALL_SUPPORTED)
; COMMAND-LINE: --incremental
; EXPECT: unknown
-; EXPECT: unknown
+; EXPECT: unsat
; EXPECT: unknown
(declare-datatypes () ((OptInt0 (Some (value0 Int)) (None))))
(declare-datatypes () ((List0 (Cons (head0 Int) (tail0 List0)) (Nil))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback