You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jan 26, 2018. It is now read-only.
The a2r axiom presents a difficult problem for MBQI. This problem can be solved by MBQI only while adding this axiom:
(assert
(!
; axiom for the conversion function Atom -> Relation
(forall ((x0 Atom)) (and (in_1 x0 (a2r_1 x0)) (forall ((y0 Atom)) (=> (in_1 y0 (a2r_1 x0)) (= x0 y0)))))
:named ax5
)
)
This lets the MBQI-enabled solver fail. The problem for MBQI is the equality between the in_1 part and the forall part. The solver behaves the same way for substituting and with = or even with "<=>" as two assertions.
(assert
(!
; axiom for the conversion function Atom -> Relation
(forall ((x0 Atom)) (=> (in_1 x0 (a2r_1 x0)) (forall ((y0 Atom)) (=> (in_1 y0 (a2r_1 x0)) (= x0 y0)))))
:named ax5_1
)
)
(assert
(!
; axiom for the conversion function Atom -> Relation
(forall ((x0 Atom)) (=> (forall ((y0 Atom)) (=> (in_1 y0 (a2r_1 x0)) (= x0 y0))) (in_1 x0 (a2r_1 x0))))
:named ax5_2
)
)
You can observe that MBQI succeeds if you drop ax5_2 from the VC.
Maybe I could fix this by introducing a lemma for each call containing a2r as an argument. The question remains: How do I implement this efficiently? So far I can only write lemmas for each declaration. I would have to extend the program to allow for for this more 'dynamic' approach.
Sign up for freeto subscribe to this conversation on GitHub.
Already have an account?
Sign in.
The a2r axiom presents a difficult problem for MBQI. This problem can be solved by MBQI only while adding this axiom:
This lets the MBQI-enabled solver fail. The problem for MBQI is the equality between the
in_1
part and theforall
part. The solver behaves the same way for substitutingand
with=
or even with"<=>"
as two assertions.You can observe that MBQI succeeds if you drop ax5_2 from the VC.
I have gotten the idea of testing MBQI only from this thread on the stackoverflow http://stackoverflow.com/questions/13025127/getting-sat-for-large-problems/13032820
The text was updated successfully, but these errors were encountered: