Partial implementation of the SMT-LIB2 define function syntax. Won't work with push...

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index cde63ae0f70bf9fbaca595a1b2ad960a36fbf86b..567f6d282e12d02a172017ce0d4ca5d16a1e489c 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -23,6 +23,7 @@
 #include "../simplifier/UseITEContext.h"
 #include "../simplifier/AlwaysTrue.h"
 #include "../simplifier/AIGSimplifyPropositionalCore.h"
+#include "../simplifier/TransformExtensionality.h"
 #include <memory>
 
 namespace BEEV {
@@ -81,6 +82,11 @@ namespace BEEV {
         NewSolver.setSeed(bm->UserFlags.random_seed);
       }
 
+    TransformExtensionality t(bm);
+    original_input = t.topLevel(original_input);
+
+
+
        SOLVER_RETURN_TYPE result;
     result = TopLevelSTPAux(NewSolver,
                              original_input);

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 9f59e0f455b2a5119e58be58fe9be1ac7b697fdb..8d8e0ef2fe68290625a9e10e9e0eddad55dc05e7 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -955,8 +955,8 @@ namespace BEEV
         // invalid
         if (ASTTrue == orig_result)
           {
-            if (bm->UserFlags.check_counterexample_flag)
-                                CheckCounterExample(SatSolver.okay());
+            //if (bm->UserFlags.check_counterexample_flag)
+              //                  CheckCounterExample(SatSolver.okay());
 
             if (bm->UserFlags.stats_flag
                 || bm->UserFlags.print_counterexample_flag)

diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h
index 051d48bf6d2f8a0b5971822ff3424783728f5d30..266dfa2f76ca9c4cfedfb46defcbc10ec1ef37ce 100644 (file)
--- a/src/cpp_interface/cpp_interface.h
+++ b/src/cpp_interface/cpp_interface.h
@@ -50,6 +50,15 @@ namespace BEEV
     vector<Entry> cache;
     vector<vector<ASTNode> > symbols;
 
+    struct Function
+    {
+      ASTVec params;
+      ASTNode function;
+      string name;
+    };
+
+    HASHMAP <string, Function, BEEV::LETMgr::hashF<std::string> > functions;
+
     void checkInvariant()
     {
       assert(bm.getAssertLevel() == cache.size());
@@ -183,6 +192,74 @@ namespace BEEV
       return bm.LookupOrCreateSymbol(name);
     }
 
+    void
+    removeSymbol(ASTNode s)
+    {
+      bool removed=false;
+
+     for (int i=0; i < symbols.back().size(); i++)
+       if (symbols.back()[i] == s)
+         {
+         symbols.back().erase(symbols.back().begin() + i);
+         removed = true;
+         }
+
+     if (!removed)
+       FatalError("Should have been removed...");
+
+     letMgr._parser_symbol_table.erase(s);
+    }
+
+    // Declare a function. We can't keep references to the declared variables though. So rename them..
+    void
+    storeFunction(const string name, const ASTVec& params, const ASTNode& function)
+    {
+      Function f;
+      f.name = name;
+
+      ASTNodeMap fromTo;
+      for (int i=0; i < params.size();i++)
+        {
+          ASTNode p = bm.CreateFreshVariable(params[i].GetIndexWidth(), params[i].GetValueWidth(), "STP_INTERNAL_FUNCTION_NAME");
+          fromTo.insert(make_pair(params[i], p));
+          f.params.push_back(p);
+        }
+      ASTNodeMap cache;
+      f.function = SubstitutionMap::replace(function,fromTo,cache, nf);
+      functions.insert(make_pair(f.name,f));
+    }
+
+    ASTNode
+    applyFunction(const string name, const ASTVec& params)
+    {
+      if (functions.find(name) == functions.end())
+        FatalError("Trying to apply function which has not been defined.");
+
+      Function f;
+      f = functions[string(name)];
+
+      ASTNodeMap fromTo;
+      for (int i=0; i < f.params.size();i++)
+        {
+          if (f.params[i].GetValueWidth() != params[i].GetValueWidth())
+            FatalError("Actual parameters differ from formal");
+
+          if (f.params[i].GetIndexWidth() != params[i].GetIndexWidth())
+            FatalError("Actual parameters differ from formal");
+
+          fromTo.insert(make_pair(f.params[i], params[i]));
+        }
+
+      ASTNodeMap cache;
+      return SubstitutionMap::replace(f.function,fromTo,cache, nf);
+    }
+
+    bool isFunction(const string name)
+    {
+      return (functions.find(name) != functions.end());
+    }
+
+
     ASTNode
     LookupOrCreateSymbol(string name)
     {

diff --git a/src/parser/LetMgr.h b/src/parser/LetMgr.h
index 6455fba4dd7bbd25de58eafa61317afd499f281d..bb2ba26962957bb08547a8912cc66ee6eb2357e1 100644 (file)
--- a/src/parser/LetMgr.h
+++ b/src/parser/LetMgr.h
@@ -18,9 +18,8 @@ namespace BEEV
 //LET Management
   class LETMgr 
   {
-  private:
-
-         // Hash function for the hash_map of a string..
+  public:
+    // Hash function for the hash_map of a string..
        template <class T>
        struct hashF {
                                  size_t operator() (const T & x) const {
@@ -28,6 +27,7 @@ namespace BEEV
                                  }
                  };
 
+  private:
     const ASTNode ASTUndefined;
 
     typedef hash_map<string,ASTNode, hashF<std::string> > MapType;

diff --git a/src/parser/smt2.lex b/src/parser/smt2.lex
index 2d64ff06e5d4938e11193674def0c2a769a15824..2609de5e06f0789b71b2a505436af41571adc91d 100644 (file)
--- a/src/parser/smt2.lex
+++ b/src/parser/smt2.lex
@@ -81,6 +81,13 @@
        nptr = BEEV::parserInterface->letMgr.resolveLet(str);
        found = true;
     }
+    else if (BEEV::parserInterface->isFunction(str))
+    {
+               smt2lval.str = new std::string(str);
+               return  FUNCTIONID_TOK;
+    }
+    
+    
 
        if (found)
        {
@@ -166,6 +173,7 @@ bv{DIGIT}+  { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_
 "set-info"             { return NOTES_TOK;  }
 "set-option"           { return OPTION_TOK;  }
 "declare-fun"          { return DECLARE_FUNCTION_TOK; }
+"define-fun"           { return DEFINE_FUNCTION_TOK; }
 "push"                         { return PUSH_TOK;}
 "pop"                          { return POP_TOK;}
  

diff --git a/src/parser/smt2.y b/src/parser/smt2.y
index aa79897ad03a3eb933210d41ef537a2d04afeb9e..cdecd55b6ea65f854c9fdd77075d1cee3cf90d91 100644 (file)
--- a/src/parser/smt2.y
+++ b/src/parser/smt2.y
@@ -84,9 +84,10 @@
 %start cmd
 
 %type <node> status
-%type <vec> an_formulas an_terms
+%type <vec> an_formulas an_terms function_params an_mixed
 
-%type <node> an_term  an_formula 
+
+%type <node> an_term  an_formula function_param
 
 %token <uintval> NUMERAL_TOK
 %token <str> BVCONST_DECIMAL_TOK
@@ -96,8 +97,8 @@
  /* We have this so we can parse :smt-lib-version 2.0 */
 %token  DECIMAL_TOK
 
-%token <node> FORMID_TOK TERMID_TOK 
-%token <str> STRING_TOK
+%token <node> FORMID_TOK TERMID_TOK  
+%token <str> STRING_TOK FUNCTIONID_TOK
 
 
  /* set-info tokens */
@@ -180,6 +181,7 @@
 %token NOTES_TOK
 %token OPTION_TOK
 %token DECLARE_FUNCTION_TOK
+%token DEFINE_FUNCTION_TOK
 %token FORMULA_TOK
 %token PUSH_TOK
 %token POP_TOK
@@ -254,6 +256,10 @@ cmdi:
     {
     parserInterface->success();
     }
+|   LPAREN_TOK DEFINE_FUNCTION_TOK function_decl RPAREN_TOK
+    {
+    parserInterface->success();
+    }
 |   LPAREN_TOK FORMULA_TOK an_formula RPAREN_TOK
        {
        parserInterface->AddAssert(*$3);
@@ -262,6 +268,70 @@ cmdi:
        }
 ;
 
+
+function_param:
+LPAREN_TOK STRING_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK RPAREN_TOK
+{
+  $$ = new ASTNode(BEEV::parserInterface->LookupOrCreateSymbol($2->c_str())); 
+  parserInterface->addSymbol(*$$);
+  $$->SetIndexWidth(0);
+  $$->SetValueWidth($6);
+  delete $2;
+};
+
+/* Returns a vector of parameters.*/
+function_params:
+function_param
+{
+  $$ = new ASTVec;
+  $$->push_back(*$1);
+  delete $1;
+}
+| function_params function_param
+{
+  $$ = $1;
+  $$->push_back(*$2);
+  delete $2;
+};
+
+
+function_decl:
+STRING_TOK LPAREN_TOK function_params RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK LPAREN_TOK an_term RPAREN_TOK 
+{
+       if ($11->GetValueWidth() != $8)
+               {
+                       char msg [100];
+                       sprintf(msg, "Different bit-widths specified: %d %d", $11->GetValueWidth(), $8);
+                       yyerror(msg);
+               }
+       
+       BEEV::parserInterface->storeFunction(*$1, *$3, *$11);
+
+       // Next time the variable is used, we want it to be fresh.
+    for (int i = 0; i < $3->size(); i++)
+     BEEV::parserInterface->removeSymbol((*$3)[i]);
+       
+       delete $1;
+       delete $3;
+       delete $11;
+}
+|
+STRING_TOK LPAREN_TOK function_params RPAREN_TOK BOOL_TOK an_formula 
+{
+       // Check the bitwidth defined/ and actually are the same.
+       BEEV::parserInterface->storeFunction(*$1, *$3, *$6);
+
+       // Next time the variable is used, we want it to be fresh.
+    for (int i = 0; i < $3->size(); i++)
+     BEEV::parserInterface->removeSymbol((*$3)[i]);
+
+       delete $1;
+       delete $3;
+       delete $6;
+}
+;
+
+
 status:
 STRING_TOK { 
  
@@ -300,9 +370,10 @@ SOURCE_TOK
 {
        parserInterface->setPrintSuccess(false);
 }
-
 ;
 
+
+
 var_decl:
 STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK
 {
@@ -345,6 +416,45 @@ STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TO
 }
 ;
 
+an_mixed:
+an_formula
+{
+  $$ = new ASTVec;
+  if ($1 != NULL) {
+    $$->push_back(*$1);
+    parserInterface->deleteNode($1);
+  }
+}
+|
+an_term
+{
+  $$ = new ASTVec;
+  if ($1 != NULL) {
+    $$->push_back(*$1);
+    parserInterface->deleteNode($1);
+  }
+}
+|
+an_mixed an_formula 
+{
+  if ($1 != NULL && $2 != NULL) {
+    $1->push_back(*$2);
+    $$ = $1;
+    parserInterface->deleteNode($2);
+  }
+}
+|
+an_mixed an_term 
+{
+  if ($1 != NULL && $2 != NULL) {
+    $1->push_back(*$2);
+    $$ = $1;
+    parserInterface->deleteNode($2);
+  }
+};
+
+
+
 an_formulas:
 an_formula
 {
@@ -546,6 +656,14 @@ TRUE_TOK
   //Cleanup the LetIDToExprMap
   parserInterface->letMgr.CleanupLetIDMap();                      
 }
+| LPAREN_TOK FUNCTIONID_TOK an_mixed RPAREN_TOK
+{      
+  $$ = parserInterface->newNode(parserInterface->applyFunction(*$2,*$3));
+  if ($$->GetType() != BOOLEAN_TYPE)
+       yyerror("Must be boolean type");
+  delete $2;
+  delete $3;
+}
 ;
 
 lets: let lets 
@@ -959,6 +1077,17 @@ TERMID_TOK
     $$->SetValueWidth(width);
     delete $1;
 }
+| LPAREN_TOK FUNCTIONID_TOK an_mixed RPAREN_TOK
+{      
+  $$ = parserInterface->newNode(parserInterface->applyFunction(*$2,*$3));
+  
+  if ($$->GetType() != BITVECTOR_TYPE)
+       yyerror("Must be bitvector type");
+  
+  delete $2;
+  delete $3;
+}
+
 ;
 
 %%