  This file is part of the Kind 2 model checker . 

    Copyright ( c ) 2015 by the Board of Trustees of the University of Iowa 

    Licensed under the Apache License , Version 2.0 ( the " License " ) ; you 
    may not use this file except in compliance with the License .   You 
    may obtain a copy of the License at 

    -2.0 

    Unless required by applicable law or agreed to in writing , software 
    distributed under the License is distributed on an " AS IS " BASIS , 
    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND , either express or 
    implied . See the License for the specific language governing 
    permissions and limitations under the License . 



   Copyright (c) 2015 by the Board of Trustees of the University of Iowa

   Licensed under the Apache License, Version 2.0 (the "License"); you
   may not use this file except in compliance with the License.  You
   may obtain a copy of the License at

   -2.0 

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
   implied. See the License for the specific language governing
   permissions and limitations under the License. 

*)


* Very basic helper functions for unrolling . More precisely , asserting 
 one- and two - state invariants .
one- and two-state invariants. *)

(** Asserts some terms from [0] to [k-1]. *)
val assert_0_to : SMTSolver.t -> Numeral.t -> Term.t -> unit

* Asserts some terms from [ 1 ] to [ k-1 ] .
val assert_1_to : SMTSolver.t -> Numeral.t -> Term.t -> unit

* Asserts some new one- and two - state invariant up to [ k-1 ] , starting at 
   * [ 0 ] for one - state invariants , 
   * [ 1 ] for two - state invariants .
  * [0] for one-state invariants,
  * [1] for two-state invariants. *)
val assert_new_invs_to : SMTSolver.t -> Numeral.t -> (
  Term.TermSet.t * Term.TermSet.t
) -> unit


 
    Local Variables : 
    compile - command : " make -C .. -k " 
    tuareg - interactive - program : " ./kind2.top -I ./_build -I  / SExpr " 
    indent - tabs - mode : nil 
    End : 

   Local Variables:
   compile-command: "make -C .. -k"
   tuareg-interactive-program: "./kind2.top -I ./_build -I ./_build/SExpr"
   indent-tabs-mode: nil
   End: 
*)
* Asserts some terms from [0] to [k-1]. 
  This file is part of the Kind 2 model checker . 

    Copyright ( c ) 2015 by the Board of Trustees of the University of Iowa 

    Licensed under the Apache License , Version 2.0 ( the " License " ) ; you 
    may not use this file except in compliance with the License .   You 
    may obtain a copy of the License at 

    -2.0 

    Unless required by applicable law or agreed to in writing , software 
    distributed under the License is distributed on an " AS IS " BASIS , 
    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND , either express or 
    implied . See the License for the specific language governing 
    permissions and limitations under the License . 



   Copyright (c) 2015 by the Board of Trustees of the University of Iowa

   Licensed under the Apache License, Version 2.0 (the "License"); you
   may not use this file except in compliance with the License.  You
   may obtain a copy of the License at

   -2.0 

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
   implied. See the License for the specific language governing
   permissions and limitations under the License. 

*)


* Very basic helper functions for unrolling . More precisely , asserting 
 one- and two - state invariants .
one- and two-state invariants. *)

val assert_0_to : SMTSolver.t -> Numeral.t -> Term.t -> unit

* Asserts some terms from [ 1 ] to [ k-1 ] .
val assert_1_to : SMTSolver.t -> Numeral.t -> Term.t -> unit

* Asserts some new one- and two - state invariant up to [ k-1 ] , starting at 
   * [ 0 ] for one - state invariants , 
   * [ 1 ] for two - state invariants .
  * [0] for one-state invariants,
  * [1] for two-state invariants. *)
val assert_new_invs_to : SMTSolver.t -> Numeral.t -> (
  Term.TermSet.t * Term.TermSet.t
) -> unit


 
    Local Variables : 
    compile - command : " make -C .. -k " 
    tuareg - interactive - program : " ./kind2.top -I ./_build -I  / SExpr " 
    indent - tabs - mode : nil 
    End : 

   Local Variables:
   compile-command: "make -C .. -k"
   tuareg-interactive-program: "./kind2.top -I ./_build -I ./_build/SExpr"
   indent-tabs-mode: nil
   End: 
*)