Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. CONTRIBUTORS: new proof method "argo"
  2. NEWS: new proof method "argo"
  3. use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
  4. invoke argo as part of the tried automatic proof methods
  5. new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
Changeset 63964:9f0308e80366 by boehmes:
CONTRIBUTORS: new proof method "argo"
The file was modified CONTRIBUTORS (diff)
Changeset 63963:ed98a055b9a5 by boehmes:
NEWS: new proof method "argo"
The file was modified NEWS (diff)
Changeset 63962:83a625d06e91 by boehmes:
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
The file was addedsrc/HOL/Tools/Argo/argo_sat_solver.ML
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/SAT.thy (diff)
Changeset 63961:2fd9656c4c82 by boehmes:
invoke argo as part of the tried automatic proof methods
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Tools/try0.ML (diff)
Changeset 63960:3daf02070be5 by boehmes:
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
The file was addedsrc/HOL/Argo.thy
The file was addedsrc/HOL/Tools/Argo/argo_real.ML
The file was addedsrc/HOL/Tools/Argo/argo_tactic.ML
The file was addedsrc/HOL/ex/Argo_Examples.thy
The file was addedsrc/Tools/Argo/argo_cc.ML
The file was addedsrc/Tools/Argo/argo_cdcl.ML
The file was addedsrc/Tools/Argo/argo_clausify.ML
The file was addedsrc/Tools/Argo/argo_cls.ML
The file was addedsrc/Tools/Argo/argo_common.ML
The file was addedsrc/Tools/Argo/argo_core.ML
The file was addedsrc/Tools/Argo/argo_expr.ML
The file was addedsrc/Tools/Argo/argo_heap.ML
The file was addedsrc/Tools/Argo/argo_lit.ML
The file was addedsrc/Tools/Argo/argo_proof.ML
The file was addedsrc/Tools/Argo/argo_rewr.ML
The file was addedsrc/Tools/Argo/argo_simplex.ML
The file was addedsrc/Tools/Argo/argo_solver.ML
The file was addedsrc/Tools/Argo/argo_term.ML
The file was addedsrc/Tools/Argo/argo_thy.ML
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Real.thy (diff)