Commit d7a230da authored by MARCHE Claude's avatar MARCHE Claude

Better support for div and mod by SMT solvers CVC4 and veriT

parent 89c2faca
......@@ -33,7 +33,7 @@ timeout "interrupted by timeout"
(* Disabled:
CVC4 division seems to be neither the Euclidean one, nor the Computer one
*)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -43,6 +43,7 @@ theory int.EuclideanDivision
remove prop Div_1
end
(*
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......
......@@ -47,6 +47,7 @@ stepslimitexceeded "??"
(* Disabled:
CVC4 division seems to be neither the Euclidean one, nor the Computer one
*)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
......@@ -57,6 +58,7 @@ theory int.EuclideanDivision
remove prop Div_1
end
(*
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......
......@@ -29,6 +29,15 @@ transformation "simplify_formula"
transformation "encoding_smt"
transformation "encoding_sort"
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
(*
Local Variables:
......
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment