Граф коммитов

83 Коммитов

Автор SHA1 Сообщение Дата
Shaz Qadeer 35249eea56 fixed a bug with my last commit
removed unused parameter
2017-01-10 13:07:54 -08:00
Shaz Qadeer f8b9eb7bfb generalized GetOutputModel to take a function for aliasPrefix 2017-01-10 12:13:25 -08:00
clovett 5237519027 Merge 2017-01-09 18:24:26 -08:00
clovett 32f44d0cf0 add strReplace function. 2017-01-09 18:23:05 -08:00
ejackson 3f4a8cf4fb Merge branch 'master' of https://github.com/Microsoft/formula 2016-11-02 12:48:21 -07:00
clovett 5d9850e417 Remove duplicate slash so build works on Unix. 2016-10-11 14:46:00 -07:00
clovett fde40fd1e4 Fix build on Unix. 2016-10-10 17:35:22 -07:00
ejackson cbe9f4154d Merge branch 'master' of https://github.com/Microsoft/formula 2016-10-10 15:12:58 -07:00
clovett a7dd07057a Copy FormulaCodeGeneratorTasks to a VS bin directory so VS doesn't lock the DLL's that are being built by the build. 2016-10-05 20:47:06 -07:00
ejackson 8af375ca61 Exposed rules, fixed bug in downgrader 2016-09-16 11:06:27 -07:00
clovett 02cdb24348 Fix incremental build (return true). 2016-09-13 11:22:40 -07:00
clovett 22afae15b8 Merge branch 'master' of https://github.com/Microsoft/formula 2016-09-13 10:41:33 -07:00
clovett 8f6f5facf8 Fix incremental compile of *.4ml files. 2016-09-13 10:41:26 -07:00
Jianqiao Yang 80805af2b0 fix csproj Condition parsing issue on xbuild for mono 2016-09-09 16:33:15 -07:00
clovett 73c52e1685 Fix incremental compile of *.4ml files. 2016-09-08 16:52:51 -07:00
clovett c1799cbfda Merge branch 'master' of https://github.com/Microsoft/formula 2016-09-07 13:27:12 -07:00
clovett ce8fcedad4 Add FormulaCodeGeneratorTask.Targets. 2016-09-07 13:27:07 -07:00
jq.yang@berkeley.edu dff7bfd21a fix for mono 2016-08-29 15:40:43 -07:00
clovett bea0bc6fb6 Fix Success result from Uninstall. 2016-08-19 18:17:23 -07:00
clovett 55aa3f76ec missed change 2016-08-17 17:39:33 -07:00
clovett afa3cbba95 Add ProgramName to Span.
Remove ToLowerInvariant on Uri's so we can work properly in Linux environments.
Use Uri to normalize slashes and do Uri comparisons.
2016-08-17 17:39:23 -07:00
clovett e22d7d02cc Make z3 build optional, but "build.bat" will build the solver by default. 2016-07-25 19:17:42 -07:00
clovett 95ef93c549 Make "Z3 Solver" an optional part of the build. To build a version that does not depend on Z3 use this command line:
"build -solver false -e".
2016-07-25 18:44:28 -07:00
clovett 6eb795865a Make the Z3 Solver method optional (conditional compilation).
Merge Core.sln and Core64.sln.
2016-07-25 17:32:03 -07:00
Shaz Qadeer b2359205f4 minor bug fix 2016-07-25 17:23:16 -07:00
ejackson 4016e05627 (1) Enabled support for building with VS 2015. (2) Added tunload to unload
tasks from command line. (3) Fixed memory leak in maps due to threadlocal
storage; replaced with spinlocks for thread-safe reads.
2015-11-20 19:28:30 -06:00
ejackson fae5147888 Fixed bug in uninstall 2015-06-08 17:43:12 -07:00
ejackson ce0aa5f531 Fixed bug in propagate 2015-04-28 15:09:37 -07:00
ejackson f0980623f6 Increased amount of inlining 2014-12-24 20:45:04 -08:00
ejackson a940400ccc Removed variable renaming during rule inlining 2014-12-23 23:57:27 -08:00
ejackson aa4cf15c26 Variables are oriented in left-right order 2014-10-27 22:30:01 -07:00
ejackson 0e24ca31e9 Modified stats command to return activations in sorted order 2014-10-22 19:44:06 -07:00
ejackson 71ff2f29c6 Added toOrdinal operator 2014-10-02 17:11:03 -07:00
ejackson bd6a4624bb Fix bug where aliasing lost span data 2014-09-26 12:46:27 -07:00
ejackson fa8f2fc50c Fixed proof enumeration algorithm 2014-09-25 13:04:48 -07:00
ejackson 34d6619ddb Rewrite of proof enumerator 2014-09-24 22:07:05 -07:00
ejackson 1b41678966 Allowed alias prefix to be null in ApplyResult.GetOutputModel, in which case no aliasing 2014-09-11 18:07:19 -07:00
ejackson 7b1d7a8033 added lstReverse 2014-09-11 17:08:55 -07:00
ejackson 89eda778b1 Added rule_Watch to get notifications of rule firings 2014-09-08 13:20:48 -07:00
ejackson 7fb34342e2 Handled locator propagation over rule inlining. Added settings for max
locators per proof and rule classes
2014-08-19 19:14:53 -07:00
ejackson 47cdfb6086 Modified results to enumerate derivations and proofs from non-ground
goals.
2014-08-18 18:08:48 -07:00
ejackson c053f7c368 Added support for locating results of CoreSubRules 2014-08-16 00:24:54 -07:00
ejackson 0ee645cad8 Added locator computations, except for sub rules 2014-08-15 19:33:28 -07:00
ejackson e711dea4a7 Intermediate check-in before refactoring Locator 2014-08-14 12:26:05 -07:00
ejackson e4e5e48ff4 Added locator comparison and default locator 2014-08-11 23:15:57 -07:00
ejackson 388c9d5e9b Added handling for models split over multiple files 2014-08-09 23:55:32 -07:00
ejackson bcc4604d8d Adding logic for converting proofs to line numbers 2014-08-09 19:57:03 -07:00
unknown cdd90a3c52 Action -> System.Action in code generator 2014-08-01 10:55:10 -07:00
ejackson e151f6f462 Modified code generation 2014-05-28 15:45:28 -07:00
ejackson 4c36dd0989 Added rule table optimizations.
Added execution statistics.
Changed printer for type expressions.
Added "stats" command.
2014-04-09 10:17:15 -07:00