From ca57717a91b94e6e36437c2707a7a6ec213376b9 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 15 Jun 2012 14:28:01 +0000 Subject: [PATCH] Partial implementation of the SMT-LIB2 define function syntax. Won't work with push/pop. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1665 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 6 + .../CounterExample.cpp | 4 +- src/cpp_interface/cpp_interface.h | 77 ++++++++++ src/parser/LetMgr.h | 6 +- src/parser/smt2.lex | 8 + src/parser/smt2.y | 139 +++++++++++++++++- 6 files changed, 230 insertions(+), 10 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index cde63ae..567f6d2 100644 --- 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 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 9f59e0f..8d8e0ef 100644 --- 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 051d48b..266dfa2 100644 --- a/src/cpp_interface/cpp_interface.h +++ b/src/cpp_interface/cpp_interface.h @@ -50,6 +50,15 @@ namespace BEEV vector cache; vector > symbols; + struct Function + { + ASTVec params; + ASTNode function; + string name; + }; + + HASHMAP > 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 6455fba..bb2ba26 100644 --- 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 struct hashF { size_t operator() (const T & x) const { @@ -28,6 +27,7 @@ namespace BEEV } }; + private: const ASTNode ASTUndefined; typedef hash_map > MapType; diff --git a/src/parser/smt2.lex b/src/parser/smt2.lex index 2d64ff0..2609de5 100644 --- 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 aa79897..cdecd55 100644 --- a/src/parser/smt2.y +++ b/src/parser/smt2.y @@ -84,9 +84,10 @@ %start cmd %type status -%type an_formulas an_terms +%type an_formulas an_terms function_params an_mixed -%type an_term an_formula + +%type an_term an_formula function_param %token NUMERAL_TOK %token BVCONST_DECIMAL_TOK @@ -96,8 +97,8 @@ /* We have this so we can parse :smt-lib-version 2.0 */ %token DECIMAL_TOK -%token FORMID_TOK TERMID_TOK -%token STRING_TOK +%token FORMID_TOK TERMID_TOK +%token 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; +} + ; %% -- 2.47.3