Dynamic label

README → DerivationSolver_py2/README

@@ -1,7 +1,7 @@
-Derivation Solver 
+#Derivation Solver 
 
 
-# License Notice
+##License Notice
 ****************************
 Derivation Solver provides implementation of derivation solvers for dependent 
 type inference. It consists of four constraint solvers, i.e., one-shot, 
@@ -26,7 +26,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 
 
 
-# Dependency
+##Dependency
 ****************************
 
 The solvers are implemented in Python with external support from Z3.  Our 
@@ -55,7 +55,7 @@ the python in use. Please refer to the Z3 binding
 (https://github.com/Z3Prover/z3) for more details. 
 
 
-# Quick Taste
+##Quick Taste
 ****************************
 
 Here is a quick demo to run a small test case(dsram.con). By default, the 
@@ -73,7 +73,7 @@ the it is complete. The file contains the execution time for all 6 test cases.
 
 
 
-# Reproducing the evaluation result
+##Reproducing the evaluation result
 ****************************
 
 To reproduce the evaluation result reported in the paper, here are the steps:
@@ -110,7 +110,7 @@ $ gnuplot -c plot-seq-comb.gnu result/all-time_3333_13_21_34.csv
 
 
 
-# Reuse 
+##Reuse 
 ****************************
 
 The current implementation provides multiple levels of reuse for future needs.

DerivationSolver_py2/README.md

@@ -0,0 +1,186 @@
+# Derivation Solver 
+
+
+## License Notice
+****************************
+Derivation Solver provides implementation of derivation solvers for dependent 
+type inference. It consists of four constraint solvers, i.e., one-shot, 
+early-accept, early-reject and hybrid solver along with two partition 
+algorithms: sequential and combinational partitioning. A parser for the core 
+constraint language and plotting scripts are also available in the package.
+
+Copyright (C) 2018  Peixuan Li
+
+Derivation Solver is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+Derivation Solver is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+
+
+## Dependency
+****************************
+
+The solvers are implemented in Python with external support from Z3.  Our 
+evaluation is set up using Python 2.7.10 and Z3 4.5.0, but the implementation 
+is not specialized to these versions. It is expected to be compatible for most 
+of the existing version of Python and Z3. After evaluation data are 
+obtained, we use gnuplot to visualize the result. 
+In summary, here is the list of dependency:
+
+- python (https://www.python.org/)
+- Z3 (https://github.com/Z3Prover/z3)
+- gnuplot (http://www.gnuplot.info/)
+
+
+** Note that Z3 needs to be installed and be binded to the python in use. Here 
+is a quick test to verify the binding:
+1. launch python in the command line:
+$ python
+2. In the python console, type :
+>>> from z3 import *
+>>> x = Real('x')
+
+If both statements finished with no error message, then Z3 is successfully 
+binded; otherwise, either Z3 is not successfully installed or not binding with 
+the python in use. Please refer to the Z3 binding 
+(https://github.com/Z3Prover/z3) for more details. 
+
+
+## Quick Taste
+****************************
+
+Here is a quick demo to run a small test case(dsram.con). By default, the 
+ test will solve the constraints in tests/dsram.con using all three 
+different solvers across two partition algorithms(6 unit tests in total):
+
+$ python test_solver.py tests/dsram.con
+
+
+Debug message will be printing out during the execution and the execution time 
+is saved under the result folder with name in form of 
+'[test file name]+[arguments]+[timestamps].csv'. 
+Thus, you should find a result file "dsramXXXXXXXX.csv" in result folder when 
+the it is complete. The file contains the execution time for all 6 test cases. 
+
+
+
+## Reproducing the evaluation result
+****************************
+
+To reproduce the evaluation result reported in the paper, here are the steps:
+1. run all the test files with three solvers(no early-reject since most of the 
+test cases are solvable and early-reject solver is not useful for solvable 
+cases) across two partition algorithms:
+
+$ python test_solver.py all
+
+This could take hours(~8h in our case) to finish. A brief break-down:
+100 test file * 3 approaches * 2 partition algorithms = 600 unit test cases.
+
+When it is done, a performance file "all[timestamp].csv" should be produced 
+under result/ folder. We include our previous result file 
+"all-time_3333_13_21_34.csv" in the folder. We use this 
+file as example for the next steps.
+
+2. plot the performance graph[Fig 9] using the result file. The file 
+performance graph, named "performance-file.pdf" should be produced 
+under result\ folder.
+
+$ gnuplot -c plot-filewise.gnu result/all-time_3333_13_21_34.csv
+
+
+3. plot the scalability graph[Fig 10] using the result file. The scalability 
+graph, named "scalability.pdf" should be produced under result\ folder.
+
+$ gnuplot -c plot-scalability.gnu result/all-time_3333_13_21_34.csv
+
+4. plot the sequential vs combination graph[Fig 11] using the result file. The 
+comparison graph, named "seq-comb.pdf" should be produced under result\ folder.
+
+$ gnuplot -c plot-seq-comb.gnu result/all-time_3333_13_21_34.csv
+
+
+
+## Reuse 
+****************************
+
+The current implementation provides multiple levels of reuse for future needs.
+
+- Tuning running parameters.
+The complete usage of the code is as follow:
+Usage: test_solver.py [test_file] -op [op]
+	 [test_file]: test file .con; use 'all' to run all the file under tests/
+	 -partt [0-1]: specifying partition algorithm: 0=sequential, 
+				   1=combinational; if not specified, it tests all the partt 
+				   algorithms
+	 -appr [0-3]: specifying approaches: 0=hybrid, 1=early-accept, 2=one-shot,
+				 3=early-reject; if not specified, it tests [0,1,2] approaches.
+	 -time  i : specifying time-out minutes; default i=3 min.
+	 -debug [0-1] : print debug message; default 1 with debug message on.
+
+Example 1: run tests/dsram.con using hybrid solver with sequential partitioning:
+$ python test_solver.py tests/dsram.con -partt 0 -appr 0
+
+Example 2: run all tests file using early-accept with 1 min time-out
+$ python test_solver.py all -appr 1 -time 1
+
+
+- New constraint files.
+New constraints formalized in core constraint language are acceptable if the 
+predicates parts can be understood by Z3. 
+
+Example 3: new constraint file using (2.1) in Figure 1:
+ L <: ax And az <: ax And ax <: L;
+ (d>0) => H <: ay;
+ (Not(d>0)) => L <: ay;
+ (d>0) => H<: ay;
+ (d<0)=> ay<:ax;
+
+User can create a "new.con" file under the tests/ folder with content above and 
+run with any settings in the usage.
+
+
+- Code extension
+The current code follows modular design. Key functionality of a component is 
+implemented in a base class. Extension for parser, lattice, partition algorithm 
+and solver can benefit from the base implementation and not be tangled by other 
+components. Future user can extend the current version with implementation of 
+their own in a straightforward manner. 
+Here is a table for components and classes:
+-----------------------------------------------------------------
+| Components    |    Base class     | Current implementation    |
+| lattice       | Lattice           | TwoPointLattice           |
+| parser        |CoreConstraintParser| LeftJoinParser           |
+| partitioning  |PartitionContext   | SequentialPartition, CombinationPartition|
+| solver        |PartitionDerivationSolver| TestSolver          |
+-----------------------------------------------------------------
+
+Example 4: new partition algorithm, Optimized Combinational Partitioning. The 
+code is available at the end of partt.py(Commented out). 
+1. Implement the functionality:
+__init__(): specify the initial state of the program
+init_partt(): specify the initialization of partition algorithm
+next_partt(): how to generate the next partition. self.stop.partt: keep track 
+of stop condition
+
+In this example, uncomment the line 148-178 in partt.py. 
+
+2. Specify the new options for the extensions.
+Uncomment the Line 24, 29 in globals.py and Line 163,164 in test_solver.py. 
+
+3. Now user can run the new implementation using:
+
+$ python test_solver.py tests/dsram.con -partt 2
+
+"OpCombinationPartition" will show up in the debug message to indicate the new 
+implementation is in use.
+

DerivationSolver_py2/duplicate_remove.py

@@ -0,0 +1,46 @@
+import sys
+
+def process_file(input_file_name, output_file_name):
+    try:
+        with open(input_file_name, 'r') as input_file:
+            lines = input_file.readlines()
+
+        processed_lines = []
+        unique_strings = {}  # Maps unique strings to their lines
+
+        for line in lines:
+            processed_line = line.split(';')[0] + ';\n'
+            if '=>' in processed_line:
+                start_index = processed_line.find('=>') + 3
+                end_index = len(processed_line)  # Assuming ';' was removed
+                unique_string = processed_line[start_index:end_index].strip()
+                # Store or replace the line based on the unique string
+                unique_strings[unique_string] = processed_line
+            else:
+                processed_lines.append(processed_line)
+
+        # Add lines with unique strings between '=>' and ';' to processed_lines
+        for key in unique_strings:
+            if unique_strings[key] not in processed_lines:
+                processed_lines.append(unique_strings[key])
+
+        # Writing to output, ensuring no duplicates
+        final_lines = []
+        for line in processed_lines:
+            if line not in final_lines:
+                final_lines.append(line)
+
+        with open(output_file_name, 'w') as output_file:
+            for line in final_lines:
+                output_file.write(line)
+
+
+    except IOError as e:
+        print "bye"
+if __name__ == "__main__":
+    if len(sys.argv) < 3:
+        print "Usage: python script.py <input_file> <output_file>"
+    else:
+        input_file_name = sys.argv[1]
+        output_file_name = sys.argv[2]
+        process_file(input_file_name, output_file_name)

DerivationSolver_py2/globals.py

@@ -0,0 +1,41 @@
+#     This file is part of Derivation Solver. Derivation Solver provides
+#     implementation of derivation solvers for dependent type inference.
+# 
+#     Copyright (C) 2018  Peixuan Li
+# 
+#     Derivation Solver is free software: you can redistribute it and/or modify
+#     it under the terms of the GNU General Public License as published by
+#     the Free Software Foundation, either version 3 of the License, or
+#     (at your option) any later version.
+#
+#     Derivation Solver is distributed in the hope that it will be useful,
+#     but WITHOUT ANY WARRANTY; without even the implied warranty of
+#     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+#     GNU General Public License for more details.
+#
+#     You should have received a copy of the GNU General Public License
+#     along with Foobar.  If not, see <https://www.gnu.org/licenses/>.
+# 
+DEBUG = 1
+STOP_MIN = 3
+
+SEQ_PARTT = 0
+COMB_PARTT = 1
+# OP_COMB_PARTT = 2
+
+ParttAlg= {}
+ParttAlg[SEQ_PARTT] = "Sequential"
+ParttAlg[COMB_PARTT] = "Combinational"
+# ParttAlg[OP_COMB_PARTT] = "Optimized Combinational"
+
+HYBRID_APPROACH = 0
+EARLY_ACCETP_APPROACH = 1
+EARLY_REJECT_APPROACH = 3
+ONE_SHOT_APPROACH = 2
+
+Approach = {}
+Approach[HYBRID_APPROACH] = "Hybrid"
+Approach[EARLY_ACCETP_APPROACH] = "Early_Accept"
+Approach[EARLY_REJECT_APPROACH] = "Early_Reject"
+Approach[ONE_SHOT_APPROACH] = "One_Shot"
+