Steps to Reproduce

1. Save the following in a file, say file.slk. Note that the three lemmas entail1, entail2, and entail3 correspond respectively to the entailments (1), (2), and (3).

   data ch_star{
       int val;
   }.
   
   pred arr_seg<n>     == self::ch_star<_> & n=1
                       or self::ch_star<_> * q::arr_seg<n-1> & q=self+1 & n>1
     inv n>=1.
   
   pred int_block<v>   == self::ch_star<a> * x::ch_star<b> * y::ch_star<c> * z::ch_star<d>
                        & x=self+1 & y=x+1 & z=y+1 & v=a+256*b+65536*c+16777216*d.
   
   pred int_arr_seg<n> == self::int_block<_> & n=1
                       or self::int_block<_> * q::int_arr_seg<n-1> & q=self+4 & n>1
     inv n>=1.
   
   /*
    * (1)
    */
   checkentail x::arr_seg<4> |- x::int_block<_>.
   print residue.
   expect Valid.
   lemma "entail1" self::arr_seg<4> -> self::int_block<_>.
   
   /*
    * (2)
    */
   checkentail x::int_block<_> |- x::int_arr_seg<1>.
   print residue.
   expect Valid.
   lemma "entail2" self::int_block<_> -> self::int_arr_seg<1>.
   
   /*
    * (3)
    */
   lemma "entail3" self::arr_seg<4> -> self::int_arr_seg<1>.
   checkentail x::arr_seg<4> |- x::int_arr_seg<1>.
   print residue.
   expect Valid.
   

2. Run sleek on file.slk.
3. Comment out lemma "entail3" self::arr_seg<4> -> self::int_arr_seg<1>., then run sleek on file.slk again.

Expected Behavior

As expected, on the first run, lemma "entail3" self::arr_seg<4> -> self::int_arr_seg<1>. makes entailment (3) valid.
On the second run, entailment (3) should also be valid.

Actual Behavior

On the second run, although the two lemmas lemma "entail1" self::arr_seg<4> -> self::int_block<_>. and lemma "entail2" self::int_block<_> -> self::int_arr_seg<1>. are present, and the consequent of entail1 is the same as the antecedent of entail2 (i.e. self::int_block<_>), making their transitive combination equivalent to entail3.

Despite all this, on the second run, due to the lack of explicit declaration of lemma "entail3" self::arr_seg<4> -> self::int_arr_seg<1>., entailment (3) is not valid.

Allow for reasoning of constant strings and character literals.

Import the support for type polymorphism from the session work.

Steps to Reproduce

Travis job log:

1. First, all dependencies are installed, and make is invoked:

   make
   

   which by default, processes the first rule, in this case, all.
2. Then, make traverses through the rules, and the xml rule is processed fine.

   cd /home/travis/build/zhengqunkoo/hipsleek/xml; make all; make opt; cd ..
   ocamlopt -o xml-light.cmxa -a  xml_parser.cmx xml_lexer.cmx dtd.cmx xmlParser.cmx xml.cmx
   ocamlopt xml-light.cmxa test.ml -o test_opt.exe
   make[1]: Leaving directory `/home/travis/build/zhengqunkoo/hipsleek/xml'
   make[1]: Entering directory `/home/travis/build/zhengqunkoo/hipsleek/xml'
   make[1]: Nothing to be done for `opt'.
   make[1]: Leaving directory `/home/travis/build/zhengqunkoo/hipsleek/xml'
   

3. So, the sleek.byte rule is processed. But ocamlbuild fails:

   IMPORTANT: I cannot work with leftover compiled files.
   

   also known as files with suffix .so, .a, and .o.

Expected Behavior

Build does not fail.

Actual Behavior

ocamlbuild fails purely due to all leftover compiled files from hipsleek/dependencies.

• Clear the warnings (specially for @deprecated stuff)
• add a make fail option when warnings are raised

Steps to Reproduce

1. Visit http://loris-5.d2.comp.nus.edu.sg/TeachHIP/infer.html?ex=ex1&type=slk&options=oc
2. Click Verify, Verification Details
3. Observe that result of Entail 2 is: ❌
4. Observe details:

   Entail 2: Fail.(must) cause: true |-  false. LOCS:[0] (RHS: contradiction)
   
   Validate 2: Expecting(3)Valid BUT got : Fail_Must
   

5. Change expect Valid. on line 15 to expect Fail.
6. Click Verify, Verification Details
7. Observe that result of Entail 2 is: ❌
8. Observe details:

   Entail 2: Fail.(must) cause: true |-  false. LOCS:[0] (RHS: contradiction)
   
   Validate 2: OK
   

Expected Behavior

Should indicate that the ❌ and ✓ in the Results list on TeachHIP indicate resp. Entail 2: Valid. and Entail 2: Fail.. I.e., ❌ and ✓ do not indicate resp. Validate 2: OK and Validate 2: Expecting(3)Valid BUT got : Fail_Must.

Actual Behavior

No indication that the ❌ and ✓ in the Results list on TeachHIP indicate resp. Entail 2: Valid and Entail 2: Fail.

We should make HIP/SLEEK work with the latest mona, making mona run interactively.

Travis CI announced in an email https://mailchi.mp/3d439eeb1098/travis-ciorg-is-moving-to-travis-cicom that CI management will be under travis-ci.com by the end of this year.

We could still stick with Travis CI, but rOpenSci advocates migrating from Travis CI altogether https://ropensci.org/technotes/2020/11/19/moving-away-travis/. GitHub Actions looks promising.

• 1. Some aliases do not become trivial.
  [f| emp & flted_175_250=1+(4*n) & y=2+x |- q_284::arr_seg<b_282>@M & flted_176_269=b_282+flted_175_250 & flted_175_250+x=q_284 |f] is translated by the class VarReplacer by traversing the string from left to right, and for each variable, if the variable is known to be aliased (as given by AliasCollector), replacing the variable with the aliased value, until a fixpoint. Here is one step of the fixpoint computation:

  emp & flted_175_250=1+(4*n) & y=2+x |- q_284::arr_seg<b_282>@M & flted_176_269=b_282+flted_175_250 & flted_175_250+x=q_284
  emp & 1+(4*n)=1+(4*n) & y=2+x |- q_284::arr_seg<b_282>@M & flted_176_269=b_282+flted_175_250 & flted_175_250+x=q_284
  emp & 1+(4*n)=1+(4*n) & 2+x=2+x |- q_284::arr_seg<b_282>@M & flted_176_269=b_282+flted_175_250 & flted_175_250+x=q_284
  emp & 1+(4*n)=1+(4*n) & 2+x=2+x |- q_284::arr_seg<b_282>@M & b_282+flted_175_250=b_282+flted_175_250 & flted_175_250+x=q_284
  emp & 1+(4*n)=1+(4*n) & 2+x=2+x |- q_284::arr_seg<b_282>@M & b_282+flted_175_250=b_282+1+(4*n) & flted_175_250+x=q_284
  emp & 1+(4*n)=1+(4*n) & 2+x=2+x |- q_284::arr_seg<b_282>@M & b_282+flted_175_250=b_282+1+(4*n) & 1+(4*n)+x=q_284
  

  and then the class AliasRemover gives the result: emp |- q_284::arr_seg<b_282>@M & b_282+flted_175_250=b_282+1+(4*n) & 1+(4*n)+x=q_284. However, it should be translated into emp |- q_284::arr_seg<b_282>@M & 1+(4*n)+x=q_284.

  flted_175_250 in b_282+flted_175_250 is not replaced, since the NodeVisitor class does not modify parse trees in-place. So the aforementioned flted_175_250 does not exist at that location in the parse tree. However, on the next step of the fixpoint computation, the aforementioned flted_175_250 will exist there.

  An initial solution is to not just replace variables in the parse tree, but also replace variables in the collected aliases.
  After more analysis, the root cause is that the list of aliased variables (as given by AliasCollector) is emptied on every step of the fixpoint computation.
  The solution is to collect aliases given by every step of the fixpoint computation, and to not empty the list of aliased variables. Note that this solution is sound, since for any variable n that appears multiple times in the list of aliased variables, n must be aliased to the same value. Otherwise, the formula contains aliases of the same variable n to multiple different values, and this is already a contradiction, therefore the solution is trivially sound.

• 2. With the current implementation of AliasRemover (with the two existing functions visit_head and visit_restHead), trivial aliases that occur in boolExps cannot be removed, as mentioned in 54a1a98, since the boolExp may contain subformulas other than trivial aliases, and so removing the entire boolExp is wrong. However, trivial aliases that occur in boolExps may be removed if:

  1. The boolExp rule is broken into boolExpHead and boolExpRestHead, similarly to the existing rules head and restHead, and with similar justification. The justification for this is, a trivial alias in head (e.g. n=n in n=n & ..., or e.g. n=n in n=n | ...) should be removed, and both the operator and the trivial alias in restHead (e.g. & n=n in ... & n=n & ...) should be removed. Note that removing a trivial alias in head is not entirely correct, as the operator following the trivial alias should also be removed (e.g. & in n=n & ..., or e.g. | in n=n | ... should be removed), and
  2. AliasRemover implements the visit_boolExpHead and visit_boolExpRestHead functions in a similar way to visit_head and visit_restHead. However, these functions need to account for boolExp's arbitrary nestedness, and also account for possible parentheses around a boolExp.

  With this, the semantic distinguishment of alias syntaxes in 54a1a98 is no longer needed.

• 3. As mentioned above, removing a trivial alias in head is not entirely correct, as the operator following the trivial alias should also be removed (e.g. & in n=n & ..., or e.g. | in n=n | ... should be removed). As the grammar is left-recursive, this should be solved by setting some boolean state in the AliasRemover class on visiting a trivial alias in visit_head, and then whenever this boolean state is true in visit_headRest, the operator should be removed.

To normalize the textual representation of the code (e.g. remove trailing whitespaces). This allows faster developer workflow when running git add -p. I suggest an opinionated linter like OCamlFormat.

Steps to Reproduce

1. Save the following in a file, say file.slk. Note: ch_star and arr_seg are "established definitions", and are defined as in testcases/ex5/ex5a.slk.

   data ch_star{
       int val;
   }.
   
   pred arr_seg<n>     == self::ch_star<_> & n=1
                         or (exists q: self::ch_star<_> * q::arr_seg<n-1> & q = self + 1 & n > 1)
     inv n>=1.
   
   /*
    * SECTION 1.
    * `BaseCaseUnfold` of `arr_seg` sometimes fails, entailments (3),(4),(5),(6) in this section fail.
    * Introducing the following lemma makes all entailments in this section valid.
    * This section shows that `ch_star` and `arr_seg` have the expected behaviors.
    */
   lemma self::arr_seg<a+b> & self+a=q <-> self::arr_seg<a> * q::arr_seg<b>.
   
   // (1)
   checkentail x::ch_star<_> * y::ch_star<_> & y=x+1 |- x::arr_seg<2>.
   print residue.
   expect Valid.
   
   // (2)
   checkentail x::ch_star<_> * y::arr_seg<1> & y=x+1 |- x::arr_seg<2>.
   print residue.
   expect Valid.
   
   // (3)
   checkentail x::arr_seg<1> * y::ch_star<_> & y=x+1 |- x::arr_seg<2>.
   print residue.
   expect Valid.
   
   // (4)
   checkentail x::arr_seg<1> * y::arr_seg<1> & y=x+1 |- x::arr_seg<2>.
   print residue.
   expect Valid.
   
   // (5)
   checkentail x::arr_seg<2> & y=x+1 |- x::arr_seg<1> * y::arr_seg<1>.
   print residue.
   expect Valid.
   
   // (6)
   checkentail x::arr_seg<1> * y::arr_seg<1> & y=x+1 |- x::arr_seg<2>.
   print residue.
   expect Valid.
   
   /*
    * SECTION 2.
    * But even with the lemma, there are still entailments that fail.
    */
   
   // (7)
   checkentail x::arr_seg<3> & y=x+1 |- x::arr_seg<1> * y::arr_seg<2>.
   print residue.
   expect Valid.
   
   // (8)
   checkentail x::arr_seg<3> & y=x+2 |- x::arr_seg<2> * y::arr_seg<1>.
   print residue.
   expect Valid.
   
   // (9)
   checkentail x::arr_seg<4> & y=x+1 |- x::arr_seg<1> * y::arr_seg<3>.
   print residue.
   expect Valid.
   
   // (a)
   checkentail x::arr_seg<4> & y=x+2 |- x::arr_seg<2> * y::arr_seg<2>.
   print residue.
   expect Valid.
   
   // (b)
   checkentail x::arr_seg<4> & y=x+3 |- x::arr_seg<3> * y::arr_seg<1>.
   print residue.
   expect Valid.
   

2. Run sleek on file.slk.

Expected Behavior

Changing the order of entailments does not change the unexpected entailments.

Actual Behavior

Changing the order of entailments changes the unexpected entailments.

Let's say the above file has entailment order "123456789ab", where "a" and "b" represent the tenth and eleventh entailments.

Shifting entailment (1) down the list of entailments results in this table, where in the i^th row, entailment (1) is in the i^th position:

Shifting entailments (2),(3),(4),(6) down the list of entailments results in analogous tables: the "Actual Unexpected Entailments" column is the same. That is, entailment (7) always fails, and if the shifted entailment appears after entailment (7), then the entailment after the shifted entailment fails.

Shifting entailment (5) down the list of entailments results in this table, where entailment (7) always fails, and all other entailments are always valid:

Shifting entailment (7) down the list of entailments results in this table, where entailment (8) always fails, except when the shifted entailment appears immediately before entailment (8). Also, entailment (7) fails only when entailment (7) is before entailment (8):

Shifting entailment (8) down the list of entailments results in this table:

Shifting entailments (9),(a),(b) down the list of entailments results in analogous tables: the "Unexpected List" column is the same. That is, entailment (7) always fails, except when the shifted entailment appears immediately before entailment (7). Also, the shifted entailment fails only when the shifted entailment is before entailment (7).

smtsolver.ml contains hardcoded references to z3 versions.

Note: z3.ml is not actually run by sleek. On the other hand smtsolver.ml is actually run by sleek.

Steps to Reproduce

0. Clone this repository.
1. Compile oc from the omega_modified directory, add that directory to the PATH environment variable.
2. Run hip or sleek.

Expected Behavior

hip or sleek runs.

Actual Behavior

hip or sleek does not run, because oc (and fixcalc) is not found.

oc (and fixcalc) is only searched for in the current directory and /usr/local/bin. Indeed, strace shows that only these two locations are checked (a similar trace is shown for fixcalc):

stat("./oc", 0x7ffd0eca7e00)            = -1 ENOENT (No such file or directory)
stat("/usr/local/bin/oc", {st_mode=S_IFREG|0755, st_size=3552638, ...}) = 0

Hi,

I am trying to verify a program that needs the support of set/bag theory. In HIP/SLEEK, I understand that it uses the Isabelle prover for solving set/bag constraints (e.g., union). However, HIP requires the Isabelle image which I'm unable to find in Isabelle document. I suspect that HIP supports the older version of Isabelle but I'm unable to resolve it myself.

Specifically, I want to run this file: https://github.com/hipsleek/hipsleek/blob/master/examples/bag_examples/qsort.ss

The installed ocamlformat is version 0.14.3, but the version specified at https://github.com/hipsleek/hipsleek/blob/master/.ocamlformat is 0.14.2.

CI continues to succeed at this repository, but fails at https://github.com/zhengqunkoo/hipsleek. This could be due to installing from the CI cache instead of from rake dependencies:install.

The solution is likely to bump the version number, and stop installing from CI cache. This should not be too harmful, as CI cache does not seem to provide much speedup.

Steps to Reproduce

1. Run sleek on:

   checkentail x>0 |- false.
   expect Fail.
   
   checkentail x>0 |- x=1.
   expect Fail.
   

2. Observe output:

   Entail 1: Fail.(must) cause: true |-  false. LOCS:[0] (RHS: contradiction)
   
   Validate 1: OK
   
   
   Entail 2: Fail.(may) cause: 0<x |-  x=1. LOCS:[4] (may-bug)
   
   Validate 2: OK
   

Expected Behavior

expect expressions are as detailed as the entailment failure cause. expect Fail_Must. and expect Fail_May. are allowable expressions.

Actual Behavior

It's good that expect Fail. covers both entailment failure causes (witnessed by Validate n: OK in the output above), but allowable expect expressions (Valid, Fail) are less detailed than the entailment failure cause (Fail.(must) cause, Fail.(may) cause). expect Fail_Must. and expect Fail_May. are not allowable expressions.

One candidate: TravisCI

• adapt hip/sleek's interface with cvc3 to cvc4
• remove references to cvcl and cvc3.
• explore what capabilities cvc4 has that we could perhaps leverage on.

Steps to Reproduce

1. Save the following in a file, say file.slk.

   data ch_star { int val; }.
   checkentail x::ch_star<_> |- x::ch_star<_>.
   print residue.
   

2. Run sleek -dre=compute_actions file.slk.
3. Run sleek --pprint -dre=compute_actions file.slk.
4. Run sleek -dre=compute_actions --trace-log-num 1 file.slk.
5. Run sleek --pprint -dre=compute_actions --trace-log-num 1 file.slk.

Expected Behavior

sleek -dre=compute_actions file.slk has the same output as sleek --pprint -dre=compute_actions file.slk, but with some formulas pretty-printed.
sleek -dre=compute_actions --trace-log-num 1 file.slk has the same output as sleek --pprint -dre=compute_actions --trace-log-num 1 file.slk, but with some formulas pretty-printed.

Actual Behavior

sleek -dre=compute_actions file.slk has a drastically different output than sleek --pprint -dre=compute_actions file.slk.
sleek -dre=compute_actions --trace-log-num 1 file.slk has a drastically different output than sleek --pprint -dre=compute_actions --trace-log-num 1 file.slk.

In #37, pretty printing was extended to formulas that appear in places other than invocations of sleek -dre=compute_pretty_actions. With #37, the script argument --pprint introduced in #36 is no longer just a flag that enables invocations of sleek -dre=compute_pretty_actions to output calls to compute_pretty_actions. With #37, the script argument --pprint becomes a toggle for turning on and off pretty printing: compare the output of sleek file.slk with sleek --pprint file.slk.

So, from a user experience point of view, there is an expectation that --pprint toggles pretty printing. However, the user expectation is not fulfilled in two ways:

• 1. sleek -dre=compute_actions file.slk outputs calls to compute_actions, but sleek --pprint -dre=compute_actions file.slk does not output calls to compute_actions. Instead, sleek --pprint -dre=compute_pretty_actions file.slk is needed to output calls to compute_pretty_actions (which is the pretty analogue of compute_actions). But the user should not need to change any other script arguments whenever --pprint is added.
  The addition/removal of the script argument --pprint results in a behavior (needing to change script arguments) that is beyond the behavior that a user expects out of --pprint (toggling of pretty printing for formulas only).

• 2. At first, the behavior in item 1 might seem to be not a big deal, because one might think that outputting or printing should not affect anything else. One might think "the user just has to change the -dre script argument, which is a little inconvenient, but the output is still as expected by the user". However, this is not the case. There is one script argument, --trace-log-num, that prints to output only when the corresponding call is output, and so is dependent on which calls are output. Concretely, sleek -dre=compute_actions --trace-log-num 1 file.slk outputs the trace log, but sleek --pprint -dre=compute_actions --trace-log-num 1 file.slk does not.
  The addition/removal of the script argument --pprint results in a behavior (toggling of --trace-log-num) that is beyond the behavior that a user expects out of --pprint (toggling of pretty printing for formulas only).

Steps to Reproduce

1. Save the following in a file, say file.slk.

   data ch_star { int val; }.
   checkentail x::ch_star<_> |- x::ch_star<_>.
   print residue.
   

2. Run sleek --pprint -dre=compute_pretty_actions --trace-log-num 1 file.slk.

Expected Behavior

The trace log is output.

Actual Behavior

The trace log is not output.

This means the chain of function calls with the string "pretty" in the function names, starting from the function that defines the printers for debugging, and ending at the function that calls ho_aux at https://github.com/hipsleek/hipsleek/pull/33/files#diff-1e5e2b2e2c21c746e3a0ec298c86b670R4088-R4171, is not a faithful copy of the original chain of function calls triggered by compute_actions.

Move all the files that are related to the off-the-shelf provers into a separate folder. That includes the interface files, procutils, and the provers source files.