SOLVER_INVALID=0,
SOLVER_VALID=1,
SOLVER_UNDECIDED=2,
- SOLVER_ERROR=-100
+ SOLVER_ERROR=-100,
+ SOLVER_UNSATISFIABLE = 1,
+ SOLVER_SATISFIABLE = 0
};
//Empty vector. Useful commonly used ASTNodes
extern int cvclex_destroy(void);
extern int smtlex_destroy(void);
extern int smt2lex_destroy(void);
+extern vector<ASTVec> assertionsSMT2;
// callback for SIGALRM.
void handle_time_out(int parameter){
else
parserInterface = &piTypeCheckSimp;
+ if (onePrintBack)
+ {
+ if (bm->UserFlags.smtlib2_parser_flag)
+ {
+ cerr << "Printback from SMTLIB2 inputs isn't currently working." << endl;
+ cerr << "Please try again later" << endl;
+ cerr << "It works prior to revision 1354" << endl;
+ exit(1);
+ }
+ }
+
if (bm->UserFlags.smtlib1_parser_flag) {
smtparse((void*) AssertsQuery);
smtlex_destroy();
} else if (bm->UserFlags.smtlib2_parser_flag) {
- smt2parse((void*) AssertsQuery);
+ assertionsSMT2.push_back(ASTVec());
+ smt2parse((void*) AssertsQuery);
+ //parserInterface->letMgr.cleanupParserSymbolTable();
smt2lex_destroy();
} else {
cvcparse((void*) AssertsQuery);
}
bm->GetRunTimes()->stop(RunTimes::Parsing);
- if(((ASTVec*)AssertsQuery)->empty())
+ /* The SMTLIB2 has a command language. The parser calls all the functions,
+ * so when we get to here the parser has already called "exit". i.e. if the
+ * language is smt2 then all the work has already been done, and all we need
+ * to do is cleanup...
+ * */
+ if (!bm->UserFlags.smtlib2_parser_flag)
{
- FatalError("Input is Empty. Please enter some asserts and query\n");
- }
- if(((ASTVec*)AssertsQuery)->size() != 2)
- {
- FatalError("Input must contain a query\n");
- }
+ if (((ASTVec*) AssertsQuery)->empty())
+ {
+ FatalError("Input is Empty. Please enter some asserts and query\n");
+ }
- ASTNode asserts = (*(ASTVec*)AssertsQuery)[0];
- ASTNode query = (*(ASTVec*)AssertsQuery)[1];
+ if (((ASTVec*) AssertsQuery)->size() != 2)
+ {
+ FatalError("Input must contain a query\n");
+ }
- if (onePrintBack)
- {
+ ASTNode asserts = (*(ASTVec*) AssertsQuery)[0];
+ ASTNode query = (*(ASTVec*) AssertsQuery)[1];
- ASTNode original_input = bm->CreateNode(AND,
- bm->CreateNode(NOT, query),
- asserts);
+ if (onePrintBack)
+ {
+ ASTNode original_input = bm->CreateNode(AND, bm->CreateNode(NOT, query), asserts);
- if(bm->UserFlags.print_STPinput_back_flag)
- {
- if(bm->UserFlags.smtlib1_parser_flag)
- bm->UserFlags.print_STPinput_back_SMTLIB2_flag = true;
- else
- bm->UserFlags.print_STPinput_back_CVC_flag = true;
- }
+ if (bm->UserFlags.print_STPinput_back_flag)
+ {
+ if (bm->UserFlags.smtlib1_parser_flag)
+ bm->UserFlags.print_STPinput_back_SMTLIB2_flag = true;
+ else
+ bm->UserFlags.print_STPinput_back_CVC_flag = true;
+ }
- if (bm->UserFlags.print_STPinput_back_CVC_flag)
- {
- //needs just the query. Reads the asserts out of the data structure.
- print_STPInput_Back(query);
- }
+ if (bm->UserFlags.print_STPinput_back_CVC_flag)
+ {
+ //needs just the query. Reads the asserts out of the data structure.
+ print_STPInput_Back(query);
+ }
- if (bm->UserFlags.print_STPinput_back_SMTLIB1_flag)
- {
- printer::SMTLIB1_PrintBack(cout, original_input);
- }
+ if (bm->UserFlags.print_STPinput_back_SMTLIB1_flag)
+ {
+ printer::SMTLIB1_PrintBack(cout, original_input);
+ }
- if (bm->UserFlags.print_STPinput_back_SMTLIB2_flag)
- {
- printer::SMTLIB2_PrintBack(cout, original_input);
- }
+ if (bm->UserFlags.print_STPinput_back_SMTLIB2_flag)
+ {
+ printer::SMTLIB2_PrintBack(cout, original_input);
+ }
- if (bm->UserFlags.print_STPinput_back_C_flag)
- {
- printer::C_Print(cout, original_input);
- }
+ if (bm->UserFlags.print_STPinput_back_C_flag)
+ {
+ printer::C_Print(cout, original_input);
+ }
- if (bm->UserFlags.print_STPinput_back_GDL_flag)
- {
- printer::GDL_Print(cout, original_input);
- }
+ if (bm->UserFlags.print_STPinput_back_GDL_flag)
+ {
+ printer::GDL_Print(cout, original_input);
+ }
- if (bm->UserFlags.print_STPinput_back_dot_flag)
- {
- printer::Dot_Print(cout, original_input);
- }
+ if (bm->UserFlags.print_STPinput_back_dot_flag)
+ {
+ printer::Dot_Print(cout, original_input);
+ }
- return 0;
- }
+ return 0;
+ }
- SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query);
- if (bm->UserFlags.quick_statistics_flag)
- {
- bm->GetRunTimes()->print();
- }
- (GlobalSTP->tosat)->PrintOutput(ret);
+ SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query);
+ if (bm->UserFlags.quick_statistics_flag)
+ {
+ bm->GetRunTimes()->print();
+ }
+ (GlobalSTP->tosat)->PrintOutput(ret);
+ asserts = ASTNode();
+ query = ASTNode();
+ }
AssertsQuery->clear();
delete AssertsQuery;
- asserts = ASTNode();
- query = ASTNode();
+
_empty_ASTVec.clear();
simpCleaner.release();
delete ParserBM;
-
-
return 0;
}//end of Main
#include <cassert>
#include "LetMgr.h"
#include "../STPManager/STPManager.h"
+#include "../STPManager/STP.h"
//#include "../boost/pool/object_pool.hpp"
namespace BEEV
{
assert(nf != NULL);
alreadyWarned = false;
+ cache.push_back(Entry(SOLVER_UNDECIDED));
+ symbols.push_back(ASTVec());
+
}
const ASTVec GetAsserts(void)
delete n;
//node_pool.destroy(n);
}
+
+ struct Entry
+ {
+ explicit Entry( SOLVER_RETURN_TYPE result_)
+ {
+ result = result_;
+ }
+
+ SOLVER_RETURN_TYPE result;
+ ASTNode node;
+
+ void print()
+ {
+ if (result == SOLVER_UNSATISFIABLE)
+ cerr << "u";
+ else if (result == SOLVER_SATISFIABLE)
+ cerr << "s";
+ else if (result == SOLVER_UNDECIDED)
+ cerr << "?";
+ }
+ };
+ vector<Entry> cache;
+ vector<vector<ASTNode> > symbols;
+
+ void
+ addSymbol(ASTNode &s)
+ {
+ symbols.back().push_back(s);
+ letMgr._parser_symbol_table.insert(s);
+ }
+
+ void
+ pop()
+ {
+ if (symbols.size() ==0)
+ FatalError("Popping from an empty stack.");
+ if (symbols.size() ==1)
+ FatalError("Can't pop away the default base element.");
+
+ assert(symbols.size() == cache.size());
+ cache.erase(cache.end()-1);
+ ASTVec & current = symbols.back();
+ for (int i=0; i < current.size() ;i++)
+ letMgr._parser_symbol_table.erase(current[i]);
+ symbols.erase(symbols.end()-1);
+ }
+
+ void
+ push()
+ {
+ // If the prior one is unsatisiable then the new one will be too.
+ if (cache.size() > 1 && cache.back().result == SOLVER_UNSATISFIABLE)
+ cache.push_back(Entry(SOLVER_UNSATISFIABLE));
+ else
+ cache.push_back(Entry(SOLVER_UNDECIDED));
+
+ symbols.push_back(ASTVec());
+ assert(symbols.size() == cache.size());
+ }
+
+ void printStatus()
+ {
+ for (int i=0; i < cache.size();i++)
+ {
+ cache[i].print();
+ }
+ cerr<< endl;
+ }
+
+ // Does some simple caching of prior results.
+ void
+ checkSat(vector<ASTVec> & assertionsSMT2)
+ {
+ bm.GetRunTimes()->stop(RunTimes::Parsing);
+ assert(assertionsSMT2.size() == cache.size());
+
+ Entry& cacheEntry = cache.back();
+
+ //cerr << "------------" << endl;
+ //printStatus();
+
+ if ((cacheEntry.result == SOLVER_SATISFIABLE || cacheEntry.result == SOLVER_UNSATISFIABLE)
+ && (assertionsSMT2.back().size() ==1 && assertionsSMT2.back()[0] == cacheEntry.node))
+ { // If we already know the answer then return.
+ if (bm.UserFlags.quick_statistics_flag)
+ {
+ bm.GetRunTimes()->print();
+ }
+
+ (GlobalSTP->tosat)->PrintOutput(cache.back().result);
+ bm.GetRunTimes()->start(RunTimes::Parsing);
+ return;
+ }
+
+ bm.ClearAllTables();
+ GlobalSTP->ClearAllTables();
+
+ // Loop through the set of assertions converting them to single nodes..
+ ASTVec v;
+ for (int i = 0; i < assertionsSMT2.size(); i++)
+ {
+ if (assertionsSMT2[i].size() == 1)
+ {}
+ else if (assertionsSMT2[i].size() == 0)
+ assertionsSMT2[i].push_back(bm.ASTTrue);
+ else
+ {
+ ASTNode v = parserInterface->CreateNode(AND, assertionsSMT2[i]);
+ assertionsSMT2[i].clear();
+ assertionsSMT2[i].push_back(v);
+ }
+ assert(assertionsSMT2[i].size() ==1);
+ v.push_back(assertionsSMT2[i][0]);
+ }
+
+ ASTNode query;
+
+ if (v.size() > 1)
+ query = parserInterface->CreateNode(AND, v);
+ else if (v.size() > 0)
+ query = v[0];
+ else
+ query = bm.ASTTrue;
+
+ SOLVER_RETURN_TYPE last_result = GlobalSTP->TopLevelSTP(query, bm.ASTFalse);
+
+ // Write in the answer to the current slot.
+ if (last_result ==SOLVER_SATISFIABLE || last_result ==SOLVER_UNSATISFIABLE)
+ {
+ Entry e(last_result);
+ e.node = assertionsSMT2.back()[0];
+ cacheEntry = e;
+ assert (!cacheEntry.node.IsNull());
+ }
+
+ // It's satisfiable, so everything beneath it is satisfiable too.
+ if (last_result ==SOLVER_SATISFIABLE)
+ {
+ for (int i=0; i < cache.size(); i++)
+ {
+ assert(cache[i].result != SOLVER_UNSATISFIABLE);
+ cache[i].result = SOLVER_SATISFIABLE;
+ }
+ }
+
+ if (bm.UserFlags.quick_statistics_flag)
+ {
+ bm.GetRunTimes()->print();
+ }
+
+ (GlobalSTP->tosat)->PrintOutput(last_result);
+ //printStatus();
+ bm.GetRunTimes()->start(RunTimes::Parsing);
+ }
+
+ void cleanUp()
+ {
+ letMgr.cleanupParserSymbolTable();
+ cache.clear();
+ symbols.clear();
+ }
};
}
"set-logic" { return LOGIC_TOK; }
"set-info" { return NOTES_TOK; }
"declare-fun" { return DECLARE_FUNCTION_TOK; }
+"push" { return PUSH_TOK;}
+"pop" { return POP_TOK;}
+
/*
"set-option"
"declare-sort"
"define-sort"
- "push"
+
"pop"
*/
"assert" { return FORMULA_TOK; }
}
ASTNode querysmt2;
- ASTVec assertionsSMT2;
- vector<string> commands;
+ vector<ASTVec> assertionsSMT2;
+
#define YYLTYPE_IS_TRIVIAL 1
#define YYMAXDEPTH 104857600
#define YYERROR_VERBOSE 1
%token NOTES_TOK
%token DECLARE_FUNCTION_TOK
%token FORMULA_TOK
+%token PUSH_TOK
+%token POP_TOK
/* Functions for QF_AUFBV. */
%token SELECT_TOK;
%%
cmd: commands END
{
- if(querysmt2.IsNull())
- {
- querysmt2 = parserInterface->CreateNode(FALSE);
- }
-
- if (assertionsSMT2.size() > 1)
- ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(AND,assertionsSMT2));
- else if (assertionsSMT2.size() > 0)
- ((ASTVec*)AssertsQuery)->push_back((assertionsSMT2[0]));
- else
- ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
- ((ASTVec*)AssertsQuery)->push_back(querysmt2);
- parserInterface->letMgr.cleanupParserSymbolTable();
querysmt2 = ASTNode();
assertionsSMT2.clear();
+ parserInterface->cleanUp();
YYACCEPT;
}
;
cmdi:
LPAREN_TOK EXIT_TOK RPAREN_TOK
{
- commands.push_back("exit");
+ querysmt2 = ASTNode();
+ assertionsSMT2.clear();
+ parserInterface->cleanUp();
+ YYACCEPT;
}
| LPAREN_TOK CHECK_SAT_TOK RPAREN_TOK
{
- commands.push_back("check-sat");
+ parserInterface->checkSat(assertionsSMT2);
}
|
LPAREN_TOK LOGIC_TOK STRING_TOK RPAREN_TOK
{}
| LPAREN_TOK NOTES_TOK attribute RPAREN_TOK
{}
+| LPAREN_TOK PUSH_TOK NUMERAL_TOK RPAREN_TOK
+ {
+ for (int i=0; i < $3;i++)
+ {
+ parserInterface->push();
+ assertionsSMT2.push_back(ASTVec());
+ }
+ }
+| LPAREN_TOK POP_TOK NUMERAL_TOK RPAREN_TOK
+ {
+ for (int i=0; i < $3;i++)
+ {
+ parserInterface->pop();
+ assertionsSMT2.erase(assertionsSMT2.end()-1);
+ }
+ }
| LPAREN_TOK DECLARE_FUNCTION_TOK var_decl RPAREN_TOK
{}
| LPAREN_TOK FORMULA_TOK an_formula RPAREN_TOK
{
- assertionsSMT2.push_back(*$3);
+ assertionsSMT2.back().push_back(*$3);
parserInterface->deleteNode($3);
}
;
STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK
{
ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str());
- parserInterface->letMgr._parser_symbol_table.insert(s);
+ parserInterface->addSymbol(s);
//Sort_symbs has the indexwidth/valuewidth. Set those fields in
//var
s.SetIndexWidth(0);
ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str());
s.SetIndexWidth(0);
s.SetValueWidth(0);
- parserInterface->letMgr._parser_symbol_table.insert(s);
+ parserInterface->addSymbol(s);
delete $1;
}
| STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK ARRAY_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK RPAREN_TOK
{
ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str());
- parserInterface->letMgr._parser_symbol_table.insert(s);
+ parserInterface->addSymbol(s);
unsigned int index_len = $9;
unsigned int value_len = $14;
if(index_len > 0) {
projects / francis / stp.git / commitdiff