Skip to content

Instantly share code, notes, and snippets.

ashiato45 ashiato45

View GitHub Profile
View qfbv.smt
(set-logic QF_BV)
(set-option :produce-models true)
(declare-const x (_ BitVec 3))
(declare-const y (_ BitVec 3))
(define-fun A0 () Bool (bvule (bvadd x y) (_ bv3 3))) ; the number 3 in the bitvector of width 3
(assert A0)
(check-sat)
(get-model)
View test.smt
;; activate interpolation
(set-option :produce-interpolants true)
(set-logic QF_LIA)
(declare-sort U 0)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(define-fun A1 () Bool (= y (* 2 x)))
View msat.py
# Copyright 2014 Andrea Micheli and Marco Gario
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
View settest.py
class C:
def __init__(self, x):
self.x = x
def __eq__(self, y): # crucial!
return self.x == y.x
def __hash__(self):
return hash(self.x)
x = set()
a = C(2)
@ashiato45
ashiato45 / test.yml
Last active Feb 6, 2019
Install pyenv and install modules by pip-module
View test.yml
---
- hosts: all
remote_user: ubuntu
tasks:
- name: sync
synchronize:
src: .
dest: /home/ubuntu
- name: loadpyenv
git:
View generator_of_Zp.py
def print_in_p(n, p):
x = 1
while x <= n:
x *= p
d = []
while x != 1:
x = x//p
View vagrant-getip
#! /bin/sh
vagrant ssh -c "curl http://inet-ip.info/ip" $1 2>/dev/null
echo
@ashiato45
ashiato45 / main.cpp
Last active Oct 21, 2018
Macro to write 10eN for competitive programming
View main.cpp
constexpr int ORD(int n){
int res = 1;
for(int i=0; i < n; i++){
res *= 10;
}
res++;
return res;
}
@ashiato45
ashiato45 / main.cpp
Created Oct 21, 2018
Finding second maximum using std::set, for_each, custom ordering
View main.cpp
auto cmp = [](int a, int b){return a > b;};
set<int, decltype(cmp)> s(cmp);
for_each(evens, evens + 100001, [&](int n){s.insert(n);});
int num_secondpop_evens = 0;
if(s.size() > 1){
num_secondpop_evens = *(++s.begin());
}
@ashiato45
ashiato45 / README.md
Last active Oct 19, 2018
Rank minimization using Nuclear norm optimization for python3 using CVXOPT
View README.md

This is a small modification of [http://cvxopt.org/applications/nucnrm/] for Python3 & CVXOPT. As the comment says, this program was originally written by Z. Liu and L. Vandenberghe, and it distributed under GPL.

You can’t perform that action at this time.