From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 13 Apr 2011 02:00:29 +0000 (+0000)
Subject: Improvement. Replace the hashing node factory with the simplifying node factory.... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e83c89ff8d5d317e98c08a1e1e2630278e60d75e;p=francis%2Fstp.git

Improvement. Replace the hashing node factory with the simplifying node factory. Add an extra obscure simplification rule.

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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index d77af5e..4e1668e 100644
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -13,6 +13,7 @@ namespace BEEV
 SubstitutionMap::~SubstitutionMap()
 {
 	delete SolverMap;
+	delete nf;
 }
 
 // if false. Don't simplify while creating the substitution map.
@@ -126,31 +127,52 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
   else if (XOR == k)
   {
 	  if (a.Degree() !=2)
-		  return output;
+	    return output;
 
 	  int to = TermOrder(a[0],a[1]);
 	  if (0 == to)
-		  return output;
-
-	  ASTNode symbol,rhs;
-	  if (to==1)
-	  {
-		  symbol = a[0];
-		  rhs = a[1];
-	  }
+	    {
+	      if (a[0].GetKind() == NOT && a[0][0].GetKind() == EQ && a[0][0][0].GetValueWidth() ==1 && a[0][0][1].GetKind() == SYMBOL)
+	        {
+	          // (XOR (NOT(= (1 v)))  ... )
+	          const ASTNode& symbol = a[0][0][1];
+	          const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], a[0][0][0], nf->CreateTerm(BVNEG, 1,a[0][0][0]));
+
+                  if (UpdateSolverMap(symbol, newN))
+                      output =  ASTTrue;
+	        }
+	      else if (a[0].GetKind() == EQ && a[0][0].GetValueWidth() ==1 && a[0][1].GetKind() == SYMBOL)
+	        {
+                  // XOR ((= 1 v) ... )
+
+	          const ASTNode& symbol = a[0][1];
+                  const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], nf->CreateTerm(BVNEG, 1,a[0][0]), a[0][0]);
+
+                  if (UpdateSolverMap(symbol, newN))
+                      output =  ASTTrue;
+	        }
+	      else
+	      return output;
+	    }
 	  else
-	  {
-		  symbol = a[0];
-		  rhs = a[1];
-	  }
-
-	  assert(symbol.GetKind() == SYMBOL);
-
-	  // If either side is already solved for.
-	  if (CheckSubstitutionMap(symbol) || CheckSubstitutionMap(rhs))
-	  {}
-	  else if (UpdateSolverMap(symbol, bm->CreateNode(NOT, rhs)))
-			output =  ASTTrue;
+	    {
+                ASTNode symbol,rhs;
+                if (to==1)
+                {
+                    symbol = a[0];
+                    rhs = a[1];
+                }
+                else
+                {
+                    symbol = a[1];
+                    rhs = a[0];
+                }
+
+                assert(symbol.GetKind() == SYMBOL);
+
+                if (UpdateSolverMap(symbol, nf->CreateNode(NOT, rhs)))
+                   output =  ASTTrue;
+	    }
   }
   else if (AND == k)
     {
@@ -178,7 +200,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
       else if (o.size() == 1)
         output = o[0];
       else if (o != c)
-    	output = bm->CreateNode(AND, o);
+    	output = nf->CreateNode(AND, o);
       else
     	output = a;
     }
@@ -191,8 +213,7 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n)
 {
 	bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions);
 	ASTNodeMap cache;
-	SimplifyingNodeFactory nf(*bm->hashingNodeFactory, *bm);
-	ASTNode result =  replace(n,*SolverMap,cache,&nf, false);
+	ASTNode result =  replace(n,*SolverMap,cache,nf, false);
 
 	// NB. This is an expensive check. Remove it after it's been idempotent
 	// for a while.
@@ -210,8 +231,7 @@ ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n)
 {
 	bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions);
 	ASTNodeMap cache;
-	SimplifyingNodeFactory nf(*bm->hashingNodeFactory, *bm);
-	ASTNode result = replace(n,*SolverMap,cache,&nf, true);
+	ASTNode result = replace(n,*SolverMap,cache,nf, true);
 	bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions);
 	return result;
 }
diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 5c4ca60..bc4bff8 100644
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -24,6 +24,7 @@ class SubstitutionMap {
 	Simplifier *simp;
 	STPMgr* bm;
 	ASTNode ASTTrue, ASTFalse, ASTUndefined;
+	NodeFactory *nf;
 
 	// These are used to avoid substituting {x = f(y,z), z = f(x)}
 	typedef hash_map<ASTNode, Symbols*,ASTNode::ASTNodeHasher> DependsType;
@@ -60,7 +61,8 @@ public:
 
 	VariablesInExpression vars;
 
-	SubstitutionMap(Simplifier *_simp, STPMgr* _bm) {
+	SubstitutionMap(Simplifier *_simp, STPMgr* _bm)
+	{
 		simp = _simp;
 		bm = _bm;
 
@@ -71,6 +73,7 @@ public:
 		SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
 		loopCount = 0;
 		substitutionsLastApplied =0;
+	        nf = new SimplifyingNodeFactory (*bm->hashingNodeFactory, *bm);
 	}
 
 	void clear()