smt Questions
2
Solved
I'm looking at doing some verification work where I've got regular tree grammars as an underlying theory.
Z3 lets you define your own stuff with uninterpreted functions, but that doesn't tend to w...
Verlaverlee asked 1/10, 2017 at 3:18
2
Solved
I am trying to retrieve all possible models for some first-order theory using Z3, an SMT solver developed by Microsoft Research. Here is a minimal working example:
(declare-const f Bool)
(assert (...
Seadon asked 15/11, 2012 at 10:18
2
Solved
I'd like to use Z3 to solve problems that are most naturally expressed in terms of atoms (symbols), sets, predicates, and first order logic. For example (in pseudocode):
A = {a1, a2, a3, ...} # A i...
Studied asked 17/10, 2021 at 18:11
3
I am trying to express the sum of the range of an unbounded Array in z3. For instance in Python:
IntArray = ArraySort(IntSort(), IntSort())
sum = Function('sum', IntArray, IntSort())
........
...
1
Solved
Recently I am learning SMT solver. Although SMT solver is a new concept to me, it reminds me of logic programming, e.g. Prolog and minikanren. So I tried a classic example of logic programming in S...
Garland asked 20/7, 2021 at 6:58
3
Is there a way to run Z3 solver from javascript? Or is there a better SMT solver that I can be used in JavaScript?
Prowel asked 28/9, 2015 at 13:47
0
What are the main differences between an SMT solver, like CVC4, and Prolog? Can one do something the other cannot?
My plan is to produce queries using R, send them to an SMT solver, and to modify ...
1
Solved
I am writing to inquire the theory/algorithm behind the Z3 Optimize function, especially for its maximum and minimum function. This seems pretty magic to me. Is it somehow a binary search or so? Ho...
1
Solved
I wrote an application in Haskell that calls Z3 solver to solve constrains with some complex formulas. Thanks to Haskell I can quickly switch the data type I'm working with.
When using SBV's AlgRe...
1
Solved
I'm using Z3 to solve the Eight Queens puzzle. I know that each queen can be represented by a single integer in this problem. But, when I represent a queen by two integers as following:
from z3 im...
1
Solved
I would like to prove properties of expressions involving matrices and vectors (potentially large size, but size is fixed).
For example I want to prove that the outcome of an expression is a diag...
Gearhart asked 7/11, 2017 at 18:56
0
Monadic First Order Logic, where all predicates take exactly one argument, is a known decidable fragment of first order logic. Testing whether a formula is satisfiable in this logic is decidable, a...
Feinberg asked 7/11, 2017 at 6:37
2
Solved
Recently, I started to study formal verification techniques. In literature, model checker and solver are used somehow interchangeably.
But, how model checker and solver are connected with each othe...
Domineering asked 11/5, 2017 at 7:16
1
Is there an incremental SMT solver or an API for some incremental SMT solver where I can add constraints incrementally, where I can uniquely identify each constraint by some label/name?
The reaso...
Monogenic asked 4/6, 2017 at 16:31
1
Solved
How to convert a simple while loop(c- code) to smt2 language or z3?
For ex :
int x,a;
while(x > 10 && x < 100){
a = x + a;
x++;
}
1
Solved
I have a question regarding how Z3 incrementally solves problems. After reading through some answers here, I found the following:
There are two ways to use Z3 for incremental solving: one is push...
2
Solved
Is there a complete listing of all theories/logics that z3 supports? I have consulted this SMTLIB Tutorial which provides a number of logics, but I do not believe that the list is exhaustive. The z...
1
Solved
Let say that I have some formulas that can be sat but I want to get the smaller (or larger) possible value so sat that formula.
Is there a way to tell the SMT solver to give that kind of small so...
1
Solved
I'm trying to represent temporal constraints in SMT-LIB in order to check their satisfiability. I'm looking for feedback on the direction I'm taking. I'm relatively new to SMT-LIB and I'll highly a...
1
Solved
I have a simple example in nonlinear integer arithmetic, namely a search for Pythagorean triples. Based on what I read in related questions (see below), I'd expect Z3 to find a solution to this pro...
0
Sorry that this question is subjective, but given that the Stack Overflow has the largest Z3 user base, I want to give it a try.
I have a big constraint satisfaction problem that consists of...
1
Solved
Let's say I have a z3 solver with a certain number of asserted constraints that are satisfiable. Let S be a set of constraints, I would like to verify for every constraint in S whether the formula ...
Ptolemaic asked 14/6, 2015 at 11:4
1
Solved
Does the Hyper Threading allow to use of L1-cache to exchange the data between the two threads, which are executed simultaneously on a single physical core, but in two virtual cores?
With the prov...
Pankey asked 6/1, 2015 at 11:12
2
Solved
How can I get a random propositional formula in haskell? Preferably I need the formula in CNF, but I would
I want to use the formulas for performance testing that also involves SAT solvers. Please...
Wit asked 30/4, 2014 at 0:23
2
Solved
I want to parse a String that depicts a propositional formula and then find all models of the propositional formula with a SAT solver.
Now I can parse a propositional formula with the hatt package...
Novobiocin asked 23/4, 2014 at 2:55
1 Next >
© 2022 - 2024 — McMap. All rights reserved.