questions about the Simplifier of STP

[angel...@gmail.com]

Dear All,

I'm new to constraint solving and STP.
I want to use STP to simplify formulas.
I used the method "vc_simplify" which is specified in "c_interface.h", but the result is not the same as that I expected.
"vc_simplify" can filter the duplication of a formular, for example, if the input formula is "a>b && b<c && a>b" (they are specified in CVC), "vc_simplify" can output "a>b && b<c".
However, for following cases:
(1) "a>b && a>b+1" (it should be simplied to "a>b+1")
(2) "a>b && a<=b" (it should be simplied to "false" which represents a controdiction)
"vc_simplify" outputs the same formula without any simplification.

Can anyone show me how to use the simplification functionality of STP?

Any your help will be appreciated! Thanks.

Best regards,

Mingyue Jiang

[Jonas Wagner]

Just a quick question: What are the types of your variables? If they are bitvectors, a>b+1 does not imply a>b because of overflow.

I don't know how the simplifier works, but I would expect it to perform mostly cheap syntactic changes.

Cheers,

Jonas

--

---
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/groups/opt_out.

[Vijay Ganesh]

Hi,

You have some mis-conceptions about the semantics of bit-vectors. As Jonas pointed out, a>b+1 does not imply a>b in bit-vector logic (modular arithmetic).

-Vijay.

[angel...@gmail.com]

Thanks. Jonas.

Yes, they are bitvectors.

I have little knowledge about bit-vector logic. 

 

But I thought such simplication should be accomplished during constraint solving.  "vc_simplify" seems incapable of doing it.

 

Do you have any experence of getting the simplified constraint from STP?

 

Mingyue

在 2014年1月29日星期三UTC+11下午7时08分54秒，Jonas Wagner写道：

[angel...@gmail.com]

Thanks, Jonas.

Yes, they are bit-vectors. I have little knowledge about bit-vector logic.

 

But I thought such simplification should be accomplished during constraint solving.  "vc_simplify" seems incapale of doing it.

 

Do you have any experience of getting simplified constraint from STP?

 

Mingyue

 

在 2014年1月29日星期三UTC+11下午7时08分54秒，Jonas Wagner写道：

Just a quick question: What are the types of your variables? If they are bitvectors, a>b+1 does not imply a>b because of overflow.

[Stephen McCamant]

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

M> Thanks. Jonas.
M> Yes, they are bitvectors.
M> I have little knowledge about bit-vector logic.

M> But I thought such simplification should be accomplished during
M> constraint solving. "vc_simplify" seems incapable of doing it.

M> Do you have any experience of getting the simplified constraint
M> from STP?

It seems like your expectation is that STP will perform every
simplification that you would perform when looking at a formula by
hand, and I don't think that's reasonable. STP's main job is not
simplifying formulas, it's solving formulas. It is able to perform
some simplifications that the developers thought would be profitable
in the solving process, but it doesn't attempt to perform every
simplification that might be possible.

First, just to be sure it's clear, one of the simplifications you were
hoping to be performed is in fact incorrect. Checking whether a
simplification is correct is in fact one thing that STP *can* do
easily. For instance if a and b are 8-bit values, we can express the
correctness of your proposed simplification in CVC format as:

a : BV(8);
b : BV(8);
QUERY((BVGT(a, b) AND BVGT(a, BVPLUS(8, b, 0x01)))
<=>
(BVGT(a, BVPLUS(8, b, 0x01))));
COUNTEREXAMPLE;

If you run this it will show you a counterexample.

Some of the patterns of simplifications you want could be expressed in
terms of properties that could be checked with STP. For instance I
think in your example (1), you want to simplify "P && Q" to "Q" when
"P => Q"; you could use STP to check whether "P => Q" for a particular
P and Q. Or your example (2) you want to replace a certain part of
your formula with "false" because it's unsatisfiable. You could pass a
sub-formula of your larger formula to STP to see if that's the
case. However this would be a more expensive process that what
vc_simplify does, because it would involve solving many satisfiability
queries. By contrast, vc_simplify performs only a more limited set of
simplifications because of its role as an optimization: the goal is
for the process of first simplifying the formula, and then solving the
simplified formula, to be faster than solving the original formula.

Hope this helps,

-- Stephen