Cvc.lean user manual

Index🔗

Symbols

  1. Ω
    1. Cvc.Ω

A

  1. add
    1. Cvc.Typed.Term.add
  2. and
    1. Cvc.Typed.Term.and
  3. and
    1. Cvc.Untyped.Term.and
  4. array­To
    1. Cvc.Srt.array­To
  5. assert
    1. Cvc.Typed.Solver.assert

B

  1. BVar
    1. Cvc.Typed.BVar
  2. BVars
    1. Cvc.Typed.BVars

C

  1. Cvc.Env
  2. Cvc.Is­Arith
  3. Cvc.IsArith.mk
    1. Instance constructor of Cvc.Is­Arith
  4. Cvc.Proof.View
  5. Cvc.Proof.View.absorb
    1. Constructor of Cvc.Proof.View
  6. Cvc.Proof.View.aci­Norm
    1. Constructor of Cvc.Proof.View
  7. Cvc.Proof.View.and­Elim
    1. Constructor of Cvc.Proof.View
  8. Cvc.Proof.View.and­Intro
    1. Constructor of Cvc.Proof.View
  9. Cvc.Proof.View.assume
    1. Constructor of Cvc.Proof.View
  10. Cvc.Proof.View.chain­MResolution
    1. Constructor of Cvc.Proof.View
  11. Cvc.Proof.View.chain­Resolution
    1. Constructor of Cvc.Proof.View
  12. Cvc.Proof.View.cnf­And­Neg
    1. Constructor of Cvc.Proof.View
  13. Cvc.Proof.View.cnf­And­Pos
    1. Constructor of Cvc.Proof.View
  14. Cvc.Proof.View.cnf­Equiv­Neg1
    1. Constructor of Cvc.Proof.View
  15. Cvc.Proof.View.cnf­Equiv­Neg2
    1. Constructor of Cvc.Proof.View
  16. Cvc.Proof.View.cnf­Equiv­Pos1
    1. Constructor of Cvc.Proof.View
  17. Cvc.Proof.View.cnf­Equiv­Pos2
    1. Constructor of Cvc.Proof.View
  18. Cvc.Proof.View.cnf­Implies­Neg1
    1. Constructor of Cvc.Proof.View
  19. Cvc.Proof.View.cnf­Implies­Neg2
    1. Constructor of Cvc.Proof.View
  20. Cvc.Proof.View.cnf­Implies­Pos
    1. Constructor of Cvc.Proof.View
  21. Cvc.Proof.View.cnf­Ite­Neg1
    1. Constructor of Cvc.Proof.View
  22. Cvc.Proof.View.cnf­Ite­Neg2
    1. Constructor of Cvc.Proof.View
  23. Cvc.Proof.View.cnf­Ite­Neg3
    1. Constructor of Cvc.Proof.View
  24. Cvc.Proof.View.cnf­Ite­Pos1
    1. Constructor of Cvc.Proof.View
  25. Cvc.Proof.View.cnf­Ite­Pos2
    1. Constructor of Cvc.Proof.View
  26. Cvc.Proof.View.cnf­Ite­Pos3
    1. Constructor of Cvc.Proof.View
  27. Cvc.Proof.View.cnf­Or­Neg
    1. Constructor of Cvc.Proof.View
  28. Cvc.Proof.View.cnf­Or­Pos
    1. Constructor of Cvc.Proof.View
  29. Cvc.Proof.View.cnf­Xor­Neg1
    1. Constructor of Cvc.Proof.View
  30. Cvc.Proof.View.cnf­Xor­Neg2
    1. Constructor of Cvc.Proof.View
  31. Cvc.Proof.View.cnf­Xor­Pos1
    1. Constructor of Cvc.Proof.View
  32. Cvc.Proof.View.cnf­Xor­Pos2
    1. Constructor of Cvc.Proof.View
  33. Cvc.Proof.View.cong
    1. Constructor of Cvc.Proof.View
  34. Cvc.Proof.View.contra
    1. Constructor of Cvc.Proof.View
  35. Cvc.Proof.View.dsl­Rewrite
    1. Constructor of Cvc.Proof.View
  36. Cvc.Proof.View.eq­Resolve
    1. Constructor of Cvc.Proof.View
  37. Cvc.Proof.View.equiv­Elim1
    1. Constructor of Cvc.Proof.View
  38. Cvc.Proof.View.equiv­Elim2
    1. Constructor of Cvc.Proof.View
  39. Cvc.Proof.View.evaluate
    1. Constructor of Cvc.Proof.View
  40. Cvc.Proof.View.factoring
    1. Constructor of Cvc.Proof.View
  41. Cvc.Proof.View.false­Elim
    1. Constructor of Cvc.Proof.View
  42. Cvc.Proof.View.false­Intro
    1. Constructor of Cvc.Proof.View
  43. Cvc.Proof.View.implies­Elim
    1. Constructor of Cvc.Proof.View
  44. Cvc.Proof.View.ite­Elim1
    1. Constructor of Cvc.Proof.View
  45. Cvc.Proof.View.ite­Elim2
    1. Constructor of Cvc.Proof.View
  46. Cvc.Proof.View.modus­Ponens
    1. Constructor of Cvc.Proof.View
  47. Cvc.Proof.View.nary­Cong
    1. Constructor of Cvc.Proof.View
  48. Cvc.Proof.View.not­And
    1. Constructor of Cvc.Proof.View
  49. Cvc.Proof.View.not­Equiv­Elim1
    1. Constructor of Cvc.Proof.View
  50. Cvc.Proof.View.not­Equiv­Elim2
    1. Constructor of Cvc.Proof.View
  51. Cvc.Proof.View.not­Implies­Elim1
    1. Constructor of Cvc.Proof.View
  52. Cvc.Proof.View.not­Implies­Elim2
    1. Constructor of Cvc.Proof.View
  53. Cvc.Proof.View.not­Ite­Elim1
    1. Constructor of Cvc.Proof.View
  54. Cvc.Proof.View.not­Ite­Elim2
    1. Constructor of Cvc.Proof.View
  55. Cvc.Proof.View.not­Not­Elim
    1. Constructor of Cvc.Proof.View
  56. Cvc.Proof.View.not­Or­Elim
    1. Constructor of Cvc.Proof.View
  57. Cvc.Proof.View.not­Xor­Elim1
    1. Constructor of Cvc.Proof.View
  58. Cvc.Proof.View.not­Xor­Elim2
    1. Constructor of Cvc.Proof.View
  59. Cvc.Proof.View.other
    1. Constructor of Cvc.Proof.View
  60. Cvc.Proof.View.pairwise­Cong
    1. Constructor of Cvc.Proof.View
  61. Cvc.Proof.View.refl
    1. Constructor of Cvc.Proof.View
  62. Cvc.Proof.View.reordering
    1. Constructor of Cvc.Proof.View
  63. Cvc.Proof.View.resolution
    1. Constructor of Cvc.Proof.View
  64. Cvc.Proof.View.sat­Refutation
    1. Constructor of Cvc.Proof.View
  65. Cvc.Proof.View.scope
    1. Constructor of Cvc.Proof.View
  66. Cvc.Proof.View.split
    1. Constructor of Cvc.Proof.View
  67. Cvc.Proof.View.symm
    1. Constructor of Cvc.Proof.View
  68. Cvc.Proof.View.theory­Rewrite
    1. Constructor of Cvc.Proof.View
  69. Cvc.Proof.View.trans
    1. Constructor of Cvc.Proof.View
  70. Cvc.Proof.View.true­Elim
    1. Constructor of Cvc.Proof.View
  71. Cvc.Proof.View.true­Intro
    1. Constructor of Cvc.Proof.View
  72. Cvc.Proof.View.trust
    1. Constructor of Cvc.Proof.View
  73. Cvc.Proof.View.trust­Theory­Rewrite
    1. Constructor of Cvc.Proof.View
  74. Cvc.Proof.View.xor­Elim1
    1. Constructor of Cvc.Proof.View
  75. Cvc.Proof.View.xor­Elim2
    1. Constructor of Cvc.Proof.View
  76. Cvc.Srt.array­To
  77. Cvc.To­Typ
  78. Cvc.ToTyp.mk
    1. Instance constructor of Cvc.To­Typ
  79. Cvc.Typed.BVar
  80. Cvc.Typed.BVars
  81. Cvc.Typed.Solver
  82. Cvc.Typed.Solver.Env­Sat
  83. Cvc.Typed.Solver.Env­Unknown
  84. Cvc.Typed.Solver.Env­Unsat
  85. Cvc.Typed.Solver.Proof
  86. Cvc.Typed.Solver.Proof.fold
  87. Cvc.Typed.Solver.Proof.fold­Up
  88. Cvc.Typed.Solver.Proof.free­Assumptions
  89. Cvc.Typed.Solver.Proof.rule­Counts
  90. Cvc.Typed.Solver.Proof.size
  91. Cvc.Typed.Solver.Proof.trusted
  92. Cvc.Typed.Solver.Proof.view
  93. Cvc.Typed.Solver.Proof­View
  94. Cvc.Typed.Solver.assert
  95. Cvc.Typed.Solver.check­Is­Sat
  96. Cvc.Typed.Solver.check­Sat
  97. Cvc.Typed.Solver.check­Sat?
  98. Cvc.Typed.Solver.define­Fun
  99. Cvc.Typed.Solver.get­Timeout­Core
  100. Cvc.Typed.Solver.get­Unsat­Core
  101. Cvc.Typed.Solver.get­Unsat­Proof
  102. Cvc.Typed.Solver.get­Value
  103. Cvc.Typed.Solver.new
  104. Cvc.Typed.Term
  105. Cvc.Typed.Term.add
  106. Cvc.Typed.Term.and
  107. Cvc.Typed.Term.lambda
  108. Cvc.Typed.Term.mk­Bool
  109. Cvc.Typed.Term.mk­Exists
  110. Cvc.Typed.Term.mk­Forall
  111. Cvc.Typed.Term.mk­Int
  112. Cvc.Typed.Term.mk­Symbol
  113. Cvc.Typed.Term.mk­Symbol­As
  114. Cvc.Typed.Term.to­Untyped
  115. Cvc.Untyped.Solver.Proof­View
  116. Cvc.Untyped.Solver.set­Logic
  117. Cvc.Untyped.Solver.set­Opt
  118. Cvc.Untyped.Solver.set­Option
  119. Cvc.Untyped.Term
  120. Cvc.Untyped.Term.and
  121. Cvc.Untyped.Term.mk­Bool
  122. Cvc.Untyped.Term.mk­Int
  123. Cvc.Untyped.Term.mk­Symbol
  124. Cvc.Untyped.Term.mk­Symbol­As
  125. Cvc.Untyped.Term.to­Typed
  126. Cvc.Untyped.Term.to­Typed­As
  127. Cvc.Ω
  128. check­Is­Sat
    1. Cvc.Typed.Solver.check­Is­Sat
  129. check­Sat
    1. Cvc.Typed.Solver.check­Sat
  130. check­Sat?
    1. Cvc.Typed.Solver.check­Sat?

D

  1. define­Fun
    1. Cvc.Typed.Solver.define­Fun

E

  1. Env
    1. Cvc.Env
  2. Env­Sat
    1. Cvc.Typed.Solver.Env­Sat
  3. Env­Unknown
    1. Cvc.Typed.Solver.Env­Unknown
  4. Env­Unsat
    1. Cvc.Typed.Solver.Env­Unsat

F

  1. fold
    1. Cvc.Typed.Solver.Proof.fold
  2. fold­Up
    1. Cvc.Typed.Solver.Proof.fold­Up
  3. free­Assumptions
    1. Cvc.Typed.Solver.Proof.free­Assumptions

G

  1. get­Timeout­Core
    1. Cvc.Typed.Solver.get­Timeout­Core
  2. get­Unsat­Core
    1. Cvc.Typed.Solver.get­Unsat­Core
  3. get­Unsat­Proof
    1. Cvc.Typed.Solver.get­Unsat­Proof
  4. get­Value
    1. Cvc.Typed.Solver.get­Value

I

  1. Is­Arith
    1. Cvc.Is­Arith

L

  1. lambda
    1. Cvc.Typed.Term.lambda

M

  1. manager
  2. mk­Bool
    1. Cvc.Typed.Term.mk­Bool
  3. mk­Bool
    1. Cvc.Untyped.Term.mk­Bool
  4. mk­Exists
    1. Cvc.Typed.Term.mk­Exists
  5. mk­Forall
    1. Cvc.Typed.Term.mk­Forall
  6. mk­Int
    1. Cvc.Typed.Term.mk­Int
  7. mk­Int
    1. Cvc.Untyped.Term.mk­Int
  8. mk­Symbol
    1. Cvc.Typed.Term.mk­Symbol
  9. mk­Symbol
    1. Cvc.Untyped.Term.mk­Symbol
  10. mk­Symbol­As
    1. Cvc.Typed.Term.mk­Symbol­As
  11. mk­Symbol­As
    1. Cvc.Untyped.Term.mk­Symbol­As

N

  1. new
    1. Cvc.Typed.Solver.new

P

  1. Proof
    1. Cvc.Typed.Solver.Proof
  2. Proof­View
    1. Cvc.Typed.Solver.Proof­View
  3. Proof­View
    1. Cvc.Untyped.Solver.Proof­View

R

  1. rule­Counts
    1. Cvc.Typed.Solver.Proof.rule­Counts

S

  1. Solver
    1. Cvc.Typed.Solver
  2. set­Logic
    1. Cvc.Untyped.Solver.set­Logic
  3. set­Opt
    1. Cvc.Untyped.Solver.set­Opt
  4. set­Option
    1. Cvc.Untyped.Solver.set­Option
  5. size
    1. Cvc.Typed.Solver.Proof.size

T

  1. Term
    1. Cvc.Typed.Term
  2. Term
    1. Cvc.Untyped.Term
  3. To­Typ
    1. Cvc.To­Typ
  4. to­Typed
    1. Cvc.Untyped.Term.to­Typed
  5. to­Typed­As
    1. Cvc.Untyped.Term.to­Typed­As
  6. to­Untyped
    1. Cvc.Typed.Term.to­Untyped
  7. trusted
    1. Cvc.Typed.Solver.Proof.trusted
  8. typ
    1. Cvc.ToTyp.typ (class method)

V

  1. View
    1. Cvc.Proof.View
  2. valid_typ
    1. Cvc.IsArith.valid_typ (class method)
  3. view
    1. Cvc.Typed.Solver.Proof.view