hoice
hoice copied to clipboard
hopv
An ICE-based predicate synthesizer for Horn clauses.
I modified the parser so that it can handle `!`. ## Detail In order to handle smt2 files preprocessed by `z3`, we have to handle annotations specified by `!`. Annotations...
hoice crushes for the benchmark: https://github.com/chc-comp/rust-horn/blob/master/trees-1-append-safe.smt2 when run with "-v -v -v". ``` $ hoice -v -v -v trees-1-append-safe.smt2 ; Running top pre-processing ; running simplify ... ; looking for...
# Input ``` (set-logic HORN) (declare-fun main@_6 ( Int Int Int ) Bool ) (declare-fun [email protected] ( Int Int Int Int ) Bool ) (declare-fun [email protected] ( Int Int )...
The following SMT2 code is not accepted by HoIce, probably by a bug. I tried the following code on HoIce. (Sorry for this noisy and messy bug report!) ``` (set-logic...
Hoice's error-handling is based on [`error-chain`](https://crates.io/crates/error-chain) and has several issues as far as Hoice is concerned. The main problem is that `error-chain` erases errors, *i.e.* [`rsmt2`](https://crates.io/crates/rsmt2)'s errors become `dyn std::error::Error`...
## Input: smt2 file ``` (set-logic HORN) (set-option :produce-proofs true) (declare-fun X0 (Int) Bool) (declare-fun X1 (Int) Bool) (declare-fun X2 (Int) Bool) (declare-fun X3 (Int) Bool) (declare-fun X4 (Int) Bool)...
I am confused with the way HoIce parses "or". For the following input, HoIce seems to reject the 2nd and 5th clauses but accepts the other. (The comments indicates error...
## Changes Made I changed `tag_opt` to `word_opt` to handle identifiers correctly. ## Bugs Fixed Previously, there was a bug that produced an error like the following: ``` (declare-fun andx...
The following input causes Hoice to error with "invalid datatype declaration, unknown sort 'D1'". I expect Hoice to return `sat` without raising an error for this input. ``` (set-logic HORN)...
