summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options2
-rw-r--r--src/smt/smt_engine.cpp4
-rw-r--r--src/theory/quantifiers/bounded_integers.cpp298
-rw-r--r--src/theory/quantifiers/bounded_integers.h30
-rw-r--r--src/theory/quantifiers/full_model_check.cpp67
-rw-r--r--src/theory/quantifiers/quant_split.cpp6
-rw-r--r--src/theory/quantifiers_engine.cpp17
-rw-r--r--src/theory/quantifiers_engine.h2
-rw-r--r--src/theory/rep_set.cpp166
-rw-r--r--src/theory/rep_set.h21
-rw-r--r--test/regress/regress0/fmf/Makefile.am7
-rw-r--r--test/regress/regress0/fmf/bounded_sets.smt218
-rw-r--r--test/regress/regress0/fmf/fmf-bound-2dim.smt215
-rw-r--r--test/regress/regress0/fmf/fmf-strange-bounds-2.smt224
-rw-r--r--test/regress/regress0/fmf/fmf-strange-bounds.smt235
-rw-r--r--test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc52
16 files changed, 503 insertions, 261 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index f6b6e2177..856de103e 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -325,7 +325,7 @@ option macrosQuant --macros-quant bool :read-write :default false
perform quantifiers macro expansion
option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler stringToMacrosQuantMode
mode for quantifiers macro expansion
-option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode
+option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode
mode for dynamic quantifiers splitting
option quantAntiSkolem --quant-anti-skolem bool :read-write :default false
perform anti-skolemization for quantified formulas
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 30da29813..019cae9a1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1774,6 +1774,10 @@ void SmtEngine::setDefaults() {
//now, have determined whether finite model find is on/off
//apply finite model finding options
if( options::finiteModelFind() ){
+ //apply conservative quantifiers splitting
+ if( !options::quantDynamicSplit.wasSetByUser() ){
+ options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT );
+ }
if( !options::eMatching.wasSetByUser() ){
options::eMatching.set( options::fmfInstEngine() );
}
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index dc0019383..1112c2ef2 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -171,31 +171,110 @@ bool BoundedIntegers::isBound( Node f, Node v ) {
return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
}
-bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
- if( b.getKind()==BOUND_VARIABLE ){
- if( !isBound( f, b ) ){
- return true;
- }
- }else{
- for( unsigned i=0; i<b.getNumChildren(); i++ ){
- if( hasNonBoundVar( f, b[i] ) ){
+bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) {
+ if( visited.find( b )==visited.end() ){
+ visited[b] = true;
+ if( b.getKind()==BOUND_VARIABLE ){
+ if( !isBound( f, b ) ){
return true;
}
+ }else{
+ for( unsigned i=0; i<b.getNumChildren(); i++ ){
+ if( hasNonBoundVar( f, b[i], visited ) ){
+ return true;
+ }
+ }
}
}
return false;
}
+bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
+ std::map< Node, bool > visited;
+ return hasNonBoundVar( f, b, visited );
+}
-void BoundedIntegers::processLiteral( Node q, Node lit, bool pol,
- std::map< Node, unsigned >& bound_lit_type_map,
- std::map< int, std::map< Node, Node > >& bound_lit_map,
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
- std::map< int, std::map< Node, Node > >& bound_int_range_term ) {
- if( lit.getKind()==GEQ ){
- if( lit[0].getType().isInteger() ){
+bool BoundedIntegers::processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ) {
+ if( n.getKind()==EQUAL ){
+ for( unsigned i=0; i<2; i++ ){
+ Node t = n[i];
+ if( !hasNonBoundVar( q, n[1-i] ) ){
+ if( t==v ){
+ v_cases.push_back( n[1-i] );
+ return true;
+ }else if( v.isNull() && t.getKind()==BOUND_VARIABLE ){
+ v = t;
+ v_cases.push_back( n[1-i] );
+ return true;
+ }
+ }
+ }
+ }
+ return false;
+}
+
+void BoundedIntegers::process( Node q, Node n, bool pol,
+ std::map< Node, unsigned >& bound_lit_type_map,
+ std::map< int, std::map< Node, Node > >& bound_lit_map,
+ std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
+ std::map< int, std::map< Node, Node > >& bound_int_range_term,
+ std::map< Node, std::vector< Node > >& bound_fixed_set ){
+ if( n.getKind()==OR || n.getKind()==AND ){
+ if( (n.getKind()==OR)==pol ){
+ for( unsigned i=0; i<n.getNumChildren(); i++) {
+ process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
+ }
+ }else{
+ //if we are ( x != t1 ^ ...^ x != tn ), then x can be bound to { t1...tn }
+ Node conj = n;
+ if( !pol ){
+ conj = TermDb::simpleNegate( conj );
+ }
+ Trace("bound-int-debug") << "Process possible finite disequality conjunction : " << conj << std::endl;
+ Assert( conj.getKind()==AND );
+ Node v;
+ std::vector< Node > v_cases;
+ bool success = true;
+ for( unsigned i=0; i<conj.getNumChildren(); i++ ){
+ if( conj[i].getKind()==NOT && processEqDisjunct( q, conj[i][0], v, v_cases ) ){
+ //continue
+ }else{
+ Trace("bound-int-debug") << "...failed due to " << conj[i] << std::endl;
+ success = false;
+ break;
+ }
+ }
+ if( success && !isBound( q, v ) ){
+ Trace("bound-int-debug") << "Success with variable " << v << std::endl;
+ bound_lit_type_map[v] = BOUND_FIXED_SET;
+ bound_lit_map[0][v] = n;
+ bound_lit_pol_map[0][v] = pol;
+ bound_fixed_set[v].clear();
+ bound_fixed_set[v].insert( bound_fixed_set[v].end(), v_cases.begin(), v_cases.end() );
+ }
+ }
+ }else if( n.getKind()==EQUAL ){
+ if( !pol ){
+ // non-applied DER on x != t, x can be bound to { t }
+ Node v;
+ std::vector< Node > v_cases;
+ if( processEqDisjunct( q, n, v, v_cases ) ){
+ if( !isBound( q, v ) ){
+ bound_lit_type_map[v] = BOUND_FIXED_SET;
+ bound_lit_map[0][v] = n;
+ bound_lit_pol_map[0][v] = pol;
+ Assert( v_cases.size()==1 );
+ bound_fixed_set[v].clear();
+ bound_fixed_set[v].push_back( v_cases[0] );
+ }
+ }
+ }
+ }else if( n.getKind()==NOT ){
+ process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
+ }else if( n.getKind()==GEQ ){
+ if( n[0].getType().isInteger() ){
std::map< Node, Node > msum;
- if( QuantArith::getMonomialSumLit( lit, msum ) ){
- Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
+ if( QuantArith::getMonomialSumLit( n, msum ) ){
+ Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is monomial sum : " << std::endl;
QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" );
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( q, it->first ) ){
@@ -221,7 +300,7 @@ void BoundedIntegers::processLiteral( Node q, Node lit, bool pol,
int loru = n1==it->first ? 0 : 1;
bound_lit_type_map[it->first] = BOUND_INT_RANGE;
bound_int_range_term[loru][it->first] = t;
- bound_lit_map[loru][it->first] = lit;
+ bound_lit_map[loru][it->first] = n;
bound_lit_pol_map[loru][it->first] = pol;
}else{
Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
@@ -231,32 +310,15 @@ void BoundedIntegers::processLiteral( Node q, Node lit, bool pol,
}
}
}
- }else if( lit.getKind()==MEMBER ){
- //TODO: enable this when sets models are fixed
- if( !pol && lit[0].getKind()==BOUND_VARIABLE && !isBound( q, lit[0] ) && !lit[1].hasBoundVar() ){
- Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is membership." << std::endl;
- bound_lit_type_map[lit[0]] = BOUND_SET_MEMBER;
- bound_lit_map[0][lit[0]] = lit;
- bound_lit_pol_map[0][lit[0]] = pol;
+ }else if( n.getKind()==MEMBER ){
+ if( !pol && n[0].getKind()==BOUND_VARIABLE && !isBound( q, n[0] ) && !hasNonBoundVar( q, n[1] ) ){
+ Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
+ bound_lit_type_map[n[0]] = BOUND_SET_MEMBER;
+ bound_lit_map[0][n[0]] = n;
+ bound_lit_pol_map[0][n[0]] = pol;
}
- }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
- Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
- }
-}
-
-void BoundedIntegers::process( Node q, Node n, bool pol,
- std::map< Node, unsigned >& bound_lit_type_map,
- std::map< int, std::map< Node, Node > >& bound_lit_map,
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
- std::map< int, std::map< Node, Node > >& bound_int_range_term ){
- if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){
- for( unsigned i=0; i<n.getNumChildren(); i++) {
- process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
- }
- }else if( n.getKind()==NOT ){
- process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
- }else {
- processLiteral( q, n, pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
+ }else{
+ Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT );
}
}
@@ -294,8 +356,9 @@ void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl;
}
-void BoundedIntegers::registerQuantifier( Node f ) {
- Trace("bound-int") << "Register quantifier " << f << std::endl;
+void BoundedIntegers::preRegisterQuantifier( Node f ) {
+ //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
+ Trace("bound-int") << "preRegister quantifier " << f << std::endl;
bool success;
do{
@@ -303,8 +366,9 @@ void BoundedIntegers::registerQuantifier( Node f ) {
std::map< int, std::map< Node, Node > > bound_lit_map;
std::map< int, std::map< Node, bool > > bound_lit_pol_map;
std::map< int, std::map< Node, Node > > bound_int_range_term;
+ std::map< Node, std::vector< Node > > bound_fixed_set;
success = false;
- process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
+ process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set );
//for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
for( std::map< Node, unsigned >::iterator it = bound_lit_type_map.begin(); it != bound_lit_type_map.end(); ++it ){
Node v = it->first;
@@ -315,7 +379,6 @@ void BoundedIntegers::registerQuantifier( Node f ) {
if( bound_lit_map[0].find( v )!=bound_lit_map[0].end() && bound_lit_map[1].find( v )!=bound_lit_map[1].end() ){
setBoundedVar( f, v, BOUND_INT_RANGE );
setBoundVar = true;
- success = true;
for( unsigned b=0; b<2; b++ ){
//set the bounds
Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() );
@@ -330,9 +393,23 @@ void BoundedIntegers::registerQuantifier( Node f ) {
setBoundVar = true;
d_setm_range[f][v] = bound_lit_map[0][v][1];
d_setm_range_lit[f][v] = bound_lit_map[0][v];
+ d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl;
+ }else if( it->second==BOUND_FIXED_SET ){
+ setBoundedVar( f, v, BOUND_FIXED_SET );
+ setBoundVar = true;
+ for( unsigned i=0; i<bound_fixed_set[v].size(); i++ ){
+ Node t = bound_fixed_set[v][i];
+ if( t.hasBoundVar() ){
+ d_fixed_set_ngr_range[f][v].push_back( t );
+ }else{
+ d_fixed_set_gr_range[f][v].push_back( t );
+ }
+ }
+ Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[0][v] << std::endl;
}
if( setBoundVar ){
+ success = true;
//set Attributes on literals
for( unsigned b=0; b<2; b++ ){
if( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ){
@@ -346,6 +423,19 @@ void BoundedIntegers::registerQuantifier( Node f ) {
}
}
}
+ if( !success ){
+ //resort to setting a finite bound on a variable
+ for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+ if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
+ TypeNode tn = f[0][i].getType();
+ if( tn.isSort() || getTermDatabase()->mayComplete( tn ) ){
+ success = true;
+ setBoundedVar( f, f[0][i], BOUND_FINITE );
+ break;
+ }
+ }
+ }
+ }
}while( success );
Trace("bound-int") << "Bounds are : " << std::endl;
@@ -361,12 +451,9 @@ void BoundedIntegers::registerQuantifier( Node f ) {
bool bound_success = true;
for( unsigned i=0; i<f[0].getNumChildren(); i++) {
if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
- TypeNode tn = f[0][i].getType();
- if( !tn.isSort() && !getTermDatabase()->mayComplete( tn ) ){
- Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl;
- bound_success = false;
- break;
- }
+ Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl;
+ bound_success = false;
+ break;
}
}
@@ -375,17 +462,13 @@ void BoundedIntegers::registerQuantifier( Node f ) {
for( unsigned i=0; i<d_set[f].size(); i++) {
Node v = d_set[f][i];
if( d_bound_type[f][v]==BOUND_INT_RANGE || d_bound_type[f][v]==BOUND_SET_MEMBER ){
- Node r;
- if( d_bound_type[f][v]==BOUND_INT_RANGE ){
- r = d_range[f][v];
- }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
- r = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
- }
+ Node r = d_range[f][v];
+ Assert( !r.isNull() );
bool isProxy = false;
if( r.hasBoundVar() ){
//introduce a new bound
Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" );
- d_nground_range[f][v] = d_range[f][v];
+ d_nground_range[f][v] = r;
d_range[f][v] = new_range;
r = new_range;
isProxy = true;
@@ -403,6 +486,10 @@ void BoundedIntegers::registerQuantifier( Node f ) {
}
}
+void BoundedIntegers::registerQuantifier( Node q ) {
+
+}
+
void BoundedIntegers::assertNode( Node n ) {
Trace("bound-int-assert") << "Assert " << n << std::endl;
Node nlit = n.getKind()==NOT ? n[0] : n;
@@ -490,6 +577,8 @@ bool BoundedIntegers::isGroundRange( Node q, Node v ) {
return !getLowerBound(q,v).hasBoundVar() && !getUpperBound(q,v).hasBoundVar();
}else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){
return !d_setm_range[q][v].hasBoundVar();
+ }else if( d_bound_type[q][v]==BOUND_FIXED_SET ){
+ return !d_fixed_set_ngr_range[q][v].empty();
}
}
return false;
@@ -592,21 +681,23 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
Assert( q[0][v]==d_set[q][i] );
Node t = rsi->getCurrentTerm( v );
Trace("bound-int-rsi") << "term : " << t << std::endl;
+ if( rsi->d_rep_set->d_values_to_terms.find( t )!=rsi->d_rep_set->d_values_to_terms.end() ){
+ t = rsi->d_rep_set->d_values_to_terms[t];
+ Trace("bound-int-rsi") << "term (post-rep) : " << t << std::endl;
+ }
vars.push_back( d_set[q][i] );
subs.push_back( t );
}
//check if it has been instantiated
if( !vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs) ){
- if( d_bound_type[q][v]==BOUND_INT_RANGE ){
+ if( d_bound_type[q][v]==BOUND_INT_RANGE || d_bound_type[q][v]==BOUND_SET_MEMBER ){
//must add the lemma
Node nn = d_nground_range[q][v];
nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
d_quantEngine->getOutputChannel().lemma(lem, false, true);
- }else{
- //TODO : sets
}
return false;
}else{
@@ -614,3 +705,84 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
}
}
+bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) {
+ if( initial || !isGroundRange( q, v ) ){
+ elements.clear();
+ unsigned bvt = getBoundVarType( q, v );
+ if( bvt==BOUND_INT_RANGE ){
+ Node l, u;
+ getBoundValues( q, v, rsi, l, u );
+ if( l.isNull() || u.isNull() ){
+ //failed, abort the iterator
+ return false;
+ }else{
+ Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl;
+ Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
+ Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
+ Node tl = l;
+ Node tu = u;
+ getBounds( q, v, rsi, tl, tu );
+ Assert( !tl.isNull() && !tu.isNull() );
+ if( ra==d_quantEngine->getTermDatabase()->d_true ){
+ long rr = range.getConst<Rational>().getNumerator().getLong()+1;
+ Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
+ for( unsigned k=0; k<rr; k++ ){
+ Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) );
+ t = Rewriter::rewrite( t );
+ elements.push_back( t );
+ }
+ return true;
+ }else{
+ Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << v << "." << std::endl;
+ return false;
+ }
+ }
+ }else if( bvt==BOUND_SET_MEMBER ){
+ Node srv = getSetRangeValue( q, v, rsi );
+ if( srv.isNull() ){
+ return false;
+ }else{
+ Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
+ if( srv.getKind()!=EMPTYSET ){
+ while( srv.getKind()==UNION ){
+ Assert( srv[1].getKind()==kind::SINGLETON );
+ elements.push_back( srv[1][0] );
+ srv = srv[0];
+ }
+ Assert( srv.getKind()==kind::SINGLETON );
+ elements.push_back( srv[0] );
+ }
+ return true;
+ }
+ }else if( bvt==BOUND_FIXED_SET ){
+ std::map< Node, std::vector< Node > >::iterator it = d_fixed_set_gr_range[q].find( v );
+ if( it!=d_fixed_set_gr_range[q].end() ){
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ elements.push_back( it->second[i] );
+ }
+ }
+ it = d_fixed_set_ngr_range[q].find( v );
+ if( it!=d_fixed_set_ngr_range[q].end() ){
+ std::vector< Node > vars;
+ std::vector< Node > subs;
+ if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ Node t = it->second[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+ elements.push_back( t );
+ }
+ return true;
+ }else{
+ return false;
+ }
+ }else{
+ return true;
+ }
+ }else{
+ return false;
+ }
+ }else{
+ //no change required
+ return true;
+ }
+}
+
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 0dfd7eafd..5c5a52855 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -44,34 +44,36 @@ public:
BOUND_FINITE,
BOUND_INT_RANGE,
BOUND_SET_MEMBER,
+ BOUND_FIXED_SET,
BOUND_NONE
};
private:
//for determining bounds
bool isBound( Node f, Node v );
+ bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited );
bool hasNonBoundVar( Node f, Node b );
//bound type
std::map< Node, std::map< Node, unsigned > > d_bound_type;
std::map< Node, std::vector< Node > > d_set;
std::map< Node, std::map< Node, int > > d_set_nums;
- //integer lower/upper bounds
- std::map< Node, std::map< Node, Node > > d_bounds[2];
std::map< Node, std::map< Node, Node > > d_range;
std::map< Node, std::map< Node, Node > > d_nground_range;
+ //integer lower/upper bounds
+ std::map< Node, std::map< Node, Node > > d_bounds[2];
//set membership range
std::map< Node, std::map< Node, Node > > d_setm_range;
std::map< Node, std::map< Node, Node > > d_setm_range_lit;
+ //fixed finite set range
+ std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_gr_range;
+ std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_ngr_range;
void hasFreeVar( Node f, Node n );
- void process( Node f, Node n, bool pol,
+ void process( Node q, Node n, bool pol,
std::map< Node, unsigned >& bound_lit_type_map,
std::map< int, std::map< Node, Node > >& bound_lit_map,
std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
- std::map< int, std::map< Node, Node > >& bound_int_range_term );
- void processLiteral( Node f, Node lit, bool pol,
- std::map< Node, unsigned >& bound_lit_type_map,
- std::map< int, std::map< Node, Node > >& bound_lit_map,
- std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
- std::map< int, std::map< Node, Node > >& bound_int_range_term );
+ std::map< int, std::map< Node, Node > >& bound_int_range_term,
+ std::map< Node, std::vector< Node > >& bound_fixed_set );
+ bool processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases );
std::vector< Node > d_bound_quants;
private:
class RangeModel {
@@ -144,13 +146,15 @@ public:
void presolve();
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
- void registerQuantifier( Node f );
+ void registerQuantifier( Node q );
+ void preRegisterQuantifier( Node q );
void assertNode( Node n );
Node getNextDecisionRequest( unsigned& priority );
bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
unsigned getBoundVarType( Node q, Node v );
unsigned getNumBoundVars( Node q ) { return d_set[q].size(); }
Node getBoundVar( Node q, int i ) { return d_set[q][i]; }
+private:
//for integer range
Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; }
Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; }
@@ -160,11 +164,13 @@ public:
//for set range
Node getSetRange( Node q, Node v, RepSetIterator * rsi );
Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi );
+
+ bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
+public:
+ bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements );
/** Identify this module */
std::string identify() const { return "BoundedIntegers"; }
-private:
- bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
};
}
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 6b756428b..7e528fef3 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -737,56 +737,37 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
}
}
+class RepBoundFmcEntry : public RepBoundExt {
+public:
+ Node d_entry;
+ FirstOrderModelFmc * d_fm;
+ bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) {
+ if( d_fm->isInterval(d_entry[i]) ){
+ //explicitly add the interval TODO?
+ }else if( d_fm->isStar(d_entry[i]) ){
+ //add the full range
+ return false;
+ }else{
+ //only need to consider the single point
+ elements.push_back( d_entry[i] );
+ return true;
+ }
+ return false;
+ }
+};
+
bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
RepSetIterator riter( d_qe, &(fm->d_rep_set) );
Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " ";
debugPrintCond("fmc-exh", c, true);
Trace("fmc-exh")<< std::endl;
- Trace("fmc-exh-debug") << "Set interval domains..." << std::endl;
- //set the bounds on the iterator based on intervals
- for( unsigned i=0; i<c.getNumChildren(); i++ ){
- if( c[i].getType().isInteger() ){
- if( fm->isInterval(c[i]) ){
- Trace("fmc-exh-debug") << "...set " << i << " based on interval." << std::endl;
- for( unsigned b=0; b<2; b++ ){
- if( !fm->isStar(c[i][b]) ){
- riter.d_bounds[b][i] = c[i][b];
- }
- }
- }else if( !fm->isStar(c[i]) ){
- Trace("fmc-exh-debug") << "...set " << i << " based on point." << std::endl;
- riter.d_bounds[0][i] = c[i];
- riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );
- }
- }
- }
+ RepBoundFmcEntry rbfe;
+ rbfe.d_entry = c;
+ rbfe.d_fm = fm;
Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
//initialize
- if( riter.setQuantifier( f ) ){
+ if( riter.setQuantifier( f, &rbfe ) ){
Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
- //set the domains based on the entry
- for (unsigned i=0; i<c.getNumChildren(); i++) {
- if( riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS || riter.d_enum_type[i]==RepSetIterator::ENUM_SET_MEMBERS ){
- TypeNode tn = c[i].getType();
- if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
- if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){
- //add the full range
- }else{
- if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
- riter.d_domain[i].clear();
- riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
- riter.d_enum_type[i] = RepSetIterator::ENUM_DOMAIN_ELEMENTS;
- }else{
- Trace("fmc-exh") << "---- Does not have rep : " << c[i] << " for type " << tn << std::endl;
- return false;
- }
- }
- }else{
- Trace("fmc-exh") << "---- Does not have type : " << tn << std::endl;
- return false;
- }
- }
- }
int addedLemmas = 0;
//now do full iteration
while( !riter.isFinished() ){
@@ -829,7 +810,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
int index = riter.increment();
Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
if( !riter.isFinished() ){
- if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_INT_RANGE) {
+ if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_BOUND_INT ) {
Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
riter.increment2( index-1 );
}
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index c88430dbf..24d26e72f 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -50,7 +50,11 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0;
}else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
- score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1;
+ //only split if goes from being unhandled -> handled by finite instantiation
+ // an example is datatypes with uninterpreted sort fields, which are "interpreted finite" but not "finite"
+ if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){
+ score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1;
+ }
}
Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl;
if( score>max_score ){
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a3b6293fb..2d79826a6 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -251,8 +251,7 @@ void QuantifiersEngine::finishInit(){
d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
d_modules.push_back( d_lte_part_inst );
}
- if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) ||
- options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
+ if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){
d_qsplit = new quantifiers::QuantDSplit( this, c );
d_modules.push_back( d_qsplit );
}
@@ -328,6 +327,20 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
return mo==m || mo==NULL;
}
+bool QuantifiersEngine::isFiniteBound( Node q, Node v ) {
+ if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){
+ return true;
+ }else{
+ TypeNode tn = v.getType();
+ if( tn.isSort() && options::finiteModelFind() ){
+ return true;
+ }else if( getTermDatabase()->mayComplete( tn ) ){
+ return true;
+ }
+ }
+ return false;
+}
+
void QuantifiersEngine::presolve() {
Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
for( unsigned i=0; i<d_modules.size(); i++ ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 43beec6e3..83076c51a 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -271,6 +271,8 @@ public:
void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
/** considers */
bool hasOwnership( Node q, QuantifiersModule * m = NULL );
+ /** is finite bound */
+ bool isFiniteBound( Node q, Node v );
public:
/** initialize */
void finishInit();
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index a2797dd8d..c308b9c67 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -139,14 +139,10 @@ RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe),
int RepSetIterator::domainSize( int i ) {
Assert(i>=0);
int v = d_var_order[i];
- if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){
- return d_domain[v].size();
- }else{
- return d_domain[v][0];
- }
+ return d_domain_elements[v].size();
}
-bool RepSetIterator::setQuantifier( Node f ){
+bool RepSetIterator::setQuantifier( Node f, RepBoundExt* rext ){
Trace("rsi") << "Make rsi for " << f << std::endl;
Assert( d_types.empty() );
//store indicies
@@ -154,10 +150,10 @@ bool RepSetIterator::setQuantifier( Node f ){
d_types.push_back( f[0][i].getType() );
}
d_owner = f;
- return initialize();
+ return initialize( rext );
}
-bool RepSetIterator::setFunctionDomain( Node op ){
+bool RepSetIterator::setFunctionDomain( Node op, RepBoundExt* rext ){
Trace("rsi") << "Make rsi for " << op << std::endl;
Assert( d_types.empty() );
TypeNode tn = op.getType();
@@ -165,10 +161,10 @@ bool RepSetIterator::setFunctionDomain( Node op ){
d_types.push_back( tn[i] );
}
d_owner = op;
- return initialize();
+ return initialize( rext );
}
-bool RepSetIterator::initialize(){
+bool RepSetIterator::initialize( RepBoundExt* rext ){
Trace("rsi") << "Initialize rep set iterator..." << std::endl;
for( unsigned v=0; v<d_types.size(); v++ ){
d_index.push_back( 0 );
@@ -176,7 +172,8 @@ bool RepSetIterator::initialize(){
d_index_order.push_back( v );
d_var_order[v] = v;
//store default domain
- d_domain.push_back( RepDomain() );
+ //d_domain.push_back( RepDomain() );
+ d_domain_elements.push_back( std::vector< Node >() );
TypeNode tn = d_types[v];
Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
if( tn.isSort() ){
@@ -191,27 +188,27 @@ bool RepSetIterator::initialize(){
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
d_rep_set->add( tn, var );
}
- }else{
- bool inc = true;
- //check if it is bound by bounded integer module
- if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
+ }
+ bool inc = true;
+ //check if it is externally bound
+ if( rext && rext->setBound( d_owner, v, tn, d_domain_elements[v] ) ){
+ d_enum_type.push_back( ENUM_DEFAULT );
+ inc = false;
+ //builtin: check if it is bound by bounded integer module
+ }else if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
+ if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){
unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
- if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){
- Trace("rsi") << " variable is bounded integer." << std::endl;
- d_enum_type.push_back( ENUM_INT_RANGE );
- inc = false;
- }else if( bvt==quantifiers::BoundedIntegers::BOUND_SET_MEMBER ){
- Trace("rsi") << " variable is bounded by set membership." << std::endl;
- d_enum_type.push_back( ENUM_SET_MEMBERS );
+ if( bvt!=quantifiers::BoundedIntegers::BOUND_FINITE ){
+ d_enum_type.push_back( ENUM_BOUND_INT );
inc = false;
+ }else{
+ //will treat in default way
}
}
+ }
+ if( !tn.isSort() ){
if( inc ){
- //check if it is otherwise bound
- if( d_bounds[0].find( v )!=d_bounds[0].end() && d_bounds[1].find( v )!=d_bounds[1].end() ){
- Trace("rsi") << " variable is bounded." << std::endl;
- d_enum_type.push_back( ENUM_INT_RANGE );
- }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
+ if( d_qe->getTermDatabase()->mayComplete( tn ) ){
Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
d_rep_set->complete( tn );
//must have succeeded
@@ -223,12 +220,14 @@ bool RepSetIterator::initialize(){
}
}
}
+
//if we have yet to determine the type of enumeration
if( d_enum_type.size()<=v ){
- d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
if( d_rep_set->hasType( tn ) ){
+ d_enum_type.push_back( ENUM_DEFAULT );
for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
- d_domain[v].push_back( j );
+ //d_domain[v].push_back( j );
+ d_domain_elements[v].push_back( d_rep_set->d_type_reps[tn][j] );
}
}else{
Assert( d_incomplete );
@@ -285,92 +284,13 @@ int RepSetIterator::resetIndex( int i, bool initial ) {
d_index[i] = 0;
int v = d_var_order[i];
Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
- //determine the current range
- if( initial || ( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() &&
- d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) &&
- !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][v] ) ) ){
- Trace("bound-int-rsi") << "Getting range of " << d_owner[0][v] << std::endl;
- if( d_enum_type[v]==ENUM_INT_RANGE ){
- Node actual_l;
- Node l, u;
- if( d_qe->getBoundedIntegers() ){
- unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
- if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){
- d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][v], this, l, u );
- }
- }
- for( unsigned b=0; b<2; b++ ){
- if( d_bounds[b].find(v)!=d_bounds[b].end() ){
- Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][v] << std::endl;
- if( b==0 && (l.isNull() || d_bounds[b][v].getConst<Rational>() > l.getConst<Rational>()) ){
- if( !l.isNull() ){
- //bound was limited externally, record that the value lower bound is not equal to the term lower bound
- actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v], l );
- }
- l = d_bounds[b][v];
- }else if( b==1 && (u.isNull() || d_bounds[b][v].getConst<Rational>() <= u.getConst<Rational>()) ){
- u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v],
- NodeManager::currentNM()->mkConst( Rational(1) ) );
- u = Rewriter::rewrite( u );
- }
- }
- }
-
- if( l.isNull() || u.isNull() ){
- //failed, abort the iterator
- return -1;
- }else{
- Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][v] << " to " << l << "..." << u << std::endl;
- Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
- Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
- d_domain[v].clear();
- Node tl = l;
- Node tu = u;
- if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){
- d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][v], this, tl, tu );
- }
- d_lower_bounds[v] = tl;
- if( !actual_l.isNull() ){
- //if bound was limited externally, must consider the offset
- d_lower_bounds[v] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) );
- }
- if( ra==d_qe->getTermDatabase()->d_true ){
- long rr = range.getConst<Rational>().getNumerator().getLong()+1;
- Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
- d_domain[v].push_back( (int)rr );
- if( rr<=0 ){
- return 0;
- }
- }else{
- Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][v] << "." << std::endl;
- return -1;
- }
- }
- }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){
- Assert( d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] )==quantifiers::BoundedIntegers::BOUND_SET_MEMBER );
- Node srv = d_qe->getBoundedIntegers()->getSetRangeValue( d_owner, d_owner[0][v], this );
- if( srv.isNull() ){
- return -1;
- }
- Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
- d_domain[v].clear();
- d_setm_bounds[v].clear();
- if( srv.getKind()!=EMPTYSET ){
- while( srv.getKind()==UNION ){
- Assert( srv[1].getKind()==kind::SINGLETON );
- d_setm_bounds[v].push_back( srv[1][0] );
- srv = srv[0];
- }
- Assert( srv.getKind()==kind::SINGLETON );
- d_setm_bounds[v].push_back( srv[0] );
- d_domain[v].push_back( d_setm_bounds[v].size() );
- }else{
- d_domain[v].push_back( 0 );
- return 0;
- }
+ if( d_enum_type[v]==ENUM_BOUND_INT ){
+ Assert( d_owner.getKind()==FORALL );
+ if( !d_qe->getBoundedIntegers()->getBoundElements( this, initial, d_owner, d_owner[0][v], d_domain_elements[v] ) ){
+ return -1;
}
}
- return 1;
+ return d_domain_elements[v].empty() ? 0 : 1;
}
int RepSetIterator::increment2( int i ){
@@ -436,24 +356,12 @@ bool RepSetIterator::isFinished(){
}
Node RepSetIterator::getCurrentTerm( int v ){
- Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
int ii = d_index_order[v];
int curr = d_index[ii];
- if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){
- TypeNode tn = d_types[v];
- Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
- Assert( 0<=d_domain[v][curr] && d_domain[v][curr]<(int)d_rep_set->d_type_reps[tn].size() );
- return d_rep_set->d_type_reps[tn][d_domain[v][curr]];
- }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){
- Assert( 0<=curr && curr<(int)d_setm_bounds[v].size() );
- return d_setm_bounds[v][curr];
- }else{
- Trace("rsi-debug") << "Get, with offset : " << v << " " << d_lower_bounds[v] << " " << curr << std::endl;
- Assert( !d_lower_bounds[v].isNull() );
- Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[v], NodeManager::currentNM()->mkConst( Rational(curr) ) );
- t = Rewriter::rewrite( t );
- return t;
- }
+ Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
+ Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl;
+ Assert( 0<=curr && curr<(int)d_domain_elements[v].size() );
+ return d_domain_elements[v][curr];
}
void RepSetIterator::debugPrint( const char* c ){
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index a56fba39b..2a2110cfa 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -56,18 +56,23 @@ public:
//representative domain
typedef std::vector< int > RepDomain;
+
+class RepBoundExt {
+public:
+ virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0;
+};
+
/** this class iterates over a RepSet */
class RepSetIterator {
public:
enum {
- ENUM_DOMAIN_ELEMENTS,
- ENUM_INT_RANGE,
- ENUM_SET_MEMBERS,
+ ENUM_DEFAULT,
+ ENUM_BOUND_INT,
};
private:
QuantifiersEngine * d_qe;
//initialize function
- bool initialize();
+ bool initialize( RepBoundExt* rext = NULL );
//for int ranges
std::map< int, Node > d_lower_bounds;
//for set ranges
@@ -101,9 +106,9 @@ public:
RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
~RepSetIterator(){}
//set that this iterator will be iterating over instantiations for a quantifier
- bool setQuantifier( Node f );
+ bool setQuantifier( Node f, RepBoundExt* rext = NULL );
//set that this iterator will be iterating over the domain of a function
- bool setFunctionDomain( Node op );
+ bool setFunctionDomain( Node op, RepBoundExt* rext = NULL );
public:
//pointer to model
RepSet* d_rep_set;
@@ -114,9 +119,7 @@ public:
//types we are considering
std::vector< TypeNode > d_types;
//domain we are considering
- std::vector< RepDomain > d_domain;
- //intervals
- std::map< int, Node > d_bounds[2];
+ std::vector< std::vector< Node > > d_domain_elements;
public:
/** increment the iterator at index=counter */
int increment2( int i );
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 31fdb0a40..d734a6b95 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -57,7 +57,12 @@ TESTS = \
LeftistHeap.scala-8-ncm.smt2 \
sc-crash-052316.smt2 \
bound-int-alt.smt2 \
- bug723-irrelevant-funs.smt2
+ bug723-irrelevant-funs.smt2 \
+ bounded_sets.smt2 \
+ fmf-strange-bounds.smt2 \
+ fmf-strange-bounds-2.smt2 \
+ fmf-bound-2dim.smt2 \
+ memory_model-R_cpp-dd.cvc
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/bounded_sets.smt2 b/test/regress/regress0/fmf/bounded_sets.smt2
new file mode 100644
index 000000000..b06c3636f
--- /dev/null
+++ b/test/regress/regress0/fmf/bounded_sets.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun S () (Set Int))
+(declare-fun P (Int) Bool)
+(declare-fun a () Int)
+(assert (member a S))
+(assert (forall ((y Int)) (=> (member y S) (P y))))
+
+
+(declare-fun T () (Set Int))
+(declare-fun b () Int)
+(assert (member b T))
+(assert (forall ((y Int)) (=> (member y T) (not (P y)))))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/fmf-bound-2dim.smt2 b/test/regress/regress0/fmf/fmf-bound-2dim.smt2
new file mode 100644
index 000000000..5f5c22770
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-bound-2dim.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun P (Int Int) Bool)
+
+(declare-fun a () Int)
+(assert (> a 10))
+
+(assert (forall ((x Int) (y Int))
+(=> (and (<= a x) (<= x (+ a 5)) (<= 14 y) (<= y (+ 7 x)))
+(P x y))))
+(assert (not (P 15 4)))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 b/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2
new file mode 100644
index 000000000..f1c53c4ef
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun P (Int U) Bool)
+
+(declare-fun S (U) (Set Int))
+
+(declare-fun f (U) U)
+
+(assert (forall ((x Int) (z U))
+(=> (member x (S (f z)))
+(P x z))))
+
+; need model of U size 2 to satisfy these
+(declare-fun a () U)
+(assert (member 77 (S a)))
+(assert (not (P 77 a)))
+
+; unsat
+(assert (forall ((x U) (y U)) (= x y)))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/fmf-strange-bounds.smt2 b/test/regress/regress0/fmf/fmf-strange-bounds.smt2
new file mode 100644
index 000000000..7812c2431
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-strange-bounds.smt2
@@ -0,0 +1,35 @@
+; COMMAND-LINE: --fmf-bound
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun P (Int Int U) Bool)
+
+(declare-fun S () (Set Int))
+
+(declare-fun f (Int) U)
+(declare-fun g (Int) U)
+
+(declare-fun h (U) Int)
+
+(assert (member 77 S))
+(assert (>= (h (f 77)) 3))
+(assert (>= (h (g 77)) 2))
+(assert (not (= (g 77) (f 77))))
+
+(assert (forall ((x Int) (y Int) (z U)) (=>
+(or (= z (f x)) (= z (g x)))
+(=> (member x S)
+(=> (and (<= 0 y) (<= y (h z)))
+(P x y z))))))
+
+
+(declare-fun Q (U Int) Bool)
+(declare-const a U)
+(declare-const b U)
+(declare-const c U)
+(assert (distinct a b c))
+(assert (forall ((x U) (y Int)) (=> (and (<= 3 y) (<= y 10) (or (= x c) (= x (f y)))) (Q x y))))
+(assert (not (Q b 6)))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc b/test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc
new file mode 100644
index 000000000..5d1289997
--- /dev/null
+++ b/test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc
@@ -0,0 +1,52 @@
+% EXPECT: sat
+OPTION "produce-models";
+OPTION "fmf-bound";
+
+DATATYPE MOPERATION = R | W | M END;
+DATATYPE ORDER = I | SC | U END;
+DATATYPE ATOM = AT | NA END;
+
+DATATYPE BINT = I0 | I1 | I2 | I3 END;
+
+DATATYPE TEAR_TYPE = TEAR_TRUE | TEAR_FALSE END;
+SDBLOCK_TYPE: TYPE;
+VALUE_TYPE: TYPE;
+ADDRESS_TYPE: TYPE = SET OF BINT;
+
+MEM_OP_TYPE : TYPE = [# O:MOPERATION, T:TEAR_TYPE, R:ORDER, A:ATOM, B:SDBLOCK_TYPE, M:ADDRESS_TYPE, V:VALUE_TYPE #];
+EV_REL: TYPE = SET OF [MEM_OP_TYPE, MEM_OP_TYPE];
+THREAD_TYPE : TYPE = [# E:SET OF MEM_OP_TYPE, PO:EV_REL #];
+
+m1 : SDBLOCK_TYPE;
+
+ow1 : MEM_OP_TYPE;
+or2 : MEM_OP_TYPE;
+
+v1 : VALUE_TYPE;
+v2 : VALUE_TYPE;
+
+ASSERT (ow1.O = W) AND
+ (ow1.T = TEAR_FALSE) AND
+ (ow1.R = U) AND
+ (ow1.A = NA) AND
+ (ow1.B = m1) AND
+ (ow1.M = {I0}) AND
+ (ow1.V = v1);
+
+ASSERT (or2.O = R) AND
+ (or2.T = TEAR_FALSE) AND
+ (or2.R = U) AND
+ (or2.A = NA) AND
+ (or2.B = m1) AND
+ (or2.M = {I0}) AND
+ (or2.V = v2);
+
+ev_set : SET OF MEM_OP_TYPE;
+
+ASSERT ev_set = {ow1, or2};
+
+RF : EV_REL;
+
+ASSERT FORALL (r,w: MEM_OP_TYPE) : (((r IS_IN ev_set) AND (w IS_IN ev_set)) => (((r,w) IS_IN RF) <=> ((r.O = R) AND (w.O = W))));
+
+CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback