search

salmans / Razor

5 stars 0 forks source link

Surprise Me: Relaxed model construction / Allowing random collapses #38

Open salmans opened 9 years ago

salmans commented 9 years ago

Relaxed model construction (using --relax) returns models with random collapses when the underlying interface to the SMT solver is SBV; however, Razor always returns homomorphically minimal models when using SMTLib2. Is this a bug in Razor or an unexpected feature of SMTLib2?

salmans commented 9 years ago

The bug was fixed after adding an extra set of axioms, which ask the solver to return a model in which two distinct elements of the current model may be collapsed. This feature currently doesn't work with infinite models, because of the "incomplete" predicates in the set of ground sequents.

thedotmatrix commented 9 years ago

Important point from duplicate issues.... Does allowing random collapses at the SMT layer enable us to return more complete models than the current "collapse at infinity" mode would?

Other than this point, surprising models could be implemented completely adhoc via automated augmentations.

dandougherty commented 9 years ago

On Wed, May 20, 2015 at 8:05 PM, Ryan Danas notifications@github.com wrote:

Does allowing random collapses at the SMT layer enable us to return more complete models than the current "collapse at infinity" mode would?

what do you mean by "more complete models"? I wonder if you mean to be asking whether (or not) SMT collapsing gives us any more models, after minimization, than collapse-at-infinity? That is a good question to ask. Try to answer it!