liquid-fixpoint 0.5.0.1 → 0.6.0.1

raw patch · 139 files changed

+17879/−3386 lines, 139 filesdep +timedep ~basenew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: time

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• .ghci +1/−0
• .git +1/−0
• .gitignore +30/−0
• .travis.yml +51/−0
• CHANGES.md +29/−0
• Makefile +59/−0
• README.md +303/−0
• TODO.md +37/−0
• default.nix +32/−0
• liquid-fixpoint.cabal +79/−9
• scripts/travis +137/−0
• shell.nix +17/−0
• src/Language/Fixpoint/Defunctionalize.hs +368/−0
• src/Language/Fixpoint/Graph.hs +10/−0
• src/Language/Fixpoint/Graph/Deps.hs +549/−0
• src/Language/Fixpoint/Graph/Indexed.hs +100/−0
• src/Language/Fixpoint/Graph/Partition.hs +213/−0
• src/Language/Fixpoint/Graph/Reducible.hs +62/−0
• src/Language/Fixpoint/Graph/Types.hs +184/−0
• src/Language/Fixpoint/Minimize.hs +107/−49
• src/Language/Fixpoint/Misc.hs +123/−24
• src/Language/Fixpoint/Parse.hs +372/−174
• src/Language/Fixpoint/Partition.hs +0/−463
• src/Language/Fixpoint/Smt/Bitvector.hs +1/−1
• src/Language/Fixpoint/Smt/Interface.hs +162/−105
• src/Language/Fixpoint/Smt/Serialize.hs +89/−388
• src/Language/Fixpoint/Smt/Theories.hs +259/−95
• src/Language/Fixpoint/Smt/Types.hs +61/−64
• src/Language/Fixpoint/Solver.hs +104/−119
• src/Language/Fixpoint/Solver/Eliminate.hs +50/−85
• src/Language/Fixpoint/Solver/GradualSolution.hs +420/−0
• src/Language/Fixpoint/Solver/GradualSolve.hs +319/−0
• src/Language/Fixpoint/Solver/Graph.hs +0/−162
• src/Language/Fixpoint/Solver/Instantiate.hs +533/−0
• src/Language/Fixpoint/Solver/Monad.hs +167/−74
• src/Language/Fixpoint/Solver/Sanitize.hs +425/−0
• src/Language/Fixpoint/Solver/Solution.hs +234/−152
• src/Language/Fixpoint/Solver/Solve.hs +118/−113
• src/Language/Fixpoint/Solver/TrivialSort.hs +7/−7
• src/Language/Fixpoint/Solver/Types.hs +0/−39
• src/Language/Fixpoint/Solver/UniqifyBinds.hs +63/−40
• src/Language/Fixpoint/Solver/UniqifyKVars.hs +46/−34
• src/Language/Fixpoint/Solver/Validate.hs +0/−276
• src/Language/Fixpoint/Solver/Worklist.hs +24/−82
• src/Language/Fixpoint/SortCheck.hs +485/−220
• src/Language/Fixpoint/Types.hs +12/−24
• src/Language/Fixpoint/Types/Config.hs +116/−110
• src/Language/Fixpoint/Types/Constraints.hs +291/−153
• src/Language/Fixpoint/Types/Environments.hs +139/−17
• src/Language/Fixpoint/Types/Errors.hs +27/−3
• src/Language/Fixpoint/Types/Graphs.hs +0/−70
• src/Language/Fixpoint/Types/Names.hs +44/−19
• src/Language/Fixpoint/Types/PrettyPrint.hs +21/−23
• src/Language/Fixpoint/Types/Refinements.hs +134/−36
• src/Language/Fixpoint/Types/Solutions.hs +387/−0
• src/Language/Fixpoint/Types/Sorts.hs +118/−39
• src/Language/Fixpoint/Types/Spans.hs +7/−3
• src/Language/Fixpoint/Types/Substitutions.hs +25/−5
• src/Language/Fixpoint/Types/Triggers.hs +64/−0
• src/Language/Fixpoint/Types/Utils.hs +22/−11
• src/Language/Fixpoint/Types/Visitor.hs +113/−46
• src/Language/Fixpoint/Utils/Files.hs +12/−1
• src/Language/Fixpoint/Utils/Statistics.hs +6/−6
• stack.yaml +12/−0
• tests/crash/num00.fq +29/−0
• tests/crash/sort00.fq +12/−0
• tests/crash/sort01.fq +13/−0
• tests/cut/test00-tx.fq +12/−0
• tests/cut/test00.fq +28/−0
• tests/cut/test00a-tx.fq +43/−0
• tests/cut/test00a.fq +29/−0
• tests/cut/test1-tx.fq +43/−0
• tests/cut/test1.fq +29/−0
• tests/cut/test2-tx.fq +112/−0
• tests/cut/test2.fq +51/−0
• tests/elim/div00.fq +23/−0
• tests/elim/elim00.fq +1494/−0
• tests/elim/kvparam00.fq +20/−0
• tests/elim/len00.fq +23/−0
• tests/elim/test00-tx.fq +12/−0
• tests/elim/test00.fq +26/−0
• tests/elim/test00a.fq +28/−0
• tests/elim/test1.fq +29/−0
• tests/elim/test2.fq +53/−0
• tests/elim/tuple00.fq +114/−0
• tests/elim/tuple01.fq +137/−0
• tests/minimize/two-cores.fq +30/−0
• tests/neg/NonLinear.fq +28/−0
• tests/neg/NonLinear.hs.fq +91/−0
• tests/neg/elim-dep-00.fq +43/−0
• tests/neg/num00.fq +0/−28
• tests/neg/pack00.fq +37/−0
• tests/neg/pack01.fq +45/−0
• tests/neg/poly0.fq +1/−0
• tests/neg/poly1.fq +1/−0
• tests/neg/poly2.fq +1/−0
• tests/neg/test00.hs.fq +286/−0
• tests/pos/LogicCurry1.hs.fq +245/−0
• tests/pos/NonLinear-pack.fq +40/−0
• tests/pos/bad-subst01.fq +3/−0
• tests/pos/bad-subst02.fq +22/−0
• tests/pos/bool00.fq +28/−0
• tests/pos/bool03.fq +28/−0
• tests/pos/bool04.fq +20/−0
• tests/pos/elim00.fq +2/−0
• tests/pos/hex.ts.fq +342/−0
• tests/pos/ho00.fq +21/−0
• tests/pos/kvar-param-poly-00.fq +26/−0
• tests/pos/len00.fq +2/−2
• tests/pos/listqual.hs.fq +577/−0
• tests/pos/literals.fq +3/−0
• tests/pos/literals01.fq +9/−0
• tests/pos/literals02.fq +28/−0
• tests/pos/literals03.fq +16/−0
• tests/pos/literals04.fq +16/−0
• tests/pos/literals05.fq +14/−0
• tests/pos/meas00.fq +21/−0
• tests/pos/meas02.fq +25/−0
• tests/pos/min00.fq +22/−0
• tests/pos/multi-sorts.fq +10/−0
• tests/pos/multiple-func-sorts.fq +1/−2
• tests/pos/numoverload00.fq +23/−0
• tests/pos/poly0.fq +1/−0
• tests/pos/poly1.fq +1/−0
• tests/pos/poly2.fq +1/−0
• tests/pos/qualif-inst.fq +1/−1
• tests/pos/test00.fq +4/−2
• tests/pos/test00.hs.fq +1021/−0
• tests/pos/test000.hs.fq +489/−0
• tests/pos/unused.fq +11/−0
• tests/pos/wl02.fq +242/−0
• tests/smt2/Smt.hs +28/−0
• tests/test.hs +11/−6
• tests/testParser.hs +308/−0
• tests/todo/MergeSort.fq +3234/−0
• tests/todo/baz.fq +22/−0
• tests/todo/poly.fq +14/−0
• tests/todo/wl01.fq +39/−0
• unix/Language/Fixpoint/Utils/Progress.hs +4/−4

@@ -0,0 +1,1 @@+:set -isrc

@@ -0,0 +1,1 @@+gitdir: ../.git/modules/liquid-fixpoint

@@ -0,0 +1,30 @@+.depend+*.cmi+*.cmo+*.cmx+*.o+/dist*+.liquid+/.vagrant/+/.stack-work/+/build.sh+/external/fixpoint/config.make+/external/fixpoint/fixpoint.native+/external/fixpoint/misc+/external/fixpoint/smtZ3.ml+/external/ocamlgraph/META+/external/ocamlgraph/Makefile+/external/ocamlgraph/config.status+/external/ocamlgraph/graph.a+/external/ocamlgraph/graph.cma+/external/ocamlgraph/graph.cmxa+/external/ocamlgraph/src/dot_lexer.ml+/external/ocamlgraph/src/dot_parser.ml+/external/ocamlgraph/src/dot_parser.mli+/external/ocamlgraph/src/dot_parser.output+/external/ocamlgraph/src/gml.ml+/external/ocamlgraph/src/version.ml+/tests/neg/.liquid/+/tests/pos/.liquid/+/external/ocamlgraph/config.log+/TAGS

@@ -0,0 +1,51 @@+language: c+sudo: false++# Only build master, develop, and PRs+branches:+  only:+  - master+  - develop+  - parser-az++matrix:+  include:+    - env: SMT="z3" CABAL=1.22 GHC=7.10.3+      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3,],sources: [hvr-ghc]}}+    - env: SMT="z3" CABAL=1.24 GHC=8.0.1+      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,],sources: [hvr-ghc]}}+    - env: SMT="z3" CABAL=1.24 GHC=8.0.2+      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.2,],sources: [hvr-ghc]}}+    - env: CABALVER=head GHCVER=head+      addons: {apt: {packages: [cabal-install-head,ghc-head],  sources: [hvr-ghc]}}++  allow_failures:+   - env: CABALVER=head GHCVER=head++cache:+  directories:+  - $HOME/.cabal+  - $HOME/.ghc++before_install:+ - export PATH="$HOME/.cabal/bin:/opt/ghc/$GHC/bin:/opt/cabal/$CABAL/bin:$PATH"+ - scripts/travis clean_cache "$SMT"++install:+ - scripts/travis install_cabal_deps+ - scripts/travis install_smt "$SMT"++script:+ - scripts/travis do_build && scripts/travis do_test "$SMT"+ - scripts/travis clean_cache "$SMT"++after_failure:+ - scripts/travis dump_fail_logs++notifications:+  slack:+    rooms:+      secure: VT1SqW+4WQKb2PXgObQ/rNdQN8pFK5LaFacxB0fEvRZ2FSbM3qp1NGgii7WHlQdr598+L5qYhkpy1B8ssgNeR7iMmYP4GV/fhCoMd8nTQHLSrTMH8iQgT0D7SnuKdk5FQq1IXWtHjUzXtTIhnkfwOJF/xYf6BMMrO0sCta5JZgg=+    on_success: change+    on_failure: always+    on_start: never

@@ -0,0 +1,29 @@+# CHANGES++## NEXT++## 0.3.0.0++- Make interpreted mul and div the default, when `solver = z3`+- Use `higherorder` flag to allow higher order binders into the environment ++## 0.2.2.0++- Added support for theory of Arrays `Map_t`, `Map_select`, `Map_store`++- Added support for theory of Bitvectors -- see `Language.Fixpoint.Smt.Bitvector`++- Added support for string literals++## 0.2.1.0++- Pre-compiled binaries of the underlying ocaml solver are now+  provided for Linux, Mac OSX, and Windows.++  No more need to install Ocaml!++## 0.2.0.0++- Parsing has been improved to require *much* fewer parentheses.++- Experimental support for Z3's theory of real numbers with the `--real` flag.

@@ -0,0 +1,59 @@++OPTS="-W -O2 -XStandaloneDeriving"+PROFOPTS="-O2 -rtsopts -prof -auto-all -caf-all -XStandaloneDeriving -XDeriveDataTypeable"++CABAL=cabal+CABALI=$(CABAL) install --ghc-options=$(OPTS)+CABALP=$(CABAL) install --ghc-options=$(OPTS) -p++DEPS=unix-compat transformers mtl filemanip text parsec ghc-paths deepseq comonad contravariant semigroupoids semigroups bifunctors hscolour ansi-terminal hashable unordered-containers++TASTY=./dist/build/test/test++all:+	$(CABAL) install --ghc-options=$(OPTS)++force:+	$(CABAL) install --force-reinstalls --ghc-options=$(OPTS)++rebuild: ocaml+	make++igoto:+	$(CABAL) configure --ghc-options=$(OPTS)++goto:+	$(CABAL) build --ghc-options=$(OPTS)+	cp dist/build/liquid/liquid ~/.cabal/bin/++prof:+	$(CABAL) install --enable-executable-profiling --enable-library-profiling --ghc-options=$(PROFOPTS)++clean:+	cabal clean++docs:+	$(CABAL) haddock --executables --internal --hoogle --hyperlink-source #--html-location=http://goto.ucsd.edu/~rjhala/llvm-haskell/+++deps:+	$(CABALI) $(DEPS)++pdeps:+	$(CABALP) $(DEPS)++lint:+	hlint --colour --report .++tags:+	hasktags -c src/+	hasktags -e src/+	hasktags -x -c src/++test:+	cabal configure -fdevel --enable-tests --disable-library-profiling -O2+	cabal build+	cabal exec $(TASTY)++test710:+	$(TASTY)

@@ -0,0 +1,303 @@+Liquid Fixpoint [![Hackage](https://img.shields.io/hackage/v/liquid-fixpoint.svg)](https://hackage.haskell.org/package/liquid-fixpoint) [![Hackage-Deps](https://img.shields.io/hackage-deps/v/liquid-fixpoint.svg)](http://packdeps.haskellers.com/feed?needle=liquid-fixpoint) [![Build Status](https://img.shields.io/travis/ucsd-progsys/liquid-fixpoint/master.svg)](https://travis-ci.org/ucsd-progsys/liquid-fixpoint)+===============+++This package implements a Horn-Clause/Logical Implication constraint solver used+for various Liquid Types. The solver uses SMTLIB2 to implement an algorithm similar to:+++ [Houdini](https://users.soe.ucsc.edu/~cormac/papers/fme01.pdf)++ [cartesian predicate abstraction](http://swt.informatik.uni-freiburg.de/berit/papers/boolean-and-cartesian-....pdf)+++Requirements+------------++In addition to the .cabal dependencies you require an SMTLIB2 compatible solver binary:++- [Z3](http://z3.codeplex.com)+- [CVC4](http://cvc4.cs.nyu.edu)+- [MathSat](http://mathsat.fbk.eu/download.html)++If on Windows, please make sure to place the binary and any associated DLLs somewhere+in your path.++How To Build and Install+------------------------++Simply do:++    git clone https://github.com/ucsd-progsys/liquid-fixpoint.git+    cd liquid-fixpoint+    stack install++or (`cabal` instead of `stack` if you prefer.)+++Using SMTLIB-based SMT Solvers+------------------------------++You can use one of several SMTLIB2 compliant solvers, by:++    fixpoint --smtsolver=z3 path/to/file.hs++Currently, we support++    * Z3+    * CVC4+    * MathSat++++Configuration Management+------------------------++It is very important that the version of Liquid Fixpoint be maintained properly.++Suppose that the current version of Liquid Haskell is `A.B.C.D`:+++ After a release to hackage is made, if any of the components `B`, `C`, or `D` are missing, they shall be added and set to `0`. Then the `D` component of Liquid Fixpoint shall be incremented by `1`. The version of Liquid Fixpoint is now `A.B.C.(D + 1)`+++ The first time a new function or type is exported from Liquid Fixpoint, if any of the components `B`, or `C` are missing, they shall be added and set to `0`. Then the `C` component shall be incremented by `1`, and the `D` component shall stripped. The version of Liquid Fixpoint is now `A.B.(C + 1)`+++ The first time the signature of an exported function or type is changed, or an exported function or type is removed (this includes functions or types that Liquid Fixpoint re-exports from its own dependencies), if the `B` component is missing, it shall be added and set to `0`. Then the `B` component shall be incremented by `1`, and the `C` and `D` components shall be stripped. The version of Liquid Fixpoint is now `A.(B + 1)`+++ The `A` component shall be updated at the sole discretion of the project owners.++It is recommended to use the [Bumper](https://hackage.haskell.org/package/bumper) utility to manage the versioning of Liquid Fixpoint. Bumper will automatically do the correct update to the cabal file. Additionally, it will update any packages that you have the source for that depend on Liquid Fixpoint.++To update Liquid Fixpoint and Liquid Haskell, first clone Liquid Haskell and Liquid Fixpoint to a common location:++```+git clone https://github.com/ucsd-progsys/liquidhaskell.git+git clone https://github.com/ucsd-progsys/liquid-fixpoint.git+```++To increment the `D` component of Liquid Fixpoint:++```+./path/to/bumper -3 liquid-fixpoint+```++This will update the `D` component of Liquid Fixpoint. If necessary, this will update the `Build-Depends` of Liquid Haskell. If the `Build-Depends` was updated, Liquid Haskell's `D` component will be incremented.++To increment the `C` component of Liquid Fixpoint, and strip the `D` component:++```+./path/to/bumper --minor liquid-fixpoint+```++As before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell.++To increment the `B` component of Liquid Fixpoint, and strip the `D` and `C` components:++```+./path/to/bumper --major liquid-fixpoint+```++As before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell++SMTLIB2 Interface+-----------------++There is a new SMTLIB2 interface directly from Haskell:+++ Language.Fixpoint.SmtLib2++See `tests/smt2/{Smt.hs, foo.smt2}` for an example of how to use it.++Options+-------++`--higherorder` allows higher order binders into the environment++`--extsolver` runs the **deprecated** external solver.++`--parts` Partitions an `FInfo` into a `[FInfo]` and emits a bunch of files. So:++    $ fixpoint -n -p path/to/foo.fq++will now emit files:++    path/to/.liquid/foo.1.fq+    path/to/.liquid/foo.2.fq+    . . .+    path/to/.liquid/foo.k.fq++and also a dot file with the constraint dependency graph:++    path/to/.liquid/foo.fq.dot+++## FInfo Invariants++### Binders++This is the field++```+     , bs       :: !BindEnv         -- ^ Bind  |-> (Symbol, SortedReft)+```++or in the .fq files as++```+bind 1 x : ...+bind 2 y : ...+```++* Each `BindId` must be a distinct `Int`,+* Each `BindId` that appears in a constraint+  environment i.e. inside _any_ `IBindEnv`+  must appear inside the `bs`++### Environments++* Each constraint's environment is a set of `BindId`+  which must be defined in the `bindInfo`. Furthermore++* Each constraint should not have _duplicate_ names in its+  environment, that is if you have two binders++```+  bind 1 x : ...+  bind 12 x : ...+```++  Then a single `IBindEnv` should only mention _at most_+  one of `1` or `12`.++* There is also a "tree-shape" property that its a bit hard+  to describe ... TODO     ++### LHS++Each `slhs` of a constraint is a `SortedReft`.++- Each `SortredReft` is basically a `Reft` -- a logical predicate.+  The important bit is that a `KVar` i.e. terms of the formalized++```+     $k1[x1:=y1][x2:=y2]...[xn:=yn]+```++  That is represented in the `Expr` type as++```+  | PKVar  !KVar !Subst+```++  must appear _only_ at the **top-level** that is not under _any_+  other operators, i.e. not as a sub-`Expr` of other expressions.+++- This is basically a predicate that needs to be "well sorted"+  with respect to the `BindId`, intuitively++```+    x:int, y:int |- x + y : int+```++  is well sorted. but++```+    x:int  |- x + y : int+```++  is not, and++```+    x:int, y: list |- x + y : int+```++  is not. The exact definition is formalized in `Language.Fixpoint.SortCheck`+++### RHS++Similarly each `rhs` of a `SubC` must either be a single `$k[...]` or an plain `$k`-free `Expr`.++### Global vs. Distinct Literals++```+     , gLits    :: !(SEnv Sort)               -- ^ Global Constant symbols+     , dLits    :: !(SEnv Sort)       +```++The _global_ literals `gLits` are symbols that+are in scope _everywhere_ i.e. need not be separately+defined in individual environments. These include things like++- uninterpreted _measure_ functions `len`, `height`,+- uninterpreted _data constructor_ literals `True`, `False`++Suppose you have an enumerated type like:++```+data Day = Sun | Mon | Tue | Wed | ... | Sat+```++You can model the above values in fixpoint as:++```+constant lit#Sun : Day+constant lit#Mon : Day+constant lit#Tue : Day+constant lit#Wed : Day+```++The _distinct_ literals are a subset of the above where we+want to tell the SMT solver that the values are *distinct*+i.e. **not equal** to each other, for example, you can+**additionally** specify this as:++```+distinct lit#Sun : Day+distinct lit#Mon : Day+distinct lit#Tue : Day+distinct lit#Wed : Day+```++The above two are represented programmatically by generating   +suitable `Symbol` values (for the literals  see `litSymbol`)+and `Sort` values as `FTC FTycon` and then making an `SEnv`+from the `[(Symbol, Sort)]`.++### Sorts++> What's the difference between an FTC and an FObj?++In early versions of fixpoint, there was support for +three sorts for expressions (`Expr`) that were sent +to the SMT solver:++1. `int`+2. `bool`+3. "other"++The `FObj` sort was introduced to represent essentially _all_ +non-int and non-bool values (e.g. tuples, lists, trees, pointers...)++However, we later realized that it is valuable to keep _more_+precise information for `Expr`s and so we introduced the `FTC`+(fixpoint type constructor), which lets us represent the above+respectively as:++- `FTC "String" []`                   -- in Haskell `String`+- `FTC "Tuple"  [FInt, Bool]`         -- in Haskell `(Int, Bool)`+- `FTC "List" [FTC "List" [FInt]]`    -- in Haskell `[[Int]]`++> There is a comment that says FObj's are uninterpretted types;+> so probably a type the SMT solver doesn't know about?+> Does that then make FTC types that the SMT solver does+> know about (bools, ints, lists, sets, etc.)?++The SMT solver knows about `bool`, `int` and `set` (also `bitvector` +and `map`) but _all_ other types are _currently_ represented as plain +`Int` inside the SMT solver. However, we _will be_ changing this +to make use of SMT support for ADTs ...++To sum up: the `FObj` is there for historical reasons; it has been +subsumed by `FTC` which is what I recomend you use. However `FObj` +is there if you want a simple "unitype" / "any" type for terms +that are not "interpreted".+

@@ -0,0 +1,37 @@+# TODO++## Proper Encoding of DataTypes++```+(declare-datatypes (T) ((LL lnil (lcons (lhd T) (ltl LL)))))+(declare-fun l1 () (LL Int))+(declare-fun l2 () (LL Int))+(declare-fun l3 () (LL Int))+(declare-fun x  () Int)+(declare-fun zzz () Int)++(assert (not (= l1 (as lnil (LL Int)))))+(assert (not (= l2 (as lnil (LL Int)))))++(assert (= (lhd l1) (lhd l2)))+(assert (not (= l1 l2)))+(assert (= l3 (lcons x l2)))+(assert (> x 100))+(check-sat)++(get-model)+++(declare-fun xs () (LL Int))+(declare-fun ys () (LL Int))+(declare-fun y  () Int)++(assert (= xs (as lnil (LL Int))))+(assert (= ys (lcons y ys)))+(assert (= xs ys))+(check-sat)+++;; (assert (= (ltl l1) (ltl l2)))+;; (check-sat)+```

@@ -0,0 +1,32 @@+{ fetchgitLocal }:+{ mkDerivation, ansi-terminal, array, ascii-progress, async+, attoparsec, base, bifunctors, binary, boxes, bytestring, cereal+, cmdargs, containers, deepseq, directory, filemanip, filepath+, ghc-prim, hashable, intern, located-base, mtl, parallel, parsec, pretty+, process, stdenv, syb, tasty, tasty-hunit, tasty-rerun, text+, text-format, transformers, unordered-containers, z3+, dotgen, fgl, fgl-visualize+}:+mkDerivation {+  pname = "liquid-fixpoint";+  version = "9.9.9.9";+  src = fetchgitLocal ./.;+  isLibrary = true;+  isExecutable = true;+  libraryHaskellDepends = [+    ansi-terminal array ascii-progress async attoparsec base bifunctors+    binary boxes bytestring cereal cmdargs containers deepseq directory+    filemanip filepath ghc-prim hashable intern located-base mtl parallel parsec+    pretty process syb text text-format transformers+    unordered-containers+    dotgen fgl fgl-visualize+  ];+  executableHaskellDepends = [ base ];+  testHaskellDepends = [+    base directory filepath process tasty tasty-hunit tasty-rerun text+  ];+  testSystemDepends = [ z3 ];+  homepage = "https://github.com/ucsd-progsys/liquid-fixpoint";+  description = "Predicate Abstraction-based Horn-Clause/Implication Constraint Solver";+  license = stdenv.lib.licenses.bsd3;+}

@@ -1,6 +1,6 @@ name:                liquid-fixpoint-version:             0.5.0.1-Copyright:           2010-15 Ranjit Jhala, University of California, San Diego.+version:             0.6.0.1+Copyright:           2010-17 Ranjit Jhala, University of California, San Diego. synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver homepage:            https://github.com/ucsd-progsys/liquid-fixpoint license:             BSD3@@ -10,7 +10,10 @@ category:            Language build-type:          Simple cabal-version:       >=1.10+Tested-With:         GHC == 7.10.3, GHC == 8.0.1 ++ description:     This package is a Haskell wrapper to the SMTLIB-based                  Horn-Clause/Logical Implication constraint solver used                  for Liquid Types.@@ -48,7 +51,7 @@   if flag(devel)     ghc-options: -Werror   hs-source-dirs: bin-  Build-Depends: base >= 4.7 && < 5+  Build-Depends: base >= 4.8 && < 5                , liquid-fixpoint  Library@@ -56,6 +59,7 @@   ghc-options:     -W -fno-warn-missing-methods   if flag(devel)     ghc-options:   -Werror+  ghc-prof-options: -fprof-auto   hs-source-dirs:  src   Exposed-Modules: Language.Fixpoint.Types.Names,                    Language.Fixpoint.Types.Errors,@@ -68,15 +72,22 @@                    Language.Fixpoint.Types.Substitutions,                    Language.Fixpoint.Types.Environments,                    Language.Fixpoint.Types.Constraints,-                   Language.Fixpoint.Types.Graphs,+                   Language.Fixpoint.Types.Triggers,+                   Language.Fixpoint.Types.Solutions,                    Language.Fixpoint.Types.Utils,                    Language.Fixpoint.Types,+                   Language.Fixpoint.Graph.Types,+                   Language.Fixpoint.Graph.Reducible,+                   Language.Fixpoint.Graph.Indexed,+                   Language.Fixpoint.Graph.Partition,+                   Language.Fixpoint.Graph.Deps,+                   Language.Fixpoint.Graph,+                   Language.Fixpoint.Defunctionalize,                    Language.Fixpoint.Smt.Types,                    Language.Fixpoint.Smt.Bitvector,                    Language.Fixpoint.Smt.Theories,                    Language.Fixpoint.Smt.Serialize,                    Language.Fixpoint.Smt.Interface,-                   Language.Fixpoint.Partition,                    Language.Fixpoint.Minimize,                    Language.Fixpoint.Solver,                    Language.Fixpoint.Parse,@@ -84,8 +95,7 @@                    Language.Fixpoint.Misc,                    Language.Fixpoint.Utils.Progress,                    Language.Fixpoint.Utils.Files,-                   Language.Fixpoint.Solver.Types,-                   Language.Fixpoint.Solver.Graph,+                   Language.Fixpoint.Solver.GradualSolution,                    Language.Fixpoint.Solver.Solution,                    Language.Fixpoint.Solver.Worklist,                    Language.Fixpoint.Solver.Monad,@@ -93,11 +103,13 @@                    Language.Fixpoint.Solver.UniqifyKVars,                    Language.Fixpoint.Solver.UniqifyBinds,                    Language.Fixpoint.Solver.Eliminate,-                   Language.Fixpoint.Solver.Validate,+                   Language.Fixpoint.Solver.Instantiate,+                   Language.Fixpoint.Solver.Sanitize,                    Language.Fixpoint.Utils.Statistics,+                   Language.Fixpoint.Solver.GradualSolve,                    Language.Fixpoint.Solver.Solve -  Build-Depends: base >= 4.7 && < 5+  Build-Depends: base >= 4.8 && < 5                , array                , async                , attoparsec@@ -130,6 +142,8 @@                , fgl                , fgl-visualize                , dotgen+               , time+   if impl(ghc >= 7.10.2)     Build-Depends: located-base   if !os(windows)@@ -154,3 +168,59 @@                     tasty-hunit,                     tasty-rerun >= 1.1,                     text++test-suite testparser+  default-language: Haskell98+  type:             exitcode-stdio-1.0+  hs-source-dirs:   tests+  ghc-options:      -threaded+  if flag(devel)+    ghc-options:    -Werror+  main-is:          testParser.hs+  build-depends:    base,+                    directory,+                    filepath,+                    tasty >= 0.10,+                    tasty-hunit,+                    tasty-rerun >= 1.1,+                    text+  if flag(devel)+    hs-source-dirs:   tests src+    build-depends:+                 array+               , async+               , attoparsec+               , syb+               , cmdargs+               , ansi-terminal+               , bifunctors+               , binary+               , bytestring+               , containers+               , deepseq+               , directory+               , filemanip+               , filepath+               , ghc-prim+               , intern+               , mtl+               , parsec+               , pretty+               , boxes+               , parallel+               , process+               , syb+               , text+               , transformers+               , hashable+               , unordered-containers+               , cereal+               , text-format+               , fgl+               , fgl-visualize+               , dotgen+               , time+    if impl(ghc >= 7.10.2)+      Build-Depends: located-base+  else+    build-depends: liquid-fixpoint

@@ -0,0 +1,137 @@+#!/bin/bash++set -eu+set -o pipefail++## Helper Functions++function loud {+  echo "$ $@"+  $@+}++# Source: https://github.com/travis-ci/travis-build/blob/fc4ae8a2ffa1f2b3a2f62533bbc4f8a9be19a8ae/lib/travis/build/script/templates/header.sh#L104-L123+RED="\033[31;1m"+GREEN="\033[32;1m"+RESET="\033[0m"+function travis_retry {+  local result=0+  local count=1+  while [ $count -le 3 ]; do+    [ $result -ne 0 ] && {+      echo -e "\n${RED}The command \"$@\" failed. Retrying, $count of 3.${RESET}\n" >&2+    }+    set +e+    "$@"+    result=$?+    set -e+    [ $result -eq 0 ] && break+    count=$(($count + 1))+    sleep 1+  done++  [ $count -eq 4 ] && {+    echo "\n${RED}The command \"$@\" failed 3 times.${RESET}\n" >&2+  }++  return $result+}++function prevent_timeout {+  local cmd="$@"++  $cmd &+  local cmd_pid=$!++  poke_stdout &+  local poke_pid=$!++  wait $cmd_pid+  exit_code=$?++  kill $poke_pid+  (wait $poke_pid 2>/dev/null) || true++  return $exit_code+}++function poke_stdout {+  # Print an invisible character every minute+  while true; do+    echo -ne "\xE2\x80\x8B"+    sleep 60+  done+}++function pastebin {+  curl -s -F 'clbin=<-' https://clbin.com+}++## Testing Stages++function clean_cache {+  local smt="$1"++  loud ghc-pkg unregister liquid-fixpoint --force || true+  loud rm "$HOME/.cabal/bin/$smt" || true+}++function install_smt {+  local smt="$1"++  mkdir -p "$HOME/.cabal/bin"+  loud curl "http://goto.ucsd.edu/~gridaphobe/$smt" -o "$HOME/.cabal/bin/$smt"+  loud chmod a+x "$HOME/.cabal/bin/$smt"+}++function install_cabal_deps {+  if ! _install_cabal_deps; then+    echo " ==> Cabal install failed. Clearing dependency cache and retrying."+    loud rm -rf "$HOME/.cabal"+    loud rm -rf "$HOME/.ghc"+    _install_cabal_deps+  fi+}++function _install_cabal_deps {+  loud travis_retry cabal update || return 1+  loud travis_retry cabal install --only-dependencies --enable-tests || return 1+}++function do_build {+  loud cabal configure -fbuild-external --enable-tests -v2+  loud prevent_timeout cabal build -j2+  loud cabal haddock+}++function do_test {+  loud prevent_timeout ./dist/build/test/test+}++function dump_fail_logs {+  find . -type f -wholename '*/.liquid/*' -name '*.log' -print0 | while IFS= read -r -d $'\0' file; do+    echo "${file}:"+    echo "    $(pastebin < "${file}")"+  done+}++function test_source_pkg {+  loud cabal sdist++  local src_tgz="dist/$(cabal info . | awk '{print $2 ".tar.gz";exit}')"++  if [ -f "$src_tgz" ]; then+    loud prevent_timeout cabal install -j4 "$src_tgz"+  else+    echo "expected '$src_tgz' not found"+    return 1+  fi+}++## Run Test Stage++stage="$1"+shift++$stage "$@"+

@@ -0,0 +1,17 @@+{ nixpkgs ? import <nixpkgs> {}, compiler ? "default" }:++let++  inherit (nixpkgs) pkgs;++  f = import ./default.nix { inherit (pkgs) fetchgitLocal; };++  haskellPackages = if compiler == "default"+                       then pkgs.haskellPackages+                       else pkgs.haskell.packages.${compiler};++  drv = haskellPackages.callPackage f { inherit (pkgs) z3; };++in++  if pkgs.lib.inNixShell then drv.env else drv

@@ -0,0 +1,368 @@+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE TupleSections        #-}+{-# LANGUAGE PatternGuards        #-}+{-# LANGUAGE OverloadedStrings    #-}++--------------------------------------------------------------------------------+-- | `defunctionalize` traverses the query to:+--      1. "normalize" lambda terms by renaming binders,+--      2. generate alpha- and beta-equality axioms for+--   The lambdas and redexes found in the query.+--+--   NOTE: `defunctionalize` should happen **BEFORE**+--   `elaborate` as the latter converts all actual `EApp`+--   into the (uninterpreted) `smt_apply`.+--   We cannot elaborate prior to `defunc` as we need the+--   `EApp` and `ELam` to determine the lambdas and redexes.+--------------------------------------------------------------------------------++module Language.Fixpoint.Defunctionalize (defunctionalize, Defunc(..), defuncAny, makeLamArg) where++import qualified Data.HashMap.Strict as M+import           Data.Hashable+import           Data.Maybe             (isJust, maybeToList)+import qualified Data.List           as L++import           Control.Monad.State+import           Language.Fixpoint.Misc            (sortNub, fM, whenM, secondM, mapSnd)+import           Language.Fixpoint.Solver.Sanitize (symbolEnv)+import           Language.Fixpoint.Types        hiding (allowHO)+import           Language.Fixpoint.Types.Config+import           Language.Fixpoint.SortCheck       (checkSortExpr)+import           Language.Fixpoint.Types.Visitor   (mapMExpr, stripCasts)+-- import Debug.Trace (trace)++defunctionalize :: (Fixpoint a) => Config -> SInfo a -> SInfo a+defunctionalize cfg si = evalState (defunc si) (makeInitDFState cfg si)++defuncAny :: Defunc a => Config -> SEnv Sort -> a -> a +defuncAny cfg env e = evalState (defunc e) (makeDFState cfg env emptyIBindEnv)+++--------------------------------------------------------------------------------+-- | Expressions defunctionalization -------------------------------------------+--------------------------------------------------------------------------------+txExpr :: Expr -> DF Expr+txExpr e = do+  hoFlag <- gets dfHO+  if hoFlag then defuncExpr e else return e++defuncExpr :: Expr -> DF Expr+defuncExpr = mapMExpr reBind+         >=> mapMExpr logLam+         >=> mapMExpr logRedex+         >=> mapMExpr (fM normalizeLams)++reBind :: Expr -> DF Expr+reBind (ELam (x, s) e) = (\y -> ELam (y, s) (subst1 e (x, EVar y))) <$> freshSym s+reBind e               = return e++maxLamArg :: Int+maxLamArg = 7++-- NIKI TODO: allow non integer lambda arguments+-- sorts = [setSort intSort, bitVecSort intSort, mapSort intSort intSort, boolSort, realSort, intSort]+makeLamArg :: Sort -> Int -> Symbol+makeLamArg _ = intArgName++--------------------------------------------------------------------------------++makeAxioms :: DF [Expr]+makeAxioms = do+  alphEqs <- concatMap makeAlphaAxioms <$> getLams+  betaEqs <- concatMap makeBetaAxioms  <$> getRedexes+  env     <- gets dfEnv+  return   $ filter (validAxiom env) (alphEqs ++ betaEqs)++validAxiom :: SEnv Sort -> Expr -> Bool+validAxiom env = isJust . checkSortExpr env++--------------------------------------------------------------------------------+-- | Alpha Equivalence ---------------------------------------------------------+--------------------------------------------------------------------------------+makeAlphaAxioms ::  Expr -> [Expr]+makeAlphaAxioms = makeAlphaEq . normalizeLams++makeAlphaEq :: Expr -> [Expr]+makeAlphaEq e = go e ++ go' e+  where+    go ee+      = makeEqForAll ee (normalize ee)+    go' ee@(ELam (x, s) e)+      = [makeEq ee ee'+         | (i, ee') <- map (\j -> normalizeLamsFromTo j (ELam (x, s) e)) [1..maxLamArg-1]+         , i <= maxLamArg ]+    go' _+      = []++--------------------------------------------------------------------------------+-- | Normalizations ------------------------------------------------------------+--------------------------------------------------------------------------------++-- head normal form [TODO: example]++normalize :: Expr -> Expr+normalize = snd . go+  where+    go (ELam (y, sy) e) = let (i', e') = go e+                              y'      = makeLamArg sy i'+                          in (i'+1, ELam (y', sy) (e' `subst1` (y, EVar y')))+    go (EApp e e2)+      |  (ELam (x, _) bd) <- unECst e+                        = let (i1, e1') = go bd+                              (i2, e2') = go e2+                          in (max i1 i2, e1' `subst1` (x, e2'))+    go (EApp e1 e2)     = let (i1, e1') = go e1+                              (i2, e2') = go e2+                          in (max i1 i2, EApp e1' e2')+    go (ECst e s)       = mapSnd (`ECst` s) (go e)+    go (PAll bs e)      = mapSnd (PAll bs)  (go e)+    go e                = (1, e)++    unECst (ECst e _) = unECst e+    unECst e          = e++-- normalize lambda arguments [TODO: example]++normalizeLams :: Expr -> Expr+normalizeLams e = snd $ normalizeLamsFromTo 1 e++normalizeLamsFromTo :: Int -> Expr -> (Int, Expr)+normalizeLamsFromTo i   = go+  where+    go (ELam (y, sy) e) = let (i', e') = go e+                              y'      = makeLamArg sy i'+                          in (i' + 1, ELam (y', sy) (e' `subst1` (y, EVar y')))+    go (EApp e1 e2)     = let (i1, e1') = go e1+                              (i2, e2') = go e2+                          in (max i1 i2, EApp e1' e2')+    go (ECst e s)       = mapSnd (`ECst` s) (go e)+    go (PAll bs e)      = mapSnd (PAll bs) (go e)+    go e                = (i, e)++--------------------------------------------------------------------------------+-- | Beta Equivalence ----------------------------------------------------------+--------------------------------------------------------------------------------+makeBetaAxioms :: Expr -> [Expr]+makeBetaAxioms e = makeEqForAll (normalizeLams e) (normalize e)+  -- where+  --  e             = trace ("BETA-NL e = " ++ showpp e0) e0++makeEq :: Expr -> Expr -> Expr+makeEq e1 e2+  | e1 == e2  = PTrue+  | otherwise = EEq e1 e2++makeEqForAll :: Expr -> Expr -> [Expr]+makeEqForAll e1 e2 = [ makeEq (closeLam su e1') (closeLam su e2') | su <- instantiate xs]+  where+    (xs1, e1')     = splitPAll [] e1+    (xs2, e2')     = splitPAll [] e2+    xs             = L.nub (xs1 ++ xs2)++closeLam :: [(Symbol, (Symbol, Sort))] -> Expr -> Expr+closeLam ((x,(y,s)):su) e = ELam (y,s) (subst1 (closeLam su e) (x, EVar y))+closeLam []             e = e++splitPAll :: [(Symbol, Sort)] -> Expr -> ([(Symbol, Sort)], Expr)+splitPAll acc (PAll xs e) = splitPAll (acc ++ xs) e+splitPAll acc e           = (acc, e)++-- NOPROP instantiate :: [(Symbol, Sort)] -> [[(Symbol, (Symbol,Sort))]]+-- NOPROP instantiate []     = [[]]+-- NOPROP instantiate xs     = L.foldl' (\acc x -> combine (instOne x) acc) [] xs+  -- NOPROP where+    -- NOPROP instOne (x, s) = [(x, (makeLamArg s i, s)) | i <- [1..maxLamArg]]+    -- NOPROP combine xs []  = [[x] | x <- xs]+    -- NOPROP combine xs acc = concat [(x:) <$> acc | x <- xs]++instantiate    :: [(Symbol, Sort)] -> [[(Symbol, (Symbol,Sort))]]+instantiate     = choices . map inst1+  where+    inst1 (x,s) = [(x, (makeLamArg s i, s)) | i <- [1..maxLamArg]]++choices :: [[a]] -> [[a]]+choices []       = [[]]+choices (xs:xss) = [a:as | a <- xs, as <- choices xss]++--------------------------------------------------------------------------------+-- | Containers defunctionalization --------------------------------------------+--------------------------------------------------------------------------------++class Defunc a where+  defunc :: a -> DF a++instance (Defunc (c a), TaggedC c a) => Defunc (GInfo c a) where+  defunc fi = do+    cm'    <- defunc $ cm    fi+    ws'    <- defunc $ ws    fi+    -- NOPROP setBinds $ mconcat ((senv <$> M.elems (cm fi)) ++ (wenv <$> M.elems (ws fi)))+    gLits' <- defunc $ gLits fi+    dLits' <- defunc $ dLits fi+    bs'    <- defunc $ bs    fi+    ass'   <- defunc $ asserts fi +    -- NOPROP quals' <- defunc $ quals fi+    axioms <- makeAxioms+    return $ fi { cm      = cm'+                , ws      = ws'+                , gLits   = gLits'+                , dLits   = dLits'+                , bs      = bs'+                -- NOPROP , quals   = quals'+                , asserts = (noTrigger <$> axioms) ++ ass' +                }++instance (Defunc a) => Defunc (Triggered a) where+  defunc (TR t e) = TR t <$> defunc e ++instance Defunc (SimpC a) where+  defunc sc = do crhs' <- defunc $ _crhs sc+                 return $ sc {_crhs = crhs'}++instance Defunc (WfC a)   where+  defunc wf@(WfC {}) = do+    let (x, t, k) = wrft wf+    t' <- defunc t+    return $ wf { wrft = (x, t', k) }+  defunc wf@(GWfC {}) = do+    let (x, t, k) = wrft wf+    t' <- defunc t+    e' <- defunc $ wexpr wf+    return $ wf { wrft = (x, t', k), wexpr = e' }++instance Defunc SortedReft where+  defunc (RR s r) = RR s <$> defunc r++instance Defunc (Symbol, SortedReft) where+  defunc (x, sr) = (x,) <$> defunc sr++instance Defunc (Symbol, Sort) where+  defunc (x, t) = (x,) <$> defunc t++instance Defunc Reft where+  defunc (Reft (x, e)) = Reft . (x,) <$> defunc e++instance Defunc Expr where+  defunc = txExpr++instance Defunc a => Defunc (SEnv a) where+  defunc = mapMSEnv defunc++instance Defunc BindEnv   where+  defunc bs = do dfbs <- gets dfBEnv+                 let f (i, xs) = if i `memberIBindEnv` dfbs+                                       then  (i,) <$> defunc xs+                                       else  (i,) <$> matchSort xs+                 mapWithKeyMBindEnv f bs+   where+    -- The refinement cannot be elaborated thus defunc-ed because+    -- the bind does not appear in any contraint,+    -- thus unique binders does not perform properly+    -- The sort should be defunc, to ensure same sort on double binders+    matchSort (x, RR s r) = ((x,) . (`RR` r)) <$> defunc s++-- Sort defunctionalization [should be done by elaboration]+instance Defunc Sort where+  defunc = return++instance Defunc a => Defunc [a] where+  defunc = mapM defunc++instance (Defunc a, Eq k, Hashable k) => Defunc (M.HashMap k a) where+  defunc m = M.fromList <$> mapM (secondM defunc) (M.toList m)++type DF    = State DFST++data DFST = DFST+  { dfFresh   :: !Int+  , dfEnv   :: !(SEnv Sort)+  , dfBEnv  :: !IBindEnv+  , dfLam   :: !Bool        -- ^ normalize lams+  , dfExt   :: !Bool        -- ^ enable extensionality axioms+  , dfAEq   :: !Bool        -- ^ enable alpha equivalence axioms+  , dfBEq   :: !Bool        -- ^ enable beta equivalence axioms+  , dfNorm  :: !Bool        -- ^ enable normal form axioms+  , dfHO    :: !Bool        -- ^ allow higher order thus defunctionalize+  , dfLNorm :: !Bool+  , dfLams  :: ![Expr]      -- ^ lambda expressions appearing in the expressions+  , dfRedex :: ![Expr]      -- ^ redexes appearing in the expressions+  , dfBinds :: !(SEnv Sort) -- ^ sorts of new lambda-binders+  }+++makeDFState :: Config -> SEnv Sort -> IBindEnv -> DFST+makeDFState cfg senv ibind = DFST+  { dfFresh = 0+  , dfEnv   = senv +  , dfBEnv  = ibind+  , dfLam   = True+  , dfExt   = False +  , dfAEq   = alphaEquivalence cfg+  , dfBEq   = betaEquivalence  cfg+  , dfNorm  = normalForm       cfg+  , dfHO    = allowHO cfg  || defunction cfg+  , dfLNorm = True+  -- INVARIANT: lambads and redexes are not defunctionalized+  , dfLams  = []+  , dfRedex = []+  , dfBinds = mempty+  }+++makeInitDFState :: Config -> SInfo a -> DFST+makeInitDFState cfg si +  = makeDFState cfg +         (symbolEnv cfg si) +         (mconcat ((senv <$> M.elems (cm si)) ++ (wenv <$> M.elems (ws si))))++--------------------------------------------------------------------------------+-- | Low level monad manipulation ----------------------------------------------+--------------------------------------------------------------------------------+freshSym :: Sort -> DF Symbol+freshSym t = do+  n    <- gets dfFresh+  let x = intSymbol "lambda_fun_" n+  modify $ \s -> s {dfFresh = n + 1, dfBinds = insertSEnv x t (dfBinds s)}+  return x++logLam :: Expr -> DF Expr+logLam e = whenM (gets dfAEq) (putLam e) >> return e++logRedex :: Expr -> DF Expr+logRedex e = whenM (gets dfBEq) (putRedex e) >> return e++putLam :: Expr -> DF ()+putLam e@(ELam {}) = modify $ \s -> s { dfLams = e : dfLams s}+putLam _           = return ()++putRedex :: Expr -> DF ()+putRedex e@(EApp f _)+  | ELam _ _ <- stripCasts f+  = modify $ \s -> s { dfRedex = e : dfRedex s }+putRedex _+  = return ()+++-- | getLams and getRedexes return the (previously seen) lambdas and redexes,+--   after "closing" them by quantifying out free vars corresponding to the+--   fresh binders in `dfBinds`.+getLams    :: DF [Expr]+getLams    = getClosedField dfLams++getRedexes :: DF [Expr]+getRedexes = getClosedField dfRedex++getClosedField :: (DFST -> [Expr]) -> DF [Expr]+getClosedField fld = do+  env <- gets dfBinds+  es  <- gets fld+  return (closeLams env <$> es)++closeLams :: SEnv Sort -> Expr -> Expr+closeLams env e = PAll (freeBinds env e) e++freeBinds :: SEnv Sort -> Expr -> [(Symbol, Sort)]+freeBinds env e = [ (y, t) | y <- sortNub (syms e)+                           , t <- maybeToList (lookupSEnv y env) ]

@@ -0,0 +1,10 @@+-- | This module re-exports the data types, operations and+--   serialization functions for representing and computing+--   with constraint dependencies.++module Language.Fixpoint.Graph (module X ) where++import Language.Fixpoint.Graph.Types     as X+import Language.Fixpoint.Graph.Partition as X+import Language.Fixpoint.Graph.Reducible as X+import Language.Fixpoint.Graph.Deps      as X

@@ -0,0 +1,549 @@+{-# LANGUAGE TupleSections         #-}+{-# LANGUAGE OverloadedStrings     #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE RecordWildCards       #-}++module Language.Fixpoint.Graph.Deps (+       -- * Remove Constraints that don't affect Targets+         slice++       -- * Predicate describing Targets+       , isTarget++      -- * Eliminatable KVars+      , Elims (..)+      , elimVars+      , elimDeps++      -- * Compute Raw Dependencies+      , kvEdges++      -- * Partition+      , decompose++      -- * Debug+      , graphStatistics+      ) where++import           Prelude hiding (init)+import           Data.Maybe                       (mapMaybe, fromMaybe)+import           Data.Tree (flatten)+import           Language.Fixpoint.Misc+import           Language.Fixpoint.Utils.Files+import           Language.Fixpoint.Types.Config+import qualified Language.Fixpoint.Types.Visitor      as V+import           Language.Fixpoint.Types.PrettyPrint+import qualified Language.Fixpoint.Types              as F+import           Language.Fixpoint.Graph.Types+import           Language.Fixpoint.Graph.Reducible  (isReducible)+import           Language.Fixpoint.Graph.Indexed++import           Control.Monad             (when)+import qualified Data.HashSet                         as S+import qualified Data.List                            as L+import qualified Data.HashMap.Strict                  as M+import qualified Data.Graph                           as G+import           Data.Function (on)+import           Data.Hashable+import           Text.PrettyPrint.HughesPJ+import           Debug.Trace (trace)++--------------------------------------------------------------------------------+-- | Compute constraints that transitively affect target constraints,+--   and delete everything else from F.SInfo a+--------------------------------------------------------------------------------+slice :: (F.TaggedC c a) => Config -> F.GInfo c a -> F.GInfo c a+--------------------------------------------------------------------------------+slice cfg fi +  | noslice cfg +  = fi +  | otherwise+  = fi { F.cm = cm'+       , F.ws = ws' }+  where+     cm' = M.filterWithKey inC (F.cm fi)+     ws' = M.filterWithKey inW (F.ws fi)+     ks  = sliceKVars fi sl+     is  = S.fromList (slKVarCs sl ++ slConcCs sl)+     sl  = mkSlice fi+     inC i _ = S.member i is+     inW k _ = S.member k ks++sliceKVars :: (F.TaggedC c a) => F.GInfo c a -> Slice -> S.HashSet F.KVar+sliceKVars fi sl = S.fromList $ concatMap (subcKVars be) cs+  where+    cs           = lookupCMap cm <$> slKVarCs sl ++ slConcCs sl+    be           = F.bs fi+    cm           = F.cm fi++subcKVars :: (F.TaggedC c a) => F.BindEnv -> c a -> [F.KVar]+subcKVars be c = V.envKVars be c ++ V.rhsKVars c++--------------------------------------------------------------------------------+mkSlice :: (F.TaggedC c a) => F.GInfo c a -> Slice+--------------------------------------------------------------------------------+mkSlice fi        = mkSlice_ (F.cm fi) g' es v2i i2v+  where+    g'            = G.transposeG g  -- "inverse" of g (reverse the dep-edges)+    (g, vf, cf)   = G.graphFromEdges es+    es            = gEdges $ cGraph fi+    v2i           = fst3 . vf+    i2v i         = fromMaybe (errU i) $ cf i+    errU i        = errorstar $ "graphSlice: Unknown constraint " ++ show i++mkSlice_ :: F.TaggedC c a+         => M.HashMap F.SubcId (c a)+         -> G.Graph+         -> [DepEdge]+         -> (G.Vertex -> F.SubcId)+         -> (F.SubcId -> G.Vertex)+         -> Slice+mkSlice_ cm g' es v2i i2v = Slice { slKVarCs = kvarCs+                                  , slConcCs = concCs+                                  , slEdges  = sliceEdges kvarCs es+                                  }+  where+    -- n                  = length kvarCs+    concCs             = [ i | (i, c) <- M.toList cm, isTarget c ]+    kvarCs             = v2i <$> reachVs+    rootVs             = i2v <$> concCs+    reachVs            = concatMap flatten $ G.dfs g' rootVs++sliceEdges :: [F.SubcId] -> [DepEdge] -> [DepEdge]+sliceEdges is es = [ (i, i, filter inSlice js) | (i, _, js) <- es, inSlice i ]+  where+    inSlice i    = M.member i im+    im           = M.fromList $ (, ()) <$> is++-- | DO NOT DELETE!+-- sliceCSucc :: Slice -> CSucc+-- sliceCSucc sl = \i -> M.lookupDefault [] i im+  -- where+    -- im        = M.fromList [(i, is) | (i,_,is) <- slEdges sl]++--------------------------------------------------------------------------------+isTarget :: (F.TaggedC c a) => c a -> Bool+--------------------------------------------------------------------------------+isTarget c   = V.isConcC c && isNonTriv c+  where+   isNonTriv = not .  F.isTautoPred . F.crhs+++--------------------------------------------------------------------------------+-- | Constraint Graph ----------------------------------------------------------+--------------------------------------------------------------------------------+cGraph :: (F.TaggedC c a) => F.GInfo c a -> CGraph+---------------------------------------------------------------------------+cGraph fi = CGraph { gEdges = es+                   , gRanks = outRs+                   , gSucc  = next+                   , gSccs  = length sccs }+  where+    es             = [(i, i, M.lookupDefault [] i next) | i <- M.keys $ F.cm fi]+    next           = kvSucc fi+    (g, vf, _)     = G.graphFromEdges es+    (outRs, sccs)  = graphRanks g vf++--------------------------------------------------------------------------------+-- | Ranks from Graph ----------------------------------------------------------+--------------------------------------------------------------------------------+graphRanks :: G.Graph -> (G.Vertex -> DepEdge) -> (CMap Int, [[G.Vertex]])+---------------------------------------------------------------------------+graphRanks g vf = (M.fromList irs, sccs)+  where+    irs        = [(v2i v, r) | (r, vs) <- rvss, v <- vs ]+    rvss       = zip [0..] sccs+    sccs       = L.reverse $ map flatten $ G.scc g+    v2i        = fst3 . vf++--------------------------------------------------------------------------------+-- | Dependencies --------------------------------------------------------------+--------------------------------------------------------------------------------+kvSucc :: (F.TaggedC c a) => F.GInfo c a -> CMap [F.SubcId]+--------------------------------------------------------------------------------+kvSucc fi = succs cm rdBy+  where+    rdBy  = kvReadBy fi+    cm    = F.cm     fi++succs :: (F.TaggedC c a) => CMap (c a) -> KVRead -> CMap [F.SubcId]+succs cm rdBy = (sortNub . concatMap kvReads . kvWrites) <$> cm+  where+    kvReads k = M.lookupDefault [] k rdBy+    kvWrites  = V.kvars . F.crhs++--------------------------------------------------------------------------------+kvWriteBy :: (F.TaggedC c a) => CMap (c a) -> F.SubcId -> [F.KVar]+--------------------------------------------------------------------------------+kvWriteBy cm = V.kvars . F.crhs . lookupCMap cm++--------------------------------------------------------------------------------+kvReadBy :: (F.TaggedC c a) => F.GInfo c a -> KVRead+--------------------------------------------------------------------------------+kvReadBy fi = group [ (k, i) | (i, ci) <- M.toList cm+                             , k       <- V.envKVars bs ci]+  where+    cm      = F.cm fi+    bs      = F.bs fi++--------------------------------------------------------------------------------+decompose :: (F.TaggedC c a) => F.GInfo c a -> KVComps+--------------------------------------------------------------------------------+decompose = componentsWith (kvgEdges . kvGraph)++--------------------------------------------------------------------------------+kvGraph :: (F.TaggedC c a) => F.GInfo c a -> KVGraph+--------------------------------------------------------------------------------+kvGraph = edgeGraph . kvEdges++edgeGraph :: [CEdge] -> KVGraph+edgeGraph es = KVGraph [(v, v, vs) | (v, vs) <- groupList es ]++kvEdges :: (F.TaggedC c a) => F.GInfo c a -> [CEdge]+kvEdges fi = selfes ++ concatMap (subcEdges bs) cs+  where+    bs     = F.bs fi+    cs     = M.elems (F.cm fi)+    ks     = fiKVars fi+    selfes =  [(Cstr i , Cstr  i) | c <- cs, let i = F.subcId c]+           ++ [(KVar k , DKVar k) | k <- ks]+           ++ [(DKVar k, DKVar k) | k <- ks]++fiKVars :: F.GInfo c a -> [F.KVar]+fiKVars = M.keys . F.ws++subcEdges :: (F.TaggedC c a) => F.BindEnv -> c a -> [CEdge]+subcEdges bs c =  [(KVar k, Cstr i ) | k  <- V.envKVars bs c]+               ++ [(Cstr i, KVar k') | k' <- V.rhsKVars c ]+  where+    i          = F.subcId c++--------------------------------------------------------------------------------+-- | Eliminated Dependencies+--------------------------------------------------------------------------------+elimDeps :: F.SInfo a -> [CEdge] -> S.HashSet F.KVar -> CDeps+elimDeps si es nonKutVs = graphDeps si es'+  where+    es'                 = graphElim es nonKutVs+    _msg                = "graphElim: " ++ show (length es')++{- | `graphElim` "eliminates" a kvar k by replacing every "path"++          ki -> ci -> k -> c++      with an edge++          ki ------------> c+-}+graphElim :: [CEdge] -> S.HashSet F.KVar -> [CEdge]+graphElim es ks = ikvgEdges $ elimKs ks $ edgesIkvg es+  where+    elimKs      = flip (S.foldl' elimK)++elimK  :: IKVGraph -> F.KVar -> IKVGraph+elimK g k   = (g `addLinks` es') `delNodes` (kV : cis)+  where+   es'      = [(ki, c) | ki@(KVar _) <- kis, c@(Cstr _) <- cs]+   cs       = getSuccs g kV+   cis      = getPreds g kV+   kis      = concatMap (getPreds g) cis+   kV       = KVar k++--------------------------------------------------------------------------------+-- | Generic Dependencies ------------------------------------------------------+--------------------------------------------------------------------------------+data Elims a+  = Deps { depCuts    :: !(S.HashSet a)+         , depNonCuts :: !(S.HashSet a)+         }+    deriving (Show)++instance PPrint (Elims a) where+  pprintTidy _ d = "#Cuts ="    <+> ppSize (depCuts d) <+>+                   "#NonCuts =" <+> ppSize (depNonCuts d)+    where+      ppSize     = pprint . S.size++instance (Eq a, Hashable a) => Monoid (Elims a) where+  mempty                            = Deps S.empty S.empty+  mappend (Deps d1 n1) (Deps d2 n2) = Deps (S.union d1 d2) (S.union n1 n2)++dCut, dNonCut :: (Hashable a) => a -> Elims a+dNonCut v = Deps S.empty (S.singleton v)+dCut    v = Deps (S.singleton v) S.empty++--------------------------------------------------------------------------------+-- | Compute Dependencies and Cuts ---------------------------------------------+--------------------------------------------------------------------------------+elimVars :: (F.TaggedC c a) => Config -> F.GInfo c a -> ([CEdge], Elims F.KVar)+--------------------------------------------------------------------------------+elimVars cfg si = (es, ds)+  where+    ds          = edgeDeps cfg si es+    es          = kvEdges si++removeKutEdges ::  S.HashSet F.KVar -> [CEdge] -> [CEdge]+removeKutEdges ks = filter (not . isKut . snd)+  where+    cutVs         = S.map KVar ks+    isKut         = (`S.member` cutVs)++cutVars :: (F.TaggedC c a) => Config -> F.GInfo c a -> S.HashSet F.KVar+cutVars cfg si+  | autoKuts cfg = S.empty+  | otherwise    = F.ksVars . F.kuts $ si++forceKuts :: (Hashable a, Eq a) => S.HashSet a -> Elims a  -> Elims a+forceKuts xs (Deps cs ns) = Deps (S.union cs xs) (S.difference ns xs)++edgeDeps :: (F.TaggedC c a) => Config -> F.GInfo c a -> [CEdge] -> Elims F.KVar+edgeDeps cfg si  = forceKuts ks+                 . edgeDeps' cfg+                 . removeKutEdges ks+                 . filter isRealEdge+  where+    ks           = givenKs `S.union` nlKs+    givenKs      = cutVars cfg    si+    nlKs+      | nonLinCuts cfg = nonLinearKVars si+      | otherwise      = mempty++edgeDeps' :: Config -> [CEdge] -> Elims F.KVar+edgeDeps' cfg es = Deps (takeK cs) (takeK ns)+  where+    Deps cs ns   = gElims cfg kF cutF g+    g            = kvgEdges    (edgeGraph es)+    cutF         = edgeRankCut (edgeRank es)+    takeK        = sMapMaybe tx+    tx (KVar z)  = Just z+    tx _         = Nothing+    kF (KVar _)  = True+    kF _         = False++sMapMaybe :: (Hashable b, Eq b) => (a -> Maybe b) -> S.HashSet a -> S.HashSet b+sMapMaybe f = S.fromList . mapMaybe f . S.toList++--------------------------------------------------------------------------------+type EdgeRank = M.HashMap F.KVar Integer+--------------------------------------------------------------------------------+edgeRank :: [CEdge] -> EdgeRank+edgeRank es = minimum . (n :) <$> kiM+  where+    n       = 1 + maximum [ i | (Cstr i, _)     <- es ]+    kiM     = group [ (k, i) | (KVar k, Cstr i) <- es ]++edgeRankCut :: EdgeRank -> Cutter CVertex+edgeRankCut km vs = case ks of+                      []  -> Nothing+                      k:_ -> Just (KVar k, [x | x@(u,_,_) <- vs, u /= KVar k])+  where+    ks            = orderBy [k | (KVar k, _ ,_) <- vs]+    rank          = (km M.!)+    orderBy       = L.sortBy (compare `on` rank)++--------------------------------------------------------------------------------+type Cutter a = [(a, a, [a])] -> Maybe (a, [(a, a, [a])])+--------------------------------------------------------------------------------++--------------------------------------------------------------------------------+type Cutable a = (Eq a, Ord a, Hashable a, Show a)+--------------------------------------------------------------------------------+gElims :: (Cutable a) => Config -> (a -> Bool) -> Cutter a -> [(a, a, [a])] -> Elims a+--------------------------------------------------------------------------------+gElims cfg kF cutF g = boundElims cfg kF g $ sccElims cutF g++--------------------------------------------------------------------------------+-- | `sccElims` returns an `Elims` that renders the dependency graph acyclic+--    by picking _at least one_ kvar from each non-trivial SCC in the graph+--------------------------------------------------------------------------------++sccElims :: (Cutable a) => Cutter a -> [(a, a, [a])] -> Elims a+sccElims f = sccsToDeps f . G.stronglyConnCompR++sccsToDeps :: (Cutable a) => Cutter a -> [G.SCC (a, a, [a])] -> Elims a+sccsToDeps f xs = mconcat $ sccDep f <$> xs++sccDep :: (Cutable a) =>  Cutter a -> G.SCC (a, a, [a]) -> Elims a+sccDep _ (G.AcyclicSCC (v,_,_)) = dNonCut v+sccDep f (G.CyclicSCC vs)      = cycleDep f vs++cycleDep :: (Cutable a) => Cutter a -> [(a, a, [a])] -> Elims a+cycleDep _ [] = mempty+cycleDep f vs = addCut f (f vs)++addCut :: (Cutable a) => Cutter a -> Maybe (a, [(a, a, [a])]) -> Elims a+addCut _ Nothing         = mempty+addCut f (Just (v, vs')) = mconcat $ dCut v : (sccDep f <$> sccs)+  where+    sccs                 = G.stronglyConnCompR vs'+++--------------------------------------------------------------------------------+-- | `boundElims` extends the input `Elims` by adding kuts that ensure that+--   the *maximum distance* between an eliminated KVar and a cut KVar is+--   *upper bounded* by a given threshold.+--------------------------------------------------------------------------------+boundElims :: (Cutable a) => Config -> (a -> Bool) -> [(a, a, [a])] -> Elims a -> Elims a+--------------------------------------------------------------------------------+boundElims cfg isK es ds = maybe ds (bElims isK es ds) (elimBound cfg)++bElims :: (Cutable a) => (a -> Bool) -> [(a, a, [a])] -> Elims a -> Int -> Elims a+bElims isK es ds dMax   = forceKuts kS' ds+  where+    (_ , kS')           = L.foldl' step (M.empty, depCuts ds) vs+    vs                  = topoSort ds es+    predM               = invertEdges es+    addK v ks+      | isK v           = S.insert v ks+      | otherwise       = ks++    zero                = (0, S.empty)++    step (dM, kS) v+      | v `S.member` kS = (M.insert v zero  dM,        kS)+      | vDist < dMax    = (M.insert v dv    dM,        kS)+      | otherwise       = (M.insert v zero  dM, addK v kS)+      where+        dv              = trace msg dv_+        msg             = show v ++ " DIST =" ++ show vDist ++ " SIZE = " ++ show vSize+        dv_@(vDist, s)  = distV predM v dM+        vSize           = S.size s++distV :: (Cutable a) => M.HashMap a [a] -> a -> M.HashMap a (Int, S.HashSet a) -> (Int, S.HashSet a)+distV predM v dM = (d, s)+  where+    d            = 1 + maximumDef 0 (fst . du <$> us)+    s            = S.insert v (S.unions (snd . du <$> us))+    du u         = fromMaybe (oops u) $ M.lookup u dM+    us           = M.lookupDefault [] v predM+    oops u       = errorstar $ "dist: don't have dist for " ++ show u ++ " when checking " ++ show v++topoSort :: (Cutable a) => Elims a -> [(a, a, [a])] -> [a]+topoSort ds = G.flattenSCCs . reverse . G.stronglyConnComp . ripKuts ds++ripKuts :: (Cutable a) => Elims a -> [(a, a, [a])] -> [(a, a, [a])]+ripKuts ds es = [ (u, x, notKuts vs) | (u, x, vs) <- es ]+  where+    notKuts   = filter (not . (`S.member` ks))+    ks        = depCuts ds++invertEdges :: (Cutable a) => [(a, a, [a])] -> M.HashMap a [a]+invertEdges es = group [ (v, u) | (u, _, vs) <- es, v <- vs ]++maximumDef :: (Ord a) => a -> [a] -> a+maximumDef d [] = d+maximumDef _ xs = maximum xs+++---------------------------------------------------------------------------+graphDeps :: F.SInfo a -> [CEdge] -> CDeps+---------------------------------------------------------------------------+graphDeps fi cs = CDs { cSucc   = gSucc cg+                      , cPrev   = cPrevM+                      , cNumScc = gSccs cg+                      , cRank   = M.fromList [(i, rf i) | i <- is ]+                      }+  where+    rf          = rankF (F.cm fi) outRs inRs+    inRs        = inRanks fi es outRs+    outRs       = gRanks cg+    es          = gEdges cg+    cg          = cGraphCE cs+    is          = [i | (Cstr i, _) <- cs]+    cPrevM      = sortNub <$> group [ (i, k) | (KVar k, Cstr i) <- cs ]++--TODO merge these with cGraph and kvSucc+cGraphCE :: [CEdge] -> CGraph+cGraphCE cs = CGraph { gEdges = es+                     , gRanks = outRs+                     , gSucc  = next+                     , gSccs  = length sccs }+  where+    es             = [(i, i, M.lookupDefault [] i next) | (Cstr i, _) <- cs]+    next           = cSuccM cs+    (g, vf, _)     = G.graphFromEdges es+    (outRs, sccs)  = graphRanks g vf++cSuccM      :: [CEdge] -> CMap [F.SubcId]+cSuccM es    = (sortNub . concatMap kRdBy) <$> iWrites+  where+    kRdBy k  = M.lookupDefault [] k kReads+    iWrites  = group [ (i, k) | (Cstr i, KVar k) <- es ]+    kReads   = group [ (k, j) | (KVar k, Cstr j) <- es ]++rankF :: CMap (F.SimpC a) -> CMap Int -> CMap Int -> F.SubcId -> Rank+rankF cm outR inR = \i -> Rank (outScc i) (inScc i) (tag i)+  where+    outScc        = lookupCMap outR+    inScc         = lookupCMap inR+    tag           = F._ctag . lookupCMap cm++---------------------------------------------------------------------------+inRanks :: F.SInfo a -> [DepEdge] -> CMap Int -> CMap Int+---------------------------------------------------------------------------+inRanks fi es outR+  | ks == mempty      = outR+  | otherwise         = fst $ graphRanks g' vf'+  where+    ks                = F.kuts fi+    cm                = F.cm fi+    (g', vf', _)      = G.graphFromEdges es'+    es'               = [(i, i, filter (not . isCut i) js) | (i,_,js) <- es ]+    isCut i j         = S.member i cutCIds && isEqOutRank i j+    isEqOutRank i j   = lookupCMap outR i == lookupCMap outR j+    cutCIds           = S.fromList [i | i <- M.keys cm, isKutWrite i ]+    isKutWrite        = any (`F.ksMember` ks) . kvWriteBy cm++--------------------------------------------------------------------------------+graphStatistics :: Config -> F.SInfo a -> IO ()+--------------------------------------------------------------------------------+graphStatistics cfg si = when (elimStats cfg) $ do+  -- writeGraph f  (kvGraph si)+  writeEdges f es'+  appendFile f . ppc . ptable $ graphStats cfg si+  where+    f        = queryFile Dot cfg+    es'      = removeKutEdges (depCuts ds) es+    (es, ds) = elimVars cfg si+    ppc d    = showpp $ vcat [" ", " ", "/*", pprint d, "*/"]++data Stats = Stats {+    stNumKVCuts   :: !Int   -- ^ number of kvars whose removal makes deps acyclic+  , stNumKVNonLin :: !Int   -- ^ number of kvars that appear >= 2 in some LHS+  , stNumKVTotal  :: !Int   -- ^ number of kvars+  , stIsReducible :: !Bool  -- ^ is dep-graph reducible+  , stSetKVNonLin :: !(S.HashSet F.KVar) -- ^ set of non-linear kvars+  }++instance PTable Stats where+  ptable (Stats {..})  = DocTable [+      ("# KVars [Cut]"    , pprint stNumKVCuts)+    , ("# KVars [NonLin]" , pprint stNumKVNonLin)+    , ("# KVars [All]"    , pprint stNumKVTotal)+    , ("# Reducible"      , pprint stIsReducible)+    , ("KVars NonLin"     , pprint stSetKVNonLin)+    ]++graphStats :: Config -> F.SInfo a -> Stats+graphStats cfg si = Stats {+    stNumKVCuts   = S.size $ F.tracepp "CUTS:" (depCuts d)+  , stNumKVNonLin = S.size  nlks+  , stNumKVTotal  = S.size (depCuts d) + S.size (depNonCuts d)+  , stIsReducible = isReducible si+  , stSetKVNonLin = nlks+  }+  where+    nlks          = nonLinearKVars si+    d             = snd $ elimVars cfg si++--------------------------------------------------------------------------------+nonLinearKVars :: (F.TaggedC c a) => F.GInfo c a -> S.HashSet F.KVar+--------------------------------------------------------------------------------+nonLinearKVars fi = S.unions $ nlKVarsC bs <$> cs+  where+    bs            = F.bs fi+    cs            = M.elems (F.cm fi)++nlKVarsC :: (F.TaggedC c a) => F.BindEnv -> c a -> S.HashSet F.KVar+nlKVarsC bs c = S.fromList [ k |  (k, n) <- V.envKVarsN bs c, n >= 2]

@@ -0,0 +1,100 @@+--------------------------------------------------------------------------------+-- | This module implements Indexed KV Graphs,+--   a representation of the KVGraph with a fast+--   succ, pred lookup+--------------------------------------------------------------------------------++{-# LANGUAGE OverloadedStrings #-}++module Language.Fixpoint.Graph.Indexed (+  -- * (Abstract) Indexed Graphs+    IKVGraph (..)++  -- * Constructor+  , edgesIkvg++  -- * Destructor+  , ikvgEdges++  -- * Modify+  , addLinks+  , delNodes++  -- * Lookup+  , getSuccs+  , getPreds+  ) where++import           Language.Fixpoint.Graph.Types+import qualified Data.HashSet              as S+import qualified Data.HashMap.Strict       as M+import qualified Data.List as L+import           Data.Hashable (Hashable)++--------------------------------------------------------------------------------+-- | `IKVGraph` is representation of the KVGraph with a fast succ, pred lookup+--------------------------------------------------------------------------------++data IKVGraph = IKVGraph+  { igSucc :: !(M.HashMap CVertex (S.HashSet CVertex))  -- ^ out-edges of a `CVertex`+  , igPred :: !(M.HashMap CVertex (S.HashSet CVertex))  -- ^ in-edges  of a `CVertex`+  } deriving (Show)+++addLinks :: IKVGraph -> [CEdge] -> IKVGraph+addLinks = L.foldl' addLink++addLink :: IKVGraph -> CEdge -> IKVGraph+addLink g (u, v) = addSucc (u, v) . addPred (u, v) $ g++delNodes :: IKVGraph -> [CVertex] -> IKVGraph+delNodes = L.foldl' delNode++delNode :: IKVGraph -> CVertex -> IKVGraph+delNode g v = delVtx v . txMany delSucc uvs . txMany delPred vws $ g+  where+    uvs     = [ (u, v) | u <- getPreds g v ]+    vws     = [ (v, w) | w <- getSuccs g v ]++edgesIkvg :: [CEdge] -> IKVGraph+edgesIkvg = addLinks empty++ikvgEdges :: IKVGraph -> [CEdge]+ikvgEdges g = [ (u, v) | (u, vs) <- M.toList (igSucc g), v <- S.toList vs]++getSuccs :: IKVGraph -> CVertex -> [CVertex]+getSuccs g u = S.toList $ M.lookupDefault S.empty u (igSucc g)++getPreds :: IKVGraph -> CVertex -> [CVertex]+getPreds g v = S.toList $ M.lookupDefault S.empty v (igPred g)++--------------------------------------------------------------------------------+empty :: IKVGraph+empty = IKVGraph M.empty M.empty++txMany :: (a -> b -> b) -> [a] -> b -> b+txMany op es g = L.foldl' (flip op) g es++addSucc :: CEdge -> IKVGraph -> IKVGraph+addSucc (u, v) g = g { igSucc = inserts u v (igSucc g) }++addPred :: CEdge -> IKVGraph -> IKVGraph+addPred (u, v) g = g { igPred = inserts v u (igPred g) }++delSucc :: CEdge -> IKVGraph -> IKVGraph+delSucc (u, v) g = g { igSucc = removes u v (igSucc g)}++delPred :: (CVertex, CVertex) -> IKVGraph -> IKVGraph+delPred (u, v) g = g { igPred = removes v u (igPred g)}++delVtx :: CVertex -> IKVGraph -> IKVGraph+delVtx v g = g { igSucc = M.delete v (igSucc g) }+               { igPred = M.delete v (igPred g) }++inserts :: (Eq k, Eq v, Hashable k, Hashable v)+        => k -> v -> M.HashMap k (S.HashSet v) -> M.HashMap k (S.HashSet v)+inserts k v m = M.insert k (S.insert v $ M.lookupDefault S.empty k m) m++removes :: (Eq k, Eq v, Hashable k, Hashable v)+        => k -> v -> M.HashMap k (S.HashSet v) -> M.HashMap k (S.HashSet v)+removes k v m = M.insert k (S.delete v (M.lookupDefault S.empty k m)) m

@@ -0,0 +1,213 @@+{-# LANGUAGE ConstraintKinds   #-}+{-# LANGUAGE OverloadedStrings #-}++-- | This module implements functions to build constraint / kvar+--   dependency graphs, partition them and print statistics about+--   their structure.++module Language.Fixpoint.Graph.Partition (++  -- * Split constraints+    CPart (..)+  , partition, partition', partitionN++  -- * Information about cores+  , MCInfo (..)+  , mcInfo++  -- * Debug+  , dumpPartitions++  ) where++import           GHC.Conc                  (getNumProcessors)+import           Control.Monad             (forM_)+-- import           GHC.Generics              (Generic)+import           Language.Fixpoint.Misc         -- hiding (group)+import           Language.Fixpoint.Utils.Files+import           Language.Fixpoint.Types.Config+-- import           Language.Fixpoint.Types.PrettyPrint+-- import qualified Language.Fixpoint.Types.Visitor      as V+import qualified Language.Fixpoint.Types              as F+import           Language.Fixpoint.Graph.Types+import           Language.Fixpoint.Graph.Deps++import qualified Data.HashMap.Strict                  as M+-- import qualified Data.Graph                           as G+-- import qualified Data.Tree                            as T+-- import           Data.Function (on)+import           Data.Maybe                     (fromMaybe)+import           Data.Hashable+import           Text.PrettyPrint.HughesPJ+import           Data.List (sortBy)+-- import qualified Data.HashSet              as S++-- import qualified Language.Fixpoint.Solver.Solution    as So+-- import Data.Graph.Inductive++++--------------------------------------------------------------------------------+-- | Constraint Partition Container --------------------------------------------+--------------------------------------------------------------------------------++data CPart a = CPart { pws :: !(M.HashMap F.KVar (F.WfC a))+                     , pcm :: !(M.HashMap Integer (F.SubC a))+                     }++instance Monoid (CPart a) where+   mempty = CPart mempty mempty+   mappend l r = CPart { pws = pws l `mappend` pws r+                       , pcm = pcm l `mappend` pcm r+                       }++--------------------------------------------------------------------------------+-- | Multicore info ------------------------------------------------------------+--------------------------------------------------------------------------------++data MCInfo = MCInfo { mcCores       :: !Int+                     , mcMinPartSize :: !Int+                     , mcMaxPartSize :: !Int+                     } deriving (Show)++mcInfo :: Config -> IO MCInfo+mcInfo c = do+   np <- getNumProcessors+   let nc = fromMaybe np (cores c)+   return MCInfo { mcCores = nc+                 , mcMinPartSize = minPartSize c+                 , mcMaxPartSize = maxPartSize c+                 }++partition :: (F.Fixpoint a) => Config -> F.FInfo a -> IO (F.Result (Integer, a))+partition cfg fi+  = do dumpPartitions cfg fis+       -- writeGraph      f   g+       return mempty+    where+      --f   = queryFile Dot cfg+      fis = partition' Nothing fi++------------------------------------------------------------------------------+-- | Partition an FInfo into multiple disjoint FInfos. Info is Nothing to+--   produce the maximum possible number of partitions. Or a MultiCore Info+--   to control the partitioning+------------------------------------------------------------------------------+partition' :: Maybe MCInfo -> F.FInfo a -> [F.FInfo a]+------------------------------------------------------------------------------+partition' mn fi  = case mn of+   Nothing -> fis mkPartition id+   Just mi -> partitionN mi fi $ fis mkPartition' finfoToCpart+  where+    css            = decompose fi+    fis partF ctor = applyNonNull [ctor fi] (pbc partF) css+    pbc partF      = partitionByConstraints partF fi++-- | Partition an FInfo into a specific number of partitions of roughly equal+-- amounts of work+partitionN :: MCInfo    -- ^ describes thresholds and partiton amounts+           -> F.FInfo a   -- ^ The originial FInfo+           -> [CPart a] -- ^ A list of the smallest possible CParts+           -> [F.FInfo a] -- ^ At most N partitions of at least thresh work+partitionN mi fi cp+   | cpartSize (finfoToCpart fi) <= minThresh = [fi]+   | otherwise = map (cpartToFinfo fi) $ toNParts sortedParts+   where+      toNParts p+         | isDone p = p+         | otherwise = toNParts $ insertSorted firstTwo rest+            where (firstTwo, rest) = unionFirstTwo p+      isDone [] = True+      isDone [_] = True+      isDone fi'@(a:b:_) = length fi' <= prts+                            && (cpartSize a >= minThresh+                                || cpartSize a + cpartSize b >= maxThresh)+      sortedParts = sortBy sortPredicate cp+      unionFirstTwo (a:b:xs) = (a `mappend` b, xs)+      unionFirstTwo _        = errorstar "Partition.partitionN.unionFirstTwo called on bad arguments"+      sortPredicate lhs rhs+         | cpartSize lhs < cpartSize rhs = GT+         | cpartSize lhs > cpartSize rhs = LT+         | otherwise = EQ+      insertSorted a []     = [a]+      insertSorted a (x:xs) = if sortPredicate a x == LT+                              then x : insertSorted a xs+                              else a : x : xs+      prts      = mcCores mi+      minThresh = mcMinPartSize mi+      maxThresh = mcMaxPartSize mi+++-- | Return the "size" of a CPart. Used to determine if it's+-- substantial enough to be worth parallelizing.+cpartSize :: CPart a -> Int+cpartSize c = (M.size . pcm) c + (length . pws) c++-- | Convert a CPart to an FInfo+cpartToFinfo :: F.FInfo a -> CPart a -> F.FInfo a+cpartToFinfo fi p = fi { F.cm = pcm p+                       , F.ws = pws p+                       }++-- | Convert an FInfo to a CPart+finfoToCpart :: F.FInfo a -> CPart a+finfoToCpart fi = CPart { pcm = F.cm fi+                        , pws = F.ws fi+                        }++-------------------------------------------------------------------------------------+dumpPartitions :: (F.Fixpoint a) => Config -> [F.FInfo a] -> IO ()+-------------------------------------------------------------------------------------+dumpPartitions cfg fis =+  forM_ (zip [0..] fis) $ \(i, fi) ->+    writeFile (queryFile (Part i) cfg) (render $ F.toFixpoint cfg fi)+++-- | Type alias for a function to construct a partition. mkPartition and+--   mkPartition' are the two primary functions that conform to this interface+type PartitionCtor a b = F.FInfo a+                       -> M.HashMap Int [(Integer, F.SubC a)]+                       -> M.HashMap Int [(F.KVar, F.WfC a)]+                       -> Int+                       -> b -- ^ typically a F.FInfo a or F.CPart a++partitionByConstraints :: PartitionCtor a b -- ^ mkPartition or mkPartition'+                          -> F.FInfo a+                          -> KVComps+                          -> ListNE b -- ^ [F.FInfo a] or [F.CPart a]+partitionByConstraints f fi kvss = f fi icM iwM <$> js+  where+    js   = fst <$> jkvs                                -- groups+    gc   = groupFun cM                                 -- (i, ci) |-> j+    gk   = groupFun kM                                 -- k       |-> j++    iwM  = groupMap (gk . fst) (M.toList (F.ws fi))    -- j |-> [w]+    icM  = groupMap (gc . fst) (M.toList (F.cm fi))    -- j |-> [(i, ci)]++    jkvs = zip [1..] kvss+    kvI  = [ (x, j) | (j, kvs) <- jkvs, x <- kvs ]+    kM   = M.fromList [ (k, i) | (KVar k, i) <- kvI ]+    cM   = M.fromList [ (c, i) | (Cstr c, i) <- kvI ]++mkPartition :: F.GInfo F.SubC a+            -> M.HashMap Int [(Integer, c a)]+            -> M.HashMap Int [(F.KVar, F.WfC a)]+            -> Int+            -> F.GInfo c a+mkPartition fi icM iwM j+  = fi { F.cm       = M.fromList $ M.lookupDefault [] j icM+       , F.ws       = M.fromList $ M.lookupDefault [] j iwM+       }++mkPartition' :: F.FInfo a1+             -> M.HashMap Int [(Integer, F.SubC a)]+             -> M.HashMap Int [(F.KVar, F.WfC a)]+             -> Int+             -> CPart a+mkPartition' _ icM iwM j+  = CPart { pcm       = M.fromList $ M.lookupDefault [] j icM+          , pws       = M.fromList $ M.lookupDefault [] j iwM+          }++groupFun :: (Show k, Eq k, Hashable k) => M.HashMap k Int -> k -> Int+groupFun m k = safeLookup ("groupFun: " ++ show k) k m

@@ -0,0 +1,62 @@+{-# LANGUAGE ConstraintKinds   #-}+{-# LANGUAGE OverloadedStrings #-}++-- | This module a test for whether the constraint dependencies form a+--   reducible graph.++module Language.Fixpoint.Graph.Reducible ( isReducible ) where++import qualified Data.Tree                            as T+import qualified Data.HashMap.Strict                  as M+import           Data.Graph.Inductive++import           Language.Fixpoint.Misc         -- hiding (group)+import qualified Language.Fixpoint.Types.Visitor      as V+import qualified Language.Fixpoint.Types              as F+++--------------------------------------------------------------------------------+isReducible :: F.SInfo a -> Bool+--------------------------------------------------------------------------------+isReducible fi = all (isReducibleWithStart g) vs+  where+    g  = convertToGraph fi+    vs = {- trace (showDot $ fglToDotGeneric g show (const "") id) -} nodes g++isReducibleWithStart :: Gr a b -> Node -> Bool+isReducibleWithStart g x = all (isBackEdge domList) rEdges+  where+    dfsTree              = head $ dff [x] g --head because only care about nodes reachable from 'start node'?+    rEdges               = [ e | e@(a,b) <- edges g, isDescendant a b dfsTree]+    domList              = dom g x++++convertToGraph :: F.SInfo a -> Gr Int ()+convertToGraph fi = mkGraph vs es+  where+    subCs        = M.elems (F.cm fi)+    es           = lUEdge <$> concatMap (subcEdges' kvI $ F.bs fi) subCs+    ks           = M.keys (F.ws fi)+    kiM          = M.fromList $ zip ks [0..]+    kvI k        = safeLookup ("convertToGraph: " ++ show k) k kiM+    vs           = lNode . kvI <$> M.keys (F.ws fi)+    lNode i      = (i, i)+    lUEdge (i,j) = (i, j, ())++isDescendant :: Node -> Node -> T.Tree Node -> Bool+isDescendant x y (T.Node z f) | z == y    = f `contains` x+                              | z == x    = False+                              | otherwise = any (isDescendant x y) f++contains :: [T.Tree Node] -> Node -> Bool+contains t x = x `elem` concatMap T.flatten t++isBackEdge :: [(Node, [Node])] -> Edge -> Bool+isBackEdge t (u,v) = v `elem` xs+  where+    (Just xs) = lookup u t++subcEdges' :: (F.KVar -> Node) -> F.BindEnv -> F.SimpC a -> [(Node, Node)]+subcEdges' kvI be c = [(kvI k1, kvI k2) | k1 <- V.envKVars be c+                                        , k2 <- V.kvars $ F.crhs c]

@@ -0,0 +1,184 @@++-- | This module contains the types for representing dependency+--   graphs between kvars and constraints.++{-# LANGUAGE ImplicitParams        #-}+{-# LANGUAGE DeriveGeneric     #-}+{-# LANGUAGE OverloadedStrings #-}++module Language.Fixpoint.Graph.Types (++  -- * Graphs+    CVertex (..)+  , CEdge+  , isRealEdge+  , KVGraph (..)++  -- * Components+  , Comps+  , KVComps++  -- * Printing+  , writeGraph+  , writeEdges++  -- * Constraints+  , F.SubcId+  , KVRead+  , DepEdge++  -- * Slice of relevant constraints+  , Slice (..)++  -- * Constraint Dependency Graphs+  , CGraph (..)++  -- * Alias for Constraint Maps+  , F.CMap+  , lookupCMap++  -- * Ranks+  , Rank (..)++  -- * Constraint Dependencies+  , CDeps (..)++  -- * Solver Info+  , SolverInfo (..)+  )+  where++import           GHC.Generics              (Generic)+import           Data.Hashable+import           Text.PrettyPrint.HughesPJ++import           Language.Fixpoint.Misc         -- hiding (group)+import           Language.Fixpoint.Types.PrettyPrint+import           Language.Fixpoint.Types.Refinements -- Constraints+import qualified Language.Fixpoint.Types.Solutions as F+-- import           Language.Fixpoint.Misc (safeLookup)+import qualified Language.Fixpoint.Types   as F+import qualified Data.HashMap.Strict       as M+import qualified Data.HashSet              as S++import GHC.Stack+--------------------------------------------------------------------------------++data CVertex = KVar  !KVar    -- ^ real kvar vertex+             | DKVar !KVar    -- ^ dummy to ensure each kvar has a successor+             | Cstr  !Integer -- ^ constraint-id which creates a dependency+               deriving (Eq, Ord, Show, Generic)++instance PPrint CVertex where+  pprintTidy _ (KVar k)  = doubleQuotes $ pprint $ kv k+  pprintTidy _ (Cstr i)  = text "id_" <> pprint i+  pprintTidy _ (DKVar k) = pprint k   <> text "*"+++instance Hashable CVertex++data KVGraph    = KVGraph { kvgEdges :: [(CVertex, CVertex, [CVertex])] }+type CEdge      = (CVertex, CVertex)+type Comps a    = [[a]]+type KVComps    = Comps CVertex++instance PPrint KVGraph where+  pprintTidy _ = pprint . kvgEdges++--------------------------------------------------------------------------------+writeGraph :: FilePath -> KVGraph -> IO ()+--------------------------------------------------------------------------------+writeGraph f = writeEdges f . graphEdges+  where+    graphEdges :: KVGraph -> [CEdge]+    graphEdges (KVGraph g) = [ (v, v') | (v,_,vs) <- g, v' <- vs]++--------------------------------------------------------------------------------+writeEdges :: FilePath -> [CEdge] -> IO ()+--------------------------------------------------------------------------------+writeEdges f = writeFile f . render . ppEdges++ppEdges :: [CEdge] -> Doc+ppEdges             = vcat . wrap ["digraph Deps {"] ["}"]+                           . map ppE+                           . (if True then filter isRealEdge else txEdges)  -- RJ: use this to collapse "constraint" vertices+  where+    ppE (v, v')     = pprint v <+> "->" <+> pprint v'++isRealEdge :: CEdge -> Bool+isRealEdge (DKVar _, _)     = False+isRealEdge (_, DKVar _)     = False+isRealEdge (Cstr _, Cstr _) = False+isRealEdge _                = True++txEdges    :: [CEdge] -> [CEdge]+txEdges es = concatMap iEs is+  where+    is     = [i | (Cstr i, Cstr _) <- es]+    kvInM  = group [ (i, k) | (KVar k, Cstr i) <- es]+    kvOutM = group [ (i, k') | (Cstr i, KVar k') <- es]+    ins i  = M.lookupDefault [] i kvInM+    outs i = M.lookupDefault [] i kvOutM+    iEs i  = case (ins i, outs i) of+                 (ks, [] ) -> [(KVar k, Cstr i ) | k  <- ks ]+                 ([], ks') -> [(Cstr i, KVar k') | k' <- ks']+                 (ks, ks') -> [(KVar k, KVar k') | k  <- ks, k' <- ks']++++---------------------------------------------------------------------------+-- | Dramatis Personae+---------------------------------------------------------------------------+type KVRead  = M.HashMap F.KVar [F.SubcId]+type DepEdge = (F.SubcId, F.SubcId, [F.SubcId])++data Slice = Slice { slKVarCs :: [F.SubcId]     -- ^ F.SubcIds that transitively "reach" below+                   , slConcCs :: [F.SubcId]     -- ^ F.SubcIds with Concrete RHS+                   , slEdges  :: [DepEdge] -- ^ Dependencies between slKVarCs+                   } deriving (Eq, Show)++data CGraph = CGraph { gEdges :: [DepEdge]+                     , gRanks :: !(F.CMap Int)+                     , gSucc  :: !(F.CMap [F.SubcId])+                     , gSccs  :: !Int+                     }++---------------------------------------------------------------------------+-- | CMap API -------------------------------------------------------------+---------------------------------------------------------------------------+lookupCMap :: (?callStack :: CallStack) => F.CMap a -> F.SubcId -> a+lookupCMap rm i = safeLookup err i rm+  where+    err      = "lookupCMap: cannot find info for " ++ show i++--------------------------------------------------------------------------------+-- | Constraint Dependencies ---------------------------------------------------+--------------------------------------------------------------------------------++data CDeps = CDs { cSucc   :: !(F.CMap [F.SubcId]) -- ^ Constraints *written by* a SubcId+                 , cPrev   :: !(F.CMap [F.KVar])   -- ^ (Cut) KVars *read by*    a SubcId+                 , cRank   :: !(F.CMap Rank)       -- ^ SCC rank of a SubcId+                 , cNumScc :: !Int                 -- ^ Total number of Sccs+                 }+++-- | Ranks ---------------------------------------------------------------------++data Rank = Rank { rScc  :: !Int    -- ^ SCC number with ALL dependencies+                 , rIcc  :: !Int    -- ^ SCC number without CUT dependencies+                 , rTag  :: !F.Tag  -- ^ The constraint's Tag+                 } deriving (Eq, Show)++instance PPrint Rank where+  pprintTidy _ = text . show++--------------------------------------------------------------------------------+-- | `SolverInfo` contains all the stuff needed to produce a result, and is the+--   the essential ingredient of the state needed by solve_+--------------------------------------------------------------------------------+data SolverInfo a b = SI+  { siSol     :: !(F.Sol b F.QBind)             -- ^ the initial solution+  , siQuery   :: !(F.SInfo a)                   -- ^ the whole input query+  , siDeps    :: !CDeps                         -- ^ dependencies between constraints/ranks etc.+  , siVars    :: !(S.HashSet F.KVar)            -- ^ set of KVars to actually solve for+  }

@@ -1,74 +1,132 @@--- | This module implements a "delta-debugging" based query minimizer---   that attempts to shrink UNSAT queries down to a minimal subset---   of constraints.+-- | This module implements a "delta-debugging" based query minimizer.+--   Exported clients of that minimizer include one that attempts to+--   shrink UNSAT queries down to a minimal subset of constraints,+--   one that shrinks SAT queries down to a minimal subset of qualifiers,+--   and one that shrinks SAT queries down to a minimal subset of KVars+--   (replacing all others by True).  {-# LANGUAGE ScopedTypeVariables #-} -module Language.Fixpoint.Minimize ( minQuery ) where+module Language.Fixpoint.Minimize ( minQuery, minQuals, minKvars ) where  import qualified Data.HashMap.Strict                as M import           Control.Monad                      (filterM)-import           Language.Fixpoint.Types.Config     (Config (..))+import           Language.Fixpoint.Types.Visitor    (mapKVars)+import           Language.Fixpoint.Types.Config     (Config (..), queryFile) import           Language.Fixpoint.Types.Errors+import           Language.Fixpoint.Misc             (safeHead) import           Language.Fixpoint.Utils.Files      hiding (Result)-import           Language.Fixpoint.Partition        -- (mcInfo, partition, partition')+import           Language.Fixpoint.Graph import           Language.Fixpoint.Types import           Control.DeepSeq -concatMapM :: (Monad m) => (a -> m [b]) -> [a] -> m [b]-concatMapM f = fmap concat . mapM f- ----------------------------------------------------------------------------minQuery :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a-         -> IO (Result (Integer, a))-----------------------------------------------------------------------------minQuery cfg solve fi = do-  let cfg'     = cfg { minimize = False }-  let (_, fis) = partition' Nothing fi-  failFis     <- filterM (fmap isUnsafe . solve cfg') fis-  failCs      <- concatMapM (getMinFailingCons cfg' solve) failFis-  let minFi    = fi { cm = M.fromList failCs, fileName = minFileName fi }-  saveQuery cfg' minFi-  putStrLn $ "Minimized Constraints: " ++ show (fst <$> failCs)-  return mempty--minFileName :: FInfo a -> FilePath-minFileName = extFileName Min . fileName--isUnsafe :: Result a -> Bool-isUnsafe (Result Safe _)  = False-isUnsafe _                = True--type ConsList a = [(Integer, SubC a)]-type Oracle a c = (Config -> Solver a -> FInfo a -> [c] -> IO Bool)- -- polymorphic delta debugging implementation-deltaDebug :: Oracle a c -> Config -> Solver a -> FInfo a -> [c] -> [c] -> IO [c]-deltaDebug testSet cfg solve finfo set r = do+---------------------------------------------------------------------------+deltaDebug :: Bool -> Oracle a c -> Config -> Solver a -> FInfo a -> [c] -> [c] -> IO [c]+deltaDebug min testSet cfg solve finfo set r = do   let (s1, s2) = splitAt (length set `div` 2) set   if length set == 1-    then return set+    then deltaDebug1 min testSet cfg solve finfo set r     else do       test1 <- testSet cfg solve finfo (s1 ++ r)       if test1-        then deltaDebug testSet cfg solve finfo s1 r+        then deltaDebug min testSet cfg solve finfo s1 r         else do           test2 <- testSet cfg solve finfo (s2 ++ r)           if test2-            then deltaDebug testSet cfg solve finfo s2 r+            then deltaDebug min testSet cfg solve finfo s2 r             else do-              d1 <- deltaDebug testSet cfg solve finfo s1 (s2 ++ r)-              d2 <- deltaDebug testSet cfg solve finfo s2 (s1 ++ r)+              d1 <- deltaDebug min testSet cfg solve finfo s1 (s2 ++ r)+              d2 <- deltaDebug min testSet cfg solve finfo s2 (d1 ++ r)               return (d1 ++ d2) -testConstraints :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a -> ConsList a -> IO Bool-testConstraints cfg solve fi cons  = do-  let fi' = fi { cm = M.fromList cons }-  res <- solve cfg fi'-  return $ isUnsafe res+deltaDebug1 :: Bool -> (a -> b -> c -> d -> IO Bool)+            -> a -> b -> c -> [e] -> d+            -> IO [e]+deltaDebug1 True  _       _   _     _     set _ = return set+deltaDebug1 False testSet cfg solve finfo set r = do+  test <- testSet cfg solve finfo r+  if test then return [] else return set --- run delta debugging on a failing partition to find minimal set of failing constraints-getMinFailingCons :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a -> IO (ConsList a)-getMinFailingCons cfg solve fi = do-  let cons = M.toList $ cm fi-  deltaDebug testConstraints cfg solve fi cons []+type Oracle a c = (Config -> Solver a -> FInfo a -> [c] -> IO Bool)++commonDebug :: (NFData a, Fixpoint a) => (FInfo a -> [c])+                                      -> (FInfo a -> [c] -> FInfo a)+                                      -> (Result (Integer, a) -> Bool)+                                      -> Bool+                                      -> Config+                                      -> Solver a+                                      -> FInfo a+                                      -> Ext+                                      -> (FInfo a -> [c] -> String)+                                      -> IO (Result (Integer, a))+commonDebug init updateFi checkRes min cfg solve fi ext formatter = do+  let cs0 = init fi+  let oracle = mkOracle updateFi checkRes+  cs <- deltaDebug min oracle cfg solve fi cs0 []+  let minFi = updateFi fi cs+  saveQuery (addExt ext cfg) minFi+  putStrLn $ formatter fi cs+  return mempty++---------------------------------------------------------------------------+minQuery :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a+         -> IO (Result (Integer, a))+---------------------------------------------------------------------------+minQuery cfg solve fi = do+  let cfg'  = cfg { minimize = False }+  let fis   = partition' Nothing fi+  failFis  <- filterM (fmap (not . isSafe) . solve cfg') fis+  let failFi = safeHead "--minimize can only be called on UNSAT fq" failFis+  let format _ cs = "Minimized Constraints: " ++ show (fst <$> cs)+  let update fi cs = fi { cm = M.fromList cs }+  commonDebug (M.toList . cm) update (not . isSafe) True cfg' solve failFi Min format++---------------------------------------------------------------------------+minQuals :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a+         -> IO (Result (Integer, a))+---------------------------------------------------------------------------+minQuals cfg solve fi = do+  let cfg'  = cfg { minimizeQs = False }+  let format fi qs = "Required Qualifiers: " ++ show (length qs)+                  ++ "; Total Qualifiers: "  ++ show (length $ quals fi)+  let update fi qs = fi { quals = qs }+  commonDebug quals update isSafe False cfg' solve fi MinQuals format++---------------------------------------------------------------------------+minKvars :: (NFData a, Fixpoint a) => Config -> Solver a -> FInfo a+         -> IO (Result (Integer, a))+---------------------------------------------------------------------------+minKvars cfg solve fi = do+  let cfg'  = cfg { minimizeKs = False }+  let format fi ks = "Required KVars: " ++ show (length ks)+                  ++ "; Total KVars: "  ++ show (length $ ws fi)+  commonDebug (M.keys . ws) removeOtherKs isSafe False cfg' solve fi MinKVars format++removeOtherKs :: FInfo a -> [KVar] -> FInfo a+removeOtherKs fi0 ks = fi1 { ws = ws', cm = cm' }+  where+    fi1 = mapKVars go fi0+    go k | k `elem` ks = Nothing+         | otherwise   = Just PTrue+    ws' = M.filterWithKey (\k _ -> k `elem` ks) $ ws fi1+    cm' = M.filter (isNonTrivial . srhs) $ cm fi1++---------------------------------------------------------------------------+-- Helper functions+---------------------------------------------------------------------------+isSafe :: Result a -> Bool+isSafe (Result Safe _ _) = True+isSafe _                 = False++addExt :: Ext -> Config -> Config+addExt ext cfg = cfg { srcFile = queryFile ext cfg }++mkOracle :: (NFData a, Fixpoint a) => (FInfo a -> [c] -> FInfo a)+                                   -> (Result (Integer, a) -> Bool)+                                   -> Oracle a c+mkOracle updateFi checkRes cfg solve fi qs = do+  let fi' = updateFi fi qs+  res <- solve cfg fi'+  return $ checkRes res

@@ -3,6 +3,8 @@ {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE TupleSections             #-}+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE TypeOperators             #-} {-# LANGUAGE ImplicitParams            #-} -- ignore hlint  module Language.Fixpoint.Misc where@@ -12,13 +14,16 @@ import           Data.Hashable -- import           Data.IORef import           Control.Arrow                    (second)-import           Control.Monad                    (forM_)+import           Control.Monad                    (when, forM_) import qualified Data.HashMap.Strict              as M import qualified Data.List                        as L import           Data.Tuple                       (swap) import           Data.Maybe-import           Data.Array                hiding (indices)+import           Data.Array                       hiding (indices) import           Data.Function                    (on)+import qualified Data.Graph                       as G+import qualified Data.Tree                        as T+import           Data.Unique import           Debug.Trace                      (trace) import           System.Console.ANSI import           System.Console.CmdArgs.Verbosity (whenLoud)@@ -26,9 +31,9 @@ import           System.Directory                 (createDirectoryIfMissing) import           System.FilePath                  (takeDirectory) import           Text.PrettyPrint.HughesPJ        hiding (first)-import           System.IO                       (stdout, hFlush )-import Control.Concurrent.Async-+import           System.IO                        (stdout, hFlush )+import           System.Exit                      (ExitCode)+import           Control.Concurrent.Async  #ifdef MIN_VERSION_located_base import Prelude hiding (error, undefined)@@ -36,6 +41,8 @@ import GHC.Stack #endif +type (|->) a b = M.HashMap a b+ firstMaybe :: (a -> Maybe b) -> [a] -> Maybe b firstMaybe f = listToMaybe . mapMaybe f @@ -50,6 +57,16 @@ hashMapToAscList = L.sortBy (compare `on` fst) . M.toList  ---------------------------------------------------------------+-- | Unique Int -----------------------------------------------+---------------------------------------------------------------++getUniqueInt :: IO Int+getUniqueInt = do+  n1 <- hashUnique <$> newUnique+  n2 <- hashUnique <$> newUnique+  return (n1 * n2)++--------------------------------------------------------------- -- | Edit Distance -------------------------------------------- --------------------------------------------------------------- @@ -75,35 +92,49 @@  data Moods = Ok | Loud | Sad | Happy | Angry +moodColor :: Moods -> Color moodColor Ok    = Black moodColor Loud  = Blue moodColor Sad   = Magenta moodColor Happy = Green moodColor Angry = Red +wrapStars :: String -> String wrapStars msg = "\n**** " ++ msg ++ " " ++ replicate (74 - length msg) '*' +withColor :: Color -> IO () -> IO () -- withColor _ act = act withColor c act    = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c]         act         setSGR [ Reset] +colorStrLn :: Moods -> String -> IO () colorStrLn c       = withColor (moodColor c) . putStrLn++colorPhaseLn :: Moods -> String -> String -> IO () colorPhaseLn c msg = colorStrLn c . wrapStars .  (msg ++)++startPhase :: Moods -> String -> IO () startPhase c msg   = colorPhaseLn c "START: " msg >> colorStrLn Ok " "++doneLine   :: Moods -> String -> IO () doneLine   c msg   = colorPhaseLn c "DONE:  " msg >> colorStrLn Ok " " +donePhase :: Moods -> String -> IO () donePhase c str   = case lines str of       (l:ls) -> doneLine c l >> forM_ ls (colorPhaseLn c "") >> hFlush stdout       _      -> return () +putBlankLn :: IO () putBlankLn = putStrLn "" >> hFlush stdout ------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+wrap :: [a] -> [a] -> [a] -> [a] wrap l r s = l ++ s ++ r +repeats :: Int -> [a] -> [a] repeats n  = concat . replicate n  #ifdef MIN_VERSION_located_base@@ -123,6 +154,9 @@ thd3 ::  (a, b, c) -> c thd3 (_,_,x) = x +secondM :: Functor f => (b -> f c) -> (a, b) -> f (a, c)+secondM act (x, y) = (x,) <$> act y+ #ifdef MIN_VERSION_located_base mlookup    :: (?callStack :: CallStack, Eq k, Show k, Hashable k) => M.HashMap k v -> k -> v safeLookup :: (?callStack :: CallStack, Eq k, Hashable k) => String -> k -> M.HashMap k v -> v@@ -137,33 +171,41 @@   where     err     = errorstar $ "mlookup: unknown key " ++ show k -safeLookup msg k m = fromMaybe (errorstar msg) (M.lookup k m)-+safeLookup msg k m   = fromMaybe (errorstar msg) (M.lookup k m) mfromJust _ (Just x) = x mfromJust s Nothing  = errorstar $ "mfromJust: Nothing " ++ s --- inserts       ::  Hashable k => k -> v -> M.HashMap k [v] -> M.HashMap k [v]+inserts ::  (Eq k, Hashable k) => k -> v -> M.HashMap k [v] -> M.HashMap k [v] inserts k v m = M.insert k (v : M.lookupDefault [] k m) m +removes ::  (Eq k, Hashable k, Eq v) => k -> v -> M.HashMap k [v] -> M.HashMap k [v]+removes k v m = M.insert k (L.delete v (M.lookupDefault [] k m)) m+ count :: (Eq k, Hashable k) => [k] -> [(k, Int)] count = M.toList . fmap sum . group . fmap (, 1) -group         :: (Eq k, Hashable k) => [(k, v)] -> M.HashMap k [v]-group         = groupBase M.empty+group :: (Eq k, Hashable k) => [(k, v)] -> M.HashMap k [v]+group = groupBase M.empty -groupBase     = L.foldl' (\m (k, v) -> inserts k v m)+groupBase :: (Eq k, Hashable k) => M.HashMap k [v] -> [(k, v)] -> M.HashMap k [v]+groupBase = L.foldl' (\m (k, v) -> inserts k v m) -groupList     = M.toList . group+groupList :: (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]+groupList = M.toList . group --- groupMap      :: Hashable k => (a -> k) -> [a] -> M.HashMap k [a]+groupMap   :: (Eq k, Hashable k) => (a -> k) -> [a] -> M.HashMap k [a] groupMap f = L.foldl' (\m x -> inserts (f x) x m) M.empty +allMap :: (Eq k, Hashable k) => (v -> Bool) -> M.HashMap k v -> Bool+allMap p = L.foldl' (\a v -> a && p v) True+ sortNub :: (Ord a) => [a] -> [a] sortNub = nubOrd . L.sort-  where nubOrd (x:t@(y:_))-          | x == y    = nubOrd t-          | otherwise = x : nubOrd t-        nubOrd xs = xs+  where+    nubOrd (x:t@(y:_))+      | x == y    = nubOrd t+      | otherwise = x : nubOrd t+    nubOrd xs     = xs   #ifdef MIN_VERSION_located_base@@ -176,8 +218,9 @@   = zip xs ys   | otherwise   = errorstar $ "safeZip called on non-eq-sized lists (nxs = " ++ show nxs ++ ", nys = " ++ show nys ++ ") : " ++ msg-  where nxs = length xs-        nys = length ys+  where+    nxs = length xs+    nys = length ys  safeZipWith msg f xs ys   | nxs == nys@@ -205,6 +248,7 @@ safeUnsnoc :: String -> ListNE a -> ([a], a) #endif + safeHead _   (x:_) = x safeHead msg _     = errorstar $ "safeHead with empty list " ++ msg @@ -219,32 +263,73 @@  safeUnsnoc msg = swap . second reverse . safeUncons msg . reverse -+executeShellCommand :: String -> String -> IO ExitCode executeShellCommand phase cmd   = do writeLoud $ "EXEC: " ++ cmd        bracket_ (startPhase Loud phase) (donePhase Loud phase) $ system cmd +applyNonNull :: b -> ([a] -> b) -> [a] -> b applyNonNull def _ [] = def applyNonNull _   f xs = f xs -+arrow, dcolon :: Doc arrow              = text "->" dcolon             = colon <> colon++intersperse :: Doc -> [Doc] -> Doc intersperse d ds   = hsep $ punctuate d ds +tshow :: (Show a) => a -> Doc tshow              = text . show --- | if loud, write a string to stdout+-- | If loud, write a string to stdout writeLoud :: String -> IO () writeLoud s = whenLoud $ putStrLn s >> hFlush stdout - ensurePath :: FilePath -> IO () ensurePath = createDirectoryIfMissing True . takeDirectory +singleton :: a -> [a]+singleton x = [x]+ fM :: (Monad m) => (a -> b) -> a -> m b fM f = return . f +whenM :: (Monad m) => m Bool -> m () -> m ()+whenM cond act = do+  b <- cond+  when b act+++mapEither :: (a -> Either b c) -> [a] -> ([b], [c])+mapEither _ []     = ([], [])+mapEither f (x:xs) = case f x of+                       Left y  -> (y:ys, zs)+                       Right z -> (ys, z:zs)+                     where+                       (ys, zs) = mapEither f xs++componentsWith :: (Ord c) => (a -> [(b, c, [c])]) -> a -> [[b]]+componentsWith eF x = map (fst3 . f) <$> vss+  where+    (g,f,_)         = G.graphFromEdges . eF $ x+    vss             = T.flatten <$> G.components g+++type EqHash a = (Eq a, Ord a, Hashable a)++-- >>> coalesce [[1], [2,1], [5], [5, 6], [5, 7], [9, 6], [10], [10,100]]+-- [[1,2],[5,7,6,9],[10,100]]++coalesce :: (EqHash v) => [ListNE v] -> [ListNE v]+coalesce = componentsWith coalesceEdges++coalesceEdges :: (EqHash v) => [ListNE v] -> [(v, v, [v])]+coalesceEdges vss = [ (u, u, vs) | (u, vs) <- groupList (uvs ++ vus) ]+  where+    vus           = swap <$> uvs+    uvs           = [ (u, v) | (u : vs) <- vss, v <- vs ]+ {- exitColorStrLn :: Moods -> String -> IO () exitColorStrLn c s = do@@ -252,3 +337,17 @@   putStrLn "\n"   colorStrLn c s -}++mapFst :: (a -> c) -> (a, b) -> (c, b)+mapFst f (x, y) = (f x, y)++mapSnd :: (b -> c) -> (a, b) -> (a, c)+mapSnd f (x, y) = (x, f y)+++{-@ allCombinations :: xss:[[a]] -> [{v:[a]| len v == len xss}] @-}+allCombinations :: [[a]] -> [[a]]+allCombinations []          = [[]]+allCombinations [[]]        = [[]]+allCombinations ([]:_)     = []+allCombinations ((x:xs):ys) = ((x:) <$> allCombinations ys) ++ allCombinations (xs:ys)

@@ -5,7 +5,6 @@ {-# LANGUAGE TypeSynonymInstances      #-} {-# LANGUAGE UndecidableInstances      #-} {-# LANGUAGE DeriveGeneric             #-}-{-# LANGUAGE PatternGuards             #-} {-# LANGUAGE OverloadedStrings         #-}  module Language.Fixpoint.Parse (@@ -33,6 +32,7 @@   --   fTyConP  -- Type constructors   , lowerIdP    -- Lower-case identifiers   , upperIdP    -- Upper-case identifiers+  , infixIdP    -- String Haskell infix Id   , symbolP     -- Arbitrary Symbols   , constantP   -- (Integer) Constants   , integer     -- Integer@@ -52,7 +52,7 @@   , bvSortP     -- Bit-Vector Sort    -- * Some Combinators-  , condIdP     -- condIdP  :: [Char] -> (Text -> Bool) -> Parser Text+  , condIdP     --  condIdP  :: [Char] -> (Text -> Bool) -> Parser Text    -- * Add a Location to a parsed value   , locParserP@@ -69,15 +69,21 @@    -- * Utilities   , isSmall++  , initPState, PState++  , Fixity(..), Assoc(..), addOperatorP++  -- * For testing+  , expr0P   ) where  import qualified Data.HashMap.Strict         as M import qualified Data.HashSet                as S import qualified Data.Text                   as T-import           Data.Maybe                  (fromJust)-import           Text.Parsec+import           Data.Maybe                  (fromJust, fromMaybe)+import           Text.Parsec       hiding (State) import           Text.Parsec.Expr-import           Text.Parsec.Language        (emptyDef) import qualified Text.Parsec.Token           as Token -- import           Text.Printf                 (printf) import           GHC.Generics                (Generic)@@ -85,22 +91,46 @@ import           Data.Char                   (isLower) import           Language.Fixpoint.Smt.Bitvector import           Language.Fixpoint.Types.Errors-import           Language.Fixpoint.Misc      (tshow, sortNub, thd3)+import           Language.Fixpoint.Misc      (tshow, thd3) import           Language.Fixpoint.Smt.Types---import           Language.Fixpoint.Types.Names     (headSym)-import           Language.Fixpoint.Types.Visitor   (foldSort, mapSort)+-- import           Language.Fixpoint.Types.Names     (headSym)+-- import           Language.Fixpoint.Types.Visitor   (foldSort, mapSort) import           Language.Fixpoint.Types hiding    (mapSort) import           Text.PrettyPrint.HughesPJ         (text, nest, vcat, (<+>))-type Parser = Parsec String Integer +import Control.Monad.State++type Parser = ParsecT String Integer (State PState)+type ParserT u a = ParsecT String u (State PState) a++data PState = PState {fixityTable :: OpTable}++ -------------------------------------------------------------------- ++emptyDef :: Monad m => Token.GenLanguageDef String a m+emptyDef    = Token.LanguageDef+               { Token.commentStart   = ""+               , Token.commentEnd     = ""+               , Token.commentLine    = ""+               , Token.nestedComments = True+               , Token.identStart     = letter <|> char '_'+               , Token.identLetter    = alphaNum <|> oneOf "_"+               , Token.opStart        = Token.opLetter emptyDef+               , Token.opLetter       = oneOf ":!#$%&*+./<=>?@\\^|-~'"+               , Token.reservedOpNames= []+               , Token.reservedNames  = []+               , Token.caseSensitive  = True+               }++languageDef :: Monad m => Token.GenLanguageDef String a m languageDef =   emptyDef { Token.commentStart    = "/* "            , Token.commentEnd      = " */"            , Token.commentLine     = "//"-           , Token.identStart      = satisfy (const False)-           , Token.identLetter     = satisfy (const False)+           -- , Token.identStart      = satisfy (const False)+           -- , Token.identLetter     = satisfy (const False)            , Token.reservedNames   = [ "SAT"                                      , "UNSAT"                                      , "true"@@ -108,19 +138,54 @@                                      , "mod"                                      , "data"                                      , "Bexp"+                                     , "True"+                                     , "Int"+                                     , "import"+                                     , "if", "then", "else"+                                     , "func"++                                     -- reserved words used in liquid haskell                                      , "forall"                                      , "exists"-                                     , "assume"-                                     , "measure"                                      , "module"                                      , "spec"                                      , "where"-                                     , "True"-                                     , "Int"++                                     , "decrease"+                                     , "lazyvar"+                                     , "LIQUID"+                                     , "lazy"+                                     , "local"+                                     , "assert"+                                     , "assume"+                                     , "automatic-instances"+                                     , "autosize"+                                     , "axiomatize"+                                     , "bound"+                                     , "class"+                                     , "data"+                                     , "define"+                                     , "defined"+                                     , "embed"+                                     , "expression"                                      , "import"-                                     , "_|_"-                                     , "|"-                                     , "if", "then", "else"+                                     , "include"+                                     , "infix"+                                     , "infixl"+                                     , "infixr"+                                     , "inline"+                                     , "instance"+                                     , "invariant"+                                     , "measure"+                                     , "newtype"+                                     , "predicate"+                                     , "qualif"+                                     , "reflect"+                                     , "type"+                                     , "using"+                                     , "with"++                                      ]            , Token.reservedOpNames = [ "+", "-", "*", "/", "\\", ":"                                      , "<", ">", "<=", ">=", "=", "!=" , "/="@@ -131,35 +196,59 @@                                      , "->"                                      , ":="                                      , "&", "^", "<<", ">>", "--"-                                     , "?", "Bexp" -- , "'"+                                     , "?", "Bexp"+                                     , "'"+                                     , "_|_"+                                     , "|"+                                     , "<:"+                                     , "|-"+                                     , "::"+                                     , "."                                      ]            } -lexer         = Token.makeTokenParser languageDef+lexer :: Monad m => Token.GenTokenParser String u m+lexer = Token.makeTokenParser languageDef+++reserved :: String -> Parser () reserved      = Token.reserved      lexer++reservedOp :: String -> Parser () reservedOp    = Token.reservedOp    lexer++parens, brackets, angles, braces :: ParserT u a -> ParserT u a parens        = Token.parens        lexer brackets      = Token.brackets      lexer angles        = Token.angles        lexer+braces        = Token.braces        lexer++semi, colon, comma, stringLiteral :: Parser String semi          = Token.semi          lexer colon         = Token.colon         lexer comma         = Token.comma         lexer-whiteSpace    = Token.whiteSpace    lexer stringLiteral = Token.stringLiteral lexer-braces        = Token.braces        lexer++whiteSpace :: Parser ()+whiteSpace    = Token.whiteSpace    lexer++double :: Parser Double double        = Token.float         lexer -- integer       = Token.integer       lexer  -- identifier = Token.identifier lexer -+-- TODO:AZ: pretty sure there is already a whitespace eater in parsec,+blanks :: Parser String blanks  = many (satisfy (`elem` [' ', '\t'])) +-- | Integer+integer :: Parser Integer integer = posInteger  --  try (char '-' >> (negate <$> posInteger)) --       <|> posInteger-+posInteger :: Parser Integer posInteger = toI <$> (many1 digit <* spaces)   where     toI :: String -> Integer@@ -178,6 +267,7 @@  -- FIXME: we (LH) rely on this parser being dumb and *not* consuming trailing -- whitespace, in order to avoid some parsers spanning multiple lines..+ condIdP  :: S.HashSet Char -> (String -> Bool) -> Parser Symbol condIdP chars f   = do c  <- letter <|> char '_'@@ -185,24 +275,43 @@        blanks        if f (c:cs) then return (symbol $ c:cs) else parserZero +-- | Lower-case identifiers upperIdP :: Parser Symbol-upperIdP = condIdP symChars (not . isSmall . head)+upperIdP = do+  c <- upper+  cs <- many (satisfy (`S.member` symChars))+  blanks+  return (symbol $ c:cs) +-- | Lower-case identifiers lowerIdP :: Parser Symbol-lowerIdP = condIdP symChars (isSmall . head)--isSmall :: Char -> Bool-isSmall c = isLower c || c == '_'+lowerIdP = do+  c <- satisfy (\c -> isLower c || c == '_' )+  cs <- many (satisfy (`S.member` symChars))+  blanks+  return (symbol $ c:cs)  symCharsP :: Parser Symbol symCharsP = condIdP symChars (`notElem` keyWordSyms)+  where+    keyWordSyms = ["if", "then", "else", "mod"] +-- | String Haskell infix Id+infixIdP :: Parser String+infixIdP = many (satisfy (`notElem` [' ', '.']))++isSmall :: Char -> Bool+isSmall c = isLower c || c == '_'++locLowerIdP, locUpperIdP :: Parser LocSymbol locLowerIdP = locParserP lowerIdP locUpperIdP = locParserP upperIdP +-- | Arbitrary Symbols symbolP :: Parser Symbol symbolP = symbol <$> symCharsP +-- | (Integer) Constants constantP :: Parser Constant constantP =  try (R <$> double)          <|> I <$> integer@@ -215,16 +324,27 @@   =  (fastIfP EIte exprP)  <|> (ESym <$> symconstP)  <|> (ECon <$> constantP)- <|> (reserved "_|_" >> return EBot)+ <|> (reservedOp "_|_" >> return EBot)  <|> lamP- <|> try (parens  exprP)- <|> try (parens  exprCastP)+  -- TODO:AZ get rid of these try, after the rest+ <|> try (parens exprP)+ <|> try (parens exprCastP)  <|> (charsExpr <$> symCharsP)+  where +exprCastP :: Parser Expr+exprCastP+  = do e  <- exprP+       (try dcolon) <|> colon+       so <- sortP+       return $ ECst e so++charsExpr :: Symbol -> Expr charsExpr cs   | isSmall (headSym cs) = expr cs   | otherwise            = EVar cs +fastIfP :: (Expr -> a -> a -> a) -> Parser a -> Parser a fastIfP f bodyP   = do reserved "if"        p <- predP@@ -245,69 +365,121 @@       return $ f p b1 b2 -} +-- | Used as input to @Text.Parsec.Expr.buildExpressionParser@ to create @exprP@ expr1P :: Parser Expr expr1P   =  try funAppP  <|> expr0P +-- | Expressions exprP :: Parser Expr-exprP = buildExpressionParser bops expr1P+exprP = (fixityTable <$> get) >>= (`buildExpressionParser` expr1P) -funAppP            =  (try litP) <|> (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP <|> simpleAppP+data Fixity+  = FInfix   {fpred :: Maybe Int, fname :: String, fop2 :: Maybe (Expr -> Expr -> Expr), fassoc :: Assoc}+  | FPrefix  {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Expr -> Expr)}+  | FPostfix {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Expr -> Expr)}+++-- Invariant : OpTable has 10 elements+type OpTable = OperatorTable String Integer (State PState) Expr++addOperatorP :: Fixity -> Parser ()+addOperatorP op+  = modify $ \s -> s{fixityTable =  addOperator op (fixityTable s)}++addOperator :: Fixity -> OpTable -> OpTable+addOperator (FInfix p x f assoc) ops+ = insertOperator (makePrec p) (Infix (reservedOp x >> return (makeInfixFun x f)) assoc) ops+addOperator (FPrefix p x f) ops+ = insertOperator (makePrec p) (Prefix (reservedOp x >> return (makePrefixFun x f))) ops+addOperator (FPostfix p x f) ops+ = insertOperator (makePrec p) (Postfix (reservedOp x >> return (makePrefixFun x f))) ops++makePrec :: Maybe Int -> Int+makePrec = fromMaybe 9++makeInfixFun :: String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr+makeInfixFun x = fromMaybe (\e1 e2 -> EApp (EApp (EVar $ symbol x) e1) e2)++makePrefixFun :: String -> Maybe (Expr -> Expr) -> Expr -> Expr+makePrefixFun x = fromMaybe (EApp (EVar $ symbol x))++insertOperator :: Int -> Operator String Integer (State PState) Expr -> OpTable -> OpTable+insertOperator i op ops = go (9 - i) ops   where-    exprFunSpacesP = mkEApp <$> funSymbolP <*> sepBy1 expr0P blanks-    exprFunCommasP = mkEApp <$> funSymbolP <*> parens        (sepBy exprP comma)-    exprFunSemisP  = mkEApp <$> funSymbolP <*> parenBrackets (sepBy exprP semi)-    simpleAppP     = EApp <$> (parens exprP) <*> (parens exprP)+    go _ []       = die $ err dummySpan (text "insertOperator on empty ops")+    go 0 (xs:xss) = (xs++[op]):xss+    go i (xs:xss) = xs:go (i-1) xss++initOpTable :: OpTable+initOpTable = replicate 10 [] --  take 10 (repeat [])++bops :: OpTable+bops = foldl (flip addOperator) initOpTable buildinOps+  where+-- Build in Haskell ops https://www.haskell.org/onlinereport/decls.html#fixity+    buildinOps = [ FPrefix (Just 9) "-"   (Just ENeg)+                 , FInfix  (Just 7) "*"   (Just $ EBin Times) AssocLeft+                 , FInfix  (Just 7) "/"   (Just $ EBin Div)   AssocLeft+                 , FInfix  (Just 6) "-"   (Just $ EBin Minus) AssocLeft+                 , FInfix  (Just 6) "+"   (Just $ EBin Plus)  AssocLeft+                 , FInfix  (Just 5) "mod" (Just $ EBin Mod)   AssocLeft -- Haskell gives mod 7+                 ]++-- | Function Applications+funAppP :: Parser Expr+funAppP            =  litP <|> exprFunP <|> simpleAppP+  where+    exprFunP = mkEApp <$> funSymbolP <*> funRhsP+    funRhsP  =  sepBy1 expr0P blanks+            <|> parens innerP+    innerP =   brackets (sepBy exprP semi)+           <|> sepBy exprP comma++    -- TODO:AZ the parens here should be superfluous, but it hits an infinite loop if removed+    simpleAppP     = EApp <$> parens exprP <*> parens exprP     funSymbolP     = locParserP symbolP  +-- TODO:AZ: The comment says BitVector literal, but it accepts any @Sort@ -- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj))+litP :: Parser Expr litP = do reserved "lit"           l <- stringLiteral           t <- sortP           return $ ECon $ L (T.pack l) t -parenBrackets  = parens . brackets--bops = [ [ Prefix (reservedOp "-"   >> return ENeg)]-       , [ Infix  (reservedOp "*"   >> return (EBin Times)) AssocLeft-         , Infix  (reservedOp "/"   >> return (EBin Div  )) AssocLeft-         ]-       , [ Infix  (reservedOp "-"   >> return (EBin Minus)) AssocLeft-         , Infix  (reservedOp "+"   >> return (EBin Plus )) AssocLeft-         ]-       , [ Infix  (reservedOp "mod"  >> return (EBin Mod  )) AssocLeft]-       ]+-- parenBrackets :: Parser a -> Parser a+-- parenBrackets  = parens . brackets  -- eMinus     = EBin Minus (expr (0 :: Integer)) -- eCons x xs = EApp (dummyLoc consName) [x, xs] -- eNil       = EVar nilName -exprCastP-  = do e  <- exprP-       (try dcolon) <|> colon-       so <- sortP-       return $ ECst e so--+lamP :: Parser Expr lamP-  = do reserved "\\"+  = do reservedOp "\\"        x <- symbolP        colon        t <- sortP-       reserved "->"+       reservedOp "->"        e  <- exprP        return $ ELam (x, t) e -+dcolon :: Parser String dcolon = string "::" <* spaces +varSortP :: Parser Sort varSortP  = FVar  <$> parens intP++funcSortP :: Parser Sort funcSortP = parens $ mkFFunc <$> intP <* comma <*> sortsP +sortsP :: Parser [Sort] sortsP = brackets $ sepBy sortP semi +-- | Sort sortP    :: Parser Sort sortP    = sortP' (sepBy sortArgP blanks) @@ -323,18 +495,19 @@  sortP' :: Parser [Sort] -> Parser Sort sortP' appArgsP-   =  try (parens sortP)-  <|> try (string "func" >> funcSortP)-  <|> try (fAppTC listFTyCon . single <$> brackets sortP)-  <|> try bvSortP-  <|> try (fAppTC <$> fTyConP <*> appArgsP)-  <|> try (fApp   <$> tvarP   <*> appArgsP)+   =  parens sortP+  <|> (reserved "func" >> funcSortP)+  <|> (fAppTC listFTyCon . single <$> brackets sortP)+  <|> bvSortP+  <|> (fAppTC <$> fTyConP <*> appArgsP)+  <|> (fApp   <$> tvarP   <*> appArgsP) +single :: a -> [a] single x = [x]  tvarP :: Parser Sort tvarP-   =  try (string "@" >> varSortP)+   =  (string "@" >> varSortP)   <|> (FObj . symbol <$> lowerIdP)  @@ -343,21 +516,22 @@   =   (reserved "int"     >> return intFTyCon)   <|> (reserved "Integer" >> return intFTyCon)   <|> (reserved "Int"     >> return intFTyCon)-  <|> (reserved "int"     >> return intFTyCon)+  <|> (reserved "int"     >> return intFTyCon) -- TODO:AZ duplicate?   <|> (reserved "real"    >> return realFTyCon)   <|> (reserved "bool"    >> return boolFTyCon)   <|> (reserved "num"     >> return numFTyCon)+  <|> (reserved "Str"     >> return strFTyCon)   <|> (symbolFTycon      <$> locUpperIdP) -bvSortP-  = mkSort <$> (bvSizeP "Size32" S32 <|> bvSizeP "Size64" S64)+-- | Bit-Vector Sort+bvSortP :: Parser Sort+bvSortP = mkSort <$> (bvSizeP "Size32" S32 <|> bvSizeP "Size64" S64)+  where+    bvSizeP ss s = do+      parens (reserved "BitVec" >> reserved ss)+      return s -bvSizeP ss s = do-  parens (reserved "BitVec" >> reserved ss)-  return s -keyWordSyms = ["if", "then", "else", "mod"]- -------------------------------------------------------------------------------- -- | Predicates ---------------------------------------------------------------- --------------------------------------------------------------------------------@@ -365,16 +539,22 @@ pred0P :: Parser Expr pred0P =  trueP       <|> falseP-      <|> try (reserved "??" >> return PGrad)-      <|> try kvarPredP-      <|> try (fastIfP pIte predP)+      <|> (reservedOp "??" >> makeUniquePGrad)+      <|> kvarPredP+      <|> (fastIfP pIte predP)       <|> try predrP-      <|> try (parens predP)-      <|> try (reserved "?" *> exprP)+      <|> (parens predP)+      <|> (reservedOp "?" *> exprP)       <|> try funAppP-      <|> try (reservedOp "&&" >> PAnd <$> predsP)-      <|> try (reservedOp "||" >> POr  <$> predsP)+      <|> (eVar <$> symbolP)+      <|> (reservedOp "&&" >> pGAnds <$> predsP)+      <|> (reservedOp "||" >> POr  <$> predsP) +makeUniquePGrad :: Parser Expr +makeUniquePGrad+  = do uniquePos <- getPosition+       return $ PGrad (KV $ symbol $ show uniquePos) mempty mempty+ -- qmP    = reserved "?" <|> reserved "Bexp"  trueP, falseP :: Parser Expr@@ -390,23 +570,23 @@ substP :: Parser Subst substP = mkSubst <$> many (brackets $ pairP symbolP aP exprP)   where-    aP = reserved ":="--predP  :: Parser Expr-predP  = buildExpressionParser lops pred0P-+    aP = reservedOp ":=" +predsP :: Parser [Expr] predsP = brackets $ sepBy predP semi --lops = [ [Prefix (reservedOp "~"    >> return PNot)]-       , [Prefix (reservedOp "not " >> return PNot)]-       , [Infix  (reservedOp "&&"   >> return (\x y -> PAnd [x,y])) AssocRight]-       , [Infix  (reservedOp "||"   >> return (\x y -> POr  [x,y])) AssocRight]-       , [Infix  (reservedOp "=>"   >> return PImp) AssocRight]-       , [Infix  (reservedOp "==>"  >> return PImp) AssocRight]-       , [Infix  (reservedOp "<=>"  >> return PIff) AssocRight]]+predP  :: Parser Expr+predP  = buildExpressionParser lops pred0P+  where+    lops = [ [Prefix (reservedOp "~"    >> return PNot)]+           , [Prefix (reservedOp "not " >> return PNot)]+           , [Infix  (reservedOp "&&"   >> return (\x y -> pGAnd x y)) AssocRight]+           , [Infix  (reservedOp "||"   >> return (\x y -> POr  [x,y])) AssocRight]+           , [Infix  (reservedOp "=>"   >> return PImp) AssocRight]+           , [Infix  (reservedOp "==>"  >> return PImp) AssocRight]+           , [Infix  (reservedOp "<=>"  >> return PIff) AssocRight]] +predrP :: Parser Expr predrP = do e1    <- exprP             r     <- brelP             e2    <- exprP@@ -424,36 +604,49 @@      <|> (reservedOp ">"  >> return (PAtom Gt))      <|> (reservedOp ">=" >> return (PAtom Ge)) ------------------------------------------------------------------------------------------------------------------------ BareTypes ----------------------------------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | BareTypes -----------------------------------------------------------------+-------------------------------------------------------------------------------- +-- | Refa refaP :: Parser Expr refaP =  try (pAnd <$> brackets (sepBy predP semi))      <|> predP  -+-- | (Sorted) Refinements with configurable sub-parsers refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a refBindP bp rp kindP   = braces $ do       x  <- bp       t  <- kindP-      reserved "|"+      reservedOp "|"       ra <- rp <* spaces       return $ t (Reft (x, ra)) + -- bindP      = symbol    <$> (lowerIdP <* colon)-bindP      = symbolP <* colon+-- | Binder (lowerIdP <* colon)+bindP :: Parser Symbol+bindP = symbolP <* colon++optBindP :: Symbol -> Parser Symbol optBindP x = try bindP <|> return x +-- | (Sorted) Refinements+refP :: Parser (Reft -> a) -> Parser a refP       = refBindP bindP refaP++-- | (Sorted) Refinements with default binder+refDefP :: Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a refDefP x  = refBindP (optBindP x)  --------------------------------------------------------------------- -- | Parsing Qualifiers --------------------------------------------- --------------------------------------------------------------------- +-- | Qualifiers+qualifierP :: Parser Sort -> Parser Qualifier qualifierP tP = do   pos    <- getPosition   n      <- upperIdP@@ -461,62 +654,43 @@   _      <- colon   body   <- predP   return  $ mkQual n params body pos--sortBindP = pairP symbolP colon+  where+    sortBindP = pairP symbolP colon  pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b) pairP xP sepP yP = (,) <$> xP <* sepP <*> yP -mkQual :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier-mkQual n xts p = Q n ((v, t) : yts) (subst su p)-  where-    (v, t):zts = gSorts xts-    -- yts        = first mkParam <$> zts-    yts        = zts-    su         = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts- -- mkParam :: Symbol -> Symbol -- mkParam s       = unsafeTextSymbol ('~' `T.cons` toUpper c `T.cons` cs) --  where --    Just (c,cs) = T.uncons $ symbolSafeText s -gSorts :: [(a, Sort)] -> [(a, Sort)]-gSorts xts     = [(x, substVars su t) | (x, t) <- xts]-  where-    su         = (`zip` [0..]) . sortNub . concatMap (sortVars . snd) $ xts -substVars :: [(Symbol, Int)] -> Sort -> Sort-substVars su = mapSort tx-  where-    tx (FObj x)-      | Just i <- lookup x su = FVar i-    tx t                      = t--sortVars :: Sort -> [Symbol]-sortVars = foldSort go []-  where-    go b (FObj x) = x : b-    go b _        = b-- --------------------------------------------------------------------- -- | Parsing Constraints (.fq files) -------------------------------- ---------------------------------------------------------------------  -- Entities in Query File data Def a-  = Srt Sort-  | Axm Expr-  | Cst (SubC a)-  | Wfc (WfC a)-  | Con Symbol Sort-  | Qul Qualifier-  | Kut KVar-  | IBind Int Symbol SortedReft+  = Srt !Sort+  | Axm !Expr+  | Cst !(SubC a)+  | Wfc !(WfC a)+  | Con !Symbol !Sort+  | Dis !Symbol !Sort+  | Qul !Qualifier+  | Kut !KVar+  | Pack !KVar !Int+  | IBind !Int !Symbol !SortedReft+  | Opt !String   deriving (Show, Generic)   --  Sol of solbind   --  Dep of FixConstraint.dep +fInfoOptP :: Parser (FInfoWithOpts ())+fInfoOptP = do ps <- many defP+               return $ FIO (defsFInfo ps) [s | Opt s <- ps]+ fInfoP :: Parser (FInfo ()) fInfoP = defsFInfo <$> {-# SCC "many-defP" #-} many defP @@ -526,9 +700,12 @@     <|> Cst   <$> (reserved "constraint" >> colon >> {-# SCC "subCP" #-} subCP)     <|> Wfc   <$> (reserved "wf"         >> colon >> {-# SCC "wfCP"  #-} wfCP)     <|> Con   <$> (reserved "constant"   >> symbolP) <*> (colon >> sortP)+    <|> Dis   <$> (reserved "distinct"   >> symbolP) <*> (colon >> sortP)+    <|> Pack  <$> (reserved "pack"       >> kvarP)   <*> (colon >> intP)     <|> Qul   <$> (reserved "qualif"     >> qualifierP sortP)     <|> Kut   <$> (reserved "cut"        >> kvarP)     <|> IBind <$> (reserved "bind"       >> intP) <*> symbolP <*> (colon >> {-# SCC "sortedReftP" #-} sortedReftP)+    <|> Opt   <$> (reserved "fixpoint"   >> stringLiteral)  sortedReftP :: Parser SortedReft sortedReftP = refP (RR <$> (sortP <* spaces))@@ -555,6 +732,14 @@            pos' <- getPosition            return $ subC' env lhs rhs i tag pos pos' +subC' :: IBindEnv+      -> SortedReft+      -> SortedReft+      -> Integer+      -> Tag+      -> SourcePos+      -> SourcePos+      -> SubC () subC' env lhs rhs i tag l l'   = case cs of       [c] -> c@@ -575,15 +760,17 @@ intP = fromInteger <$> integer  defsFInfo :: [Def a] -> FInfo a-defsFInfo defs = {-# SCC "defsFI" #-} FI cm ws bs lts kts qs mempty mempty False +defsFInfo defs = {-# SCC "defsFI" #-} FI cm ws bs lts dts kts qs mempty mempty mempty mempty   where-    cm     = M.fromList       [(cid c, c)       | Cst c       <- defs]-    ws     = M.fromList       [(thd3 $ wrft w, w) | Wfc w     <- defs]-    bs     = bindEnvFromList  [(n, x, r)        | IBind n x r <- defs]-    lts    = fromListSEnv     [(x, t)           | Con x t     <- defs]-    kts    = KS $ S.fromList  [k                | Kut k       <- defs]-    qs     =                  [q                | Qul q       <- defs]-    cid    = fromJust . sid+    cm         = M.fromList         [(cid c, c)         | Cst c       <- defs]+    ws         = M.fromList         [(thd3 $ wrft w, w) | Wfc w       <- defs]+    bs         = bindEnvFromList    [(n, x, r)          | IBind n x r <- defs]+    lts        = fromListSEnv       [(x, t)             | Con x t     <- defs]+    dts        = fromListSEnv       [(x, t)             | Dis x t     <- defs]+    kts        = KS $ S.fromList    [k                  | Kut k       <- defs]+    -- pks        = Packs $ M.fromList [(k, i)             | Pack k i    <- defs]+    qs         =                    [q                  | Qul q       <- defs]+    cid        = fromJust . sid     -- msg    = show $ "#Lits = " ++ (show $ length consts)  ---------------------------------------------------------------------@@ -596,44 +783,49 @@  <|> (reserved "UNSAT" >> Unsafe <$> brackets (sepBy pp comma))  <|> (reserved "CRASH" >> crashP pp) -crashP pp-  = do i   <- pp-       msg <- many anyChar-       return $ Crash [i] msg--predSolP-  = parens (predP  <* (comma >> iQualP))+crashP :: Parser a -> Parser (FixResult a)+crashP pp = do+  i   <- pp+  msg <- many anyChar+  return $ Crash [i] msg +predSolP :: Parser Expr+predSolP = parens (predP  <* (comma >> iQualP)) -iQualP-  = upperIdP >> parens (sepBy symbolP comma)+iQualP :: Parser [Symbol]+iQualP = upperIdP >> parens (sepBy symbolP comma) -solution1P-  = do reserved "solution:"-       k  <- kvP-       reserved ":="-       ps <- brackets $ sepBy predSolP semi-       return (k, simplify $ PAnd ps)-    where-      kvP = try kvarP <|> (KV <$> symbolP)+solution1P :: Parser (KVar, Expr)+solution1P = do+  reserved "solution:"+  k  <- kvP+  reservedOp ":="+  ps <- brackets $ sepBy predSolP semi+  return (k, simplify $ PAnd ps)+  where+    kvP = try kvarP <|> (KV <$> symbolP)  solutionP :: Parser (M.HashMap KVar Expr)-solutionP-  = M.fromList <$> sepBy solution1P whiteSpace--solutionFileP-  = (,) <$> fixResultP integer <*> solutionP+solutionP = M.fromList <$> sepBy solution1P whiteSpace -------------------------------------------------------------------------+solutionFileP :: Parser (FixResult Integer, M.HashMap KVar Expr)+solutionFileP = (,) <$> fixResultP integer <*> solutionP +--------------------------------------------------------------------------------+remainderP :: Parser a -> Parser (a, String, SourcePos) remainderP p   = do res <- p        str <- getInput        pos <- getPosition        return (res, str, pos) ++initPState :: PState+initPState = PState {fixityTable = bops}++doParse' :: Parser a -> SourceName -> String -> a doParse' parser f s-  = case runParser (remainderP (whiteSpace >> parser)) 0 f s of+  = case evalState (runParserT (remainderP (whiteSpace >> parser)) 0 f s) initPState of       Left e            -> die $ err (errorSpan e) (dErr e)       Right (r, "", _)  -> r       Right (_, r, l)   -> die $ err (SS l l) (dRem r)@@ -644,6 +836,8 @@                     , nest 4 (text r)                     , "when parsing from" <+> text f ] ++errorSpan :: ParseError -> SrcSpan errorSpan e = SS l l where l = errorPos e  parseFromFile :: Parser b -> SourceName -> IO b@@ -657,9 +851,10 @@ --------------------------------------------------------------------- -- Standalone SMTLIB2 commands -------------------------------------- ----------------------------------------------------------------------+commandsP :: Parser [Command] commandsP = sepBy commandP semi +commandP :: Parser Command commandP   =  (reserved "var"      >> cmdVarP)  <|> (reserved "push"     >> return Push)@@ -668,11 +863,11 @@  <|> (reserved "assert"   >> (Assert Nothing <$> predP))  <|> (reserved "distinct" >> (Distinct <$> brackets (sepBy exprP comma))) -cmdVarP-  = do x <- bindP-       t <- sortP-       return $ Declare x [] t-+cmdVarP :: Parser Command+cmdVarP = do+  x <- bindP+  t <- sortP+  return $ Declare x [] t  --------------------------------------------------------------------- -- Bundling Parsers into a Typeclass --------------------------------@@ -701,6 +896,9 @@  instance Inputable (FInfo ()) where   rr' = {-# SCC "fInfoP" #-} doParse' fInfoP++instance Inputable (FInfoWithOpts ()) where+  rr' = {-# SCC "fInfoWithOptsP" #-} doParse' fInfoOptP  instance Inputable Command where   rr' = doParse' commandP

@@ -1,463 +0,0 @@-{-# LANGUAGE ConstraintKinds   #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE RecordWildCards #-}---- | This module implements functions to build constraint / kvar---   dependency graphs, partition them and print statistics about---   their structure.--module Language.Fixpoint.Partition (--  -- * Split constraints-    CPart (..)-  , partition, partition', partitionN--  -- * Information about cores-  , MCInfo (..)-  , mcInfo--  -- * Queries over dependencies-  , graphStatistics-  , GDeps (..)-  , deps-  -- , isReducible--  -- * Debug-  , elimSolGraph-  ) where--import           GHC.Conc                  (getNumProcessors)-import           Control.Monad             (when, forM_)--- import           GHC.Generics              (Generic)-import           Language.Fixpoint.Misc         -- hiding (group)-import           Language.Fixpoint.Utils.Files-import           Language.Fixpoint.Types.Config-import           Language.Fixpoint.Types.PrettyPrint-import qualified Language.Fixpoint.Types.Visitor      as V-import qualified Language.Fixpoint.Solver.Solution    as So-import qualified Language.Fixpoint.Types              as F-import           Language.Fixpoint.Types.Graphs-import qualified Data.HashMap.Strict                  as M-import qualified Data.Graph                           as G-import qualified Data.Tree                            as T-import           Data.Function (on)-import           Data.Maybe                     (mapMaybe, fromMaybe)-import           Data.Hashable-import           Text.PrettyPrint.HughesPJ-import           Data.List (sortBy)-import qualified Data.HashSet              as S--import Data.Graph.Inductive--------------------------------------------------------------------------------------- | Constraint Partition Container -------------------------------------------------------------------------------------------------------------------------------data CPart a = CPart { pws :: M.HashMap F.KVar (F.WfC a)-                     , pcm :: M.HashMap Integer (F.SubC a)-                     , cFileName :: FilePath-                     }--instance Monoid (CPart a) where-   mempty = CPart mempty mempty mempty-   mappend l r = CPart { pws = pws l `mappend` pws r-                       , pcm = pcm l `mappend` pcm r-                       , cFileName = cFileName l-                       }------------------------------------------------------------------------------------- | Multicore info -----------------------------------------------------------------------------------------------------------------------------------------------data MCInfo = MCInfo { mcCores :: Int-                     , mcMinPartSize :: Int-                     , mcMaxPartSize :: Int-                     } deriving (Show)--mcInfo :: Config -> IO MCInfo-mcInfo c = do-   np <- getNumProcessors-   let nc = fromMaybe np (cores c)-   return MCInfo { mcCores = nc-                 , mcMinPartSize = minPartSize c-                 , mcMaxPartSize = maxPartSize c-                 }--partition :: (F.Fixpoint a) => Config -> F.FInfo a -> IO (F.Result (Integer, a))-partition cfg fi-  = do dumpPartitions cfg fis-       writeGraph      f   g-       return mempty-    where-      f        = queryFile Dot cfg-      (g, fis) = partition' Nothing fi----------------------------------------------------------------------------------- | Partition an FInfo into multiple disjoint FInfos--------------------------------------------------------------------------------partition' :: Maybe MCInfo -- ^ Nothing to produce the maximum possible-                             -- number of partitions. Or a MultiCore Info-                             -- to control the partitioning-           -> F.FInfo a -> (KVGraph, [F.FInfo a])--------------------------------------------------------------------------------partition' mn fi  = case mn of-   Nothing -> (g, fis mkPartition id)-   Just mi -> (g, partitionN mi fi $ fis mkPartition' finfoToCpart)-  where-    g              = kvGraph   fi-    css            = decompose g-    fis partF ctor = applyNonNull [ctor fi] (pbc partF) css-    pbc partF      = partitionByConstraints partF fi----- | Partition an FInfo into a specific number of partitions of roughly equal--- amounts of work-partitionN :: MCInfo    -- ^ describes thresholds and partiton amounts-           -> F.FInfo a   -- ^ The originial FInfo-           -> [CPart a] -- ^ A list of the smallest possible CParts-           -> [F.FInfo a] -- ^ At most N partitions of at least thresh work-partitionN mi fi cp-   | cpartSize (finfoToCpart fi) <= minThresh = [fi]-   | otherwise = map (cpartToFinfo fi) $ toNParts sortedParts-   where-      toNParts p-         | isDone p = p-         | otherwise = toNParts $ insertSorted firstTwo rest-            where (firstTwo, rest) = unionFirstTwo p-      isDone [] = True-      isDone [_] = True-      isDone fi'@(a:b:_) = length fi' <= prts-                            && (cpartSize a >= minThresh-                                || cpartSize a + cpartSize b >= maxThresh)-      sortedParts = sortBy sortPredicate cp-      unionFirstTwo (a:b:xs) = (a `mappend` b, xs)-      unionFirstTwo _        = errorstar "Partition.partitionN.unionFirstTwo called on bad arguments"-      sortPredicate lhs rhs-         | cpartSize lhs < cpartSize rhs = GT-         | cpartSize lhs > cpartSize rhs = LT-         | otherwise = EQ-      insertSorted a []     = [a]-      insertSorted a (x:xs) = if sortPredicate a x == LT-                              then x : insertSorted a xs-                              else a : x : xs-      prts      = mcCores mi-      minThresh = mcMinPartSize mi-      maxThresh = mcMaxPartSize mi----- | Return the "size" of a CPart. Used to determine if it's--- substantial enough to be worth parallelizing.-cpartSize :: CPart a -> Int-cpartSize c = (M.size . pcm) c + (length . pws) c---- | Convert a CPart to an FInfo-cpartToFinfo :: F.FInfo a -> CPart a -> F.FInfo a-cpartToFinfo fi p = fi { F.cm = pcm p-                       , F.ws = pws p-                       , F.fileName = cFileName p-                       }---- | Convert an FInfo to a CPart-finfoToCpart :: F.FInfo a -> CPart a-finfoToCpart fi = CPart { pcm = F.cm fi-                        , pws = F.ws fi-                        , cFileName = F.fileName fi-                        }----------------------------------------------------------------------------------------dumpPartitions :: (F.Fixpoint a) => Config -> [F.FInfo a] -> IO ()---------------------------------------------------------------------------------------dumpPartitions cfg fis =-  forM_ (zip [0..] fis) $ \(i, fi) ->-    writeFile (partFile fi i) (render $ F.toFixpoint cfg fi)--partFile :: F.FInfo a -> Int -> FilePath-partFile fi j = extFileName (Part j) (F.fileName fi)----- | Type alias for a function to construct a partition. mkPartition and--- mkPartition' are the two primary functions that conform to this interface-type PartitionCtor a b = F.FInfo a-                         -> M.HashMap Int [(Integer, F.SubC a)]-                         -> M.HashMap Int [(F.KVar, F.WfC a)]-                         -> Int-                         -> b -- ^ typically a F.FInfo a or F.CPart a--partitionByConstraints :: PartitionCtor a b -- ^ mkPartition or mkPartition'-                          -> F.FInfo a-                          -> KVComps-                          -> ListNE b -- ^ [F.FInfo a] or [F.CPart a]-partitionByConstraints f fi kvss = f fi icM iwM <$> js-  where-    js   = fst <$> jkvs                                -- groups-    gc   = groupFun cM                                 -- (i, ci) |-> j-    gk   = groupFun kM                                 -- k       |-> j--    iwM  = groupMap (gk . fst) (M.toList (F.ws fi))             -- j |-> [w]-    icM  = groupMap (gc . fst) (M.toList (F.cm fi))  -- j |-> [(i, ci)]--    jkvs = zip [1..] kvss-    kvI  = [ (x, j) | (j, kvs) <- jkvs, x <- kvs ]-    kM   = M.fromList [ (k, i) | (KVar k, i) <- kvI ]-    cM   = M.fromList [ (c, i) | (Cstr c, i) <- kvI ]--mkPartition fi icM iwM j-  = fi { F.cm       = M.fromList $ M.lookupDefault [] j icM-       , F.ws       = M.fromList $ M.lookupDefault [] j iwM-       , F.fileName = partFile fi j-       }--mkPartition' fi icM iwM j-  = CPart { pcm       = M.fromList $ M.lookupDefault [] j icM-          , pws       = M.fromList $ M.lookupDefault [] j iwM-          , cFileName = partFile fi j-          }--groupFun :: (Show k, Eq k, Hashable k) => M.HashMap k Int -> k -> Int-groupFun m k = safeLookup ("groupFun: " ++ show k) k m-----------------------------------------------------------------------------------decompose :: KVGraph -> KVComps---------------------------------------------------------------------------------decompose kg = map (fst3 . f) <$> vss-  where-    (g,f,_)  = G.graphFromEdges kg-    vss      = T.flatten <$> G.components g----------------------------------------------------------------------------------kvGraph :: (F.TaggedC c a) => F.GInfo c a -> KVGraph---------------------------------------------------------------------------------kvGraph = edgeGraph . kvEdges--edgeGraph :: [CEdge] -> KVGraph-edgeGraph es = [(v,v,vs) | (v, vs) <- groupList es ]--kvEdges :: (F.TaggedC c a) => F.GInfo c a -> [CEdge]-kvEdges fi = selfes ++ concatMap (subcEdges bs) cs-  where-    bs     = F.bs fi-    cs     = M.elems (F.cm fi)-    ks     = fiKVars fi-    selfes =  [(Cstr i, Cstr i)   | c <- cs, let i = F.subcId c]-           ++ [(KVar k, DKVar k)  | k <- ks]-           ++ [(DKVar k, DKVar k) | k <- ks]---fiKVars :: F.GInfo c a -> [F.KVar]-fiKVars = M.keys . F.ws--subcEdges :: (F.TaggedC c a) => F.BindEnv -> c a -> [CEdge]-subcEdges bs c =  [(KVar k, Cstr i ) | k  <- V.envKVars bs c]-               ++ [(Cstr i, KVar k') | k' <- V.rhsKVars c ]-  where-    i          = F.subcId c------------------------------------------------------------------------------------- | Generic Dependencies ----------------------------------------------------------------------------------------------------------------------------------------data GDeps a-  = Deps { depCuts    :: !(S.HashSet a)-         , depNonCuts :: !(S.HashSet a)-         }-    deriving (Show)--instance (Eq a, Hashable a) => Monoid (GDeps a) where-  mempty                            = Deps S.empty S.empty-  mappend (Deps d1 n1) (Deps d2 n2) = Deps (S.union d1 d2) (S.union n1 n2)--dCut, dNonCut :: (Hashable a) => a -> GDeps a-dNonCut v = Deps S.empty (S.singleton v)-dCut    v = Deps (S.singleton v) S.empty------------------------------------------------------------------------------------- | Compute Dependencies and Cuts -------------------------------------------------------------------------------------------------------------------------------deps :: (F.TaggedC c a) => F.GInfo c a -> GDeps F.KVar----------------------------------------------------------------------------------deps si         = Deps (takeK cs) (takeK ns)-  where-    Deps cs ns  = gDeps cutF (edgeGraph es)-    es          = kvEdges si-    -- ORIG cutF = chooseCut isK (cuts si)-    cutF        = edgeRankCut (edgeRank es)-    takeK       = sMapMaybe tx-    tx (KVar z) = Just z-    tx _        = Nothing---- crash _ = undefined--- cutter :: F.TaggedC c a => F.GInfo c a -> Cutter CVertex--- cutter si = chooseCut isK (cuts si)---- ORIG isK :: CVertex -> Bool--- ORIG isK (KVar _) = True--- ORIG isK _        = False--- ORIG cuts :: (F.TaggedC c a) => F.GInfo c a -> S.HashSet CVertex--- ORIG cuts = S.map KVar . F.ksVars . F.kuts---sMapMaybe :: (Hashable b, Eq b) => (a -> Maybe b) -> S.HashSet a -> S.HashSet b-sMapMaybe f = S.fromList . mapMaybe f . S.toList-----------------------------------------------------------------------------------type EdgeRank = M.HashMap F.KVar Integer----------------------------------------------------------------------------------edgeRank :: [CEdge] -> EdgeRank-edgeRank es = minimum . (n :) <$> kiM-  where-    n       = 1 + maximum [ i | (Cstr i, _)     <- es ]-    kiM     = group [ (k, i) | (KVar k, Cstr i) <- es ]--edgeRankCut :: EdgeRank -> Cutter CVertex-edgeRankCut km vs = case ks of-                      [] -> Nothing-                      k:_ -> Just (KVar k, [x | x@(u,_,_) <- vs, u /= KVar k])-  where-    ks            = orderBy [k | (KVar k, _ ,_) <- vs]-    rank          = (km M.!)-    orderBy       = sortBy (compare `on` rank)-----------------------------------------------------------------------------------type Cutter a = [(a, a, [a])] -> Maybe (a, [(a, a, [a])])------------------------------------------------------------------------------------ ORIG chooseCut :: (Cutable a) => (a -> Bool) -> S.HashSet a -> Cutter a--- ORIG ----------------------------------------------------------------------------------- ORIG chooseCut f ks vs = case vs'' of-                      -- ORIG []  -> Nothing-                      -- ORIG v:_ -> Just (v, [x | x@(u,_,_) <- vs, u /= v])-  -- ORIG where-    -- ORIG vs'           = [x | (x,_,_) <- vs, f x]-    -- ORIG is            = S.intersection (S.fromList vs') ks-    -- ORIG vs''          = if S.null is then vs' else S.toList is-       -- ORIG -- ^ -- we select a RANDOM element,-       -- ORIG ------- instead pick the "first" element.-------------------------------------------------------------------------------------type Cutable a = (Eq a, Ord a, Hashable a, Show a)----------------------------------------------------------------------------------gDeps :: (Cutable a) => Cutter a -> [(a, a, [a])] -> GDeps a----------------------------------------------------------------------------------gDeps f g = sccsToDeps f (G.stronglyConnCompR g)---sccsToDeps :: (Cutable a) => Cutter a -> [G.SCC (a, a, [a])] -> GDeps a-sccsToDeps f xs = mconcat $ sccDep f <$> xs--sccDep :: (Cutable a) =>  Cutter a -> G.SCC (a, a, [a]) -> GDeps a-sccDep _ (G.AcyclicSCC (v,_,_)) = dNonCut v-sccDep f (G.CyclicSCC vs)      = cycleDep f vs---cycleDep :: (Cutable a) => Cutter a -> [(a,a,[a])] -> GDeps a-cycleDep _ [] = mempty-cycleDep f vs = addCut f (f vs)--addCut _ Nothing         = mempty-addCut f (Just (v, vs')) = mconcat $ dCut v : (sccDep f <$> sccs)-  where-    sccs                 = G.stronglyConnCompR vs'-----------------------------------------------------------------------------------isReducible :: F.SInfo a -> Bool----------------------------------------------------------------------------------isReducible fi = all (isReducibleWithStart g) vs-  where-    g  = convertToGraph fi-    vs = {- trace (showDot $ fglToDotGeneric g show (const "") id) -} nodes g--isReducibleWithStart :: Gr a b -> Node -> Bool-isReducibleWithStart g x = all (isBackEdge domList) rEdges-  where-    dfsTree = head $ dff [x] g --head because only care about nodes reachable from 'start node'?-    rEdges = [e | e@(a,b) <- edges g, isDescendant a b dfsTree]-    domList = dom g x--convertToGraph :: F.SInfo a -> Gr Int ()-convertToGraph fi = mkGraph vs es-  where-    subCs        = M.elems (F.cm fi)-    es           = lUEdge <$> concatMap (subcEdges' kvI $ F.bs fi) subCs-    ks           = M.keys (F.ws fi)-    kiM          = M.fromList $ zip ks [0..]-    kvI k        = safeLookup ("convertToGraph: " ++ show k) k kiM-    vs           = lNode . kvI <$> M.keys (F.ws fi)-    lNode i      = (i, i)-    lUEdge (i,j) = (i, j, ())--isDescendant :: Node -> Node -> T.Tree Node -> Bool-isDescendant x y (T.Node z f) | z == y    = f `contains` x-                              | z == x    = False-                              | otherwise = any (isDescendant x y) f--contains :: [T.Tree Node] -> Node -> Bool-contains t x = x `elem` concatMap T.flatten t--isBackEdge :: [(Node, [Node])] -> Edge -> Bool-isBackEdge t (u,v) = v `elem` xs-  where-    (Just xs) = lookup u t--subcEdges' :: (F.KVar -> Node) -> F.BindEnv -> F.SimpC a -> [(Node, Node)]-subcEdges' kvI be c = [(kvI k1, kvI k2) | k1 <- V.envKVars be c-                                        , k2 <- V.kvars $ F.crhs c]-----------------------------------------------------------------------------------graphStatistics :: Config -> F.SInfo a -> IO ()----------------------------------------------------------------------------------graphStatistics cfg si = when (elimStats cfg) $ do-  writeGraph f  (kvGraph si)-  appendFile f . ppc . ptable $ graphStats si-  where-    f     = queryFile Dot cfg-    ppc d = showpp $ vcat [" ", " ", "/*", pprint d, "*/"]--data Stats = Stats {-    stNumKVCuts   :: !Int   -- ^ number of kvars whose removal makes deps acyclic-  , stNumKVNonLin :: !Int   -- ^ number of kvars that appear >= 2 in some LHS-  , stNumKVTotal  :: !Int   -- ^ number of kvars-  , stIsReducible :: !Bool  -- ^ is dep-graph reducible-  , stSetKVNonLin :: S.HashSet F.KVar -- ^ set of non-linear kvars-  }--instance PTable Stats where-  ptable (Stats {..})  = DocTable [-      ("# KVars [Cut]"    , pprint stNumKVCuts)-    , ("# KVars [NonLin]" , pprint stNumKVNonLin)-    , ("# KVars [All]"    , pprint stNumKVTotal)-    , ("# Reducible"      , pprint stIsReducible)-    , ("KVars NonLin"     , pprint stSetKVNonLin)-    ]--graphStats :: F.SInfo a -> Stats-graphStats si     = Stats {-    stNumKVCuts   = S.size (depCuts d)-  , stNumKVNonLin = S.size  nlks-  , stNumKVTotal  = S.size (depCuts d) + S.size (depNonCuts d)-  , stIsReducible = isReducible si-  , stSetKVNonLin = nlks-  }-  where-    nlks          = nlKVars si-    d             = deps si--nlKVars :: (F.TaggedC c a) => F.GInfo c a -> S.HashSet F.KVar-nlKVars fi = S.unions $ nlKVarsC bs <$> cs-  where-    bs     = F.bs fi-    cs     = M.elems (F.cm fi)--nlKVarsC :: (F.TaggedC c a) => F.BindEnv -> c a -> S.HashSet F.KVar-nlKVarsC bs c = S.fromList [ k |  (k, n) <- V.envKVarsN bs c, n >= 2]------------------------------------------------------------------------------------- | Build and print the graph of post eliminate solution, which has an edge---   from k -> k' if k' appears directly inside the "solution" for k----------------------------------------------------------------------------------elimSolGraph :: Config -> F.Solution -> IO ()-elimSolGraph cfg s = writeGraph f (So.solutionGraph s)-  where-    f              = queryFile Dot cfg

@@ -29,7 +29,7 @@ import           Language.Fixpoint.Types.Names import           Language.Fixpoint.Types -data Bv     = Bv BvSize String+data Bv     = Bv !BvSize !String  data BvSize = S32   | S64               deriving (Eq, Ord, Show, Data, Typeable, Generic)

@@ -4,6 +4,7 @@ {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE RecordWildCards           #-} {-# LANGUAGE UndecidableInstances      #-}+{-# LANGUAGE ScopedTypeVariables       #-}  -- | This module contains an SMTLIB2 interface for --   1. checking the validity, and,@@ -37,50 +38,61 @@      -- * Query API     , smtDecl+    , smtDecls     , smtAssert+    , smtAssertAxiom     , smtCheckUnsat     , smtCheckSat     , smtBracket     , smtDistinct--    -- * Theory Symbols-    -- , theorySymbols-      -- smt_set_funs+    , smtPush, smtPop      -- * Check Validity-    , checkValid, checkValidWithContext+    , checkValid+    , checkValid'+    , checkValidWithContext     , checkValids-    , makeZ3Context+    , makeSmtContext      ) where -import           Language.Fixpoint.Types.Config (SMTSolver (..))-import           Language.Fixpoint.Misc   (errorstar)+import           Language.Fixpoint.Types.Config ( SMTSolver (..)+                                                , Config+                                                , solver+                                                , extensionality+                                                , alphaEquivalence+                                                , betaEquivalence+                                                , normalForm+                                                , stringTheory)+import           Language.Fixpoint.Misc         (errorstar) import           Language.Fixpoint.Types.Errors+-- import           Language.Fixpoint.SortCheck    (elaborate) import           Language.Fixpoint.Utils.Files-import           Language.Fixpoint.Types+import           Language.Fixpoint.Types hiding (allowHO) import           Language.Fixpoint.Smt.Types-import           Language.Fixpoint.Smt.Theories  (preamble)-import           Language.Fixpoint.Smt.Serialize (initSMTEnv)--+import qualified Language.Fixpoint.Smt.Theories as Thy+import           Language.Fixpoint.Smt.Serialize ()  import           Control.Applicative      ((<|>)) import           Control.Monad+import           Control.Exception import           Data.Char import           Data.Monoid import qualified Data.Text                as T-import           Data.Text.Format         hiding (format)+import           Data.Text.Format import qualified Data.Text.IO             as TIO--- import qualified Data.Text.Lazy           as LT--- import qualified Data.Text.Lazy.IO        as LTIO+import qualified Data.Text.Lazy           as LT+import qualified Data.Text.Lazy.Builder   as Builder+import qualified Data.Text.Lazy.IO        as LTIO import           System.Directory import           System.Console.CmdArgs.Verbosity import           System.Exit              hiding (die) import           System.FilePath-import           System.IO                (IOMode (..), hClose, hFlush, openFile)+import           System.IO                (Handle, IOMode (..), hClose, hFlush, openFile) import           System.Process import qualified Data.Attoparsec.Text     as A+import qualified Data.HashMap.Strict      as M+import           Data.Attoparsec.Internal.Types (Parser) import           Text.PrettyPrint.HughesPJ (text) {- runFile f@@ -98,39 +110,44 @@   -- TODO take makeContext's Bool from caller instead of always using False?-makeZ3Context :: FilePath -> [(Symbol, Sort)] -> IO Context-makeZ3Context f xts-  = do me <- makeContextWithSEnv False Z3 f $ fromListSEnv xts-       smtDecls me (toListSEnv initSMTEnv)-       smtDecls me xts-       return me+makeSmtContext :: Config -> FilePath -> [(Symbol, Sort)] -> IO Context+makeSmtContext cfg f xts = do+  me <- makeContextWithSEnv cfg f $ fromListSEnv xts+  smtDecls me theoryDecls+  smtDecls me xts+  return me -checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool-checkValidWithContext me xts p q-  = smtBracket me $ do smtDecls me xts-                       smtAssert me $ pAnd [p, PNot q]-                       smtCheckUnsat me+theoryDecls :: [(Symbol, Sort)]+theoryDecls = [ (x, tsSort ty) | (x, ty) <- M.toList Thy.theorySymbols, not (tsInterp ty)] +checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool+checkValidWithContext me xts p q =+  smtBracket me "checkValidWithContext" $+    checkValid' me xts p q  -- | type ClosedPred E = {v:Pred | subset (vars v) (keys E) } -- checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Bool-checkValid :: Bool -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool-checkValid u f xts p q-  = do me <- makeContext u Z3 f-       smtDecls me xts-       smtAssert me $ pAnd [p, PNot q]-       smtCheckUnsat me+checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool+checkValid cfg f xts p q = do+  me <- makeContext cfg f+  checkValid' me xts p q +checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool+checkValid' me xts p q = do+  smtDecls me xts+  smtAssert me $ pAnd [p, PNot q]+  smtCheckUnsat me+ -- | If you already HAVE a context, where all the variables have declared types --   (e.g. if you want to make MANY repeated Queries)  -- checkValid :: e:Env -> [ClosedPred e] -> IO [Bool]-checkValids :: Bool -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]-checkValids u f xts ps-  = do me <- makeContext u Z3 f+checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]+checkValids cfg f xts ps+  = do me <- makeContext cfg f        smtDecls me xts        forM ps $ \p ->-          smtBracket me $+          smtBracket me "checkValids" $             smtAssert me (PNot p) >> smtCheckUnsat me  -- debugFile :: FilePath@@ -144,15 +161,15 @@ -------------------------------------------------------------------------- command              :: Context -> Command -> IO Response ---------------------------------------------------------------------------command me !cmd      = {-# SCC "command" #-} say cmd >> hear cmd+command me !cmd       = say cmd >> hear cmd   where-    say               = smtWrite me . runSmt2 (smtenv me)+    say               = smtWrite me . Builder.toLazyText . runSmt2     hear CheckSat     = smtRead me     hear (GetValue _) = smtRead me     hear _            = return Ok  -smtWrite :: Context -> T.Text -> IO ()+smtWrite :: Context -> Raw -> IO () smtWrite me !s = smtWriteRaw me s  smtRead :: Context -> IO Response@@ -162,22 +179,29 @@        case A.eitherResult res of          Left e  -> errorstar $ "SMTREAD:" ++ e          Right r -> do-           maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (cLog me)+           maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (ctxLog me)            -- when (verbose me) $ TIO.putStrLn $ format "SMT Says: {}" (Only $ show r)            return r +type SmtParser a = Parser T.Text a++responseP :: SmtParser Response responseP = {-# SCC "responseP" #-} A.char '(' *> sexpP          <|> A.string "sat"     *> return Sat          <|> A.string "unsat"   *> return Unsat          <|> A.string "unknown" *> return Unknown +sexpP :: SmtParser Response sexpP = {-# SCC "sexpP" #-} A.string "error" *> (Error <$> errorP)      <|> Values <$> valuesP +errorP :: SmtParser T.Text errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")" +valuesP :: SmtParser [(Symbol, T.Text)] valuesP = A.many1' pairP <* A.char ')' +pairP :: SmtParser (Symbol, T.Text) pairP = {-# SCC "pairP" #-}   do A.skipSpace      A.char '('@@ -187,107 +211,129 @@      A.char ')'      return (x,v) +symbolP :: SmtParser Symbol symbolP = {-# SCC "symbolP" #-} symbol <$> A.takeWhile1 (not . isSpace) +valueP :: SmtParser T.Text valueP = {-# SCC "valueP" #-} negativeP       <|> A.takeWhile1 (\c -> not (c == ')' || isSpace c)) +negativeP :: SmtParser T.Text negativeP   = do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')'        return $ "(" <> v <> ")" --- {- pairs :: {v:[a] | (len v) mod 2 = 0} -> [(a,a)] -}--- pairs :: [a] -> [(a,a)]--- pairs !xs = case L.splitAt 2 xs of---              ([],_)      -> []---              ([x,y], zs) -> (x,y) : pairs zs--smtWriteRaw      :: Context -> T.Text -> IO ()+smtWriteRaw      :: Context -> Raw -> IO () smtWriteRaw me !s = {-# SCC "smtWriteRaw" #-} do-  hPutStrLnNow (cOut me) s-  -- whenLoud $ TIO.appendFile debugFile (s <> "\n")-  maybe (return ()) (`hPutStrLnNow` s) (cLog me)+  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")+  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")+  hPutStrLnNow (ctxCout me) s+  maybe (return ()) (`hPutStrLnNow` s) (ctxLog me) -smtReadRaw       :: Context -> IO Raw-smtReadRaw me    = {-# SCC "smtReadRaw" #-} TIO.hGetLine (cIn me)+smtReadRaw       :: Context -> IO T.Text+smtReadRaw me    = {-# SCC "smtReadRaw" #-} TIO.hGetLine (ctxCin me) -hPutStrLnNow h !s   = TIO.hPutStrLn h s >> hFlush h+hPutStrLnNow     :: Handle -> LT.Text -> IO ()+hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h  -------------------------------------------------------------------------- -- | SMT Context --------------------------------------------------------- --------------------------------------------------------------------------  ---------------------------------------------------------------------------makeContext   :: Bool -> SMTSolver -> FilePath -> IO Context+makeContext   :: Config -> FilePath -> IO Context ---------------------------------------------------------------------------makeContext u s f-  = do me   <- makeProcess s-       pre  <- smtPreamble u s me+makeContext cfg f+  = do me   <- makeProcess cfg+       pre  <- smtPreamble cfg (solver cfg) me        createDirectoryIfMissing True $ takeDirectory smtFile        hLog <- openFile smtFile WriteMode-       let me' = me { cLog = Just hLog }+       let me' = me { ctxLog = Just hLog }        mapM_ (smtWrite me') pre        return me'     where        smtFile = extFileName Smt2 f -makeContextWithSEnv :: Bool -> SMTSolver -> FilePath  -> SMTEnv -> IO Context-makeContextWithSEnv u s f env-  = (\cxt -> cxt {smtenv = env}) <$> makeContext u s f+makeContextWithSEnv :: Config -> FilePath -> SMTEnv -> IO Context+makeContextWithSEnv cfg f env+  = (\cxt -> cxt {ctxSmtEnv = env}) <$> makeContext cfg f+  -- where msg = "makeContextWithSEnv" ++ show env -makeContextNoLog :: Bool -> SMTSolver -> IO Context-makeContextNoLog u s-  = do me  <- makeProcess s-       pre <- smtPreamble u s me+makeContextNoLog :: Config -> IO Context+makeContextNoLog cfg+  = do me  <- makeProcess cfg+       pre <- smtPreamble cfg (solver cfg) me        mapM_ (smtWrite me) pre        return me -makeProcess :: SMTSolver -> IO Context-makeProcess s-  = do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd s+makeProcess :: Config -> IO Context+makeProcess cfg+  = do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd (solver cfg)        loud <- isLoud-       return Ctx { pId     = pid-                  , cIn     = hIn-                  , cOut    = hOut-                  , cLog    = Nothing-                  , verbose = loud-                  , smtenv  = initSMTEnv+       return Ctx { ctxPid     = pid+                  , ctxCin     = hIn+                  , ctxCout    = hOut+                  , ctxLog     = Nothing+                  , ctxVerbose = loud+                  , ctxExt     = extensionality cfg+                  , ctxAeq     = alphaEquivalence cfg+                  , ctxBeq     = betaEquivalence  cfg+                  , ctxNorm    = normalForm       cfg+                  , ctxSmtEnv  = Thy.theorySEnv                   }  -------------------------------------------------------------------------- cleanupContext :: Context -> IO ExitCode ---------------------------------------------------------------------------cleanupContext (Ctx {..})-  = do hClose cIn-       hClose cOut-       maybe (return ()) hClose cLog-       waitForProcess pId+cleanupContext (Ctx {..}) = do+  hCloseMe "ctxCin"  ctxCin+  hCloseMe "ctxCout" ctxCout+  maybe (return ()) (hCloseMe "ctxLog") ctxLog+  waitForProcess ctxPid +hCloseMe :: String -> Handle -> IO ()+hCloseMe msg h = hClose h `catch` (\(exn :: IOException) -> putStrLn $ "OOPS, hClose breaks: " ++ msg ++ show exn)+ {- "z3 -smt2 -in"                   -} {- "z3 -smtc SOFT_TIMEOUT=1000 -in" -} {- "z3 -smtc -in MBQI=false"        -} +smtCmd         :: SMTSolver -> String --  T.Text smtCmd Z3      = "z3 -smt2 -in" smtCmd Mathsat = "mathsat -input=smt2" smtCmd Cvc4    = "cvc4 --incremental -L smtlib2"  -- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...-smtPreamble u Z3 me+smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]+smtPreamble cfg Z3 me   = do smtWrite me "(get-info :version)"        v:_ <- T.words . (!!1) . T.splitOn "\"" <$> smtReadRaw me-       if T.splitOn "." v `versionGreater` ["4", "3", "2"]-         then return $ z3_432_options ++ preamble u Z3-         else return $ z3_options     ++ preamble u Z3-smtPreamble u s _-  = return $ preamble u s+       checkValidStringFlag Z3 v cfg+       if T.splitOn "." v `versionGreaterEq` ["4", "3", "2"]+         then return $ z3_432_options ++ makeMbqi cfg ++ Thy.preamble cfg Z3+         else return $ z3_options     ++ makeMbqi cfg ++ Thy.preamble cfg Z3+smtPreamble cfg s _+  = checkValidStringFlag s "" cfg >> return (Thy.preamble cfg s) -versionGreater (x:xs) (y:ys)+checkValidStringFlag :: SMTSolver -> T.Text -> Config -> IO ()+checkValidStringFlag smt v cfg+  = when (noString smt v cfg) $+      die $ err dummySpan (text "stringTheory is only supported by z3 version >=4.2.2")++noString :: SMTSolver -> T.Text -> Config -> Bool+noString smt v cfg+  =  stringTheory cfg+  && not (smt == Z3 && (T.splitOn "." v `versionGreaterEq` ["4", "4", "2"]))+++versionGreaterEq :: Ord a => [a] -> [a] -> Bool+versionGreaterEq (x:xs) (y:ys)   | x >  y = True-  | x == y = versionGreater xs ys+  | x == y = versionGreaterEq xs ys   | x <  y = False-versionGreater _  [] = True-versionGreater [] _  = False-versionGreater _ _ = errorstar "Interface.versionGreater called with bad arguments"+versionGreaterEq _  [] = True+versionGreaterEq [] _  = False+versionGreaterEq _ _ = errorstar "Interface.versionGreater called with bad arguments"  ----------------------------------------------------------------------------- -- | SMT Commands -----------------------------------------------------------@@ -297,9 +343,8 @@ smtPush me        = interact' me Push smtPop me         = interact' me Pop - smtDecls :: Context -> [(Symbol, Sort)] -> IO ()-smtDecls me xts = forM_ xts (\(x,t) -> smtDecl me x t)+smtDecls = mapM_ . uncurry . smtDecl  smtDecl :: Context -> Symbol -> Sort -> IO () smtDecl me x t = interact' me (Declare x ins out)@@ -311,45 +356,57 @@                 Just (_, ins, out) -> (ins, out)                 Nothing            -> ([] , t  ) +-- hack now this is used only for checking gradual condition. smtCheckSat :: Context -> Expr -> IO Bool smtCheckSat me p--- hack now this is used only for checking gradual condition.  = smtAssert me p >> (ans <$> command me CheckSat)  where    ans Sat = True    ans _   = False  smtAssert :: Context -> Expr -> IO ()-smtAssert me p    = interact' me (Assert Nothing p)+smtAssert me p  = interact' me (Assert Nothing p) ++smtAssertAxiom :: Context -> Triggered Expr -> IO ()+smtAssertAxiom me p  = interact' me (AssertAxiom p)+ smtDistinct :: Context -> [Expr] -> IO () smtDistinct me az = interact' me (Distinct az)  smtCheckUnsat :: Context -> IO Bool smtCheckUnsat me  = respSat <$> command me CheckSat -smtBracket :: Context -> IO a -> IO a-smtBracket me a   = do smtPush me-                       r <- a-                       smtPop me-                       return r+smtBracket :: Context -> String -> IO a -> IO a+smtBracket me _msg a   = do+  smtPush me+  r <- a+  smtPop me+  return r +respSat :: Response -> Bool respSat Unsat   = True respSat Sat     = False respSat Unknown = False respSat r       = die $ err dummySpan $ text ("crash: SMTLIB2 respSat = " ++ show r) +interact' :: Context -> Command -> IO () interact' me cmd  = void $ command me cmd +makeMbqi :: Config -> [LT.Text]+makeMbqi cfg+  | extensionality cfg = [""]+  | otherwise          = ["\n(set-option :smt.mbqi false)"]+ -- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...+z3_432_options :: [LT.Text] z3_432_options   = [ "(set-option :auto-config false)"     , "(set-option :model true)"-    , "(set-option :model.partial false)"-    , "(set-option :smt.mbqi false)" ]+    , "(set-option :model.partial false)"] +z3_options :: [LT.Text] z3_options   = [ "(set-option :auto-config false)"     , "(set-option :model true)"-    , "(set-option :model-partial false)"-    , "(set-option :mbqi false)" ]+    , "(set-option :model-partial false)"]

@@ -3,88 +3,61 @@ {-# LANGUAGE OverloadedStrings    #-} {-# LANGUAGE PatternGuards        #-} {-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE DoAndIfThenElse      #-}  -- | This module contains the code for serializing Haskell values --   into SMTLIB2 format, that is, the instances for the @SMTLIB2@ --   typeclass. We split it into a separate module as it depends on --   Theories (see @smt2App@). -module Language.Fixpoint.Smt.Serialize where+module Language.Fixpoint.Smt.Serialize () where  import           Language.Fixpoint.Types---import           Language.Fixpoint.Types.Names (mulFuncName, divFuncName) import           Language.Fixpoint.Smt.Types import qualified Language.Fixpoint.Smt.Theories as Thy-import qualified Data.Text                      as T-import           Data.Text.Format               hiding (format)-import           Language.Fixpoint.Misc (errorstar) -- , traceShow)--import           Language.Fixpoint.SortCheck (elaborate)--import           Control.Monad.State- +import           Data.Monoid+import qualified Data.Text.Lazy.Builder         as Builder+import           Data.Text.Format+import           Language.Fixpoint.Misc (errorstar) import           Data.Maybe (fromMaybe) --{--    (* (L t1 t2 t3) is now encoded as-        ---> (((L @ t1) @ t2) @ t3)-        ---> App(@, [App(@, [App(@, [L[]; t1]); t2]); t3])-        The following decodes the above as-     *)-    let rec app_args_of_t acc = function-      | App (c, [t1; t2]) when c = tc_app -> app_args_of_t (t2 :: acc) t1-      | App (c, [])                       -> (c, acc)-      | t                                 -> (tc_app, t :: acc)--      (*-      | Ptr (Loc s)                       -> (tycon s, acc)-      | t                                 -> assertf "app_args_of_t: unexpected t1 = %s" (to_string t)-      *)--    let app_of_t = function-      | App (c, _) as t when c = tc_app   -> Some (app_args_of_t [] t)-      | App (c, ts)                       -> Some (c, ts)-      | _                                 -> None---}+-- instance SMTLIB2 Sort where+--   smt2 s@(FFunc _ _)           = errorstar $ "smt2 FFunc: " ++ showpp s+--   smt2 FInt                    = "Int"+--   smt2 FReal                   = "Real"+--   smt2 t+--     | t == boolSort            = "Bool"+--   smt2 t+--     | Just d <- Thy.smt2Sort t = d+--   smt2 _                       = "Int" -instance SMTLIB2 Sort where-  smt2 s@(FFunc _ _)           = errorstar $ "smt2 FFunc: " ++ show s-  smt2 FInt                    = "Int"-  smt2 FReal                   = "Real"-  smt2 t-    | t == boolSort            = "Bool"-  smt2 t-    | Just d <- Thy.smt2Sort t = d-  smt2 _                       = "Int"+instance SMTLIB2 (Symbol, Sort) where+  smt2 c@(sym, t) = build "({} {})" (smt2 sym, smt2Sort c t) -  defunc (FAbs _ t)      = defunc t-  defunc (FFunc _ _)     = return $ intSort-  defunc t | isSMTSort t = return t-  defunc _               = return intSort+smt2Sort :: (PPrint a) => a -> Sort -> Builder.Builder+smt2Sort msg = go+  where+    go s@(FFunc _ _)             = errorstar $ unwords ["smt2 FFunc:", showpp msg, showpp s]+    go FInt                      = "Int"+    go FReal                     = "Real"+    go t+      | t == boolSort            = "Bool"+    go t+      | Just d <- Thy.smt2Sort t = d+    go _                         = "Int"  instance SMTLIB2 Symbol where   smt2 s     | Just t <- Thy.smt2Symbol s = t-  smt2 s                         = symbolSafeText  s--instance SMTLIB2 (Symbol, Sort) where-  smt2 (sym, t) = format "({} {})" (smt2 sym, smt2 t)--  defunc (sym, t) = do bx <- defunc sym -                       bt <- defunc t -                       return $ (bx, bt)-+  smt2 s                         = Builder.fromText $ symbolSafeText  s  instance SMTLIB2 SymConst where-  smt2   = smt2   . symbol-+  smt2 = smt2 . symbol  instance SMTLIB2 Constant where-  smt2 (I n)   = format "{}" (Only n)-  smt2 (R d)   = format "{}" (Only d)-  smt2 (L t _) = format "{}" (Only t) -- errorstar $ "Horrors, how to translate: " ++ show c+  smt2 (I n)   = build "{}" (Only n)+  smt2 (R d)   = build "{}" (Only d)+  smt2 (L t _) = build "{}" (Only t)  instance SMTLIB2 LocSymbol where   smt2 = smt2 . val@@ -92,8 +65,8 @@ instance SMTLIB2 Bop where   smt2 Plus   = "+"   smt2 Minus  = "-"-  smt2 Times  = symbolSafeText mulFuncName-  smt2 Div    = symbolSafeText divFuncName+  smt2 Times  = Builder.fromText $ symbolSafeText mulFuncName+  smt2 Div    = Builder.fromText $ symbolSafeText divFuncName   smt2 RTimes = "*"   smt2 RDiv   = "/"   smt2 Mod    = "mod"@@ -109,366 +82,94 @@  -- NV TODO: change the way EApp is printed instance SMTLIB2 Expr where-  smt2 (ESym z)         = smt2 (symbol z)+  smt2 (ESym z)         = smt2 z   smt2 (ECon c)         = smt2 c   smt2 (EVar x)         = smt2 x   smt2 e@(EApp _ _)     = smt2App e-  smt2 (ENeg e)         = format "(- {})" (Only $ smt2 e)-  smt2 (EBin o e1 e2)   = format "({} {} {})" (smt2 o, smt2 e1, smt2 e2)-  smt2 (EIte e1 e2 e3)  = format "(ite {} {} {})" (smt2 e1, smt2 e2, smt2 e3)+  smt2 (ENeg e)         = build "(- {})" (Only $ smt2 e)+  smt2 (EBin o e1 e2)   = build "({} {} {})" (smt2 o, smt2 e1, smt2 e2)+  smt2 (EIte e1 e2 e3)  = build "(ite {} {} {})" (smt2 e1, smt2 e2, smt2 e3)   smt2 (ECst e _)       = smt2 e   smt2 (PTrue)          = "true"   smt2 (PFalse)         = "false"   smt2 (PAnd [])        = "true"-  smt2 (PAnd ps)        = format "(and {})"   (Only $ smt2s ps)+  smt2 (PAnd ps)        = build "(and {})"   (Only $ smt2s ps)   smt2 (POr [])         = "false"-  smt2 (POr ps)         = format "(or  {})"   (Only $ smt2s ps)-  smt2 (PNot p)         = format "(not {})"   (Only $ smt2  p)-  smt2 (PImp p q)       = format "(=> {} {})" (smt2 p, smt2 q)-  smt2 (PIff p q)       = format "(= {} {})"  (smt2 p, smt2 q)-  smt2 (PExist bs p)    = format "(exists ({}) {})"  (smt2s bs, smt2 p)-  smt2 (PAll   bs p)    = format "(forall ({}) {})"  (smt2s bs, smt2 p)+  smt2 (POr ps)         = build "(or  {})"   (Only $ smt2s ps)+  smt2 (PNot p)         = build "(not {})"   (Only $ smt2  p)+  smt2 (PImp p q)       = build "(=> {} {})" (smt2 p, smt2 q)+  smt2 (PIff p q)       = build "(= {} {})"  (smt2 p, smt2 q)+  smt2 (PExist [] p)    = smt2 p+  smt2 (PExist bs p)    = build "(exists ({}) {})"  (smt2s bs, smt2 p)+  smt2 (PAll   [] p)    = smt2 p+  smt2 (PAll   bs p)    = build "(forall ({}) {})"  (smt2s bs, smt2 p)    smt2 (PAtom r e1 e2)  = mkRel r e1 e2-  smt2 PGrad            = "true"+  smt2 (ELam (x, _) e)  = smt2Lam x e   smt2  e               = errorstar ("smtlib2 Pred  " ++ show e)  --- new version -  defunc e@(ESym _)       = return e -  defunc e@(ECon _)       = return e -  defunc e@(EVar _)       = return e -  defunc e@(EApp _ _)     = defuncApp e-  defunc (ENeg e)         = ENeg <$> defunc e -  defunc (EBin o e1 e2)   = defuncBop o e1 e2-  defunc (EIte e1 e2 e3)  = do e1'   <- defunc e1 -                               e2'   <- defunc e2 -                               e3'   <- defunc e3 -                               return $ EIte e1' e2' e3'-  defunc (ECst e t)       = (`ECst` t) <$> defunc e-  defunc (PTrue)          = return PTrue-  defunc (PFalse)         = return PFalse-  defunc (PAnd [])        = return PTrue-  defunc (PAnd ps)        = PAnd <$> mapM defunc ps-  defunc (POr [])         = return PFalse-  defunc (POr ps)         = POr <$> mapM defunc ps-  defunc (PNot p)         = PNot <$> defunc  p-  defunc (PImp p q)       = PImp <$> defunc p <*> defunc q -  defunc (PIff p q)       = PIff <$> defunc p <*> defunc q -  defunc (PExist bs p)    = do bs' <- mapM defunc bs -                               p'  <- withExtendedEnv bs $ defunc p -                               return $ PExist bs' p'-  defunc (PAll   bs p)    = do bs' <- mapM defunc bs -                               p'  <- withExtendedEnv bs $ defunc p -                               return $ PAll bs' p' -  defunc (PAtom r e1 e2)  = PAtom r <$> defunc e1 <*> defunc e2 -  defunc PGrad            = return PGrad-  defunc  e               = errorstar ("smtlib2 Pred  " ++ show e)--defuncBop o e1 e2-  | o == Times, s1 == FReal, s2 == FReal-  = do e1' <- defunc e1 -       e2' <- defunc e2-       return $ EBin RTimes e1' e2'-  | o == Div, s1 == FReal, s2 == FReal-  = do e1' <- defunc e1-       e2' <- defunc e2-       return $ EBin RDiv e1' e2' -  | otherwise-  = do e1' <- defunc e1 -       e2' <- defunc e2 -       return $ EBin o e1' e2' -  where-    s1 = exprSort e1-    s2 = exprSort e2-+smt2Lam :: Symbol -> Expr -> Builder.Builder+smt2Lam x e = build "({} {} {})" (smt2 lambdaName, smt2 x, smt2 e) -smt2App :: Expr -> T.Text-smt2App e = fromMaybe (format "({} {})" (smt2 f, smt2many (smt2 <$> es))) (Thy.smt2App (eliminate f) $ (smt2 <$> es))+smt2App :: Expr -> Builder.Builder+smt2App e = fromMaybe (build "({} {})" (smt2 f, smt2s es)) $ Thy.smt2App (eliminate f) $ map smt2 es   where-    (f, es) = splitEApp e+    (f, es) = splitEApp' e  -defuncApp :: Expr -> SMT2 Expr -defuncApp e = case Thy.smt2App (eliminate f) $ (smt2 <$> es) of -                Just _ -> eApps f <$> mapM defunc es  -                _      -> defuncApp' f es+splitEApp' :: Expr -> (Expr, [Expr])+splitEApp'            = go []   where-    (f, es) = splitEApp e+    go acc (EApp f e) = go (e:acc) f+    go acc (ECst e _) = go acc e+    go acc e          = (e, acc) -eliminate (ECst e _) = e+eliminate :: Expr -> Expr+eliminate (ECst e _) = eliminate e eliminate e          = e -defuncApp' :: Expr -> [Expr] -> SMT2 Expr -defuncApp' f [] = defunc f-defuncApp' f es = makeApplication f es--- smt2App' env f es = format "({} {})" (smt2 env f, smt2many (smt2 env <$> es)) -- makeApplication env f es--+mkRel :: Brel -> Expr -> Expr -> Builder.Builder+mkRel Ne  e1 e2 = mkNe e1 e2+mkRel Une e1 e2 = mkNe e1 e2+mkRel r   e1 e2 = build "({} {} {})" (smt2 r, smt2 e1, smt2 e2) -mkRel Ne  e1 e2         = mkNe e1 e2-mkRel Une e1 e2         = mkNe e1 e2-mkRel r   e1 e2         = format "({} {} {})" (smt2 r, smt2 e1, smt2 e2)-mkNe  e1 e2             = format "(not (= {} {}))" (smt2 e1, smt2 e2)+mkNe :: Expr -> Expr -> Builder.Builder+mkNe  e1 e2              = build "(not (= {} {}))" (smt2 e1, smt2 e2)  instance SMTLIB2 Command where   -- NIKI TODO: formalize this transformation-  smt2 (Declare x ts t)    = format "(declare-fun {} ({}) {})"     (smt2 x, smt2s ts, smt2 t)-  smt2 (Define t)          = format "(declare-sort {})"            (Only $ smt2 t)-  smt2 (Assert Nothing p)  = format "(assert {})"                  (Only $ smt2 p)-  smt2 (Assert (Just i) p) = format "(assert (! {} :named p-{}))"  (smt2 p, i)+  smt2 c@(Declare x ts t)  = build "(declare-fun {} ({}) {})"     (smt2 x, smt2many (smt2Sort c <$> ts), smt2Sort c t) -- HEREHEREHERE (smt2 x, smt2s ts, smt2 t)+  smt2 c@(Define t)        = build "(declare-sort {})"            (Only $ smt2Sort c t)+  smt2 (Assert Nothing p)  = build "(assert {})"                  (Only $ smt2 p)+  smt2 (Assert (Just i) p) = build "(assert (! {} :named p-{}))"  (smt2 p, i)   smt2 (Distinct az)     -- Distinct must have at least 2 arguments     | length az < 2        = ""-    | otherwise            = format "(assert (distinct {}))"       (Only $ smt2s az)+    | otherwise            = build "(assert (distinct {}))"       (Only $ smt2s az)+  smt2 (AssertAxiom t)     = build "(assert {})"                  (Only $ smt2 t)   smt2 (Push)              = "(push 1)"   smt2 (Pop)               = "(pop 1)"   smt2 (CheckSat)          = "(check-sat)"-  smt2 (GetValue xs)       = T.unwords $ ["(get-value ("] ++ fmap smt2 xs ++ ["))"]+  smt2 (GetValue xs)       = "(get-value (" <> smt2s xs <> "))"   smt2 (CMany cmds)        = smt2many (smt2 <$> cmds) --  defunc (Declare x ts t)-     | isSMTSymbol x-     = do dx  <- defunc x -          dts <- mapM defunc ts-          dt  <- defunc t   -          return $ Declare dx dts dt -     | null ts && isSMTSort t-     = do dx <- defunc x -          dt <- defunc t-          return $ Declare dx [] dt -     | otherwise-     = do dx <- defunc x -          return $ Declare dx [] intSort--  defunc (Define t)  = return $ Define t -  defunc (Assert Nothing p)  -    = do env <- smt2env <$> get -         (p', fs) <- grapLambdas $ elaborate env p-         dfs <- mapM defineFun fs -         p'' <- defunc p'-         return $ CMany (concat dfs ++ [Assert Nothing p''])--  defunc (Assert (Just i) p) -    = do env <- smt2env <$> get -         (p', fs) <- grapLambdas $ elaborate env p-         dfs <- mapM defineFun fs -         p'' <- defunc p' -         return $ CMany (concat dfs ++ [Assert (Just i) p''])---   smt2 env (Assert (Just i) p) = format "(assert (! {} :named p-{}))"  (smt2 env $ elaborate env p, i)-  defunc (Distinct az)       = Distinct <$> mapM defunc az -  defunc (Push)              = return Push -  defunc (Pop)               = return Pop -  defunc (CheckSat)          = return CheckSat-  defunc (GetValue xs)       = return $ GetValue xs -  defunc (CMany cmds)        = CMany <$> mapM defunc cmds --smt2s    :: SMTLIB2 a => [a] -> T.Text-smt2s as = smt2many (smt2 <$> as)--smt2many :: [T.Text] -> T.Text-smt2many = T.intercalate " "---defineFun :: (Symbol, Expr) -> SMT2 [Command]-defineFun (f, ELam (x, t) (ECst e tr))-  = do decl   <- defunc $ Declare f (t:(snd <$> xts)) tr -       assert <- withExtendedEnv [(f, FFunc t tr)] $ -                   defunc $ Assert Nothing (PAll ((x,t):xts) -                                  (PAtom Eq (mkApp (EApp (EVar f) (EVar x)) (fst <$> xts)) bd))-       return $ [decl, assert]-  where-    go acc (ELam (x, t) e) = go ((x,t):acc) e -    go acc (ECst e _)      = go acc e -    go acc e               = (acc, e)-    -    (xts, bd) = go [] e --    mkApp e' []     = e' -    mkApp e' (x:xs) = mkApp (EApp e' (EVar x)) xs--defineFun  _ -  = errorstar "die"---isSMTSymbol x = Thy.isTheorySymbol x || memberSEnv x initSMTEnv --{--(declare-fun x () Int)-(declare-fun y () Int)-(assert (<= 0 x))-(assert (< x y))-(push 1)-(assert (not (<= 0 y)))-(check-sat)-(pop 1)-(push 1)-(assert (<= 0 y))-(check-sat)-(pop 1)--}+instance SMTLIB2 (Triggered Expr) where+  smt2 (TR NoTrigger e)       = smt2 e  +  smt2 (TR _ (PExist [] p))   = smt2 p+  smt2 t@(TR _ (PExist bs p)) = build "(exists ({}) (! {} :pattern({})))"  (smt2s bs, smt2 p, smt2s $ makeTriggers t)+  smt2 (TR _ (PAll   [] p))   = smt2 p+  smt2 t@(TR _ (PAll   bs p)) = build "(forall ({}) (! {} :pattern({})))"  (smt2s bs, smt2 p, smt2s $ makeTriggers t)+  smt2 (TR _ e)               = smt2 e   -------------------------------------------------------------------------------------------------------  Defunctionalizaion ----------------------------------------------------------------------------------------------------------------------------------------grapLambdas e = go [] e -  where-    go acc e@(ELam _ _) = do f <- freshSym -                             return (EVar f, (f, e):acc)-    go acc e@(ESym _)   = return (e, acc)-    go acc e@(ECon _)   = return (e, acc)-    go acc e@(EVar _)   = return (e, acc)-    go acc (EApp e1 e2) = do (e1', fs1) <- go [] e1 -                             (e2', fs2) <- go [] e2-                             return (EApp e1' e2', fs1 ++ fs2 ++ acc) -    go acc (ENeg e)     = do (e', fs) <- go acc e -                             return (ENeg e', fs)-    go acc (PNot e)     = do (e', fs) <- go acc e -                             return (PNot e', fs)-    go acc (EBin b e1 e2) = do (e1', fs1) <- go [] e1 -                               (e2', fs2) <- go [] e2-                               return (EBin b e1' e2', fs1 ++ fs2 ++ acc) -    go acc (PAtom b e1 e2) = do (e1', fs1) <- go [] e1 -                                (e2', fs2) <- go [] e2-                                return (PAtom b e1' e2', fs1 ++ fs2 ++ acc) -    go acc (EIte e e1 e2) = do (e' , fs)  <- go [] e-                               (e1', fs1) <- go [] e1 -                               (e2', fs2) <- go [] e2-                               return (EIte e' e1' e2', fs ++ fs1 ++ fs2 ++ acc) -    go acc (ECst e s)     = do (e', fs) <- go acc e-                               return (ECst e' s, fs)-    go acc (ETAbs e s)    = do (e', fs) <- go acc e -                               return (ETAbs e' s, fs)-    go acc (ETApp e s)    = do (e', fs) <- go acc e -                               return (ETApp e' s, fs)-    go acc (PAnd es)      = do es' <- mapM (go []) es-                               return (PAnd (fst <$> es'), concat (acc:(snd <$> es')))-    go acc (POr es)       = do es' <- mapM (go []) es-                               return (POr (fst <$> es'),  concat (acc:(snd <$> es')))-    go acc (PImp e1 e2)   = do (e1', fs1) <- go [] e1 -                               (e2', fs2) <- go [] e2-                               return (PImp e1' e2', fs1 ++ fs2 ++ acc) -    go acc (PIff e1 e2)   = do (e1', fs1) <- go [] e1 -                               (e2', fs2) <- go [] e2-                               return (PIff e1' e2', fs1 ++ fs2 ++ acc) -    go acc (PAll bs e)    = do (e', fs) <- go acc e -                               return (PAll bs e', fs) -    go acc (PExist bs e)  = do (e', fs) <- go acc e -                               return (PExist bs e', fs) -    go acc e@PGrad        = return (e, acc)-    go acc e@(PKVar _ _)  = return (e, acc)---- NIKI: This is new code, check and formalize!----- make Application is called on uninterpreted functions------ makeApplication e [e1, ..., en] =  apply^n_s (e, toInt e1, ..., toInt en)--- where--- applyn :: (Int, Int, ..., Int) -> s--- e      :: (Int, ..., Int) -> s--- toInt e = e, if e :: s, s is smt uninterpeted--- toInt e = s_to_Int (e), otherwise---- s_to_Int :: s -> Int--makeApplication :: Expr -> [Expr] -> SMT2 Expr -makeApplication e es-  = do df  <- defunc f -       de  <- defunc e -       des <- mapM toInt es -       return $ eApps (EVar df) (de:des)-  where-    f  = makeFunSymbol e $ length es---makeFunSymbol :: Expr -> Int -> Symbol-makeFunSymbol e i-  | (FApp (FTC c) _)          <- s, fTyconSymbol c == "Set_Set"-  = setApplyName i-  | (FApp (FApp (FTC c) _) _) <- s, fTyconSymbol c == "Map_t"-  = mapApplyName i-  | (FApp (FTC bv) (FTC s))   <- s, Thy.isBv bv, Just _ <- Thy.sizeBv s-  = bitVecApplyName i-  | FTC c                     <- s, c == boolFTyCon-  = boolApplyName i-  | s == FReal-  = realApplyName i-  | otherwise-  = intApplyName i-  where-    s = dropArgs i $ exprSort e--    dropArgs 0 t           = t-    dropArgs i (FAbs _ t)  = dropArgs i t-    dropArgs i (FFunc _ t) = dropArgs (i-1) t-    dropArgs _ _           = die $ err dummySpan "dropArgs: the impossible happened"--toInt :: Expr -> SMT2 Expr -toInt e-  |  (FApp (FTC c) _)         <- s, fTyconSymbol c == "Set_Set"-  = castWith setToIntName e-  | (FApp (FApp (FTC c) _) _) <- s, fTyconSymbol c == "Map_t"-  = castWith mapToIntName e-  | (FApp (FTC bv) (FTC s))   <- s, Thy.isBv bv, Just _ <- Thy.sizeBv s-  = castWith bitVecToIntName e-  | FTC c                     <- s, c == boolFTyCon-  = castWith boolToIntName e-  | FTC c                     <- s, c == realFTyCon-  = castWith realToIntName e-  | otherwise-  = defunc e-  where-    s = exprSort e--isSMTSort :: Sort -> Bool-isSMTSort s-  | (FApp (FTC c) _)         <- s, fTyconSymbol c == "Set_Set"-  = True-  | (FApp (FApp (FTC c) _) _) <- s, fTyconSymbol c == "Map_t"-  = True-  | (FApp (FTC bv) (FTC s))   <- s, Thy.isBv bv, Just _ <- Thy.sizeBv s-  = True-  | FTC c                     <- s, c == boolFTyCon-  = True-  | s == FReal-  = True-  | otherwise-  = False---castWith :: Symbol -> Expr -> SMT2 Expr -castWith s e = -  do bs <- defunc s -     be <- defunc e-     return $ EApp (EVar bs) be--initSMTEnv = fromListSEnv $-  [ (setToIntName,    FFunc (setSort intSort)   intSort)-  , (bitVecToIntName, FFunc bitVecSort intSort)-  , (mapToIntName,    FFunc (mapSort intSort intSort) intSort)-  , (boolToIntName,   FFunc boolSort   intSort)-  , (realToIntName,   FFunc realSort   intSort)-  ]-  ++ concatMap makeApplies [1..7]--makeApplies i =-  [ (intApplyName i,    go i intSort)-  , (setApplyName i,    go i (setSort intSort))-  , (bitVecApplyName i, go i bitVecSort)-  , (mapApplyName i,    go i $ mapSort intSort intSort)-  , (realApplyName i,   go i realSort)-  , (boolApplyName i,   go i boolSort)-  ]-  where-    go 0 s = FFunc intSort s-    go i s = FFunc intSort $ go (i-1) s-+{-# INLINE smt2s #-}+smt2s    :: SMTLIB2 a => [a] -> Builder.Builder+smt2s as = smt2many (map smt2 as) -exprSort :: Expr -> Sort-exprSort (ECst _ s) = s-exprSort e          = errorstar ("\nexprSort on unexpected expressions" ++ show e)+smt2many :: [Builder.Builder] -> Builder.Builder+smt2many []     = mempty+smt2many [b]    = b+smt2many (b:bs) = b <> mconcat [ " " <> b | b <- bs ]+{-# INLINE smt2many #-}

@@ -16,42 +16,50 @@      , preamble         -- * Bit Vector Operations-     , isBv, sizeBv+     , sizeBv+     , toInt -     , isTheorySymbol-     , theoryEnv+       -- * Theory Symbols+     , theorySymbols+     , theorySEnv +     -- * String+     -- , string+     -- , genLen+        -- * Theories-     , theorySymbols      , setEmpty, setEmp, setCap, setSub, setAdd, setMem      , setCom, setCup, setDif, setSng, mapSel, mapSto++      -- * Query Theories+     , isSmt2App+     , isConName+     , axiomLiterals      ) where  import           Prelude hiding (map)+import           Language.Fixpoint.Types.Sorts import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types import           Language.Fixpoint.Smt.Types import qualified Data.HashMap.Strict      as M-import qualified Data.Text                as T-import           Data.Text.Format         hiding (format)-+import           Data.Maybe (catMaybes, isJust)+import           Data.Monoid+import qualified Data.Text.Lazy           as T+import qualified Data.Text.Lazy.Builder   as Builder+import           Data.Text.Format+import qualified Data.Text+import           Data.String                 (IsString(..))  -------------------------------------------------------------------------- -- | Set Theory ---------------------------------------------------------- -------------------------------------------------------------------------- -elt, set, map :: Raw +elt, set, map :: Raw elt  = "Elt" set  = "Set" map  = "Map" ---- bit, sz32, sz64 :: Raw--- bit  = symbolText bitVecName -- "BitVec"--- sz32 = symbolText size32Name -- "Size32"--- sz64 = symbolText size64Name -- "Size64"-- emp, add, cup, cap, mem, dif, sub, com, sel, sto :: Raw emp   = "smt_set_emp" add   = "smt_set_add"@@ -64,7 +72,6 @@ sel   = "smt_map_sel" sto   = "smt_map_sto" - setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng, mapSel, mapSto :: Symbol setEmpty = "Set_empty" setEmp   = "Set_emp"@@ -79,9 +86,36 @@ mapSel   = "Map_select" mapSto   = "Map_store" -z3Preamble :: Bool -> [T.Text]++strLen, strSubstr, strConcat :: (IsString a) => a -- Symbol+strLen    = "strLen"+strSubstr = "subString"+strConcat = "concatString"+-- NOPROP genLen :: Symbol+-- NOPROP genLen = "len"++-- NOPROP strlen, strsubstr, strconcat :: Raw+-- NOPROP strlen    = "strLen"+-- NOPROP strsubstr = "subString"+-- NOPROP strconcat = "concatString"++z3strlen, z3strsubstr, z3strconcat :: Raw+z3strlen    = "str.len"+z3strsubstr = "str.substr"+z3strconcat = "str.++"++strLenSort, substrSort, concatstrSort :: Sort+strLenSort    = FFunc strSort intSort+substrSort    = mkFFunc 0 [strSort, intSort, intSort, strSort]+concatstrSort = mkFFunc 0 [strSort, strSort, strSort]++string :: Raw+string = strConName++z3Preamble :: Config -> [T.Text] z3Preamble u-  = [ format "(define-sort {} () Int)"+  = stringPreamble u +++    [ format "(define-sort {} () Int)"         (Only elt)     , format "(define-sort {} () (Array {} Bool))"         (set, elt)@@ -107,20 +141,27 @@         (sel, map, elt, elt)     , format "(define-fun {} ((m {}) (k {}) (v {})) {} (store m k v))"         (sto, map, elt, elt, map)-    , uifDef u (symbolText mulFuncName) ("*"::T.Text)-    , uifDef u (symbolText divFuncName) ("div"::T.Text)+    , format "(define-fun {} ((b Bool)) Int (ite b 1 0))"+        (Only (boolToIntName :: T.Text))+    , uifDef u (symbolText mulFuncName) ("*"   :: T.Text)+    , uifDef u (symbolText divFuncName) "div"     ]  -- RJ: Am changing this to `Int` not `Real` as (1) we usually want `Int` and -- (2) have very different semantics. TODO: proper overloading, post genEApp-uifDef u f op | u         = format "(declare-fun {} (Int Int) Int)" (Only f)-              | otherwise = format "(define-fun {} ((x Int) (y Int)) Int ({} x y))" (f, op)+uifDef :: Config -> Data.Text.Text -> T.Text -> T.Text+uifDef cfg f op+  | linear cfg || Z3 /= solver cfg+  = format "(declare-fun {} (Int Int) Int)" (Only f)+  | otherwise+  = format "(define-fun {} ((x Int) (y Int)) Int ({} x y))" (f, op) -cvc4Preamble :: Bool -> [T.Text]+cvc4Preamble :: Config -> [T.Text] cvc4Preamble _ --TODO use uif flag u (see z3Preamble)   = [        "(set-logic ALL_SUPPORTED)"     , format "(define-sort {} () Int)"       (Only elt)     , format "(define-sort {} () Int)"       (Only set)+    , format "(define-sort {} () Int)"       (Only string)     , format "(declare-fun {} () {})"        (emp, set)     , format "(declare-fun {} ({} {}) {})"   (add, set, elt, set)     , format "(declare-fun {} ({} {}) {})"   (cup, set, set, set)@@ -134,9 +175,11 @@         (sel, map, elt, elt)     , format "(define-fun {} ((m {}) (k {}) (v {})) {} (store m k v))"         (sto, map, elt, elt, map)+    , format "(define-fun {} ((b Bool)) Int (ite b 1 0))"+        (Only (boolToIntName :: Raw))     ] -smtlibPreamble :: Bool -> [T.Text]+smtlibPreamble :: Config -> [T.Text] smtlibPreamble _ --TODO use uif flag u (see z3Preamble)   = [       --  "(set-logic QF_AUFRIA)",       format "(define-sort {} () Int)"       (Only elt)@@ -151,64 +194,168 @@     , format "(define-sort {} () Int)"       (Only map)     , format "(declare-fun {} ({} {}) {})"    (sel, map, elt, elt)     , format "(declare-fun {} ({} {} {}) {})" (sto, map, elt, elt, map)+    , format "(declare-fun {} ({} {} {}) {})" (sto, map, elt, elt, map)+    , format "(define-fun {} ((b Bool)) Int (ite b 1 0))" (Only (boolToIntName :: Raw))     ] -{--mkSetSort _ _  = set-mkEmptySet _ _ = emp-mkSetAdd _ s x = format "({} {} {})" (add, s, x)-mkSetMem _ x s = format "({} {} {})" (mem, x, s)-mkSetCup _ s t = format "({} {} {})" (cup, s, t)-mkSetCap _ s t = format "({} {} {})" (cap, s, t)-mkSetDif _ s t = format "({} {} {})" (dif, s, t)-mkSetSub _ s t = format "({} {} {})" (sub, s, t)--} --- smt_set_funs :: M.HashMap Symbol Raw--- smt_set_funs = M.fromList [ (setEmp, emp), (setAdd, add), (setCup, cup)---                           , (setCap, cap), (setMem, mem), (setDif, dif)---                           , (setSub, sub), (setCom, com)]+stringPreamble :: Config -> [T.Text]+stringPreamble cfg | stringTheory cfg+  = [+      format "(define-sort {} () String)" (Only string)+    , format "(define-fun {} ((s {})) Int ({} s))"+        (strLen :: Raw, string, z3strlen)+    , format "(define-fun {} ((s {}) (i Int) (j Int)) {} ({} s i j))"+        (strSubstr :: Raw, string, string, z3strsubstr)+    , format "(define-fun {} ((x {}) (y {})) {} ({} x y))"+        (strConcat :: Raw, string, string, string, z3strconcat)+    ]+stringPreamble _+  = [+      format "(define-sort {} () Int)" (Only string)+    , format "(declare-fun {} ({}) Int)"+        (strLen :: Raw, string)+    , format "(declare-fun {} ({} Int Int) {})"+        (strSubstr :: Raw, string, string)+    , format "(declare-fun {} ({} {}) {})"+        (strConcat :: Raw, string, string, string)+    ]  -isTheorySymbol :: Symbol -> Bool-isTheorySymbol x = M.member x theorySymbols -theoryEnv = M.map tsSort theorySymbols +-------------------------------------------------------------------------------+-- | Exported API -------------------------------------------------------------+-------------------------------------------------------------------------------+smt2Symbol :: Symbol -> Maybe Builder.Builder+smt2Symbol x = Builder.fromLazyText . tsRaw <$> M.lookup x theorySymbols +smt2Sort :: Sort -> Maybe Builder.Builder+smt2Sort (FApp (FTC c) _)+  | isConName setConName c      = Just $ build "{}" (Only set)+smt2Sort (FApp (FApp (FTC c) _) _)+  | isConName mapConName c      = Just $ build "{}" (Only map)+smt2Sort (FApp (FTC bv) (FTC s))+  | isConName bitVecName bv+  , Just n <- sizeBv s          = Just $ build "(_ BitVec {})" (Only n)+smt2Sort s+  | isString s                  = Just $ build "{}" (Only string)+smt2Sort _                      = Nothing++smt2App :: Expr -> [Builder.Builder] -> Maybe Builder.Builder+smt2App (EVar f) [d]+  | f == setEmpty = Just $ build "{}"             (Only emp)+  | f == setEmp   = Just $ build "(= {} {})"      (emp, d)+  | f == setSng   = Just $ build "({} {} {})"     (add, emp, d)+smt2App (EVar f) (d:ds)+  | Just s <- M.lookup f theorySymbols+  = Just $ build "({} {})" (tsRaw s, d <> mconcat [ " " <> d | d <- ds])+smt2App _ _           = Nothing++-- isSmt2App :: Expr -> [a] -> Bool+-- isSmt2App e xs = tracepp ("isSmt2App e := " ++ show e) (isSmt2App' e xs)++isSmt2App :: Expr -> [a] -> Bool+isSmt2App (EVar f) [_]+  | f == setEmpty = True+  | f == setEmp   = True+  | f == setSng   = True+isSmt2App (EVar f) _+  =  isJust $ M.lookup f theorySymbols+isSmt2App _ _+  = False+++preamble :: Config -> SMTSolver -> [T.Text]+preamble u Z3   = z3Preamble u+preamble u Cvc4 = cvc4Preamble u+preamble u _    = smtlibPreamble u++--------------------------------------------------------------------------------+-- | Converting Non-Int types to Int -------------------------------------------+--------------------------------------------------------------------------------+-- toInt :: Expr -> Sort -> Expr+-- toInt e s = tracepp msg (toInt' e s)+  -- where+    -- msg   = "toInt e = " ++ show e ++ ", t = " ++ show s++toInt :: Expr -> Sort -> Expr+toInt e s+  |  (FApp (FTC c) _) <- s+  , isConName setConName c+  = castWith setToIntName e+  | (FApp (FApp (FTC c) _) _) <- s+  , isConName mapConName c+  = castWith mapToIntName e+  | (FApp (FTC bv) (FTC s)) <- s+  , isConName bitVecName bv+  , Just _ <- sizeBv s+  = castWith bitVecToIntName e+  | FTC c <- s+  , c == boolFTyCon+  = castWith boolToIntName e+  | FTC c <- s+  , c == realFTyCon+  = castWith realToIntName e+  | otherwise+  = e++castWith :: Symbol -> Expr -> Expr+castWith s = eAppC intSort (EVar s)++--------------------------------------------------------------------------------+-- | Theory Symbols : `uninterpSEnv` should be disjoint from see `interpSEnv`+--   to avoid duplicate SMT definitions.  `uninterpSEnv` is for uninterpreted+--   symbols, and `interpSEnv` is for interpreted symbols.+--------------------------------------------------------------------------------+theorySEnv :: SEnv Sort+theorySEnv = fromListSEnv . M.toList . fmap tsSort $ theorySymbols++-- | `theorySymbols` contains the list of ALL SMT symbols with interpretations,+--   i.e. which are given via `define-fun` (as opposed to `declare-fun`) theorySymbols :: M.HashMap Symbol TheorySymbol-theorySymbols = M.fromList-  [ tSym setEmp   emp (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)-  , tSym setEmpty emp (FAbs 0 $ FFunc intSort (setSort $ FVar 0))-  , tSym setAdd add   setbopSort -  , tSym setCup cup   setbopSort-  , tSym setCap cap   setbopSort-  , tSym setMem mem   setmemSort-  , tSym setDif dif   setbopSort-  , tSym setSub sub   setcmpSort-  , tSym setCom com   setcmpSort-  , tSym mapSel sel   mapselSort-  , tSym mapSto sto   mapstoSort-  , tSym bvOrName "bvor"   bvbopSort-  , tSym bvAndName "bvand" bvbopSort+theorySymbols = M.fromList $ uninterpSymbols ++ interpSymbols++-- isTheorySymbol :: Symbol -> Bool+-- isTheorySymbol x = M.member x theorySymbols++interpSymbols :: [(Symbol, TheorySymbol)]+interpSymbols =+  [ interpSym setEmp   emp  (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)+  , interpSym setEmpty emp  (FAbs 0 $ FFunc intSort (setSort $ FVar 0))+  , interpSym setAdd   add   setBopSort+  , interpSym setCup   cup   setBopSort+  , interpSym setCap   cap   setBopSort+  , interpSym setMem   mem   setMemSort+  , interpSym setDif   dif   setBopSort+  , interpSym setSub   sub   setCmpSort+  , interpSym setCom   com   setCmpSort+  , interpSym mapSel   sel   mapSelSort+  , interpSym mapSto   sto   mapStoSort+  , interpSym bvOrName "bvor"   bvBopSort+  , interpSym bvAndName "bvand" bvBopSort+  , interpSym strLen    strLen    strLenSort+  , interpSym strSubstr strSubstr substrSort+  , interpSym strConcat strConcat concatstrSort+  , interpSym boolInt   boolInt   (FFunc boolSort intSort)   ]   where-    setbopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)-    setmemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort-    setcmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort-    mapselSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1)) $ FFunc (FVar 0) (FVar 0)-    mapstoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1)) -                                 $ FFunc (FVar 0) -                                 $ FFunc (FVar 1) +    boolInt    = boolToIntName+    setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)+    setMemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort+    setCmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort+    mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1)) $ FFunc (FVar 0) (FVar 1)+    mapStoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))+                                 $ FFunc (FVar 0)+                                 $ FFunc (FVar 1)                                          (mapSort (FVar 0) (FVar 1))-    bvbopSort  = FFunc bitVecSort $ FFunc bitVecSort bitVecSort+    bvBopSort  = FFunc bitVecSort $ FFunc bitVecSort bitVecSort  -tSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)-tSym x n t = (x, Thy x n t)-+interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)+interpSym x n t = (x, Thy x n t True) -isBv :: FTycon -> Bool-isBv = (bitVecName ==) . val . fTyconSymbol+isConName :: Symbol -> FTycon -> Bool+isConName s = (s ==) . val . fTyconSymbol  sizeBv :: FTycon -> Maybe Int sizeBv tc@@ -218,36 +365,53 @@   where     s               = val $ fTyconSymbol tc +uninterpSymbols :: [(Symbol, TheorySymbol)]+uninterpSymbols = [ (x, uninterpSym x t) | (x, t) <- uninterpSymbols'] ----------------------------------------------------------------------------------- | Exported API ---------------------------------------------------------------------------------------------------------------------------------------------+uninterpSym :: Symbol -> Sort -> TheorySymbol+uninterpSym x t =  Thy x (lt x) t False+  where+    lt           = T.fromStrict . symbolSafeText -smt2Symbol :: Symbol -> Maybe T.Text-smt2Symbol x = tsRaw <$> M.lookup x theorySymbols+uninterpSymbols' :: [(Symbol, Sort)]+uninterpSymbols' =+  [ (setToIntName,    FFunc (setSort intSort)   intSort)+  , (bitVecToIntName, FFunc bitVecSort intSort)+  , (mapToIntName,    FFunc (mapSort intSort intSort) intSort)+  , (realToIntName,   FFunc realSort   intSort)+  , (lambdaName   ,   FFunc intSort (FFunc intSort intSort))+  ]+  ++ concatMap makeApplies [1..maxLamArg]+  ++ [(makeLamArg s i, s) | i <- [1..maxLamArg], s <- sorts] -smt2Sort :: Sort -> Maybe T.Text-smt2Sort (FApp (FTC c) _)-  | fTyconSymbol c == "Set_Set" = Just $ format "{}" (Only set)-smt2Sort (FApp (FApp (FTC c) _) _)-  | fTyconSymbol c == "Map_t"   = Just $ format "{}" (Only map)-smt2Sort (FApp (FTC bv) (FTC s))-  | isBv bv-  , Just n <- sizeBv s          = Just $ format "(_ BitVec {})" (Only n)-smt2Sort _                      = Nothing+-- THESE ARE DUPLICATED IN DEFUNCTIONALIZATION+maxLamArg :: Int+maxLamArg = 7 -smt2App :: Expr -> [T.Text] -> Maybe T.Text-smt2App (EVar f) [d]-  | f == setEmpty = Just $ format "{}"             (Only emp)-  | f == setEmp   = Just $ format "(= {} {})"      (emp, d)-  | f == setSng   = Just $ format "({} {} {})"     (add, emp, d)-smt2App (EVar f) ds-  | Just s <- M.lookup f theorySymbols-  = Just $ format "({} {})" (tsRaw s, T.intercalate " " ds) -smt2App _ _           = Nothing+sorts :: [Sort]+sorts = [intSort] +-- NIKI TODO: allow non integer lambda arguments+-- sorts = [setSort intSort, bitVecSort intSort, mapSort intSort intSort, boolSort, realSort, intSort] -preamble :: Bool -> SMTSolver -> [T.Text]-preamble u Z3   = z3Preamble u-preamble u Cvc4 = cvc4Preamble u-preamble u _    = smtlibPreamble u+makeLamArg :: Sort -> Int  -> Symbol+makeLamArg _ = intArgName++makeApplies :: Int -> [(Symbol, Sort)]+makeApplies i =+  [ (intApplyName i,    go i intSort)+  , (setApplyName i,    go i (setSort intSort))+  , (bitVecApplyName i, go i bitVecSort)+  , (mapApplyName i,    go i $ mapSort intSort intSort)+  , (realApplyName i,   go i realSort)+  , (boolApplyName i,   go i boolSort)+  ]+  where+    go 0 s = FFunc intSort s+    go i s = FFunc intSort $ go (i-1) s++axiomLiterals :: [(Symbol, Sort)] -> [Expr]+axiomLiterals lts = catMaybes [ lenAxiom l <$> litLen l | (l, t) <- lts, isString t ]+  where+    lenAxiom l n  = EEq (EApp (expr (strLen :: Symbol)) (expr l)) (expr n `ECst` intSort)+    litLen        = fmap (Data.Text.length .  symbolText) . unLitSymbol

@@ -10,6 +10,7 @@      -- * Serialized Representation       Raw+    , symbolBuilder      -- * Commands     , Command  (..)@@ -19,106 +20,102 @@      -- * Typeclass for SMTLIB2 conversion     , SMTLIB2 (..)+    , runSmt2      -- * SMTLIB2 Process Context     , Context (..) -    -- * SMTLIB2 symbol environment -    , SMTEnv, emptySMTEnv, SMTSt(..), withExtendedEnv, SMT2, freshSym-     -- * Theory Symbol     , TheorySymbol (..)--    -- * Strict Formatter-    , format-+    , SMTEnv     ) where  import           Language.Fixpoint.Types-import qualified Data.Text.Format         as DTF-import           Data.Text.Format.Params  (Params)+-- import           Language.Fixpoint.Misc   (traceShow) import qualified Data.Text                as T import qualified Data.Text.Lazy           as LT+import qualified Data.Text.Lazy.Builder   as LT+import           Text.PrettyPrint.HughesPJ + import           System.IO                (Handle) import           System.Process-import           Control.Monad.State ------------------------------------------------------------------------------ | Types ------------------------------------------------------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Types ---------------------------------------------------------------------+--------------------------------------------------------------------------------+type Raw          = LT.Text -type Raw          = T.Text+symbolBuilder :: Symbol -> LT.Builder+symbolBuilder = LT.fromText . symbolSafeText  -- | Commands issued to SMT engine data Command      = Push                   | Pop                   | CheckSat-                  | Declare   Symbol [Sort] Sort-                  | Define    Sort-                  | Assert    (Maybe Int) Expr+                  | Declare   !Symbol [Sort] !Sort+                  | Define    !Sort+                  | Assert    !(Maybe Int) !Expr+                  | AssertAxiom  !(Triggered Expr)                   | Distinct  [Expr] -- {v:[Expr] | 2 <= len v}                   | GetValue  [Symbol]                   | CMany [Command]                   deriving (Eq, Show) +instance PPrint Command where+  pprintTidy _ = ppCmd++ppCmd :: Command -> Doc+ppCmd Push          = text "Push"+ppCmd Pop           = text "Pop"+ppCmd CheckSat      = text "CheckSat"+ppCmd (Declare {})  = text "Declare ..."+ppCmd (Define {})   = text "Define ..."+ppCmd (Assert _ e)  = text "Assert" <+> pprint e+ppCmd (AssertAxiom _) = text "AssertAxiom ..."+ppCmd (Distinct {}) = text "Distinct ..."+ppCmd (GetValue {}) = text "GetValue ..."+ppCmd (CMany {})    = text "CMany ..."+ -- | Responses received from SMT engine data Response     = Ok                   | Sat                   | Unsat                   | Unknown-                  | Values [(Symbol, Raw)]-                  | Error Raw+                  | Values [(Symbol, T.Text)]+                  | Error !T.Text                   deriving (Eq, Show)  -- | Information about the external SMT process-data Context      = Ctx { pId     :: ProcessHandle-                        , cIn     :: Handle-                        , cOut    :: Handle-                        , cLog    :: Maybe Handle-                        , verbose :: Bool-                        , smtenv  :: SMTEnv-                        }---- | Theory Symbol-data TheorySymbol  = Thy { tsSym  :: Symbol-                         , tsRaw  :: Raw-                         , tsSort :: Sort-                         }-                     deriving (Eq, Ord, Show)---------------------------------------------------------------------------- | AST Conversion: Types that can be serialized -----------------------------------------------------------------------------------------------format :: Params ps => DTF.Format -> ps -> T.Text-format f x = LT.toStrict $ DTF.format f x--type SMTEnv = SEnv Sort -data SMTSt  = SMTSt {fresh :: Int , smt2env :: SMTEnv}--type SMT2   = State SMTSt+data Context = Ctx+  { ctxPid     :: !ProcessHandle+  , ctxCin     :: !Handle+  , ctxCout    :: !Handle+  , ctxLog     :: !(Maybe Handle)+  , ctxVerbose :: !Bool+  , ctxExt     :: !Bool              -- ^ flag to enable function extentionality axioms+  , ctxAeq     :: !Bool              -- ^ flag to enable lambda a-equivalence axioms+  , ctxBeq     :: !Bool              -- ^ flag to enable lambda b-equivalence axioms+  , ctxNorm    :: !Bool              -- ^ flag to enable lambda normal form equivalence axioms+  , ctxSmtEnv  :: !SMTEnv+  } -emptySMTEnv = emptySEnv +type SMTEnv = SEnv Sort -withExtendedEnv bs act = do -  env <- smt2env <$> get -  let env' = foldl (\env (x, t) -> insertSEnv x t env) env bs-  modify $ \s -> s{smt2env = env'}-  r <- act -  modify $ \s -> s{smt2env = env}-  return r +-- | Theory Symbol+data TheorySymbol  = Thy+  { tsSym    :: !Symbol    -- ^ name+  , tsRaw    :: !Raw       -- ^ serialized SMTLIB2 name+  , tsSort   :: !Sort      -- ^ sort+  , tsInterp :: !Bool      -- ^ TRUE = defined (interpreted), FALSE = declared (uninterpreted)+  }+  deriving (Eq, Ord, Show) -freshSym = do -  n <- fresh <$> get -  modify $ \s -> s{fresh = n + 1}-  return $ intSymbol "lambda_fun_" n +--------------------------------------------------------------------------------+-- | AST Conversion: Types that can be serialized ------------------------------+-------------------------------------------------------------------------------- --- | Types that can be serialized class SMTLIB2 a where-  defunc :: a -> SMT2 a-  defunc = return --  smt2 :: a -> T.Text +  smt2 :: a -> LT.Builder -  runSmt2 :: SMTEnv -> a -> T.Text -  runSmt2 env a = smt2 $ evalState (defunc a) (SMTSt 0 env)+runSmt2 :: (SMTLIB2 a) => a -> LT.Builder+runSmt2 = smt2

@@ -18,70 +18,70 @@   , parseFInfo ) where - import           Control.Concurrent import           Data.Binary--- import           Data.Maybe                         (fromMaybe)--- import           Data.List                          hiding (partition)--- import qualified Data.HashSet                       as S import           System.Exit                        (ExitCode (..))---- import           System.Console.CmdArgs.Verbosity   hiding (Loud)+import           System.Console.CmdArgs.Verbosity   (whenNormal) import           Text.PrettyPrint.HughesPJ          (render)--- import           Text.Printf                        (printf) import           Control.Monad                      (when) import           Control.Exception                  (catch)--import           Language.Fixpoint.Solver.Graph     -- (slice)-import           Language.Fixpoint.Solver.Validate  (sanitize)-import qualified Language.Fixpoint.Solver.Eliminate as E--- import           Language.Fixpoint.Solver.Deps      -- (deps, GDeps (..))+import           Language.Fixpoint.Solver.Sanitize  (symbolEnv, sanitize) import           Language.Fixpoint.Solver.UniqifyBinds (renameAll)+import           Language.Fixpoint.Defunctionalize (defunctionalize)+import           Language.Fixpoint.SortCheck            (Elaborate (..)) import           Language.Fixpoint.Solver.UniqifyKVars (wfcUniqify) import qualified Language.Fixpoint.Solver.Solve     as Sol--- import           Language.Fixpoint.Solver.Solution  (Solution)--import           Language.Fixpoint.Types.Config           (queryFile, multicore, Config (..))+import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types.Errors import           Language.Fixpoint.Utils.Files            hiding (Result) import           Language.Fixpoint.Misc-import           Language.Fixpoint.Utils.Progress import           Language.Fixpoint.Utils.Statistics (statistics)-import           Language.Fixpoint.Partition        -- (mcInfo, partition, partition')-import           Language.Fixpoint.Parse            (rr', mkQual)+import           Language.Fixpoint.Graph+import           Language.Fixpoint.Parse            (rr') import           Language.Fixpoint.Types-import           Language.Fixpoint.Minimize (minQuery)+import           Language.Fixpoint.Minimize (minQuery, minQuals, minKvars)+import           Language.Fixpoint.Solver.Instantiate (instantiateFInfo)+import           Language.Fixpoint.Smt.Interface (makeSmtContext, smtPush) import           Control.DeepSeq - --------------------------------------------------------------------------- -- | Solve an .fq file ---------------------------------------------------- --------------------------------------------------------------------------- solveFQ :: Config -> IO ExitCode --------------------------------------------------------------------------- solveFQ cfg = do-    fi      <- readFInfo file-    r       <- solve cfg fi-    let stat = resStatus $!! r+    (fi, opts) <- readFInfo file+    cfg'       <- withPragmas cfg opts+    let fi'     = ignoreQualifiers cfg' fi+    r          <- solve cfg' fi'+    let stat    = resStatus $!! r     -- let str  = render $ resultDoc $!! (const () <$> stat)     -- putStrLn "\n"-    colorStrLn (colorResult stat) (statStr $!! stat)+    whenNormal $ colorStrLn (colorResult stat) (statStr $!! stat)     return $ eCode r   where-    file    = inFile       cfg+    file    = srcFile      cfg     eCode   = resultExit . resStatus     statStr = render . resultDoc . fmap fst ------------------------------------------------------------------------------- | Solve FInfo system of horn-clause constraints ----------------------------------------------------------------------------------------------------+ignoreQualifiers :: Config -> FInfo a -> FInfo a+ignoreQualifiers cfg fi+  | eliminate cfg == All = fi { quals = [] }+  | otherwise            = fi+++--------------------------------------------------------------------------------+-- | Solve FInfo system of horn-clause constraints -----------------------------+-------------------------------------------------------------------------------- solve :: (NFData a, Fixpoint a) => Solver a----------------------------------------------------------------------------+-------------------------------------------------------------------------------- solve cfg q-  | parts cfg    = partition  cfg        $!! q-  | stats cfg    = statistics cfg        $!! q-  | minimize cfg = minQuery   cfg solve' $!! q-  | otherwise    = solve'     cfg        $!! q+  | parts cfg      = partition  cfg        $!! q+  | stats cfg      = statistics cfg        $!! q+  | minimize cfg   = minQuery   cfg solve' $!! q+  | minimizeQs cfg = minQuals cfg solve'   $!! q+  | minimizeKs cfg = minKvars cfg solve'   $!! q+  | otherwise      = solve'     cfg        $!! q  solve' :: (NFData a, Fixpoint a) => Solver a solve' cfg q = do@@ -93,98 +93,107 @@   | multicore cfg = solveParWith   | otherwise     = solveSeqWith -----------------------------------------------------------------------------readFInfo :: FilePath -> IO (FInfo ())-----------------------------------------------------------------------------readFInfo f        = fixFileName <$> act-  where-    fixFileName q  = q {fileName = f}-    act-      | isBinary f = readBinFq f-      | otherwise  = readFq f+--------------------------------------------------------------------------------+readFInfo :: FilePath -> IO (FInfo (), [String])+--------------------------------------------------------------------------------+readFInfo f+  | isBinary f = (,) <$> readBinFq f <*> return []+  | otherwise  = readFq f -readFq :: FilePath -> IO (FInfo ())+readFq :: FilePath -> IO (FInfo (), [String]) readFq file = do   str   <- readFile file-  let q = {-# SCC "parsefq" #-} rr' file str :: FInfo ()-  return q+  let q  = {-# SCC "parsefq" #-} rr' file str :: FInfoWithOpts ()+  return (fioFI q, fioOpts q)  readBinFq :: FilePath -> IO (FInfo ()) readBinFq file = {-# SCC "parseBFq" #-} decodeFile file ----------------------------------------------------------------------------+-------------------------------------------------------------------------------- -- | Solve in parallel after partitioning an FInfo to indepdendant parts----------------------------------------------------------------------------+-------------------------------------------------------------------------------- solveSeqWith :: (Fixpoint a) => Solver a -> Solver a-solveSeqWith s c fi0 = withProgressFI fi $ s c fi+solveSeqWith s c fi0 = {- withProgressFI fi $ -} s c fi   where-    fi               = slice fi0-+    fi               = slice c fi0 ----------------------------------------------------------------------------+-------------------------------------------------------------------------------- -- | Solve in parallel after partitioning an FInfo to indepdendant parts----------------------------------------------------------------------------+-------------------------------------------------------------------------------- solveParWith :: (Fixpoint a) => Solver a -> Solver a----------------------------------------------------------------------------+-------------------------------------------------------------------------------- solveParWith s c fi0 = do   -- putStrLn "Using Parallel Solver \n"-  let fi       = slice fi0-  withProgressFI fi $ do-    mci <- mcInfo c-    let (_, fis) = partition' (Just mci) fi-    writeLoud $ "Number of partitions : " ++ show (length fis)-    writeLoud $ "number of cores      : " ++ show (cores c)-    writeLoud $ "minimum part size    : " ++ show (minPartSize c)-    writeLoud $ "maximum part size    : " ++ show (maxPartSize c)-    case fis of-      []        -> errorstar "partiton' returned empty list!"-      [onePart] -> s c onePart-      _         -> inParallelUsing (s c) fis+  let fi    = slice c fi0+  mci      <- mcInfo c+  let fis   = partition' (Just mci) fi+  writeLoud $ "Number of partitions : " ++ show (length fis)+  writeLoud $ "number of cores      : " ++ show (cores c)+  writeLoud $ "minimum part size    : " ++ show (minPartSize c)+  writeLoud $ "maximum part size    : " ++ show (maxPartSize c)+  case fis of+    []        -> errorstar "partiton' returned empty list!"+    [onePart] -> s c onePart+    _         -> inParallelUsing (f s c) $ zip [1..] fis+    where+      f s c (j, fi) = s (c {srcFile = queryFile (Part j) c}) fi --------------------------------------------------------------------------------+-------------------------------------------------------------------------------- -- | Solve a list of FInfos using the provided solver function in parallel--------------------------------------------------------------------------------+-------------------------------------------------------------------------------- inParallelUsing :: (a -> IO (Result b)) -> [a] -> IO (Result b)--------------------------------------------------------------------------------+-------------------------------------------------------------------------------- inParallelUsing f xs = do    setNumCapabilities (length xs)    rs <- asyncMapM f xs    return $ mconcat rs ------------------------------------------------------------------------------- | Native Haskell Solver ----------------------------------------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Native Haskell Solver -----------------------------------------------------+-------------------------------------------------------------------------------- solveNative, solveNative' :: (NFData a, Fixpoint a) => Solver a----------------------------------------------------------------------------+-------------------------------------------------------------------------------- solveNative !cfg !fi0 = (solveNative' cfg fi0)                           `catch`                              (return . result)  result :: Error -> Result a-result e = Result (Crash [] msg) mempty+result e = Result (Crash [] msg) mempty mempty   where     msg  = showpp e +loudDump :: (Fixpoint a) => Int -> Config -> SInfo a -> IO ()+loudDump i cfg si = writeLoud $ msg ++ render (toFixpoint cfg si)+  where+    msg           = "fq file after Uniqify & Rename " ++ show i ++ "\n"+ solveNative' !cfg !fi0 = do   -- writeLoud $ "fq file in: \n" ++ render (toFixpoint cfg fi)   -- rnf fi0 `seq` donePhase Loud "Read Constraints"   -- let qs   = quals fi0   -- whenLoud $ print qs-  let fi1  = fi0 { quals = remakeQual <$> quals fi0 }+  -- TODO: make this less of a hack+  ctx <- makeSmtContext cfg (srcFile cfg ++ ".evals") []+  smtPush ctx+  fi1 <- instantiateFInfo cfg ctx $ fi0 { quals = remakeQual <$> quals fi0 }   -- whenLoud $ putStrLn $ showFix (quals fi1)   let si0   = {-# SCC "convertFormat" #-} convertFormat fi1   -- writeLoud $ "fq file after format convert: \n" ++ render (toFixpoint cfg si0)   -- rnf si0 `seq` donePhase Loud "Format Conversion"-  let si1 = either die id $ {-# SCC "validate" #-} sanitize $!! si0-  -- writeLoud $ "fq file after validate: \n" ++ render (toFixpoint cfg si1)+  let si1 = either die id $ {-# SCC "sanitize" #-} sanitize $!! si0+  -- writeLoud $ "fq file after sanitize: \n" ++ render (toFixpoint cfg si1)   -- rnf si1 `seq` donePhase Loud "Validated Constraints"   graphStatistics cfg si1   let si2  = {-# SCC "wfcUniqify" #-} wfcUniqify $!! si1-  let si3  = {-# SCC "renameAll" #-} renameAll $!! si2-  -- rnf si2 `seq` donePhase Loud "Uniqify"-  (s0, si4) <- {-# SCC "elim" #-} elim cfg $!! si3-  -- writeLoud $ "About to solve: \n" ++ render (toFixpoint cfg si4)-  res <- {-# SCC "Sol.solve" #-} Sol.solve cfg s0 $!! si4+  let si3  = {-# SCC "renameAll"  #-} renameAll  $!! si2+  rnf si3 `seq` donePhase Loud "Uniqify & Rename"+  loudDump 1 cfg si3+  let si4  = {-# SCC "defunction" #-} defunctionalize cfg $!! si3+  -- putStrLn $ "AXIOMS: " ++ showpp (asserts si4)+  loudDump 2 cfg si4+  let si5  = {-# SCC "elaborate"  #-} elaborate "solver" (symbolEnv cfg si4) si4+  loudDump 3 cfg si5+  res <- {-# SCC "Sol.solve" #-} Sol.solve cfg $!! si5   -- rnf soln `seq` donePhase Loud "Solve2"   --let stat = resStatus res   saveSolution cfg res@@ -193,58 +202,34 @@   -- colorStrLn (colorResult stat) (show stat)   return res --elim :: (Fixpoint a) => Config -> SInfo a -> IO (Solution, SInfo a)-elim cfg fi-  | eliminate cfg = do-      let (s0, fi') = E.eliminate fi-      writeLoud $ "fq file after eliminate: \n" ++ render (toFixpoint cfg fi')-      -- elimSolGraph cfg s0-      donePhase Loud "Eliminate"-      writeLoud $ "Solution after eliminate: \n" ++ showpp s0 -- toFixpoint cfg fi')-      -- donePhase Loud "DonePrint"-      return (s0, fi')-  | otherwise     =-      return (mempty, fi)--remakeQual :: Qualifier -> Qualifier-remakeQual q = {- traceShow msg $ -} mkQual (q_name q) (q_params q) (q_body q) (q_pos q)---   where---     msg      = "REMAKEQUAL: " ++ show q-------------------------------------------------------------------------------- | Extract ExitCode from Solver Result --------------------------------------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Extract ExitCode from Solver Result ---------------------------------------+-------------------------------------------------------------------------------- resultExit :: FixResult a -> ExitCode----------------------------------------------------------------------------+-------------------------------------------------------------------------------- resultExit Safe        = ExitSuccess resultExit (Unsafe _)  = ExitFailure 1 resultExit _           = ExitFailure 2 ------------------------------------------------------------------------------- | Parse External Qualifiers -------------------------------------------------------------------------------------------------------------------------parseFInfo :: [FilePath] -> IO (FInfo a) -- [Qualifier]----------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- | Parse External Qualifiers -------------------------------------------------+--------------------------------------------------------------------------------+parseFInfo :: [FilePath] -> IO (FInfo a)+-------------------------------------------------------------------------------- parseFInfo fs = mconcat <$> mapM parseFI fs -parseFI :: FilePath -> IO (FInfo a) --[Qualifier]+parseFI :: FilePath -> IO (FInfo a) parseFI f = do   str   <- readFile f   let fi = rr' f str :: FInfo ()   return $ mempty { quals = quals  fi-                  , lits  = lits   fi }+                  , gLits = gLits  fi+                  , dLits = dLits  fi }  saveSolution :: Config -> Result a -> IO () saveSolution cfg res = when (save cfg) $ do   let f = queryFile Out cfg   putStrLn $ "Saving Solution: " ++ f ++ "\n"   ensurePath f-  writeFile f $ "\nSolution:\n"  ++ showpp (resSolution res)-------------------------------------------------------------------------------- | Initialize Progress Bar-----------------------------------------------------------------------------withProgressFI :: FInfo a -> IO b -> IO b-----------------------------------------------------------------------------withProgressFI = withProgress . fromIntegral . gSccs . cGraph+  writeFile f $ "\nSolution:\n" ++ showpp (resSolution  res)+                ++ (if (gradual cfg) then ("\n\n" ++ showpp (gresSolution res)) else mempty)