stp-users

Contact owners and managers

1–30 of 84

Hi,

Welcome to the STP users group.

For more information about the STP Constraint Solver, please visit:

http://sites.google.com/site/stpfastprover/

Thanks & Warm Regards,
Dr. Vijay Ganesh (Project Leader)

0 selected

angel...@gmail.com, … Jonas Wagner5

8/26/14

A question about the addition operation of bit vectors

Hi, I want to avoid such kind of solutions because I'm using the solutions of STP as a test input

unread,

A question about the addition operation of bit vectors

Hi, I want to avoid such kind of solutions because I'm using the solutions of STP as a test input

8/26/14

6/4/14

Any example of c++ interface?

I downloaded the stp project from github, but only found a simple example of c interface. Can anybody

unread,

Any example of c++ interface?

I downloaded the stp project from github, but only found a simple example of c interface. Can anybody

6/4/14

Linus F., Stephen McCamant3

5/16/14

CNF file not created

Thanks for the reply. I answered in the other github forum. Or which of the forums would you

unread,

CNF file not created

Thanks for the reply. I answered in the other github forum. Or which of the forums would you

5/16/14

Jurriaan Bremer, Jonas Wagner2

5/5/14

Quick introduction to my upcoming Python bindings for STP

Hi Jurriaan, I really think this looks exciting and makes it very easy to use the solver. I don't

unread,

Quick introduction to my upcoming Python bindings for STP

Hi Jurriaan, I really think this looks exciting and makes it very easy to use the solver. I don't

5/5/14

5/2/14

[Announcement] STP Shared library now built by default

Hi, Just a small announcement. ``libstp`` can now be built as a shared library in upstream STP and it

unread,

[Announcement] STP Shared library now built by default

Hi, Just a small announcement. ``libstp`` can now be built as a shared library in upstream STP and it

5/2/14

Stefan Kölbl, Stephen McCamant4

4/24/14

Cryptominisat - Update Version

SMcC> In testing one small example a while ago I was able to dump the SMcC> vector of CNF

unread,

Cryptominisat - Update Version

SMcC> In testing one small example a while ago I was able to dump the SMcC> vector of CNF

4/24/14

Manjeet Dahiya, … Khoo Yit Phang4

4/15/14

push/pop context

Hi Manjeet, If I recall correctly, vc_push clears the previous counterexamples and adds a new context

unread,

push/pop context

Hi Manjeet, If I recall correctly, vc_push clears the previous counterexamples and adds a new context

4/15/14

Jon Passki, … Stefan Kölbl3

4/10/14

Iterating in STP to Enumerate All CounterExamples

Hi, I got follow up question on this. If you use this workflow (STP -> CNF -> SAT-Solver) what

unread,

Iterating in STP to Enumerate All CounterExamples

Hi, I got follow up question on this. If you use this workflow (STP -> CNF -> SAT-Solver) what

4/10/14

3/17/14

Fuzzgrind based on STP

Hi All, Following is an interesting tool based on STP: http://esec-lab.sogeti.com/pages/Fuzzgrind Has

unread,

Fuzzgrind based on STP

Hi All, Following is an interesting tool based on STP: http://esec-lab.sogeti.com/pages/Fuzzgrind Has

3/17/14

Dan Liew, Stephen McCamant2

3/17/14

[Announcement] New testing infrastructure for STP

>>>>> "DL" == Dan Liew <delc...@gmail.com> writes: DL> Hi All, DL

unread,

[Announcement] New testing infrastructure for STP

>>>>> "DL" == Dan Liew <delc...@gmail.com> writes: DL> Hi All, DL

3/17/14

Tim King, … Mark Tuttle6

3/17/14

Old flex compile problems

Thanks, Stephen, I did find later versions of flex and bison built in my environment, and I did

unread,

Old flex compile problems

Thanks, Stephen, I did find later versions of flex and bison built in my environment, and I did

3/17/14

Tomasz Kuchta, Vijay Ganesh2

3/3/14

Query complexity estimation

Hi Tomasz, This is a great question. I don't anybody who has done this for SMT solvers in general

unread,

Query complexity estimation

Hi Tomasz, This is a great question. I don't anybody who has done this for SMT solvers in general

3/3/14

angel...@gmail.com, … Stephen McCamant6

2/4/14

questions about the Simplifier of STP

>>>>> "M" == angel haha <angel...@gmail.com> writes: M> Thanks.

unread,

questions about the Simplifier of STP

>>>>> "M" == angel haha <angel...@gmail.com> writes: M> Thanks.

2/4/14

Stephen McCamant, Manjeet Dahiya3

1/16/14

Re: Substitution related query formulation

>>>>> "MD" == Manjeet Dahiya <manjee...@gmail.com> writes: MD>

unread,

Re: Substitution related query formulation

>>>>> "MD" == Manjeet Dahiya <manjee...@gmail.com> writes: MD>

1/16/14

1/12/14

Substitution related query formulation

Hello, I have a boolean fourmula f(a, b, x, y). Where a and b are boolean expressions and x and y are

unread,

Substitution related query formulation

Hello, I have a boolean fourmula f(a, b, x, y). Where a and b are boolean expressions and x and y are

1/12/14

12/5/13

Counterexample about array read

Hi, I'm trying to use stp to my formulas, especially for generating a counterexample. However I

unread,

Counterexample about array read

Hi, I'm trying to use stp to my formulas, especially for generating a counterexample. However I

12/5/13

Ryan Govostes, … Vijay Ganesh4

9/18/13

Proposal: Project migration to GitHub

Hi Greg, STP is distributed under the MIT license. We have very clear licensing of all the sub-

unread,

Proposal: Project migration to GitHub

Hi Greg, STP is distributed under the MIT license. We have very clear licensing of all the sub-

9/18/13

Dan Liew, … Vijay Ganesh4

9/5/13

STP failing to compile on Bison 3.0 (patch included)

Hi All, As Delcypher just mentioned, Ryan Govostes has created an STP repo on Github. This is going

unread,

STP failing to compile on Bison 3.0 (patch included)

Hi All, As Delcypher just mentioned, Ryan Govostes has created an STP repo on Github. This is going

9/5/13

Tomasz Kuchta, Vijay Ganesh3

9/3/13

Multi-threaded STP

Thank you very much for the information. Best regards, Tomasz On Friday, 16 August 2013 18:35:42 UTC+

unread,

Multi-threaded STP

Thank you very much for the information. Best regards, Tomasz On Friday, 16 August 2013 18:35:42 UTC+

9/3/13

8/16/13

Patch for STP's parsers that break with Bison 3.0

Hi, STP's Bison parsers fail to build for the latest Bison (3.0) because a deprecated feature (

unread,

Patch for STP's parsers that break with Bison 3.0

Hi, STP's Bison parsers fail to build for the latest Bison (3.0) because a deprecated feature (

8/16/13

Noomene Ben Henda, … Stephen McCamant6

7/10/13

STP Crash On Start

>>>>> "NBH" == Noomene Ben Henda <noo...@gmail.com> writes: NBH>

unread,

STP Crash On Start

>>>>> "NBH" == Noomene Ben Henda <noo...@gmail.com> writes: NBH>

7/10/13

Edward Schwartz, Ryan Govostes2

4/11/13

smtlib2 parsing bug

It doesn't look like this has yet been checked in. Is anyone reviewing patches on this list? On

unread,

smtlib2 parsing bug

It doesn't look like this has yet been checked in. Is anyone reviewing patches on this list? On

4/11/13

varza victor, Vijay Ganesh3

4/3/13

Transform STP queries into linear equation

Vijay, Thank you for answering me. Do you have documentation or some example of how to use this built

unread,

Transform STP queries into linear equation

Vijay, Thank you for answering me. Do you have documentation or some example of how to use this built

4/3/13

Khoo Yit Phang2

3/4/13

Clear ArrayTransformer::ack_pair between queries

Hi, Ping! Any feedback? For reference, here's my patch: https://bitbucket.org/khooyp/stp-khooyp/

unread,

Clear ArrayTransformer::ack_pair between queries

Hi, Ping! Any feedback? For reference, here's my patch: https://bitbucket.org/khooyp/stp-khooyp/

3/4/13

Jingyue Wu, Trevor Hansen2

2/11/13

Print SBVMOD Nodes

On Saturday, December 8, 2012 2:32:29 AM UTC+11, Jingyue Wu wrote: I enclosed a patch to support

unread,

Print SBVMOD Nodes

On Saturday, December 8, 2012 2:32:29 AM UTC+11, Jingyue Wu wrote: I enclosed a patch to support

2/11/13

Ryan Govostes, Trevor Hansen2

2/11/13

Bad CVC parsing in vc_parseMemExpr in C interface

On Friday, February 8, 2013 1:02:55 PM UTC+11, Ryan Govostes wrote: In the C interface,

unread,

Bad CVC parsing in vc_parseMemExpr in C interface

On Friday, February 8, 2013 1:02:55 PM UTC+11, Ryan Govostes wrote: In the C interface,

2/11/13

2/7/13

Incorrect implementation of vc_sbv(Mod|Rem)Expr in C interface?

In c_interface.cpp, vc_sbvModExpr and vc_sbvRemExpr are defined as follows: Expr vc_sbvModExpr(VC vc,

unread,

Incorrect implementation of vc_sbv(Mod|Rem)Expr in C interface?

In c_interface.cpp, vc_sbvModExpr and vc_sbvRemExpr are defined as follows: Expr vc_sbvModExpr(VC vc,

2/7/13

Jingyue Wu, Vijay Ganesh2

12/8/12

vc_eqExpr two booleans

You will have to use an IFF operator (if and only if operator) to compare two Booleans. -Vijay. On

unread,

vc_eqExpr two booleans

You will have to use an IFF operator (if and only if operator) to compare two Booleans. -Vijay. On

12/8/12

Jonas Wagner, Vijay Ganesh4

11/1/12

Fatal Error: BVConstEvaluator:division by zero error

On Thu, Nov 1, 2012 at 12:17 PM, Jonas Wagner <jonas....@epfl.ch> wrote: > Hello, >

unread,

Fatal Error: BVConstEvaluator:division by zero error

On Thu, Nov 1, 2012 at 12:17 PM, Jonas Wagner <jonas....@epfl.ch> wrote: > Hello, >

11/1/12

EasyQiu, Vijay Ganesh2

8/10/12

minimal unsat core

Hi All, I hope all of you are having a great summer! As some of you are aware, I will start in

unread,

minimal unsat core

Hi All, I hope all of you are having a great summer! As some of you are aware, I will start in

8/10/12

Search

Clear search

Close search

Google apps

Main menu