Styjun

Of strange atmospheres - the survivable but unbreathable

How did NASA Langley end up with the first 737?

Underwater city sanitation

Why is 'additive' EQ more difficult to use than 'subtractive'?

Are runways booked by airlines to land their planes?

Can a ring of spell storing and access to Find spells produce an endless menagerie?

How to politely tell someone they did not hit reply all in email?

What were the Ethiopians doing in Xerxes' army?

A burglar's sunglasses, a lady's odyssey

How does the Earth's center produce heat?

Where is Jon going?

Python program for fibonacci sequence using a recursive function

Best shape for a necromancer's undead minions for battle?

Surprisingly persistent local variable

Why did Jon Snow do this immoral act if he is so honorable?

Is keeping the forking link on a true fork necessary (Github/GPL)?

Can we assume that a hash function with high collision resistance also means highly uniform distribution?

Shorten or merge multiple lines of `&> /dev/null &`

How to deceive the MC

3 prong range outlet

What would prevent living skin from being a good conductor for magic?

Navigating a quick return to previous employer

Can a UK national work as a paid shop assistant in the USA?

No Iron for your fair-folk maiden? (Part 1)

Appropriate Z3 tactic to eliminate trivial existential quantifier

quantifier elimination over bit vectors produces overly complicated resultsQuantifier Elimination - More questionsArrays and QuantifierQuantifier elimination for multilinear rational arithmetic in Z3What is the state-of-the-art solver for quantifier elimination under LRA?How can I write a long smt-lib expression with an existential quantifier?Z3 Interpolants in presence of quantifiersUse Z3 to determine difficulty of quantifier elimination for BV-queriesWhat tactic configurations makes solving Quantifier logic faster in general?z3py: Usage of existential quantifier

.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty height:90px;width:728px;box-sizing:border-box;

0

I'm experimenting with Z3 tactics and was wondering which tactic can simplify trivial existential quantifiers like the following:

(declare-datatypes () ((Value none (some (val String)))))
(declare-const foo Value)

(assert (exists ((x String)) (and (= foo (some x)) (= x "bar"))))

I've attempted something simple like this:

(apply (repeat (then (or-else split-clause skip) propagate-values simplify)))

But it doesn't get rid of the exists. I can throw qe or qe2 into the mix there, but those feel like overkill here, and generally take ages on nontrivial problems.

If I do a straightforward (check-sat) with maximum verbosity, Z3 has zero trouble solving it:

(simplifier :num-exprs 8 :num-asts 174 :time 0.00 :before-memory 2.78 :after-memory 2.78)
(smt.tactic start)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.reducing)
(smt.refine-injectivity)
(smt.cheap-fourier-motzkin)
(smt.reducing)
(smt.pattern-inference)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
sat
(model 
 (define-fun foo () Value
 (some "bar"))
)

And I was hoping some of the steps would suggest tactics I can apply myself, but they don't.

Is there a good tactic for this?

z3 smt

share|improve this question

edited Mar 24 at 14:07

copumpkin

asked Mar 23 at 22:45

copumpkincopumpkin

2,2821321

add a comment | 

0

I'm experimenting with Z3 tactics and was wondering which tactic can simplify trivial existential quantifiers like the following:

(declare-datatypes () ((Value none (some (val String)))))
(declare-const foo Value)

(assert (exists ((x String)) (and (= foo (some x)) (= x "bar"))))

I've attempted something simple like this:

(apply (repeat (then (or-else split-clause skip) propagate-values simplify)))

But it doesn't get rid of the exists. I can throw qe or qe2 into the mix there, but those feel like overkill here, and generally take ages on nontrivial problems.

If I do a straightforward (check-sat) with maximum verbosity, Z3 has zero trouble solving it:

(simplifier :num-exprs 8 :num-asts 174 :time 0.00 :before-memory 2.78 :after-memory 2.78)
(smt.tactic start)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.reducing)
(smt.refine-injectivity)
(smt.cheap-fourier-motzkin)
(smt.reducing)
(smt.pattern-inference)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
sat
(model 
 (define-fun foo () Value
 (some "bar"))
)

And I was hoping some of the steps would suggest tactics I can apply myself, but they don't.

Is there a good tactic for this?

z3 smt

share|improve this question

edited Mar 24 at 14:07

copumpkin

asked Mar 23 at 22:45

copumpkincopumpkin

2,2821321

add a comment | 

I'm experimenting with Z3 tactics and was wondering which tactic can simplify trivial existential quantifiers like the following:

(declare-datatypes () ((Value none (some (val String)))))
(declare-const foo Value)

(assert (exists ((x String)) (and (= foo (some x)) (= x "bar"))))

I've attempted something simple like this:

(apply (repeat (then (or-else split-clause skip) propagate-values simplify)))

But it doesn't get rid of the exists. I can throw qe or qe2 into the mix there, but those feel like overkill here, and generally take ages on nontrivial problems.

If I do a straightforward (check-sat) with maximum verbosity, Z3 has zero trouble solving it:

(simplifier :num-exprs 8 :num-asts 174 :time 0.00 :before-memory 2.78 :after-memory 2.78)
(smt.tactic start)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.reducing)
(smt.refine-injectivity)
(smt.cheap-fourier-motzkin)
(smt.reducing)
(smt.pattern-inference)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
sat
(model 
 (define-fun foo () Value
 (some "bar"))
)

And I was hoping some of the steps would suggest tactics I can apply myself, but they don't.

Is there a good tactic for this?

z3 smt

share|improve this question

edited Mar 24 at 14:07

copumpkin

asked Mar 23 at 22:45

copumpkincopumpkin

2,2821321

(declare-datatypes () ((Value none (some (val String)))))
(declare-const foo Value)

(assert (exists ((x String)) (and (= foo (some x)) (= x "bar"))))

(apply (repeat (then (or-else split-clause skip) propagate-values simplify)))

(simplifier :num-exprs 8 :num-asts 174 :time 0.00 :before-memory 2.78 :after-memory 2.78)
(smt.tactic start)
(smt.propagate-values)
(smt.nnf-cnf)
(smt.reduce-asserted)
(smt.lift-ite)
(smt.reducing)
(smt.refine-injectivity)
(smt.cheap-fourier-motzkin)
(smt.reducing)
(smt.pattern-inference)
(smt.maximizing-bv-sharing)
(smt.reduce-asserted)
(smt.simplifier-done)
(smt.searching)
sat
(model 
 (define-fun foo () Value
 (some "bar"))
)

share|improve this question

edited Mar 24 at 14:07

copumpkin

asked Mar 23 at 22:45

copumpkincopumpkin

2,2821321

share|improve this question

edited Mar 24 at 14:07

copumpkin

asked Mar 23 at 22:45

copumpkincopumpkin

2,2821321

asked Mar 23 at 22:45

copumpkincopumpkin

2,2821321

asked Mar 23 at 22:45

copumpkincopumpkin

2,2821321