From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 23 May 2009 15:11:23 +0000 (+0000)
Subject: Propositional ITEs as per SMTLIB.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4b46d1fca989dd1871af0de98d3423db5be69ba9;p=francis%2Fstp.git

Propositional ITEs as per SMTLIB.

* Previously the "if_then_else" function not the "ite" function handled "then" and "else"'s which were propositional. Now the "ite" does both.
* Remove deprecation warnings.. Will fix later.
* Fix the BVTypecheck for ITEs.





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

diff --git a/AST/AST.cpp b/AST/AST.cpp
index d61f0ca..5d88742 100644
--- a/AST/AST.cpp
+++ b/AST/AST.cpp
@@ -1842,9 +1842,7 @@ string ASTNode::functionToSMTLIBName(const Kind k) const
       case SYMBOL:
 	return;
       case ITE:     
-	if(BOOLEAN_TYPE != n[0].GetType() && 
-	   BITVECTOR_TYPE != n[1].GetType() &&
-	   BITVECTOR_TYPE != n[2].GetType())
+	if (BOOLEAN_TYPE != n[0].GetType() || (n[1].GetType() != n[2].GetType()))
 	  FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",n);
 	if(n[1].GetValueWidth() != n[2].GetValueWidth())
 	  FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n",n);
diff --git a/AST/AST.h b/AST/AST.h
index 4ec8e7f..14d3a39 100644
--- a/AST/AST.h
+++ b/AST/AST.h
@@ -1493,6 +1493,7 @@ namespace BEEV {
     ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2);
     ASTNode ITEOpt_InEqs(const ASTNode& in1);
     ASTNode CreateSimplifiedTermITE(const ASTNode& t1, const ASTNode& t2, const ASTNode& t3);
+    ASTNode CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2);
     ASTNode CreateSimplifiedINEQ(Kind k, const ASTNode& a0, const ASTNode& a1, bool pushNeg);
     ASTNode SimplifyNotFormula(const ASTNode& a, bool pushNeg);
     ASTNode SimplifyAndOrFormula(const ASTNode& a, bool pushNeg);
diff --git a/Makefile.common b/Makefile.common
index 36be902..3200510 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -11,7 +11,7 @@
 #OPTIMIZE = -g     # Debugging
 OPTIMIZE = -O3     # Maximum optimization
 
-CFLAGS_BASE = $(OPTIMIZE) $(OPTIONS1) $(OPTIONS2)
+CFLAGS_BASE = $(OPTIMIZE) $(OPTIONS1) $(OPTIONS2) 
 # You can compile using make STATIC=true to compile a statically linked executable
 # Note that you should execute liblinks.sh first.
 ifdef STATIC
@@ -43,7 +43,7 @@ else
   CFLAGS = $(CFLAGS_BASE)
 endif
 
-CXXFLAGS = $(CFLAGS) -Wall -DEXT_HASH_MAP
+CXXFLAGS = $(CFLAGS) -Wall -DEXT_HASH_MAP -Wno-deprecated
 #CXXFLAGS = $(CFLAGS) -Wall -DTR1_UNORDERED_MAP
 #CXXFLAGS = $(CFLAGS) -Wall 
 #LDFLAGS= -lstdc++
diff --git a/parser/smtlib.lex b/parser/smtlib.lex
index 27c2b1f..a045e1f 100644
--- a/parser/smtlib.lex
+++ b/parser/smtlib.lex
@@ -128,7 +128,6 @@ bit{DIGIT}+     {
 "not"           { return NOT_TOK; }
 "implies"       { return IMPLIES_TOK; }
 "ite"           { return ITE_TOK;}
-"if_then_else"  { return IF_THEN_ELSE_TOK; }
 "and"           { return AND_TOK; }
 "or"            { return OR_TOK; }
 "xor"           { return XOR_TOK; }
diff --git a/parser/smtlib.y b/parser/smtlib.y
index 55fb325..ad49743 100644
--- a/parser/smtlib.y
+++ b/parser/smtlib.y
@@ -113,7 +113,6 @@
 %token NOT_TOK
 %token IMPLIES_TOK
 %token ITE_TOK
-%token IF_THEN_ELSE_TOK
 %token AND_TOK
 %token OR_TOK
 %token XOR_TOK
@@ -570,9 +569,9 @@ an_formula:
       delete $3;
       delete $4;
     }
-  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula RPAREN_TOK
+  | LPAREN_TOK ITE_TOK an_formula an_formula an_formula RPAREN_TOK
     {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$3, *$4, *$5));
+      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateSimplifiedFormulaITE(*$3, *$4, *$5));
       delete $3;
       delete $4;
       delete $5;
diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp
index 2aa88b5..b984687 100644
--- a/simplifier/simplifier.cpp
+++ b/simplifier/simplifier.cpp
@@ -578,6 +578,32 @@ namespace BEEV {
     return CreateTerm(ITE,t1.GetValueWidth(),t0,t1,t2);
   }
 
+ASTNode BeevMgr::CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2) {
+	ASTNode t0 = in0;
+	ASTNode t1 = in1;
+	ASTNode t2 = in2;
+	CountersAndStats("CreateSimplifiedFormulaITE");
+
+	if (optimize) {
+		if (t0 == ASTTrue)
+			return t1;
+		if (t0 == ASTFalse)
+			return t2;
+		if (t1 == t2)
+			return t1;
+		if (CheckAlwaysTrueFormMap(t0)) {
+			return t1;
+		}
+		if (CheckAlwaysTrueFormMap(CreateNode(NOT, t0)) || (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) {
+			return t2;
+		}
+	}
+	ASTNode result = CreateNode(ITE, t0, t1, t2);
+	BVTypeCheck(result);
+	return result;
+}
+
+
   ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg) {
     ASTNode output;
     //cerr << "input:\n" << a << endl;