---------------------
  Hard Reality Tool 
--------------------

HRT is a tool for randomly extracting
hard and realistic theory problems (conjunctive constraints)
from SMT problems with a non-trivial boolean structure.  

Available: http://www.cs.man.ac.uk/~korovink/hr/
Authors: Konstantin Korovin and Andrei Voronkov

----------------------
Installation:
----------------------
Requires: recent versions of OCaml and ocamlbuild

To build run: make 

This will create:  hard_reality

To clean: make clean 


--------------------------
Simple examples of usage:
--------------------------

1. "hard_reality --help"

   for an explanation of different options

2. "hard_reality 
      --input_dir ~/SMT_Bench/QF_LRA/all 
      --output_dir ~/SMT_Bench/QF_LRA/out_dir"

  HRT generates random problems from files in "~/SMT_Bench/QF_LRA/all"
  (there should be no subdirs in all)
  outputs problems into "~/SMT_Bench/QF_LRA/out_dir"
  this is done without a difficulty measure see 4. for this.

3. "hard_reality 
      --input_dir ~/SMT_Bench/QF_LRA/all 
      --output_dir ~/SMT_Bench/QF_LRA/out_dir 
      --solver "/home/z3/z3 -in"
    "

   Similar to 2. but runs z3 SMT solver on the generated problems 
   and outputs some statistics (see also out_dir/hard_reality.log)
   You can use any SMT solver accepting problems in SMT format 
   via stdin (e.g. "cvc3-optimized -lang smt")
   
4.  "hard_reality 
     --input_dir ~/SMT_Bench/QF_LRA/all 
     --output_dir ~/SMT_Bench/QF_LRA/out_dir 
     --solver "/home/z3/z3 -in" 
     --solver_input_time_limit 1. 
     --solver_output_time_limit 0.1 "

   HRT searches for difficult random theory problems: 
   1. skip the input problems which take less than 1s to solve
   2. accept only problems which takes greater or equal to 0.1s to solve

5. "hard_reality 
     --input_dir ~/SMT_Bench/QF_LRA/all 
     --output_dir ~/SMT_Bench/QF_LRA/out_dir 
     --solver "/home/z3/z3 -in" 
     --solver_input_time_limit 1. 
     --solver_output_time_limit 0.1 
     --search_max_sat true
  "
  HRT 1. searches for random theory problems
      2. extracts a maximal satisfiable subset
      3. accepts the result only if difficult enough (>= 0.1s to solve)

6.  "hard_reality 
     --input_dir ~/SMT_Bench/QF_LRA/all 
     --output_dir ~/SMT_Bench/QF_LRA/out_dir 
     --solver "/home/z3/z3 -in" 
     --solver_input_time_limit 1. 
     --solver_output_time_limit 0. 
     --search_min_unsat true
  "
  HRT 1. searches for random theory problems
      2. extracts a minimal unsatisfiable subset 

7. "hard_reality 
     --input_dir ~/SMT_Bench/QF_LRA/all 
     --output_dir ~/SMT_Bench/QF_LRA/out_dir 
     --solver "/home/z3/z3 -in" 
     --solver_input_time_limit 1. 
     --solver_output_time_limit 0.1
     --simplify_lra true
     --keep_non_lra_lits false
    "
 HRT for linear arithmetic:
  1. searches for random theory problems 
  2. from the theory problem extracts linear arithmetic terms 
  3. simplifies l.a. terms into the from 
      (and (> poly 0) (>= poly 0) (= poly 0)) 
     where poly is a sum of (* c_i x_i)(+c_0)  
     all c_i's are non zero integers and no repetition of variables 
  4. accepts the result only if difficult enough (>= 0.1s to solve)


------------------------------------------------
These are just examples, 
there are many other useful combinations of options, 
see hard_reality --help 
(default options can be found in src/options.ml)
--------------------------------------------------

----------------------
Acknowledgements:
----------------------

Hard Reality uses:

SMT-LIB parser/checker version 3.0
Available: http://combination.cs.uiowa.edu/smtlib/

Designed and implemented by  
  George Hagen, University of Iowa,
  Daniele Zucchelli, University of Milan, 
  Cesare Tinelli, University of Iowa


------------------------------------------------------------------------------------
Please, send your comments, suggestions and bug reports to  "korovin at cs.man.ac.uk"
------------------------------------------------------------------------------------