using namespace std;
using namespace BEEV;
-// Asynchronously stop solving.
-bool finished = false;
-
// Holds the rewrite that was disproved at the largest bitwidth.
ASTNode highestDisproved;
int highestLevel = 0;
const int mask = (1 << (bits)) - 1;
//////////////////////////////////
+// Set by the signal handler to write out the rules that have been discovered.
+volatile bool force_writeout = false;
+
// Saves a little bit of time. The vectors are saved between invocations.
vector<ASTVec> saved_array;
// Stores the difficulties that have already been generated.
map<ASTNode, int> difficulty_cache;
-Rewrite_system to_write;
+Rewrite_system rewrite_system;
void
clearSAT();
containsNode(const ASTNode& n, const ASTNode& hunting, string& current);
void
-applyRewritesToAll(ASTVec & v);
-
-void
-writeOutRules(string fileName);
+writeOutRules();
int
getDifficulty(const ASTNode& n_);
bool
unifyNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width);
-int
-findNewRewrites();
-
typedef HASHMAP<ASTNode, string, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeString;
BEEV::STPMgr* mgr;
assert(symbols.size() > 0);
// Both of them might not be contained in the assignment.
- different.setV(mgr->CreateBVConst(symbols[0].GetValueWidth(), 0));
- different.setW(mgr->CreateBVConst(symbols[0].GetValueWidth(), 0));
+ different.setV(mgr->CreateZeroConst(symbols[0].GetValueWidth()));
+ different.setW(mgr->CreateZeroConst(symbols[0].GetValueWidth()));
// It might have been widened.
for (int i = 0; i < symbols.size(); i++)
}
}
+void do_write_out(int ignore)
+{
+ force_writeout = true;
+}
+
+
int
startup()
{
mgr->UserFlags.stats_flag = false;
mgr->UserFlags.optimize_flag = true;
- ss = new MinisatCore<Minisat::Solver>(finished);
+ ss = new MinisatCore<Minisat::Solver>(mgr->soft_timeout_expired);
// Prime the cache with 100..
for (int i = 0; i < 100; i++)
// w = mgr->LookupOrCreateSymbol("w");
// w.SetValueWidth(bits);
+ // Write out the work so far..
+ signal(SIGUSR1,do_write_out);
}
clearSAT()
{
delete ss;
- ss = new MinisatCore<Minisat::Solver>(finished);
+ ss = new MinisatCore<Minisat::Solver>(mgr->soft_timeout_expired);
}
// Return true if the negation of the query is unsatisfiable.
isConstantToSat(const ASTNode & query)
{
assert(query.GetType() == BOOLEAN_TYPE);
- cout << "to";
GlobalSTP->ClearAllTables();
clearSAT();
SOLVER_RETURN_TYPE r = GlobalSTP->Ctr_Example->CallSAT_ResultCheck(*ss, query2, query2, GlobalSTP->tosat, false);
- cout << "from";
return (r == SOLVER_VALID); // unsat, always true
}
}
cout << '\n' << "depth:" << depth << ", size:" << expressions.size() << " values:" << values.size() << " found: "
- << to_write.size() << '\n';
+ << rewrite_system.size() << " done:" << discarded << "\n";
assert(expressions.size() >0);
continue;
// nb. I haven't rebuilt the map, it's done by writeOutRules().
- equiv[i] == to_write.rewriteNode(equiv[i]);
+ equiv[i] == rewrite_system.rewriteNode(equiv[i]);
for (int j = i + 1; j < equiv.size(); j++) /// commutative so skip some.
{
if (equiv[i].GetKind() == UNDEFINED || equiv[j].GetKind() == UNDEFINED)
continue;
- equiv[j] = to_write.rewriteNode(equiv[j]);
+ equiv[j] = rewrite_system.rewriteNode(equiv[j]);
ASTNode from = equiv[i];
ASTNode to = equiv[j];
cout << to;
cout << getDifficulty(from) << " to " << getDifficulty(to) << endl;
cout << "After rewriting";
- cout << to_write.rewriteNode(from);
- cout << to_write.rewriteNode(to);
+ cout << rewrite_system.rewriteNode(from);
+ cout << rewrite_system.rewriteNode(to);
cout << "------";
- to_write.push_back(Rewrite_rule(mgr, from, to, getCurrentTime() - st));
+ Rewrite_rule rr(mgr, from, to, getCurrentTime() - st);
+
+ if (!rr.timedCheck(10000))
+ continue;
+
+ rewrite_system.push_back(rr);
// Remove the more difficult expression.
if (from == equiv[i])
}
// Write out the rules intermitently.
- if (lastOutput + 5000 < to_write.size())
+ if (force_writeout || lastOutput + 5000 < rewrite_system.size())
{
- writeOutRules("array.smt2");
- lastOutput = to_write.size();
+ rewrite_system.rewriteAll();
+ writeOutRules();
+ lastOutput = rewrite_system.size();
}
}
}
+ discarded += expressions.size();
}
// Converts the node into an IF statement that matches the node.
return ss.str();
}
-// Write out all the rules that have been discovered to file.
+// Write out all the rules that have been discovered to various files in different formats.
void
-writeOutRules(string fileName)
+writeOutRules()
{
- to_write.rewriteAll();
+ force_writeout = false;
std::vector<string> output;
std::map<string, Rewrite_rule> dup;
- for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++)
+ for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++)
{
if (!it->isOK())
{
- to_write.erase(it--);
+ rewrite_system.erase(it--);
continue;
}
ASTNodeMap fromTo;
+ cerr << f;
f = renameVars(f);
//cerr << "renamed" << f;
bool result = unifyNode(f,dup.find(sofar)->second.getFrom(),fromTo,2) ;
cout << rewrite(f,*it,seen );
// The text of this rule is the same as another rule.
- to_write.erase(it--);
+ rewrite_system.erase(it--);
continue;
}
else
// Remove the duplicates from output.
removeDuplicates(output);
- cout << "Rules Discovered in total: " << to_write.size() << endl;
+ cout << "Rules Discovered in total: " << rewrite_system.size() << endl;
// Group functions of the same kind all together.
hash_map<string, vector<string>, hashF<std::string> > buckets;
}
outputFile.close();
- ofstream outputFileSMT2;
- outputFileSMT2.open("rewrite_data.smt2", ios::trunc);
-
- for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++)
- {
- assert(it->isOK());
- outputFileSMT2 << "; " << "bits:" << bits << "->" << widen_to << " time to verify:" << it->getTime()
- << '\n';
- for (int j = widen_to; j < widen_to + 5; j++)
- {
- ASTNode widened = widen(it->getN(),j);
- outputFileSMT2 << "(push 1)\n";
- printer::SMTLIB2_PrintBack(outputFileSMT2, mgr->CreateNode(NOT, widened), true, false);
- outputFileSMT2 << "(pop 1)\n";
- }
- }
-
- outputFileSMT2.close();
+ ///////////////
+ outputFile.open("rules_new.smt2", ios::trunc);
+ for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++)
+ {
+ it->writeOut(outputFile);
+ }
+ outputFile.close();
- outputFileSMT2.open(fileName.c_str(), ios::trunc);
+ /////////////////
+ outputFile.open("array.smt2", ios::trunc);
ASTVec v;
- for (Rewrite_system::RewriteRuleContainer::iterator it = to_write.toWrite.begin() ; it != to_write.toWrite.end(); it++)
+ for (Rewrite_system::RewriteRuleContainer::iterator it = rewrite_system.toWrite.begin() ; it != rewrite_system.toWrite.end(); it++)
{
v.push_back(it->getN());
}
if (v.size() > 0)
{
ASTNode n = mgr->CreateNode(AND, v);
- printer::SMTLIB2_PrintBack(outputFileSMT2, n, true);
+ printer::SMTLIB2_PrintBack(outputFile, n, true);
}
- outputFileSMT2.close();
+ outputFile.close();
}
vector<Rewrite_rule>& rr =
n[0].Degree() > 0 ?
- (to_write.kind_kind_to_rr[n.GetKind()][n[0].GetKind()]) :
- (to_write.kind_to_rr[n.GetKind()]) ;
+ (rewrite_system.kind_kind_to_rr[n.GetKind()][n[0].GetKind()]) :
+ (rewrite_system.kind_to_rr[n.GetKind()]) ;
for (int i = 0; i < rr.size(); i++)
return n2;
}
+int smt2_scan_string(const char *yy_str);
+
+void
+loadNewRules()
+{
+ string fileName = "rules_new.smt2";
+
+ if(!ifstream(fileName.c_str()))
+ return; // file doesn't exist.
+
+ FILE * in = fopen(fileName.c_str(), "r");
+
+ TypeChecker nfTypeCheckDefault(*mgr->hashingNodeFactory, *mgr);
+ Cpp_interface piTypeCheckDefault(*mgr, &nfTypeCheckDefault);
+ mgr->UserFlags.print_STPinput_back_SMTLIB2_flag = true;
+ parserInterface = &piTypeCheckDefault;
+
+
+ // This file I/O code: 1) Is terrible 2) I'm in a big rush so just getting it working 3) am embarised by it.
+ while (!feof(in))
+ {
+ int id, verified_to_bits, time_used, from_v, to_v;
+
+ string s;
+ char line [63000];
+
+ bool first = true;
+ bool done = false;
+ while (true)
+ {
+ fgets ( line, sizeof line, in );
+ if (first)
+ {
+ int rv = sscanf(line, ";id:%d\tverified_to:%d\ttime:%d\tfrom_difficulty:%d\tto_difficulty:%d\n", &id, &verified_to_bits, &time_used, &from_v, &to_v);
+ if (rv !=5)
+ {
+ done = true;
+ break;
+ }
+ first = false;
+ continue;
+ }
+ s+= line;
+ if (!strcmp(line,"(exit)\n"))
+ break;
+ }
+ if (done)
+ break;
+
+ mgr->GetRunTimes()->start(RunTimes::Parsing);
+
+ // Load it into a string because other wise the parser reads in big blocks way past where we want it to.
+ smt2_scan_string(s.c_str());
+ smt2parse();
+ ASTVec values = piTypeCheckDefault.GetAsserts();
+ values = FlattenKind(AND, values);
+
+ assert(values.size() ==1);
+
+ ASTNode from = values[0][0];
+ ASTNode to = values[0][1];
+
+ // Rule should be orderable.
+ bool ok = orderEquivalence(from, to);
+ if (!ok)
+ {
+ cout << "discarding rule that can't be ordered";
+ cout << from << to;
+ cout << "----";
+ continue;
+ }
+
+ Rewrite_rule r(mgr, from, to, 0, id);
+ r.setVerified(verified_to_bits,time_used);
+
+ assert(r.isOK());
+ rewrite_system.push_back(r);
+
+ mgr->PopQuery();
+ parserInterface->popToFirstLevel();
+ //parserInterface->cleanUp();
+ }
+ //fclose(smt2in);
+
+ cout << "New Style Rules Loaded:" << rewrite_system.size() << endl;
+}
+
+//read from stdin, then tests it until the timeout.
+void
+testIndividualRule(int timeout_ms)
+{
+ int id, verified_to_bits, time_used, from_v, to_v;
+ scanf(";id:%d\tverified_to:%d\ttime:%d\tfrom_difficulty:%d\tto_difficulty:%d\n", &id, &verified_to_bits, &time_used, &from_v, &to_v);
+
+ TypeChecker nfTypeCheckDefault(*mgr->hashingNodeFactory, *mgr);
+ Cpp_interface piTypeCheckDefault(*mgr, &nfTypeCheckDefault);
+
+ mgr->UserFlags.print_STPinput_back_SMTLIB2_flag = true;
+
+ parserInterface = &piTypeCheckDefault;
+ mgr->GetRunTimes()->start(RunTimes::Parsing);
+ smt2parse();
+ ASTVec values = piTypeCheckDefault.GetAsserts();
+ values = FlattenKind(AND, values);
+
+ assert(values.size() ==1);
+ if ((values[0].GetKind() != EQ))
+ {
+ cout << "Not equality??";
+ cout << values[0];
+ return;
+ }
+
+ ASTNode from = values[0][0];
+ ASTNode to = values[0][1];
+
+ // Rule should be orderable.
+ bool ok = orderEquivalence(from, to);
+ if (!ok)
+ {
+ cout << "discarding rule that can't be ordered";
+ cout << from << to;
+ cout << "----";
+ return;
+ }
+
+ Rewrite_rule r(mgr, from, to, 0, id);
+ r.setVerified(verified_to_bits,time_used);
+
+ assert(r.isOK());
+ rewrite_system.push_back(r);
+
+ mgr->PopQuery();
+ parserInterface->popToFirstLevel();
+ parserInterface->cleanUp();
+
+
+ if (r.timedCheck(timeout_ms))
+ r.writeOut(cout); // omit failed.
+}
+
// loads the already existing rules.
void loadExistingRules(string fileName)
{
bool ok = orderEquivalence(from, to);
if (!ok)
{
- cout << "discarding rule that can't be ordere";
+ cout << "discarding rule that can't be ordered";
+ cout << from << to;
+ cout << "----";
continue;
}
Rewrite_rule r(mgr, from, to, 0);
if (r.isOK());
- to_write.push_back(r);
+ rewrite_system.push_back(r);
}
mgr->PopQuery();
parserInterface->popToFirstLevel();
parserInterface->cleanUp();
- to_write.buildLookupTable();
+ rewrite_system.buildLookupTable();
ASTVec vvv = mgr->GetAsserts();
for (int i=0; i < vvv.size() ;i++)
cout << vvv[i];
// So we don't output as soon as one is discovered...
- lastOutput = to_write.size();
+ lastOutput = rewrite_system.size();
}
void
w0 = mgr->LookupOrCreateSymbol("w0");
w0.SetValueWidth(bits);
- writeOutRules("test-2.smt2");
- to_write.verifyAllwithSAT();
- to_write.clear();
+ writeOutRules();
+ rewrite_system.verifyAllwithSAT();
+ rewrite_system.clear();
}
-int
-main()
+void
+createVariables()
{
- startup();
- //test();
- //exit(1);
-
- loadExistingRules("array.smt2");
-
v = mgr->LookupOrCreateSymbol("v");
v.SetValueWidth(bits);
w0 = mgr->LookupOrCreateSymbol("w0");
w0.SetValueWidth(bits);
-
- testProps();
-
- findNewRewrites();
- writeOutRules("array.smt2");
- to_write.verifyAllwithSAT();
- writeOutRules("array-with-times.smt2"); // verifyingallwithsat gives us the times..
}
int
-findNewRewrites()
+main(int argc, const char* argv[])
{
- to_write.buildLookupTable();
+ startup();
+
+ if (argc == 1) // Read the current rule set, find new rules.
+ {
+ loadExistingRules("array.smt2");
+ createVariables();
+ ////////////
+ rewrite_system.buildLookupTable();
+
+ Function_list functionList;
+ functionList.buildAll();
- Function_list functionList;
- functionList.buildAll();
+ // The hash is generated on these values.
+ vector<VariableAssignment> values;
+ findRewrites(functionList.functions, values);
- // The hash is generated on these values.
- vector<VariableAssignment> values;
- findRewrites(functionList.functions, values);
+ cout << "Initial:" << bits << " widening to :" << widen_to << endl;
+ cout << "Highest disproved @ level: " << highestLevel << endl;
+ cout << highestDisproved << endl;
+ ////////////
- cout << "Initial:" << bits << " widening to :" << widen_to << endl;
- cout << "Highest disproved @ level: " << highestLevel << endl;
- cout << highestDisproved << endl;
- return 0;
+ rewrite_system.rewriteAll();
+ writeOutRules();
+ }
+ else if (argc == 3 && !strcmp("verify-single",argv[1]))
+ {
+ int timeout_ms = atoi(argv[2]);
+ assert(timeout_ms > 0);
+ testIndividualRule(timeout_ms);
+ }
+ else if (argc == 2 && !strcmp("verify-all",argv[1]))
+ {
+ loadNewRules();
+ createVariables();
+ rewrite_system.verifyAllwithSAT();
+ writeOutRules(); // have the times now..
+ }
+ else if (argc == 2 && !strcmp("write-out",argv[1]))
+ {
+ loadNewRules();
+ createVariables();
+ rewrite_system.rewriteAll();
+ writeOutRules(); // have the times now..
+ }
+ else if (argc == 2 && !strcmp("test",argv[1]))
+ {
+ testProps();
+ }
+ else if (argc == 2 && !strcmp("delete-failed",argv[1]))
+ {
+ loadNewRules();
+ ifstream fin;
+ fin.open("failed.txt",ios::in);
+ char line[256];
+ while (!fin.eof())
+ {
+ fin.getline(line,256);
+ int id;
+ sscanf(line,"FAILED:%d",&id);
+ //cerr << "Failed id: " << id << endl;
+ rewrite_system.deleteID(id);
+ }
+ createVariables();
+ writeOutRules();
+ }
}
+
// Term variables have a specified width!!!
bool
unifyNode(const ASTNode& n0, const ASTNode& n1, ASTNodeMap& fromTo, const int term_variable_width)
ASTNode
widen(const ASTNode& w, int width);
+int
+getDifficulty(const ASTNode& n_);
+
+void soft_time_out(int ignored)
+{
+ mgr->soft_timeout_expired = true;
+}
+
+bool
+isConstant(const ASTNode& n, VariableAssignment& different);
+
+
vector<ASTNode>
getVariables(const ASTNode& n);
ASTNode to;
ASTNode n;
- int id;
+ int id;
+ static int static_id;
- static int static_id;
+ int time_to_verify;
+ int verified_to_bits;
public:
- int time;
+ void writeOut(ostream& outputFileSMT2)
+ {
+ assert(isOK());
+ outputFileSMT2 << ";id:" << getId()
+ << "\tverified_to:" << verified_to_bits << "\ttime:" << getTime()
+ << "\tfrom_difficulty:" << getDifficulty(getFrom())
+ << "\tto_difficulty:" << getDifficulty(getTo())
+ << "\n";
+ outputFileSMT2 << "(push 1)" << endl;
+ printer::SMTLIB2_PrintBack(outputFileSMT2, getN(), true, false);
+ outputFileSMT2 << "(exit)" << endl;
+ }
+
+ // If we've verified it to bigger than before. Then store the bit / time.
+ void
+ setVerified(int bits_, int time_)
+ {
+ if (bits_ > verified_to_bits)
+ {
+ verified_to_bits = bits_;
+ time_to_verify = time_;
+ }
+ }
+
+ int
+ getVerifiedToBits()
+ {
+ return verified_to_bits;
+ }
const ASTNode&
getFrom() const
int
getTime() const
- {return time;}
+ {return time_to_verify;}
ASTNode
getN() const
return n;
}
+ int
+ getId() const
+ {
+ return id;
+ }
+
bool
sameID(const Rewrite_rule& t) const
{
+ return (*this == t);
+
if (id == t.id)
{
assert(n == t.n);
}
- Rewrite_rule(BEEV::STPMgr* bm, const BEEV::ASTNode& from_, const BEEV::ASTNode& to_, const int t)
+ Rewrite_rule(BEEV::STPMgr* bm, const BEEV::ASTNode& from_, const BEEV::ASTNode& to_, const int t, int _id=-1)
: from(from_), to(to_)
{
- id = static_id++;
- time = t;
+ if (_id ==-1)
+ id = static_id++;
+ else
+ {
+ id =_id; // relied on to be unique. So be careful.
+ static_id =id+1; // assuming we are loading them all up..
+ }
+ verified_to_bits = 0;
+ time_to_verify = t;
ASTVec c;
c.push_back(to_);
{
return (n < t.n);
}
+
+ // Tests for the timeout amount of time. FALSE if a bad instance was found. Otherwise true.
+ bool
+ timedCheck(int timeout_ms)
+ {
+ VariableAssignment assignment;
+
+ mgr->soft_timeout_expired = false;
+ itimerval timeout;
+ signal(SIGVTALRM, soft_time_out);
+ timeout.it_interval.tv_usec = 0;
+ timeout.it_interval.tv_sec = 0;
+ timeout.it_value.tv_usec = 1000 * (timeout_ms % 1000);
+ timeout.it_value.tv_sec = timeout_ms / 1000;
+ setitimer(ITIMER_VIRTUAL, &timeout, NULL);
+
+ const int st = getCurrentTime();
+ int checked_to = 0;
+
+ // Start it verifying where we left off..
+ for (int i = std::max(bits, getVerifiedToBits() + 1); i < 1024; i++)
+ {
+ //cout << i << " ";
+ ASTVec children;
+ children.push_back(from);
+ children.push_back(to);
+
+ const ASTNode n = mgr->hashingNodeFactory->CreateNode(EQ, children);
+ const ASTNode& widened = widen(n, i);
+ if (widened == mgr->ASTUndefined)
+ {
+ cout << "cannot widen";
+ cerr << from << to;
+ }
+
+ bool result = isConstant(widened, assignment);
+ if (!result && !mgr->soft_timeout_expired)
+ {
+ // not a constant, and not timed out!
+ cerr << "FAILED:" << getId() << endl << i << from << to;
+ writeOut(cerr);
+ return false;
+ }
+ if (mgr->soft_timeout_expired)
+ break;
+
+ checked_to = i;
+ }
+
+ if (getVerifiedToBits() <= checked_to)
+ setVerified(checked_to, getTime() + (getCurrentTime() - st));
+
+ return true;
+ }
+
};
#endif
projects / francis / stp.git / commitdiff