From e9d8ae34db4c4a8161cc1abdfb225c3e9e2bd9ee Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 12 Feb 2013 23:04:53 -0500 Subject: Fix a preprocessing performance issue. --- src/theory/theory_engine.cpp | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'src/theory') diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index efbc42ebf..f85a5f3cd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -728,16 +728,6 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut); Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl; - //must add substitutions to model - theory::TheoryModel* m = getModel(); - if( m ){ - for( SubstitutionMap::iterator pos = substitutionOut.begin(); pos != substitutionOut.end(); ++pos) { - Node n = (*pos).first; - Node v = (*pos).second; - Trace("model") << "Add substitution : " << n << " " << v << std::endl; - m->addSubstitution( n, v ); - } - } return solveStatus; } -- cgit v1.2.3