Propdefs not calculating everything

[Joachim Jansen]

In the attached file, some propagation is not done.

When approxdefs are turned off, the BDDs do the full propagation (so it is for certain possible with the propagating definitions.

The transformed XSB program is also added. Querying this with the symbol that should be propagated results in the answer that is desired (true) - so there is something going wrong querying the program.

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset c70cbd5f8a57>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset e107c9bdc6d4>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset 16fc752294e6>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset 430a9c6590c9>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset 9bd2290d4dbd>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset 54db0e1d5d5a>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset 97f899618eca>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset fcbd989b50fc>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset 6fca86582c65>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset aa1c5cbeb975>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset a381c14f274f>>

[Joachim Jansen]

Fixed bug in Top-down rules for quantified formula's

The call to the subformula did not always have the right subterms. Example:

! x : ? y : P(x,y).

transformed into the following incorrect rule (with Tx the tseitin for the forall formula):

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(v) ) ) & Tx_ct(x).

where the call to P_cf/2 lacked the variable x. The correct rule is:

! x y : P_ct(x,y) <- (!v : ( (v=y) | P_cf(x,v) ) ) & Tx_ct(x).

This fixes bug #432

Note that this fix has a serious impact on the running time of the propagation. It may be desirable to ignore this rule altogether because of performance reasons.

→ <<cset 81e21909f97e>>