From bf34600f08d732680f7a9b3d85a257caf435418b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 12 Aug 2024 08:49:55 -1000 Subject: [PATCH] add release nodes and add the author reference in qfnra_tactic Signed-off-by: Lev Nachmanson --- RELEASE_NOTES.md | 7 +++++++ src/tactic/smtlogics/qfnra_tactic.h | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 3830f566ffa..b69772dcd5f 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -10,6 +10,13 @@ Version 4.next - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. +Version 4.13.1 +============== +- single-sample cell projection in nlsat was designed by Haokun Li and Bican Xia. +- using simple-checker together with and variable ordering supported by qfnra_tactic was developed by Mengyu Zhao (Linxi) and Shaowei Cai. + + The projection is described in paper by Haokun Li and Bican Xia, [Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection](https://arxiv.org/abs/2003.00409). The code ported from https://github.com/hybridSMT/hybridSMT.git + Version 4.13.0 ============== - add ARM64 wheels for Python, thanks to Steven Moy, smoy diff --git a/src/tactic/smtlogics/qfnra_tactic.h b/src/tactic/smtlogics/qfnra_tactic.h index 09a5d0480c8..344ea3f366e 100644 --- a/src/tactic/smtlogics/qfnra_tactic.h +++ b/src/tactic/smtlogics/qfnra_tactic.h @@ -12,7 +12,7 @@ Module Name: Author: Leonardo (leonardo) 2012-02-28 - + Mengyu Zhao (Linxi) and Shaowei Cai, ported from https://github.com/hybridSMT/hybridSMT.git Notes: --*/