diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-27 09:30:06 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-27 09:30:06 +0200 |
commit | 65c2e1688d83dfeb913b689c10d9b43c5dc89cc0 (patch) | |
tree | f552414624cd7259e638b6edc0c7a710a4215138 /src/theory/rep_set.cpp | |
parent | e4cff69e3b565e928dbf04960249477ce2c9ef6b (diff) |
Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index eb05564e5..6a64f762e 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -16,6 +16,7 @@ #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; using namespace CVC4; @@ -187,8 +188,14 @@ bool RepSetIterator::initialize(){ TypeNode tn = d_types[i]; Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl; if( tn.isSort() ){ + //must ensure uninterpreted type is non-empty. if( !d_rep_set->hasType( tn ) ){ - Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); + //FIXME: + // terms in rep_set are now constants which mapped to terms through TheoryModel + // thus, should introduce a constant and a term. for now, just a term. + + //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); + Node var = d_qe->getModel()->getSomeDomainElement( tn ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); } @@ -216,15 +223,18 @@ bool RepSetIterator::initialize(){ d_incomplete = true; } } - //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now + //enumerate if the sort is reasonably small }else 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 + Assert( d_rep_set->hasType( tn ) ); }else{ Trace("rsi") << " variable cannot be bounded." << std::endl; Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } + //if we have yet to determine the type of enumeration if( d_enum_type.size()<=i ){ d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); if( d_rep_set->hasType( tn ) ){ |