Merge branch 'dev' into feat_smt

.github/workflows/continuousIntegration.yml

@@ -16,7 +16,6 @@ jobs:
   forge-tests:
     runs-on: ubuntu-latest
     container: docker://karimmouline/forge-dev-img:latest
-
     steps:
     - name: Checkout repo
       uses: actions/checkout@v3

forge/examples/prim/prim.frg

@@ -159,7 +159,7 @@ pred difflengthedges_2 {
 // Are 2 of these options equivalent? If yes, our confidence increases:
 test expect {
   {wellformedgraph implies {difflengthedges iff difflengthedges_2}}
-    for 5 Node is theorem
+    for 5 Node is checked
 }
 
 -- Find a graph where all possible edges are present (at some weight)

forge/lang/alloy-syntax/lexer.rkt

@@ -111,7 +111,8 @@
    ["test"      (token+ `TEST-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["theorem"   (token+ `THEOREM-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["forge_error" (token+ `FORGE_ERROR-TOK "" lexeme "" lexeme-start lexeme-end)]
-   ["two"       (token+ `TWO-TOK "" lexeme "" lexeme-start lexeme-end)]
+   ["checked"   (token+ `CHECKED-TOK "" lexeme "" lexeme-start lexeme-end)]
+   ;["two"       (token+ `TWO-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["univ"      (token+ `UNIV-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["unsat"     (token+ `UNSAT-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["unknown"   (token+ `UNKNOWN-TOK "" lexeme "" lexeme-start lexeme-end)]  
@@ -151,6 +152,7 @@
    ["'"  (token+ `PRIME-TOK "" lexeme "" lexeme-start lexeme-end)]      
 
    ; Tokenize this to prevent it from being used as a sig/relation name
+   ; (Not intended to be a user-facing error message.)
    ["Time"      (token+ `TIME-TOK "" lexeme "" lexeme-start lexeme-end)]
 
    ;; int stuff
@@ -174,7 +176,7 @@
 
    ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    ;; identifiers   
-   ; Don't allow priming
+   ; Don't allow priming, as this is now semantic ("next state")
    [(: (or alphabetic "@" "_") (* (or alphabetic numeric "_" "\"")))   ;; "’" "”"
     (token+ 'IDENTIFIER-TOK "" lexeme "" lexeme-start lexeme-end #f #t)]
    [(* (char-set "➡️"))   ;; "’" "”"
@@ -228,12 +230,14 @@
            "some"
            "sum"
            "test"
-           "two"
+           ;"two"
            "expect"
            "sat"
            "unsat"
            "unknown"
            "theorem"
+           "forge_error"
+           "checked"
            "univ"
            "break"
 

forge/lang/alloy-syntax/parser.rkt

@@ -87,7 +87,7 @@ AssertDecl : /ASSERT-TOK Name? Block
 CmdDecl :  (Name /COLON-TOK)? (RUN-TOK | CHECK-TOK) (QualName | Block)? Scope? (/FOR-TOK Bounds)?
 
 TestDecl : (Name /COLON-TOK)? (QualName | Block) Scope? (/FOR-TOK Bounds)? /IS-TOK
-           (SAT-TOK | UNSAT-TOK | UNKNOWN-TOK | THEOREM-TOK | FORGE_ERROR-TOK (PATH-OR-STR-TOK)? )
+           (SAT-TOK | UNSAT-TOK | UNKNOWN-TOK | THEOREM-TOK | FORGE_ERROR-TOK (PATH-OR-STR-TOK)? | CHECKED-TOK )
 TestExpectDecl : TEST-TOK? EXPECT-TOK Name? TestBlock
 TestBlock : /LEFT-CURLY-TOK TestDecl* /RIGHT-CURLY-TOK
 Scope : /FOR-TOK Number (/BUT-TOK @TypescopeList)?

forge/lang/expander.rkt

@@ -336,7 +336,7 @@
                               pred-block:BlockClass))
               (~optional scope:ScopeClass)
               (~optional bounds:BoundsClass)
-              (~or "sat" "unsat" "unknown" "theorem" (~seq "forge_error" (~optional msg:string))))))
+              (~or "sat" "unsat" "unknown" "theorem" "checked" (~seq "forge_error" (~optional msg:string))))))
 
   ; TestBlock : /LEFT-CURLY-TOK TestDecl* /RIGHT-CURLY-TOK
   (define-syntax-class TestBlockClass
@@ -988,7 +988,7 @@
                                         preds:BlockClass))
                         (~optional scope:ScopeClass)
                         (~optional bounds:BoundsClass)
-                        (~and expected (~or "sat" "unsat" "unknown" "theorem" "forge_error"))
+                        (~and expected (~or "sat" "unsat" "unknown" "theorem" "forge_error" "checked"))
                         (~optional expected-details))
    (with-syntax ([name #`(~? name.name #,(make-temporary-name stx))]
                  [preds #'(~? pred.name preds)]
@@ -1028,7 +1028,7 @@
         #:preds [imp_total]
         #:scope pwd.scope
         #:bounds pwd.bounds
-        #:expect theorem ))]))
+        #:expect checked ))]))
 
 
 (define-syntax (QuantifiedPropertyDecl stx)
@@ -1062,7 +1062,7 @@
          #:preds [imp_total]
          #:scope qpd.scope
          #:bounds qpd.bounds
-         #:expect theorem )))]))
+         #:expect checked )))]))
 
 
 (define-syntax (SatisfiabilityDecl stx)

forge/logging/2023/main.rkt

@@ -62,8 +62,13 @@
 
 (define (setup language port path)
   (define peek-port (peeking-input-port port))
-  (define project (read peek-port))
-  (define user (read peek-port))
+  (define-values [project user]
+    (let* ((err? (lambda (ee) (or (exn:fail:contract? ee) (exn:fail:read? ee))))
+           (default (lambda (ee) (list #f #f)))
+           (res*
+            (with-handlers ((err? default))
+              (list (read peek-port) (read peek-port)))))
+      (apply values res*)))
   (close-input-port peek-port)
   (if (and (string? project) (string? user))
       (let ((got-data-file? (path-string? (get-log-file))))

forge/sigs-functional.rkt

@@ -760,7 +760,7 @@
         #:command syntax?)
        void?)
   (cond
-    [(equal? expected 'theorem)
+    [(equal? expected 'checked)
      (let* ([test-check (check-from-state state
                                           #:name name
                                           #:preds preds
@@ -772,7 +772,7 @@
                                           #:command command)]
             [first-instance (tree:get-value (Run-result test-check))])
        (if (Sat? first-instance)
-           (raise (format "Theorem ~a failed. Found instance:~n~a"
+           (raise (format "Test ~a failed. Found counterexample instance:~n~a"
                           name first-instance))
            (close-run test-check)))]
     [(or (equal? expected 'sat) (equal? expected 'unsat))
@@ -795,7 +795,7 @@
                               (if (Unsat-core first-instance)
                                   (format " Core: ~a" (Unsat-core first-instance))
                                   ""))))))]
-    [else (raise (format "Illegal argument to test. Received ~a, expected sat, unsat, or theorem."
+    [else (raise (format "Illegal argument to test. Received ~a, expected sat, unsat, or checked."
                          expected))]))
 
 ; Creates a new run to use for a test, then calls test-from-run

forge/sigs.rkt

@@ -632,12 +632,11 @@
                            #:command run-command))
          (update-state! (state-add-runmap curr-state 'name name))))]))
 
-; Test that a spec is sat or unsat
-; (test name
-;       [#:preds [(pred ...)]] 
-;       [#:scope [((sig [lower 0] upper) ...)]]
-;       [#:bounds [bound ...]]
-;       [|| sat unsat]))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Primary testing form: check whether a constraint-set, under
+; some provided bounds, is sat, unsat, or an error. 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (define-syntax (test stx)
   (syntax-case stx ()
     [(test name args ... #:expect expected)
@@ -706,29 +705,33 @@
                 #:run name)
                (close-run name))]
 
-          [(equal? 'expected 'theorem)          
+          [(equal? 'expected 'checked)
            ;#,(syntax/loc stx (check name args ...))
            check-stx
            (define first-instance (tree:get-value (Run-result name)))
            (cond [(Sat? first-instance)
                   (report-test-failure #:name 'name
-                                       #:msg (format "Theorem ~a failed. Found instance:~n~a"
+                                       #:msg (format "Test ~a failed. Found counterexample instance:~n~a"
                                                      'name first-instance)
                                        #:context loc
                                        #:instance first-instance
                                        #:run name)]
                  [(Unknown? first-instance)
                   (report-test-failure #:name 'name
-                                       #:msg (format "Theorem ~a failed. Solver returned Unknown.~n"
+                                       #:msg (format "Test ~a failed. Solver returned Unknown.~n"
                                                      'name)
                                        #:context loc
                                        #:instance first-instance
                                        #:run name)]
                  [else 
                   (close-run name)])]
 
+          [(equal? 'expected 'theorem)
+           (raise-forge-error #:msg "The syntax 'is theorem' is deprecated and will be re-enabled in a future version for complete solver backends only; use 'is checked' instead."
+                              #:context loc)]
+
           [else (raise-forge-error                 
-                 #:msg (format "Illegal argument to test. Received ~a, expected sat, unsat, theorem, or forge_error."
+                 #:msg (format "Illegal argument to test. Received ~a, expected sat, unsat, checked, or forge_error."
                                'expected)
                  #:context loc)]))))]))
 

forge/tests/error/failed_theorem.frg

@@ -5,5 +5,5 @@ option verbose 0
 sig Cell {}
 
 test expect {    
-    foo: {Cell != Cell} is theorem    
+    foo: {Cell != Cell} is checked    
 }

forge/tests/error/is_theorem_disabled.frg

@@ -0,0 +1,5 @@
+#lang forge
+
+test expect { 
+  {} is theorem
+}

forge/tests/error/main.rkt

@@ -155,7 +155,7 @@
     (list "failed_sat.frg" #rx"Failed test") 
     ;;; ? after * makes the match lazy, meaning it will match as few characters as possible while still allowing the remainder of the regular expression to match.
 
-    (list "multiple_test_failures.frg" #rx".*?Assertion_All_isRoot_is_necessary_for_isNotRoot failed.*?Invalid example 'thisIsNotATree'.*?Theorem t1 failed")
+    (list "multiple_test_failures.frg" #rx".*?Assertion_All_isRoot_is_necessary_for_isNotRoot failed.*?Invalid example 'thisIsNotATree'.*?Test t1 failed")
     (list "properties_undirected_tree_underconstraint_multiple_errors.frg" #rx".*?Assertion_TreeWithEdges_is_necessary_for_isUndirectedTree failed.*?Assertion_All_TreeWithEdges_is_necessary_for_isUndirectedTree failed")
     (list "properties_undirected_tree_overconstraint_error.frg" #rx"Assertion_isUndirected_is_sufficient_for_isUndirectedTree failed.")
     (list "properties_directed_tree_sufficiency_error.frg" #rx"Assertion_All_arethesame_is_sufficient_for_bothRoots failed.")
@@ -210,6 +210,10 @@
 
     ;; priming error tests
     (list "priming-basic.frg" #rx"Prime operator used in non-temporal context")
+
+    ;; The "is theorem" test construct is temporarily disabled in favor of "is checked";
+    ;; it will be re-enabled for complete solver backends only
+    (list "is_theorem_disabled.frg" #rx"use 'is checked' instead")
   ))
 
 

forge/tests/error/multiple_test_failures.frg

@@ -34,5 +34,5 @@ example thisIsNotATree is {isDirectedTree} for {
 }
 
 test expect {
-    t1 : {some r1 : Node | isRoot[r1]} is theorem
+    t1 : {some r1 : Node | isRoot[r1]} is checked
 }

forge/tests/error/parsing_less_dash.frg

@@ -7,5 +7,5 @@ test expect {
     parsing_should_error: {
         (Person.age <- 1)
         iff
-        (Person.age < -1)} is theorem
+        (Person.age < -1)} is checked
 }

forge/tests/forge-core/expressions/expressionOperators.rkt

@@ -95,20 +95,20 @@
               (set ([n1 Node] [n2 Node]) (&& (in (-> n1 n2) edges)
                                               (in n2 (join n edges)))))))
 
-(test tilde #:preds [Tilde] #:expect theorem)
-(test caret #:preds [Caret] #:expect theorem)
-(test star #:preds [Star] #:expect theorem)
-(test plus #:preds [Plus] #:expect theorem)
-(test minus #:preds [Minus] #:expect theorem)
-(test ampersandd #:preds [Ampersand] #:expect theorem)
-(test arrow #:preds [Arrow] #:expect theorem)
-(test dot #:preds [Dot] #:expect theorem)
+(test tilde #:preds [Tilde] #:expect checked)
+(test caret #:preds [Caret] #:expect checked)
+(test star #:preds [Star] #:expect checked)
+(test plus #:preds [Plus] #:expect checked)
+(test minus #:preds [Minus] #:expect checked)
+(test ampersandd #:preds [Ampersand] #:expect checked)
+(test arrow #:preds [Arrow] #:expect checked)
+(test dot #:preds [Dot] #:expect checked)
 
 (test ite1 #:preds [IfThenElse1] #:expect unsat)
 (test ite2 #:preds [IfThenElse2] #:expect unsat)
 
-(test domainRestriction #:preds [DomainRestriction] #:expect theorem)
-(test rangeRestriction #:preds [RangeRestriction] #:expect theorem)
+(test domainRestriction #:preds [DomainRestriction] #:expect checked)
+(test rangeRestriction #:preds [RangeRestriction] #:expect checked)
 
 
 ; Helper functions `fun`
@@ -148,7 +148,7 @@
               (= (helper2d value1 value2) (& value2 value1))
               (= (helper2e value1 value2) (& value2 value1))
               (= (helper2f value1 value2) (& value2 value1)))))
-(test helperfuns #:preds [HelperFun] #:expect theorem)
+(test helperfuns #:preds [HelperFun] #:expect checked)
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

forge/tests/forge-core/expressions/setComprehensions.rkt

@@ -43,12 +43,12 @@
 (test comprehensionsOnSigs 
       #:preds [ComprehensionsOnSigs]
       #:bounds [relations]
-      #:expect theorem)
+      #:expect checked)
 (test comprehensionsOnSets
       #:preds [ComprehensionsOnSets]
       #:bounds [relations]
-      #:expect theorem)
+      #:expect checked)
 (test multiComprehension
       #:preds [MultiComprehension]
       #:bounds [relations]
-      #:expect theorem)
+      #:expect checked)

forge/tests/forge-core/formulas/booleanFormulaOperators.rkt

@@ -62,22 +62,22 @@
 
 (test basicTrueFalse 
       #:preds [TrueFalse]
-      #:expect theorem)
+      #:expect checked)
 (test notOps 
       #:preds [Not]
-      #:expect theorem)
+      #:expect checked)
 (test andOps 
       #:preds [And]
-      #:expect theorem)
+      #:expect checked)
 (test orOps 
       #:preds [Or]
-      #:expect theorem)
+      #:expect checked)
 (test xorOps 
       #:preds [Xor]
-      #:expect theorem)
+      #:expect checked)
 (test impliesOps 
       #:preds [Implies]
-      #:expect theorem)
+      #:expect checked)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ; Test helper predicates and captured metadata
@@ -101,7 +101,7 @@
               (iff (pred2d value1 value2) (and (in value1 Int) (in value2 Int)))
               ; cannot easily test higher-order helper predicate with forall, so pred_arity2_arg is left out here
               )))
-(test helperpreds #:preds [HelperPred] #:expect theorem)
+(test helperpreds #:preds [HelperPred] #:expect checked)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ; Test metadata

forge/tests/forge-core/formulas/disj-all-core.rkt

@@ -9,7 +9,7 @@
 
 (pred oneVarall (all ([n0 Node]) (in n0 (join Node edges))))
 (pred oneVarallDisj (all #:disj ([n0 Node]) (in n0 (join Node edges))))
-(test oneall #:preds [(iff oneVarall oneVarallDisj)] #:expect theorem)
+(test oneall #:preds [(iff oneVarall oneVarallDisj)] #:expect checked)
 
 (pred twoVarall
       (all ([n1 Node] [n2 Node])
@@ -18,7 +18,7 @@
 (pred twoVarallDisj
       (all #:disj ([n1 Node] [n2 Node])
         (in n1 (join n2 edges))))
-(test twoall #:preds [(iff twoVarall twoVarallDisj)] #:expect theorem)
+(test twoall #:preds [(iff twoVarall twoVarallDisj)] #:expect checked)
 
 (pred manyVarall
       (all ([n0 Node] [n1 Node] [n2 Node] [n3 Node])
@@ -30,4 +30,4 @@
     (all #:disj ([n0 Node] [n1 Node] [n2 Node] [n3 Node])
         (&& (in (-> n1 n2) edges)
             (in (-> n3 n0) edges))))
-(test manyall #:preds [(iff manyVarall manyVarallDisj)] #:expect theorem)
+(test manyall #:preds [(iff manyVarall manyVarallDisj)] #:expect checked)

forge/tests/forge-core/formulas/disj-lone-core.rkt

@@ -8,7 +8,7 @@
 
 (pred loneVarlone (lone ([n0 lonede]) (in n0 (join lonede edges))))
 (pred loneVarloneDisj (lone #:disj ([n0 lonede]) (in n0 (join lonede edges))))
-(test lonelone #:preds [(iff loneVarlone loneVarloneDisj)] #:expect theorem)
+(test lonelone #:preds [(iff loneVarlone loneVarloneDisj)] #:expect checked)
 
 (pred twoVarlone
       (lone ([n1 lonede] [n2 lonede])
@@ -17,7 +17,7 @@
 (pred twoVarloneDisj
       (lone #:disj ([n1 lonede] [n2 lonede])
         (in n1 (join n2 edges))))
-(test twoVar #:preds [(iff twoVarlone twoVarloneDisj)] #:expect theorem)
+(test twoVar #:preds [(iff twoVarlone twoVarloneDisj)] #:expect checked)
 
 (pred manyVarlone
       (lone ([n0 lonede] [n1 lonede] [n2 lonede] [n3 lonede])
@@ -29,4 +29,4 @@
     (lone #:disj ([n0 lonede] [n1 lonede] [n2 lonede] [n3 lonede])
         (&& (in (-> n1 n2) edges)
             (in (-> n3 n0) edges))))
-(test manylone #:preds [(iff manyVarlone manyVarloneDisj)] #:expect theorem)
+(test manylone #:preds [(iff manyVarlone manyVarloneDisj)] #:expect checked)