simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

new regression test for (get-model); fix mdx test

Browse source
This commit is contained in:
Simon Cruanes 2022-02-02 16:12:55 -05:00
parent 50bfe79b6a
commit c4bbaddc06
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
4 changed files with 29 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/guide.md
View file

@ -344,7 +344,7 @@ Sidekick_base_solver.Solver.Sat
(model
(true := true)
(false := false)
(_sk_lra__le0 := _sk_lra__le0)
(_sk_lra__le0 := 0)
((_sk_lra__le0 <= 0) := true))

11
src/tests/regression/dune Normal file
View file

@ -0,0 +1,11 @@
(rule
(targets reg_model_lra1.out)
(deps reg_model_lra1.smt2)
(action (with-stdout-to %{targets} (bash "../../main/main.exe %{deps} | tail -n +2"))))
(alias
(name runtest)
(locks /test)
(package sidekick-bin)
(action (diff reg_model_lra1.out.expected reg_model_lra1.out)))

11
src/tests/regression/reg_model_lra1.out.expected Normal file
View file

@ -0,0 +1,11 @@
(model
(true := true)
(false := false)
(a := 5/3)
(_sk_lra__le0 := 5)
((to_real _sk_lra__le0) := 5)
((= 5 (to_real _sk_lra__le0)) := true)
(((to_real _sk_lra__le0) >= 5) := true)
(((to_real _sk_lra__le0) <= 5) := true)
((a <= 5/3) := true)
((a >= 5/3) := true))

6
src/tests/regression/reg_model_lra1.smt2 Normal file
View file

@ -0,0 +1,6 @@
(set-logic QF_LRA)
(declare-const a Real)
(assert (= (* 3 a) 5))
(check-sat)
(get-model)