search

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.
1 stars 0 forks source link

a2r messes things up #28

Open jonnybest opened 11 years ago

jonnybest commented 11 years ago

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.

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

jonnybest commented 11 years ago

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.