pretty-printing of rationals, bug #15

uuverifiers · Oct 13, 2024 · b30a220 · b30a220
1 parent 552b18c
commit b30a220
Show file tree

Hide file tree

Showing 4 changed files with 73 additions and 51 deletions.
diff --git a/src/main/scala/ap/parser/SMTLineariser.scala b/src/main/scala/ap/parser/SMTLineariser.scala
@@ -767,8 +767,11 @@ object SMTLineariser {
             None
           }
         }
-      case Some(Rationals) if fun == Rationals.frac =>
-        Some(("/", ""))
+      case Some(Rationals) => fun match {
+        case Rationals.frac => Some(("/", ""))
+        case Rationals.int  => Some(("/", "1"))
+        case _              => None
+      }
       case Some(ModuloArithmetic) => fun match {
         case ModuloArithmetic.int_cast => Some(("bv2nat", ""))
         case ModuloArithmetic.bv_add   => Some(("bvadd", ""))

diff --git a/testcases/api/TestRat.scala → ...scala/ap/theories/rationals/TestRat.scala b/testcases/api/TestRat.scala → ...scala/ap/theories/rationals/TestRat.scala
@@ -3,7 +3,7 @@
  * arithmetic with uninterpreted predicates.
  * <http://www.philipp.ruemmer.org/princess.shtml>
  *
- * Copyright (C) 2020 Philipp Ruemmer <ph_r@gmx.net>
+ * Copyright (C) 2020-2024 Philipp Ruemmer <ph_r@gmx.net>
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -31,27 +31,89 @@
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  */
 
-// package ap.theories.rationals
+package ap.theories.rationals
 
 import ap.parser._
 import ap.SimpleAPI
-import ap.theories.rationals.Rationals
 
-object TestRat extends App {
+import org.scalacheck.Properties
+import ap.util.ExtraAssertions
+import ap.util.Prop._
+
+class TestRat extends Properties("TestRat") with ExtraAssertions {
+
+  val expectedOutput = """
+-- Printing Literals
+Rat_int(0)
+Rat_int(1)
+(/ 0 1)
+(/ 1 1)
+(/ 42 1)
+(/ 1 2)
+
+-- Test 1
+Rat_frac(1, 12)
+Sat
+{x -> Rat_frac(1, 12), Rat_denom -> 12}
+
+-- Test 2
+Sat
+{y -> Rat_frac(-99, 10), x -> Rat_frac(0, 1), Rat_denom -> 10}
+
+-- Test 3
+Sat
+{x -> Rat_frac(3, 5), Rat_denom -> 5}
+Sat
+{y -> Rat_frac(5, 3), x -> Rat_frac(3, 5), Rat_denom -> 15}
+
+-- Test 4
+Valid
+
+-- Test 5
+Invalid
+{y -> Rat_frac(-3, 2), x -> Rat_frac(-3, 2), Rat_denom -> 2}
+
+-- Test 6
+Sat
+{x -> Rat_frac(-4, 3), Rat_denom -> 9}
+Rat_frac(-4, 3)
+
+-- Test 7
+Sat
+{y -> Rat_frac(1, 2), x -> Rat_frac(5, 1), Rat_denom -> 2}
+
+-- Test 8
+Sat
+{y -> Rat_frac(1, 2), x -> Rat_frac(5, 1), Rat_denom -> 2}
+
+-- Test 9
+Sat
+{y -> Rat_frac(-1, 1), x -> Rat_frac(-11, 1), Rat_denom -> 1}
+"""
 
   def part(str : String) = {
     println
     println("-- " + str)
   }
 
+  property("TestRat") = checkOutput(expectedOutput) {
   SimpleAPI.withProver(enableAssert = true) { p =>
+    ap.util.Debug.enableAllAssertions(true)
     import p._
     import Rationals._
     import IExpression._
 
+    part("Printing Literals")
+
     println(zero)
     println(one)
 
+    println(smtPP(zero))
+    println(smtPP(one))
+
+    println(smtPP(int2ring(42)))
+    println(smtPP(frac(1, 2)))
+
     val x = createConstant("x", dom)
     val y = createConstant("y", dom)
 
@@ -132,5 +194,6 @@ object TestRat extends App {
       println(partialModel)
     }
   }
+  }
 
 }
diff --git a/testcases/api/Answers b/testcases/api/Answers
@@ -1,47 +1,4 @@
 
-TestRat
-Rat_int(0)
-Rat_int(1)
-
--- Test 1
-Rat_frac(1, 12)
-Sat
-{x -> Rat_frac(1, 12), Rat_denom -> 12}
-
--- Test 2
-Sat
-{y -> Rat_frac(-99, 10), x -> Rat_frac(0, 1), Rat_denom -> 10}
-
--- Test 3
-Sat
-{x -> Rat_frac(3, 5), Rat_denom -> 5}
-Sat
-{y -> Rat_frac(5, 3), x -> Rat_frac(3, 5), Rat_denom -> 15}
-
--- Test 4
-Valid
-
--- Test 5
-Invalid
-{y -> Rat_frac(-3, 2), x -> Rat_frac(-3, 2), Rat_denom -> 2}
-
--- Test 6
-Sat
-{x -> Rat_frac(-4, 3), Rat_denom -> 9}
-Rat_frac(-4, 3)
-
--- Test 7
-Sat
-{y -> Rat_frac(1, 2), x -> Rat_frac(5, 1), Rat_denom -> 2}
-
--- Test 8
-Sat
-{y -> Rat_frac(1, 2), x -> Rat_frac(5, 1), Rat_denom -> 2}
-
--- Test 9
-Sat
-{y -> Rat_frac(-1, 1), x -> Rat_frac(-11, 1), Rat_denom -> 1}
-
 TestSaturationProcedure
 Valid
 Unsat

diff --git a/testcases/api/runtests b/testcases/api/runtests
@@ -9,8 +9,7 @@ RUNOPTIONS="-cp `pwd`/../../bin:."
 
 export JAVA_OPTS="-Xss20000k -Xmx1500m"
 
-TESTS="TestRat \
-       TestSaturationProcedure"
+TESTS="TestSaturationProcedure"
 
 for testname in $TESTS; do
   echo