Speedup. Shortcut if the thing we are simplifying is already a constant.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@860 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index da4e501e8c783d70d1f81788a81e9c89a049dbc8..47271b99454b863e28e5d96b453b378db70b510d 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1592,7 +1592,10 @@ namespace BEEV
   Simplifier::SimplifyTerm(const ASTNode& actualInputterm, 
                            ASTNodeMap* VarConstMap)
   {
-    ASTNode inputterm(actualInputterm); // mutable local copy.
+    if (actualInputterm.isConstant())
+       return actualInputterm;
+
+       ASTNode inputterm(actualInputterm); // mutable local copy.
 
     //cout << "SimplifyTerm: input: " << a << endl;
     // if (!optimize_flag)