From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 20 Feb 2014 23:03:24 +0000 (-0600)
Subject: Merge branch 'master' of github.com:tiliang/CVC4
X-Git-Tag: cvc5-1.0.0~7080^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f0f26da448a22fd111041f1c33194040ef4dc25;p=cvc5.git

Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
	src/theory/strings/theory_strings_preprocess.cpp
---

7f0f26da448a22fd111041f1c33194040ef4dc25
diff --cc src/theory/strings/theory_strings_preprocess.cpp
index 04e7a06cc,6520f5517..1df79ccff
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@@ -238,11 -236,6 +238,11 @@@ Node StringsPreprocess::simplify( Node 
  			Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
  			Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
  
- 			Node lem = NodeManager::currentNM()->mkNode(kind::IFF,
++			/*Node lem = NodeManager::currentNM()->mkNode(kind::IFF,
 +				t.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
 +				t[0].eqNode(d_zero));
- 			new_nodes.push_back(lem);
++			new_nodes.push_back(lem);*/
 +
  			Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
  			Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
  			Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
@@@ -276,10 -269,6 +276,10 @@@
  			Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
  			Node cc2 = ufx.eqNode(ufMx);
  			cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2);
 +			// leading zero
- 			Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(t[0]).negate());
++			Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate());
 +			Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero));
 +			//cc3
  			Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
  			Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);