Fix solver tests. (#117)

ufmg-smite · Jun 24, 2024 · 921d31e · 921d31e
1 parent 139bf3d
commit 921d31e
Show file tree

Hide file tree

Showing 7 changed files with 61 additions and 7 deletions.
diff --git a/Test/Solver/Error.expected b/Test/Solver/Error.expected
@@ -1,2 +1,2 @@
 
-Test/Solver/Error.lean:15:0: error: Cannot bind x to symbol of type Int, maybe the symbol has already been defined?
+Test/Solver/Error.lean:26:0: error: Cannot bind x to symbol of type Int, maybe the symbol has already been defined?
diff --git a/Test/Solver/Error.lean b/Test/Solver/Error.lean
@@ -2,14 +2,25 @@ import Smt.Translate.Solver
 
 open Smt Translate Solver
 
+def cvc5.os :=
+  if System.Platform.isWindows then "Win64"
+  else if System.Platform.isOSX then "macOS"
+  else "Linux"
+
+def cvc5.arch :=
+  if System.Platform.target.startsWith "x86_64" then "x86_64"
+  else "arm64"
+
+def cvc5.target := s!"{os}-{arch}-static"
+
 def query : SolverM Result := do
   setLogic "LIA"
   declareConst "x" (.symbolT "Int")
   declareConst "x" (.symbolT "Int")
   checkSat
 
 def main : IO Unit := do
-  let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none
+  let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none
   _ ← StateT.run query ss
 
 #eval main
diff --git a/Test/Solver/Interactive.lean b/Test/Solver/Interactive.lean
@@ -2,6 +2,17 @@ import Smt.Translate.Solver
 
 open Smt Translate Solver
 
+def cvc5.os :=
+  if System.Platform.isWindows then "Win64"
+  else if System.Platform.isOSX then "macOS"
+  else "Linux"
+
+def cvc5.arch :=
+  if System.Platform.target.startsWith "x86_64" then "x86_64"
+  else "arm64"
+
+def cvc5.target := s!"{os}-{arch}-static"
+
 open Term in
 def query : SolverM Result := do
   setLogic "LIA"
@@ -17,7 +28,7 @@ def query : SolverM Result := do
   return res
 
 def main : IO Unit := do
-  let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none
+  let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none
   let (res, ss) ← StateT.run query ss
   _ ← StateT.run exit ss
   println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}"

diff --git a/Test/Solver/Model.lean b/Test/Solver/Model.lean
@@ -2,14 +2,25 @@ import Smt.Translate.Solver
 
 open Smt Translate Solver
 
+def cvc5.os :=
+  if System.Platform.isWindows then "Win64"
+  else if System.Platform.isOSX then "macOS"
+  else "Linux"
+
+def cvc5.arch :=
+  if System.Platform.target.startsWith "x86_64" then "x86_64"
+  else "arm64"
+
+def cvc5.target := s!"{os}-{arch}-static"
+
 def query : SolverM (Result × Sexp) := do
   setLogic "LIA"
   setOption "produce-models" "true"
   declareConst "x" (.symbolT "Int")
   return (← checkSat, ← getModel)
 
 def main : IO Unit := do
-  let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none
+  let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none
   let ((res, model), ss) ← StateT.run query ss
   _ ← StateT.run exit ss
   println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}\n\nmodel:\n{model}"

diff --git a/Test/Solver/Proof.lean b/Test/Solver/Proof.lean
@@ -2,14 +2,25 @@ import Smt.Translate.Solver
 
 open Smt Translate Solver
 
+def cvc5.os :=
+  if System.Platform.isWindows then "Win64"
+  else if System.Platform.isOSX then "macOS"
+  else "Linux"
+
+def cvc5.arch :=
+  if System.Platform.target.startsWith "x86_64" then "x86_64"
+  else "arm64"
+
+def cvc5.target := s!"{os}-{arch}-static"
+
 def query : SolverM Sexp := do
   setLogic "QF_UF"
   assert (.symbolT "false")
   _ ← checkSat
   getProof
 
 def main : IO Unit := do
-  let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none
+  let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none
   let (res, ss) ← StateT.run query ss
   _ ← StateT.run exit ss
   println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: unsat\n\nproof:\n{res}"

diff --git a/Test/Solver/Triv.lean b/Test/Solver/Triv.lean
@@ -2,10 +2,21 @@ import Smt.Translate.Solver
 
 open Smt Translate Solver
 
+def cvc5.os :=
+  if System.Platform.isWindows then "Win64"
+  else if System.Platform.isOSX then "macOS"
+  else "Linux"
+
+def cvc5.arch :=
+  if System.Platform.target.startsWith "x86_64" then "x86_64"
+  else "arm64"
+
+def cvc5.target := s!"{os}-{arch}-static"
+
 def query : SolverM Result := checkSat
 
 def main : IO Unit := do
-  let ss ← createFromKind .cvc5 ".lake/packages/cvc5/.lake/cvc5/bin/cvc5" none
+  let ss ← createFromKind .cvc5 s!".lake/packages/cvc5/.lake/cvc5-{cvc5.target}/bin/cvc5" none
   let (res, ss) ← StateT.run query ss
   _ ← StateT.run exit ss
   println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}"

diff --git a/Test/linarith.expected b/Test/linarith.expected
@@ -15,7 +15,6 @@ Test/linarith.lean:124:9: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:124:13: warning: unused variable `c`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-Test/linarith.lean:145:2: error: [arithPolyNorm]: could not prove x - y = -x + y
 Test/linarith.lean:167:34: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:168:5: warning: unused variable `h5`