Leonardo de Moura
|
4bf9fc2cf5
|
refactor(library/blast): move simple_strategy to strategies folder
We will add more strategies in the future.
|
2015-12-04 11:46:56 -08:00 |
|
Leonardo de Moura
|
73622150a6
|
refactor(library/blast): move actions to actions folder
to make Daniel happy.
|
2015-12-04 10:00:04 -08:00 |
|
Daniel Selsam
|
6e478696d2
|
feat(library/blast/unit): preprocessor placeholder
|
2015-12-04 08:30:04 -08:00 |
|
Leonardo de Moura
|
2296168bda
|
feat(library/blast): add blast.ematch option, and ematching search procedure
|
2015-12-02 22:52:54 -08:00 |
|
Daniel Selsam
|
46e60abda6
|
feat(library/blast/forward): branch extension
|
2015-11-23 13:58:13 -08:00 |
|
Daniel Selsam
|
a8700e6778
|
refactor(library/blast/unit): rename unit propagation module
|
2015-11-23 13:58:13 -08:00 |
|
Leonardo de Moura
|
b442fe66b2
|
chore(library/blast/simple_strategy): fix style
|
2015-11-22 18:24:59 -08:00 |
|
Leonardo de Moura
|
0fcf8ed7d2
|
refactor(library/blast): hypothesis activation protocol
|
2015-11-22 18:22:26 -08:00 |
|
Leonardo de Moura
|
1bd827dffc
|
feat(library/blast/simplifier/simplifier_actions): add simplify_hypothesis_action
|
2015-11-22 17:49:00 -08:00 |
|
Leonardo de Moura
|
028a2ab785
|
feat(library/blast): add get_config()
|
2015-11-20 10:39:26 -08:00 |
|
Daniel Selsam
|
21cb409e6c
|
refactor(library/blast/simplifier): move simplifier module into blast
|
2015-11-19 19:43:04 -08:00 |
|
Leonardo de Moura
|
2d93fe4b76
|
feat(library/blast/congruence_closure): implement congruence closure
Proof extraction is still missing
|
2015-11-19 19:37:11 -08:00 |
|
Leonardo de Moura
|
ee3083c12c
|
feat(library/blast): add action based on congruence closure module
|
2015-11-19 12:30:45 -08:00 |
|
Daniel Selsam
|
5ada4312d7
|
feat(library/blast/forward): propositional forward chaining
|
2015-11-19 11:44:53 -08:00 |
|
Leonardo de Moura
|
aa1451888c
|
fix(library/blast): spurious trace messages, typo
|
2015-11-18 19:12:29 -08:00 |
|
Daniel Selsam
|
413989afd6
|
feat(library/blast/backward): backward chaining strategy
|
2015-11-18 17:48:39 -08:00 |
|
Leonardo de Moura
|
bf5fe8d180
|
feat(library/blast): add trace module
|
2015-11-18 12:59:53 -08:00 |
|
Leonardo de Moura
|
453e90261b
|
refactor(library/blast): make sure all actions return action_result, add macros for simplifying strategy definition
revert is not an action, but a procedure for helping us to build actions.
|
2015-11-18 12:29:43 -08:00 |
|
Leonardo de Moura
|
60945e95b4
|
feat(library/blast): add 'discard' action for detecting irrelevant hypotheses
|
2015-11-16 11:43:51 -08:00 |
|
Leonardo de Moura
|
db59c6829c
|
feat(library/blast): add basic support for non-recursive recursors/eliminators in the simple_strategy, fix bug at recursor_action
|
2015-11-15 18:39:12 -08:00 |
|
Leonardo de Moura
|
24ed427c2f
|
feat(library/blast): add "recursor" (aka elimination/induction) action
|
2015-11-15 18:00:32 -08:00 |
|
Leonardo de Moura
|
9e8627380a
|
chore(library/blast/simple_strategy): fix style
|
2015-11-15 15:08:01 -08:00 |
|
Leonardo de Moura
|
ffd0c2b09a
|
refactor(library/blast/simple_strategy): eliminate duplicated code
|
2015-11-15 14:30:24 -08:00 |
|
Leonardo de Moura
|
4cd5e18bd0
|
refactor(library/blast): add strategy abstract object
|
2015-11-15 13:12:21 -08:00 |
|
Leonardo de Moura
|
fd41a4f76d
|
feat(library/blast): add simplify_target action
|
2015-11-14 16:18:12 -08:00 |
|
Leonardo de Moura
|
b5db77961d
|
feat(library/blast): add "trivial" action
|
2015-11-14 15:02:14 -08:00 |
|
Leonardo de Moura
|
0803db21d3
|
refactor(library/blast): add "_action" suffix to files defining actions
|
2015-11-14 13:22:12 -08:00 |
|
Leonardo de Moura
|
9921228dd5
|
feat(library/blast): add simp_rule_sets to branch
|
2015-11-14 13:16:00 -08:00 |
|
Leonardo de Moura
|
0f4e59a84f
|
feat(library/blast): add "no_confusion" action
|
2015-11-13 18:19:05 -08:00 |
|
Leonardo de Moura
|
6c038626f8
|
fix(library/blast/simple_strategy): tracing
|
2015-11-13 15:22:09 -08:00 |
|
Leonardo de Moura
|
ca4c078089
|
feat(library/blast): add "subst" action
|
2015-11-13 15:21:26 -08:00 |
|
Leonardo de Moura
|
bc8c5a3f68
|
feat(library/blast): basic tracing for blast
|
2015-11-13 13:05:20 -08:00 |
|
Leonardo de Moura
|
2e32cf51f9
|
feat(library/blast/state): do not track dependecies to values
|
2015-11-13 10:38:25 -08:00 |
|
Leonardo de Moura
|
fee0cff295
|
feat(library/blast): add simple indexing data-structure for active hypotheses
|
2015-11-11 00:02:47 -08:00 |
|
Leonardo de Moura
|
f8f3f9402e
|
feat(library/blast): major reorg and basic backward chaining action
|
2015-11-10 17:00:16 -08:00 |
|
Leonardo de Moura
|
6f01a7339a
|
refactor(library/blast): move simple search strategy to separate module
|
2015-11-10 11:44:18 -08:00 |
|