strategies are now in the <k> cell. goals in <claim>

prover/build

@@ -40,7 +40,6 @@ other_md_files = [ 'lang/smt-lang.md'
                  , 'strategies/unfolding.md'
                  , 'utils/error.md'
                  , 'utils/instantiate-assumptions.md'
-                 , 'utils/load-named.md'
                  , 'utils/heatcool.md'
                  , 'utils/syntactic-match.md'
                  , 'utils/visitor.md'
@@ -61,8 +60,8 @@ prover_smt  = prover('prover-smt',  '--main-module DRIVER-SMT  --syntax-module D
 # Functional tests
 # ----------------
 
-# prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
-# prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine')
+prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
+prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine')
 
 def log_on_success(file, message):
     return proj.rule( 'log-to-success'
@@ -131,8 +130,11 @@ secondary_tests('qf_shidlia_entl_unsat_tests', 't/test-lists/qf_shidlia_entl.uns
 secondary_tests('qf_shlid_entl_unsat_tests',   't/test-lists/qf_shlid_entl.unsat')
 secondary_tests('shid_entl_unsat_tests',       't/test-lists/shid_entl.unsat')
 
+# TODO: Why are smt tests `-krun` and kore tests `-run`?
+def test_path(name, type):
+    return ".build/t/%s.%s" % (name, type)
 def sl_comp_test_path(name):
-    return ".build/t/SL-COMP18/bench/qf_shid_entl/%s.prover-smt-krun" % (name)
+    return test_path("SL-COMP18/bench/qf_shid_entl/%s" % name, 'prover-smt-krun')
 
 proj.alias('smoke-tests', list(map( sl_comp_test_path, [ 
            "02.tst.smt2"                         , # RList trans 
@@ -145,9 +147,12 @@ proj.alias('smoke-tests', list(map( sl_comp_test_path, [
            "skl2-vc03.smt2"                      , # needs framing but not match-pto 
            "odd-lseg3_slk-5.smt2"                , # needs framing and match-pto 
            "nll-vc01.smt2"                       , # needs large number of unfolding but no kt
-           "ls_nonrec_entail_ls_07.sb.smt2"      , # 6 variable transitivity: ls_nonrec(x,x1) * ... * ls_nonrec(x4,x5) -> ls(x,x5)  - needs large number of kts and unfolding
+           "ls_nonrec_entail_ls_05.sb.smt2"      , # 4 variable transitivity: ls_nonrec(x,x1) * ... * ls_nonrec(x4,x5) -> ls(x,x5)  - needs large number of kts and unfolding
            "ls_lsrev_concat_entail_ls_1.sb.smt2" , # need unfolding within implication context
-          ])))
+          ])) +
+          [ test_path('listSegmentLeft-implies-listSegmentRight.kore', 'prover-kore-run')
+          ]
+          )
 
 # Unit Tests
 # ----------

prover/drivers/base.md

@@ -2,8 +2,8 @@ Configuration
 =============
 
 The configuration consists of a list of goals. The first goal is considered
-active. The `<k>` cell contains the Matching Logic Pattern for which we are
-searching for a proof. The `<strategy>` cell contains an imperative language
+active. The `<claim>` cell contains the Matching Logic Pattern for which we are
+searching for a proof. The `<k>` cell contains an imperative language
 that controls which (high-level) proof rules are used to complete the goal. The
 `<trace>` cell stores a log of the strategies used in the search of a proof and
 other debug information. Eventually, this could be used for constructing a proof
@@ -17,7 +17,7 @@ module PROVER-CONFIGURATION
   syntax Pgm
   syntax Strategy
   syntax CommandLine
-  syntax GoalId ::= ClaimName | Int
+  syntax GoalId ::= AxiomName | Int
 
   configuration
       <prover>
@@ -26,8 +26,8 @@ module PROVER-CONFIGURATION
           <goal multiplicity="*" type="List" format="%1%i%n%2, %3%n%4%n%5n%6%n%7%n%d%8">
             <id format="id: %2"> .K </id>
             <parent format="parent: %2"> .K </parent>
+            <claim> \and(.Patterns) </claim> // TODO: make this optional instead?
             <k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>
-            <strategy> .K </strategy>
             <expected> .K </expected>
             <local-context>
               <local-decl multiplicity="*" type="Set">  .K </local-decl>
@@ -83,15 +83,14 @@ module DRIVER-BASE
   imports VISITOR
   imports PATTERN-LENGTH
   imports HEATCOOL-RULES
-  imports LOAD-NAMED-RULES
 
   rule <k> .CommandLine => .K ... </k>
 
   rule <goals>
          <goal>
            <id> .K </id>
            <expected> .K </expected>
-           <strategy> .K </strategy>
+           <k> .K </k>
            ...
          </goal>
        </goals>

prover/drivers/kore-driver.md

@@ -58,19 +58,22 @@ Add various standard Kore declarations to the configuration directly:
 ```
 
 The `claim` Declaration creates a new `<goal>` cell.
-We create a subgoal, so that all the reasoning happens
-in the subgoal and the claim of the named goal remains intact.
 
 ```k
   rule <k> claim PATTERN strategy STRAT
-        => claim getFreshClaimName() : PATTERN strategy STRAT
+        => claim getFreshGlobalAxiomName() : PATTERN strategy STRAT
            ...
        </k>
   rule <k> claim NAME : PATTERN
            strategy STRAT
-        => subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT))
+        => subgoal(NAME, PATTERN, STRAT)
+        ~> axiom NAME : PATTERN
            ...
        </k>
+
+  // the rule above generates `success ~> axiom _ : _ ~> Declarations`
+  rule <k> (success => .K) ~> D:Declaration ... </k>
+  rule <k> (success => .K) ~> D:Declarations ... </k>
 ```
 
 ```k

prover/drivers/smt-driver.md

@@ -217,7 +217,7 @@ module DRIVER-SMT
        </k>
     requires notBool #matchesUnfoldMutRecs(STRAT)
 
-  rule <strategy> unfold-mut-recs => noop ... </strategy>
+  rule <k> unfold-mut-recs => noop ... </k>
 
   syntax Bool ::= #matchesUnfoldMutRecs(Strategy) [function]
   rule #matchesUnfoldMutRecs(unfold-mut-recs) => true
@@ -319,23 +319,20 @@ module DRIVER-SMT
   rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S)
 
   syntax KItem ::= "expect" TerminalStrategy
-  rule <strategy> S ~> expect S => .K ... </strategy>
+  rule <k> S ~> expect S => .K ... </k>
 
-  rule <goals>
-         <k> #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
+  rule <k> ( #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
           ~> (check-sat)
-          => #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
-             ...
-         </k>
-         <strategy> .K
-                 => subgoal(\implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps))))
-                           , STRAT
-                           )
-                 ~> expect EXPECTED
-         </strategy>
-         ...
-       </goals>
-   requires notBool PATTERN ==K  \exists { .Patterns } \and ( .Patterns )
+           )
+        => ( subgoal(\implies( \and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps))))
+                    , STRAT
+                    )
+        ~>   #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
+           )
+           ...
+       </k>
+    requires notBool PATTERN ==K  \exists { .Patterns } \and ( .Patterns )
+  rule <k> (success => .K) ~> #goal( goal: _, strategy: _, expected: _) ... </k>
 ```
 
 ```k

prover/drivers/unit-tests.md

@@ -27,7 +27,7 @@ module UNIT-TEST
 
   syntax Declaration ::= "suite" String
   rule <k> suite(SUITE) => next-test(SUITE, 1) ... </k>
-  
+
   syntax Declaration ::= "next-test" "(" String "," Int ")"
   rule <k> next-test(SUITE, N)
         => test(SUITE, N)

prover/lang/kore-lang.md

@@ -182,8 +182,6 @@ only in this scenario*.
   syntax SymbolDeclaration ::= "symbol" Symbol "(" Sorts ")" ":" Sort
   syntax SortDeclaration ::= "sort" Sort
   syntax AxiomName ::= LowerName | UpperName
-  syntax ClaimName ::= LowerName | UpperName
-  syntax AxiomOrClaimName ::= AxiomName | ClaimName
 
   syntax Declaration ::= "imports" String
                        | "axiom" Pattern
@@ -854,21 +852,15 @@ Simplifications
 
   rule freshAxiomName(I:Int) => StringToAxiomName("ax" +String Int2String(I))
 
-  syntax String ::= ClaimNameToString(ClaimName) [function, hook(STRING.token2string)]
-  syntax ClaimName ::= StringToClaimName(String) [function, functional, hook(STRING.string2token)]
-                     | freshClaimName(Int)       [freshGenerator, function, functional]
-
-  rule freshClaimName(I:Int) => StringToClaimName("cl" +String Int2String(I))
-
   syntax Set ::= collectClaimNames() [function]
                | #collectClaimNames(Set) [function]
 
   rule collectClaimNames() => #collectClaimNames(.Set)
 
   rule [[ #collectClaimNames(Ns)
-          => #collectClaimNames(Ns SetItem(ClaimNameToString(N))) ]]
-       <id> N:ClaimName </id>
-       requires notBool (ClaimNameToString(N) in Ns)
+          => #collectClaimNames(Ns SetItem(AxiomNameToString(N))) ]]
+       <id> N:AxiomName </id>
+       requires notBool (AxiomNameToString(N) in Ns)
 
   rule #collectClaimNames(Ns) => Ns [owise]
 
@@ -1012,10 +1004,6 @@ assume a pattern of the form:
   rule getFreshAxiomName(GId)
        => StringToAxiomName(getFreshName("ax", collectNamed(GId)))
 
-  syntax ClaimName ::= getFreshClaimName() [function]
-  rule getFreshClaimName()
-       => StringToClaimName(getFreshName("cl", collectGlobalNamed()))
-
   syntax Set ::= collectSymbolsS(GoalId) [function]
                | #collectSymbolsS(Declarations) [function]
 
@@ -1034,6 +1022,14 @@ assume a pattern of the form:
        => StringToSymbol(
             getFreshNameNonum(Base, collectSymbolsS(GId)))
 
+  syntax KItem ::= loadNamed(AxiomName)
+
+  rule <k> loadNamed(Name) => P ...</k>
+       <declaration> axiom Name : P </declaration>
+
+  rule <k> loadNamed(Name) => P ...</k>
+       <local-decl> axiom Name : P </local-decl>
+
 ```
 
 ```k

prover/lang/smt-lang.md

@@ -244,6 +244,7 @@ module SMTLIB2-HELPERS
   rule CheckSAT.parseResult(#systemResult(0, "sat\n", STDERR))     => sat
   rule CheckSAT.parseResult(#systemResult(0, "unsat\n", STDERR))   => unsat
   rule CheckSAT.parseResult(#systemResult(0, "unknown\n", STDERR)) => unknown
+  rule CheckSAT.parseResult(#systemResult(0, "timeout\n", STDERR)) => unknown
   rule CheckSAT.parseResult(#systemResult(I, STDOUT, STDERR))      => #error(#systemResult(I, STDOUT, STDERR))
     requires I =/=Int 0
 endmodule

prover/prover.md

@@ -21,7 +21,6 @@ requires "strategies/unfolding.k"
 requires "utils/error.k"
 requires "utils/instantiate-assumptions.k"
 requires "utils/heatcool.k"
-requires "utils/load-named.k"
 requires "utils/syntactic-match.k"
 requires "utils/visitor.k"
 ```
@@ -63,7 +62,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                     | "frame"
                     | "unfold-mut-recs"
                     | "apply-equation"
-                        RewriteDirection AxiomOrClaimName
+                        RewriteDirection AxiomName
                         "at" Int "by" "[" Strategies "]"
                     | "apply-equation"
                       "(" "eq:" Pattern
@@ -73,7 +72,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                       ")"
                     | "intros" AxiomName
                     | "replace-evar-with-func-constant" Variables
-                    | "duplicate" AxiomOrClaimName "as" AxiomName
+                    | "duplicate" AxiomName "as" AxiomName
                     | "instantiate-universals" "("
                         "in:" AxiomName ","
                         "vars:" VariableNames ","
@@ -82,7 +81,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                     // of the axiom or claim given as the first arg.
                     // Uses the strategy given in second argument
                     // to discharge the axiom's premises.
-                    | "apply" "(" AxiomOrClaimName
+                    | "apply" "(" AxiomName
                               "," Strategy ")"
                     | "inst-exists" "(" Variable "," Pattern
                                     "," Strategy ")"