fix: skolem depth 0 only; cleanup

forge/lang/bounds.rkt

@@ -12,7 +12,7 @@
 
 ; Error-checking constructors for bounds
 (define (make-bound relation lower upper)
-  (printf "make-bound; upper was: ~a~n" upper)
+  ;(printf "make-bound; upper was: ~a~n" upper)
   (for ([t (in-list lower)])
     (unless (and (list? t) (= (length t) (relation-arity relation)))
       (raise-arguments-error 'make-bound (format "lower bounds must contain tuples of arity ~a" (relation-arity relation)) "lower" t)))

forge/solver-specific/cvc5-tor.rkt

@@ -73,30 +73,43 @@
                            (bound-upper b)))
              ; Declare the "used" relation for this sig
              name name)]
+    ; Skolem relation of arity 1
+    [(equal? (string-ref name 0) #\$)
+     ; Temporarily disable situations where Skolem relations would need to be non-nullary
+     ; this "as uninterpreted function" approach required us to wrap references to these
+     ; in (singleton (tuple ...)) in to-smtlib-tor.rkt.
+     (unless (equal? arity 1)
+       (raise-forge-error #:msg (format "SMT backend does not currently support problems that require Skolemization depth > 0; ~a had arity ~a." name arity)
+                          #:context #f))
+     (format "(declare-const ~a ~a)~n" name (deparen (map sort-name-of typenames)))]
     ; Fields
     [else
      (format "(declare-fun ~a () (Relation ~a))~n" name (deparen (map sort-name-of typenames)))]))
 
 (define (translate-to-cvc5-tor run-spec all-atoms relations total-bounds step0)
-  ; For now, just print constraints, etc. 
+  ; For now, just print constraints, etc.
+  (printf "~n********************************~n")
   (printf "Translating to CVC5 theory-of-relations~nConstraints:~n")
 
   ; Last version pre-solver, pre-SMT conversion
-  (printf "~nStep 0 (from Forge):~n")
-  (for ([constraint step0])
-    (printf "  ~a~n" constraint))
+  (when (@> (get-verbosity) VERBOSITY_LOW)
+    (printf "~nStep 0 (from Forge):~n")
+    (for ([constraint step0])
+      (printf "  ~a~n" constraint)))
 
   ; Convert to negation normal form
   (define step1 (map (lambda (f) (nnf:interpret-formula run-spec f relations all-atoms '())) step0))
-  (printf "~nStep 1 (post NNF conversion):~n")
-  (for ([constraint step1])
-    (printf "  ~a~n" constraint))
+  (when (@> (get-verbosity) VERBOSITY_LOW)
+    (printf "~nStep 1 (post NNF conversion):~n")
+    (for ([constraint step1])
+      (printf "  ~a~n" constraint)))
 
   ; Convert boxed integer references to existential quantifiers
   (define step2 (map (lambda (f) (boxed-int:interpret-formula run-spec f relations all-atoms '())) step1))
-  (printf "~nStep 2 (post boxed-integer translation):~n")
-  (for ([constraint step2])
-    (printf "  ~a~n" constraint))
+  (when (@> (get-verbosity) VERBOSITY_LOW)
+    (printf "~nStep 2 (post boxed-integer translation):~n")
+    (for ([constraint step2])
+      (printf "  ~a~n" constraint)))
 
   ; Skolemize (2nd empty list = types for quantified variables, unneeded in other descents)
   ; Note that Skolemization changes the *final* bounds. There is no Run struct for this run yet;
@@ -114,19 +127,20 @@
 
   (define step3 (first step3-both))
   (define step3-bounds (second step3-both))
-  (printf "~nStep 3 (post Skolemization):~n")
-  (for ([constraint step3])
-    (printf "  ~a~n" constraint))
+  (when (@> (get-verbosity) VERBOSITY_LOW)
+    (printf "~nStep 3 (post Skolemization):~n")
+    (for ([constraint step3])
+      (printf "  ~a~n" constraint)))
 
   (define step4 (map (lambda (f) (smt-tor:convert-formula run-spec f relations all-atoms '())) step3))
-  (printf "~nStep 4 (post SMT-LIB conversion):~n")
-  (for ([constraint step4])
-    (printf "  ~a~n" constraint))
-
-  (printf "~nBounds (post Skolemization):~n")
-  (for ([bound step3-bounds])
-    (printf "  ~a/lower: ~a~n" (bound-relation bound) (bound-lower bound))
-    (printf "  ~a/upper: ~a~n" (bound-relation bound) (bound-upper bound)))
+  (when (@> (get-verbosity) VERBOSITY_LOW)
+    (printf "~nStep 4 (post SMT-LIB conversion):~n")
+    (for ([constraint step4])
+      (printf "  ~a~n" constraint))
+    (printf "~nBounds (post Skolemization):~n")
+    (for ([bound step3-bounds])
+      (printf "  ~a/lower: ~a~n" (bound-relation bound) (bound-lower bound))
+      (printf "  ~a/upper: ~a~n" (bound-relation bound) (bound-upper bound))))
 
   ; Now, convert bounds into SMT-LIB (theory of relations) and assert all formulas
 
@@ -179,16 +193,21 @@
      (begin
        (smtlib-display stdin "(get-model)")
        (define model-s-expression (read stdout))
-       (printf "----- RECEIVED -----~n")
-       (for ([s-expr model-s-expression])
-         (printf "~a~n" s-expr))
-       (printf "--------------------~n")
+       (when (@> (get-verbosity) VERBOSITY_LOW)
+         (printf "----- RECEIVED -----~n")
+         (for ([s-expr model-s-expression])
+           (printf "~a~n" s-expr))
+         (printf "--------------------~n"))
+
        ; Forge still uses the Alloy 6 modality overall: Sat structs contain a _list_ of instances,
        ; each corresponding to the state of the instance at a given time index. Here, just 1.
        (define response (Sat (list (smtlib-tor-to-instance model-s-expression)) #f '()))
-       (printf "~nSAT: ~a~n" response)
+       (when (@> (get-verbosity) VERBOSITY_LOW)
+         (printf "~nSAT: ~a~n" response))
        response)]
     ['unsat
+     (when (@> (get-verbosity) VERBOSITY_LOW)
+       (printf "~nUNSAT~n"))
      ; No cores or statistics yet
      (Unsat #f #f 'unsat)]
     ['unknown

forge/solver-specific/testing/basic.frg → forge/solver-specific/testing/basic_tests.frg

@@ -3,11 +3,12 @@
 -- Test the SMT-LIB Theory-of-Relations translation
 option backend smtlibtor
 
--- Sterling should now get a workable instance
--- option run_sterling off
+-- Sterling should now get a workable instance, but leaving it off here since we are testing
+-- soundness and completeness of the translation, not end-to-end functionality. 
+option run_sterling off
 
--- More debugging output
-option verbose 5 
+-- Enable for more debugging output
+-- option verbose 5 
 
 sig Node {edges: set Node}
 
@@ -20,9 +21,12 @@ test expect {
     } is sat
     {
         -- for every node, there is some in-edge
-        all n: Node | some n2: Node | n in n2.edges
+        -- TODO: not currently supported because of skolem restrictions
+        --all n: Node | some n2: Node | n in n2.edges
         -- for every node, there are no in-edges
         no n: Node  | some n2: Node | n in n2.edges
+        -- Should introduce a contradiction:
+        some n: Node  | some n2: Node | n in n2.edges
     } is unsat
 }
 

forge/utils/to-nnf.rkt

@@ -91,7 +91,11 @@
   (map (lambda (x) (interpret-formula run-or-state (node/formula/op/! info (list x)) relations atom-names quantvars)) args))
 
 (define (negate-quantifier run-or-state new-quantifier decls form relations atom-names quantvars info)
-  (node/formula/quantified info new-quantifier decls (node/formula/op/! info (list (interpret-formula run-or-state form relations atom-names quantvars)))))
+  ; Called in a context like !(some ...) ~~~> (all !...).
+  ; NNF conversion thus needs to recur on the inner formula _including_ the negation.
+  (define negated-inner-form (node/formula/op/! info (list form)))
+  (define nnf-negated-inner-form (interpret-formula run-or-state negated-inner-form relations atom-names quantvars))
+  (node/formula/quantified info new-quantifier decls nnf-negated-inner-form))
 
 (define (interpret-formula-op run-or-state formula relations atom-names quantvars args)
   (when (@>= (get-verbosity) VERBOSITY_DEBUG)
@@ -137,7 +141,8 @@
         [(node/formula/op/! not-info not-children) (interpret-formula run-or-state (car not-children) relations atom-names quantvars)]
         ; Converting quantifiers to NNF
         [(node/formula/quantified quant-info quantifier decls form)
-          (match quantifier 
+          (match quantifier
+            ; !!! 
             ; not (all x | A) = some (x | not A)
             ['all (negate-quantifier run-or-state 'some decls form relations atom-names quantvars quant-info)]
             ; not (some x | A) = all (x | not A)

forge/utils/to-skolem.rkt

@@ -13,7 +13,7 @@
   (only-in racket index-of match string-join first second rest flatten cartesian-product thunk empty?)
   (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 interpret-formula)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -39,7 +39,8 @@
     new-join-expr))
 
 (define (skolemize-formula run-spec total-bounds formula relations atom-names quantvars quantvar-types info quantifier decls form)
-    (printf "skolemize-formula: ~a ~a~n" formula quantvars)
+  (when (@> (get-verbosity) VERBOSITY_LOW)
+    (printf "skolemize-formula: ~a ~a~n" formula quantvars))
   ; RESTRICTION: Because we are mapping top-level sigs to sorts, we have no "univ".
   ; Discuss. May be better to not use sorts (or worse).
   ; TODO: *top level* only! Right now, all sorts get added (For KM: discuss)
@@ -107,7 +108,7 @@
           (first upper-bound-list)
           ; otherwise, build product
           (apply cartesian-product upper-bound-list)))
-    (printf "~nskolem-upper-bound: ~a~n" skolem-upper-bound)
+    ;(printf "~nskolem-upper-bound: ~a~n" skolem-upper-bound)
 
     ; 4. add that new relation to the bounds
     (define skolem-bounds (make-bound skolem-relation '() skolem-upper-bound))

forge/utils/to-smtlib-tor.rkt

@@ -132,15 +132,14 @@
       (printf "to-smtlib-tor: convert-expr: ~a~n" expr))
   (match expr
     [(node/expr/relation info arity name typelist-thunk parent isvar)
-     (if (equal? name "Int")
-         ; *******
-         ; TODO: this is not correct *****
-         ;; ************
-         ;"(as set.universe (Set Int))"
-         "(as set.universe (Relation Int))"
-         (format "~a" name))]
+     ; Declared sigs <A> correspond to sort <ASort>, with <A> as a relation to 
+     ; denote which are used. In contrast, <Int> is the _sort_ in SMT. 
+     (cond [(equal? name "Int") "(as set.universe (Relation Int))"]
+           [(equal? #\$ (string-ref name 0)) (format "(set.singleton (tuple ~a))" name)]
+           [else (format "~a" name)])]
     [(node/expr/atom info arity name)
-     "TODO: ATOM"]
+     (raise-forge-error #:msg (format "direct atom references unsupported by SMT backend")
+                        #:context expr)]
     [(node/expr/fun-spacer info arity name args result expanded)
      (convert-expr run-or-state expanded relations atom-names quantvars)]
     [(node/expr/ite info arity a b c)  
@@ -149,6 +148,7 @@
           [processed-c (convert-expr run-or-state c relations atom-names quantvars)])
      (format "(ite ~a ~a ~a)" processed-a processed-b processed-c))]
     [(node/expr/constant info 1 'Int)
+     ; TODO: Is this production being used? 'Int is a symbol, not expanded to the Int sig?
      "TODO: EXPR CONSTANT? IDK WHAT THIS IS"]
     [(node/expr/constant info arity type)
      "TODO: ANOTHER EXPR CONSTANT? IDK WHAT THIS IS"]