Project

General

Profile

« Previous | Next » 

Revision 3e209698

Added by Pierre-Loïc Garoche almost 9 years ago

First fully working version of horn backend.

Has to be called with "-horn -node main_node"

The test script compute the smt2 file and calls z3 on them.

View differences:

ex3.smt2
121 121 
  (top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
122 122 
))
123 123 

  		




  124
  
  
    
; Collecting semantics with main node top


  		




  
  124
  
    
; Collecting semantics for node top


  		




  125
  125
  
    

  		




  126
  126
  
    
(declare-rel MAIN (Bool Bool Bool Int Bool))


  		




  127
  127
  
    
; Initial set


  		




  ......




  135
  135
  
    
))


  		




  136
  136
  
    

  		




  137
  137
  
    
; Inductive def


  		




  138
  
  
    
(declare-var dummy Bool)


  		




  139
  138
  
    
(rule (=> 


  		




  140
  
  
    
  (and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c dummy)


  		




  
  139
  
    
  (and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.OK)


  		




  141
  140
  
    
       (top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)


  		




  142
  141
  
    
  )


  		




  143
  142
  
    
  (MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x top.OK)


  		




  ......




  147
  146
  
    
(declare-rel ERR ())


  		




  148
  147
  
    
(rule (=> 


  		




  149
  148
  
    
  (and (not (= top.OK true))


  		




  150
  
  
    
       (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c))


  		




  
  149
  
    
       (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c top.OK))


  		




  151
  150
  
    
  ERR))


  		




  152
  151
  
    
(query ERR)


  		












Also available in:  Unified diff