StackRating

An Elo-based rating system for Stack Overflow
Home   |   About   |   Stats and Analysis   |   Get a Badge
Rating Stats for

Juan Ospina

Rating
1470.28 (4,519,239th) 		Reputation
962 (159,852nd)
Page: 1 2
Title Δ
How to eliminate parenthesis in algebraic expressions using Lean -3.66
quantifier elimination in z3 0.00
Using Z3 and SMT-LIB to find highest palindromic product 0.00
Using Z3 and SMT-LIB to find highest palindromic product 0.00
How to build an inductive type for cobordisms using Coq? +0.35
Distinct Array values in z3 SMT solver 0.00
Z3 is not able to prove the equivalence between two simple programs... -4.00
Z3 is not able to prove the equivalence between two simple programs... +4.00
Why does 0 = 0.5? -3.76
how can I change get-model or get-value output to print decimals in... 0.00
Z3 in place of CVC3 +0.26
Why does Z3 give no response on the following input? +0.25
Z3 Sudoku Solver 0.00
Obtaining symbolic values using Z3 0.00
Checking satisfiability for matrix valued function 0.00
How can I write a long smt-lib expression with an existential quant... 0.00
z3 simplify to polynomial form 0.00
Z3 timeout after replacement of uninterpreted sort to Int 0.00
How to produce the model for partial orders? 0.00
Is this expression really unsat? +4.30
How to make z3 recognize equivalence of certain arithmetic expressi... 0.00
How to make bounded inductive proof of a certain general theorem in... 0.00
Z3 is not able to prove the right-cancellation property in group th... -3.59
Sort name issue in Z3 -3.81
How to define a matrix? 0.00
Problems of Z3 (version 4.3): Output of Real value is not round aut... 0.00
error asserting datatype of datatype in z3 0.00
How to explain Z3's behavior when solving the following Horn clauses? 0.00
How to explain Z3's behavior when solving the following Horn clauses? 0.00
How to use Z3 and CVC4 with SMT -LIB to prove theorems for the dihe... -3.54
Using iZ3 for bit vector operations +0.19
Defining injective functions in Z3 0.00
Defining injective functions in Z3 0.00
What is the state-of-the-art solver for quantifier elimination unde... 0.00
Z3 solve-eq how to use 0.00
Converting to "set-option" SMTLib format +0.34
obtain the integer from a model after s.get_model() -1.78
How to use Z3Py online to compute Ro in a population with heterogen... 0.00
How to perform quantifier elimination using Z3Py and an idea from T... 0.00
How to perform quantifier elimination using Z3Py and an idea from T... 0.00
How to perform quantifier elimination using Python API of Z3 -1.93
How to perform quantifier elimination using Python API of Z3 -1.93
It is possible to compute the Kauffman bracket using Z3py? -3.78
simplification of conjunction of inequalities in z3 0.00
Dose z3 find all satifiable models 0.00
z3py expression simplification 0.00
z3py expression simplification 0.00
3-sat and Tutte polynomial +4.00
3-sat and Tutte polynomial -4.00
Simplify terms using SMT -3.92