push/pop context

[Manjeet Dahiya]

Hello,

I'm facing problem with pushing and popping of context.

Here is a small piece of code where push and pop are not working as desired.

  let vc = create_validity_checker () in

  let a = fresh_var vc "a" in

  print_endline (to_string (e_simplify vc a));

  Libstp.vc_push vc;

  query vc a;

  Libstp.vc_pop vc;

  print_endline (to_string (e_simplify vc a));

I expect the second print to be "a" but I get "FALSE". Is the way I have used push/pop incorrect or my understanding is wrong? Please help me with it.

Thanks,

Manjeet Dahiya
http://manjeetdahiya.com

[Delcypher]

It looks likes you are using OCaml bindings to STP. I know nothing
about OCaml and nothing about these bindings.

However my expectation is that the pushing and popping of context is
for pushing and popping assertions made (possibly introduced variables
too, I'm not really sure) and not simplifications applied to
expressions. If I look at the comment by the vc_simplify(VC vc, Expr
e) C interface function (which I expect the OCaml bindings call) I see
"Simplify e with respect to the current context". That suggests to me
that simplification is not part of the context so once an expression
is simplified it is permanent.

> --
>
> ---
> You received this message because you are subscribed to the Google Groups
> "stp-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to stp-users+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Manjeet Dahiya]

Hello Group,

Could somebody please help me understand the semantics of vc_push and vc_pop. I'm all mixed up, would like to know briefly what the context is and what exactly it stores.

My goal is to make multiple queries in my program. So exactly at what point should I push and pop? So that, I get rid of the counterexamples from the context and carry on.

Thanks,

Manjeet

--
Manjeet Dahiya
http://manjeetdahiya.com

[Khoo Yit Phang]

Hi Manjeet,

If I recall correctly, vc_push clears the previous counterexamples and adds a new context (which is just a list of
asserts, it doesn't include lets/variables), whereas vc_pop removes the most recent context. So, if you want to make
multiple queries, make sure there's a vc_push for every vc_query (and vc_pop after).

Yit