StackRating

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

Leonardo de Moura

Rating
1523.82 (25,453rd)
Reputation
18,594 (7,475th)
Page: 1 2 3 ... 9
Title Δ
Bit vector expression extension in Z3 0.00
Setting the monomial degree in z3py 0.00
Adding contraints on functions in Z3 0.00
How to estimate time spent in SAT solving part in z3 for SMT? 0.00
How to implement a custom simplify tactic in Z3? 0.00
Which techniques are used to handle Non-linear Integer Real problem... 0.00
Does z3's SAT solver obtain a complete assignment before doing a th... 0.00
Is the DPLL(T)-style SMT solving in z3 documented for Linear Real A... 0.00
How to prove that the Z3 group satisfies the associative law using... 0.00
Tactic to use soft constraints/assumptions only after a time-out? 0.00
How to compute with Inductive datatypes using Yices and Z3-SMT-LIB 0.00
How to use Z3 and CVC4 with SMT -LIB to prove theorems for the dihe... +0.44
How to use Z3 SMT-LIB to prove theorems for the group D3 0.00
How to use Z3 SMT-LIB to solve equations in the Klein Group 0.00
How to use Z3 SMT-LIB to obtain representations of the groups Z3 an... 0.00
Use of context in C++ API 0.00
Where can i get z3py tutorials 0.00
Bug in Z3 JAVA-API to set timeout 0.00
Transform java boolean expressions to SMTlib -0.27
Z3 times out on (presumably) decidable logic 0.00
I want to know whether Z3 supports that a input file includes an an... 0.00
z3py on rise4fun unavailable since several weeks -0.03
declare-fun vs declare-const in SMT2 0.00
Z3py: print large formula with 144 variables 0.00
Can options change `sat` into `unsat`? 0.00
Z3py: Convert a Z3 formula to clauses used by picosat 0.00
Inserting a comment string in Z3 0.00
z3py: assumptions from (check-sat ...) statement 0.00
z3 existential theory of the reals 0.00
How to use Z3 SMT-LIB online to solve problems with Operational Amp... 0.00
Is there a way to use Z3 to get models for constraints involving se... 0.00
mapping user-defined functions in z3 -0.03
Getting Memory Consumption using C API in Z3 Solver 0.00
How to use Z3 on formulas with quantifiers over sets? 0.00
old vs new version of Z3 0.00
Variable elimination in Z3 0.00
Is there a way to use Z3 to get models for constraints involving se... 0.00
Z3: Offering random solutions in solving 0.00
Z3 strategy for solving system with conditional integer additions 0.00
How can I solve minimizing constraint in Z3? 0.00
SyntaxError: invalid syntax while building z3 0.00
Incremental solving in Z3 using push command 0.00
What parts of the Z3 C++ API are still supported? 0.00
Why is * with numeral argument not flattened by simplify? 0.00
Z3 supports for nonlinear arithmetics 0.00
How to model signed integer with BitVector? -0.27
z3 numerical constraints: which is better? 0.00
Custom theory solver for order theory? 0.00
Array expr creation using the C++ API 0.00
How to get an index of a variable from func_interpr entry? 0.00