Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Using Scala (without Z3) to show that there are, in fact, more solutions to the constraint:</p> <pre><code>val tf = Seq(true, false) val allValid = for(a &lt;- tf; b &lt;- tf; c &lt;- tf; d &lt;- tf; if((a &amp;&amp; (b ^ c)) ^ d)) yield ( (if(a) "a" else "") + (if(b) "b" else "") + (if(c) "c" else "") + (if(d) "d" else "")) allValid.mkString("{ ", ", ", " }") </code></pre> <p>Prints:</p> <pre><code>{ abcd, ab, ac, ad, bcd, bd, cd, d } </code></pre> <p>So unless I'm missing something, the question is, why does it <em>not</em> find <em>all</em> solutions? Now here is the answer to that one. (Spoiler alert: "getAllModels" doesn't really get all models.) First, let's reproduce what you observed:</p> <pre><code>import z3.scala._ val ctx = new Z3Context("MODEL" -&gt; true) val a = ctx.mkFreshConst("a", ctx.mkBoolSort) val b = ctx.mkFreshConst("b", ctx.mkBoolSort) val c = ctx.mkFreshConst("c", ctx.mkBoolSort) val d = ctx.mkFreshConst("d", ctx.mkBoolSort) val cstr0 = ctx.mkXor(b, c) val cstr1 = ctx.mkAnd(a, cstr0) val cstr2 = ctx.mkXor(cstr1, d) ctx.assertCnstr(cstr2) </code></pre> <p>Now, if I run: <code>ctx.checkAndGetAllModels.foreach(println(_))</code>, I get:</p> <pre><code>d!3 -&gt; false a!0 -&gt; true c!2 -&gt; false b!1 -&gt; true d!3 -&gt; true // this model is problematic a!0 -&gt; false d!3 -&gt; false a!0 -&gt; true c!2 -&gt; true b!1 -&gt; false d!3 -&gt; true a!0 -&gt; true c!2 -&gt; false b!1 -&gt; false d!3 -&gt; true a!0 -&gt; true c!2 -&gt; true b!1 -&gt; true </code></pre> <p>Now, the problem is that the second model is an <em>incomplete</em> model. Z3 can return it, because whatever the values for <code>b</code> and <code>c</code> are, the constraint is satisfied (<code>b</code> and <code>c</code> are <em>don't-care</em> variables). The current implementation of <code>checkAndGetAllModels</code> simply negates the model to prevent repetition; in this case, it will ask for another model such that <code>(not (and d (not a)))</code> holds. This will prevent all other models with this two values from being returned. In a sense, the incomplete model actually represents four valid, completed, models.</p> <p>By the way, what happens if you use the DSL of ScalaZ3 with the <code>findAll</code> function is that all models will be <em>completed</em> with default values when they are incomplete (and before they are used to compute the next one). In the context of the DSL we can do this, because we know the set of variables that appear in the formula. In this case, it's harder to guess how the model should be completed. One option would be for ScalaZ3 to remember which variables were used. A better solution would be for Z3 to have an option to always return values for don't-care variables, or perhaps simply to list all <em>don't-care</em> variables in a model.</p>
    singulars
    1. This table or related slice is empty.
    1. POToo many possible configurations in z3 using scala^z3
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USPhilippe
    1. USPhilippe
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POToo many possible configurations in z3 using scala^z3
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COOf course Owen and you are right. The results shown here are correct. In the end my problem is a different one. If you see my term as a configuration and everything that is true would be delivered, then it would be too much ;) I wanted a configuration where: If you choose a left-hand-side (in XOR), the complete right-hand-side should be false. Can this be accomplished?
      singulars
      1. PO
      1. USJohn Smith
    2. COOne way would be to enhance the information in the model this way: "a->!d" "d->!a" "d->!b" "d->!c" etc... But in large models this is a lot of work...
      singulars
      1. PO
      1. USJohn Smith
    3. COI'm not sure I understand what "the complete right-hand-side" refers to. Considering your boolean expression as a tree, does that mean that you want all the _leafs_ of the right-hand-side to be false? Or as many of them as possible?
      singulars
      1. PO
      1. USPhilippe
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload