Skip to content

Add simplify-node lemma feature #149

@lisandrasilva

Description

@lisandrasilva

It would be useful if we could test if some lemma works to discharge some node in the command line, without having to write the lemma in the lemmas file, rekompile and then run the proof again. Take the example where some node has the following constraint:

#And { maxUInt8 <Int bool2Word ( maxUInt128 <Int VV0_x_114b9705:Int ) <<Int 7 #Equals true } 

And we want to easily check that the following lemma works to prove that the node has a contradiction:

rule A <Int bool2Word ( _ ) <<Int B => false
      requires A >=Int 1 <<Int B

Instead of having to add the lemma to the lemmas file and then rekompile, it would be useful to be able to:

kontrol simplify-node testName nodeId "A <Int bool2Word ( _ ) <<Int B => false requires A >=Int 1 <<Int B"

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions