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 d61f0cac117b68a7af0aca978dcfbf2f4bef09bd..5d8874200b23797cce31e39b0c0adab7f5ffceed 100644 (file)
--- 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 4ec8e7f6f32b6415f474ff1a281f72d29176633a..14d3a398c2ba5d005ed1b7547c3be2138c113a80 100644 (file)
--- 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 36be902d9faa9c1c5c19a4e4e09606656e9e5432..32005102978f89c8d5616a26325b95d8d69e76a9 100644 (file)
--- 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 27c2b1feccd8e3284a8dd316e22592b63fbc9168..a045e1f96e46790a5456907e0f75b143a8cb1d6f 100644 (file)
--- 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 55fb325d69eab0882b9d62bdbc958ad4badabce9..ad497435c379ec0a0ebf13d599e0ede8ffe53c1f 100644 (file)
--- 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 2aa88b5dc0d97cf9b7471cc6dc3b877b91349b46..b984687ce9371b69b3efc99426827033bef4c5de 100644 (file)
--- 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;