Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Upgrade scikit learn 0.23.2 #6

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Upgrade scikit learn 0.23.2 #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1608cf8
Upgrade goal_runner to work with z3 version 4.8.7
maciej-bendkowski Sep 28, 2020
675939b
Upgrade to be compatible with python 3.8.
jeremysalwen Nov 27, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 16 additions & 17 deletions fastsmt/cpp/goal_runner.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,9 +42,9 @@ tactic fromString(context& ctx, std::string s) {
return tactic(ctx, s.substr(7, (int)s.size() - 8).c_str());
} else if (s.find("AndThen(") == 0) {
auto tokens = split(s.substr(8, (int)s.size() - 9), ",");

tactic ret = fromString(ctx, tokens[0]);

for (size_t i = 1; i < tokens.size(); ++i) {
auto tactic = fromString(ctx, tokens[i]);
ret = ret & tactic;
Expand Down Expand Up @@ -79,7 +79,7 @@ tactic fromString(context& ctx, std::string s) {
int get_rlimit(solver s) {
auto stats = s.statistics();
auto sz = stats.size();

for (size_t i = 0; i < sz; ++i) {
if (stats.key(i) == "rlimit count") {
return stats.uint_value(i);
Expand All @@ -91,25 +91,24 @@ int get_rlimit(solver s) {

int main(int argc, char* argv[]) {
context ctx;

char* strategy = argv[1];
char* smt_input_file = argv[2];
char* smt_out_file = argv[3];

Z3_ast a = Z3_parse_smtlib2_file(ctx, smt_input_file, 0, 0, 0, 0, 0, 0);
expr f(ctx, a);

tactic t = fromString(ctx, strategy);
try {

auto rlimit_before = get_rlimit(t.mk_solver());
// see https://github.com/Z3Prover/z3/issues/2798
expr f(ctx, mk_and(ctx.parse_file(smt_input_file)));
tactic t = fromString(ctx, strategy);

goal g(ctx);
g.add(f);
auto old_hash = g.as_expr().hash();
auto rlimit_before = get_rlimit(t.mk_solver());

clock_t begin = clock();
goal g(ctx);
g.add(f);
auto old_hash = g.as_expr().hash();

try {
clock_t begin = clock();
apply_result r = t(g);
assert(r.size() == 1); // assert that there is only 1 resulting goal
goal new_goal = r[0];
Expand Down Expand Up @@ -145,7 +144,7 @@ int main(int argc, char* argv[]) {
double elapsed_sec = (double)(end - begin) / CLOCKS_PER_SEC;

std::cout << res << " " << rlimit << " " << old_hash << " " << new_hash << " " << elapsed_sec << std::endl;

std::vector<probe> probes;
probes.push_back(probe(ctx, "num-consts"));
probes.push_back(probe(ctx, "num-exprs"));
Expand All @@ -162,7 +161,7 @@ int main(int argc, char* argv[]) {
probes.push_back(probe(ctx, "num-bv-consts"));
probes.push_back(probe(ctx, "num-arith-consts"));
probes.push_back(probe(ctx, "is-qfbv-eq"));

for (size_t i = 0; i < probes.size(); ++i) {
if (i != 0) {
std::cout << " ";
Expand All @@ -174,6 +173,6 @@ int main(int argc, char* argv[]) {
std::cout << -1 << std::endl;
return 0;
}

return 0;
}
0 fastsmt/cpp/make_z3_4.6.2 → fastsmt/cpp/make_z3_4.8.7
View file
Open in desktop
File renamed without changes.
10 changes: 5 additions & 5 deletions fastsmt/synthesis/search/models.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,12 @@
import time

try:
import fastText
import fasttext
except ImportError:
logging.warn('fastText could not be imported (only needed to run fastText model).')
logging.warn('fasttext could not be imported (only needed to run fasttext model).')

from abc import ABC, abstractmethod
from sklearn.externals import joblib
import joblib

from fastsmt.synthesis.search.dataset import *
from fastsmt.utils.strategy import StrategyEnumerator
Expand Down Expand Up @@ -136,7 +136,7 @@ def can_predict(self):
return True

def load_model(self, file):
self.bilinear_model = fastText.load_model(file + '.bin')
self.bilinear_model = fasttext.load_model(file + '.bin')
print('Loaded bilinear model from ',file)

def save_model(self, file):
Expand Down Expand Up @@ -187,7 +187,7 @@ def retrain(self):

self.log.info('Created dataset of %d entries' % len(best_tactic))

self.bilinear_model = fastText.train_supervised(
self.bilinear_model = fasttext.train_supervised(
input=train_file.name,
epoch=self.config['models']['fast_text']['epoch'],
lr=self.config['models']['fast_text']['lr'],
Expand Down
1 change: 1 addition & 0 deletions fastsmt/test/run_tests.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
#!/bin/sh
rm -f test/test_outcome.txt
./cpp/goal_runner "AndThen(With(simplify;blast_distinct=True;elim_and=False;flat=False;hoist_mul=False;local_ctx=True;pull_cheap_ite=True;push_ite_bv=True;som=True),Tactic(qfnra-nlsat),Tactic(sat),With(propagate-values;push_ite_bv=True),Tactic(max-bv-sharing),With(aig;aig_per_assertion=False),Tactic(smt))" test/bench_7150.smt2 test/out.smt2 | head -1 | awk '{ print $1 }' >> test/test_outcome.txt
./cpp/goal_runner "AndThen(With(simplify;blast_distinct=True;elim_and=False;flat=False;hoist_mul=True;local_ctx=False;pull_cheap_ite=True;push_ite_bv=True;som=True),Tactic(purify-arith),With(aig;aig_per_assertion=False),Tactic(elim-uncnstr),Tactic(smt))" test/bench_9849.smt2 test/out.smt2 | head -1 | awk '{ print $1 }' >> test/test_outcome.txt
Expand Down
2 changes: 1 addition & 1 deletion setup.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
install_requires=[
'numpy',
'scipy',
'scikit-learn==0.20',
'scikit-learn',
'torch',
'matplotlib',
'tensorboardX',
Expand Down