From bad7f4fe4dca4c6511c2862bf81b6791640ac78f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 15 Sep 2015 10:39:29 +0200 Subject: Fix bug related to quantifiers + incremental, thanks John Backes for the bug report. Other minor cleanup. --- src/theory/theory_model.cpp | 29 ----------------------------- 1 file changed, 29 deletions(-) (limited to 'src/theory/theory_model.cpp') 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::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 ) ){ -- cgit v1.2.3