diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-15 10:39:29 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-15 10:39:29 +0200 |
commit | bad7f4fe4dca4c6511c2862bf81b6791640ac78f (patch) | |
tree | 0be31a9300766d39ae36c9efba02e2c5a68dd156 /src/theory/theory_model.cpp | |
parent | ace360b4da1edef06088a366dc21b58f9431efc2 (diff) |
Fix bug related to quantifiers + incremental, thanks John Backes for the bug report. Other minor cleanup.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 5766a26c1..c4bc94bd2 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -236,35 +236,6 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){ return Node::null(); } -//FIXME: need to ensure that theory enumerators exist for each sort -Node TheoryModel::getNewDomainValue( TypeNode tn ){ - if( tn.isSort() ){ - return Node::null(); - }else{ - TypeEnumerator te(tn); - while( !te.isFinished() ){ - Node r = *te; - if(Debug.isOn("getNewDomainValue")) { - Debug("getNewDomainValue") << "getNewDomainValue( " << tn << ")" << endl; - Debug("getNewDomainValue") << "+ TypeEnumerator gave: " << r << endl; - Debug("getNewDomainValue") << "+ d_type_reps are:"; - for(vector<Node>::const_iterator i = d_rep_set.d_type_reps[tn].begin(); - i != d_rep_set.d_type_reps[tn].end(); - ++i) { - Debug("getNewDomainValue") << " " << *i; - } - Debug("getNewDomainValue") << endl; - } - if( std::find(d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r) ==d_rep_set.d_type_reps[tn].end() ) { - Debug("getNewDomainValue") << "+ it's new, so returning " << r << endl; - return r; - } - ++te; - } - return Node::null(); - } -} - /** add substitution */ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ if( !d_substitutions.hasSubstitution( x ) ){ |