Wrap negative numbers for earlier cvc5 versions

forge/examples/smt/factorization.frg

@@ -0,0 +1,53 @@
+#lang forge
+
+/*
+  Factoring a polynomial. This in includes 2 versions:
+    - the naive/complicated/unreliable way (universal quantification over Ints)
+    - the simple way (existentials only)
+  August 2024, Tim
+*/
+
+option no_overflow true  -- in case we return to the default engine
+option backend smtlibtor -- use the cvc5 theory-of-relations backend
+
+option verbose 3
+
+one sig I {
+    root1, root2: one Int
+}
+
+test expect {
+    -- (x + 123)(x - 321) = x^2 - 198x - 39483 
+
+    -- If we encode the actual equation, we get an overcomplicated version:
+    factorPolynomialIntsHardWay: { 
+    all x: Int | { 
+        // (xi + r1i) * (xi + r2i) 
+        multiply[add[x, I.root1], add[x, I.root2]]
+        =
+        // (xi * xi) + (198 * xi) - 39483))
+        subtract[add[multiply[x, x], multiply[198, x]], 39483]
+    }} is sat
+
+    -- If we encode what "root" really means, we get a simpler version:
+    factorPolynomialEasyWay: {
+        0 = subtract[add[multiply[I.root1, I.root1], multiply[198, I.root1]], 39483]
+        0 = subtract[add[multiply[I.root2, I.root2], multiply[198, I.root2]], 39483]
+        root1 != root2
+    } is sat
+
+    -- Should only be ONE such pair
+    factorPolynomialEasyWay_unique_solution: {
+        0 = subtract[add[multiply[I.root1, I.root1], multiply[198, I.root1]], 39483]
+        0 = subtract[add[multiply[I.root2, I.root2], multiply[198, I.root2]], 39483]
+        I.root1 != I.root2
+
+        -- Neither root can be 123
+        I.root1 != 123 
+        I.root2 != 123
+        -- Neither root can be -321
+        I.root1 != -321
+        I.root2 != -321
+
+    } is unsat
+}

forge/examples/smt/pythagorean.frg

@@ -0,0 +1,89 @@
+#lang forge
+
+/*
+  Expressing the 2024 1710 SMT assignment in Forge. Forge doesn't have reals at the
+  moment, but using this to extract the shape of SMT query so I can manually 
+  convert it and test how the theory would work in the current engine.
+
+  (1) Pythagorean Triples, Part 1. Forge can prove this (ints) within a bound. 
+  (2) Pythagorean Triples, Part 2. Forge can find a counterexample (ints), but it needs a higher bitwidth.
+      E.g., n=2,m=4 needs to represent z = (2^2+4^2) = 20, and then to square z = 400, 
+      which needs 10 bits: [-512, 511]. 
+
+  (3) Let's try factorization. Ints first:
+     (x + 123)(x - 321) = x^2 - 198x - 39483
+   
+  (4) Let's try factorization in the Reals; this requires copy/paste and replacing 
+      sort names in the output SMT (for now), but gives us a good sense of whether 
+      it might be straightforward to support Reals. 
+
+  TN Aug 2024
+*/
+
+option no_overflow true  -- in case we return to the default engine
+option backend smtlibtor -- use the cvc5 theory-of-relations backend
+
+---------------------------------------------------------------------------------------------------
+
+/** 
+  x, y, z is a Pythagorean triple if x^2 + y^2 = z^2.
+*/
+pred isPythagoreanTriple[x,y,z: Int] {
+    x > 0 
+    y > 0
+    z > 0
+    let xsq = multiply[x, x], ysq = multiply[y,y], zsq = multiply[z,z] | {
+        add[xsq,ysq] = zsq        
+    }
+}
+
+/**
+  A triple is primitive if its elements have no common factors besides 1.
+  (Note: the handout is somewhat ambiguous there. Is it pairwise coprime, or collective coprime?)
+*/
+pred isPrimitive[x, y, z: Int] {
+    all d: Int | d > 1 => {
+        remainder[x, d] != 0 or
+        remainder[y, d] != 0 or
+        remainder[z, d] != 0
+    }
+}
+
+test expect {
+    /** Generate a triple using the m,n method. */
+    pt1: {
+        all m, n: Int | (m > n and n > 0) => {
+            let msq = multiply[m, m], nsq = multiply[n,n] | {
+                isPythagoreanTriple[subtract[msq, nsq], multiply[2, multiply[m, n]], add[msq, nsq]]
+            }
+        }
+    } is theorem
+
+    /** Generate a non-primitive triple using the m,n method. */
+    pt2: {
+        some m, n: Int | let msq = multiply[m, m], nsq = multiply[n,n] | { 
+            m > n
+            n > 0             
+            isPythagoreanTriple[subtract[msq, nsq], multiply[2, multiply[m, n]], add[msq, nsq]]
+            not isPrimitive[subtract[msq, nsq], multiply[2, multiply[m, n]], add[msq, nsq]]
+        }
+    -- In normal Forge, this requires a high bitwidth, so that the squares etc. can be represented.
+    -- In SMT, this won't matter (or even be considered by the solver).
+    } for 10 Int is sat
+
+}
+
+-- tests for universally quantified Ints
+test expect {
+    /** Find a _primitive_ triple via the m,n method. 
+        Note that in contrast to the above, this requires *universal* quantification. */
+    test_with_universals_find_primitive: {
+        -- exists-forall, not exists-exists
+        some m, n: Int | (m > n and n > 0) and {
+            let msq = multiply[m, m], nsq = multiply[n,n] | {
+                isPythagoreanTriple[subtract[msq, nsq], multiply[2, multiply[m, n]], add[msq, nsq]]
+                isPrimitive[        subtract[msq, nsq], multiply[2, multiply[m, n]], add[msq, nsq]]
+            }
+        }
+    } is sat
+}

forge/utils/to-smtlib-tor.rkt

@@ -14,7 +14,7 @@
   (only-in racket index-of match string-join first second rest flatten last drop-right third empty remove-duplicates empty? filter-map member)
   (only-in racket/contract define/contract or/c listof any/c)
   (prefix-in @ (only-in racket/contract -> ->*))
-  (prefix-in @ (only-in racket/base >= > - + <)))
+  (prefix-in @ (only-in racket/base >= > - + < *)))
 
 (provide convert-formula get-new-top-level-strings)
 
@@ -515,7 +515,9 @@
   (match expr
     [(node/int/constant info value)
      (cond 
-      [int-ctxt value]
+      [int-ctxt
+       ; Older versions of cvc5, and SMT lib in general, like negative ints to be wrapped.
+       (if (< value 0) `(- ,(@* -1 value)) value)]
       [else         
         (define const-name (string->symbol (format "_~a_atom" (gensym))))
         (define new-decl `(declare-const ,const-name IntAtom))